Matthias Volk
263e6ed5f8
Removed generated files from git
7 years ago
Matthias Volk
df1571d737
Added more DFT tests
7 years ago
Matthias Volk
2c9f6294a4
Started on DFT regression tests
7 years ago
dehnert
a5bc5d30e5
added new gurobi version to find script
7 years ago
dehnert
01dc240eea
fixed checking carl version
7 years ago
dehnert
4591dba631
made maxsat-based counterexample generation be applicable to DTMCs and MDPs
7 years ago
dehnert
676120229b
intermediate stage
7 years ago
TimQu
ea6c957030
tests for multi-dimensional cost bounded DTMCs
7 years ago
Matthias Volk
dbcc49f48f
Use new carl release 17.12
7 years ago
Matthias Volk
945e360bcf
Increased minimal carl version to 17.10
7 years ago
dehnert
f6eadc14ca
adding proper carl_DIR when using shipped carl
7 years ago
dehnert
a8caaf83c2
made passing carl to sylvan more robust
7 years ago
dehnert
1460e8f969
proper forwarding of Boost include directories to sylvan CMakeLists.txt
7 years ago
TimQu
64a0d7ec3a
added missing file
7 years ago
dehnert
7d65bd5e2e
fixing carl version check
7 years ago
Matthias Volk
58c8531d34
Use Carl 17.10
7 years ago
dehnert
3185719fe5
fix for linking issue under linux, adding missing l3pp dependency l3pp_ext
7 years ago
dehnert
02c23865da
reworked memory leak solution in sylvan according to Tom van Dijks hints
7 years ago
dehnert
72d58b6155
fix for sylvan workers not releasing mmap'ed memory
7 years ago
dehnert
1f16008b75
added proper exception handling to sylvan-based sharpening
7 years ago
dehnert
45a4b63a2e
fixed some issue in sylvan sharpen and forward minmax bounds to linear equation solver
7 years ago
dehnert
f2e581b3df
rational search for symbolic linear equation solvers
7 years ago
dehnert
b09cb95254
fixed wrong call in sylvan double to rational number conversion
7 years ago
dehnert
da02237769
work towards symbolic rational search
7 years ago
dehnert
6e8465e9f1
started on symbolic rational search
7 years ago
Matthias Volk
4626aa0e69
Updated search for mathsat in cmake and fixed linker problem
7 years ago
dehnert
e719a37c6c
fixes related to relative termination criterion
7 years ago
TimQu
ade8078759
added test for lower bounded properties
7 years ago
dehnert
bac50a32ab
warkaround for gcc 7.2.0: make modernjson compile again
7 years ago
dehnert
c5134c364f
Extraction and update of TBB-parallelized stuff
7 years ago
dehnert
c77b9ce404
gauss-seidel style multiplication for gmm++
7 years ago
dehnert
43643b9699
bump gmm++ version to 5.2 (from 5.0)
7 years ago
dehnert
f7c803827b
remove debug output
7 years ago
dehnert
4adee85fa5
added checking requirements of MinMax solvers to model checker helpers
7 years ago
TimQu
591a53582a
fixed test
7 years ago
TimQu
e1aba323bf
more tests for reward unfolding
7 years ago
TimQu
172b17d7ae
simple testcase for the reward unfolding
7 years ago
dehnert
e2e1407f3e
not calling sylvan_var on leaf nodes of sylvan anymore
7 years ago
dehnert
6bebb3c9d5
fix bug in rational number/function handling with sylvan
7 years ago
dehnert
a7dcdcd84d
started on tests and added a ton of debug output
7 years ago
Joachim Klein
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.
7 years ago
dehnert
eaee50f077
fixed bug, implemented new sparse quotient extraction for sylvan
7 years ago
dehnert
d23547d99f
started optimizing some DdManager methods
7 years ago
dehnert
75ec21b1d6
remove USE_CARL variable and add option to take hint for carl directory
7 years ago
Sebastian Junges
c639f39076
require carl version 17.08
7 years ago
dehnert
9a20aed7f9
proper caching in all min/max/exists abstract representative functions
7 years ago
dehnert
cdf76b0c15
fixed DD-based quotient extraction in bisimulation
7 years ago
dehnert
18ba906914
re-added gmp include directory to sylvan CMakeLists.txt
7 years ago
dehnert
d0cf2ef57b
update to version 1.4.0 of sylvan
7 years ago
dehnert
4492f428bb
worked in fix to Cudd_addMinus suggested by Fabio Somenzi
7 years ago