From 0329899304fdf4f43d98558c3523a63a7e884f91 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 21 Oct 2013 18:36:48 +0200
Subject: [PATCH] Removed debug output from Z3 adapter. Put new backward cuts
 in actions.

Former-commit-id: a26787f613713b318b2d7ef8f07d699784a407c0
---
 src/adapters/Z3ExpressionAdapter.h            |  5 --
 .../SMTMinimalCommandSetGenerator.h           | 51 +++++++++----------
 2 files changed, 23 insertions(+), 33 deletions(-)

diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h
index e3864f4fc..6a6ce210a 100644
--- a/src/adapters/Z3ExpressionAdapter.h
+++ b/src/adapters/Z3ExpressionAdapter.h
@@ -39,12 +39,10 @@ namespace storm {
                 expression->accept(this);
                 z3::expr result = stack.top();
                 stack.pop();
-                LOG4CPLUS_DEBUG(logger, "Returning " << result << ".");
                 return result;
             }
             
             virtual void visit(ir::expressions::BinaryBooleanFunctionExpression* expression) {
-                LOG4CPLUS_DEBUG(logger, "Binary boolean function expression " << expression->toString() << ".");
                 expression->getLeft()->accept(this);
                 expression->getRight()->accept(this);
                 
@@ -100,7 +98,6 @@ namespace storm {
             }
             
             virtual void visit(ir::expressions::BinaryRelationExpression* expression) {
-                LOG4CPLUS_DEBUG(logger, "Binary boolean relation expression " << expression->toString() << ".");
                 expression->getLeft()->accept(this);
                 expression->getRight()->accept(this);
                 
@@ -173,7 +170,6 @@ namespace storm {
             }
             
             virtual void visit(ir::expressions::IntegerLiteralExpression* expression) {
-                LOG4CPLUS_DEBUG(logger, "IntegerLiteralExpression " << expression->toString() << ".");
                 stack.push(context.int_val(expression->getValueAsInt(nullptr)));
             }
             
@@ -208,7 +204,6 @@ namespace storm {
             }
             
             virtual void visit(ir::expressions::VariableExpression* expression) {
-                LOG4CPLUS_DEBUG(logger, "Variable " << expression->toString() << ".");
                 stack.push(variableToExpressionMap.at(expression->getVariableName()));
             }
             
diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h
index a87653a71..e13aa2d9d 100644
--- a/src/counterexamples/SMTMinimalCommandSetGenerator.h
+++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h
@@ -525,7 +525,6 @@ namespace storm {
                             } else {
                                 guardExpression = guardExpression | !expressionAdapter.translateExpression(command.get().getGuard());
                             }
-                            std::cout << command.get().getGuard()->toString() << std::endl;
                         }
                         localSolver.add(guardExpression);
                         LOG4CPLUS_DEBUG(logger, "Asserted disjunction of negated guards.");
@@ -607,34 +606,30 @@ namespace storm {
                         // Popping the disjunction of negated guards from the solver stack.
                         localSolver.pop();
                     }
+                    
+                    for (auto const& labelSetImplicationsPair : backwardImplications) {
+                        std::vector<z3::expr> implicationExpression;
+                        
+                        // Create the first part of the implication.
+                        for (auto label : labelSetImplicationsPair.first) {
+                            if (relevancyInformation.knownLabels.find(label) == relevancyInformation.knownLabels.end()) {
+                                implicationExpression.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)));
+                            }
+                        }
+                        
+                        // Create the disjunction of conjuncts that represent the possible implications.
+                        for (auto const& implicationSet : labelSetImplicationsPair.second) {
+                            implicationExpression.push_back(context.bool_val(true));
+                            for (auto label : implicationSet) {
+                                if (relevancyInformation.knownLabels.find(label) == relevancyInformation.knownLabels.end()) {
+                                    implicationExpression.back() = implicationExpression.back() && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label));
+                                }
+                            }
+                        }
+                        
+                        assertDisjunction(context, solver, implicationExpression);
+                    }
                 }
-                
-                std::vector<z3::expr> formulae;
-                std::cout << "got " << backwardImplications.size() << " backward implications." << std::endl;
-//                for (auto const& labelSetImplicationSetsPair : backwardImplications) {
-//                    // We only need to make this an implication if the label is not already known. If it is known,
-//                    // we can directly assert the disjunction of the implications.
-//                    if (relevancyInformation.knownLabels.find(labelImplicationsPair.first) == relevancyInformation.knownLabels.end()) {
-//                        formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(labelImplicationsPair.first)));
-//                    }
-//                    
-//                    std::set<uint_fast64_t> actualImplications;
-//                    std::set_intersection(labelImplicationsPair.second.begin(), labelImplicationsPair.second.end(), precedingLabels.at(labelImplicationsPair.first).begin(), precedingLabels.at(labelImplicationsPair.first).end(), std::inserter(actualImplications, actualImplications.begin()));
-//
-//                    // We should assert the implications if they are not already known to be true anyway.
-//                    std::set<uint_fast64_t> knownImplications;
-//                    std::set_intersection(actualImplications.begin(), actualImplications.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(knownImplications, knownImplications.begin()));
-//
-//                    if (knownImplications.empty()) {
-//                        for (auto label : actualImplications) {
-//                            formulae.push_back(variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)));
-//                        }
-//                    
-//                        std::cout << "actually asserting a backward implication." << std::endl;
-//                        assertDisjunction(context, solver, formulae);
-//                        formulae.clear();
-//                    }
-//                }
             }
             
             /*!