sjunges
|
f65efdb4bb
|
disable smtrat for now
Former-commit-id: 4f63d4cd05
|
9 years ago |
sjunges
|
dbe4380b09
|
Option to force color output for clang/ninja.
Former-commit-id: c0fb2ac6a7
|
9 years ago |
sjunges
|
9254e6650c
|
Option to force color output for clang/ninja.
Former-commit-id: 89e960b383
|
9 years ago |
sjunges
|
bed31b463f
|
Added generated sources
Former-commit-id: b19af1f416
|
9 years ago |
dehnert
|
7cafd61c38
|
switched gcc to use c++14 as well
Former-commit-id: 32d9c46192
|
9 years ago |
sjunges
|
1d5faef301
|
cmake use carl flag
Former-commit-id: 75ff508329
|
9 years ago |
dehnert
|
21d9e91586
|
work towards interval reward model
Former-commit-id: 24f7e9684f
|
9 years ago |
sjunges
|
31ed578e2c
|
Xcode generation fix.
Former-commit-id: 345be05301
|
9 years ago |
sjunges
|
f219437acf
|
Faster compilation times!
Former-commit-id: a8dc8fa612
|
9 years ago |
sjunges
|
7b79725421
|
Allow hints for z3
Former-commit-id: 24885ab1bc
|
9 years ago |
dehnert
|
b94e978843
|
another round of fixes
Former-commit-id: 67f4e4be47
|
9 years ago |
dehnert
|
a9142a752d
|
fixed another bug
Former-commit-id: 2f0eb64b6f
|
9 years ago |
dehnert
|
b56766e993
|
more work on reward model that turned out to be refactoring in disguise
Former-commit-id: 31a7fa4801
|
9 years ago |
sjunges
|
c7becb3c60
|
improved cmake for z3 and gurobi
Former-commit-id: d85982abd2
|
9 years ago |
sjunges
|
72784d752d
|
permissive schedulers - ongoing work
Former-commit-id: 0f637998c6
|
9 years ago |
dehnert
|
bb7d4c3b0e
|
update for gmm++: 4.2 to 5.0
Former-commit-id: 542b048470
|
9 years ago |
dehnert
|
56b4f53ce7
|
got rid of more warnings
Former-commit-id: 5c39f63c69
|
9 years ago |
dehnert
|
04f789619c
|
some work towards eliminating compiler warnings
Former-commit-id: d1eca470a4
|
9 years ago |
dehnert
|
21627fbab4
|
Started to get rid of some warnings. In particular this means making the compiler more silent for third-party stuff.
Former-commit-id: 2b6ca07d06
|
9 years ago |
sjunges
|
613724fa9f
|
fix
Former-commit-id: 2e0bdc1268
|
9 years ago |
sjunges
|
9c0b5b028c
|
Finding z3 in system, cleaned some cmakelists.
Former-commit-id: 67ab9f7a0c
|
9 years ago |
sjunges
|
5fddb47a91
|
some cleaning and extra comments in the CMakeLists
Former-commit-id: 95b2bc6d30
|
9 years ago |
sjunges
|
37eacf574b
|
Further work on state space generation
Former-commit-id: 3c0c4c016d
|
9 years ago |
sjunges
|
50136dd31a
|
Improved import of carl/smtrat
Former-commit-id: d5ead06024
|
10 years ago |
Sebastian Junges
|
fab39f1ac2
|
Finding smtrat via their new export version
Former-commit-id: e261755b9e
|
10 years ago |
dehnert
|
913aa83dbc
|
Removed ltl2dstar.
Former-commit-id: 2045babf36
|
10 years ago |
dehnert
|
eb5d4100a6
|
Renamed Nondeterminstic equation solver as this name is more than misleading.
Former-commit-id: 7f08ed130c
|
10 years ago |
dehnert
|
239caf57eb
|
Added symbolic models and made DD-based model generator build the correct instances.
Former-commit-id: c054401cfd
|
10 years ago |
dehnert
|
a1dae8849e
|
Reworked (sparse) model files: moved them into their own namespace and deleted some functionality that is never used and not that nicely implemented.
Former-commit-id: d4e6df30b5
|
10 years ago |
David_Korzeniewski
|
8ebc0e4640
|
Final touches on cuda nondeterministic linear equation solver & modelchecker
Former-commit-id: c549ae0401
|
10 years ago |
David_Korzeniewski
|
ea2e616196
|
All tests for CUDA based TopologicalValueIterationMdpPrctlModelChecker passing on Windows.
Former-commit-id: 68cafa6f84
|
10 years ago |
dehnert
|
f0b591be77
|
Further work on reintegrating parametric model checking into main executable.
Former-commit-id: be95ce2722
|
10 years ago |
David_Korzeniewski
|
90958bb018
|
cuda library was not linked to tests, for now using static libraries as dlls don't work for non obvious reasons
Former-commit-id: a1cfba331f
|
10 years ago |
PBerger
|
e211e269d4
|
Fix for the Gurobi inclusion.
Former-commit-id: 232a806b4e
|
10 years ago |
PBerger
|
f7adf54be3
|
Added A FindGurobi file for CMake.
Adapted build process to use the new file to support all version of the library (upgrading to 6.0 breaks everything).
Former-commit-id: 820ad02968
|
10 years ago |
dehnert
|
b5f907d99d
|
Added propositional model checker. Put some of the new classes in new folders. Fixed an issue that prevented compilation.
Former-commit-id: 517a870d2f
|
10 years ago |
dehnert
|
8a4706d9c9
|
A lot of work on model checker interfaces. In particular, the SCC elimination model checker is almost integrated.
Former-commit-id: bbf988c943
|
10 years ago |
dehnert
|
9026aa9ac9
|
Adapted first model checker to the new properties.
Former-commit-id: 206d6c9858
|
10 years ago |
dehnert
|
1699732dce
|
More work on logic classes.
Former-commit-id: 9d94e02b74
|
10 years ago |
dehnert
|
320641e597
|
Started working on modified property classes.
Former-commit-id: cbcf84c2f6
|
10 years ago |
dehnert
|
00861a7479
|
Loosened the restriction to always require GMP a bit.
Former-commit-id: 0537ff217a
|
10 years ago |
dehnert
|
91e177028d
|
Started refactoring explicit model generator of PRISM models
Former-commit-id: 4ea82670d0
|
10 years ago |
dehnert
|
53196f5610
|
Created bit vector hash map and some necessary bit vector methods.
Former-commit-id: 4a9946a743
|
10 years ago |
dehnert
|
c474920fa4
|
Started refactoring SMT solvers. Now displaying MathSAT version in CLI.
Former-commit-id: 1736a0bb6b
|
10 years ago |
David_Korzeniewski
|
b8a74c61c0
|
Set cuda_root variable in cmakelists to make it show up in the gui when configuring.
Former-commit-id: 29ca44312f
|
10 years ago |
svkurowski
|
da3542dcec
|
Integrate CUDA into buildsystem and add example function
Former-commit-id: 2f5acf8dcd
|
10 years ago |
svkurowski
|
00ec9a7db6
|
Integrate CUDA into buildsystem and add example function
Former-commit-id: 392acb148a
|
10 years ago |
David_Korzeniewski
|
2e92d66bf3
|
Cmake scripts for linking mathsat and gmp or mpir which is required by mathsat
Former-commit-id: b13b68115a
|
10 years ago |
PBerger
|
eb9c1de59b
|
Added Boost DECLTYPE for MSVC.
Former-commit-id: c70dfa5e63
|
10 years ago |
dehnert
|
d3fc2d8fbf
|
Fixed small but important bug in SCC decomposition that led to wrong results when using MSVC.
Former-commit-id: 07358dc2e8
|
10 years ago |