mathsat does not like boolean arguments to ite-expressions, so we encode it ourselves now

Former-commit-id: e30e7fcd55

src/adapters/MathsatExpressionAdapter.h

@@ -58,12 +58,15 @@ namespace storm {
              */
 			msat_term translateExpression(storm::expressions::Expression const& expression) {
                 msat_term result = boost::any_cast<msat_term>(expression.getBaseExpression().accept(*this));
-                STORM_LOG_THROW(!MSAT_ERROR_TERM(result), storm::exceptions::ExpressionEvaluationException, "Could not translate expression to MathSAT's format.");
+                if (MSAT_ERROR_TERM(result)) {
+                    std::string errorMessage(msat_last_error_message(env));
+                    STORM_LOG_THROW(!MSAT_ERROR_TERM(result), storm::exceptions::ExpressionEvaluationException, "Could not translate expression to MathSAT's format. (Message: " << errorMessage << ")");
+                }
 				return result;
 			}
             
             /*!
-             * Translates the given variable to an equivalent expression for Z3.
+             * Translates the given variable to an equivalent expression for MathSAT.
              *
              * @param variable The variable to translate.
              * @return An equivalent term for MathSAT.
@@ -164,7 +167,13 @@ namespace storm {
                 msat_term conditionResult = boost::any_cast<msat_term>(expression.getCondition()->accept(*this));
 				msat_term thenResult = boost::any_cast<msat_term>(expression.getThenExpression()->accept(*this));
 				msat_term elseResult = boost::any_cast<msat_term>(expression.getElseExpression()->accept(*this));
+                
+                // MathSAT does not allow ite with boolean arguments, so we have to encode it ourselves.
+                if (expression.getThenExpression()->hasBooleanType() && expression.getElseExpression()->hasBooleanType()) {
+                    return msat_make_and(env, msat_make_or(env, msat_make_not(env, conditionResult), thenResult), msat_make_or(env, conditionResult, elseResult));
+                } else {
                     return msat_make_term_ite(env, conditionResult, thenResult, elseResult);
+                }
 			}
 
 			virtual boost::any visit(expressions::BooleanLiteralExpression const& expression) override {

src/storage/prism/menu_games/AbstractProgram.cpp

@@ -144,8 +144,6 @@ namespace storm {
                     bottomStates = bottomStateAbstractor.getAbstractStates();
                 }
                 
-                std::cout << "found " << (reachableStates && bottomStates).getNonZeroCount() << " reachable bottom states" << std::endl;
-                
                 // Find the deadlock states in the model.
                 storm::dd::Bdd<DdType> deadlockStates = transitionRelation.existsAbstract(ddInformation.successorVariables);
                 deadlockStates = reachableStates && !deadlockStates;

src/storage/prism/menu_games/StateSetAbstractor.cpp

@@ -72,14 +72,11 @@ namespace storm {
             template <storm::dd::DdType DdType, typename ValueType>
             storm::dd::Bdd<DdType> StateSetAbstractor<DdType, ValueType>::getStateBdd(storm::solver::SmtSolver::ModelReference const& model) const {
                 STORM_LOG_TRACE("Building source state BDD.");
-                std::cout << "new model: " << std::endl;
                 storm::dd::Bdd<DdType> result = ddInformation.manager->getBddOne();
                 for (auto const& variableIndexPair : relevantPredicatesAndVariables) {
                     if (model.getBooleanValue(variableIndexPair.first)) {
-                        std::cout << expressionInformation.predicates[variableIndexPair.second] << " is true" << std::endl;
                         result &= ddInformation.predicateBdds[variableIndexPair.second].first;
                     } else {
-                        std::cout << expressionInformation.predicates[variableIndexPair.second] << " is false" << std::endl;
                         result &= !ddInformation.predicateBdds[variableIndexPair.second].first;
                     }
                 }
@@ -114,7 +111,7 @@ namespace storm {
                 
                 storm::dd::Bdd<DdType> result = ddInformation.manager->getBddZero();
                 uint_fast64_t modelCounter = 0;
-                smtSolver->allSat(decisionVariables, [&result,this,&modelCounter] (storm::solver::SmtSolver::ModelReference const& model) { result |= getStateBdd(model); ++modelCounter; std::cout << "found " << modelCounter << " models" << std::endl; return modelCounter < 10000 ? true : false; } );
+                smtSolver->allSat(decisionVariables, [&result,this,&modelCounter] (storm::solver::SmtSolver::ModelReference const& model) { result |= getStateBdd(model); return true; } );
                 
                 cachedBdd = result;
             }
@@ -122,22 +119,25 @@ namespace storm {
             template <storm::dd::DdType DdType, typename ValueType>
             void StateSetAbstractor<DdType, ValueType>::popConstraintBdd() {
                 // If the last constraint was not the constant one BDD, we need to pop the constraint from the solver.
-                if (!this->constraint.isOne()) {
-                    smtSolver->pop();
+                if (this->constraint.isOne()) {
+                    return;
                 }
+                smtSolver->pop();
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
             void StateSetAbstractor<DdType, ValueType>::pushConstraintBdd() {
+                if (this->constraint.isOne()) {
+                    return;
+                }
+                
                 // Create a new backtracking point before adding the constraint.
                 smtSolver->push();
                 
                 // Then add the constraint.
                 std::pair<std::vector<storm::expressions::Expression>, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>> result = constraint.toExpression(expressionInformation.manager, ddInformation.bddVariableIndexToPredicateMap);
                 
-                std::cout << "adding expressions... " << std::endl;
                 for (auto const& expression : result.first) {
-                    std::cout << expression << std::endl;
                     smtSolver->add(expression);
                 }
             }

test/functional/abstraction/PrismMenuGameTest.cpp

@@ -31,6 +31,7 @@ TEST(PrismMenuGame, DieAbstractionTest) {
     
     EXPECT_EQ(10, game.getNumberOfTransitions());
     EXPECT_EQ(2, game.getNumberOfStates());
+    EXPECT_EQ(0, game.getBottomStates().getNonZeroCount());
 }
 
 TEST(PrismMenuGame, DieAbstractionAndRefinementTest) {
@@ -49,6 +50,7 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest) {
     
     EXPECT_EQ(10, game.getNumberOfTransitions());
     EXPECT_EQ(3, game.getNumberOfStates());
+    EXPECT_EQ(0, game.getBottomStates().getNonZeroCount());
 }
 
 TEST(PrismMenuGame, DieFullAbstractionTest) {
@@ -80,6 +82,7 @@ TEST(PrismMenuGame, DieFullAbstractionTest) {
     
     EXPECT_EQ(20, game.getNumberOfTransitions());
     EXPECT_EQ(13, game.getNumberOfStates());
+    EXPECT_EQ(0, game.getBottomStates().getNonZeroCount());
 }
 
 TEST(PrismMenuGame, CrowdsAbstractionTest) {
@@ -97,6 +100,7 @@ TEST(PrismMenuGame, CrowdsAbstractionTest) {
     
     EXPECT_EQ(11, game.getNumberOfTransitions());
     EXPECT_EQ(2, game.getNumberOfStates());
+    EXPECT_EQ(1, game.getBottomStates().getNonZeroCount());
 }
 
 TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest) {
@@ -116,6 +120,7 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest) {
     
     EXPECT_EQ(28, game.getNumberOfTransitions());
     EXPECT_EQ(4, game.getNumberOfStates());
+    EXPECT_EQ(2, game.getBottomStates().getNonZeroCount());
 }
 
 TEST(PrismMenuGame, CrowdsFullAbstractionTest) {
@@ -187,6 +192,7 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest) {
     
     EXPECT_EQ(15113, game.getNumberOfTransitions());
     EXPECT_EQ(8607, game.getNumberOfStates());
+    EXPECT_EQ(1260, game.getBottomStates().getNonZeroCount());
 }
 
 TEST(PrismMenuGame, TwoDiceAbstractionTest) {
@@ -206,6 +212,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest) {
     
     EXPECT_EQ(34, game.getNumberOfTransitions());
     EXPECT_EQ(4, game.getNumberOfStates());
+    EXPECT_EQ(0, game.getBottomStates().getNonZeroCount());
 }
 
 TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest) {
@@ -227,6 +234,7 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest) {
 
     EXPECT_EQ(164, game.getNumberOfTransitions());
     EXPECT_EQ(8, game.getNumberOfStates());
+    EXPECT_EQ(0, game.getBottomStates().getNonZeroCount());
 }
 
 TEST(PrismMenuGame, TwoDiceFullAbstractionTest) {
@@ -277,6 +285,7 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest) {
     
     EXPECT_EQ(436, game.getNumberOfTransitions());
     EXPECT_EQ(169, game.getNumberOfStates());
+    EXPECT_EQ(0, game.getBottomStates().getNonZeroCount());
 }
 
 TEST(PrismMenuGame, WlanAbstractionTest) {
@@ -295,8 +304,11 @@ TEST(PrismMenuGame, WlanAbstractionTest) {
     
     storm::prism::menu_games::MenuGame<storm::dd::DdType::CUDD> game = abstractProgram.getAbstractGame();
     
+    game.getTransitionMatrix().exportToDot("trans.dot");
+    game.getReachableStates().toAdd().exportToDot("reach.dot");
     EXPECT_EQ(281, game.getNumberOfTransitions());
     EXPECT_EQ(4, game.getNumberOfStates());
+    EXPECT_EQ(4, game.getBottomStates().getNonZeroCount());
 }
 
 TEST(PrismMenuGame, WlanAbstractionAndRefinementTest) {
@@ -319,6 +331,7 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest) {
 
     EXPECT_EQ(564, game.getNumberOfTransitions());
     EXPECT_EQ(8, game.getNumberOfStates());
+    EXPECT_EQ(8, game.getBottomStates().getNonZeroCount());
 }
 
 TEST(PrismMenuGame, WlanFullAbstractionTest) {
@@ -437,6 +450,7 @@ TEST(PrismMenuGame, WlanFullAbstractionTest) {
     
     EXPECT_EQ(9503, game.getNumberOfTransitions());
     EXPECT_EQ(5523, game.getNumberOfStates());
+    EXPECT_EQ(0, game.getBottomStates().getNonZeroCount());
 }
 
 #endif