dehnert
bda9a797e8
fixed some issues in CUDD (fixes provided by Fabio Somenzi)
9 年前
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>
9 年前
dehnert
52b07a0c2f
fixed a bug in sparse matrix builder, fixed some tests
9 年前
dehnert
4c3a409961
readd sparsepp in new version
9 年前
Matthias Volk
5bdbc00bcd
Changed carlConfig path for shipped carl
9 年前
Matthias Volk
e4783846e0
Changed carlConfig path for shipped carl
9 年前
Matthias Volk
9ad4203b09
Export to cmake for shipped carl
9 年前
Sebastian Junges
56616f1e26
trying to clarify sylvan dependency on carl
9 年前
Sebastian Junges
c46ce03e60
make storm compile with latest version of carl
9 年前
Sebastian Junges
bec6b664d9
actually check carl version, error if outdated
9 年前
dehnert
e5cbc25f00
properly installing dylib resulting from shipped carl build (now considers carl version)
9 年前
dehnert
e8fab0718c
fixed issues in division operations of sylvan for rational numbers and rational functions (division by zero not correctly handled)
9 年前
dehnert
44d582dc65
added more output about CArL when it's found on the system
9 年前
dehnert
cebd3d252d
fixed include directory (cmake) for shipped carl
9 年前
dehnert
818bf8e447
added gurobi70 to FindGurobi.cmake
9 年前
dehnert
de2646b082
This commit fixes issue #5 related to Gurobi not being linked properly when requested.
9 年前
Matthias Volk
f5c327a10e
Boost must be set for shipped carl
9 年前
dehnert
ea02ea0838
started overhaul of cli/api
9 年前
Matthias Volk
b76ee0210a
Fixed setting cmake flags for building shipped carl
9 年前
Matthias Volk
a9d6d80ef0
Warning in cmake if Z3 is not found
9 年前
TimQu
0cdd32ff9f
added two test cases for the drn parser
9 年前
TimQu
1ce122a0d6
fixed compile issue related to ambiguous call of operator<<
9 年前
TimQu
722e67fe64
parsing choice labels for explicit models
9 年前
Sebastian Junges
87f494627c
Fixes after carl update in order to get ginac from carl.
9 年前
dehnert
8f42bd2ec0
moved to new sparsepp version and made the appropriate changes
9 年前
Sebastian Junges
ed2a1dc1de
CMake now ensures that carl is not only configured, but also built and thereby prevents compilation-time errors.
10 年前
Sebastian Junges
920d48c2bd
storm config version now also correctly exported
10 年前
Sebastian Junges
92f04cdfa1
CppTemplate was not correctly listed as a dependency of storm.
10 年前
TimQu
5f120fd5bb
Fixed enabling CLN when there is no system version of carl
10 年前
dehnert
28e91b8d0f
more work on symbolic bisimulation
10 年前
dehnert
03ad4c2783
first version of symbolic bisimulation minimization
10 年前
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
10 年前
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
10 年前
dehnert
86a783de92
two more fixes for issues pointed out by Tim: concurrency bug in sylvan and bug in symbolic quantitative check result
10 年前
ArashPartow
4c99790213
Minor updates to ExprTk
Updated unknown symbol resolver interface to handle all types (scalar, string and vector)
Added compile-time check for vector indexing when using constant values
Added return statement enable/disable via parser settings
Added exprtk_disable_return_statement macro for disabling return statements and associated exceptions at the source code level.
10 年前
sjunges
977dd1ef53
Get GMP location from carl, set it as a hint for sylvan.
10 年前
sjunges
1c22fdabe1
Edit in Sylvan/cmake: Allow for hints about gmp location
10 年前
dehnert
97a7689c67
gcc and clang working on Debian Stretch again
10 年前
dehnert
6d9e906291
remove LTO from sylvan as it causes more problems than it solves
10 年前
dehnert
ec3468aef5
hopefully fixed the compile issue on Linux
10 年前
sjunges
8bfa699519
attempt to fix link error
10 年前
dehnert
187e8bc52b
fixed two bugs related to hybrid quantitative results
10 年前
ArashPartow
2cdda140b8
Minor updates to ExprTk
Updated multi-sub expression operator to return final sub-expression type.
Updates to exprtk_disable_return_statement macro for disabling return statements and associated exceptions at the source code level.
10 年前
TimQu
de87ff1152
fixed finding of z3 library when its location is given via -DZ3_ROOT
10 年前
dehnert
becc43e1e1
added wokaround proposed by jklein to make the new sylvan version build on older osx
10 年前
dehnert
853b035473
fixed bug and added testsfor symbolic linear equation solver (rational number and rational function)
10 年前
dehnert
f6e194592f
remove always building sylvan
10 年前
dehnert
0135793c44
update to newest sylvan version
10 年前
dehnert
153339c5be
first draft of policy iteration using DDs
10 年前
dehnert
952776a057
hybrid engine working for rational numbers
10 年前