diff options
| -rw-r--r-- | src/theory/arith/dio_solver.cpp | 8 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith.cpp | 172 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith.h | 15 | ||||
| -rw-r--r-- | src/util/options.cpp | 10 | ||||
| -rw-r--r-- | src/util/options.h | 6 | ||||
| -rw-r--r-- | test/regress/regress0/arith/integers/Makefile.am | 43 |
6 files changed, 48 insertions, 206 deletions
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index dead34807..1e47d6cdd 100644 --- 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 824bb59ed..64e713b0a 100644 --- 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 6b14ae6ff..256a197cd 100644 --- 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 842bd84b2..e5f185d24 100644 --- 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 1e392e87d..32d26c750 100644 --- 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 f6d200f2a..ccfeb51f1 100644 --- 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 |