From 3d1c57e0506b2454aa815c3c1cb634d96ade1d7c Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 4 May 2012 03:03:34 +0000 Subject: [PATCH] - 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. --- src/theory/arith/constraint.cpp | 5 +- src/theory/arith/constraint.h | 11 +++- src/theory/arith/linear_equality.cpp | 16 +---- src/theory/arith/simplex.cpp | 21 +++++-- src/theory/arith/simplex.h | 2 + src/theory/arith/theory_arith.cpp | 88 ++++++++++++---------------- src/theory/arith/theory_arith.h | 1 + 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 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() != 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. -- 2.30.2