dehnert
5ecc96fa3a
Fixed some more places in the code to use the new option system.
Former-commit-id: 15ff64f1dc
10 years ago
dehnert
a995d7dd4a
The tests now run fine with the new option system.
Former-commit-id: 6d6c510131
10 years ago
dehnert
266d660d89
Added functions responsible for printing the help. Started adapting the tests to the new option system.
Former-commit-id: 0407d8223e
10 years ago
dehnert
9ad12616e2
Renamed files in settings module a bit. Started on the pseudo-modular module-settings.
Former-commit-id: b3162aa86b
10 years ago
dehnert
96e1f8faf9
Renamed Settings class to SettingsManager.
Former-commit-id: 2b33f4c8d0
10 years ago
dehnert
fff4e61fc3
Changed interface of matrix builder slightly to be able to also not force the resulting matrix to certain dimensions, but merely to reserve the desired space.
Former-commit-id: e36d05398e
10 years ago
dehnert
ac420f13d0
Fixed some warnings in various places.
Former-commit-id: fbfbfc2bcb
10 years ago
dehnert
aecd0e3cb8
Made Storm compile again without Z3: guarded some header inclusions and function definitions/implementations. Also guarded the tests that require certain libraries (like Gurobi, glpk, Z3), so that tests do not fail any more when the libraries are not available.
Former-commit-id: 307036e25c
10 years ago
David_Korzeniewski
52d3d91060
Implemented Unsat Core/Assumtions & simple test
Former-commit-id: f79ee3a809
11 years ago
David_Korzeniewski
a815a6f425
Implemented allSat with z3 and test
Former-commit-id: 3795fc00c2
11 years ago
David_Korzeniewski
93c03fff3f
Fixed order of checks in Z3ExpressionAdapter, fixed missing override of isVariable in VariableExpression, removed unnecessary exception in Z3SmtSolver model generation
Former-commit-id: ca5f876655
11 years ago
David_Korzeniewski
a0319cb6e7
Model Generation and Tests for translating from z3 to storm
translating from z3 to storm has still some errors
Former-commit-id: 2a46b6c615
11 years ago
David_Korzeniewski
79984db3ee
Added test for checkWithAssumptions
Former-commit-id: 4f64100ec5
11 years ago
David_Korzeniewski
9a7b4f69ef
More tests and some small bugfixes for Z3SmtSolver
Former-commit-id: 71def90649
11 years ago
David_Korzeniewski
45bc8ea665
Conditional compilation for all parts using z3 by checking STORM_HAVE_Z3
Added first simple tests for Z3SmtSolver and Z3ExpressionAdapter
Former-commit-id: 77ade5ffa6
11 years ago
dehnert
29d8111991
Adapted Gurobi and glpk LP solvers to expression-based interface. Adapted tests and made them work again.
Former-commit-id: 62379ddafd
11 years ago
PBerger
94b25c02ca
Fixed bugs in some files.
Made LTL a little better to compile under WIN32.
Former-commit-id: 71377f0672
11 years ago
dehnert
12743e0a7e
Moved from additional row grouping to the one embedded in the matrix itself.
Former-commit-id: 9d7a1fff10
11 years ago
PBerger
68a6e533be
Added error handling in GurobiLpSolver.cpp
Fixed a bug related to commit 486e99d6ae
[formerly 1300d77ae8
] where updateModel was not called before adding constraints in the GurobiLpSolverTest.cpp
Former-commit-id: 9f619e5039
11 years ago
dehnert
38833e308f
Started to add row-grouping to sparse matrix class.
Former-commit-id: 39e3703095
11 years ago
dehnert
ef5eb19e9c
Corrected test formulation in case StoRM was built without support for a given LP solver.
Former-commit-id: 7ae692f274
11 years ago
dehnert
36fb44e206
Added functional tests for nondeterministic linear equation solvers. Added functional tests for LPs in addition to the existing MILP tests.
Former-commit-id: 8c0fa08f2d
11 years ago
dehnert
514aace4fd
Added function tests for both glpk- and Gurobi-based LP solver implementations. Found and fixed some bugs while doing this.
Former-commit-id: 99e58097f7
11 years ago
dehnert
588a4b60b6
Refactored linear equation solvers and nondeterministic linear equation solvers. Added functional tests for both.
Former-commit-id: 0abb11828a
11 years ago