sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Further work on MathSAT solver. 

Former-commit-id: dd67b23505
main
dehnert 10 years ago
parent
81571878f7
commit
ba14ba3613
5 changed files with 249 additions and 215 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 222
      src/solver/MathsatSmtSolver.cpp
  2. 8
      src/solver/MathsatSmtSolver.h
  3. 8
      src/solver/Z3SmtSolver.cpp
  4. 142
      test/functional/solver/MathSatSmtSolverTest.cpp
  5. 84
      test/functional/solver/Z3SmtSolverTest.cpp

222
src/solver/MathsatSmtSolver.cpp
View File

@ -1,7 +1,6 @@
#include "src/solver/MathsatSmtSolver.h" #include "src/solver/MathsatSmtSolver.h"
#include <vector>
#include "src/exceptions/NotSupportedException.h"
#include "src/exceptions/UnexpectedException.h" #include "src/exceptions/UnexpectedException.h"
#include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidStateException.h"
@ -44,7 +43,7 @@ namespace storm {
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
msat_push_backtrack_point(env); msat_push_backtrack_point(env);
#else #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 #endif
} }
@ -52,16 +51,20 @@ namespace storm {
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
msat_pop_backtrack_point(env); msat_pop_backtrack_point(env);
#else #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 #endif
} }
void MathsatSmtSolver::pop(uint_fast64_t n) {
SmtSolver::pop(n);
}
void MathsatSmtSolver::reset() void MathsatSmtSolver::reset()
{ {
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
msat_reset_env(env); msat_reset_env(env);
#else #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 #endif
} }
@ -70,7 +73,7 @@ namespace storm {
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
msat_assert_formula(env, expressionAdapter->translateExpression(e, true)); msat_assert_formula(env, expressionAdapter->translateExpression(e, true));
#else #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 #endif
} }
@ -91,7 +94,7 @@ namespace storm {
} }
return this->lastResult; return this->lastResult;
#else #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 #endif
} }
@ -119,7 +122,7 @@ namespace storm {
} }
return this->lastResult; return this->lastResult;
#else #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 #endif
} }
@ -147,18 +150,17 @@ namespace storm {
} }
return this->lastResult; return this->lastResult;
#else #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 #endif
} }
storm::expressions::SimpleValuation MathsatSmtSolver::getModel() storm::expressions::SimpleValuation MathsatSmtSolver::getModel()
{ {
#ifdef STORM_HAVE_MSAT #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(); return this->convertMathsatModelToValuation();
#else #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 #endif
} }
@ -166,27 +168,25 @@ namespace storm {
storm::expressions::SimpleValuation MathsatSmtSolver::convertMathsatModelToValuation() { storm::expressions::SimpleValuation MathsatSmtSolver::convertMathsatModelToValuation() {
storm::expressions::SimpleValuation stormModel; 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_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)); char* name = msat_decl_get_name(msat_term_get_decl(t));
switch (var_i_interp.getReturnType()) {
switch (variableIInterpretation.getReturnType()) {
case storm::expressions::ExpressionReturnType::Bool: case storm::expressions::ExpressionReturnType::Bool:
stormModel.addBooleanIdentifier(std::string(name), var_i_interp.evaluateAsBool());
stormModel.addBooleanIdentifier(std::string(name), variableIInterpretation.evaluateAsBool());
break; break;
case storm::expressions::ExpressionReturnType::Int: case storm::expressions::ExpressionReturnType::Int:
stormModel.addIntegerIdentifier(std::string(name), var_i_interp.evaluateAsInt());
stormModel.addIntegerIdentifier(std::string(name), variableIInterpretation.evaluateAsInt());
break; break;
case storm::expressions::ExpressionReturnType::Double: case storm::expressions::ExpressionReturnType::Double:
stormModel.addDoubleIdentifier(std::string(name), var_i_interp.evaluateAsDouble());
stormModel.addDoubleIdentifier(std::string(name), variableIInterpretation.evaluateAsDouble());
break; break;
default: default:
STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Variable interpretation in model is not of type bool, int or double.") 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) std::vector<storm::expressions::SimpleValuation> MathsatSmtSolver::allSat(std::vector<storm::expressions::Expression> const& important)
{ {
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
std::vector<storm::expressions::SimpleValuation> valuations; 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; return valuations;
#else #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 #endif
} }
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
class AllsatValuationsCallbackUserData {
class AllsatValuationCallbackUserData {
public: 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; 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 #endif
uint_fast64_t MathsatSmtSolver::allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> const& callback) uint_fast64_t MathsatSmtSolver::allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> const& callback)
{ {
#ifdef STORM_HAVE_MSAT #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; std::vector<msat_term> msatImportant;
msatImportant.reserve(important.size()); 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 #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 #endif
} }
uint_fast64_t MathsatSmtSolver::allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(SmtSolver::ModelReference&)> const& callback) uint_fast64_t MathsatSmtSolver::allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(SmtSolver::ModelReference&)> const& callback)
{ {
#ifdef STORM_HAVE_MSAT #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 #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 #endif
} }
std::vector<storm::expressions::Expression> MathsatSmtSolver::getUnsatAssumptions() { std::vector<storm::expressions::Expression> MathsatSmtSolver::getUnsatAssumptions() {
#ifdef STORM_HAVE_MSAT #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; size_t numUnsatAssumpations;
msat_term* msatUnsatAssumptions = msat_get_unsat_assumptions(env, &numUnsatAssumpations); msat_term* msatUnsatAssumptions = msat_get_unsat_assumptions(env, &numUnsatAssumpations);
@ -309,43 +350,34 @@ namespace storm {
return unsatAssumptions; return unsatAssumptions;
#else #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 #endif
} }
void MathsatSmtSolver::setInterpolationGroup(uint_fast64_t group) { void MathsatSmtSolver::setInterpolationGroup(uint_fast64_t group) {
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
auto groupIter = this->interpolationGroups.find(group); auto groupIter = this->interpolationGroups.find(group);
if( groupIter == this->interpolationGroups.end() ) {
if (groupIter == this->interpolationGroups.end() ) {
int newGroup = msat_create_itp_group(env); int newGroup = msat_create_itp_group(env);
auto insertResult = this->interpolationGroups.insert(std::make_pair(group, newGroup)); 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; groupIter = insertResult.first;
} }
msat_set_itp_group(env, groupIter->second); msat_set_itp_group(env, groupIter->second);
#else #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 #endif
} }
storm::expressions::Expression MathsatSmtSolver::getInterpolant(std::vector<uint_fast64_t> const& groupsA) { storm::expressions::Expression MathsatSmtSolver::getInterpolant(std::vector<uint_fast64_t> const& groupsA) {
#ifdef STORM_HAVE_MSAT #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; std::vector<int> msatInterpolationGroupsA;
msatInterpolationGroupsA.reserve(groupsA.size()); msatInterpolationGroupsA.reserve(groupsA.size());
for (auto groupOfA : groupsA) { for (auto groupOfA : groupsA) {
auto groupIter = this->interpolationGroups.find(groupOfA); 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); msatInterpolationGroupsA.push_back(groupIter->second);
} }
msat_term interpolant = msat_get_interpolant(env, msatInterpolationGroupsA.data(), msatInterpolationGroupsA.size()); msat_term interpolant = msat_get_interpolant(env, msatInterpolationGroupsA.data(), msatInterpolationGroupsA.size());
@ -354,7 +386,7 @@ namespace storm {
return this->expressionAdapter->translateTerm(interpolant); return this->expressionAdapter->translateTerm(interpolant);
#else #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 #endif
} }
} }

8
src/solver/MathsatSmtSolver.h
View File

@ -41,7 +41,7 @@ namespace storm {
class MathSatModelReference : public SmtSolver::ModelReference { class MathSatModelReference : public SmtSolver::ModelReference {
public: public:
#ifdef STORM_HAVE_MSAT #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 #endif
virtual bool getBooleanValue(std::string const& name) const override; virtual bool getBooleanValue(std::string const& name) const override;
virtual int_fast64_t getIntegerValue(std::string const& name) const override; virtual int_fast64_t getIntegerValue(std::string const& name) const override;
@ -50,11 +50,11 @@ namespace storm {
private: private:
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
msat_env const& env; msat_env const& env;
storm::adapters::MathsatExpressionAdapter& expressionAdapter;
msat_term* model;
std::unordered_map<std::string, uint_fast64_t> const& atomNameToSlotMapping;
#endif #endif
}; };
public:
MathsatSmtSolver(Options const& options = Options()); MathsatSmtSolver(Options const& options = Options());
virtual ~MathsatSmtSolver(); virtual ~MathsatSmtSolver();
@ -63,6 +63,8 @@ namespace storm {
virtual void pop() override; virtual void pop() override;
virtual void pop(uint_fast64_t n) override;
virtual void reset() override; virtual void reset() override;
virtual void add(storm::expressions::Expression const& assertion) override; virtual void add(storm::expressions::Expression const& assertion) override;

8
src/solver/Z3SmtSolver.cpp
View File

@ -146,7 +146,7 @@ namespace storm {
#endif #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 #ifdef STORM_HAVE_Z3
lastCheckAssumptions = true; lastCheckAssumptions = true;
@ -216,7 +216,7 @@ namespace storm {
{ {
#ifdef STORM_HAVE_Z3 #ifdef STORM_HAVE_Z3
std::vector<storm::expressions::SimpleValuation> valuations; 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; return valuations;
#else #else
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
@ -227,7 +227,7 @@ namespace storm {
{ {
#ifdef STORM_HAVE_Z3 #ifdef STORM_HAVE_Z3
for (storm::expressions::Expression const& atom : important) { 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; uint_fast64_t numberOfModels = 0;
@ -278,7 +278,7 @@ namespace storm {
{ {
#ifdef STORM_HAVE_Z3 #ifdef STORM_HAVE_Z3
for (storm::expressions::Expression const& atom : important) { 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; uint_fast64_t numberOfModels = 0;

142
test/functional/solver/MathSatSmtSolverTest.cpp
View File

@ -2,17 +2,17 @@
#include "storm-config.h" #include "storm-config.h"
#ifdef STORM_HAVE_MSAT #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"))); 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_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()); ASSERT_NO_THROW(s.reset());
storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
@ -24,21 +24,21 @@ TEST(MathSatSmtSolver, CheckSat) {
&& c == (a * b) && c == (a * b)
&& b + a > c; && b + a > c;
ASSERT_NO_THROW(s.assertExpression(exprFormula));
ASSERT_NO_THROW(s.add(exprFormula));
ASSERT_NO_THROW(result = s.check()); 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()); 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"))); 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_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()); ASSERT_NO_THROW(s.reset());
storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
@ -50,40 +50,40 @@ TEST(MathSatSmtSolver, CheckUnsat) {
&& c == (a + b + storm::expressions::Expression::createIntegerLiteral(1)) && c == (a + b + storm::expressions::Expression::createIntegerLiteral(1))
&& b + a > c; && b + a > c;
ASSERT_NO_THROW(s.assertExpression(exprFormula));
ASSERT_NO_THROW(s.add(exprFormula));
ASSERT_NO_THROW(result = s.check()); 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 expr1 = storm::expressions::Expression::createTrue();
storm::expressions::Expression expr2 = storm::expressions::Expression::createFalse(); storm::expressions::Expression expr2 = storm::expressions::Expression::createFalse();
storm::expressions::Expression expr3 = 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_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.push());
ASSERT_NO_THROW(s.assertExpression(expr2));
ASSERT_NO_THROW(s.add(expr2));
ASSERT_NO_THROW(result = s.check()); 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(s.pop());
ASSERT_NO_THROW(result = s.check()); 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.push());
ASSERT_NO_THROW(s.assertExpression(expr2));
ASSERT_NO_THROW(s.add(expr2));
ASSERT_NO_THROW(result = s.check()); 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.push());
ASSERT_NO_THROW(s.assertExpression(expr3));
ASSERT_NO_THROW(s.add(expr3));
ASSERT_NO_THROW(result = s.check()); 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(s.pop(2));
ASSERT_NO_THROW(result = s.check()); 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()); ASSERT_NO_THROW(s.reset());
storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
@ -96,21 +96,21 @@ TEST(MathSatSmtSolver, Backtracking) {
&& b + a > c; && b + a > c;
storm::expressions::Expression exprFormula2 = c > a + b + storm::expressions::Expression::createIntegerLiteral(1); 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_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.push());
ASSERT_NO_THROW(s.assertExpression(exprFormula2));
ASSERT_NO_THROW(s.add(exprFormula2));
ASSERT_NO_THROW(result = s.check()); 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(s.pop());
ASSERT_NO_THROW(result = s.check()); 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 a = storm::expressions::Expression::createIntegerVariable("a");
storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); 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 f2 = storm::expressions::Expression::createBooleanVariable("f2");
storm::expressions::Expression exprFormula2 = f2.implies(c > a + b + storm::expressions::Expression::createIntegerLiteral(1)); 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_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_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_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_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_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::solver::SmtSolver::CheckResult result;
storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
@ -150,9 +150,9 @@ TEST(MathSatSmtSolver, GenerateModel) {
&& c == (a + b - storm::expressions::Expression::createIntegerLiteral(1)) && c == (a + b - storm::expressions::Expression::createIntegerLiteral(1))
&& b + a > c; && b + a > c;
(s.assertExpression(exprFormula));
(s.add(exprFormula));
(result = s.check()); (result = s.check());
ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
storm::expressions::SimpleValuation model; storm::expressions::SimpleValuation model;
(model = s.getModel()); (model = s.getModel());
int_fast64_t a_eval = model.getIntegerValue("a"); int_fast64_t a_eval = model.getIntegerValue("a");
@ -161,9 +161,9 @@ TEST(MathSatSmtSolver, GenerateModel) {
ASSERT_TRUE(c_eval == a_eval + b_eval - 1); 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 a = storm::expressions::Expression::createIntegerVariable("a");
storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); 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 exprFormula2 = y.implies(a < storm::expressions::Expression::createIntegerLiteral(5));
storm::expressions::Expression exprFormula3 = z.implies(b < 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}); 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 a = storm::expressions::Expression::createIntegerVariable("a");
storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); 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 f2 = storm::expressions::Expression::createBooleanVariable("f2");
storm::expressions::Expression exprFormula2 = f2.implies(c > a + b + storm::expressions::Expression::createIntegerLiteral(1)); 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 })); (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(); std::vector<storm::expressions::Expression> unsatCore = s.getUnsatAssumptions();
ASSERT_EQ(unsatCore.size(), 1); ASSERT_EQ(unsatCore.size(), 1);
ASSERT_TRUE(unsatCore[0].isVariable()); ASSERT_TRUE(unsatCore[0].isVariable());
ASSERT_STREQ("f2", unsatCore[0].getIdentifier().c_str()); 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 a = storm::expressions::Expression::createIntegerVariable("a");
storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b");
@ -232,28 +232,28 @@ TEST(MathSatSmtSolver, InterpolationTest) {
storm::expressions::Expression exprFormula3 = c > a; storm::expressions::Expression exprFormula3 = c > a;
s.setInterpolationGroup(0); s.setInterpolationGroup(0);
s.assertExpression(exprFormula);
s.add(exprFormula);
s.setInterpolationGroup(1); s.setInterpolationGroup(1);
s.assertExpression(exprFormula2);
s.add(exprFormula2);
s.setInterpolationGroup(2); s.setInterpolationGroup(2);
s.assertExpression(exprFormula3);
s.add(exprFormula3);
ASSERT_NO_THROW(result = s.check()); 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; storm::expressions::Expression interpol;
ASSERT_NO_THROW(interpol = s.getInterpolant({0, 1})); 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_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.reset());
ASSERT_NO_THROW(s2.assertExpression(interpol && exprFormula3));
ASSERT_NO_THROW(s2.add(interpol && exprFormula3));
ASSERT_NO_THROW(result = s2.check()); ASSERT_NO_THROW(result = s2.check());
ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::UNSAT);
ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
} }
#endif #endif

84
test/functional/solver/Z3SmtSolverTest.cpp
View File

@ -7,13 +7,13 @@
TEST(Z3SmtSolver, CheckSat) { TEST(Z3SmtSolver, CheckSat) {
storm::solver::Z3SmtSolver s; 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"))); 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_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()); ASSERT_NO_THROW(s.reset());
storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a"); storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
@ -25,21 +25,21 @@ TEST(Z3SmtSolver, CheckSat) {
&& c == (a * b) && c == (a * b)
&& b + a > c; && b + a > c;
ASSERT_NO_THROW(s.assertExpression(exprFormula));
ASSERT_NO_THROW(s.add(exprFormula));
ASSERT_NO_THROW(result = s.check()); 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()); ASSERT_NO_THROW(s.reset());
} }
TEST(Z3SmtSolver, CheckUnsat) { TEST(Z3SmtSolver, CheckUnsat) {
storm::solver::Z3SmtSolver s; 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"))); 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_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()); ASSERT_NO_THROW(s.reset());
@ -52,41 +52,41 @@ TEST(Z3SmtSolver, CheckUnsat) {
&& c == (a * b) && c == (a * b)
&& b + a > c; && b + a > c;
ASSERT_NO_THROW(s.assertExpression(exprFormula));
ASSERT_NO_THROW(s.add(exprFormula));
ASSERT_NO_THROW(result = s.check()); 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) { TEST(Z3SmtSolver, Backtracking) {
storm::solver::Z3SmtSolver s; 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 expr1 = storm::expressions::Expression::createTrue();
storm::expressions::Expression expr2 = storm::expressions::Expression::createFalse(); storm::expressions::Expression expr2 = storm::expressions::Expression::createFalse();
storm::expressions::Expression expr3 = 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_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.push());
ASSERT_NO_THROW(s.assertExpression(expr2));
ASSERT_NO_THROW(s.add(expr2));
ASSERT_NO_THROW(result = s.check()); 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(s.pop());
ASSERT_NO_THROW(result = s.check()); 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.push());
ASSERT_NO_THROW(s.assertExpression(expr2));
ASSERT_NO_THROW(s.add(expr2));
ASSERT_NO_THROW(result = s.check()); 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.push());
ASSERT_NO_THROW(s.assertExpression(expr3));
ASSERT_NO_THROW(s.add(expr3));
ASSERT_NO_THROW(result = s.check()); 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(s.pop(2));
ASSERT_NO_THROW(result = s.check()); 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()); ASSERT_NO_THROW(s.reset());
@ -100,21 +100,21 @@ TEST(Z3SmtSolver, Backtracking) {
&& b + a > c; && b + a > c;
storm::expressions::Expression exprFormula2 = a >= storm::expressions::Expression::createIntegerLiteral(2); 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_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.push());
ASSERT_NO_THROW(s.assertExpression(exprFormula2));
ASSERT_NO_THROW(s.add(exprFormula2));
ASSERT_NO_THROW(result = s.check()); 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(s.pop());
ASSERT_NO_THROW(result = s.check()); 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) { TEST(Z3SmtSolver, Assumptions) {
storm::solver::Z3SmtSolver s; 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 a = storm::expressions::Expression::createIntegerVariable("a");
storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b"); 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 f2 = storm::expressions::Expression::createBooleanVariable("f2");
storm::expressions::Expression exprFormula2 = f2.implies(a >= storm::expressions::Expression::createIntegerLiteral(2)); 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_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_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_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_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_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) { TEST(Z3SmtSolver, GenerateModel) {
@ -154,9 +154,9 @@ TEST(Z3SmtSolver, GenerateModel) {
&& c == (a * b) && c == (a * b)
&& b + a > c; && b + a > c;
(s.assertExpression(exprFormula));
(s.add(exprFormula));
(result = s.check()); (result = s.check());
ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
storm::expressions::SimpleValuation model; storm::expressions::SimpleValuation model;
(model = s.getModel()); (model = s.getModel());
int_fast64_t a_eval; 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 exprFormula2 = y.implies(a < storm::expressions::Expression::createIntegerLiteral(5));
storm::expressions::Expression exprFormula3 = z.implies(b < 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}); 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 f2 = storm::expressions::Expression::createBooleanVariable("f2");
storm::expressions::Expression exprFormula2 = f2.implies(a >= storm::expressions::Expression::createIntegerLiteral(2)); 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 }); 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(); std::vector<storm::expressions::Expression> unsatCore = s.getUnsatAssumptions();
ASSERT_EQ(unsatCore.size(), 1); ASSERT_EQ(unsatCore.size(), 1);
ASSERT_TRUE(unsatCore[0].isVariable()); ASSERT_TRUE(unsatCore[0].isVariable());

Write Preview
Loading…
Cancel
Save