ea6c957030 
								
							
								 
							
						 
						
							
							
								
								tests for multi-dimensional cost bounded DTMCs  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								dbcc49f48f 
								
							
								 
							
						 
						
							
							
								
								Use new carl release 17.12  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								945e360bcf 
								
							
								 
							
						 
						
							
							
								
								Increased minimal carl version to 17.10  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f6eadc14ca 
								
							
								 
							
						 
						
							
							
								
								adding proper carl_DIR when using shipped carl  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a8caaf83c2 
								
							
								 
							
						 
						
							
							
								
								made passing carl to sylvan more robust  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								1460e8f969 
								
							
								 
							
						 
						
							
							
								
								proper forwarding of Boost include directories to sylvan CMakeLists.txt  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								64a0d7ec3a 
								
							
								 
							
						 
						
							
							
								
								added missing file  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								7d65bd5e2e 
								
							
								 
							
						 
						
							
							
								
								fixing carl version check  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								58c8531d34 
								
							
								 
							
						 
						
							
							
								
								Use Carl 17.10  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								3185719fe5 
								
							
								 
							
						 
						
							
							
								
								fix for linking issue under linux, adding missing l3pp dependency l3pp_ext  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								02c23865da 
								
							
								 
							
						 
						
							
							
								
								reworked memory leak solution in sylvan according to Tom van Dijks hints  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								72d58b6155 
								
							
								 
							
						 
						
							
							
								
								fix for sylvan workers not releasing mmap'ed memory  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								1f16008b75 
								
							
								 
							
						 
						
							
							
								
								added proper exception handling to sylvan-based sharpening  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								45a4b63a2e 
								
							
								 
							
						 
						
							
							
								
								fixed some issue in sylvan sharpen and forward minmax bounds to linear equation solver  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f2e581b3df 
								
							
								 
							
						 
						
							
							
								
								rational search for symbolic linear equation solvers  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								b09cb95254 
								
							
								 
							
						 
						
							
							
								
								fixed wrong call in sylvan double to rational number conversion  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								da02237769 
								
							
								 
							
						 
						
							
							
								
								work towards symbolic rational search  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6e8465e9f1 
								
							
								 
							
						 
						
							
							
								
								started on symbolic rational search  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4626aa0e69 
								
							
								 
							
						 
						
							
							
								
								Updated search for mathsat in cmake and fixed linker problem  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e719a37c6c 
								
							
								 
							
						 
						
							
							
								
								fixes related to relative termination criterion  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								ade8078759 
								
							
								 
							
						 
						
							
							
								
								added test for lower bounded properties  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								bac50a32ab 
								
							
								 
							
						 
						
							
							
								
								warkaround for gcc 7.2.0: make modernjson compile again  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								c5134c364f 
								
							
								 
							
						 
						
							
							
								
								Extraction and update of TBB-parallelized stuff  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								c77b9ce404 
								
							
								 
							
						 
						
							
							
								
								gauss-seidel style multiplication for gmm++  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								43643b9699 
								
							
								 
							
						 
						
							
							
								
								bump gmm++ version to 5.2 (from 5.0)  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f7c803827b 
								
							
								 
							
						 
						
							
							
								
								remove debug output  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4adee85fa5 
								
							
								 
							
						 
						
							
							
								
								added checking requirements of MinMax solvers to model checker helpers  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								591a53582a 
								
							
								 
							
						 
						
							
							
								
								fixed test  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e1aba323bf 
								
							
								 
							
						 
						
							
							
								
								more tests for reward unfolding  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								172b17d7ae 
								
							
								 
							
						 
						
							
							
								
								simple testcase for the reward unfolding  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e2e1407f3e 
								
							
								 
							
						 
						
							
							
								
								not calling sylvan_var on leaf nodes of sylvan anymore  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								6bebb3c9d5 
								
							
								 
							
						 
						
							
							
								
								fix bug in rational number/function handling with sylvan  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								a7dcdcd84d 
								
							
								 
							
						 
						
							
							
								
								started on tests and added a ton of debug output  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								40a982430c 
								
							
								 
							
						 
						
							
							
								
								cmake for carl: handle situation where carl version information is missing  
							
							
 
							
							
							Older carl versions don't provide detailed version information, so we
provide an informative error message instead of cmake syntax errors during
the comparison. 
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								eaee50f077 
								
							
								 
							
						 
						
							
							
								
								fixed bug, implemented new sparse quotient extraction for sylvan  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d23547d99f 
								
							
								 
							
						 
						
							
							
								
								started optimizing some DdManager methods  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								75ec21b1d6 
								
							
								 
							
						 
						
							
							
								
								remove USE_CARL variable and add option to take hint for carl directory  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								c639f39076 
								
							
								 
							
						 
						
							
							
								
								require carl version 17.08  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								9a20aed7f9 
								
							
								 
							
						 
						
							
							
								
								proper caching in all min/max/exists abstract representative functions  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								cdf76b0c15 
								
							
								 
							
						 
						
							
							
								
								fixed DD-based quotient extraction in bisimulation  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								18ba906914 
								
							
								 
							
						 
						
							
							
								
								re-added gmp include directory to sylvan CMakeLists.txt  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								d0cf2ef57b 
								
							
								 
							
						 
						
							
							
								
								update to version 1.4.0 of sylvan  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4492f428bb 
								
							
								 
							
						 
						
							
							
								
								worked in fix to Cudd_addMinus suggested by Fabio Somenzi  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								f5ba5204c9 
								
							
								 
							
						 
						
							
							
								
								adding some debug functionality to DdManager to corner dynamic reordering issue with CUDD  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								bda9a797e8 
								
							
								 
							
						 
						
							
							
								
								fixed some issues in CUDD (fixes provided by Fabio Somenzi)  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								66e1cf8bd6 
								
							
								 
							
						 
						
							
							
								
								Add support for Fedora's z3 package.  
							
							
 
							
							
							Fedora installs the z3 headers in /usr/include/z3, which was not being
detected by CMake.
Signed-off-by: dehnert <dehnert@cs.rwth-aachen.de> 
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								52b07a0c2f 
								
							
								 
							
						 
						
							
							
								
								fixed a bug in sparse matrix builder, fixed some tests  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								4c3a409961 
								
							
								 
							
						 
						
							
							
								
								readd sparsepp in new version  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								5bdbc00bcd 
								
							
								 
							
						 
						
							
							
								
								Changed carlConfig path for shipped carl  
							
							
								
 
							
							
						 
						8 years ago  
				
					
						
							
							
								 
						
							
							
							
								
							
								e4783846e0 
								
							
								 
							
						 
						
							
							
								
								Changed carlConfig path for shipped carl  
							
							
								
 
							
							
						 
						8 years ago