Working on the new explanation system.

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index e26687bf138ef8c8dda51ebe48bbb235e3901a25..78b9d3494e7da08ad4a1cb9475f01b2aac490a3c 100644 (file)
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -922,6 +922,28 @@ bool ConstraintValue::proofIsEmpty() const{
   return result;
 }
 
+Node ConstraintValue::makeImplication(const std::vector<Constraint>& b) const{
+  Node antecedent = makeConjunction(b);
+  Node implied = getLiteral();
+  return antecedent.impNode(implied);
+}
+
+
+Node ConstraintValue::makeConjunction(const std::vector<Constraint>& b){
+  NodeBuilder<> nb(kind::AND);
+  for(vector<Constraint>::const_iterator i = b.begin(), end = b.end(); i != end; ++i){
+    Constraint b_i = *i;
+    b_i->explainBefore(nb, AssertionOrderSentinel);
+  }
+  if(nb.getNumChildren() >= 2){
+    return nb;
+  }else if(nb.getNumChildren() == 1){
+    return nb[0];
+  }else{
+    return mkBoolNode(true);
+  }
+}
+
 void ConstraintValue::explainBefore(NodeBuilder<>& nb, AssertionOrder order) const{
   Assert(hasProof());
   Assert(!isSelfExplaining() || assertedToTheTheory());

diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index a5d64a6525941b76fca366e62c11d35d4c8785b4..4966115d2f9bd13a82b64ba74b07ba34e16ae64b 100644 (file)
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -598,6 +598,8 @@ public:
   void impliedBy(Constraint a, Constraint b);
   void impliedBy(const std::vector<Constraint>& b);
 
+  Node makeImplication(const std::vector<Constraint>& b) const;
+  static Node makeConjunction(const std::vector<Constraint>& b);
 
   /** The node must have a proof already and be eligible for propagation! */
   void propagate();

diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index 4779b10121aeb81b264314f7e8de7f1f13565238..bde771102fedc7d0a867679f06f2d4e2bb675029 100644 (file)
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -581,7 +581,7 @@ void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c){
                                    << basic << ") done" << endl;
 }
 
-void LinearEqualityModule::propagateRow(RowIndex ridx, bool rowUp, Constraint c){
+void LinearEqualityModule::propagateRow(vector<Constraint>& into, RowIndex ridx, bool rowUp, Constraint c){
   Assert(!c->assertedToTheTheory());
   Assert(c->canBePropagated());
   Assert(!c->hasProof());
@@ -589,7 +589,7 @@ void LinearEqualityModule::propagateRow(RowIndex ridx, bool rowUp, Constraint c)
   ArithVar v = c->getVariable();
   Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
                                    << v <<") start" << endl;
-  vector<Constraint> bounds;
+  //vector<Constraint> bounds;
 
   Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx);
   for(; !iter.atEnd(); ++iter){
@@ -608,9 +608,8 @@ void LinearEqualityModule::propagateRow(RowIndex ridx, bool rowUp, Constraint c)
 
     Assert(bound != NullConstraint);
     Debug("arith::explainNonbasics") << "explainNonbasics" << bound << " for " << c << endl;
-    bounds.push_back(bound);
+    into.push_back(bound);
   }
-  c->impliedBy(bounds);
   Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
                                    << v << ") done" << endl;
 }

diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index 767c0934060831d34472f601431cd7617839f7ac..b1f3d00d73794f322886a3468e76307a75130cfe 100644 (file)
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -431,7 +431,7 @@ public:
    * Exports either the explanation of an upperbound or a lower bound
    * of the basic variable basic, using the non-basic variables in the row.
    */
-  void propagateRow(RowIndex ridx, bool rowUp, Constraint c);
+  void propagateRow(std::vector<Constraint>& into, RowIndex ridx, bool rowUp, Constraint c);
 
   /**
    * Computes the value of a basic variable using the assignments

diff --git a/src/theory/arith/options b/src/theory/arith/options
index cf0782a92103f317ae7ce0aec119fd85f0822099..1366addaec7bafb432c75bd788ad09047e5a0552 100644 (file)
--- a/src/theory/arith/options
+++ b/src/theory/arith/options
@@ -94,4 +94,7 @@ option exportDioDecompositions --dio-decomps bool :default false :read-write
 option newProp --new-prop bool :default false :read-write
  Use the new row propagation system
 
+option arithPropAsLemmaLength --arith-prop-clauses int :default 8 :read-write
+ Rows shorter than this are propagated as clauses
+
 endmodule

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index c71f2a6bd6f6dada641b944daa66403b7acde9c1..31b6cd03221488c2cf4c46a7a59e838d11f11507 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -116,6 +116,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context
   d_cutInContext(c),
   d_statistics()
 {
+  srand(79);
 }
 
 TheoryArithPrivate::~TheoryArithPrivate(){ }
@@ -2548,18 +2549,21 @@ bool TheoryArithPrivate::propagateCandidateBound(ArithVar basic, bool upperBound
         }
         // I think this can be skipped if canBePropagated is true
         //d_learnedBounds.push(bestImplied);
-        cout << "success " << bestImplied << endl;
-        d_partialModel.printModel(basic, cout);
-
+        if(Debug.isOn("arith::prop")){
+          Debug("arith::prop") << "success " << bestImplied << endl;
+          d_partialModel.printModel(basic, Debug("arith::prop"));
+        }
         return true;
       }
-      cout << "failed " << basic << " " << bound << assertedToTheTheory << " " <<
-        canBePropagated << " " << hasProof << endl;
-      d_partialModel.printModel(basic, cout);
+      if(Debug.isOn("arith::prop")){
+        Debug("arith::prop") << "failed " << basic << " " << bound << assertedToTheTheory << " " <<
+          canBePropagated << " " << hasProof << endl;
+        d_partialModel.printModel(basic, Debug("arith::prop"));
+      }
     }
-  }else{
-    cout << "false " << bound << " ";
-    d_partialModel.printModel(basic, cout);
+  }else if(Debug.isOn("arith::prop")){
+    Debug("arith::prop") << "false " << bound << " ";
+    d_partialModel.printModel(basic, Debug("arith::prop"));
   }
   return false;
 }
@@ -2580,7 +2584,7 @@ void TheoryArithPrivate::propagateCandidate(ArithVar basic){
 void TheoryArithPrivate::propagateCandidates(){
   TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime);
 
-  cout << "propagateCandidates begin" << endl;
+  Debug("arith::prop") << "propagateCandidates begin" << endl;
 
   Assert(d_candidateBasics.empty());
 
@@ -2615,7 +2619,7 @@ void TheoryArithPrivate::propagateCandidates(){
     Assert(d_tableau.isBasic(candidate));
     propagateCandidate(candidate);
   }
-  cout << "propagateCandidates end" << endl << endl << endl;
+  Debug("arith::prop") << "propagateCandidates end" << endl << endl << endl;
 }
 
 void TheoryArithPrivate::propagateCandidatesNew(){
@@ -2634,7 +2638,7 @@ void TheoryArithPrivate::propagateCandidatesNew(){
    */
 
   TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime);
-  cout << "propagateCandidatesNew begin" << endl;
+  Debug("arith::prop") << "propagateCandidatesNew begin" << endl;
 
   Assert(d_qflraStatus == Result::SAT);
   if(d_updatedBounds.empty()){ return; }
@@ -2651,7 +2655,7 @@ void TheoryArithPrivate::propagateCandidatesNew(){
     d_candidateRows.pop_back();
     propagateCandidateRow(candidate);
   }
-  cout << "propagateCandidatesNew end" << endl << endl << endl;
+  Debug("arith::prop") << "propagateCandidatesNew end" << endl << endl << endl;
 }
 
 bool TheoryArithPrivate::propagateMightSucceed(ArithVar v, bool ub) const{
@@ -2678,7 +2682,7 @@ bool TheoryArithPrivate::propagateMightSucceed(ArithVar v, bool ub) const{
 }
 
 bool TheoryArithPrivate::attemptSingleton(RowIndex ridx, bool rowUp){
-  cout << "  attemptSingleton" << ridx;
+  Debug("arith::prop") << "  attemptSingleton" << ridx;
 
   const Tableau::Entry* ep;
   ep = d_linEq.rowLacksBound(ridx, rowUp, ARITHVAR_SENTINEL);
@@ -2698,8 +2702,8 @@ bool TheoryArithPrivate::attemptSingleton(RowIndex ridx, bool rowUp){
   // if c < 0, v \geq -D/c so !vUp
   bool vUp = (rowUp == ( coeff.sgn() < 0));
 
-  cout << "  " << rowUp << " " << v << " " << coeff << " " << vUp << endl;
-  cout << "  " << propagateMightSucceed(v, vUp) << endl;
+  Debug("arith::prop") << "  " << rowUp << " " << v << " " << coeff << " " << vUp << endl;
+  Debug("arith::prop") << "  " << propagateMightSucceed(v, vUp) << endl;
 
   if(propagateMightSucceed(v, vUp)){
     DeltaRational dr = d_linEq.computeRowBound(ridx, rowUp, v);
@@ -2710,7 +2714,7 @@ bool TheoryArithPrivate::attemptSingleton(RowIndex ridx, bool rowUp){
 }
 
 bool TheoryArithPrivate::attemptFull(RowIndex ridx, bool rowUp){
-  cout << "  attemptFull" << ridx << endl;
+  Debug("arith::prop") << "  attemptFull" << ridx << endl;
 
   vector<const Tableau::Entry*> candidates;
 
@@ -2746,11 +2750,6 @@ bool TheoryArithPrivate::attemptFull(RowIndex ridx, bool rowUp){
     DeltaRational impliedBound = (slack - contribution)/(-c);
 
     bool success = tryToPropagate(ridx, rowUp, v, vUb, impliedBound);
-    if(success){
-      cout << " success " << v << endl;
-    }else{
-      cout << " fail " << v << endl;
-    }
     any |= success;
   }
   return any;
@@ -2770,6 +2769,30 @@ bool TheoryArithPrivate::tryToPropagate(RowIndex ridx, bool rowUp, ArithVar v, b
   return false;
 }
 
+Node flattenImplication(Node imp){
+  NodeBuilder<> nb(kind::OR);
+  Node left = imp[0];
+  Node right = imp[1];
+
+  if(left.getKind() == kind::AND){
+    for(Node::iterator i = left.begin(), iend = left.end(); i != iend; ++i) {
+      nb << (*i).negate();
+    }
+  }else{
+    nb << left.negate();
+  }
+
+  if(right.getKind() == kind::OR){
+    for(Node::iterator i = right.begin(), iend = right.end(); i != iend; ++i) {
+      nb << *i;
+    }
+  }else{
+    nb << right;
+  }
+
+  return nb;
+}
+
 bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, Constraint implied){
   Assert(implied != NullConstraint);
   ArithVar v = implied->getVariable();
@@ -2791,15 +2814,33 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C
   }
 
   if(!assertedToTheTheory && canBePropagated && !hasProof ){
-    d_linEq.propagateRow(ridx, rowUp, implied);
+    vector<Constraint> explain;
+    d_linEq.propagateRow(explain, ridx, rowUp, implied);
+    if(d_tableau.getRowLength(ridx) <= options::arithPropAsLemmaLength()){
+      Node implication = implied->makeImplication(explain);
+      Node clause = flattenImplication(implication);
+      outputLemma(clause);
+    }else{
+      implied->impliedBy(explain);
+    }
     return true;
   }
-  cout << "failed " << v << " " << assertedToTheTheory << " " <<
-    canBePropagated << " " << hasProof << " " << implied << endl;
-  d_partialModel.printModel(v, cout);
+
+  if(Debug.isOn("arith::prop")){
+    Debug("arith::prop")
+      << "failed " << v << " " << assertedToTheTheory << " "
+      << canBePropagated << " " << hasProof << " " << implied << endl;
+    d_partialModel.printModel(v, Debug("arith::prop"));
+  }
   return false;
 }
 
+double fRand(double fMin, double fMax)
+{
+    double f = (double)rand() / RAND_MAX;
+    return fMin + f * (fMax - fMin);
+}
+
 bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx){
   BoundCounts hasCount = d_linEq.hasBoundCount(ridx);
   uint32_t rowLength = d_tableau.getRowLength(ridx);
@@ -2807,10 +2848,14 @@ bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx){
   bool success = false;
   static int instance = 0;
   ++instance;
-  cout << "propagateCandidateRow " << instance << " attempt " << rowLength << " " <<  hasCount << endl;
+
+  Debug("arith::prop")
+    << "propagateCandidateRow " << instance << " attempt " << rowLength << " " <<  hasCount << endl;
 
   if(rowLength >= options::arithPropagateMaxLength()){
-    return false;
+    if(fRand(0.0,1.0) >= double(options::arithPropagateMaxLength())/rowLength){
+      return false;
+    }
   }
 
   if(hasCount.lowerBoundCount() == rowLength){