Fixed order of checks in Z3ExpressionAdapter, fixed missing override of isVariable in VariableExpression, removed unnecessary exception in Z3SmtSolver model generation

Former-commit-id: ca5f876655

src/adapters/Z3ExpressionAdapter.h

@@ -102,6 +102,11 @@ namespace storm {
             }
             
 			storm::expressions::Expression translateExpression(z3::expr const& expr) {
+				//std::cout << std::boolalpha << expr.is_var() << std::endl;
+				//std::cout << std::boolalpha << expr.is_app() << std::endl;
+				//std::cout << expr.decl().decl_kind() << std::endl;
+
+				/*
 				if (expr.is_bool() && expr.is_const()) {
 					switch (Z3_get_bool_value(expr.ctx(), expr)) {
 						case Z3_L_FALSE:
@@ -128,7 +133,8 @@ namespace storm {
 					} else {
 						LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Expression is constant real and value does not fit into a fraction with 64-bit integer numerator and denominator.");
 					}
-				} else if (expr.is_app()) {
+					} else */
+				if (expr.is_app()) {
 					switch (expr.decl().decl_kind()) {
 						case Z3_OP_TRUE:
 							return storm::expressions::Expression::createTrue();
@@ -192,8 +198,26 @@ namespace storm {
 							return this->translateExpression(expr.arg(0)) / this->translateExpression(expr.arg(1));
 						case Z3_OP_IDIV:
 							return this->translateExpression(expr.arg(0)) / this->translateExpression(expr.arg(1));
+						case Z3_OP_ANUM:
+							//Arithmetic numeral
+							if (expr.is_int() && expr.is_const()) {
+								int_fast64_t value;
+								if (Z3_get_numeral_int64(expr.ctx(), expr, &value)) {
+									return storm::expressions::Expression::createIntegerLiteral(value);
+								} else {
+									LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Expression is constant integer and value does not fit into 64-bit integer.");
+								}
+							} else if (expr.is_real() && expr.is_const()) {
+								int_fast64_t num;
+								int_fast64_t den;
+								if (Z3_get_numeral_rational_int64(expr.ctx(), expr, &num, &den)) {
+									return storm::expressions::Expression::createDoubleLiteral(static_cast<double>(num) / static_cast<double>(den));
+								} else {
+									LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Expression is constant real and value does not fit into a fraction with 64-bit integer numerator and denominator.");
+								}
+							}
 						case Z3_OP_UNINTERPRETED:
-							//this should be a variable...
+							//storm only supports uninterpreted constant functions
 							LOG_THROW(expr.is_const(), storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Encountered non constant uninterpreted function.");
 							if (expr.is_bool()) {
 								return storm::expressions::Expression::createBooleanVariable(expr.decl().name().str());

src/solver/Z3SmtSolver.cpp

@@ -162,9 +162,6 @@ namespace storm {
 
 			}
 
-
-
-			LOG_THROW(false, storm::exceptions::NotImplementedException, "Model generation is not implemented in this Z3 solver interface.");
 #else
 			LOG_THROW(false, storm::exceptions::NotImplementedException, "StoRM is compiled without Z3 support.");
 #endif

src/storage/expressions/VariableExpression.cpp

@@ -48,6 +48,10 @@ namespace storm {
         bool VariableExpression::containsVariables() const {
             return true;
         }
+
+		bool VariableExpression::isVariable() const {
+			return true;
+		}
         
         std::set<std::string> VariableExpression::getVariables() const {
             return {this->getVariableName()};

src/storage/expressions/VariableExpression.h

@@ -31,6 +31,7 @@ namespace storm {
             virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override;
             virtual std::string const& getIdentifier() const override;
             virtual bool containsVariables() const override;
+			virtual bool isVariable() const override;
 			virtual std::set<std::string> getVariables() const override;
 			virtual std::map<std::string, ExpressionReturnType> getVariablesAndTypes() const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;

test/functional/adapter/Z3ExpressionAdapterTest.cpp

@@ -171,17 +171,17 @@ TEST(Z3ExpressionAdapter, Z3ToStormBasic) {
 
 	z3::expr z3True = ctx.bool_val(true);
 	storm::expressions::Expression exprTrue;
-	ASSERT_NO_THROW(exprTrue = adapter.translateExpression(z3True));
+	exprTrue = adapter.translateExpression(z3True);
 	ASSERT_TRUE(exprTrue.isTrue());
 
 	z3::expr z3False = ctx.bool_val(false);
 	storm::expressions::Expression exprFalse;
-	ASSERT_NO_THROW(exprFalse = adapter.translateExpression(z3False));
+	exprFalse = adapter.translateExpression(z3False);
 	ASSERT_TRUE(exprFalse.isFalse());
 
 	z3::expr z3Conjunction = (ctx.bool_const("x") && ctx.bool_const("y"));
 	storm::expressions::Expression exprConjunction;
-	ASSERT_NO_THROW(exprConjunction = adapter.translateExpression(z3Conjunction));
+	(exprConjunction = adapter.translateExpression(z3Conjunction));
 	ASSERT_EQ(storm::expressions::OperatorType::And, exprConjunction.getOperator());
 	ASSERT_TRUE(exprConjunction.getOperand(0).isVariable());
 	ASSERT_EQ("x", exprConjunction.getOperand(0).getIdentifier());
@@ -190,7 +190,7 @@ TEST(Z3ExpressionAdapter, Z3ToStormBasic) {
 
 	z3::expr z3Nor = !(ctx.bool_const("x") || ctx.bool_const("y"));
 	storm::expressions::Expression exprNor;
-	ASSERT_NO_THROW(exprNor = adapter.translateExpression(z3Nor));
+	(exprNor = adapter.translateExpression(z3Nor));
 	ASSERT_EQ(storm::expressions::OperatorType::Not, exprNor.getOperator());
 	ASSERT_EQ(storm::expressions::OperatorType::Or, exprNor.getOperand(0).getOperator());
 	ASSERT_TRUE(exprNor.getOperand(0).getOperand(0).isVariable());

test/functional/solver/Z3SmtSolverTest.cpp

@@ -174,13 +174,13 @@ TEST(Z3SmtSolver, GenerateModel) {
 		&& c == (a * b)
 		&& b + a > c;
 
-	ASSERT_NO_THROW(s.assertExpression(exprFormula));
-	ASSERT_NO_THROW(result = s.check());
+	(s.assertExpression(exprFormula));
+	(result = s.check());
 	ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::SAT);
 	storm::expressions::SimpleValuation model;
-	ASSERT_NO_THROW(model = s.getModel());
+	(model = s.getModel());
 	int_fast64_t a_eval;
-	ASSERT_NO_THROW(a_eval = model.getIntegerValue("a"));
+	(a_eval = model.getIntegerValue("a"));
 	ASSERT_EQ(1, a_eval);
 
 #else