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
dehnert
f5ba5204c9
adding some debug functionality to DdManager to corner dynamic reordering issue with CUDD
7 years ago
dehnert
bda9a797e8
fixed some issues in CUDD (fixes provided by Fabio Somenzi)
7 years ago
Enno Ruijters
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>
7 years ago
dehnert
52b07a0c2f
fixed a bug in sparse matrix builder, fixed some tests
7 years ago
dehnert
4c3a409961
readd sparsepp in new version
7 years ago
Matthias Volk
5bdbc00bcd
Changed carlConfig path for shipped carl
7 years ago
Matthias Volk
e4783846e0
Changed carlConfig path for shipped carl
7 years ago
Matthias Volk
9ad4203b09
Export to cmake for shipped carl
7 years ago
Sebastian Junges
56616f1e26
trying to clarify sylvan dependency on carl
7 years ago
Sebastian Junges
c46ce03e60
make storm compile with latest version of carl
7 years ago
Sebastian Junges
bec6b664d9
actually check carl version, error if outdated
8 years ago
dehnert
e5cbc25f00
properly installing dylib resulting from shipped carl build (now considers carl version)
8 years ago
dehnert
e8fab0718c
fixed issues in division operations of sylvan for rational numbers and rational functions (division by zero not correctly handled)
8 years ago
dehnert
44d582dc65
added more output about CArL when it's found on the system
8 years ago
dehnert
cebd3d252d
fixed include directory (cmake) for shipped carl
8 years ago
dehnert
818bf8e447
added gurobi70 to FindGurobi.cmake
8 years ago
dehnert
de2646b082
This commit fixes issue #5 related to Gurobi not being linked properly when requested.
8 years ago
Matthias Volk
f5c327a10e
Boost must be set for shipped carl
8 years ago
dehnert
ea02ea0838
started overhaul of cli/api
8 years ago
Matthias Volk
b76ee0210a
Fixed setting cmake flags for building shipped carl
8 years ago
Matthias Volk
a9d6d80ef0
Warning in cmake if Z3 is not found
8 years ago
TimQu
0cdd32ff9f
added two test cases for the drn parser
8 years ago
TimQu
1ce122a0d6
fixed compile issue related to ambiguous call of operator<<
8 years ago
TimQu
722e67fe64
parsing choice labels for explicit models
8 years ago
Sebastian Junges
87f494627c
Fixes after carl update in order to get ginac from carl.
8 years ago
dehnert
8f42bd2ec0
moved to new sparsepp version and made the appropriate changes
8 years ago
Sebastian Junges
ed2a1dc1de
CMake now ensures that carl is not only configured, but also built and thereby prevents compilation-time errors.
8 years ago
Sebastian Junges
920d48c2bd
storm config version now also correctly exported
8 years ago
Sebastian Junges
92f04cdfa1
CppTemplate was not correctly listed as a dependency of storm.
8 years ago
TimQu
5f120fd5bb
Fixed enabling CLN when there is no system version of carl
8 years ago
dehnert
28e91b8d0f
more work on symbolic bisimulation
8 years ago
dehnert
03ad4c2783
first version of symbolic bisimulation minimization
8 years ago
TimQu
8c6b22bebc
Incremented minimal z3 version required for the z3LpSolver to 4.5.0 as the optimizer in 4.4.1 yielded wrong results in the tests
8 years ago
TimQu
1a9589dfa6
Incremented minimal z3 version required for the z3LpSolver to 4.5.0 as the optimizer in 4.4.1 yielded wrong results in the tests
8 years ago
dehnert
86a783de92
two more fixes for issues pointed out by Tim: concurrency bug in sylvan and bug in symbolic quantitative check result
8 years ago