Last commit accidentally lacked r2778 and r2779 from integer2. I have manually broug...

diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index dead34807ad3002387c128778bf5b515bc7c0c7f..1e47d6cdd9371a9dc476049b057f06242dbd9b30 100644 (file)
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -238,7 +238,7 @@ void DioSolver::enqueueInputConstraints(){
     TrailIndex i = d_inputConstraints[curr].d_trailPos;
     TrailIndex j = applyAllSubstitutionsToIndex(i);
 
-    if(!(triviallySat(j)  || anyCoefficientExceedsMaximum(j))){
+    if(!triviallySat(j)){
       if(triviallyUnsat(j)){
         raiseConflict(j);
       }else{
@@ -247,7 +247,7 @@ void DioSolver::enqueueInputConstraints(){
         if(!inConflict()){
           if(triviallyUnsat(k)){
             raiseConflict(k);
-          }else if(!triviallySat(k)){
+          }else if(!(triviallySat(k) || anyCoefficientExceedsMaximum(k))){
             pushToQueueBack(k);
           }
         }
@@ -772,10 +772,10 @@ void DioSolver::subAndReduceCurrentFByIndex(DioSolver::SubIndex subIndex){
 
       if(triviallyUnsat(nextTI)){
         raiseConflict(nextTI);
-      }else if(!(triviallySat(nextTI) || anyCoefficientExceedsMaximum(nextTI))){
+      }else if(!triviallySat(nextTI)){
         TrailIndex nextNextTI = reduceByGCD(nextTI);
 
-        if(!inConflict()){
+        if(!(inConflict() || anyCoefficientExceedsMaximum(nextNextTI))){
           Assert(queueConditions(nextNextTI));
           d_currentF[writeIter] = nextNextTI;
           ++writeIter;

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 824bb59ed314f6e5ca4bb94e525cef9a5556268d..64e713b0aa72a209a1053df24bf72e73e23ef0e1 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -469,28 +469,6 @@ void TheoryArith::asVectors(const Polynomial& p, std::vector<Rational>& coeffs,
   }
 }
 
-// void TheoryArith::setupSlack(TNode left){
-//   //Assert(!left.getAttribute(Slack()));
-//   Assert(!isSlack(left));
-
-
-//   ++(d_statistics.d_statSlackVariables);
-//   left.setAttribute(Slack(), true);
-
-//   d_rowHasBeenAdded = true;
-
-//   Polynomial polyLeft = Polynomial::parsePolynomial(left);
-
-//   vector<ArithVar> variables;
-//   vector<Rational> coefficients;
-
-//   asVectors(polyLeft, coefficients, variables);
-
-//   ArithVar varSlack = requestArithVar(left, true);
-//   d_tableau.addRow(varSlack, coefficients, variables);
-//   setupInitialValue(varSlack);
-// }
-
 /* Requirements:
  * For basic variables the row must have been added to the tableau.
  */
@@ -526,64 +504,6 @@ Node TheoryArith::disequalityConflict(TNode eq, TNode lb, TNode ub){
   return conflict;
 }
 
-// void TheoryArith::delayedSetupMonomial(const Monomial& mono){
-
-//   Debug("arith::delay") << "delayedSetupMonomial(" << mono.getNode() << ")" << endl;
-
-//   Assert(!mono.isConstant());
-//   VarList vl = mono.getVarList();
-  
-//   if(!d_arithvarNodeMap.hasArithVar(vl.getNode())){
-//     for(VarList::iterator i = vl.begin(), end = vl.end(); i != end; ++i){
-//       Variable var = *i;
-//       Node n = var.getNode();
-      
-//       ++(d_statistics.d_statUserVariables);
-//       ArithVar varN = requestArithVar(n,false);
-//       setupInitialValue(varN);
-//     }
-
-//     if(!vl.singleton()){
-//       d_out->setIncomplete();
-
-//       Node n = vl.getNode();
-//       ++(d_statistics.d_statUserVariables);
-//       ArithVar varN = requestArithVar(n,false);
-//       setupInitialValue(varN);
-//     }
-//   }
-// }
-
-// void TheoryArith::delayedSetupPolynomial(TNode polynomial){
-//   Debug("arith::delay") << "delayedSetupPolynomial(" << polynomial << ")" << endl;
-
-//   Assert(Polynomial::isMember(polynomial));
-//   // if d_nodeMap.hasArithVar() all of the variables and it are setup
-//   if(!d_arithvarNodeMap.hasArithVar(polynomial)){
-//     Polynomial poly = Polynomial::parsePolynomial(polynomial);
-//     Assert(!poly.containsConstant());
-//     for(Polynomial::iterator i = poly.begin(), end = poly.end(); i != end; ++i){
-//       Monomial mono = *i;
-//       delayedSetupMonomial(mono);
-//     }
-
-//     if(polynomial.getKind() == PLUS){
-//       Assert(!polynomial.getAttribute(Slack()),
-//          "Polynomial has slack attribute but not does not have arithvar");
-//       setupSlack(polynomial);
-//     }
-//   }
-// }
-
-// void TheoryArith::delayedSetupEquality(TNode equality){
-//   Debug("arith::delay") << "delayedSetupEquality(" << equality << ")" << endl;
-  
-//   Assert(equality.getKind() == EQUAL);
-
-//   TNode left = equality[0];
-//   delayedSetupPolynomial(left);
-// }
-
 bool TheoryArith::canSafelyAvoidEqualitySetup(TNode equality){
   Assert(equality.getKind() == EQUAL);
   return d_arithvarNodeMap.hasArithVar(equality[0]);
@@ -865,7 +785,7 @@ void TheoryArith::check(Effort effortLevel){
 
   if(!emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel()){
 
-    if(!emmittedConflictOrSplit){
+    if(!emmittedConflictOrSplit && Options::current()->dioSolver){
       possibleConflict = callDioSolver();
       if(possibleConflict != Node::null()){
         Debug("arith::conflict") << "dio conflict   " << possibleConflict << endl;
@@ -874,7 +794,7 @@ void TheoryArith::check(Effort effortLevel){
       }
     }
 
-    if(!emmittedConflictOrSplit && d_hasDoneWorkSinceCut){
+    if(!emmittedConflictOrSplit && d_hasDoneWorkSinceCut && Options::current()->dioSolver){
       Node possibleLemma = dioCutting();
       if(!possibleLemma.isNull()){
         Debug("arith") << "dio cut   " << possibleLemma << endl;
@@ -938,94 +858,6 @@ Node TheoryArith::roundRobinBranch(){
       Debug("integers") << "    " << lem[1] << " is not assigned a SAT literal" << endl;
     }
     return lem;
-
-  //   // branch and bound
-  //   if(r.getDenominator() == 1) {
-  //     // r is an integer, but the infinitesimal might not be
-  //     if(i.getNumerator() < 0) {
-  //       // lemma: v <= r - 1 || v >= r
-
-  //       TNode var = d_arithvarNodeMap.asNode(v);
-  //       Node nrMinus1 = NodeManager::currentNM()->mkConst(r - 1);
-  //       Node nr = NodeManager::currentNM()->mkConst(r);
-  //       Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, nrMinus1));
-  //       Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, nr));
-
-  //       Node lem = NodeManager::currentNM()->mkNode(kind::OR, leq, geq);
-  //       Trace("integers") << "integers: branch & bound: " << lem << endl;
-  //       if(d_valuation.isSatLiteral(lem[0])) {
-  //         Debug("integers") << "    " << lem[0] << " == " << d_valuation.getSatValue(lem[0]) << endl;
-  //       } else {
-  //         Debug("integers") << "    " << lem[0] << " is not assigned a SAT literal" << endl;
-  //       }
-  //       if(d_valuation.isSatLiteral(lem[1])) {
-  //         Debug("integers") << "    " << lem[1] << " == " << d_valuation.getSatValue(lem[1]) << endl;
-  //       } else {
-  //         Debug("integers") << "    " << lem[1] << " is not assigned a SAT literal" << endl;
-  //       }
-  //       return lem;
-  //     } else if(i.getNumerator() > 0) {
-  //         // lemma: v <= r || v >= r + 1
-
-  //         TNode var = d_arithvarNodeMap.asNode(v);
-  //         Node nr = NodeManager::currentNM()->mkConst(r);
-  //         Node nrPlus1 = NodeManager::currentNM()->mkConst(r + 1);
-  //         Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, nr));
-  //         Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, nrPlus1));
-
-  //         Node lem = NodeManager::currentNM()->mkNode(kind::OR, leq, geq);
-  //         Trace("integers") << "integers: branch & bound: " << lem << endl;
-  //         if(d_valuation.isSatLiteral(lem[0])) {
-  //           Debug("integers") << "    " << lem[0] << " == " << d_valuation.getSatValue(lem[0]) << endl;
-  //         } else {
-  //           Debug("integers") << "    " << lem[0] << " is not assigned a SAT literal" << endl;
-  //         }
-  //         if(d_valuation.isSatLiteral(lem[1])) {
-  //           Debug("integers") << "    " << lem[1] << " == " << d_valuation.getSatValue(lem[1]) << endl;
-  //         } else {
-  //           Debug("integers") << "    " << lem[1] << " is not assigned a SAT literal" << endl;
-  //         }
-  //         ++(d_statistics.d_externalBranchAndBounds);
-  //         d_out->lemma(lem);
-  //         result = true;
-
-  //         // split only on one var
-  //         break;
-  //       } else {
-  //         Unreachable();
-  //       }
-  //     } else {
-  //       // lemma: v <= floor(r) || v >= ceil(r)
-
-  //       TNode var = d_arithvarNodeMap.asNode(v);
-  //       Node floor = NodeManager::currentNM()->mkConst(r.floor());
-  //       Node ceiling = NodeManager::currentNM()->mkConst(r.ceiling());
-  //       Node leq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, floor));
-  //       Node geq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::GEQ, var, ceiling));
-
-  //       Node lem = NodeManager::currentNM()->mkNode(kind::OR, leq, geq);
-  //       Trace("integers") << "integers: branch & bound: " << lem << endl;
-  //       if(d_valuation.isSatLiteral(lem[0])) {
-  //         Debug("integers") << "    " << lem[0] << " == " << d_valuation.getSatValue(lem[0]) << endl;
-  //       } else {
-  //         Debug("integers") << "    " << lem[0] << " is not assigned a SAT literal" << endl;
-  //       }
-  //       if(d_valuation.isSatLiteral(lem[1])) {
-  //         Debug("integers") << "    " << lem[1] << " == " << d_valuation.getSatValue(lem[1]) << endl;
-  //       } else {
-  //         Debug("integers") << "    " << lem[1] << " is not assigned a SAT literal" << endl;
-  //       }
-  //       ++(d_statistics.d_externalBranchAndBounds);
-  //       d_out->lemma(lem);
-  //       result = true;
-
-  //       // split only on one var
-  //       break;
-  //     }
-  //   }// if(arithvar is integer-typed)
-  // } while((d_nextIntegerCheckVar = (1 + d_nextIntegerCheckVar == d_variables.size() ? 0 : 1 + d_nextIntegerCheckVar)) != rrEnd);
-
-  // return result;
   }
 }
 

diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 6b14ae6ff3a74a65515ad21142d8718da42f8266..256a197cdd5e8bbc3f1320bd3e6e89aea439fdc9 100644 (file)
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -58,6 +58,10 @@ namespace arith {
 class TheoryArith : public Theory {
 private:
 
+  /**
+   * This counter is false if nothing has been done since the last cut.
+   * This is used to break an infinite loop.
+   */
   bool d_hasDoneWorkSinceCut;
 
   /**
@@ -165,7 +169,7 @@ private:
 
   Comparison mkIntegerEqualityFromAssignment(ArithVar v);
 
-  #warning "DO NOT COMMIT TO TRUNK, USE MORE EFFICIENT CHECK INSTEAD"
+  //TODO Replace with a more efficient check
   CDArithVarSet d_varsInDioSolver;
 
   /**
@@ -325,15 +329,6 @@ private:
   /** Initial (not context dependent) sets up for a new slack variable.*/
   void setupSlack(TNode left);
 
-  /**
-   * Performs *permanent* static setup for equalities that have not been
-   * preregistered.
-   * Currently these MUST be introduced by combination.
-   */
-  //void delayedSetupEquality(TNode equality);
-
-  //void delayedSetupPolynomial(TNode polynomial);
-  //void delayedSetupMonomial(const Monomial& mono);
 
   /**
    * Performs a check to see if it is definitely true that setup can be avoided.

diff --git a/src/util/options.cpp b/src/util/options.cpp
index 842bd84b2712b678d2d45022d0b44aa499da1c0e..e5f185d2413b26f3fc52d0cfc48ac5cb08fdd2a9 100644 (file)
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -96,7 +96,8 @@ Options::Options() :
   pivotRule(MINIMUM),
   arithPivotThreshold(16),
   arithPropagateMaxLength(16),
-  ufSymmetryBreaker(true)
+  ufSymmetryBreaker(true),
+  dioSolver(true)
 {
 }
 
@@ -158,6 +159,7 @@ Additional CVC4 options:\n\
    --disable-variable-removal enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\
    --disable-arithmetic-propagation turns on arithmetic propagation\n\
    --disable-symmetry-breaker turns off UF symmetry breaker (Deharbe et al., CADE 2011)\n\
+   --disable-dio-solver   turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)\n\
 ";
 
 #warning "Change CL options as --disable-variable-removal cannot do anything currently."
@@ -324,6 +326,7 @@ enum OptionValue {
   ARITHMETIC_PROPAGATION,
   ARITHMETIC_PIVOT_THRESHOLD,
   ARITHMETIC_PROP_MAX_LENGTH,
+  ARITHMETIC_DIO_SOLVER,
   DISABLE_SYMMETRY_BREAKER,
   TIME_LIMIT,
   TIME_LIMIT_PER,
@@ -405,6 +408,7 @@ static struct option cmdlineOptions[] = {
   { "random-seed" , required_argument, NULL, RANDOM_SEED  },
   { "disable-variable-removal", no_argument, NULL, ARITHMETIC_VARIABLE_REMOVAL },
   { "disable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION },
+  { "disable-dio-solver", no_argument, NULL, ARITHMETIC_DIO_SOLVER },
   { "disable-symmetry-breaker", no_argument, NULL, DISABLE_SYMMETRY_BREAKER },
   { "tlimit"     , required_argument, NULL, TIME_LIMIT  },
   { "tlimit-per" , required_argument, NULL, TIME_LIMIT_PER },
@@ -738,6 +742,10 @@ throw(OptionException) {
       arithPropagation = false;
       break;
 
+    case ARITHMETIC_DIO_SOLVER:
+      dioSolver = false;
+      break;
+
     case DISABLE_SYMMETRY_BREAKER:
       ufSymmetryBreaker = false;
       break;

diff --git a/src/util/options.h b/src/util/options.h
index 1e392e87d14e1fc4d833260630753d04d350c8c7..32d26c7503ecdd6ae0be5d938f0fbf1111ed52eb 100644 (file)
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -208,6 +208,12 @@ struct CVC4_PUBLIC Options {
    */
   bool ufSymmetryBreaker;
 
+  /**
+   * Whether to do the linear diophantine equation solver
+   * in Arith as described by Griggio JSAT 2012 (on by default).
+   */
+  bool dioSolver;
+
   Options();
 
   /**

diff --git a/test/regress/regress0/arith/integers/Makefile.am b/test/regress/regress0/arith/integers/Makefile.am
index f6d200f2a415e8bc5d5dc08de6a4add4df08abe9..ccfeb51f1bdeb335d7003352690bb6c300d44520 100644 (file)
--- a/test/regress/regress0/arith/integers/Makefile.am
+++ b/test/regress/regress0/arith/integers/Makefile.am
@@ -12,25 +12,8 @@ MAKEFLAGS = -k
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
 TESTS =        \
-       arith-int-001.cvc \
-       arith-int-002.cvc \
-       arith-int-003.cvc \
        arith-int-004.cvc \
-       arith-int-005.cvc \
-       arith-int-006.cvc \
        arith-int-007.cvc \
-       arith-int-008.cvc \
-       arith-int-009.cvc \
-       arith-int-010.cvc \
-       arith-int-011.cvc \
-       arith-int-014.cvc \
-       arith-int-015.cvc \
-       arith-int-016.cvc \
-       arith-int-017.cvc \
-       arith-int-018.cvc \
-       arith-int-019.cvc 
-
-EXTRA_DIST = $(TESTS) \
        arith-int-012.cvc \
        arith-int-013.cvc \
        arith-int-022.cvc \
@@ -39,13 +22,32 @@ EXTRA_DIST = $(TESTS) \
        arith-int-042.cvc \
        arith-int-042.min.cvc \
        arith-int-047.cvc \
-       arith-int-048.cvc \
        arith-int-050.cvc \
        arith-int-082.cvc \
        arith-int-084.cvc \
        arith-int-085.cvc \
-       arith-int-097.cvc \
-               arith-int-020.cvc \
+       arith-int-097.cvc
+
+#failing tests
+#      arith-int-048.cvc
+
+EXTRA_DIST = $(TESTS) \
+       arith-int-001.cvc \
+       arith-int-002.cvc \
+       arith-int-003.cvc \
+       arith-int-005.cvc \
+       arith-int-006.cvc \
+       arith-int-008.cvc \
+       arith-int-009.cvc \
+       arith-int-010.cvc \
+       arith-int-011.cvc \
+       arith-int-014.cvc \
+       arith-int-015.cvc \
+       arith-int-016.cvc \
+       arith-int-017.cvc \
+       arith-int-018.cvc \
+       arith-int-019.cvc \
+       arith-int-020.cvc \
        arith-int-021.cvc \
        arith-int-023.cvc \
        arith-int-025.cvc \
@@ -115,7 +117,6 @@ EXTRA_DIST = $(TESTS) \
        arith-int-098.cvc \
        arith-int-099.cvc \
        arith-int-100.cvc
-       
 
 #if CVC4_BUILD_PROFILE_COMPETITION
 #else