Farkas proof coefficients.

This commit adds tracking of Farkas coefficients to proof enabled builds in the theory of linear
real arithmetic when proofs are enabled. There could be some performance changes due to subtly
different search paths being taken.

Additional bug fixes:
- Polynomial::exactDivide did not satisfy preconditions to the Monomial constructor.
  To prevent future problems, Monomials should now be made via one of the mkMonomial functions.
- Fixes a bug in SumOfInfeasibilitiesSPD::greedyConflictSubsets().
  There was a way to use a row twice in the construction of the conflicts.
  This was violating an assumption in the Tableau when constructing the intermediate rows.

Constraints:
- To enable proofs, all conflicts and propagations are designed to go through the Constraint system
  before they are converted to externally understandable conflicts and propagations in the form
  of Node.
- Constraints must now be given a reason for marking them as true that corresponds to a proof.
- Constraints should now be marked as being true by one of the impliedbyX functions.
- Each impliedByX function has an ArithProofType associated with it.
- Each call to an impliedByX function stores a context dependent ConstraintRule object
  to track the proof.
- After marking the node as true the caller should either try to propagate the constraint or raise
	a conflict.
- There are no more special cases for marking a node as being true when its negation has a proof
  vs. when the negation does not have a proof. One must now explicitly pass in a inConflict flag
	to the impliedByX (and similar functions).
	For example,this is now longer both:
	  void setAssertedToTheTheory(TNode witness);
	  void setAssertedToTheTheoryWithNegationTrue(TNode witness);
  There is just:
    void setAssertedToTheTheory(TNode witness, bool inConflict);

1 files changed, 87 insertions, 42 deletions

diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index 34f911b81..0d07c5ffc 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -634,12 +634,16 @@ unsigned SumOfInfeasibilitiesSPD::trySet(const ArithVarVec& set){
 }
 
 std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
+  Debug("arith::greedyConflictSubsets") << "greedyConflictSubsets start" << endl;
+
   std::vector< ArithVarVec > subsets;
   Assert(d_soiVar == ARITHVAR_SENTINEL);
 
   if(d_errorSize <= 2){
     ArithVarVec inError;
     d_errorSet.pushFocusInto(inError);
+    
+    Assert(debugIsASet(inError));
     subsets.push_back(inError);
     return subsets;
   }
@@ -653,9 +657,11 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
     ArithVar e = *iter;
     addRowSgns(sgns, e, d_errorSet.getSgn(e));
 
-    //cout << "basic error var: " << e << endl;
-    //d_tableau.debugPrintIsBasic(e);
-    //d_tableau.printBasicRow(e, cout);
+    Debug("arith::greedyConflictSubsets") << "basic error var: " << e << endl;
+    if(Debug.isOn("arith::greedyConflictSubsets")){
+      d_tableau.debugPrintIsBasic(e);
+      d_tableau.printBasicRow(e, Debug("arith::greedyConflictSubsets"));
+    }
   }
 
   // Phase 1: Try to find at least 1 pair for every element
@@ -683,9 +689,10 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
       tmp[0] = e;
       tmp[1] = b;
       if(trySet(tmp) == 2){
-        //cout << "found a pair" << endl;
+        Debug("arith::greedyConflictSubsets")  << "found a pair " << b << " " << e << endl;
         hasParticipated.softAdd(b);
         hasParticipated.softAdd(e);
+        Assert(debugIsASet(tmp));
         subsets.push_back(tmp);
         ++(d_statistics.d_soiConflicts);
         ++(d_statistics.d_hasToBeMinimal);
@@ -704,13 +711,15 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
     possibleStarts.pop_back();
     if(hasParticipated.isMember(v)){ continue; }
 
+    hasParticipated.add(v);
+    
     Assert(d_soiVar == ARITHVAR_SENTINEL);
     //d_soiVar's row =  \sumofinfeasibilites underConstruction
     ArithVarVec underConstruction;
     underConstruction.push_back(v);
     d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization, v);
 
-    //cout << "trying " << v << endl;
+    Debug("arith::greedyConflictSubsets") << "trying " << v << endl;
 
     const Tableau::Entry* spoiler = NULL;
     while( (spoiler = d_linEq.selectSlackEntry(d_soiVar, false)) != NULL){
@@ -718,16 +727,16 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
       int oppositeSgn = -(spoiler->getCoefficient().sgn());
       Assert(oppositeSgn != 0);
 
-      //cout << "looking for " << nb << " " << oppositeSgn << endl;
+      Debug("arith::greedyConflictSubsets") << "looking for " << nb << " " << oppositeSgn << endl;
 
       ArithVar basicWithOp = find_basic_in_sgns(sgns, nb, oppositeSgn, hasParticipated, false);
 
       if(basicWithOp == ARITHVAR_SENTINEL){
-        //cout << "search did not work  for " << nb << endl;
+        Debug("arith::greedyConflictSubsets") << "search did not work  for " << nb << endl;
         // greedy construction has failed
         break;
       }else{
-        //cout << "found  " << basicWithOp << endl;
+        Debug("arith::greedyConflictSubsets") << "found  " << basicWithOp << endl;
 
         addToInfeasFunc(d_statistics.d_soiConflictMinimization, d_soiVar, basicWithOp);
         hasParticipated.softAdd(basicWithOp);
@@ -735,8 +744,9 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
       }
     }
     if(spoiler == NULL){
-      //cout << "success" << endl;
+      Debug("arith::greedyConflictSubsets") << "success" << endl;
       //then underConstruction contains a conflicting subset
+      Assert(debugIsASet(underConstruction));
       subsets.push_back(underConstruction);
       ++d_statistics.d_soiConflicts;
       if(underConstruction.size() == 3){
@@ -745,7 +755,7 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
         ++d_statistics.d_maybeNotMinimal;
       }
     }else{
-      //cout << "failure" << endl;
+      Debug("arith::greedyConflictSubsets") << "failure" << endl;
     }
     tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization, d_soiVar);
     d_soiVar = ARITHVAR_SENTINEL;
@@ -762,52 +772,89 @@ std::vector< ArithVarVec > SumOfInfeasibilitiesSPD::greedyConflictSubsets(){
 
 
   Assert(d_soiVar == ARITHVAR_SENTINEL);
+  Debug("arith::greedyConflictSubsets") << "greedyConflictSubsets done" << endl;
   return subsets;
 }
 
-void SumOfInfeasibilitiesSPD::generateSOIConflict(const ArithVarVec& subset){
+bool SumOfInfeasibilitiesSPD::generateSOIConflict(const ArithVarVec& subset){
   Assert(d_soiVar == ARITHVAR_SENTINEL);
   d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization, subset);
+  Assert(!subset.empty());
+  Assert(!d_conflictBuilder->underConstruction());
+    
+  Debug("arith::generateSOIConflict") << "SumOfInfeasibilitiesSPD::generateSOIConflict(...) start" << endl;
 
-  //NodeBuilder<> conflict(kind::AND);
+  bool success = false;
+    
   for(ArithVarVec::const_iterator iter = subset.begin(), end = subset.end(); iter != end; ++iter){
     ArithVar e = *iter;
     ConstraintP violated = d_errorSet.getViolated(e);
-    //cout << "basic error var: " << violated << endl;
-    d_conflictChannel.addConstraint(violated);
-    //violated->explainForConflict(conflict);
+    Assert(violated != NullConstraint);
 
-    //d_tableau.debugPrintIsBasic(e);
-    //d_tableau.printBasicRow(e, cout);
-  }
-  for(Tableau::RowIterator i = d_tableau.basicRowIterator(d_soiVar); !i.atEnd(); ++i){
-    const Tableau::Entry& entry = *i;
-    ArithVar v = entry.getColVar();
-    if(v == d_soiVar){ continue; }
-    const Rational& coeff = entry.getCoefficient();
 
-    ConstraintP c = (coeff.sgn() > 0) ?
-      d_variables.getUpperBoundConstraint(v) :
-      d_variables.getLowerBoundConstraint(v);
+    int sgn = d_errorSet.getSgn(e);
+    const Rational& violatedCoeff = sgn > 0 ? d_negOne : d_posOne;
+    Debug("arith::generateSOIConflict") << "basic error var: "
+                                        << "(" <<  violatedCoeff << ")"
+                                        << " " << violated
+                                        << endl;
 
-    //cout << "nb : " << c << endl;
-    d_conflictChannel.addConstraint(c);
+
+    d_conflictBuilder->addConstraint(violated, violatedCoeff);
+    Assert(violated->hasProof());
+    if(!success && !violated->negationHasProof()){
+      success = true;
+      d_conflictBuilder->makeLastConsequent();
+    }
+  }
+  
+  if(!success){
+    // failure
+    d_conflictBuilder->reset();
+  } else {
+    // pick a violated constraint arbitrarily. any of them may be selected for the conflict
+    Assert(d_conflictBuilder->underConstruction());
+    Assert(d_conflictBuilder->consequentIsSet());
+    
+    for(Tableau::RowIterator i = d_tableau.basicRowIterator(d_soiVar); !i.atEnd(); ++i){
+      const Tableau::Entry& entry = *i;
+      ArithVar v = entry.getColVar();
+      if(v == d_soiVar){ continue; }
+      const Rational& coeff = entry.getCoefficient();
+
+      ConstraintP c = (coeff.sgn() > 0) ?
+        d_variables.getUpperBoundConstraint(v) :
+        d_variables.getLowerBoundConstraint(v);
+      
+      Debug("arith::generateSOIConflict") << "non-basic var: "
+                                          << "(" <<  coeff << ")"
+                                          << " " << c
+                                          << endl;
+      d_conflictBuilder->addConstraint(c, coeff);
+    }
+    ConstraintCP conflicted = d_conflictBuilder->commitConflict();
+    d_conflictChannel.raiseConflict(conflicted);
   }
 
-  //Node conf = conflict;
   tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization, d_soiVar);
   d_soiVar = ARITHVAR_SENTINEL;
-  d_conflictChannel.commitConflict();
-  //return conf;
+  Debug("arith::generateSOIConflict") << "SumOfInfeasibilitiesSPD::generateSOIConflict(...) done" << endl;
+  Assert(d_soiVar == ARITHVAR_SENTINEL);
+  Assert(!d_conflictBuilder->underConstruction());
+  return success;
 }
 
 
 WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){
   static int instance = 0;
   instance++;
-  //cout << "SOI conflict " << instance << ": |E| = " << d_errorSize << endl;
-  //d_errorSet.debugPrint(cout);
-  //cout << endl;
+  
+  Debug("arith::SOIConflict") << "SumOfInfeasibilitiesSPD::SOIConflict() start "
+                              << instance << ": |E| = " << d_errorSize << endl;
+  if(Debug.isOn("arith::SOIConflict")){
+    d_errorSet.debugPrint(cout);
+  }
+  Debug("arith::SOIConflict") << endl;
 
   tearDownInfeasiblityFunction(d_statistics.d_soiConflictMinimization, d_soiVar);
   d_soiVar = ARITHVAR_SENTINEL;
@@ -815,24 +862,22 @@ WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){
   if(options::soiQuickExplain()){
     quickExplain();
     generateSOIConflict(d_qeConflict);
-    //Node conflict = generateSOIConflict(d_qeConflict);
-    //cout << conflict << endl;
-    //d_conflictChannel(conflict);
   }else{
-
     vector<ArithVarVec> subsets = greedyConflictSubsets();
     Assert(  d_soiVar == ARITHVAR_SENTINEL);
-
+    bool anySuccess = false;
     Assert(!subsets.empty());
     for(vector<ArithVarVec>::const_iterator i = subsets.begin(), end = subsets.end(); i != end; ++i){
       const ArithVarVec& subset = *i;
-      generateSOIConflict(subset);
+      Assert(debugIsASet(subset));
+      anySuccess = generateSOIConflict(subset) || anySuccess;
       //Node conflict = generateSOIConflict(subset);
       //cout << conflict << endl;
 
       //reportConflict(conf); do not do this. We need a custom explanations!
       //d_conflictChannel(conflict);
     }
+    Assert(anySuccess);
   }
   Assert(  d_soiVar == ARITHVAR_SENTINEL);
   d_soiVar = constructInfeasiblityFunction(d_statistics.d_soiConflictMinimization);
@@ -840,7 +885,8 @@ WitnessImprovement SumOfInfeasibilitiesSPD::SOIConflict(){
   //reportConflict(conf); do not do this. We need a custom explanations!
   d_conflictVariables.add(d_soiVar);
 
-  //cout << "SOI conflict " << instance << "end" << endl;
+  Debug("arith::SOIConflict") << "SumOfInfeasibilitiesSPD::SOIConflict() done "
+                              << instance << "end" << endl;
   return ConflictFound;
 }
 
@@ -877,7 +923,6 @@ WitnessImprovement SumOfInfeasibilitiesSPD::soiRound() {
 }
 
 bool SumOfInfeasibilitiesSPD::debugSOI(WitnessImprovement w, ostream& out, int instance) const{
-//#warning "Redo SOI"
   return true;
   // out << "DLV("<<instance<<") ";
   // switch(w){