Sebastian Junges
c46ce03e60
make storm compile with latest version of carl
8 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
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.
8 years ago
sjunges
977dd1ef53
Get GMP location from carl, set it as a hint for sylvan.
8 years ago
sjunges
1c22fdabe1
Edit in Sylvan/cmake: Allow for hints about gmp location
8 years ago
dehnert
97a7689c67
gcc and clang working on Debian Stretch again
8 years ago
dehnert
6d9e906291
remove LTO from sylvan as it causes more problems than it solves
8 years ago
dehnert
ec3468aef5
hopefully fixed the compile issue on Linux
8 years ago
sjunges
8bfa699519
attempt to fix link error
8 years ago
dehnert
187e8bc52b
fixed two bugs related to hybrid quantitative results
8 years ago
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.
8 years ago
TimQu
de87ff1152
fixed finding of z3 library when its location is given via -DZ3_ROOT
8 years ago
dehnert
becc43e1e1
added wokaround proposed by jklein to make the new sylvan version build on older osx
8 years ago
dehnert
853b035473
fixed bug and added testsfor symbolic linear equation solver (rational number and rational function)
8 years ago
dehnert
f6e194592f
remove always building sylvan
8 years ago
dehnert
0135793c44
update to newest sylvan version
8 years ago
dehnert
153339c5be
first draft of policy iteration using DDs
8 years ago
dehnert
952776a057
hybrid engine working for rational numbers
8 years ago
dehnert
ee90c51b2a
cleaned up constants.cpp to finalize separation of rational functions and rational numbers
8 years ago
dehnert
aaa6f13cf4
separated rational numbers and rational functions and added support for rational numbers to sylvan
8 years ago
dehnert
acd486f0f2
reverted a change in ExprTk: dots are no longer recognized as letters
8 years ago
dehnert
0354c9024a
moved to new sylvan version and made everything work again
8 years ago
dehnert
2e8ff870ff
completed interface of (sylvan) ADDs for storing rational functions
8 years ago
TimQu
c4dffe9a8b
tests for step bounded properties
8 years ago
TimQu
24bc53549c
more tests on pmdps and fixes
8 years ago
dehnert
3f0afe9526
allowing underscore and dots as identifier symbols in exprtk
8 years ago