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
sjunges
1c22fdabe1
Edit in Sylvan/cmake: Allow for hints about gmp location
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
dehnert
187e8bc52b
fixed two bugs related to hybrid quantitative results
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
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
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
Sebastian Junges
5bfb6b817a
sylvan is now compiled with c++14 as it depends on c++14 code now (change in carl)
8 years ago
dehnert
77bd6e4a44
fixed some model building issues
8 years ago
Sebastian Junges
b865f9f2bd
sylvan builds with shipped carl
8 years ago
Sebastian Junges
b0ccd7a22f
removed double entry of include_directory in sylvan cmake
8 years ago
Philipp Berger
6d49f8cc60
Fixed include path for storm-config.h
8 years ago
dehnert
1ce5068694
fixed include dir in sylvan
8 years ago
Philipp Berger
822ae6be40
Fixes
8 years ago
Philipp Berger
da69e8d9b7
Cherry-picked changes.
8 years ago
dehnert
1f460cd8fa
made move of top-level dir for some remaining files, fixed some includes
8 years ago
Mavo
7e620e9549
Link sylvan with gmp
Former-commit-id: 8cbfec4bc3
9 years ago
dehnert
f0f9831ac3
reworked CMake stuff a bit, removed some superfluous things
Former-commit-id: 16df6afd44
[formerly f27354d54c
]
Former-commit-id: 3e706797be
8 years ago
PBerger
d76e9729da
Leave Replacement finally working.
Former-commit-id: 239ea6d897
8 years ago
PBerger
c9f2eef826
Added functionality for replacing leaves in SRF MTBDDs.
Former-commit-id: d7af779036
8 years ago
PBerger
d3c492124a
Fixed min/max Abstract w. repr.
Finally.
Former-commit-id: 1ccc06d924
8 years ago
PBerger
da199866e6
Added tests for minAbstractRepresentative.
Everything still in early alpha. Expect Debug output.
Former-commit-id: 2712fce4dd
8 years ago
PBerger
68b14b3076
Moved BDD functionality in Sylvan to sylvan_bdd_int.h to allow reuse.
Added min/maxExistsRepresentative API to storage/dd/Add.
Former-commit-id: 45ff98b35a
8 years ago
dehnert
8b29ab079c
fixed some bugs in custom cudd functions
Former-commit-id: b73b894674
8 years ago
PBerger
73a3461650
Fixed CUDD and Sylvan existsRepresentative.
Former-commit-id: e3ec69ab37
8 years ago
PBerger
c184f6a541
Worked on Sylvan min/max ADD abstract w. representative.
More tests for existsRepr.
Former-commit-id: 08c5d6e9bb
8 years ago
PBerger
e45b3d2940
Fixed Sylvan implementation of existsAbstractRepresentative.
Added more tests.
Former-commit-id: 6a4003bb5e
8 years ago
PBerger
be7353358f
Added Test for constants in Cudd/Sylvan.
Added functionality for existsAbstractRepresentative in Sylvan. Still very broken!
Former-commit-id: df2b36a8d8
8 years ago
PBerger
4fff7b39ef
Added template instanziation for storm::RationalFunction.
Added a test for Prism AbstractPrograms with storm::RationalFunction.
Former-commit-id: 5a696149cb
8 years ago
PBerger
0717ffe053
Added AND_EXISTS to sylvan+RationalFunction
Former-commit-id: 7b462145cf
8 years ago
PBerger
9eee889539
Added missing parameter to #ifdef - its gettings late.
Former-commit-id: 4c2ab46ed5
8 years ago
PBerger
867de852ab
Added the conditional debug output in the wrapper to the tracked code.
Former-commit-id: adb9cebbd5
8 years ago
PBerger
58eb54926c
Fixed Sylvan bugs.
Added a lot of debugging options and output, controlled by #define's.
Added more template specializations for storm::RationalFunction.
Former-commit-id: 416c32d196
8 years ago
PBerger
bc7e533d6b
Some debug,
Former-commit-id: aed81724ca
8 years ago
PBerger
6ced56a0cc
More ptr fixes.
Former-commit-id: f1f01a0eec
8 years ago
PBerger
1345f018fc
Fixed some issues with pointers.
Former-commit-id: a7fddc12f3
8 years ago
PBerger
9e90f41608
Implemented functions for BDD -> ADD conversion and some helpers.
Former-commit-id: 78c9003366
8 years ago
PBerger
157c9f4f5a
Reverted MINONE change.
Former-commit-id: 047c8175aa
8 years ago
PBerger
c4b7d778f3
Add MINONE macro back into lace.h
Former-commit-id: 8eb55b63c2
8 years ago
PBerger
fb4bfd724d
Reverted lace.h back to find the regression.
Former-commit-id: 03d4d796f3
8 years ago
PBerger
ca65cecbfd
Fixed a few of Sylvans nasty habits.
Former-commit-id: e965a8f613
8 years ago
PBerger
e0647f34eb
Added missing template instantiation.
Added missing function implementation for sylvan OPs.
Former-commit-id: fb10555ca3
8 years ago
PBerger
c8262a3022
Added function for retrieving the ID of the custom leaves.
Former-commit-id: 615cacf3b9
9 years ago