From 94decb8503be1fcc894094a0f2656e25d8aef251 Mon Sep 17 00:00:00 2001 From: Tim King Date: Wed, 1 May 2013 14:59:39 -0400 Subject: [PATCH] Working on the new explanation system. --- src/theory/arith/constraint.cpp | 22 +++++ src/theory/arith/constraint.h | 2 + src/theory/arith/linear_equality.cpp | 7 +- src/theory/arith/linear_equality.h | 2 +- src/theory/arith/options | 3 + src/theory/arith/theory_arith_private.cpp | 101 ++++++++++++++++------ 6 files changed, 104 insertions(+), 33 deletions(-) diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index e26687bf1..78b9d3494 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -922,6 +922,28 @@ bool ConstraintValue::proofIsEmpty() const{ return result; } +Node ConstraintValue::makeImplication(const std::vector& b) const{ + Node antecedent = makeConjunction(b); + Node implied = getLiteral(); + return antecedent.impNode(implied); +} + + +Node ConstraintValue::makeConjunction(const std::vector& b){ + NodeBuilder<> nb(kind::AND); + for(vector::const_iterator i = b.begin(), end = b.end(); i != end; ++i){ + Constraint b_i = *i; + b_i->explainBefore(nb, AssertionOrderSentinel); + } + if(nb.getNumChildren() >= 2){ + return nb; + }else if(nb.getNumChildren() == 1){ + return nb[0]; + }else{ + return mkBoolNode(true); + } +} + void ConstraintValue::explainBefore(NodeBuilder<>& nb, AssertionOrder order) const{ Assert(hasProof()); Assert(!isSelfExplaining() || assertedToTheTheory()); diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index a5d64a652..4966115d2 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -598,6 +598,8 @@ public: void impliedBy(Constraint a, Constraint b); void impliedBy(const std::vector& b); + Node makeImplication(const std::vector& b) const; + static Node makeConjunction(const std::vector& b); /** The node must have a proof already and be eligible for propagation! */ void propagate(); diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index 4779b1012..bde771102 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -581,7 +581,7 @@ void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c){ << basic << ") done" << endl; } -void LinearEqualityModule::propagateRow(RowIndex ridx, bool rowUp, Constraint c){ +void LinearEqualityModule::propagateRow(vector& into, RowIndex ridx, bool rowUp, Constraint c){ Assert(!c->assertedToTheTheory()); Assert(c->canBePropagated()); Assert(!c->hasProof()); @@ -589,7 +589,7 @@ void LinearEqualityModule::propagateRow(RowIndex ridx, bool rowUp, Constraint c) ArithVar v = c->getVariable(); Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics(" << v <<") start" << endl; - vector bounds; + //vector bounds; Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx); for(; !iter.atEnd(); ++iter){ @@ -608,9 +608,8 @@ void LinearEqualityModule::propagateRow(RowIndex ridx, bool rowUp, Constraint c) Assert(bound != NullConstraint); Debug("arith::explainNonbasics") << "explainNonbasics" << bound << " for " << c << endl; - bounds.push_back(bound); + into.push_back(bound); } - c->impliedBy(bounds); Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics(" << v << ") done" << endl; } diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index 767c09340..b1f3d00d7 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -431,7 +431,7 @@ public: * Exports either the explanation of an upperbound or a lower bound * of the basic variable basic, using the non-basic variables in the row. */ - void propagateRow(RowIndex ridx, bool rowUp, Constraint c); + void propagateRow(std::vector& into, RowIndex ridx, bool rowUp, Constraint c); /** * Computes the value of a basic variable using the assignments diff --git a/src/theory/arith/options b/src/theory/arith/options index cf0782a92..1366addae 100644 --- a/src/theory/arith/options +++ b/src/theory/arith/options @@ -94,4 +94,7 @@ option exportDioDecompositions --dio-decomps bool :default false :read-write option newProp --new-prop bool :default false :read-write Use the new row propagation system +option arithPropAsLemmaLength --arith-prop-clauses int :default 8 :read-write + Rows shorter than this are propagated as clauses + endmodule diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index c71f2a6bd..31b6cd032 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -116,6 +116,7 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context d_cutInContext(c), d_statistics() { + srand(79); } TheoryArithPrivate::~TheoryArithPrivate(){ } @@ -2548,18 +2549,21 @@ bool TheoryArithPrivate::propagateCandidateBound(ArithVar basic, bool upperBound } // I think this can be skipped if canBePropagated is true //d_learnedBounds.push(bestImplied); - cout << "success " << bestImplied << endl; - d_partialModel.printModel(basic, cout); - + if(Debug.isOn("arith::prop")){ + Debug("arith::prop") << "success " << bestImplied << endl; + d_partialModel.printModel(basic, Debug("arith::prop")); + } return true; } - cout << "failed " << basic << " " << bound << assertedToTheTheory << " " << - canBePropagated << " " << hasProof << endl; - d_partialModel.printModel(basic, cout); + if(Debug.isOn("arith::prop")){ + Debug("arith::prop") << "failed " << basic << " " << bound << assertedToTheTheory << " " << + canBePropagated << " " << hasProof << endl; + d_partialModel.printModel(basic, Debug("arith::prop")); + } } - }else{ - cout << "false " << bound << " "; - d_partialModel.printModel(basic, cout); + }else if(Debug.isOn("arith::prop")){ + Debug("arith::prop") << "false " << bound << " "; + d_partialModel.printModel(basic, Debug("arith::prop")); } return false; } @@ -2580,7 +2584,7 @@ void TheoryArithPrivate::propagateCandidate(ArithVar basic){ void TheoryArithPrivate::propagateCandidates(){ TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime); - cout << "propagateCandidates begin" << endl; + Debug("arith::prop") << "propagateCandidates begin" << endl; Assert(d_candidateBasics.empty()); @@ -2615,7 +2619,7 @@ void TheoryArithPrivate::propagateCandidates(){ Assert(d_tableau.isBasic(candidate)); propagateCandidate(candidate); } - cout << "propagateCandidates end" << endl << endl << endl; + Debug("arith::prop") << "propagateCandidates end" << endl << endl << endl; } void TheoryArithPrivate::propagateCandidatesNew(){ @@ -2634,7 +2638,7 @@ void TheoryArithPrivate::propagateCandidatesNew(){ */ TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime); - cout << "propagateCandidatesNew begin" << endl; + Debug("arith::prop") << "propagateCandidatesNew begin" << endl; Assert(d_qflraStatus == Result::SAT); if(d_updatedBounds.empty()){ return; } @@ -2651,7 +2655,7 @@ void TheoryArithPrivate::propagateCandidatesNew(){ d_candidateRows.pop_back(); propagateCandidateRow(candidate); } - cout << "propagateCandidatesNew end" << endl << endl << endl; + Debug("arith::prop") << "propagateCandidatesNew end" << endl << endl << endl; } bool TheoryArithPrivate::propagateMightSucceed(ArithVar v, bool ub) const{ @@ -2678,7 +2682,7 @@ bool TheoryArithPrivate::propagateMightSucceed(ArithVar v, bool ub) const{ } bool TheoryArithPrivate::attemptSingleton(RowIndex ridx, bool rowUp){ - cout << " attemptSingleton" << ridx; + Debug("arith::prop") << " attemptSingleton" << ridx; const Tableau::Entry* ep; ep = d_linEq.rowLacksBound(ridx, rowUp, ARITHVAR_SENTINEL); @@ -2698,8 +2702,8 @@ bool TheoryArithPrivate::attemptSingleton(RowIndex ridx, bool rowUp){ // if c < 0, v \geq -D/c so !vUp bool vUp = (rowUp == ( coeff.sgn() < 0)); - cout << " " << rowUp << " " << v << " " << coeff << " " << vUp << endl; - cout << " " << propagateMightSucceed(v, vUp) << endl; + Debug("arith::prop") << " " << rowUp << " " << v << " " << coeff << " " << vUp << endl; + Debug("arith::prop") << " " << propagateMightSucceed(v, vUp) << endl; if(propagateMightSucceed(v, vUp)){ DeltaRational dr = d_linEq.computeRowBound(ridx, rowUp, v); @@ -2710,7 +2714,7 @@ bool TheoryArithPrivate::attemptSingleton(RowIndex ridx, bool rowUp){ } bool TheoryArithPrivate::attemptFull(RowIndex ridx, bool rowUp){ - cout << " attemptFull" << ridx << endl; + Debug("arith::prop") << " attemptFull" << ridx << endl; vector candidates; @@ -2746,11 +2750,6 @@ bool TheoryArithPrivate::attemptFull(RowIndex ridx, bool rowUp){ DeltaRational impliedBound = (slack - contribution)/(-c); bool success = tryToPropagate(ridx, rowUp, v, vUb, impliedBound); - if(success){ - cout << " success " << v << endl; - }else{ - cout << " fail " << v << endl; - } any |= success; } return any; @@ -2770,6 +2769,30 @@ bool TheoryArithPrivate::tryToPropagate(RowIndex ridx, bool rowUp, ArithVar v, b return false; } +Node flattenImplication(Node imp){ + NodeBuilder<> nb(kind::OR); + Node left = imp[0]; + Node right = imp[1]; + + if(left.getKind() == kind::AND){ + for(Node::iterator i = left.begin(), iend = left.end(); i != iend; ++i) { + nb << (*i).negate(); + } + }else{ + nb << left.negate(); + } + + if(right.getKind() == kind::OR){ + for(Node::iterator i = right.begin(), iend = right.end(); i != iend; ++i) { + nb << *i; + } + }else{ + nb << right; + } + + return nb; +} + bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, Constraint implied){ Assert(implied != NullConstraint); ArithVar v = implied->getVariable(); @@ -2791,15 +2814,33 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C } if(!assertedToTheTheory && canBePropagated && !hasProof ){ - d_linEq.propagateRow(ridx, rowUp, implied); + vector explain; + d_linEq.propagateRow(explain, ridx, rowUp, implied); + if(d_tableau.getRowLength(ridx) <= options::arithPropAsLemmaLength()){ + Node implication = implied->makeImplication(explain); + Node clause = flattenImplication(implication); + outputLemma(clause); + }else{ + implied->impliedBy(explain); + } return true; } - cout << "failed " << v << " " << assertedToTheTheory << " " << - canBePropagated << " " << hasProof << " " << implied << endl; - d_partialModel.printModel(v, cout); + + if(Debug.isOn("arith::prop")){ + Debug("arith::prop") + << "failed " << v << " " << assertedToTheTheory << " " + << canBePropagated << " " << hasProof << " " << implied << endl; + d_partialModel.printModel(v, Debug("arith::prop")); + } return false; } +double fRand(double fMin, double fMax) +{ + double f = (double)rand() / RAND_MAX; + return fMin + f * (fMax - fMin); +} + bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx){ BoundCounts hasCount = d_linEq.hasBoundCount(ridx); uint32_t rowLength = d_tableau.getRowLength(ridx); @@ -2807,10 +2848,14 @@ bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx){ bool success = false; static int instance = 0; ++instance; - cout << "propagateCandidateRow " << instance << " attempt " << rowLength << " " << hasCount << endl; + + Debug("arith::prop") + << "propagateCandidateRow " << instance << " attempt " << rowLength << " " << hasCount << endl; if(rowLength >= options::arithPropagateMaxLength()){ - return false; + if(fRand(0.0,1.0) >= double(options::arithPropagateMaxLength())/rowLength){ + return false; + } } if(hasCount.lowerBoundCount() == rowLength){ -- 2.30.2