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

Adapted Z3ExpressionAdapter for new expressions 

SmtSolver now not copyable


Former-commit-id: e0d17fd21c
tempestpy_adaptions
David_Korzeniewski 11 years ago
parent
4cb346f8ce
commit
98f87a5e6d
2 changed files with 120 additions and 80 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. 195
      src/adapters/Z3ExpressionAdapter.h
  2. 5
      src/solver/SmtSolver.h

195
src/adapters/Z3ExpressionAdapter.h
View File

@ -10,13 +10,17 @@
#include <stack>
#include "src/ir/expressions/ExpressionVisitor.h"
#include "src/ir/expressions/Expressions.h"
#include "z3++.h"
#include "z3.h"
#include "src/storage/expressions/Expressions.h"
#include "src/exceptions/ExpressionEvaluationException.h"
#include "src/exceptions/NotImplementedException.h"
namespace storm {
namespace adapters {
class Z3ExpressionAdapter : public storm::ir::expressions::ExpressionVisitor {
class Z3ExpressionAdapter : public storm::expressions::ExpressionVisitor {
public:
/*!
* Creates a Z3ExpressionAdapter over the given Z3 context.
@ -25,7 +29,12 @@ namespace storm {
* the lifetime of the context as long as the instance of this adapter is used.
* @param variableToExpressionMap A mapping from variable names to their corresponding Z3 expressions.
*/
Z3ExpressionAdapter(z3::context& context, std::map<std::string, z3::expr> const& variableToExpressionMap) : context(context), stack(), variableToExpressionMap(variableToExpressionMap) {
Z3ExpressionAdapter(z3::context& context, std::map<std::string, z3::expr> const& variableToExpressionMap)
: context(context)
, stack()
, variableToExpressionMap(variableToExpressionMap)
, additionalVariableCounter(0)
, additionalAssertions() {
// Intentionally left empty.
}
@ -35,71 +44,86 @@ namespace storm {
* @param expression The expression to translate.
* @return An equivalent expression for Z3.
*/
z3::expr translateExpression(std::unique_ptr<storm::ir::expressions::BaseExpression> const& expression) {
expression->accept(this);
z3::expr translateExpression(storm::expressions::Expression const& expression) {
expression.getBaseExpression().accept(this);
z3::expr result = stack.top();
stack.pop();
while (!additionalAssertions.empty()) {
result = result && additionalAssertions.top();
additionalAssertions.pop();
}
return result;
}
virtual void visit(ir::expressions::BinaryBooleanFunctionExpression* expression) {
expression->getLeft()->accept(this);
expression->getRight()->accept(this);
virtual void visit(storm::expressions::BinaryBooleanFunctionExpression const* expression) override {
expression->getFirstOperand()->accept(this);
expression->getSecondOperand()->accept(this);
z3::expr rightResult = stack.top();
const z3::expr rightResult = stack.top();
stack.pop();
z3::expr leftResult = stack.top();
const z3::expr leftResult = stack.top();
stack.pop();
switch(expression->getFunctionType()) {
case storm::ir::expressions::BinaryBooleanFunctionExpression::AND:
switch(expression->getOperatorType()) {
case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And:
stack.push(leftResult && rightResult);
break;
case storm::ir::expressions::BinaryBooleanFunctionExpression::OR:
case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Or:
stack.push(leftResult || rightResult);
break;
break;
case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Xor:
stack.push(z3::expr(context, Z3_mk_xor(context, leftResult, rightResult)));
break;
case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Implies:
stack.push(z3::expr(context, Z3_mk_implies(context, leftResult, rightResult)));
break;
case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff:
stack.push(z3::expr(context, Z3_mk_iff(context, leftResult, rightResult)));
break;
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
<< "Unknown boolean binary operator: '" << expression->getFunctionType() << "' in expression " << expression->toString() << ".";
<< "Unknown boolean binary operator: '" << expression->getOperatorType() << "' in expression " << expression << ".";
}
}
virtual void visit(ir::expressions::BinaryNumericalFunctionExpression* expression) {
expression->getLeft()->accept(this);
expression->getRight()->accept(this);
virtual void visit(storm::expressions::BinaryNumericalFunctionExpression const* expression) override {
expression->getFirstOperand()->accept(this);
expression->getSecondOperand()->accept(this);
z3::expr rightResult = stack.top();
stack.pop();
z3::expr leftResult = stack.top();
stack.pop();
switch(expression->getFunctionType()) {
case storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS:
switch(expression->getOperatorType()) {
case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Plus:
stack.push(leftResult + rightResult);
break;
case storm::ir::expressions::BinaryNumericalFunctionExpression::MINUS:
case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Minus:
stack.push(leftResult - rightResult);
break;
case storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES:
case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Times:
stack.push(leftResult * rightResult);
break;
case storm::ir::expressions::BinaryNumericalFunctionExpression::DIVIDE:
case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Divide:
stack.push(leftResult / rightResult);
break;
case storm::ir::expressions::BinaryNumericalFunctionExpression::MIN:
case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Min:
stack.push(ite(leftResult <= rightResult, leftResult, rightResult));
break;
case storm::ir::expressions::BinaryNumericalFunctionExpression::MAX:
case storm::expressions::BinaryNumericalFunctionExpression::OperatorType::Max:
stack.push(ite(leftResult >= rightResult, leftResult, rightResult));
break;
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
<< "Unknown numerical binary operator: '" << expression->getFunctionType() << "' in expression " << expression->toString() << ".";
<< "Unknown numerical binary operator: '" << expression->getOperatorType() << "' in expression " << expression << ".";
}
}
virtual void visit(ir::expressions::BinaryRelationExpression* expression) {
expression->getLeft()->accept(this);
expression->getRight()->accept(this);
virtual void visit(storm::expressions::BinaryRelationExpression const* expression) override {
expression->getFirstOperand()->accept(this);
expression->getSecondOperand()->accept(this);
z3::expr rightResult = stack.top();
stack.pop();
@ -107,109 +131,122 @@ namespace storm {
stack.pop();
switch(expression->getRelationType()) {
case storm::ir::expressions::BinaryRelationExpression::EQUAL:
case storm::expressions::BinaryRelationExpression::RelationType::Equal:
stack.push(leftResult == rightResult);
break;
case storm::ir::expressions::BinaryRelationExpression::NOT_EQUAL:
case storm::expressions::BinaryRelationExpression::RelationType::NotEqual:
stack.push(leftResult != rightResult);
break;
case storm::ir::expressions::BinaryRelationExpression::LESS:
case storm::expressions::BinaryRelationExpression::RelationType::Less:
stack.push(leftResult < rightResult);
break;
case storm::ir::expressions::BinaryRelationExpression::LESS_OR_EQUAL:
case storm::expressions::BinaryRelationExpression::RelationType::LessOrEqual:
stack.push(leftResult <= rightResult);
break;
case storm::ir::expressions::BinaryRelationExpression::GREATER:
case storm::expressions::BinaryRelationExpression::RelationType::Greater:
stack.push(leftResult > rightResult);
break;
case storm::ir::expressions::BinaryRelationExpression::GREATER_OR_EQUAL:
case storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual:
stack.push(leftResult >= rightResult);
break;
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
<< "Unknown boolean binary operator: '" << expression->getRelationType() << "' in expression " << expression->toString() << ".";
<< "Unknown boolean binary operator: '" << expression->getRelationType() << "' in expression " << expression << ".";
}
}
virtual void visit(ir::expressions::BooleanConstantExpression* expression) {
if (!expression->isDefined()) {
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
<< ". Boolean constant '" << expression->getConstantName() << "' is undefined.";
}
stack.push(context.bool_val(expression->getValue()));
virtual void visit(storm::expressions::BooleanConstantExpression const* expression) override {
throw storm::exceptions::NotImplementedException() << "BooleanConstantExpression is not supported by Z3ExpressionAdapter.";
}
virtual void visit(ir::expressions::BooleanLiteralExpression* expression) {
stack.push(context.bool_val(expression->getValueAsBool(nullptr)));
virtual void visit(storm::expressions::BooleanLiteralExpression const* expression) override {
stack.push(context.bool_val(expression->evaluateAsBool()));
}
virtual void visit(ir::expressions::DoubleConstantExpression* expression) {
if (!expression->isDefined()) {
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
<< ". Double constant '" << expression->getConstantName() << "' is undefined.";
}
std::stringstream fractionStream;
fractionStream << expression->getValue();
stack.push(context.real_val(fractionStream.str().c_str()));
virtual void visit(storm::expressions::DoubleConstantExpression const* expression) override {
throw storm::exceptions::NotImplementedException() << "DoubleConstantExpression is not supported by Z3ExpressionAdapter.";
}
virtual void visit(ir::expressions::DoubleLiteralExpression* expression) {
virtual void visit(storm::expressions::DoubleLiteralExpression const* expression) override {
std::stringstream fractionStream;
fractionStream << expression->getValueAsDouble(nullptr);
fractionStream << expression->evaluateAsDouble();
stack.push(context.real_val(fractionStream.str().c_str()));
}
virtual void visit(ir::expressions::IntegerConstantExpression* expression) {
if (!expression->isDefined()) {
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
<< ". Integer constant '" << expression->getConstantName() << "' is undefined.";
}
stack.push(context.int_val(static_cast<int>(expression->getValue())));
virtual void visit(storm::expressions::IntegerConstantExpression const* expression) override {
throw storm::exceptions::NotImplementedException() << "IntegerConstantExpression is not supported by Z3ExpressionAdapter.";
}
virtual void visit(ir::expressions::IntegerLiteralExpression* expression) {
stack.push(context.int_val(static_cast<int>(expression->getValueAsInt(nullptr))));
virtual void visit(storm::expressions::IntegerLiteralExpression const* expression) override {
stack.push(context.int_val(static_cast<int>(expression->evaluateAsInt())));
}
virtual void visit(ir::expressions::UnaryBooleanFunctionExpression* expression) {
expression->getChild()->accept(this);
virtual void visit(storm::expressions::UnaryBooleanFunctionExpression const* expression) override {
expression->getOperand()->accept(this);
z3::expr childResult = stack.top();
stack.pop();
switch (expression->getFunctionType()) {
case storm::ir::expressions::UnaryBooleanFunctionExpression::NOT:
switch (expression->getOperatorType()) {
case storm::expressions::UnaryBooleanFunctionExpression::OperatorType::Not:
stack.push(!childResult);
break;
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
<< "Unknown boolean binary operator: '" << expression->getFunctionType() << "' in expression " << expression->toString() << ".";
<< "Unknown boolean binary operator: '" << expression->getOperatorType() << "' in expression " << expression << ".";
}
}
virtual void visit(ir::expressions::UnaryNumericalFunctionExpression* expression) {
expression->getChild()->accept(this);
virtual void visit(storm::expressions::UnaryNumericalFunctionExpression const* expression) override {
expression->getOperand()->accept(this);
z3::expr childResult = stack.top();
stack.pop();
switch(expression->getFunctionType()) {
case storm::ir::expressions::UnaryNumericalFunctionExpression::MINUS:
switch(expression->getOperatorType()) {
case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Minus:
stack.push(0 - childResult);
break;
break;
case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Floor: {
z3::expr floorVariable = context.int_const(("__floor_" + std::to_string(additionalVariableCounter++)).c_str());
additionalAssertions.push(z3::expr(context, Z3_mk_int2real(context, floorVariable)) <= childResult < (z3::expr(context, Z3_mk_int2real(context, floorVariable)) + 1));
throw storm::exceptions::NotImplementedException() << "Unary numerical function 'floor' is not supported by Z3ExpressionAdapter.";
break;
}
case storm::expressions::UnaryNumericalFunctionExpression::OperatorType::Ceil:{
z3::expr ceilVariable = context.int_const(("__floor_" + std::to_string(additionalVariableCounter++)).c_str());
additionalAssertions.push(z3::expr(context, Z3_mk_int2real(context, ceilVariable)) - 1 <= childResult < z3::expr(context, Z3_mk_int2real(context, ceilVariable)));
throw storm::exceptions::NotImplementedException() << "Unary numerical function 'floor' is not supported by Z3ExpressionAdapter.";
break;
}
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
<< "Unknown numerical unary operator: '" << expression->getFunctionType() << "'.";
<< "Unknown numerical unary operator: '" << expression->getOperatorType() << "'.";
}
}
virtual void visit(storm::expressions::IfThenElseExpression const* expression) override {
expression->getCondition()->accept(this);
expression->getThenExpression()->accept(this);
expression->getElseExpression()->accept(this);
z3::expr conditionResult = stack.top();
stack.pop();
z3::expr thenResult = stack.top();
stack.pop();
z3::expr elseResult = stack.top();
stack.pop();
stack.push(z3::expr(context, Z3_mk_ite(context, conditionResult, thenResult, elseResult)));
}
virtual void visit(ir::expressions::VariableExpression* expression) {
virtual void visit(storm::expressions::VariableExpression const* expression) override {
stack.push(variableToExpressionMap.at(expression->getVariableName()));
}
private:
z3::context& context;
std::stack<z3::expr> stack;
std::stack<z3::expr> additionalAssertions;
uint_fast64_t additionalVariableCounter;
std::map<std::string, z3::expr> variableToExpressionMap;
};

5
src/solver/SmtSolver.h
View File

@ -31,7 +31,7 @@ namespace storm {
InterpolantComputation = 0x04
};
//! possible check results
enum class CheckResult {SAT, UNSAT, UNKNOWN};
enum class CheckResult { SAT, UNSAT, UNKNOWN };
public:
/*!
* Constructs a new smt solver with the given options.
@ -42,6 +42,9 @@ namespace storm {
SmtSolver(Options options = Options::ModelGeneration) {};
virtual ~SmtSolver() {};
SmtSolver(const SmtSolver&) = delete;
SmtSolver(const SmtSolver&&) {};
//! pushes a backtrackingpoint in the solver
virtual void push() = 0;
//! pops a backtrackingpoint in the solver

Write Preview
Loading…
Cancel
Save