105 lines
4.5 KiB
105 lines
4.5 KiB
#ifndef STORM_ADAPTERS_Z3EXPRESSIONADAPTER_H_
|
|
#define STORM_ADAPTERS_Z3EXPRESSIONADAPTER_H_
|
|
|
|
#include <unordered_map>
|
|
#include <vector>
|
|
|
|
#include "storm-config.h"
|
|
|
|
// Include the headers of Z3 only if it is available.
|
|
#ifdef STORM_HAVE_Z3
|
|
#include "z3++.h"
|
|
#include "z3.h"
|
|
#endif
|
|
|
|
#include "src/storage/expressions/Variable.h"
|
|
#include "src/storage/expressions/ExpressionVisitor.h"
|
|
|
|
namespace storm {
|
|
namespace adapters {
|
|
|
|
#ifdef STORM_HAVE_Z3
|
|
class Z3ExpressionAdapter : public storm::expressions::ExpressionVisitor {
|
|
public:
|
|
/*!
|
|
* Creates an expression adapter that can translate expressions to the format of Z3.
|
|
*
|
|
* @param manager The manager that can be used to build expressions.
|
|
* @param context A reference to the Z3 context over which to build the expressions. The lifetime of the
|
|
* context needs to be guaranteed as long as the instance of this adapter is used.
|
|
*/
|
|
Z3ExpressionAdapter(storm::expressions::ExpressionManager& manager, z3::context& context);
|
|
|
|
/*!
|
|
* Translates the given expression to an equivalent expression for Z3.
|
|
*
|
|
* @param expression The expression to translate.
|
|
* @return An equivalent expression for Z3.
|
|
*/
|
|
z3::expr translateExpression(storm::expressions::Expression const& expression);
|
|
|
|
/*!
|
|
* Translates the given variable to an equivalent expression for Z3.
|
|
*
|
|
* @param variable The variable to translate.
|
|
* @return An equivalent expression for Z3.
|
|
*/
|
|
z3::expr translateExpression(storm::expressions::Variable const& variable);
|
|
|
|
storm::expressions::Expression translateExpression(z3::expr const& expr);
|
|
/*!
|
|
* Finds the counterpart to the given z3 variable declaration.
|
|
*
|
|
* @param z3Declaration The declaration for which to find the equivalent.
|
|
* @return The equivalent counterpart.
|
|
*/
|
|
storm::expressions::Variable const& getVariable(z3::func_decl z3Declaration);
|
|
|
|
virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression) override;
|
|
|
|
virtual boost::any visit(storm::expressions::BinaryNumericalFunctionExpression const& expression) override;
|
|
|
|
virtual boost::any visit(storm::expressions::BinaryRelationExpression const& expression) override;
|
|
|
|
virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression) override;
|
|
|
|
virtual boost::any visit(storm::expressions::DoubleLiteralExpression const& expression) override;
|
|
|
|
virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression) override;
|
|
|
|
virtual boost::any visit(storm::expressions::UnaryBooleanFunctionExpression const& expression) override;
|
|
|
|
virtual boost::any visit(storm::expressions::UnaryNumericalFunctionExpression const& expression) override;
|
|
|
|
virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression) override;
|
|
|
|
virtual boost::any visit(storm::expressions::VariableExpression const& expression) override;
|
|
|
|
private:
|
|
/*!
|
|
* Creates a Z3 variable for the provided variable.
|
|
*
|
|
* @param variable The variable for which to create a Z3 counterpart.
|
|
*/
|
|
z3::expr createVariable(storm::expressions::Variable const& variable);
|
|
// The manager that can be used to build expressions.
|
|
storm::expressions::ExpressionManager& manager;
|
|
|
|
// The context that is used to translate the expressions.
|
|
z3::context& context;
|
|
|
|
// A vector of assertions that need to be kept separate, because they were only implicitly part of an
|
|
// assertion that was added.
|
|
std::vector<z3::expr> additionalAssertions;
|
|
|
|
// A mapping from variables to their Z3 equivalent.
|
|
std::unordered_map<storm::expressions::Variable, z3::expr> variableToExpressionMapping;
|
|
|
|
// A mapping from z3 declarations to the corresponding variables.
|
|
std::unordered_map<Z3_func_decl, storm::expressions::Variable> declarationToVariableMapping;
|
|
};
|
|
#endif
|
|
} // namespace adapters
|
|
} // namespace storm
|
|
|
|
#endif /* STORM_ADAPTERS_Z3EXPRESSIONADAPTER_H_ */
|