From ebcdf229513341d7c0636e0e7171e916ce56d536 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Tue, 4 Feb 2020 10:31:03 -0800 Subject: [PATCH] Articulate proof-related debug statements in arith (#3700) --- src/theory/arith/constraint.cpp | 56 ++++++++++++++++++++--- src/theory/arith/constraint.h | 2 + src/theory/arith/theory_arith_private.cpp | 46 ++++++++++++++++--- src/theory/arith/theory_arith_private.h | 5 +- 4 files changed, 95 insertions(+), 14 deletions(-) diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index e7b1289a4..20405d359 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -526,6 +526,50 @@ bool Constraint::hasTrichotomyProof() const { return getProofType() == TrichotomyAP; } +void Constraint::printProofTree(std::ostream& out, size_t depth) const +{ +#if IS_PROOFS_BUILD + const ConstraintRule& rule = getConstraintRule(); + out << std::string(2 * depth, ' ') << "* " << getVariable() << " ["; + if (hasLiteral()) + { + out << getLiteral(); + } + else + { + out << "NOLIT"; + }; + out << "]" << ' ' << getType() << ' ' << getValue() << " (" << getProofType() + << ")"; + if (getProofType() == FarkasAP) + { + out << " ["; + bool first = true; + for (const auto& coeff : *rule.d_farkasCoefficients) + { + if (not first) + { + out << ", "; + } + first = false; + out << coeff; + } + out << "]"; + } + out << endl; + + for (AntecedentId i = rule.d_antecedentEnd; i != AntecedentIdSentinel; --i) { + ConstraintCP antecdent = d_database->getAntecedent(i); + if (antecdent == NullConstraint) { + break; + } + antecdent->printProofTree(out, depth + 1); + } +#else /* IS_PROOFS_BUILD */ + out << "Cannot print proof. This is not a proof build." << endl; +#endif /* IS_PROOFS_BUILD */ +} + bool Constraint::sanityChecking(Node n) const { Comparison cmp = Comparison::parseNormalForm(n); Kind k = cmp.comparisonKind(); @@ -1361,7 +1405,7 @@ Node Constraint::externalExplainByAssertions(const ConstraintCPVec& b){ } Node Constraint::externalExplainConflict() const{ - Debug("pf::arith") << this << std::endl; + Debug("pf::arith::explain") << this << std::endl; Assert(inConflict()); NodeBuilder<> nb(kind::AND); externalExplainByAssertions(nb); @@ -1431,11 +1475,11 @@ void Constraint::externalExplain(NodeBuilder<>& nb, AssertionOrder order) const{ Assert(!isAssumption() || assertedToTheTheory()); Assert(!isInternalAssumption()); - if (Debug.isOn("pf::arith")) + if (Debug.isOn("pf::arith::explain")) { - Debug("pf::arith") << "Explaining: " << this << " with rule "; - getConstraintRule().print(Debug("pf::arith")); - Debug("pf::arith") << std::endl; + Debug("pf::arith::explain") << "Explaining: " << this << " with rule "; + getConstraintRule().print(Debug("pf::arith::explain")); + Debug("pf::arith::explain") << std::endl; } if(assertedBefore(order)){ @@ -1448,7 +1492,7 @@ void Constraint::externalExplain(NodeBuilder<>& nb, AssertionOrder order) const{ ConstraintCP antecedent = d_database->d_antecedents[p]; while(antecedent != NullConstraint){ - Debug("pf::arith") << "Explain " << antecedent << std::endl; + Debug("pf::arith::explain") << "Explain " << antecedent << std::endl; antecedent->externalExplain(nb, order); --p; antecedent = d_database->d_antecedents[p]; diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index f2c0c4b02..61b999a25 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -517,6 +517,8 @@ class Constraint { /** Returns true if the node has a trichotomy proof. */ bool hasTrichotomyProof() const; + void printProofTree(std::ostream & out, size_t depth = 0) const; + /** * A sets the constraint to be an internal assumption. * diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 2b8ce922d..76d8dbc01 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1194,7 +1194,7 @@ Node TheoryArithPrivate::ppRewriteTerms(TNode n) { // 0 <= n[0] - toIntSkolem < 1 Node one = mkRationalNode(1); Node lem = mkAxiomForTotalIntDivision(n[0], one, toIntSkolem); - d_containing.d_out->lemma(lem); + outputLemma(lem); }else{ toIntSkolem = (*it).second; } @@ -1247,7 +1247,7 @@ Node TheoryArithPrivate::ppRewriteTerms(TNode n) { nm->mkNode(kind::LT, num, nm->mkNode(kind::MULT, den, nm->mkNode(kind::PLUS, intVar, nm->mkConst(Rational(-1)))))))); } if( !lem.isNull() ){ - d_containing.d_out->lemma(lem); + outputLemma(lem); } }else{ intVar = (*it).second; @@ -1270,7 +1270,7 @@ Node TheoryArithPrivate::ppRewriteTerms(TNode n) { if( it==d_div_skolem.end() ){ var = nm->mkSkolem("nonlinearDiv", nm->realType(), "the result of a non-linear div term"); d_div_skolem[rw] = var; - d_containing.d_out->lemma(nm->mkNode(kind::IMPLIES, den.eqNode(nm->mkConst(Rational(0))).negate(), nm->mkNode(kind::MULT, den, var).eqNode(num))); + outputLemma(nm->mkNode(kind::IMPLIES, den.eqNode(nm->mkConst(Rational(0))).negate(), nm->mkNode(kind::MULT, den, var).eqNode(num))); }else{ var = (*it).second; } @@ -2017,6 +2017,10 @@ bool TheoryArithPrivate::assertionCases(ConstraintP constraint){ ConstraintP floorConstraint = constraint->getFloor(); if(!floorConstraint->isTrue()){ bool inConflict = floorConstraint->negationHasProof(); + if (Debug.isOn("arith::intbound")) { + Debug("arith::intbound") << "literal, before: " << constraint->getLiteral() << std::endl; + Debug("arith::intbound") << "constraint, after: " << floorConstraint << std::endl; + } floorConstraint->impliedByIntHole(constraint, inConflict); floorConstraint->tryToPropagate(); if(inConflict){ @@ -2033,6 +2037,10 @@ bool TheoryArithPrivate::assertionCases(ConstraintP constraint){ ConstraintP ceilingConstraint = constraint->getCeiling(); if(!ceilingConstraint->isTrue()){ bool inConflict = ceilingConstraint->negationHasProof(); + if (Debug.isOn("arith::intbound")) { + Debug("arith::intbound") << "literal, before: " << constraint->getLiteral() << std::endl; + Debug("arith::intbound") << "constraint, after: " << ceilingConstraint << std::endl; + } ceilingConstraint->impliedByIntHole(constraint, inConflict); ceilingConstraint->tryToPropagate(); if(inConflict){ @@ -2172,6 +2180,11 @@ void TheoryArithPrivate::outputConflicts(){ << conflict[conflict.getNumChildren() - i - 1]; } + if (Debug.isOn("arith::pf::tree")) { + confConstraint->printProofTree(Debug("arith::pf::tree")); + confConstraint->getNegation()->printProofTree(Debug("arith::pf::tree")); + } + Assert(conflict.getNumChildren() == pf.d_farkasCoefficients->size()); d_containing.d_proofRecorder->saveFarkasCoefficients( conflictInFarkasCoefficientOrder, pf.d_farkasCoefficients); @@ -2181,7 +2194,7 @@ void TheoryArithPrivate::outputConflicts(){ Debug("arith::conflict") << "(normalized to) " << conflict << endl; } - (d_containing.d_out)->conflict(conflict); + outputConflict(conflict); } } if(!d_blackBoxConflict.get().isNull()){ @@ -2195,15 +2208,30 @@ void TheoryArithPrivate::outputConflicts(){ Debug("arith::conflict") << "(normalized to) " << bb << endl; } - (d_containing.d_out)->conflict(bb); + outputConflict(bb); } } void TheoryArithPrivate::outputLemma(TNode lem) { - Debug("arith::lemma") << "Arith Lemma: " << lem << std::endl; + Debug("arith::channel") << "Arith lemma: " << lem << std::endl; (d_containing.d_out)->lemma(lem); } +void TheoryArithPrivate::outputConflict(TNode lit) { + Debug("arith::channel") << "Arith conflict: " << lit << std::endl; + (d_containing.d_out)->conflict(lit); +} + +void TheoryArithPrivate::outputPropagate(TNode lit) { + Debug("arith::channel") << "Arith propagation: " << lit << std::endl; + (d_containing.d_out)->propagate(lit); +} + +void TheoryArithPrivate::outputRestart() { + Debug("arith::channel") << "Arith restart!" << std::endl; + (d_containing.d_out)->demandRestart(); +} + // void TheoryArithPrivate::branchVector(const std::vector& lemmas){ // //output the lemmas // for(vector::const_iterator i = lemmas.begin(); i != lemmas.end(); @@ -4889,6 +4917,12 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C // * coeffs[i+1] is for explain[i] d_linEq.propagateRow(explain, ridx, rowUp, implied, coeffs); if(d_tableau.getRowLength(ridx) <= options::arithPropAsLemmaLength()){ + if (Debug.isOn("arith::prop::pf")) { + for (const auto & constraint : explain) { + Assert(constraint->hasProof()); + constraint->printProofTree(Debug("arith::prop::pf")); + } + } Node implication = implied->externalImplication(explain); Node clause = flattenImplication(implication); PROOF(if (d_containing.d_proofRecorder diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 3f46ddd59..f964c4e04 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -655,8 +655,9 @@ private: d_nlIncomplete = true; } void outputLemma(TNode lem); - inline void outputPropagate(TNode lit) { (d_containing.d_out)->propagate(lit); } - inline void outputRestart() { (d_containing.d_out)->demandRestart(); } + void outputConflict(TNode lit); + void outputPropagate(TNode lit); + void outputRestart(); inline bool isSatLiteral(TNode l) const { return (d_containing.d_valuation).isSatLiteral(l); -- 2.30.2