From ba14ba36135fc27d24d4d96e8482e68b26c855f1 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 18 Dec 2014 19:31:51 +0100
Subject: [PATCH] Further work on MathSAT solver.
Former-commit-id: dd67b235056773363f5cf07b943eca7016163e8e
---
src/solver/MathsatSmtSolver.cpp | 222 ++++++++++--------
src/solver/MathsatSmtSolver.h | 8 +-
src/solver/Z3SmtSolver.cpp | 8 +-
.../solver/MathSatSmtSolverTest.cpp | 142 +++++------
test/functional/solver/Z3SmtSolverTest.cpp | 84 +++----
5 files changed, 249 insertions(+), 215 deletions(-)
diff --git a/src/solver/MathsatSmtSolver.cpp b/src/solver/MathsatSmtSolver.cpp
index 2fc22103a..6be855dae 100644
--- a/src/solver/MathsatSmtSolver.cpp
+++ b/src/solver/MathsatSmtSolver.cpp
@@ -1,7 +1,6 @@
#include "src/solver/MathsatSmtSolver.h"
-#include <vector>
-
+#include "src/exceptions/NotSupportedException.h"
#include "src/exceptions/UnexpectedException.h"
#include "src/exceptions/InvalidStateException.h"
@@ -44,7 +43,7 @@ namespace storm {
#ifdef STORM_HAVE_MSAT
msat_push_backtrack_point(env);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
#endif
}
@@ -52,16 +51,20 @@ namespace storm {
#ifdef STORM_HAVE_MSAT
msat_pop_backtrack_point(env);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
#endif
}
+ void MathsatSmtSolver::pop(uint_fast64_t n) {
+ SmtSolver::pop(n);
+ }
+
void MathsatSmtSolver::reset()
{
#ifdef STORM_HAVE_MSAT
msat_reset_env(env);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
#endif
}
@@ -70,7 +73,7 @@ namespace storm {
#ifdef STORM_HAVE_MSAT
msat_assert_formula(env, expressionAdapter->translateExpression(e, true));
#else
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
#endif
}
@@ -91,7 +94,7 @@ namespace storm {
}
return this->lastResult;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
#endif
}
@@ -119,7 +122,7 @@ namespace storm {
}
return this->lastResult;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
#endif
}
@@ -147,18 +150,17 @@ namespace storm {
}
return this->lastResult;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
#endif
}
storm::expressions::SimpleValuation MathsatSmtSolver::getModel()
{
#ifdef STORM_HAVE_MSAT
-
- STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Requested Model but last check result was not SAT.");
+ STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable.");
return this->convertMathsatModelToValuation();
#else
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
#endif
}
@@ -166,27 +168,25 @@ namespace storm {
storm::expressions::SimpleValuation MathsatSmtSolver::convertMathsatModelToValuation() {
storm::expressions::SimpleValuation stormModel;
- msat_model_iterator model = msat_create_model_iterator(env);
-
- STORM_LOG_THROW(!MSAT_ERROR_MODEL_ITERATOR(model), storm::exceptions::UnexpectedException, "MathSat returned an illegal model iterator.");
+ msat_model_iterator modelIterator = msat_create_model_iterator(env);
+ STORM_LOG_THROW(!MSAT_ERROR_MODEL_ITERATOR(modelIterator), storm::exceptions::UnexpectedException, "MathSat returned an illegal model iterator.");
- while (msat_model_iterator_has_next(model)) {
+ while (msat_model_iterator_has_next(modelIterator)) {
msat_term t, v;
- msat_model_iterator_next(model, &t, &v);
+ msat_model_iterator_next(modelIterator, &t, &v);
- storm::expressions::Expression var_i_interp = this->expressionAdapter->translateTerm(v);
+ storm::expressions::Expression variableIInterpretation = this->expressionAdapter->translateTerm(v);
char* name = msat_decl_get_name(msat_term_get_decl(t));
- switch (var_i_interp.getReturnType()) {
+ switch (variableIInterpretation.getReturnType()) {
case storm::expressions::ExpressionReturnType::Bool:
-
- stormModel.addBooleanIdentifier(std::string(name), var_i_interp.evaluateAsBool());
+ stormModel.addBooleanIdentifier(std::string(name), variableIInterpretation.evaluateAsBool());
break;
case storm::expressions::ExpressionReturnType::Int:
- stormModel.addIntegerIdentifier(std::string(name), var_i_interp.evaluateAsInt());
+ stormModel.addIntegerIdentifier(std::string(name), variableIInterpretation.evaluateAsInt());
break;
case storm::expressions::ExpressionReturnType::Double:
- stormModel.addDoubleIdentifier(std::string(name), var_i_interp.evaluateAsDouble());
+ stormModel.addDoubleIdentifier(std::string(name), variableIInterpretation.evaluateAsDouble());
break;
default:
STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Variable interpretation in model is not of type bool, int or double.")
@@ -204,99 +204,140 @@ namespace storm {
std::vector<storm::expressions::SimpleValuation> MathsatSmtSolver::allSat(std::vector<storm::expressions::Expression> const& important)
{
#ifdef STORM_HAVE_MSAT
-
std::vector<storm::expressions::SimpleValuation> valuations;
-
- this->allSat(important, [&valuations](storm::expressions::SimpleValuation& valuation) -> bool {valuations.push_back(valuation); return true; });
-
+ this->allSat(important, [&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; });
return valuations;
-
#else
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
#endif
}
#ifdef STORM_HAVE_MSAT
- class AllsatValuationsCallbackUserData {
+ class AllsatValuationCallbackUserData {
public:
- AllsatValuationsCallbackUserData(msat_env &env,
- storm::adapters::MathsatExpressionAdapter &adapter,
- std::function<bool(storm::expressions::SimpleValuation&)> const& callback)
- : env(env), adapter(adapter), callback(callback) {
+ AllsatValuationCallbackUserData(msat_env& env, std::function<bool(storm::expressions::SimpleValuation&)> const& callback) : env(env), callback(callback) {
+ // Intentionally left empty.
}
- msat_env &env;
- storm::adapters::MathsatExpressionAdapter &adapter;
+
+ static int allsatValuationsCallback(msat_term* model, int size, void* user_data) {
+ AllsatValuationCallbackUserData* user = reinterpret_cast<AllsatValuationCallbackUserData*>(user_data);
+
+ storm::expressions::SimpleValuation valuation;
+ for (int i = 0; i < size; ++i) {
+ bool currentTermValue = true;
+ msat_term currentTerm = model[i];
+ if (msat_term_is_not(user->env, currentTerm)) {
+ currentTerm = msat_term_get_arg(currentTerm, 0);
+ currentTermValue = false;
+ }
+ char* name = msat_decl_get_name(msat_term_get_decl(currentTerm));
+ std::string nameAsString(name);
+ msat_free(name);
+ valuation.addBooleanIdentifier(nameAsString, currentTermValue);
+ }
+
+ if (user->callback(valuation)) {
+ return 1;
+ } else {
+ return 0;
+ }
+ }
+
+ protected:
+ // The MathSAT environment. It is used to retrieve the values of the atoms in a model.
+ msat_env& env;
+
+ // The function that is to be called when the MathSAT model has been translated to a valuation.
std::function<bool(storm::expressions::SimpleValuation&)> const& callback;
};
-
- int allsatValuationsCallback(msat_term *model, int size, void *user_data) {
- AllsatValuationsCallbackUserData* user = reinterpret_cast<AllsatValuationsCallbackUserData*>(user_data);
-
- storm::expressions::SimpleValuation valuation;
-
- for (int i = 0; i < size; ++i) {
- bool currentTermValue = true;
- msat_term currentTerm = model[i];
- if (msat_term_is_not(user->env, currentTerm)) {
- currentTerm = msat_term_get_arg(currentTerm, 0);
- currentTermValue = false;
- }
- char* name = msat_decl_get_name(msat_term_get_decl(currentTerm));
- std::string name_str(name);
- valuation.addBooleanIdentifier(name_str, currentTermValue);
- msat_free(name);
- }
-
- if (user->callback(valuation)) {
- return 1;
- } else {
- return 0;
- }
- }
+
+ class AllsatModelReferenceCallbackUserData {
+ public:
+ AllsatModelReferenceCallbackUserData(msat_env& env, std::unordered_map<std::string, uint_fast64_t> const& atomNameToSlotMapping, std::function<bool(storm::solver::SmtSolver::ModelReference&)> const& callback) : env(env), atomNameToSlotMapping(atomNameToSlotMapping), callback(callback) {
+ // Intentionally left empty.
+ }
+
+ static int allsatModelReferenceCallback(msat_term* model, int size, void* user_data) {
+ AllsatModelReferenceCallbackUserData* user = reinterpret_cast<AllsatModelReferenceCallbackUserData*>(user_data);
+ MathsatSmtSolver::MathSatModelReference modelReference(user->env, model, user->atomNameToSlotMapping);
+ if (user->callback(modelReference)) {
+ return 1;
+ } else {
+ return 0;
+ }
+ }
+
+ protected:
+ // The MathSAT environment. It is used to retrieve the values of the atoms in a model.
+ msat_env& env;
+
+ // Store a mapping from the names of atoms to their slots in the model.
+ std::unordered_map<std::string, uint_fast64_t> const& atomNameToSlotMapping;
+
+ // The function that is to be called when the MathSAT model has been translated to a valuation.
+ std::function<bool(storm::solver::SmtSolver::ModelReference&)> const& callback;
+ };
#endif
uint_fast64_t MathsatSmtSolver::allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> const& callback)
{
#ifdef STORM_HAVE_MSAT
+ // Create a backtracking point, because MathSAT will modify the assertions stack during its AllSat procedure.
+ this->push();
+
std::vector<msat_term> msatImportant;
msatImportant.reserve(important.size());
- for (storm::expressions::Expression e : important) {
- if (!e.isVariable()) {
- throw storm::exceptions::InvalidArgumentException() << "The important expressions for AllSat must be atoms, i.e. variable expressions.";
- }
- msatImportant.push_back(expressionAdapter->translateExpression(e));
+ for (storm::expressions::Expression const& atom : important) {
+ STORM_LOG_THROW(atom.isVariable() && atom.hasBooleanReturnType(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be boolean variables.");
+ msatImportant.push_back(expressionAdapter->translateExpression(atom));
}
- AllsatValuationsCallbackUserData allSatUserData(env, *expressionAdapter, callback);
- int numModels = msat_all_sat(env, msatImportant.data(), msatImportant.size(), &allsatValuationsCallback, &allSatUserData);
+ AllsatValuationCallbackUserData allSatUserData(env, callback);
+ int numberOfModels = msat_all_sat(env, msatImportant.data(), msatImportant.size(), &AllsatValuationCallbackUserData::allsatValuationsCallback, &allSatUserData);
- return numModels;
+ // Restore original assertion stack and return.
+ this->pop();
+ return static_cast<uint_fast64_t>(numberOfModels);
#else
- LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support.");
+ LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
#endif
}
uint_fast64_t MathsatSmtSolver::allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(SmtSolver::ModelReference&)> const& callback)
{
#ifdef STORM_HAVE_MSAT
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not Implemented.");
+ // Create a backtracking point, because MathSAT will modify the assertions stack during its AllSat procedure.
+ this->push();
+
+ std::vector<msat_term> msatImportant;
+ msatImportant.reserve(important.size());
+ std::unordered_map<std::string, uint_fast64_t> atomNameToSlotMapping;
+
+ for (storm::expressions::Expression const& atom : important) {
+ STORM_LOG_THROW(atom.isVariable() && atom.hasBooleanReturnType(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be boolean variables.");
+ msatImportant.push_back(expressionAdapter->translateExpression(atom));
+ atomNameToSlotMapping[atom.getIdentifier()] = msatImportant.size() - 1;
+ }
+
+ AllsatModelReferenceCallbackUserData allSatUserData(env, atomNameToSlotMapping, callback);
+ int numberOfModels = msat_all_sat(env, msatImportant.data(), msatImportant.size(), &AllsatModelReferenceCallbackUserData::allsatModelReferenceCallback, &allSatUserData);
+
+ // Restore original assertion stack and return.
+ this->pop();
+ return static_cast<uint_fast64_t>(numberOfModels);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
#endif
}
std::vector<storm::expressions::Expression> MathsatSmtSolver::getUnsatAssumptions() {
#ifdef STORM_HAVE_MSAT
- if (lastResult != SmtSolver::CheckResult::Unsat) {
- throw storm::exceptions::InvalidStateException() << "Unsat Assumptions was called but last state is not unsat.";
- }
- if (!lastCheckAssumptions) {
- throw storm::exceptions::InvalidStateException() << "Unsat Assumptions was called but last check had no assumptions.";
- }
-
+ STORM_LOG_THROW(lastResult == SmtSolver::CheckResult::Unsat, storm::exceptions::InvalidStateException, "Unable to generate unsatisfiable core of assumptions, because the last check did not determine the formulas to be unsatisfiable.")
+ STORM_LOG_THROW(lastCheckAssumptions, storm::exceptions::InvalidStateException, "Unable to generate unsatisfiable core of assumptions, because the last check did not involve assumptions.");
+
size_t numUnsatAssumpations;
msat_term* msatUnsatAssumptions = msat_get_unsat_assumptions(env, &numUnsatAssumpations);
@@ -309,43 +350,34 @@ namespace storm {
return unsatAssumptions;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
#endif
}
void MathsatSmtSolver::setInterpolationGroup(uint_fast64_t group) {
#ifdef STORM_HAVE_MSAT
auto groupIter = this->interpolationGroups.find(group);
- if( groupIter == this->interpolationGroups.end() ) {
+ if (groupIter == this->interpolationGroups.end() ) {
int newGroup = msat_create_itp_group(env);
auto insertResult = this->interpolationGroups.insert(std::make_pair(group, newGroup));
- if (!insertResult.second) {
- throw storm::exceptions::InvalidStateException() << "Internal error in MathSAT wrapper: Unable to insert newly created interpolation group.";
- }
groupIter = insertResult.first;
}
msat_set_itp_group(env, groupIter->second);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
#endif
}
storm::expressions::Expression MathsatSmtSolver::getInterpolant(std::vector<uint_fast64_t> const& groupsA) {
#ifdef STORM_HAVE_MSAT
- if (lastResult != SmtSolver::CheckResult::Unsat) {
- throw storm::exceptions::InvalidStateException() << "getInterpolant was called but last state is not unsat.";
- }
- if (lastCheckAssumptions) {
- throw storm::exceptions::InvalidStateException() << "getInterpolant was called but last check had assumptions.";
- }
+ STORM_LOG_THROW(lastResult == SmtSolver::CheckResult::Unsat, storm::exceptions::InvalidStateException, "Unable to generate interpolant, because the last check did not determine the formulas to be unsatisfiable.");
+ STORM_LOG_THROW(!lastCheckAssumptions, storm::exceptions::InvalidStateException, "Unable to generate interpolant, because the last check for satisfiability involved assumptions.");
std::vector<int> msatInterpolationGroupsA;
msatInterpolationGroupsA.reserve(groupsA.size());
for (auto groupOfA : groupsA) {
auto groupIter = this->interpolationGroups.find(groupOfA);
- if (groupIter == this->interpolationGroups.end()) {
- throw storm::exceptions::InvalidArgumentException() << "Requested interpolant for non existing interpolation group " << groupOfA;
- }
+ STORM_LOG_THROW(groupIter != this->interpolationGroups.end(), storm::exceptions::InvalidArgumentException, "Unable to generate interpolant, because an unknown interpolation group was referenced.");
msatInterpolationGroupsA.push_back(groupIter->second);
}
msat_term interpolant = msat_get_interpolant(env, msatInterpolationGroupsA.data(), msatInterpolationGroupsA.size());
@@ -354,7 +386,7 @@ namespace storm {
return this->expressionAdapter->translateTerm(interpolant);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without MathSat support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
#endif
}
}
diff --git a/src/solver/MathsatSmtSolver.h b/src/solver/MathsatSmtSolver.h
index 4cff5f4f1..efd488450 100644
--- a/src/solver/MathsatSmtSolver.h
+++ b/src/solver/MathsatSmtSolver.h
@@ -41,7 +41,7 @@ namespace storm {
class MathSatModelReference : public SmtSolver::ModelReference {
public:
#ifdef STORM_HAVE_MSAT
- MathSatModelReference(msat_env const& env, storm::adapters::MathsatExpressionAdapter& adapter);
+ MathSatModelReference(msat_env const& env, msat_term* model, std::unordered_map<std::string, uint_fast64_t> const& atomNameToSlotMapping);
#endif
virtual bool getBooleanValue(std::string const& name) const override;
virtual int_fast64_t getIntegerValue(std::string const& name) const override;
@@ -50,11 +50,11 @@ namespace storm {
private:
#ifdef STORM_HAVE_MSAT
msat_env const& env;
- storm::adapters::MathsatExpressionAdapter& expressionAdapter;
+ msat_term* model;
+ std::unordered_map<std::string, uint_fast64_t> const& atomNameToSlotMapping;
#endif
};
- public:
MathsatSmtSolver(Options const& options = Options());
virtual ~MathsatSmtSolver();
@@ -63,6 +63,8 @@ namespace storm {
virtual void pop() override;
+ virtual void pop(uint_fast64_t n) override;
+
virtual void reset() override;
virtual void add(storm::expressions::Expression const& assertion) override;
diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp
index 17360d2a5..638972027 100644
--- a/src/solver/Z3SmtSolver.cpp
+++ b/src/solver/Z3SmtSolver.cpp
@@ -146,7 +146,7 @@ namespace storm {
#endif
}
- SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::initializer_list<storm::expressions::Expression> assumptions)
+ SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions)
{
#ifdef STORM_HAVE_Z3
lastCheckAssumptions = true;
@@ -216,7 +216,7 @@ namespace storm {
{
#ifdef STORM_HAVE_Z3
std::vector<storm::expressions::SimpleValuation> valuations;
- this->allSat(important, [&valuations](storm::expressions::SimpleValuation& valuation) -> bool { valuations.push_back(valuation); return true; });
+ this->allSat(important, [&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; });
return valuations;
#else
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
@@ -227,7 +227,7 @@ namespace storm {
{
#ifdef STORM_HAVE_Z3
for (storm::expressions::Expression const& atom : important) {
- STORM_LOG_THROW(atom.isVariable(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be atoms, i.e. variables.");
+ STORM_LOG_THROW(atom.isVariable() && atom.hasBooleanReturnType(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be boolean variables.");
}
uint_fast64_t numberOfModels = 0;
@@ -278,7 +278,7 @@ namespace storm {
{
#ifdef STORM_HAVE_Z3
for (storm::expressions::Expression const& atom : important) {
- STORM_LOG_THROW(atom.isVariable(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be atoms, i.e. variables.");
+ STORM_LOG_THROW(atom.isVariable() && atom.hasBooleanReturnType(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be boolean variables.");
}
uint_fast64_t numberOfModels = 0;
diff --git a/test/functional/solver/MathSatSmtSolverTest.cpp b/test/functional/solver/MathSatSmtSolverTest.cpp
index e495c4be8..2ca48d935 100644
--- a/test/functional/solver/MathSatSmtSolverTest.cpp
+++ b/test/functional/solver/MathSatSmtSolverTest.cpp
@@ -2,17 +2,17 @@
#include "storm-config.h"
#ifdef STORM_HAVE_MSAT
-#include "src/solver/MathSatSmtSolver.h"
+#include "src/solver/MathsatSmtSolver.h"
-TEST(MathSatSmtSolver, CheckSat) {
- storm::solver::MathSatSmtSolver s;
- storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN;
+TEST(MathsatSmtSolver, CheckSat) {
+ storm::solver::MathsatSmtSolver s;
+ storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
storm::expressions::Expression exprDeMorgan = !(storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")).iff((!storm::expressions::Expression::createBooleanVariable("x") || !storm::expressions::Expression::createBooleanVariable("y")));
- ASSERT_NO_THROW(s.assertExpression(exprDeMorgan));
+ ASSERT_NO_THROW(s.add(exprDeMorgan));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
ASSERT_NO_THROW(s.reset());
storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
@@ -24,21 +24,21 @@ TEST(MathSatSmtSolver, CheckSat) {
&& c == (a * b)
&& b + a > c;
- ASSERT_NO_THROW(s.assertExpression(exprFormula));
+ ASSERT_NO_THROW(s.add(exprFormula));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
ASSERT_NO_THROW(s.reset());
}
-TEST(MathSatSmtSolver, CheckUnsat) {
- storm::solver::MathSatSmtSolver s;
- storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN;
+TEST(MathsatSmtSolver, CheckUnsat) {
+ storm::solver::MathsatSmtSolver s;
+ storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
storm::expressions::Expression exprDeMorgan = !(storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")).iff( (!storm::expressions::Expression::createBooleanVariable("x") || !storm::expressions::Expression::createBooleanVariable("y")));
- ASSERT_NO_THROW(s.assertExpression(!exprDeMorgan));
+ ASSERT_NO_THROW(s.add(!exprDeMorgan));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
ASSERT_NO_THROW(s.reset());
storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
@@ -50,40 +50,40 @@ TEST(MathSatSmtSolver, CheckUnsat) {
&& c == (a + b + storm::expressions::Expression::createIntegerLiteral(1))
&& b + a > c;
- ASSERT_NO_THROW(s.assertExpression(exprFormula));
+ ASSERT_NO_THROW(s.add(exprFormula));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
}
-TEST(MathSatSmtSolver, Backtracking) {
- storm::solver::MathSatSmtSolver s;
- storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN;
+TEST(MathsatSmtSolver, Backtracking) {
+ storm::solver::MathsatSmtSolver s;
+ storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
storm::expressions::Expression expr1 = storm::expressions::Expression::createTrue();
storm::expressions::Expression expr2 = storm::expressions::Expression::createFalse();
storm::expressions::Expression expr3 = storm::expressions::Expression::createFalse();
- ASSERT_NO_THROW(s.assertExpression(expr1));
+ ASSERT_NO_THROW(s.add(expr1));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
ASSERT_NO_THROW(s.push());
- ASSERT_NO_THROW(s.assertExpression(expr2));
+ ASSERT_NO_THROW(s.add(expr2));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
ASSERT_NO_THROW(s.pop());
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
ASSERT_NO_THROW(s.push());
- ASSERT_NO_THROW(s.assertExpression(expr2));
+ ASSERT_NO_THROW(s.add(expr2));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
ASSERT_NO_THROW(s.push());
- ASSERT_NO_THROW(s.assertExpression(expr3));
+ ASSERT_NO_THROW(s.add(expr3));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
ASSERT_NO_THROW(s.pop(2));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
ASSERT_NO_THROW(s.reset());
storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
@@ -96,21 +96,21 @@ TEST(MathSatSmtSolver, Backtracking) {
&& b + a > c;
storm::expressions::Expression exprFormula2 = c > a + b + storm::expressions::Expression::createIntegerLiteral(1);
- ASSERT_NO_THROW(s.assertExpression(exprFormula));
+ ASSERT_NO_THROW(s.add(exprFormula));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
ASSERT_NO_THROW(s.push());
- ASSERT_NO_THROW(s.assertExpression(exprFormula2));
+ ASSERT_NO_THROW(s.add(exprFormula2));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
ASSERT_NO_THROW(s.pop());
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
}
-TEST(MathSatSmtSolver, Assumptions) {
- storm::solver::MathSatSmtSolver s;
- storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN;
+TEST(MathsatSmtSolver, Assumptions) {
+ storm::solver::MathsatSmtSolver s;
+ storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b");
@@ -123,22 +123,22 @@ TEST(MathSatSmtSolver, Assumptions) {
storm::expressions::Expression f2 = storm::expressions::Expression::createBooleanVariable("f2");
storm::expressions::Expression exprFormula2 = f2.implies(c > a + b + storm::expressions::Expression::createIntegerLiteral(1));
- ASSERT_NO_THROW(s.assertExpression(exprFormula));
+ ASSERT_NO_THROW(s.add(exprFormula));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
- ASSERT_NO_THROW(s.assertExpression(exprFormula2));
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
+ ASSERT_NO_THROW(s.add(exprFormula2));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
ASSERT_NO_THROW(result = s.checkWithAssumptions({f2}));
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
ASSERT_NO_THROW(result = s.checkWithAssumptions({ !f2 }));
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
}
-TEST(MathSatSmtSolver, GenerateModel) {
- storm::solver::MathSatSmtSolver s;
+TEST(MathsatSmtSolver, GenerateModel) {
+ storm::solver::MathsatSmtSolver s;
storm::solver::SmtSolver::CheckResult result;
storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
@@ -150,9 +150,9 @@ TEST(MathSatSmtSolver, GenerateModel) {
&& c == (a + b - storm::expressions::Expression::createIntegerLiteral(1))
&& b + a > c;
- (s.assertExpression(exprFormula));
+ (s.add(exprFormula));
(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
storm::expressions::SimpleValuation model;
(model = s.getModel());
int_fast64_t a_eval = model.getIntegerValue("a");
@@ -161,9 +161,9 @@ TEST(MathSatSmtSolver, GenerateModel) {
ASSERT_TRUE(c_eval == a_eval + b_eval - 1);
}
-TEST(MathSatSmtSolver, AllSat) {
- storm::solver::MathSatSmtSolver s;
- storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN;
+TEST(MathsatSmtSolver, AllSat) {
+ storm::solver::MathsatSmtSolver s;
+ storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b");
@@ -174,9 +174,9 @@ TEST(MathSatSmtSolver, AllSat) {
storm::expressions::Expression exprFormula2 = y.implies(a < storm::expressions::Expression::createIntegerLiteral(5));
storm::expressions::Expression exprFormula3 = z.implies(b < storm::expressions::Expression::createIntegerLiteral(5));
- (s.assertExpression(exprFormula1));
- (s.assertExpression(exprFormula2));
- (s.assertExpression(exprFormula3));
+ (s.add(exprFormula1));
+ (s.add(exprFormula2));
+ (s.add(exprFormula3));
std::vector<storm::expressions::SimpleValuation> valuations = s.allSat({x,y});
@@ -195,9 +195,9 @@ TEST(MathSatSmtSolver, AllSat) {
}
}
-TEST(MathSatSmtSolver, UnsatAssumptions) {
- storm::solver::MathSatSmtSolver s;
- storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN;
+TEST(MathsatSmtSolver, UnsatAssumptions) {
+ storm::solver::MathsatSmtSolver s;
+ storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b");
@@ -210,19 +210,19 @@ TEST(MathSatSmtSolver, UnsatAssumptions) {
storm::expressions::Expression f2 = storm::expressions::Expression::createBooleanVariable("f2");
storm::expressions::Expression exprFormula2 = f2.implies(c > a + b + storm::expressions::Expression::createIntegerLiteral(1));
- (s.assertExpression(exprFormula));
- (s.assertExpression(exprFormula2));
+ (s.add(exprFormula));
+ (s.add(exprFormula2));
(result = s.checkWithAssumptions({ f2 }));
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
std::vector<storm::expressions::Expression> unsatCore = s.getUnsatAssumptions();
ASSERT_EQ(unsatCore.size(), 1);
ASSERT_TRUE(unsatCore[0].isVariable());
ASSERT_STREQ("f2", unsatCore[0].getIdentifier().c_str());
}
-TEST(MathSatSmtSolver, InterpolationTest) {
- storm::solver::MathSatSmtSolver s(storm::solver::SmtSolver::Options::InterpolantComputation);
- storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN;
+TEST(MathsatSmtSolver, InterpolationTest) {
+ storm::solver::MathsatSmtSolver s(storm::solver::MathsatSmtSolver::Options(false, false, true));
+ storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b");
@@ -232,28 +232,28 @@ TEST(MathSatSmtSolver, InterpolationTest) {
storm::expressions::Expression exprFormula3 = c > a;
s.setInterpolationGroup(0);
- s.assertExpression(exprFormula);
+ s.add(exprFormula);
s.setInterpolationGroup(1);
- s.assertExpression(exprFormula2);
+ s.add(exprFormula2);
s.setInterpolationGroup(2);
- s.assertExpression(exprFormula3);
+ s.add(exprFormula3);
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
storm::expressions::Expression interpol;
ASSERT_NO_THROW(interpol = s.getInterpolant({0, 1}));
- storm::solver::MathSatSmtSolver s2;
+ storm::solver::MathsatSmtSolver s2;
- ASSERT_NO_THROW(s2.assertExpression(!(exprFormula && exprFormula2).implies(interpol)));
+ ASSERT_NO_THROW(s2.add(!(exprFormula && exprFormula2).implies(interpol)));
ASSERT_NO_THROW(result = s2.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
ASSERT_NO_THROW(s2.reset());
- ASSERT_NO_THROW(s2.assertExpression(interpol && exprFormula3));
+ ASSERT_NO_THROW(s2.add(interpol && exprFormula3));
ASSERT_NO_THROW(result = s2.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
}
#endif
\ No newline at end of file
diff --git a/test/functional/solver/Z3SmtSolverTest.cpp b/test/functional/solver/Z3SmtSolverTest.cpp
index 30d023f0d..93f2876bb 100644
--- a/test/functional/solver/Z3SmtSolverTest.cpp
+++ b/test/functional/solver/Z3SmtSolverTest.cpp
@@ -7,13 +7,13 @@
TEST(Z3SmtSolver, CheckSat) {
storm::solver::Z3SmtSolver s;
- storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN;
+ storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
storm::expressions::Expression exprDeMorgan = !(storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")).iff((!storm::expressions::Expression::createBooleanVariable("x") || !storm::expressions::Expression::createBooleanVariable("y")));
- ASSERT_NO_THROW(s.assertExpression(exprDeMorgan));
+ ASSERT_NO_THROW(s.add(exprDeMorgan));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
ASSERT_NO_THROW(s.reset());
storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
@@ -25,21 +25,21 @@ TEST(Z3SmtSolver, CheckSat) {
&& c == (a * b)
&& b + a > c;
- ASSERT_NO_THROW(s.assertExpression(exprFormula));
+ ASSERT_NO_THROW(s.add(exprFormula));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
ASSERT_NO_THROW(s.reset());
}
TEST(Z3SmtSolver, CheckUnsat) {
storm::solver::Z3SmtSolver s;
- storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN;
+ storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
storm::expressions::Expression exprDeMorgan = !(storm::expressions::Expression::createBooleanVariable("x") && storm::expressions::Expression::createBooleanVariable("y")).iff( (!storm::expressions::Expression::createBooleanVariable("x") || !storm::expressions::Expression::createBooleanVariable("y")));
- ASSERT_NO_THROW(s.assertExpression(!exprDeMorgan));
+ ASSERT_NO_THROW(s.add(!exprDeMorgan));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
ASSERT_NO_THROW(s.reset());
@@ -52,41 +52,41 @@ TEST(Z3SmtSolver, CheckUnsat) {
&& c == (a * b)
&& b + a > c;
- ASSERT_NO_THROW(s.assertExpression(exprFormula));
+ ASSERT_NO_THROW(s.add(exprFormula));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
}
TEST(Z3SmtSolver, Backtracking) {
storm::solver::Z3SmtSolver s;
- storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN;
+ storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
storm::expressions::Expression expr1 = storm::expressions::Expression::createTrue();
storm::expressions::Expression expr2 = storm::expressions::Expression::createFalse();
storm::expressions::Expression expr3 = storm::expressions::Expression::createFalse();
- ASSERT_NO_THROW(s.assertExpression(expr1));
+ ASSERT_NO_THROW(s.add(expr1));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
ASSERT_NO_THROW(s.push());
- ASSERT_NO_THROW(s.assertExpression(expr2));
+ ASSERT_NO_THROW(s.add(expr2));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
ASSERT_NO_THROW(s.pop());
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
ASSERT_NO_THROW(s.push());
- ASSERT_NO_THROW(s.assertExpression(expr2));
+ ASSERT_NO_THROW(s.add(expr2));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
ASSERT_NO_THROW(s.push());
- ASSERT_NO_THROW(s.assertExpression(expr3));
+ ASSERT_NO_THROW(s.add(expr3));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
ASSERT_NO_THROW(s.pop(2));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
ASSERT_NO_THROW(s.reset());
@@ -100,21 +100,21 @@ TEST(Z3SmtSolver, Backtracking) {
&& b + a > c;
storm::expressions::Expression exprFormula2 = a >= storm::expressions::Expression::createIntegerLiteral(2);
- ASSERT_NO_THROW(s.assertExpression(exprFormula));
+ ASSERT_NO_THROW(s.add(exprFormula));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
ASSERT_NO_THROW(s.push());
- ASSERT_NO_THROW(s.assertExpression(exprFormula2));
+ ASSERT_NO_THROW(s.add(exprFormula2));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
ASSERT_NO_THROW(s.pop());
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
}
TEST(Z3SmtSolver, Assumptions) {
storm::solver::Z3SmtSolver s;
- storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::UNKNOWN;
+ storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b");
@@ -127,18 +127,18 @@ TEST(Z3SmtSolver, Assumptions) {
storm::expressions::Expression f2 = storm::expressions::Expression::createBooleanVariable("f2");
storm::expressions::Expression exprFormula2 = f2.implies(a >= storm::expressions::Expression::createIntegerLiteral(2));
- ASSERT_NO_THROW(s.assertExpression(exprFormula));
+ ASSERT_NO_THROW(s.add(exprFormula));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
- ASSERT_NO_THROW(s.assertExpression(exprFormula2));
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
+ ASSERT_NO_THROW(s.add(exprFormula2));
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
ASSERT_NO_THROW(result = s.checkWithAssumptions({f2}));
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
ASSERT_NO_THROW(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
ASSERT_NO_THROW(result = s.checkWithAssumptions({ !f2 }));
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
}
TEST(Z3SmtSolver, GenerateModel) {
@@ -154,9 +154,9 @@ TEST(Z3SmtSolver, GenerateModel) {
&& c == (a * b)
&& b + a > c;
- (s.assertExpression(exprFormula));
+ (s.add(exprFormula));
(result = s.check());
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
storm::expressions::SimpleValuation model;
(model = s.getModel());
int_fast64_t a_eval;
@@ -178,9 +178,9 @@ TEST(Z3SmtSolver, AllSat) {
storm::expressions::Expression exprFormula2 = y.implies(a < storm::expressions::Expression::createIntegerLiteral(5));
storm::expressions::Expression exprFormula3 = z.implies(b < storm::expressions::Expression::createIntegerLiteral(5));
- (s.assertExpression(exprFormula1));
- (s.assertExpression(exprFormula2));
- (s.assertExpression(exprFormula3));
+ (s.add(exprFormula1));
+ (s.add(exprFormula2));
+ (s.add(exprFormula3));
std::vector<storm::expressions::SimpleValuation> valuations = s.allSat({x,y});
@@ -214,10 +214,10 @@ TEST(Z3SmtSolver, UnsatAssumptions) {
storm::expressions::Expression f2 = storm::expressions::Expression::createBooleanVariable("f2");
storm::expressions::Expression exprFormula2 = f2.implies(a >= storm::expressions::Expression::createIntegerLiteral(2));
- s.assertExpression(exprFormula);
- s.assertExpression(exprFormula2);
+ s.add(exprFormula);
+ s.add(exprFormula2);
result = s.checkWithAssumptions({ f2 });
- ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
+ ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
std::vector<storm::expressions::Expression> unsatCore = s.getUnsatAssumptions();
ASSERT_EQ(unsatCore.size(), 1);
ASSERT_TRUE(unsatCore[0].isVariable());