11 storm::adapters::Z3ExpressionAdapter& expressionAdapter)
12 : ModelReference(
manager), model(model), expressionAdapter(expressionAdapter) {
20 z3::expr z3Expr = this->expressionAdapter.translateExpression(variable);
21 z3::expr z3ExprValuation = model.eval(z3Expr,
true);
22 return this->expressionAdapter.translateExpression(z3ExprValuation).isTrue();
24 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Storm is compiled without Z3 support.");
31 z3::expr z3Expr = this->expressionAdapter.translateExpression(variable);
32 z3::expr z3ExprValuation = model.eval(z3Expr,
true);
33 return this->expressionAdapter.translateExpression(z3ExprValuation).evaluateAsInt();
35 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Storm is compiled without Z3 support.");
42 z3::expr z3Expr = this->expressionAdapter.translateExpression(variable);
43 z3::expr z3ExprValuation = model.eval(z3Expr,
true);
44 return this->expressionAdapter.translateExpression(z3ExprValuation).evaluateAsDouble();
46 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Storm is compiled without Z3 support.");
50std::string Z3SmtSolver::Z3ModelReference::toString()
const {
52 std::stringstream sstr;
56 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Storm is compiled without Z3 support.");
50std::string Z3SmtSolver::Z3ModelReference::toString()
const {
…}
66 expressionAdapter(nullptr),
67 lastCheckAssumptions(false),
73 config.set(
"model",
true);
74 context = std::unique_ptr<z3::context>(
new z3::context(config));
75 solver = std::unique_ptr<z3::solver>(
new z3::solver(*context));
76 expressionAdapter = std::unique_ptr<storm::adapters::Z3ExpressionAdapter>(
new storm::adapters::Z3ExpressionAdapter(this->
getManager(), *context));
88 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Storm is compiled without Z3 support.");
96 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Storm is compiled without Z3 support.");
102 this->solver->pop(
static_cast<unsigned int>(n));
104 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Storm is compiled without Z3 support.");
110 this->solver->reset();
112 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Storm is compiled without Z3 support.");
118 this->solver->add(expressionAdapter->translateExpression(assertion));
120 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Storm is compiled without Z3 support.");
126 lastCheckAssumptions =
false;
127 switch (this->solver->check()) {
138 return this->lastResult;
140 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Storm is compiled without Z3 support.");
146 lastCheckAssumptions =
true;
147 z3::expr_vector z3Assumptions(*this->context);
150 z3Assumptions.push_back(this->expressionAdapter->translateExpression(assumption));
153 switch (this->solver->check(z3Assumptions)) {
164 return this->lastResult;
166 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Storm is compiled without Z3 support.");
173 lastCheckAssumptions =
true;
174 z3::expr_vector z3Assumptions(*this->context);
177 z3Assumptions.push_back(this->expressionAdapter->translateExpression(assumption));
180 switch (this->solver->check(z3Assumptions)) {
191 return this->lastResult;
193 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Storm is compiled without Z3 support.");
200 "Unable to create model for formula that was not determined to be satisfiable.");
201 return this->convertZ3ModelToValuation(this->solver->get_model());
203 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Storm is compiled without Z3 support.");
210 "Unable to create model for formula that was not determined to be satisfiable.");
211 return std::shared_ptr<SmtSolver::ModelReference>(
new Z3ModelReference(this->
getManager(), this->solver->get_model(), *this->expressionAdapter));
213 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Storm is compiled without Z3 support.");
221 for (
unsigned i = 0; i < model.num_consts(); ++i) {
222 z3::func_decl variableI = model.get_const_decl(i);
227 stormModel.setBooleanValue(this->
getManager().getVariable(variableI.name().str()), variableInterpretation.
isTrue());
229 stormModel.setIntegerValue(this->
getManager().getVariable(variableI.name().str()), variableInterpretation.
evaluateAsInt());
231 stormModel.setRationalValue(this->
getManager().getVariable(variableI.name().str()), variableInterpretation.
evaluateAsDouble());
233 STORM_LOG_ASSERT(
false,
"Variable interpretation in model is not of type bool, int or rational.");
241std::vector<storm::expressions::SimpleValuation>
Z3SmtSolver::allSat(std::vector<storm::expressions::Variable>
const& important) {
243 std::vector<storm::expressions::SimpleValuation> valuations;
246 valuations.push_back(valuation);
251 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Storm is compiled without Z3 support.");
241std::vector<storm::expressions::SimpleValuation>
Z3SmtSolver::allSat(std::vector<storm::expressions::Variable>
const& important) {
…}
259 STORM_LOG_THROW(variable.hasBooleanType(), storm::exceptions::InvalidArgumentException,
"The important atoms for AllSat must be boolean variables.");
262 uint_fast64_t numberOfModels = 0;
271 z3::model model = this->solver->get_model();
273 z3::expr modelExpr = this->context->bool_val(
true);
277 z3::expr z3ImportantAtom = this->expressionAdapter->translateExpression(importantAtom.getExpression());
278 z3::expr z3ImportantAtomValuation = model.eval(z3ImportantAtom,
true);
279 modelExpr = modelExpr && (z3ImportantAtom == z3ImportantAtomValuation);
280 valuation.
setBooleanValue(importantAtom, this->expressionAdapter->translateExpression(z3ImportantAtomValuation).isTrue());
284 proceed = callback(valuation);
286 this->solver->add(!modelExpr);
292 return numberOfModels;
294 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Storm is compiled without Z3 support.");
301 STORM_LOG_THROW(variable.hasBooleanType(), storm::exceptions::InvalidArgumentException,
"The important atoms for AllSat must be boolean variables.");
304 uint_fast64_t numberOfModels = 0;
313 z3::model model = this->solver->get_model();
315 z3::expr modelExpr = this->context->bool_val(
true);
319 z3::expr z3ImportantAtom = this->expressionAdapter->translateExpression(importantAtom.getExpression());
320 z3::expr z3ImportantAtomValuation = model.eval(z3ImportantAtom,
true);
321 modelExpr = modelExpr && (z3ImportantAtom == z3ImportantAtomValuation);
323 Z3ModelReference modelRef(this->
getManager(), model, *expressionAdapter);
326 proceed = callback(modelRef);
328 this->solver->add(!modelExpr);
333 return numberOfModels;
335 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Storm is compiled without Z3 support.");
342 "Unable to generate unsatisfiable core of assumptions, because the last check did not determine the formulas to be unsatisfiable.");
343 STORM_LOG_THROW(lastCheckAssumptions, storm::exceptions::InvalidStateException,
344 "Unable to generate unsatisfiable core of assumptions, because the last check did not involve assumptions.");
346 z3::expr_vector z3UnsatAssumptions = this->solver->unsat_core();
347 std::vector<storm::expressions::Expression> unsatAssumptions;
349 for (
unsigned int i = 0; i < z3UnsatAssumptions.size(); ++i) {
350 unsatAssumptions.push_back(this->expressionAdapter->translateExpression(z3UnsatAssumptions[i]));
353 return unsatAssumptions;
355 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Storm is compiled without Z3 support.");
361 z3::params paramObject(*context);
362 paramObject.set(
":timeout",
static_cast<unsigned>(milliseconds));
363 solver->set(paramObject);
366 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Storm is compiled without Z3 support.");
372 z3::params paramObject(*context);
373 paramObject.set(
":timeout", 0u);
374 solver->set(paramObject);
377 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Storm is compiled without Z3 support.");
383 return solver->to_smt2();
385 STORM_LOG_THROW(
false, storm::exceptions::NotSupportedException,
"Storm is compiled without Z3 support.");
int_fast64_t evaluateAsInt(Valuation const *valuation=nullptr) const
Evaluates the expression under the valuation of variables given by the valuation and returns the resu...
double evaluateAsDouble(Valuation const *valuation=nullptr) const
Evaluates the expression under the valuation of variables given by the valuation and returns the resu...
Type const & getType() const
Retrieves the type of the expression.
bool isTrue() const
Checks if the expression is equal to the boolean literal true.
This class is responsible for managing a set of typed variables and all expressions using these varia...
A simple implementation of the valuation interface.
virtual void setBooleanValue(Variable const &booleanVariable, bool value) override
Sets the value of the given boolean variable to the provided value.
bool isBooleanType() const
Checks whether this type is a boolean type.
bool isIntegerType() const
Checks whether this type is an integral type.
bool isRationalType() const
Checks whether this type is a rational type.
ExpressionManager const & getManager() const
Retrieves the manager responsible for this variable.
The base class for all model references.
An interface that captures the functionality of an SMT solver.
storm::expressions::ExpressionManager const & getManager() const
Retrieves the expression manager associated with the solver.
CheckResult
possible check results
virtual void add(storm::expressions::Expression const &assertion) override
Adds an assertion to the solver's stack.
virtual bool unsetTimeout() override
If supported by the solver, this unsets a previous timeout.
virtual std::shared_ptr< SmtSolver::ModelReference > getModel() override
If the last call to check() or checkWithAssumptions() returned Sat, this method retrieves a model tha...
virtual storm::expressions::SimpleValuation getModelAsValuation() override
If the last call to check() or checkWithAssumptions() returned Sat, this method retrieves a model tha...
virtual CheckResult checkWithAssumptions(std::set< storm::expressions::Expression > const &assumptions) override
Checks whether the conjunction of assertions that are currently on the solver's stack together with t...
virtual std::string getSmtLibString() const override
If supported by the solver, this function returns the current assertions in the SMT-LIB format.
virtual std::vector< storm::expressions::SimpleValuation > allSat(std::vector< storm::expressions::Variable > const &important) override
Performs AllSat over the (provided) important atoms.
virtual void reset() override
Removes all assertions from the solver's stack.
virtual void push() override
Pushes a backtracking point on the solver's stack.
virtual std::vector< storm::expressions::Expression > getUnsatAssumptions() override
If the last call to checkWithAssumptions() returned Unsat, this function can be used to retrieve a su...
virtual bool setTimeout(uint_fast64_t milliseconds) override
If supported by the solver, this will limit all subsequent satisfiability queries to the given number...
virtual void pop() override
Pops a backtracking point from the solver's stack.
virtual CheckResult check() override
Checks whether the conjunction of assertions that are currently on the solver's stack is satisfiable.
#define STORM_LOG_ASSERT(cond, message)
#define STORM_LOG_THROW(cond, exception, message)
SettingsManager const & manager()
Retrieves the settings manager.