- This fixes a problem where simplex produced the same conflict in the single check call.

- This increases the number of substitutions that ppAssert can solve on integer equations.

7 files changed, 73 insertions, 71 deletions

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 3cb5464da..d2a0d9bfa 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -26,7 +26,7 @@ ConstraintType constraintTypeOfComparison(const Comparison& cmp){
       if(l.leadingCoefficientIsPositive()){ // (< x c)
         return UpperBound;
       }else{
-        return LowerBound; // (< (-x) c) 
+        return LowerBound; // (< (-x) c)
       }
     }
   case GT:
@@ -482,7 +482,8 @@ Constraint ConstraintDatabase::getConstraint(ArithVar v, ConstraintType t, const
     }else{
       pair<SortedConstraintMapIterator, bool> negInsertAttempt;
       negInsertAttempt = scm.insert(make_pair(negC->getValue(), ValueCollection()));
-      Assert(negInsertAttempt.second);
+      Assert(negInsertAttempt.second
+             || ! negInsertAttempt.first->second.hasConstraintOfType(negC->getType()));
       negPos = negInsertAttempt.first;
     }
 
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 2e0a9d067..fe10ecc4a 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -403,6 +403,15 @@ public:
   bool isUpperBound() const{
     return d_type == UpperBound;
   }
+  bool isStrictUpperBound() const{
+    Assert(isUpperBound());
+    return getValue().infinitesimalSgn() < 0;
+  }
+
+  bool isStrictLowerBound() const{
+    Assert(isLowerBound());
+    return getValue().infinitesimalSgn() > 0;
+  }
 
   bool isSplit() const {
     return d_split;
@@ -422,7 +431,7 @@ public:
 
   /**
    * Light wrapper for calling setCanBePropagated(),
-   * on this and this-d_negation.
+   * on this and this->d_negation.
    */
   void setPreregistered(){
     setCanBePropagated();
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index 964d27464..7efe349e5 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -257,7 +257,7 @@ void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c){
   Assert(d_tableau.isBasic(basic));
   Assert(c->getVariable() == basic);
   Assert(!c->assertedToTheTheory());
-  Assert(c->canBePropagated());
+  //Assert(c->canBePropagated());
   Assert(!c->hasProof());
 
   Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
@@ -279,35 +279,23 @@ void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c){
     if(upperBound){
       if(sgn < 0){
         bound = d_partialModel.getLowerBoundConstraint(nonbasic);
-        //d_partialModel.explainLowerBound(nonbasic, output);
-        //bound = d_partialModel.explainLowerBound(nonbasic);
       }else{
         Assert(sgn > 0);
         bound = d_partialModel.getUpperBoundConstraint(nonbasic);
-        //d_partialModel.explainUpperBound(nonbasic, output);
-        //bound = d_partialModel.explainUpperBound(nonbasic);
       }
     }else{
       if(sgn < 0){
         bound = d_partialModel.getUpperBoundConstraint(nonbasic);
-        //d_partialModel.explainUpperBound(nonbasic, output);
-        //bound =  d_partialModel.explainUpperBound(nonbasic);
       }else{
         Assert(sgn > 0);
         bound = d_partialModel.getLowerBoundConstraint(nonbasic);
-        //d_partialModel.explainLowerBound(nonbasic, output);
-        //bound =  d_partialModel.explainLowerBound(nonbasic);
       }
     }
     Assert(bound != NullConstraint);
     Debug("arith::explainNonbasics") << "explainNonbasics" << bound << " for " << c << endl;
     bounds.push_back(bound);
-    //Assert(!bound.isNull());
-    // Debug("arith::explainNonbasics") << "\t" << nonbasic << " " << sgn << " " << bound
-    //                                  << endl;
-    // output << bound;
   }
-  c->propagate(bounds);
+  c->impliedBy(bounds);
   Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
                                    << basic << ") done" << endl;
 }
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index d3092c044..31187afd1 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -34,6 +34,7 @@ static const bool CHECK_AFTER_PIVOT = true;
 static const uint32_t VARORDER_CHECK_PERIOD = 200;
 
 SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq, NodeCallBack& conflictChannel) :
+  d_conflictVariable(ARITHVAR_SENTINEL),
   d_linEq(linEq),
   d_partialModel(d_linEq.getPartialModel()),
   d_tableau(d_linEq.getTableau()),
@@ -203,6 +204,7 @@ Node betterConflict(TNode x, TNode y){
 
 bool SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type) {
   TimerStat::CodeTimer codeTimer(d_statistics.d_findConflictOnTheQueueTime);
+  Assert(d_successes.empty());
 
   switch(type){
   case BeforeDiffSearch:     ++(d_statistics.d_attemptBeforeDiffSearch); break;
@@ -212,21 +214,20 @@ bool SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type) {
   case AfterVarOrderSearch:  ++(d_statistics.d_attemptAfterVarOrderSearch); break;
   }
 
-  bool success = false;
   ArithPriorityQueue::const_iterator i = d_queue.begin();
   ArithPriorityQueue::const_iterator end = d_queue.end();
   for(; i != end; ++i){
     ArithVar x_i = *i;
 
-    if(d_tableau.isBasic(x_i)){
+    if(x_i != d_conflictVariable && d_tableau.isBasic(x_i) && !d_successes.isMember(x_i)){
       Node possibleConflict = checkBasicForConflict(x_i);
       if(!possibleConflict.isNull()){
-        success = true;
+        d_successes.add(x_i);
         reportConflict(possibleConflict);
       }
     }
   }
-  if(success){
+  if(!d_successes.empty()){
     switch(type){
     case BeforeDiffSearch:     ++(d_statistics.d_successBeforeDiffSearch); break;
     case DuringDiffSearch:     ++(d_statistics.d_successDuringDiffSearch); break;
@@ -234,11 +235,16 @@ bool SimplexDecisionProcedure::findConflictOnTheQueue(SearchPeriod type) {
     case DuringVarOrderSearch: ++(d_statistics.d_successDuringVarOrderSearch); break;
     case AfterVarOrderSearch:  ++(d_statistics.d_successAfterVarOrderSearch); break;
     }
+    d_successes.purge();
+    return true;
+  }else{
+    return false;
   }
-  return success;
 }
 
 bool SimplexDecisionProcedure::findModel(){
+  Assert(d_conflictVariable == ARITHVAR_SENTINEL);
+
   if(d_queue.empty()){
     return false;
   }
@@ -293,6 +299,7 @@ bool SimplexDecisionProcedure::findModel(){
   // means that the assignment we can always empty these queues.
   d_queue.clear();
   d_pivotsInRound.purge();
+  d_conflictVariable = ARITHVAR_SENTINEL;
 
   Assert(!d_queue.inCollectionMode());
   d_queue.transitionToCollectionMode();
@@ -363,6 +370,7 @@ bool SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
       if(x_j == ARITHVAR_SENTINEL ){
         ++(d_statistics.d_statUpdateConflicts);
         Node conflict = generateConflictBelowLowerBound(x_i); //unsat
+        d_conflictVariable = x_i;
         reportConflict(conflict);
         return true;
       }
@@ -374,6 +382,8 @@ bool SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
       if(x_j == ARITHVAR_SENTINEL ){
         ++(d_statistics.d_statUpdateConflicts);
         Node conflict = generateConflictAboveUpperBound(x_i); //unsat
+
+        d_conflictVariable = x_i;
         reportConflict(conflict);
         return true;
       }
@@ -386,6 +396,7 @@ bool SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
     if(CHECK_AFTER_PIVOT){
       Node possibleConflict = checkBasicForConflict(x_j);
       if(!possibleConflict.isNull()){
+        d_conflictVariable = x_j;
         reportConflict(possibleConflict);
         return true; // unsat
       }
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 6dcfccb8e..8450afb06 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -71,6 +71,8 @@ namespace arith {
 
 class SimplexDecisionProcedure {
 private:
+  ArithVar d_conflictVariable;
+  DenseSet d_successes;
 
   /** Linear equality module. */
   LinearEqualityModule& d_linEq;
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 7f0088f5b..f24b8f411 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -526,6 +526,20 @@ Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubst
   TimerStat::CodeTimer codeTimer(d_statistics.d_simplifyTimer);
   Debug("simplify") << "TheoryArith::solve(" << in << ")" << endl;
 
+//TODO: Handle this better
+// FAIL: preprocess_10.cvc (exit: 1)
+// =================================
+
+// running /home/taking/ws/cvc4/branches/arithmetic/infer-bounds/builds/x86_64-unknown-linux-gnu/debug-staticbinary/src/main/cvc4 --lang=cvc4 --segv-nospin preprocess_10.cvc [from working dir /home/taking/ws/cvc4/branches/arithmetic/infer-bounds/builds/x86_64-unknown-linux-gnu/debug-staticbinary/../../../test/regress/regress0/preprocess]
+// run_regression: error: differences between expected and actual output on stdout
+// --- /tmp/cvc4_expect_stdout.20298.5Ga5123F4L    2012-04-30 12:27:16.136684359 -0400
+// +++ /tmp/cvc4_stdout.20298.oZwTuIYuF3   2012-04-30 12:27:16.176685543 -0400
+// @@ -1 +1,3 @@
+// +TheoryArith::solve(): substitution x |-> IF b THEN 10 ELSE -10 ENDIF
+// +minVar is integral 0right 0
+//  sat
+
+
   // Solve equalities
   Rational minConstant = 0;
   Node minMonomial;
@@ -540,62 +554,33 @@ Theory::PPAssertStatus TheoryArith::ppAssert(TNode in, SubstitutionMap& outSubst
     if (m.getVarList().singleton()){
       VarList vl = m.getVarList();
       Node var = vl.getNode();
-      if (var.getKind() == kind::VARIABLE && !vl.isIntegral()) {
-        minVar = var;
+      if (var.getKind() == kind::VARIABLE){
+        // if vl.isIntegral then m.getConstant().isOne()
+        if(!vl.isIntegral() || m.getConstant().isOne()){
+          minVar = var;
+        }
       }
     }
 
-    //Assert(in[1].getKind() == kind::CONST_RATIONAL);
-    // Find the variable with the smallest coefficient
-    //Polynomial p = Polynomial::parsePolynomial(in[0]);
-
-    // Polynomial::iterator it = p.begin(), it_end = p.end();
-    // for (; it != it_end; ++ it) {
-    //   Monomial m = *it;
-    //   // Skip the constant
-    //   if (m.isConstant()) continue;
-    //   // This is a ''variable''
-    //   nVars ++;
-    //   // Skip the non-linear stuff
-    //   if (!m.getVarList().singleton()) continue;
-    //   // Get the minimal one
-    //   Rational constant = m.getConstant().getValue();
-    //   Rational absSconstant = constant > 0 ? constant : -constant;
-    //   if (minVar.isNull() || absSconstant < minConstant) {
-    //     Node var = m.getVarList().getNode();
-    //     if (var.getKind() == kind::VARIABLE) {
-    //       minVar = var;
-    //       minMonomial = m.getNode();
-    //       minConstant = constant;
-    //     }
-    //   }
-    //}
-
     // Solve for variable
     if (!minVar.isNull()) {
       Polynomial right = cmp.getRight();
-      Node eliminateVar = right.getNode();
+      Node elim = right.getNode();
       // ax + p = c -> (ax + p) -ax - c = -ax
-      // Node eliminateVar = NodeManager::currentNM()->mkNode(kind::MINUS, in[0], minMonomial);
-      // if (in[1].getConst<Rational>() != 0) {
-      //   eliminateVar = NodeManager::currentNM()->mkNode(kind::MINUS, eliminateVar, in[1]);
-      // }
-      // // x = (p - ax - c) * -1/a
-      // eliminateVar = NodeManager::currentNM()->mkNode(kind::MULT, eliminateVar, mkRationalNode(- minConstant.inverse()));
-      // // Add the substitution if not recursive
-      Node rewritten = eliminateVar;
-      Assert(rewritten == Rewriter::rewrite(eliminateVar));
-      if (!rewritten.hasSubterm(minVar)) {
-        Node elim = Rewriter::rewrite(eliminateVar);
-        if (!minVar.getType().isInteger() || elim.getType().isInteger()) {
-          // cannot eliminate integers here unless we know the resulting
-          // substitution is integral
-          Debug("simplify") << "TheoryArith::solve(): substitution " << minVar << " |-> " << elim << endl;
-          outSubstitutions.addSubstitution(minVar, elim);
-          return PP_ASSERT_STATUS_SOLVED;
-        } else {
-          Debug("simplify") << "TheoryArith::solve(): can't substitute b/c it's integer: " << minVar << ":" << minVar.getType() << " |-> " << elim << ":" << elim.getType() << endl;
-        }
+      // x = (p - ax - c) * -1/a
+      // Add the substitution if not recursive
+      Assert(elim == Rewriter::rewrite(elim));
+      Assert(!elim.hasSubterm(minVar));
+
+      if (!minVar.getType().isInteger() || right.isIntegral()) {
+        // cannot eliminate integers here unless we know the resulting
+        // substitution is integral
+        Debug("simplify") << "TheoryArith::solve(): substitution " << minVar << " |-> " << elim << endl;
+
+        outSubstitutions.addSubstitution(minVar, elim);
+        return PP_ASSERT_STATUS_SOLVED;
+      } else {
+        Debug("simplify") << "TheoryArith::solve(): can't substitute b/c it's integer: " << minVar << ":" << minVar.getType() << " |-> " << elim << ":" << elim.getType() << endl;
       }
     }
   }
@@ -1661,6 +1646,11 @@ EqualityStatus TheoryArith::getEqualityStatus(TNode a, TNode b) {
 
 }
 
+bool TheoryArith::rowImplication(ArithVar v, bool upperBound, const DeltaRational& r){
+  Unimplemented();
+  return false;
+}
+
 bool TheoryArith::propagateCandidateBound(ArithVar basic, bool upperBound){
   ++d_statistics.d_boundComputations;
 
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 59653b62d..0b631aa9d 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -60,6 +60,7 @@ namespace arith {
  */
 class TheoryArith : public Theory {
 private:
+  bool rowImplication(ArithVar v, bool upperBound, const DeltaRational& r);
 
   /**
    * This counter is false if nothing has been done since the last cut.