You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
338 lines
14 KiB
338 lines
14 KiB
#include "src/solver/Z3Smtsolver.h"
|
|
|
|
#include "src/exceptions/NotSupportedException.h"
|
|
#include "src/exceptions/InvalidStateException.h"
|
|
|
|
namespace storm {
|
|
namespace solver {
|
|
#ifdef STORM_HAVE_Z3
|
|
Z3SmtSolver::Z3ModelReference::Z3ModelReference(storm::expressions::ExpressionManager const& manager, z3::model model, storm::adapters::Z3ExpressionAdapter& expressionAdapter) : ModelReference(manager), model(model), expressionAdapter(expressionAdapter) {
|
|
// Intentionally left empty.
|
|
}
|
|
#endif
|
|
|
|
bool Z3SmtSolver::Z3ModelReference::getBooleanValue(storm::expressions::Variable const& variable) const {
|
|
#ifdef STORM_HAVE_Z3
|
|
STORM_LOG_ASSERT(variable.getManager() == this->getManager(), "Requested variable is managed by a different manager.");
|
|
z3::expr z3Expr = this->expressionAdapter.translateExpression(variable);
|
|
z3::expr z3ExprValuation = model.eval(z3Expr, true);
|
|
return this->expressionAdapter.translateExpression(z3ExprValuation).isTrue();
|
|
#else
|
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
|
|
#endif
|
|
}
|
|
|
|
int_fast64_t Z3SmtSolver::Z3ModelReference::getIntegerValue(storm::expressions::Variable const& variable) const {
|
|
#ifdef STORM_HAVE_Z3
|
|
STORM_LOG_ASSERT(variable.getManager() == this->getManager(), "Requested variable is managed by a different manager.");
|
|
z3::expr z3Expr = this->expressionAdapter.translateExpression(variable);
|
|
z3::expr z3ExprValuation = model.eval(z3Expr, true);
|
|
return this->expressionAdapter.translateExpression(z3ExprValuation).evaluateAsInt();
|
|
#else
|
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
|
|
#endif
|
|
}
|
|
|
|
double Z3SmtSolver::Z3ModelReference::getRationalValue(storm::expressions::Variable const& variable) const {
|
|
#ifdef STORM_HAVE_Z3
|
|
STORM_LOG_ASSERT(variable.getManager() == this->getManager(), "Requested variable is managed by a different manager.");
|
|
z3::expr z3Expr = this->expressionAdapter.translateExpression(variable);
|
|
z3::expr z3ExprValuation = model.eval(z3Expr, true);
|
|
return this->expressionAdapter.translateExpression(z3ExprValuation).evaluateAsDouble();
|
|
#else
|
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
|
|
#endif
|
|
}
|
|
|
|
Z3SmtSolver::Z3SmtSolver(storm::expressions::ExpressionManager& manager)
|
|
#ifdef STORM_HAVE_Z3
|
|
: SmtSolver(manager), context(nullptr), solver(nullptr), expressionAdapter(nullptr), lastCheckAssumptions(false), lastResult(CheckResult::Unknown)
|
|
#endif
|
|
{
|
|
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(this->getManager(), *context));
|
|
}
|
|
|
|
Z3SmtSolver::~Z3SmtSolver() {
|
|
// Intentionally left empty.
|
|
}
|
|
|
|
void Z3SmtSolver::push()
|
|
{
|
|
#ifdef STORM_HAVE_Z3
|
|
this->solver->push();
|
|
#else
|
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
|
|
#endif
|
|
}
|
|
|
|
void Z3SmtSolver::pop()
|
|
{
|
|
#ifdef STORM_HAVE_Z3
|
|
this->solver->pop();
|
|
#else
|
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
|
|
#endif
|
|
}
|
|
|
|
void Z3SmtSolver::pop(uint_fast64_t n)
|
|
{
|
|
#ifdef STORM_HAVE_Z3
|
|
this->solver->pop(static_cast<unsigned int>(n));
|
|
#else
|
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
|
|
#endif
|
|
}
|
|
|
|
void Z3SmtSolver::reset()
|
|
{
|
|
#ifdef STORM_HAVE_Z3
|
|
this->solver->reset();
|
|
#else
|
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
|
|
#endif
|
|
}
|
|
|
|
void Z3SmtSolver::add(storm::expressions::Expression const& assertion)
|
|
{
|
|
#ifdef STORM_HAVE_Z3
|
|
this->solver->add(expressionAdapter->translateExpression(assertion));
|
|
#else
|
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
|
|
#endif
|
|
}
|
|
|
|
SmtSolver::CheckResult Z3SmtSolver::check()
|
|
{
|
|
#ifdef STORM_HAVE_Z3
|
|
lastCheckAssumptions = false;
|
|
switch (this->solver->check()) {
|
|
case z3::sat:
|
|
this->lastResult = SmtSolver::CheckResult::Sat;
|
|
break;
|
|
case z3::unsat:
|
|
this->lastResult = SmtSolver::CheckResult::Unsat;
|
|
break;
|
|
default:
|
|
this->lastResult = SmtSolver::CheckResult::Unknown;
|
|
break;
|
|
}
|
|
return this->lastResult;
|
|
#else
|
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
|
|
#endif
|
|
}
|
|
|
|
SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions)
|
|
{
|
|
#ifdef STORM_HAVE_Z3
|
|
lastCheckAssumptions = true;
|
|
z3::expr_vector z3Assumptions(*this->context);
|
|
|
|
for (storm::expressions::Expression assumption : assumptions) {
|
|
z3Assumptions.push_back(this->expressionAdapter->translateExpression(assumption));
|
|
}
|
|
|
|
switch (this->solver->check(z3Assumptions)) {
|
|
case z3::sat:
|
|
this->lastResult = SmtSolver::CheckResult::Sat;
|
|
break;
|
|
case z3::unsat:
|
|
this->lastResult = SmtSolver::CheckResult::Unsat;
|
|
break;
|
|
default:
|
|
this->lastResult = SmtSolver::CheckResult::Unknown;
|
|
break;
|
|
}
|
|
return this->lastResult;
|
|
#else
|
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
|
|
#endif
|
|
}
|
|
|
|
SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions)
|
|
{
|
|
#ifdef STORM_HAVE_Z3
|
|
lastCheckAssumptions = true;
|
|
z3::expr_vector z3Assumptions(*this->context);
|
|
|
|
for (storm::expressions::Expression assumption : assumptions) {
|
|
z3Assumptions.push_back(this->expressionAdapter->translateExpression(assumption));
|
|
}
|
|
|
|
switch (this->solver->check(z3Assumptions)) {
|
|
case z3::sat:
|
|
this->lastResult = SmtSolver::CheckResult::Sat;
|
|
break;
|
|
case z3::unsat:
|
|
this->lastResult = SmtSolver::CheckResult::Unsat;
|
|
break;
|
|
default:
|
|
this->lastResult = SmtSolver::CheckResult::Unknown;
|
|
break;
|
|
}
|
|
return this->lastResult;
|
|
#else
|
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
|
|
#endif
|
|
}
|
|
|
|
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());
|
|
#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->getManager(), 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) {
|
|
storm::expressions::SimpleValuation stormModel(this->getManager());
|
|
|
|
for (unsigned i = 0; i < model.num_consts(); ++i) {
|
|
z3::func_decl variableI = model.get_const_decl(i);
|
|
storm::expressions::Variable stormVariable = this->expressionAdapter->getVariable(variableI);
|
|
storm::expressions::Expression variableInterpretation = this->expressionAdapter->translateExpression(model.get_const_interp(variableI));
|
|
|
|
if (variableInterpretation.getType().isBooleanType()) {
|
|
stormModel.setBooleanValue(this->getManager().getVariable(variableI.name().str()), variableInterpretation.isTrue());
|
|
} else if (variableInterpretation.getType().isIntegralType()) {
|
|
stormModel.setIntegerValue(this->getManager().getVariable(variableI.name().str()), variableInterpretation.evaluateAsInt());
|
|
} else if (variableInterpretation.getType().isRationalType()) {
|
|
stormModel.setRationalValue(this->getManager().getVariable(variableI.name().str()), variableInterpretation.evaluateAsDouble());
|
|
} else {
|
|
STORM_LOG_ASSERT(false, "Variable interpretation in model is not of type bool, int or rational.");
|
|
}
|
|
}
|
|
|
|
return stormModel;
|
|
}
|
|
#endif
|
|
|
|
std::vector<storm::expressions::SimpleValuation> Z3SmtSolver::allSat(std::vector<storm::expressions::Variable> const& important)
|
|
{
|
|
#ifdef STORM_HAVE_Z3
|
|
std::vector<storm::expressions::SimpleValuation> valuations;
|
|
this->allSat(important, [&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; });
|
|
return valuations;
|
|
#else
|
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
|
|
#endif
|
|
}
|
|
|
|
uint_fast64_t Z3SmtSolver::allSat(std::vector<storm::expressions::Variable> const& important, std::function<bool(storm::expressions::SimpleValuation&)> const& callback) {
|
|
#ifdef STORM_HAVE_Z3
|
|
for (storm::expressions::Variable const& variable : important) {
|
|
STORM_LOG_THROW(variable.hasBooleanType(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be boolean variables.");
|
|
}
|
|
|
|
uint_fast64_t numberOfModels = 0;
|
|
bool proceed = true;
|
|
|
|
// Save the current assertion stack, to be able to backtrack after the procedure.
|
|
this->push();
|
|
|
|
// 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::expr modelExpr = this->context->bool_val(true);
|
|
storm::expressions::SimpleValuation valuation(this->getManager());
|
|
|
|
for (storm::expressions::Variable const& importantAtom : important) {
|
|
z3::expr z3ImportantAtom = this->expressionAdapter->translateExpression(importantAtom.getExpression());
|
|
z3::expr z3ImportantAtomValuation = model.eval(z3ImportantAtom, true);
|
|
modelExpr = modelExpr && (z3ImportantAtom == z3ImportantAtomValuation);
|
|
valuation.setBooleanValue(importantAtom, this->expressionAdapter->translateExpression(z3ImportantAtomValuation).isTrue());
|
|
}
|
|
|
|
// Check if we are required to proceed, and if so rule out the current model.
|
|
proceed = callback(valuation);
|
|
if (proceed) {
|
|
this->solver->add(!modelExpr);
|
|
}
|
|
}
|
|
|
|
// Restore the old assertion stack and return.
|
|
this->pop();
|
|
return numberOfModels;
|
|
#else
|
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
|
|
#endif
|
|
}
|
|
|
|
uint_fast64_t Z3SmtSolver::allSat(std::vector<storm::expressions::Variable> const& important, std::function<bool(SmtSolver::ModelReference&)> const& callback) {
|
|
#ifdef STORM_HAVE_Z3
|
|
for (storm::expressions::Variable const& variable : important) {
|
|
STORM_LOG_THROW(variable.hasBooleanType(), storm::exceptions::InvalidArgumentException, "The important atoms for AllSat must be boolean variables.");
|
|
}
|
|
|
|
uint_fast64_t numberOfModels = 0;
|
|
bool proceed = true;
|
|
|
|
// Save the current assertion stack, to be able to backtrack after the procedure.
|
|
this->push();
|
|
|
|
// 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::expr modelExpr = this->context->bool_val(true);
|
|
storm::expressions::SimpleValuation valuation(this->getManager());
|
|
|
|
for (storm::expressions::Variable const& importantAtom : important) {
|
|
z3::expr z3ImportantAtom = this->expressionAdapter->translateExpression(importantAtom.getExpression());
|
|
z3::expr z3ImportantAtomValuation = model.eval(z3ImportantAtom, true);
|
|
modelExpr = modelExpr && (z3ImportantAtom == z3ImportantAtomValuation);
|
|
}
|
|
Z3ModelReference modelRef(this->getManager(), 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->pop();
|
|
return numberOfModels;
|
|
#else
|
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
|
|
#endif
|
|
}
|
|
|
|
std::vector<storm::expressions::Expression> Z3SmtSolver::getUnsatAssumptions() {
|
|
#ifdef STORM_HAVE_Z3
|
|
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();
|
|
std::vector<storm::expressions::Expression> unsatAssumptions;
|
|
|
|
for (unsigned int i = 0; i < z3UnsatAssumptions.size(); ++i) {
|
|
unsatAssumptions.push_back(this->expressionAdapter->translateExpression(z3UnsatAssumptions[i]));
|
|
}
|
|
|
|
return unsatAssumptions;
|
|
#else
|
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
|
|
#endif
|
|
}
|
|
}
|
|
}
|