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

All tests passing again. 

Former-commit-id: ffa8bef2d2
tempestpy_adaptions
dehnert 10 years ago
parent
ba14ba3613
commit
b5d55335a6
10 changed files with 257 additions and 139 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 81
      src/solver/MathsatSmtSolver.cpp
  2. 30
      src/solver/MathsatSmtSolver.h
  3. 6
      src/solver/SmtSolver.cpp
  4. 15
      src/solver/SmtSolver.h
  5. 89
      src/solver/Z3SmtSolver.cpp
  6. 15
      src/solver/Z3SmtSolver.h
  7. 4
      src/storage/expressions/Expression.cpp
  8. 7
      src/storage/expressions/Expression.h
  9. 35
      test/functional/solver/MathSatSmtSolverTest.cpp
  10. 114
      test/functional/solver/Z3SmtSolverTest.cpp

81
src/solver/MathsatSmtSolver.cpp
View File

@ -7,9 +7,63 @@
namespace storm {
namespace solver {
#ifdef STORM_HAVE_MSAT
MathsatSmtSolver::MathsatAllsatModelReference::MathsatAllsatModelReference(msat_env const& env, msat_term* model, std::unordered_map<std::string, uint_fast64_t> const& atomNameToSlotMapping) : env(env), model(model), atomNameToSlotMapping(atomNameToSlotMapping) {
// Intentionally left empty.
}
#endif
bool MathsatSmtSolver::MathsatAllsatModelReference::getBooleanValue(std::string const& name) const {
std::unordered_map<std::string, uint_fast64_t>::const_iterator nameSlotPair = atomNameToSlotMapping.find(name);
STORM_LOG_THROW(nameSlotPair != atomNameToSlotMapping.end(), storm::exceptions::InvalidArgumentException, "Cannot retrieve value of unknown variable '" << name << "' from model.");
msat_term selectedTerm = model[nameSlotPair->second];
if (msat_term_is_not(env, selectedTerm)) {
return false;
} else {
return true;
}
}
int_fast64_t MathsatSmtSolver::MathsatAllsatModelReference::getIntegerValue(std::string const& name) const {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unable to retrieve integer value from model that only contains boolean values.");
}
double MathsatSmtSolver::MathsatAllsatModelReference::getDoubleValue(std::string const& name) const {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unable to retrieve double value from model that only contains boolean values.");
}
#ifdef STORM_HAVE_MSAT
MathsatSmtSolver::MathsatModelReference::MathsatModelReference(msat_env const& env, storm::adapters::MathsatExpressionAdapter& expressionAdapter) : env(env), expressionAdapter(expressionAdapter) {
// Intentionally left empty.
}
#endif
bool MathsatSmtSolver::MathsatModelReference::getBooleanValue(std::string const& name) const {
msat_term msatVariable = expressionAdapter.translateExpression(storm::expressions::Expression::createBooleanVariable(name), false);
msat_term msatValue = msat_get_model_value(env, msatVariable);
storm::expressions::Expression value = expressionAdapter.translateTerm(msatValue);
STORM_LOG_THROW(value.hasBooleanReturnType(), storm::exceptions::InvalidArgumentException, "Unable to retrieve boolean value of non-boolean variable '" << name << "'.");
return value.evaluateAsBool();
}
int_fast64_t MathsatSmtSolver::MathsatModelReference::getIntegerValue(std::string const& name) const {
msat_term msatVariable = expressionAdapter.translateExpression(storm::expressions::Expression::createBooleanVariable(name), false);
msat_term msatValue = msat_get_model_value(env, msatVariable);
storm::expressions::Expression value = expressionAdapter.translateTerm(msatValue);
STORM_LOG_THROW(value.hasIntegralReturnType(), storm::exceptions::InvalidArgumentException, "Unable to retrieve integer value of non-integer variable '" << name << "'.");
return value.evaluateAsInt();
}
double MathsatSmtSolver::MathsatModelReference::getDoubleValue(std::string const& name) const {
msat_term msatVariable = expressionAdapter.translateExpression(storm::expressions::Expression::createBooleanVariable(name), false);
msat_term msatValue = msat_get_model_value(env, msatVariable);
storm::expressions::Expression value = expressionAdapter.translateTerm(msatValue);
STORM_LOG_THROW(value.hasIntegralReturnType(), storm::exceptions::InvalidArgumentException, "Unable to retrieve double value of non-double variable '" << name << "'.");
return value.evaluateAsDouble();
}
MathsatSmtSolver::MathsatSmtSolver(Options const& options)
#ifdef STORM_HAVE_MSAT
: lastCheckAssumptions(false), lastResult(CheckResult::Unknown)
: expressionAdapter(nullptr), lastCheckAssumptions(false), lastResult(CheckResult::Unknown)
#endif
{
#ifdef STORM_HAVE_MSAT
@ -35,7 +89,7 @@ namespace storm {
}
MathsatSmtSolver::~MathsatSmtSolver() {
STORM_LOG_THROW(MSAT_ERROR_ENV(env), storm::exceptions::UnexpectedException, "Illegal MathSAT environment.");
STORM_LOG_THROW(!MSAT_ERROR_ENV(env), storm::exceptions::UnexpectedException, "Illegal MathSAT environment.");
msat_destroy_env(env);
}
@ -154,7 +208,7 @@ namespace storm {
#endif
}
storm::expressions::SimpleValuation MathsatSmtSolver::getModel()
storm::expressions::SimpleValuation MathsatSmtSolver::getModelAsValuation()
{
#ifdef STORM_HAVE_MSAT
STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable.");
@ -163,6 +217,15 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
#endif
}
std::shared_ptr<SmtSolver::ModelReference> MathsatSmtSolver::getModel() {
#ifdef STORM_HAVE_MSAT
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 std::shared_ptr<SmtSolver::ModelReference>(new MathsatModelReference(env, *expressionAdapter));
#else
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
#endif
}
#ifdef STORM_HAVE_MSAT
storm::expressions::SimpleValuation MathsatSmtSolver::convertMathsatModelToValuation() {
@ -175,18 +238,18 @@ namespace storm {
msat_term t, v;
msat_model_iterator_next(modelIterator, &t, &v);
storm::expressions::Expression variableIInterpretation = this->expressionAdapter->translateTerm(v);
storm::expressions::Expression variableInterpretation = this->expressionAdapter->translateTerm(v);
char* name = msat_decl_get_name(msat_term_get_decl(t));
switch (variableIInterpretation.getReturnType()) {
switch (variableInterpretation.getReturnType()) {
case storm::expressions::ExpressionReturnType::Bool:
stormModel.addBooleanIdentifier(std::string(name), variableIInterpretation.evaluateAsBool());
stormModel.addBooleanIdentifier(std::string(name), variableInterpretation.evaluateAsBool());
break;
case storm::expressions::ExpressionReturnType::Int:
stormModel.addIntegerIdentifier(std::string(name), variableIInterpretation.evaluateAsInt());
stormModel.addIntegerIdentifier(std::string(name), variableInterpretation.evaluateAsInt());
break;
case storm::expressions::ExpressionReturnType::Double:
stormModel.addDoubleIdentifier(std::string(name), variableIInterpretation.evaluateAsDouble());
stormModel.addDoubleIdentifier(std::string(name), variableInterpretation.evaluateAsDouble());
break;
default:
STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Variable interpretation in model is not of type bool, int or double.")
@ -260,7 +323,7 @@ namespace storm {
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);
MathsatSmtSolver::MathsatAllsatModelReference modelReference(user->env, model, user->atomNameToSlotMapping);
if (user->callback(modelReference)) {
return 1;
} else {

30
src/solver/MathsatSmtSolver.h
View File

@ -25,11 +25,7 @@ namespace storm {
*/
class Options {
public:
Options() : enableModelGeneration(false), enableUnsatCoreGeneration(false), enableInterpolantGeneration(false) {
// Intentionally left empty.
}
Options(bool enableModelGeneration, bool enableUnsatCoreGeneration, bool enableInterpolantGeneration) : enableModelGeneration(enableModelGeneration), enableUnsatCoreGeneration(enableUnsatCoreGeneration), enableInterpolantGeneration(enableInterpolantGeneration) {
Options(bool enableModelGeneration = true, bool enableUnsatCoreGeneration = false, bool enableInterpolantGeneration = false) : enableModelGeneration(enableModelGeneration), enableUnsatCoreGeneration(enableUnsatCoreGeneration), enableInterpolantGeneration(enableInterpolantGeneration) {
// Intentionally left empty.
}
@ -38,10 +34,10 @@ namespace storm {
bool enableInterpolantGeneration = false;
};
class MathSatModelReference : public SmtSolver::ModelReference {
class MathsatAllsatModelReference : public SmtSolver::ModelReference {
public:
#ifdef STORM_HAVE_MSAT
MathSatModelReference(msat_env const& env, msat_term* model, std::unordered_map<std::string, uint_fast64_t> const& atomNameToSlotMapping);
MathsatAllsatModelReference(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;
@ -55,6 +51,22 @@ namespace storm {
#endif
};
class MathsatModelReference : public SmtSolver::ModelReference {
public:
#ifdef STORM_HAVE_MSAT
MathsatModelReference(msat_env const& env, storm::adapters::MathsatExpressionAdapter& expressionAdapter);
#endif
virtual bool getBooleanValue(std::string const& name) const override;
virtual int_fast64_t getIntegerValue(std::string const& name) const override;
virtual double getDoubleValue(std::string const& name) const override;
private:
#ifdef STORM_HAVE_MSAT
msat_env const& env;
storm::adapters::MathsatExpressionAdapter& expressionAdapter;
#endif
};
MathsatSmtSolver(Options const& options = Options());
virtual ~MathsatSmtSolver();
@ -75,8 +87,10 @@ namespace storm {
virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) override;
virtual storm::expressions::SimpleValuation getModel() override;
virtual storm::expressions::SimpleValuation getModelAsValuation() override;
virtual std::shared_ptr<SmtSolver::ModelReference> getModel() override;
virtual std::vector<storm::expressions::SimpleValuation> allSat(std::vector<storm::expressions::Expression> const& important) override;
virtual uint_fast64_t allSat(std::vector<storm::expressions::Expression> const& important, std::function<bool(storm::expressions::SimpleValuation&)> const& callback) override;

6
src/solver/SmtSolver.cpp
View File

@ -32,7 +32,11 @@ namespace storm {
}
}
storm::expressions::SimpleValuation SmtSolver::getModel() {
storm::expressions::SimpleValuation SmtSolver::getModelAsValuation() {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation.");
}
std::shared_ptr<SmtSolver::ModelReference> SmtSolver::getModel() {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "This solver does not support model generation.");
}

15
src/solver/SmtSolver.h
View File

@ -133,8 +133,21 @@ namespace storm {
* solver was instantiated with support for model generation. Note that this function may throw an exception
* if it is not called immediately after a call to check() or checkWithAssumptions() that returned Sat
* depending on the implementation.
*
* @return A valuation that holds the values of the variables in the current model.
*/
virtual storm::expressions::SimpleValuation getModelAsValuation();
/*!
* If the last call to check() or checkWithAssumptions() returned Sat, this method retrieves a model that
* satisfies all assertions on the solver's stack (as well as provided assumptions), provided that the
* solver was instantiated with support for model generation. Note that this function may throw an exception
* if it is not called immediately after a call to check() or checkWithAssumptions() that returned Sat
* depending on the implementation.
*
* @return A reference to a model that can be queried for the values of specific variables.
*/
virtual storm::expressions::SimpleValuation getModel();
virtual std::shared_ptr<ModelReference> getModel();
/*!
* Performs AllSat over the (provided) important atoms. That is, this function returns all models of the

89
src/solver/Z3SmtSolver.cpp
View File

@ -1,4 +1,4 @@
#include "src/solver/Z3SmtSolver.h"
#include "src/solver/Z3Smtsolver.h"
#include "src/exceptions/NotSupportedException.h"
#include "src/exceptions/InvalidStateException.h"
@ -6,7 +6,7 @@
namespace storm {
namespace solver {
#ifdef STORM_HAVE_Z3
Z3SmtSolver::Z3ModelReference::Z3ModelReference(z3::model const& model, storm::adapters::Z3ExpressionAdapter& expressionAdapter) : model(model), expressionAdapter(expressionAdapter) {
Z3SmtSolver::Z3ModelReference::Z3ModelReference(z3::model model, storm::adapters::Z3ExpressionAdapter& expressionAdapter) : model(model), expressionAdapter(expressionAdapter) {
// Intentionally left empty.
}
#endif
@ -43,11 +43,15 @@ namespace storm {
Z3SmtSolver::Z3SmtSolver()
#ifdef STORM_HAVE_Z3
: context(), solver(context), expressionAdapter(context), lastCheckAssumptions(false), lastResult(CheckResult::Unknown)
: context(nullptr), solver(nullptr), expressionAdapter(nullptr), lastCheckAssumptions(false), lastResult(CheckResult::Unknown)
#endif
{
// Intentionally left empty.
}
z3::config config;
config.set("model", true);
context = std::unique_ptr<z3::context>(new z3::context(config));
solver = std::unique_ptr<z3::solver>(new z3::solver(*context));
expressionAdapter = std::unique_ptr<storm::adapters::Z3ExpressionAdapter>(new storm::adapters::Z3ExpressionAdapter(*context));
}
Z3SmtSolver::~Z3SmtSolver() {
// Intentionally left empty.
@ -56,7 +60,7 @@ namespace storm {
void Z3SmtSolver::push()
{
#ifdef STORM_HAVE_Z3
this->solver.push();
this->solver->push();
#else
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
#endif
@ -65,7 +69,7 @@ namespace storm {
void Z3SmtSolver::pop()
{
#ifdef STORM_HAVE_Z3
this->solver.pop();
this->solver->pop();
#else
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
#endif
@ -74,7 +78,7 @@ namespace storm {
void Z3SmtSolver::pop(uint_fast64_t n)
{
#ifdef STORM_HAVE_Z3
this->solver.pop(static_cast<unsigned int>(n));
this->solver->pop(static_cast<unsigned int>(n));
#else
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
#endif
@ -83,7 +87,7 @@ namespace storm {
void Z3SmtSolver::reset()
{
#ifdef STORM_HAVE_Z3
this->solver.reset();
this->solver->reset();
#else
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
#endif
@ -92,7 +96,7 @@ namespace storm {
void Z3SmtSolver::add(storm::expressions::Expression const& assertion)
{
#ifdef STORM_HAVE_Z3
this->solver.add(expressionAdapter.translateExpression(assertion, true));
this->solver->add(expressionAdapter->translateExpression(assertion, true));
#else
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
#endif
@ -102,7 +106,7 @@ namespace storm {
{
#ifdef STORM_HAVE_Z3
lastCheckAssumptions = false;
switch (this->solver.check()) {
switch (this->solver->check()) {
case z3::sat:
this->lastResult = SmtSolver::CheckResult::Sat;
break;
@ -123,13 +127,13 @@ namespace storm {
{
#ifdef STORM_HAVE_Z3
lastCheckAssumptions = true;
z3::expr_vector z3Assumptions(this->context);
z3::expr_vector z3Assumptions(*this->context);
for (storm::expressions::Expression assumption : assumptions) {
z3Assumptions.push_back(this->expressionAdapter.translateExpression(assumption));
z3Assumptions.push_back(this->expressionAdapter->translateExpression(assumption));
}
switch (this->solver.check(z3Assumptions)) {
switch (this->solver->check(z3Assumptions)) {
case z3::sat:
this->lastResult = SmtSolver::CheckResult::Sat;
break;
@ -150,13 +154,13 @@ namespace storm {
{
#ifdef STORM_HAVE_Z3
lastCheckAssumptions = true;
z3::expr_vector z3Assumptions(this->context);
z3::expr_vector z3Assumptions(*this->context);
for (storm::expressions::Expression assumption : assumptions) {
z3Assumptions.push_back(this->expressionAdapter.translateExpression(assumption));
z3Assumptions.push_back(this->expressionAdapter->translateExpression(assumption));
}
switch (this->solver.check(z3Assumptions)) {
switch (this->solver->check(z3Assumptions)) {
case z3::sat:
this->lastResult = SmtSolver::CheckResult::Sat;
break;
@ -173,15 +177,24 @@ namespace storm {
#endif
}
storm::expressions::SimpleValuation Z3SmtSolver::getModel()
storm::expressions::SimpleValuation Z3SmtSolver::getModelAsValuation()
{
#ifdef STORM_HAVE_Z3
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->convertZ3ModelToValuation(this->solver.get_model());
return this->convertZ3ModelToValuation(this->solver->get_model());
#else
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
#endif
}
std::shared_ptr<SmtSolver::ModelReference> Z3SmtSolver::getModel() {
#ifdef STORM_HAVE_Z3
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 std::shared_ptr<SmtSolver::ModelReference>(new Z3ModelReference(this->solver->get_model(), *this->expressionAdapter));
#else
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
#endif
}
#ifdef STORM_HAVE_Z3
storm::expressions::SimpleValuation Z3SmtSolver::convertZ3ModelToValuation(z3::model const& model) {
@ -189,17 +202,17 @@ namespace storm {
for (unsigned i = 0; i < model.num_consts(); ++i) {
z3::func_decl variableI = model.get_const_decl(i);
storm::expressions::Expression variableIInterpretation = this->expressionAdapter.translateExpression(model.get_const_interp(variableI));
storm::expressions::Expression variableInterpretation = this->expressionAdapter->translateExpression(model.get_const_interp(variableI));
switch (variableIInterpretation.getReturnType()) {
switch (variableInterpretation.getReturnType()) {
case storm::expressions::ExpressionReturnType::Bool:
stormModel.addBooleanIdentifier(variableI.name().str(), variableIInterpretation.evaluateAsBool());
stormModel.addBooleanIdentifier(variableI.name().str(), variableInterpretation.evaluateAsBool());
break;
case storm::expressions::ExpressionReturnType::Int:
stormModel.addIntegerIdentifier(variableI.name().str(), variableIInterpretation.evaluateAsInt());
stormModel.addIntegerIdentifier(variableI.name().str(), variableInterpretation.evaluateAsInt());
break;
case storm::expressions::ExpressionReturnType::Double:
stormModel.addDoubleIdentifier(variableI.name().str(), variableIInterpretation.evaluateAsDouble());
stormModel.addDoubleIdentifier(variableI.name().str(), variableInterpretation.evaluateAsDouble());
break;
default:
STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Variable interpretation in model is not of type bool, int or double.")
@ -239,21 +252,21 @@ namespace storm {
// Enumerate models as long as the conjunction is satisfiable and the callback has not aborted the enumeration.
while (proceed && this->check() == CheckResult::Sat) {
++numberOfModels;
z3::model model = this->solver.get_model();
z3::model model = this->solver->get_model();
z3::expr modelExpr = this->context.bool_val(true);
z3::expr modelExpr = this->context->bool_val(true);
storm::expressions::SimpleValuation valuation;
for (storm::expressions::Expression const& importantAtom : important) {
z3::expr z3ImportantAtom = this->expressionAdapter.translateExpression(importantAtom);
z3::expr z3ImportantAtom = this->expressionAdapter->translateExpression(importantAtom);
z3::expr z3ImportantAtomValuation = model.eval(z3ImportantAtom, true);
modelExpr = modelExpr && (z3ImportantAtom == z3ImportantAtomValuation);
if (importantAtom.getReturnType() == storm::expressions::ExpressionReturnType::Bool) {
valuation.addBooleanIdentifier(importantAtom.getIdentifier(), this->expressionAdapter.translateExpression(z3ImportantAtomValuation).evaluateAsBool());
valuation.addBooleanIdentifier(importantAtom.getIdentifier(), this->expressionAdapter->translateExpression(z3ImportantAtomValuation).evaluateAsBool());
} else if (importantAtom.getReturnType() == storm::expressions::ExpressionReturnType::Int) {
valuation.addIntegerIdentifier(importantAtom.getIdentifier(), this->expressionAdapter.translateExpression(z3ImportantAtomValuation).evaluateAsInt());
valuation.addIntegerIdentifier(importantAtom.getIdentifier(), this->expressionAdapter->translateExpression(z3ImportantAtomValuation).evaluateAsInt());
} else if (importantAtom.getReturnType() == storm::expressions::ExpressionReturnType::Double) {
valuation.addDoubleIdentifier(importantAtom.getIdentifier(), this->expressionAdapter.translateExpression(z3ImportantAtomValuation).evaluateAsDouble());
valuation.addDoubleIdentifier(importantAtom.getIdentifier(), this->expressionAdapter->translateExpression(z3ImportantAtomValuation).evaluateAsDouble());
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Important atom has invalid type.");
}
@ -262,7 +275,7 @@ namespace storm {
// Check if we are required to proceed, and if so rule out the current model.
proceed = callback(valuation);
if (proceed) {
this->solver.add(!modelExpr);
this->solver->add(!modelExpr);
}
}
@ -290,22 +303,22 @@ namespace storm {
// Enumerate models as long as the conjunction is satisfiable and the callback has not aborted the enumeration.
while (proceed && this->check() == CheckResult::Sat) {
++numberOfModels;
z3::model model = this->solver.get_model();
z3::model model = this->solver->get_model();
z3::expr modelExpr = this->context.bool_val(true);
z3::expr modelExpr = this->context->bool_val(true);
storm::expressions::SimpleValuation valuation;
for (storm::expressions::Expression const& importantAtom : important) {
z3::expr z3ImportantAtom = this->expressionAdapter.translateExpression(importantAtom);
z3::expr z3ImportantAtom = this->expressionAdapter->translateExpression(importantAtom);
z3::expr z3ImportantAtomValuation = model.eval(z3ImportantAtom, true);
modelExpr = modelExpr && (z3ImportantAtom == z3ImportantAtomValuation);
}
Z3ModelReference modelRef(model, expressionAdapter);
Z3ModelReference modelRef(model, *expressionAdapter);
// Check if we are required to proceed, and if so rule out the current model.
proceed = callback(modelRef);
if (proceed) {
this->solver.add(!modelExpr);
this->solver->add(!modelExpr);
}
}
@ -321,11 +334,11 @@ namespace storm {
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.");
z3::expr_vector z3UnsatAssumptions = this->solver.unsat_core();
z3::expr_vector z3UnsatAssumptions = this->solver->unsat_core();
std::vector<storm::expressions::Expression> unsatAssumptions;
for (unsigned int i = 0; i < z3UnsatAssumptions.size(); ++i) {
unsatAssumptions.push_back(this->expressionAdapter.translateExpression(z3UnsatAssumptions[i]));
unsatAssumptions.push_back(this->expressionAdapter->translateExpression(z3UnsatAssumptions[i]));
}
return unsatAssumptions;

15
src/solver/Z3SmtSolver.h
View File

@ -17,15 +17,16 @@ namespace storm {
class Z3ModelReference : public SmtSolver::ModelReference {
public:
#ifdef STORM_HAVE_Z3
Z3ModelReference(z3::model const& m, storm::adapters::Z3ExpressionAdapter& expressionAdapter);
Z3ModelReference(z3::model m, storm::adapters::Z3ExpressionAdapter& expressionAdapter);
#endif
virtual bool getBooleanValue(std::string const& name) const override;
virtual int_fast64_t getIntegerValue(std::string const& name) const override;
virtual double getDoubleValue(std::string const& name) const override;
private:
#ifdef STORM_HAVE_Z3
// The Z3 model out of which the information can be extracted.
z3::model const& model;
z3::model model;
// The expression adapter that is used to translate the variable names.
storm::adapters::Z3ExpressionAdapter& expressionAdapter;
@ -52,7 +53,9 @@ namespace storm {
virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) override;
virtual storm::expressions::SimpleValuation getModel() override;
virtual storm::expressions::SimpleValuation getModelAsValuation() override;
virtual std::shared_ptr<SmtSolver::ModelReference> getModel() override;
virtual std::vector<storm::expressions::SimpleValuation> allSat(std::vector<storm::expressions::Expression> const& important) override;
@ -73,13 +76,13 @@ namespace storm {
storm::expressions::SimpleValuation convertZ3ModelToValuation(z3::model const& model);
// The context used by the solver.
z3::context context;
std::unique_ptr<z3::context> context;
// The actual solver object.
z3::solver solver;
std::unique_ptr<z3::solver> solver;
// An expression adapter that is used for translating the expression into Z3's format.
storm::adapters::Z3ExpressionAdapter expressionAdapter;
std::unique_ptr<storm::adapters::Z3ExpressionAdapter> expressionAdapter;
// A flag storing whether the last call to a check method provided aussumptions.
bool lastCheckAssumptions;

4
src/storage/expressions/Expression.cpp
View File

@ -145,6 +145,10 @@ namespace storm {
return this->getReturnType() == ExpressionReturnType::Bool;
}
bool Expression::hasIntegralReturnType() const {
return this->getReturnType() == ExpressionReturnType::Int;
}
Expression Expression::createBooleanLiteral(bool value) {
return Expression(std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(value)));
}

7
src/storage/expressions/Expression.h
View File

@ -302,6 +302,13 @@ namespace storm {
*/
bool hasBooleanReturnType() const;
/*!
* Retrieves whether the expression has an integral return type.
*
* @return True iff the expression has a integral return type.
*/
bool hasIntegralReturnType() const;
/*!
* Accepts the given visitor.
*

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

@ -150,15 +150,14 @@ TEST(MathsatSmtSolver, GenerateModel) {
&& c == (a + b - storm::expressions::Expression::createIntegerLiteral(1))
&& b + a > c;
(s.add(exprFormula));
(result = s.check());
s.add(exprFormula);
result = s.check();
ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
storm::expressions::SimpleValuation model;
(model = s.getModel());
int_fast64_t a_eval = model.getIntegerValue("a");
int_fast64_t b_eval = model.getIntegerValue("b");
int_fast64_t c_eval = model.getIntegerValue("c");
ASSERT_TRUE(c_eval == a_eval + b_eval - 1);
std::shared_ptr<storm::solver::SmtSolver::ModelReference> model = s.getModel();
int_fast64_t aEval = model->getIntegerValue("a");
int_fast64_t bEval = model->getIntegerValue("b");
int_fast64_t cEval = model->getIntegerValue("c");
ASSERT_TRUE(cEval == aEval + bEval - 1);
}
TEST(MathsatSmtSolver, AllSat) {
@ -174,9 +173,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.add(exprFormula1));
(s.add(exprFormula2));
(s.add(exprFormula3));
s.add(exprFormula1);
s.add(exprFormula2);
s.add(exprFormula3);
std::vector<storm::expressions::SimpleValuation> valuations = s.allSat({x,y});
@ -196,7 +195,7 @@ TEST(MathsatSmtSolver, AllSat) {
}
TEST(MathsatSmtSolver, UnsatAssumptions) {
storm::solver::MathsatSmtSolver s;
storm::solver::MathsatSmtSolver s(storm::solver::MathsatSmtSolver::Options(false, true, false));
storm::solver::SmtSolver::CheckResult result = storm::solver::SmtSolver::CheckResult::Unknown;
storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
@ -210,9 +209,9 @@ 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.add(exprFormula));
(s.add(exprFormula2));
(result = s.checkWithAssumptions({ f2 }));
s.add(exprFormula);
s.add(exprFormula2);
result = s.checkWithAssumptions({ f2 });
ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
std::vector<storm::expressions::Expression> unsatCore = s.getUnsatAssumptions();
ASSERT_EQ(unsatCore.size(), 1);
@ -237,7 +236,7 @@ TEST(MathsatSmtSolver, InterpolationTest) {
s.add(exprFormula2);
s.setInterpolationGroup(2);
s.add(exprFormula3);
ASSERT_NO_THROW(result = s.check());
ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
@ -245,11 +244,11 @@ TEST(MathsatSmtSolver, InterpolationTest) {
ASSERT_NO_THROW(interpol = s.getInterpolant({0, 1}));
storm::solver::MathsatSmtSolver s2;
ASSERT_NO_THROW(s2.add(!(exprFormula && exprFormula2).implies(interpol)));
ASSERT_NO_THROW(result = s2.check());
ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
ASSERT_NO_THROW(s2.reset());
ASSERT_NO_THROW(s2.add(interpol && exprFormula3));
ASSERT_NO_THROW(result = s2.check());

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

@ -8,23 +8,23 @@
TEST(Z3SmtSolver, CheckSat) {
storm::solver::Z3SmtSolver 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.add(exprDeMorgan));
ASSERT_NO_THROW(result = s.check());
ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
ASSERT_NO_THROW(s.reset());
storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b");
storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c");
storm::expressions::Expression exprFormula = a >= storm::expressions::Expression::createIntegerLiteral(0)
&& a < storm::expressions::Expression::createIntegerLiteral(5)
&& b > storm::expressions::Expression::createIntegerLiteral(7)
&& c == (a * b)
&& b + a > c;
&& a < storm::expressions::Expression::createIntegerLiteral(5)
&& b > storm::expressions::Expression::createIntegerLiteral(7)
&& c == (a * b)
&& b + a > c;
ASSERT_NO_THROW(s.add(exprFormula));
ASSERT_NO_THROW(result = s.check());
ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
@ -34,24 +34,24 @@ TEST(Z3SmtSolver, CheckSat) {
TEST(Z3SmtSolver, CheckUnsat) {
storm::solver::Z3SmtSolver 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.add(!exprDeMorgan));
ASSERT_NO_THROW(result = s.check());
ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
ASSERT_NO_THROW(s.reset());
storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b");
storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c");
storm::expressions::Expression exprFormula = a >= storm::expressions::Expression::createIntegerLiteral(2)
&& a < storm::expressions::Expression::createIntegerLiteral(5)
&& b > storm::expressions::Expression::createIntegerLiteral(7)
&& c == (a * b)
&& b + a > c;
&& a < storm::expressions::Expression::createIntegerLiteral(5)
&& b > storm::expressions::Expression::createIntegerLiteral(7)
&& c == (a * b)
&& b + a > c;
ASSERT_NO_THROW(s.add(exprFormula));
ASSERT_NO_THROW(result = s.check());
ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat);
@ -61,11 +61,11 @@ TEST(Z3SmtSolver, CheckUnsat) {
TEST(Z3SmtSolver, Backtracking) {
storm::solver::Z3SmtSolver 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.add(expr1));
ASSERT_NO_THROW(result = s.check());
ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
@ -88,18 +88,18 @@ TEST(Z3SmtSolver, Backtracking) {
ASSERT_NO_THROW(result = s.check());
ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
ASSERT_NO_THROW(s.reset());
storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b");
storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c");
storm::expressions::Expression exprFormula = a >= storm::expressions::Expression::createIntegerLiteral(0)
&& a < storm::expressions::Expression::createIntegerLiteral(5)
&& b > storm::expressions::Expression::createIntegerLiteral(7)
&& c == (a * b)
&& b + a > c;
&& a < storm::expressions::Expression::createIntegerLiteral(5)
&& b > storm::expressions::Expression::createIntegerLiteral(7)
&& c == (a * b)
&& b + a > c;
storm::expressions::Expression exprFormula2 = a >= storm::expressions::Expression::createIntegerLiteral(2);
ASSERT_NO_THROW(s.add(exprFormula));
ASSERT_NO_THROW(result = s.check());
ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
@ -115,18 +115,18 @@ TEST(Z3SmtSolver, Backtracking) {
TEST(Z3SmtSolver, Assumptions) {
storm::solver::Z3SmtSolver 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");
storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c");
storm::expressions::Expression exprFormula = a >= storm::expressions::Expression::createIntegerLiteral(0)
&& a < storm::expressions::Expression::createIntegerLiteral(5)
&& b > storm::expressions::Expression::createIntegerLiteral(7)
&& c == (a * b)
&& b + a > c;
&& a < storm::expressions::Expression::createIntegerLiteral(5)
&& b > storm::expressions::Expression::createIntegerLiteral(7)
&& c == (a * b)
&& b + a > c;
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.add(exprFormula));
ASSERT_NO_THROW(result = s.check());
ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
@ -144,31 +144,29 @@ TEST(Z3SmtSolver, Assumptions) {
TEST(Z3SmtSolver, GenerateModel) {
storm::solver::Z3SmtSolver s;
storm::solver::SmtSolver::CheckResult result;
storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b");
storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c");
storm::expressions::Expression exprFormula = a > storm::expressions::Expression::createIntegerLiteral(0)
&& a < storm::expressions::Expression::createIntegerLiteral(5)
&& b > storm::expressions::Expression::createIntegerLiteral(7)
&& c == (a * b)
&& b + a > c;
(s.add(exprFormula));
(result = s.check());
&& a < storm::expressions::Expression::createIntegerLiteral(5)
&& b > storm::expressions::Expression::createIntegerLiteral(7)
&& c == (a * b)
&& b + a > c;
s.add(exprFormula);
result = s.check();
ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Sat);
storm::expressions::SimpleValuation model;
(model = s.getModel());
int_fast64_t a_eval;
(a_eval = model.getIntegerValue("a"));
ASSERT_EQ(1, a_eval);
std::shared_ptr<storm::solver::SmtSolver::ModelReference> model = s.getModel();
int_fast64_t aEval = model->getIntegerValue("a");
ASSERT_EQ(1, aEval);
}
TEST(Z3SmtSolver, AllSat) {
storm::solver::Z3SmtSolver s;
storm::solver::SmtSolver::CheckResult result;
storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b");
storm::expressions::Expression x = storm::expressions::Expression::createBooleanVariable("x");
@ -177,13 +175,13 @@ TEST(Z3SmtSolver, AllSat) {
storm::expressions::Expression exprFormula1 = x.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));
(s.add(exprFormula1));
(s.add(exprFormula2));
(s.add(exprFormula3));
s.add(exprFormula1);
s.add(exprFormula2);
s.add(exprFormula3);
std::vector<storm::expressions::SimpleValuation> valuations = s.allSat({x,y});
ASSERT_TRUE(valuations.size() == 3);
for (int i = 0; i < valuations.size(); ++i) {
ASSERT_EQ(valuations[i].getNumberOfIdentifiers(), 2);
@ -192,7 +190,7 @@ TEST(Z3SmtSolver, AllSat) {
}
for (int i = 0; i < valuations.size(); ++i) {
ASSERT_FALSE(valuations[i].getBooleanValue("x") && valuations[i].getBooleanValue("y"));
for (int j = i+1; j < valuations.size(); ++j) {
ASSERT_TRUE((valuations[i].getBooleanValue("x") != valuations[j].getBooleanValue("x")) || (valuations[i].getBooleanValue("y") != valuations[j].getBooleanValue("y")));
}
@ -202,15 +200,15 @@ TEST(Z3SmtSolver, AllSat) {
TEST(Z3SmtSolver, UnsatAssumptions) {
storm::solver::Z3SmtSolver s;
storm::solver::SmtSolver::CheckResult result;
storm::expressions::Expression a = storm::expressions::Expression::createIntegerVariable("a");
storm::expressions::Expression b = storm::expressions::Expression::createIntegerVariable("b");
storm::expressions::Expression c = storm::expressions::Expression::createIntegerVariable("c");
storm::expressions::Expression exprFormula = a >= storm::expressions::Expression::createIntegerLiteral(0)
&& a < storm::expressions::Expression::createIntegerLiteral(5)
&& b > storm::expressions::Expression::createIntegerLiteral(7)
&& c == (a * b)
&& b + a > c;
&& a < storm::expressions::Expression::createIntegerLiteral(5)
&& b > storm::expressions::Expression::createIntegerLiteral(7)
&& c == (a * b)
&& b + a > c;
storm::expressions::Expression f2 = storm::expressions::Expression::createBooleanVariable("f2");
storm::expressions::Expression exprFormula2 = f2.implies(a >= storm::expressions::Expression::createIntegerLiteral(2));

Write Preview
Loading…
Cancel
Save