SimplexDecisionProcedure no longer takes an OutputChannel as a parameter.

diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 1e7b5c028a11db9f59d3849a0e4ed198176243cf..bfa2d56d3dff636ed75a0c55ebb95fb0daf53004 100644 (file)
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -85,19 +85,19 @@ SimplexDecisionProcedure::Statistics::~Statistics(){
 }
 
 /* procedure AssertLower( x_i >= c_i ) */
-bool SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode original){
+Node SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode original){
   Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl;
 
   if(d_partialModel.belowLowerBound(x_i, c_i, false)){
-    return false; //sat
+    return Node::null();
   }
   if(d_partialModel.aboveUpperBound(x_i, c_i, true)){
     Node ubc = d_partialModel.getUpperConstraint(x_i);
     Node conflict =  NodeManager::currentNM()->mkNode(AND, ubc, original);
-    d_out->conflict(conflict);
+    //d_out->conflict(conflict);
     Debug("arith") << "AssertLower conflict " << conflict << endl;
     ++(d_statistics.d_statAssertLowerConflicts);
-    return true;
+    return conflict;
   }
 
   d_partialModel.setLowerConstraint(x_i,original);
@@ -111,24 +111,28 @@ bool SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_
     d_queue.enqueueIfInconsistent(x_i);
   }
 
-  return false;
+  if(Debug.isOn("model")) { d_partialModel.printModel(x_i); }
+
+  return Node::null();
 }
 
 /* procedure AssertUpper( x_i <= c_i) */
-bool SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode original){
+Node SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode original){
 
   Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
 
   if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){ // \upperbound(x_i) <= c_i
-    return false; //sat
+    //return false; //sat
+    return Node::null();
   }
   if(d_partialModel.belowLowerBound(x_i, c_i, true)){// \lowerbound(x_i) > c_i
     Node lbc = d_partialModel.getLowerConstraint(x_i);
     Node conflict =  NodeManager::currentNM()->mkNode(AND, lbc, original);
     Debug("arith") << "AssertUpper conflict " << conflict << endl;
     ++(d_statistics.d_statAssertUpperConflicts);
-    d_out->conflict(conflict);
-    return true;
+    //d_out->conflict(conflict);
+    return conflict;
+    //return true;
   }
 
   d_partialModel.setUpperConstraint(x_i,original);
@@ -141,13 +145,16 @@ bool SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_
   }else{
     d_queue.enqueueIfInconsistent(x_i);
   }
-  d_partialModel.printModel(x_i);
-  return false;
+
+  if(Debug.isOn("model")) { d_partialModel.printModel(x_i); }
+
+  return Node::null();
+  //return false;
 }
 
 
 /* procedure AssertLower( x_i == c_i ) */
-bool SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode original){
+Node SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode original){
 
   Debug("arith") << "AssertEquality(" << x_i << " " << c_i << ")"<< std::endl;
 
@@ -155,23 +162,26 @@ bool SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational&
   // This can happen if both c_i <= x_i and x_i <= c_i are in the system.
   if(d_partialModel.belowLowerBound(x_i, c_i, false) &&
      d_partialModel.aboveUpperBound(x_i, c_i, false)){
-    return false; //sat
+    //return false; //sat
+    return Node::null();
   }
 
   if(d_partialModel.aboveUpperBound(x_i, c_i, true)){
     Node ubc = d_partialModel.getUpperConstraint(x_i);
     Node conflict =  NodeManager::currentNM()->mkNode(AND, ubc, original);
-    d_out->conflict(conflict);
+    //d_out->conflict(conflict);
     Debug("arith") << "AssertLower conflict " << conflict << endl;
-    return true;
+    //return true;
+    return conflict;
   }
 
   if(d_partialModel.belowLowerBound(x_i, c_i, true)){
     Node lbc = d_partialModel.getLowerConstraint(x_i);
     Node conflict =  NodeManager::currentNM()->mkNode(AND, lbc, original);
     Debug("arith") << "AssertUpper conflict " << conflict << endl;
-    d_out->conflict(conflict);
-    return true;
+    //d_out->conflict(conflict);
+    //return true;
+    return conflict;
   }
 
   d_partialModel.setLowerConstraint(x_i,original);
@@ -189,7 +199,8 @@ bool SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational&
     //checkBasicVariable(x_i);
   }
 
-  return false;
+  //return false;
+  return Node::null();
 }
 
 set<ArithVar> tableauAndHasSet(Tableau& tab, ArithVar v){

diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 6f3ff073fea2712f11e4c04af48ffb40c1b73246..968275ae559fa82d0a58adfcef2580a3ac7e8e81 100644 (file)
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -10,7 +10,6 @@
 #include "theory/arith/delta_rational.h"
 #include "theory/arith/tableau.h"
 #include "theory/arith/partial_model.h"
-#include "theory/output_channel.h"
 
 #include "util/options.h"
 
@@ -31,8 +30,6 @@ private:
    */
   ArithPartialModel& d_partialModel;
 
-  OutputChannel* d_out;
-
   Tableau& d_tableau;
   ArithPriorityQueue d_queue;
 
@@ -45,10 +42,8 @@ private:
 
 public:
   SimplexDecisionProcedure(ArithPartialModel& pm,
-                           OutputChannel* out,
                            Tableau& tableau) :
     d_partialModel(pm),
-    d_out(out),
     d_tableau(tableau),
     d_queue(pm, tableau),
     d_numVariables(0),
@@ -61,20 +56,20 @@ public:
    * Assert*(n, orig) takes an bound n that is implied by orig.
    * and asserts that as a new bound if it is tighter than the current bound
    * and updates the value of a basic variable if needed.
-   * If this new bound is in conflict with the other bound,
-   * a conflict is created and asserted to the output channel.
    *
-   * orig must be an atom in the SAT solver so that it can be used for
+   * orig must be a literal in the SAT solver so that it can be used for
    * conflict analysis.
    *
-   * n is of the form (x =?= c) where x is a variable,
-   * c is a constant and =?= is either LT, LEQ, EQ, GEQ, or GT.
+   * x is the variable getting the new bound,
+   * c is the value of the new bound.
    *
-   * returns true if a conflict was asserted.
+   * If this new bound is in conflict with the other bound,
+   * a node describing this conflict is returned.
+   * If this new bound is not in conflict, Node::null() is returned.
    */
-  bool AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode orig);
-  bool AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode orig);
-  bool AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode orig);
+  Node AssertLower(ArithVar x, const DeltaRational& c, TNode orig);
+  Node AssertUpper(ArithVar x, const DeltaRational& c, TNode orig);
+  Node AssertEquality(ArithVar x, const DeltaRational& c, TNode orig);
 
 private:
   /**

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 726bfc210fb62ff13344eb8e1b6d5db423da7cfa..dfa81cb3fae923981f4d35029804f6332899b8f0 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -66,7 +66,7 @@ TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) :
   d_tableauResetDensity(2.0),
   d_tableauResetPeriod(10),
   d_propagator(c, out),
-  d_simplex(d_partialModel, d_out, d_tableau),
+  d_simplex(d_partialModel, d_tableau),
   d_DELTA_ZERO(0),
   d_statistics()
 {}
@@ -308,16 +308,14 @@ DeltaRational determineRightConstant(TNode assertion, Kind simpleKind){
   return DeltaRational(noninf, inf);
 }
 
-void TheoryArith::disequalityConflict(TNode eq, TNode lb, TNode ub){
-
+Node TheoryArith::disequalityConflict(TNode eq, TNode lb, TNode ub){
   NodeBuilder<3> conflict(kind::AND);
   conflict << eq << lb << ub;
   ++(d_statistics.d_statDisequalityConflicts);
-  d_out->conflict((TNode)conflict);
-
+  return conflict;
 }
 
-bool TheoryArith::assertionCases(TNode assertion){
+Node TheoryArith::assertionCases(TNode assertion){
   Kind simpKind = simplifiedKind(assertion);
   Assert(simpKind != UNDEFINED_KIND);
   ArithVar x_i = determineLeftVariable(assertion, simpKind);
@@ -331,18 +329,18 @@ bool TheoryArith::assertionCases(TNode assertion){
     if (d_partialModel.hasLowerBound(x_i) && d_partialModel.getLowerBound(x_i) == c_i) {
       Node diseq = assertion[0].eqNode(assertion[1]).notNode();
       if (d_diseq.find(diseq) != d_diseq.end()) {
-        disequalityConflict(diseq, d_partialModel.getLowerConstraint(x_i) , assertion);
-        return true;
+        Node lb = d_partialModel.getLowerConstraint(x_i);
+        return disequalityConflict(diseq, lb , assertion);
       }
     }
   case LT:
-    return d_simplex.AssertUpper(x_i, c_i, assertion);
+    return  d_simplex.AssertUpper(x_i, c_i, assertion);
   case GEQ:
     if (d_partialModel.hasUpperBound(x_i) && d_partialModel.getUpperBound(x_i) == c_i) {
       Node diseq = assertion[0].eqNode(assertion[1]).notNode();
       if (d_diseq.find(diseq) != d_diseq.end()) {
-        disequalityConflict(diseq, assertion, d_partialModel.getUpperConstraint(x_i));
-        return true;
+        Node ub = d_partialModel.getUpperConstraint(x_i);
+        return disequalityConflict(diseq, assertion, ub);
       }
     }
   case GT:
@@ -366,14 +364,13 @@ bool TheoryArith::assertionCases(TNode assertion){
           d_partialModel.getUpperBound(lhsVar) == rhsValue) {
         Node lb = d_partialModel.getLowerConstraint(lhsVar);
         Node ub = d_partialModel.getUpperConstraint(lhsVar);
-        disequalityConflict(assertion, lb, ub);
-        return true;
+        return disequalityConflict(assertion, lb, ub);
       }
     }
-    return false;
+    return Node::null();
   default:
     Unreachable();
-    return false;
+    return Node::null();
   }
 }
 
@@ -385,10 +382,11 @@ void TheoryArith::check(Effort effortLevel){
   while(!done()){
 
     Node assertion = get();
-    bool conflictDuringAnAssert = assertionCases(assertion);
+    Node possibleConflict = assertionCases(assertion);
 
-    if(conflictDuringAnAssert){
+    if(!possibleConflict.isNull()){
       d_partialModel.revertAssignmentChanges();
+      d_out->conflict(possibleConflict);
       return;
     }
   }

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index ef93b7d64953347b44531d515a05a2c3ecb824b1..07ba08e9c22f6894879c07e568c48b55d2480069 100644 (file)
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -203,14 +203,15 @@ private:
 
   /**
    * Handles the case splitting for check() for a new assertion.
-   * returns true if their is a conflict.
+   * Returns a conflict if one was found.
+   * Returns Node::null if no conflict was found.
    */
-  bool assertionCases(TNode assertion);
+  Node assertionCases(TNode assertion);
 
   /**
    * This is used for reporting conflicts caused by disequalities during assertionCases.
    */
-  void disequalityConflict(TNode eq, TNode lb, TNode ub);
+  Node disequalityConflict(TNode eq, TNode lb, TNode ub);
 
   /**
    * Returns the basic variable with the shorted row containg a non-basic variable.