Merging the branch branches/arithmetic/shared-terms into trunk. Arithmetic now supports propagating equalities when a slack variable corresponding to a difference of shared terms must be 0. Similarly disequalities are propagated when these variables cannot be zero.

1 files changed, 53 insertions, 5 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 289d5ace4..53559d949 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -61,7 +61,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
   d_atomsInContext(c),
   d_learner(d_pbSubstitutions),
   d_nextIntegerCheckVar(0),
-  d_partialModel(c),
+  d_partialModel(c, d_differenceManager),
   d_userVariables(),
   d_diseq(c),
   d_tableau(),
@@ -73,6 +73,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
   d_tableauResetPeriod(10),
   d_atomDatabase(c, out),
   d_propManager(c, d_arithvarNodeMap, d_atomDatabase, valuation),
+  d_differenceManager(c, d_propManager),
   d_simplex(d_propManager, d_partialModel, d_tableau),
   d_DELTA_ZERO(0),
   d_statistics()
@@ -89,6 +90,7 @@ TheoryArith::Statistics::Statistics():
   d_staticLearningTimer("theory::arith::staticLearningTimer"),
   d_permanentlyRemovedVariables("theory::arith::permanentlyRemovedVariables", 0),
   d_presolveTime("theory::arith::presolveTime"),
+  d_externalBranchAndBounds("theory::arith::externalBranchAndBounds",0),
   d_initialTableauSize("theory::arith::initialTableauSize", 0),
   d_currSetToSmaller("theory::arith::currSetToSmaller", 0),
   d_smallerSetToCurr("theory::arith::smallerSetToCurr", 0),
@@ -104,6 +106,7 @@ TheoryArith::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_permanentlyRemovedVariables);
   StatisticsRegistry::registerStat(&d_presolveTime);
 
+  StatisticsRegistry::registerStat(&d_externalBranchAndBounds);
 
   StatisticsRegistry::registerStat(&d_initialTableauSize);
   StatisticsRegistry::registerStat(&d_currSetToSmaller);
@@ -122,6 +125,7 @@ TheoryArith::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_permanentlyRemovedVariables);
   StatisticsRegistry::unregisterStat(&d_presolveTime);
 
+  StatisticsRegistry::unregisterStat(&d_externalBranchAndBounds);
 
   StatisticsRegistry::unregisterStat(&d_initialTableauSize);
   StatisticsRegistry::unregisterStat(&d_currSetToSmaller);
@@ -129,6 +133,11 @@ TheoryArith::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_restartTimer);
 }
 
+
+void TheoryArith::addSharedTerm(TNode n){
+  d_differenceManager.addSharedTerm(n);
+}
+
 Node TheoryArith::preprocess(TNode atom) {
   Debug("arith::preprocess") << "arith::preprocess() : " << atom << endl;
 
@@ -332,6 +341,26 @@ void TheoryArith::setupPolynomial(const Polynomial& poly) {
     d_tableau.addRow(varSlack, coefficients, variables);
     setupInitialValue(varSlack);
 
+    //Add differences to the difference manager
+    Polynomial::iterator i = poly.begin(), end = poly.end();
+    if(i != end){
+      Monomial first = *i;
+      ++i;
+      if(i != end){
+        Monomial second = *i;
+        ++i;
+        if(i == end){
+          if(first.getConstant().isOne() && second.getConstant().getValue() == -1){
+            VarList vl0 = first.getVarList();
+            VarList vl1 = second.getVarList();
+            if(vl0.singleton() && vl1.singleton()){
+              d_differenceManager.addDifference(varSlack, vl0.getNode(), vl1.getNode());
+            }
+          }
+        }
+      }
+    }
+
     ++(d_statistics.d_statSlackVariables);
     markSetup(polyNode);
   }
@@ -718,6 +747,7 @@ void TheoryArith::check(Effort effortLevel){
             } else {
               Debug("integers") << "    " << lem[1] << " is not assigned a SAT literal" << endl;
             }
+            ++(d_statistics.d_externalBranchAndBounds);
             d_out->lemma(lem);
 
             // split only on one var
@@ -743,6 +773,7 @@ void TheoryArith::check(Effort effortLevel){
             } else {
               Debug("integers") << "    " << lem[1] << " is not assigned a SAT literal" << endl;
             }
+            ++(d_statistics.d_externalBranchAndBounds);
             d_out->lemma(lem);
 
             // split only on one var
@@ -771,6 +802,7 @@ void TheoryArith::check(Effort effortLevel){
           } else {
             Debug("integers") << "    " << lem[1] << " is not assigned a SAT literal" << endl;
           }
+          ++(d_statistics.d_externalBranchAndBounds);
           d_out->lemma(lem);
 
           // split only on one var
@@ -849,7 +881,12 @@ void TheoryArith::debugPrintModel(){
 Node TheoryArith::explain(TNode n) {
   Debug("explain") << "explain @" << getContext()->getLevel() << ": " << n << endl;
   Assert(d_propManager.isPropagated(n));
-  return d_propManager.explain(n);
+
+  if(d_propManager.isFlagged(n)){
+    return d_differenceManager.explain(n);
+  }else{
+    return d_propManager.explain(n);
+  }
 }
 
 void TheoryArith::propagate(Effort e) {
@@ -862,9 +899,20 @@ void TheoryArith::propagate(Effort e) {
     }
 
     while(d_propManager.hasMorePropagations()){
-      TNode toProp = d_propManager.getPropagation();
+      const PropManager::PropUnit next = d_propManager.getNextPropagation();
+      bool flag = next.flag;
+      TNode toProp = next.consequent;
+
       TNode atom = (toProp.getKind() == kind::NOT) ? toProp[0] : toProp;
-      if(inContextAtom(atom)){
+
+      Debug("arith::propagate") << "propagate " << flag << " " << toProp << endl;
+
+      if(flag) {
+        //Currently if the flag is set this came from an equality detected by the
+        //equality engine in the the difference manager.
+        d_out->propagate(toProp);
+        propagated = true;
+      }else if(inContextAtom(atom)){
         Node satValue = d_valuation.getSatValue(toProp);
         AlwaysAssert(satValue.isNull());
         propagated = true;
@@ -872,7 +920,7 @@ void TheoryArith::propagate(Effort e) {
       }else{
         //Not clear if this is a good time to do this or not...
         Debug("arith::propagate") << "Atom is not in context" << toProp << endl;
-        #warning "enable remove atom in database"
+#warning "enable remove atom in database"
         //d_atomDatabase.removeAtom(atom);
       }
     }