From f179953e2fea6955650ccde8414f2ccd8ee6f63b Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Thu, 3 Jan 2019 15:39:35 +0100 Subject: [LRA proof] Recording & Printing LRA Proofs (#2758) * [LRA proof] Recording & Printing LRA Proofs Now we use the ArithProofRecorder to record and later print arithmetic proofs. If an LRA lemma can be proven by a single farkas proof, then that is done. Otherwise, we `trust` the lemma. I haven't **really** enabled LRA proofs yet, so `--check-proofs` still is a no-op for LRA. To test, do ``` lfsccvc4 <(./bin/cvc4 --dump-proofs ../test/regress/regress0/lemmas/mode_cntrl.induction.smt | tail -n +2) ``` where `lfsccvc4` is an alias invoking `lfscc` with all the necessary signatures. On my machine that is: ``` alias lfsccvc4="/home/aozdemir/repos/LFSC/build/src/lfscc \ /home/aozdemir/repos/CVC4/proofs/signatures/sat.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/smt.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/lrat.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_base.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_bv.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_bv_bitblast.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_arrays.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_int.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_quant.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_real.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_real.plf" ``` * Added guards to proof recording Also reverted some small, unintentional changes. Also had to add printing for STRING_SUBSTR?? * Responding to Yoni's review * SimpleFarkasProof examples * Respond to Aina's comments * Reorder Constraint declarations * fix build * Moved friend declaration in Constraint * Trichotomy example * Lift getNumChildren invocation in PLUS case Credits to aina for spotting it. * Clang-format --- src/printer/cvc/cvc_printer.cpp | 1 + src/proof/arith_proof.cpp | 577 +++++++++++++++++++++++------- src/proof/arith_proof.h | 72 +++- src/proof/arith_proof_recorder.cpp | 14 +- src/theory/arith/constraint.cpp | 47 ++- src/theory/arith/constraint.h | 424 +++++++++++----------- src/theory/arith/theory_arith_private.cpp | 65 +++- 7 files changed, 862 insertions(+), 338 deletions(-) diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 6fa7eadeb..e6ff02f10 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -917,6 +917,7 @@ void CvcPrinter::toStream( case kind::STRING_LENGTH: out << "LENGTH"; break; + case kind::STRING_SUBSTR: out << "SUBSTR"; break; default: Warning() << "Kind printing not implemented for the case of " << n.getKind() << endl; diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp index 1d51f99e1..0d2bb5be0 100644 --- a/src/proof/arith_proof.cpp +++ b/src/proof/arith_proof.cpp @@ -19,10 +19,14 @@ #include #include +#include "expr/node.h" #include "proof/proof_manager.h" #include "proof/theory_proof.h" +#include "theory/arith/constraint_forward.h" #include "theory/arith/theory_arith.h" +#define CVC4_ARITH_VAR_TERM_PREFIX "term." + namespace CVC4 { inline static Node eqNode(TNode n1, TNode n2) { @@ -674,151 +678,169 @@ void LFSCArithProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetM // !d_realMode <--> term.getType().isInteger() Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARITH); - switch (term.getKind()) { + switch (term.getKind()) + { + case kind::CONST_RATIONAL: + { + Assert(term.getNumChildren() == 0); + Assert(term.getType().isInteger() || term.getType().isReal()); - case kind::CONST_RATIONAL: { - Assert (term.getNumChildren() == 0); - Assert (term.getType().isInteger() || term.getType().isReal()); + const Rational& r = term.getConst(); + bool neg = (r < 0); - const Rational& r = term.getConst(); - bool neg = (r < 0); + os << (!d_realMode ? "(a_int " : "(a_real "); - os << (!d_realMode ? "(a_int " : "(a_real "); + if (neg) + { + os << "(~ "; + } - if (neg) { - os << "(~ "; - } + if (!d_realMode) + { + os << r.abs(); + } + else + { + printRational(os, r.abs()); + } - if (!d_realMode) { - os << r.abs(); - } else { - os << r.abs().getNumerator(); - os << "/"; - os << r.getDenominator(); + if (neg) + { + os << ") "; + } + + os << ") "; + return; } - if (neg) { + case kind::UMINUS: + { + Assert(term.getNumChildren() == 1); + Assert(term.getType().isInteger() || term.getType().isReal()); + os << (!d_realMode ? "(u-_Int " : "(u-_Real "); + d_proofEngine->printBoundTerm(term[0], os, map); os << ") "; + return; } - os << ") "; - return; - } + case kind::PLUS: + { + Assert(term.getNumChildren() >= 2); - case kind::UMINUS: { - Assert (term.getNumChildren() == 1); - Assert (term.getType().isInteger() || term.getType().isReal()); - os << (!d_realMode ? "(u-_Int " : "(u-_Real "); - d_proofEngine->printBoundTerm(term[0], os, map); - os << ") "; - return; - } + std::stringstream paren; + for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) + { + os << (!d_realMode ? "(+_Int " : "(+_Real "); + d_proofEngine->printBoundTerm(term[i], os, map); + os << " "; + paren << ") "; + } - case kind::PLUS: { - Assert (term.getNumChildren() >= 2); + d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map); + os << paren.str(); + return; + } - std::stringstream paren; - for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) { - os << (!d_realMode ? "(+_Int " : "(+_Real "); - d_proofEngine->printBoundTerm(term[i], os, map); - os << " "; - paren << ") "; + case kind::MINUS: + { + Assert(term.getNumChildren() >= 2); + + std::stringstream paren; + for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) + { + os << (!d_realMode ? "(-_Int " : "(-_Real "); + d_proofEngine->printBoundTerm(term[i], os, map); + os << " "; + paren << ") "; + } + + d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map); + os << paren.str(); + return; } - d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map); - os << paren.str(); - return; - } + case kind::MULT: + { + Assert(term.getNumChildren() >= 2); - case kind::MINUS: { - Assert (term.getNumChildren() >= 2); + std::stringstream paren; + for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) + { + os << (!d_realMode ? "(*_Int " : "(*_Real "); + d_proofEngine->printBoundTerm(term[i], os, map); + os << " "; + paren << ") "; + } - std::stringstream paren; - for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) { - os << (!d_realMode ? "(-_Int " : "(-_Real "); - d_proofEngine->printBoundTerm(term[i], os, map); - os << " "; - paren << ") "; + d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map); + os << paren.str(); + return; } - d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map); - os << paren.str(); - return; - } + case kind::DIVISION: + case kind::DIVISION_TOTAL: + { + Assert(term.getNumChildren() >= 2); - case kind::MULT: { - Assert (term.getNumChildren() >= 2); + std::stringstream paren; + for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) + { + os << (!d_realMode ? "(/_Int " : "(/_Real "); + d_proofEngine->printBoundTerm(term[i], os, map); + os << " "; + paren << ") "; + } - std::stringstream paren; - for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) { - os << (!d_realMode ? "(*_Int " : "(*_Real "); - d_proofEngine->printBoundTerm(term[i], os, map); - os << " "; - paren << ") "; + d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map); + os << paren.str(); + return; } - d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map); - os << paren.str(); - return; - } + case kind::GT: + Assert(term.getNumChildren() == 2); + os << (!d_realMode ? "(>_Int " : "(>_Real "); + d_proofEngine->printBoundTerm(term[0], os, map); + os << " "; + d_proofEngine->printBoundTerm(term[1], os, map); + os << ") "; + return; - case kind::DIVISION: - case kind::DIVISION_TOTAL: { - Assert (term.getNumChildren() >= 2); + case kind::GEQ: + Assert(term.getNumChildren() == 2); + os << (!d_realMode ? "(>=_Int " : "(>=_Real "); + d_proofEngine->printBoundTerm(term[0], os, map); + os << " "; + d_proofEngine->printBoundTerm(term[1], os, map); + os << ") "; + return; - std::stringstream paren; - for (unsigned i = 0; i < term.getNumChildren() - 1; ++i) { - os << (!d_realMode ? "(/_Int " : "(/_Real "); - d_proofEngine->printBoundTerm(term[i], os, map); + case kind::LT: + Assert(term.getNumChildren() == 2); + os << (!d_realMode ? "(<_Int " : "(<_Real "); + d_proofEngine->printBoundTerm(term[0], os, map); os << " "; - paren << ") "; - } + d_proofEngine->printBoundTerm(term[1], os, map); + os << ") "; + return; - d_proofEngine->printBoundTerm(term[term.getNumChildren() - 1], os, map); - os << paren.str(); - return; - } + case kind::LEQ: + Assert(term.getNumChildren() == 2); + os << (!d_realMode ? "(<=_Int " : "(<=_Real "); + d_proofEngine->printBoundTerm(term[0], os, map); + os << " "; + d_proofEngine->printBoundTerm(term[1], os, map); + os << ") "; + return; - case kind::GT: - Assert (term.getNumChildren() == 2); - os << (!d_realMode ? "(>_Int " : "(>_Real "); - d_proofEngine->printBoundTerm(term[0], os, map); - os << " "; - d_proofEngine->printBoundTerm(term[1], os, map); - os << ") "; - return; - - case kind::GEQ: - Assert (term.getNumChildren() == 2); - os << (!d_realMode ? "(>=_Int " : "(>=_Real "); - d_proofEngine->printBoundTerm(term[0], os, map); - os << " "; - d_proofEngine->printBoundTerm(term[1], os, map); - os << ") "; - return; - - case kind::LT: - Assert (term.getNumChildren() == 2); - os << (!d_realMode ? "(<_Int " : "(<_Real "); - d_proofEngine->printBoundTerm(term[0], os, map); - os << " "; - d_proofEngine->printBoundTerm(term[1], os, map); - os << ") "; - return; - - case kind::LEQ: - Assert (term.getNumChildren() == 2); - os << (!d_realMode ? "(<=_Int " : "(<=_Real "); - d_proofEngine->printBoundTerm(term[0], os, map); - os << " "; - d_proofEngine->printBoundTerm(term[1], os, map); - os << ") "; - return; + case kind::VARIABLE: + case kind::SKOLEM: + os << CVC4_ARITH_VAR_TERM_PREFIX << ProofManager::sanitize(term); + return; - default: - Debug("pf::arith") << "Default printing of term: " << term << std::endl; - os << term; - return; + default: + Debug("pf::arith") << "Default printing of term: " << term << std::endl; + os << term; + return; } } @@ -833,26 +855,327 @@ void LFSCArithProof::printOwnedSort(Type type, std::ostream& os) { } } -void LFSCArithProof::printTheoryLemmaProof(std::vector& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) { - os << " ;; Arith Theory Lemma \n;;"; - for (unsigned i = 0; i < lemma.size(); ++i) { - os << lemma[i] <<" "; +void LFSCArithProof::printRational(std::ostream& o, const Rational& r) +{ + if (r.sgn() < 0) + { + o << "(~ " << r.getNumerator().abs() << "/" << r.getDenominator().abs() + << ")"; + } + else + { + o << r.getNumerator() << "/" << r.getDenominator(); + } +} + +void LFSCArithProof::printLinearPolynomialNormalizer(std::ostream& o, + const Node& n) +{ + switch (n.getKind()) + { + case kind::PLUS: + { + // Since our axioms are binary, but n may be n-ary, we rig up + // a right-associative tree. + size_t nchildren = n.getNumChildren(); + for (size_t i = 0; i < nchildren; ++i) + { + if (i < nchildren - 1) + { + o << "\n (pn_+ _ _ _ _ _ "; + } + printLinearMonomialNormalizer(o, n[i]); + } + std::fill_n(std::ostream_iterator(o), nchildren - 1, ')'); + break; + } + case kind::MULT: + case kind::VARIABLE: + case kind::CONST_RATIONAL: + case kind::SKOLEM: + { + printLinearMonomialNormalizer(o, n); + break; + } + default: +#ifdef CVC4_ASSERTIONS + std::ostringstream msg; + msg << "Invalid operation " << n.getKind() << " in linear polynomial"; + Unreachable(msg.str().c_str()); +#endif // CVC4_ASSERTIONS + break; + } +} + +void LFSCArithProof::printLinearMonomialNormalizer(std::ostream& o, + const Node& n) +{ + switch (n.getKind()) + { + case kind::MULT: { +#ifdef CVC4_ASSERTIONS + std::ostringstream s; + s << "node " << n << " is not a linear monomial"; + s << " " << n[0].getKind() << " " << n[1].getKind(); + Assert((n[0].getKind() == kind::CONST_RATIONAL + && (n[1].getKind() == kind::VARIABLE + || n[1].getKind() == kind::SKOLEM)), + s.str().c_str()); +#endif // CVC4_ASSERTIONS + + o << "\n (pn_mul_c_L _ _ _ "; + printConstRational(o, n[0]); + o << " "; + printVariableNormalizer(o, n[1]); + o << ")"; + break; + } + case kind::CONST_RATIONAL: + { + o << "\n (pn_const "; + printConstRational(o, n); + o << ")"; + break; + } + case kind::VARIABLE: + case kind::SKOLEM: + { + o << "\n "; + printVariableNormalizer(o, n); + break; + } + default: +#ifdef CVC4_ASSERTIONS + std::ostringstream msg; + msg << "Invalid operation " << n.getKind() << " in linear monomial"; + Unreachable(msg.str().c_str()); +#endif // CVC4_ASSERTIONS + break; + } +} + +void LFSCArithProof::printConstRational(std::ostream& o, const Node& n) +{ + Assert(n.getKind() == kind::CONST_RATIONAL); + const Rational value = n.getConst(); + printRational(o, value); +} + +void LFSCArithProof::printVariableNormalizer(std::ostream& o, const Node& n) +{ + std::ostringstream msg; + msg << "Invalid variable kind " << n.getKind() << " in linear monomial"; + Assert(n.getKind() == kind::VARIABLE || n.getKind() == kind::SKOLEM, + msg.str().c_str()); + o << "(pn_var " << n << ")"; +} + +void LFSCArithProof::printLinearPolynomialPredicateNormalizer(std::ostream& o, + const Node& n) +{ + Assert(n.getKind() == kind::GEQ, + "can only print normalization witnesses for (>=) nodes"); + Assert(n[1].getKind() == kind::CONST_RATIONAL); + o << "(poly_formula_norm_>= _ _ _ "; + o << "\n (pn_- _ _ _ _ _ "; + printLinearPolynomialNormalizer(o, n[0]); + o << "\n (pn_const "; + printConstRational(o, n[1]); + o << ")))"; +} + +void LFSCArithProof::printTheoryLemmaProof(std::vector& lemma, + std::ostream& os, + std::ostream& paren, + const ProofLetMap& map) +{ + Debug("pf::arith") << "Printing proof for lemma " << lemma << std::endl; + // Prefixes for the names of linearity witnesses + const char* linearityWitnessPrefix = "lp"; + const char* linearizedProofPrefix = "pf_lp"; + std::ostringstream lemmaParen; + + // Construct the set of conflicting literals + std::set conflictSet; + std::transform(lemma.begin(), + lemma.end(), + std::inserter(conflictSet, conflictSet.begin()), + [](const Expr& e) { + return NodeManager::currentNM()->fromExpr(e).negate(); + }); + + // If we have Farkas coefficients stored for this lemma, use them to write a + // proof. Otherwise, just `trust` the lemma. + if (d_recorder.hasFarkasCoefficients(conflictSet)) + { + // Get farkas coefficients & literal order + const auto& farkasInfo = d_recorder.getFarkasCoefficients(conflictSet); + const Node& conflict = farkasInfo.first; + theory::arith::RationalVectorCP farkasCoefficients = farkasInfo.second; + Assert(farkasCoefficients != theory::arith::RationalVectorCPSentinel); + Assert(conflict.getNumChildren() == farkasCoefficients->size()); + const size_t nAntecedents = conflict.getNumChildren(); + + // Print proof + os << "\n;; Farkas Proof" << std::endl; + + // Construct witness that the literals are linear polynomials + os << "; Linear Polynomial Normalization Witnesses" << std::endl; + for (size_t i = 0; i != nAntecedents; ++i) + { + const Node& antecedent = conflict[i]; + const Rational farkasC = (*farkasCoefficients)[i]; + os << "\n; " << antecedent << " w/ farkas c = " << farkasC << std::endl; + os << " (@ " + << ProofManager::getLitName(antecedent.negate(), + linearityWitnessPrefix) + << " "; + const Node& nonneg = + antecedent.getKind() == kind::NOT ? antecedent[0] : antecedent; + printLinearPolynomialPredicateNormalizer(os, nonneg); + lemmaParen << ")"; + } + + // Prove linear polynomial constraints + os << "\n; Linear Polynomial Proof Conversions"; + for (size_t i = 0; i != nAntecedents; ++i) + { + const Node& antecedent = conflict[i]; + os << "\n (@ " + << ProofManager::getLitName(antecedent.negate(), linearizedProofPrefix) + << " "; + lemmaParen << ")"; + switch (conflict[i].getKind()) + { + case kind::NOT: + { + Assert(conflict[i][0].getKind() == kind::GEQ); + os << "(poly_flip_not_>= _ _ " + << "(poly_form_not _ _ " + << ProofManager::getLitName(antecedent.negate(), + linearityWitnessPrefix) + << " " << ProofManager::getLitName(antecedent.negate(), "") + << "))"; + break; + } + case kind::GEQ: + { + os << "(poly_form _ _ " + << ProofManager::getLitName(antecedent.negate(), + linearityWitnessPrefix) + << " " << ProofManager::getLitName(antecedent.negate(), "") << ")"; + break; + } + default: Unreachable(); + } + } + + /* Combine linear polynomial constraints to derive a contradiction. + * + * The linear polynomial constraints are refered to as **antecedents**, + * since they are antecedents to the contradiction. + * + * The structure of the combination is a tree + * + * (=> <=) + * | + * + 0 + * / \ + * * + 1 + * / \ + * * + 2 + * / \ + * * ... i + * \ + * + n-1 + * / \ + * * (0 >= 0) + * + * Where each * is a linearized antecedant being scaled by a farkas + * coefficient and each + is the sum of inequalities. The tricky bit is that + * each antecedent can be strict (>) or relaxed (>=) and the axiom used for + * each * and + depends on this... The axiom for * depends on the + * strictness of its linear polynomial input, and the axiom for + depends + * on the strictness of **both** its inputs. The contradiction axiom is + * also a function of the strictness of its input. + * + * There are n *s and +s and we precompute + * 1. The strictness of the ith antecedant (`ith_antecedent_is_strict`) + * 2. The strictness of the right argument of the ith sum + * (`ith_acc_is_strict`) + * 3. The strictness of the final result (`strict_contradiction`) + * + * Precomupation is helpful since + * the computation is post-order, + * but printing is pre-order. + */ + std::vector ith_antecedent_is_strict(nAntecedents, false); + std::vector ith_acc_is_strict(nAntecedents, false); + for (int i = nAntecedents - 1; i >= 0; --i) + { + ith_antecedent_is_strict[i] = conflict[i].getKind() == kind::NOT; + if (i == (int)nAntecedents - 1) + { + ith_acc_is_strict[i] = false; + } + else + { + ith_acc_is_strict[i] = + ith_acc_is_strict[i + 1] || ith_antecedent_is_strict[i + 1]; + } + } + bool strict_contradiction = + ith_acc_is_strict[0] || ith_antecedent_is_strict[0]; + + // Now, print the proof + os << "\n; Farkas Combination"; + // Choose the appropriate contradiction axiom + os << "\n (lra_contra_" << (strict_contradiction ? ">" : ">=") << " _ "; + for (size_t i = 0; i != nAntecedents; ++i) + { + const Node& lit = conflict[i]; + const char* ante_op = ith_antecedent_is_strict[i] ? ">" : ">="; + const char* acc_op = ith_acc_is_strict[i] ? ">" : ">="; + os << "\n (lra_add_" << ante_op << "_" << acc_op << " _ _ _ "; + os << "\n (lra_mul_c_" << ante_op << " _ _ "; + printRational(os, (*farkasCoefficients)[i].abs()); + os << " " << ProofManager::getLitName(lit.negate(), linearizedProofPrefix) + << ")" + << " ; " << lit; + } + + // The basis, at least, is always the same... + os << "\n (lra_axiom_>= 0/1)"; + std::fill_n(std::ostream_iterator(os), + nAntecedents, + ')'); // close lra_add_*_* + os << ")"; // close lra_contra_* + + os << lemmaParen.str(); // close normalizers and proof-normalizers + } + else + { + os << "\n; Arithmetic proofs which use reasoning more complex than Farkas " + "proofs are currently unsupported\n(clausify_false trust)\n"; } - os <<"\n"; - //os << " (clausify_false trust)"; - ArithProof::printTheoryLemmaProof(lemma, os, paren, map); } void LFSCArithProof::printSortDeclarations(std::ostream& os, std::ostream& paren) { + // Nothing to do here at this point. } void LFSCArithProof::printTermDeclarations(std::ostream& os, std::ostream& paren) { - for (ExprSet::const_iterator it = d_declarations.begin(); it != d_declarations.end(); ++it) { + for (ExprSet::const_iterator it = d_declarations.begin(); + it != d_declarations.end(); + ++it) + { Expr term = *it; Assert(term.isVariable()); - os << "(% " << ProofManager::sanitize(term) << " "; - os << "(term "; - os << term.getType() << ")\n"; + os << "(% " << ProofManager::sanitize(term) << " var_real\n"; + os << "(@ " << CVC4_ARITH_VAR_TERM_PREFIX << ProofManager::sanitize(term) + << " "; + os << "(a_var_real " << ProofManager::sanitize(term) << ")\n"; + paren << ")"; paren << ")"; } } diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h index a58294998..640d2db8d 100644 --- a/src/proof/arith_proof.h +++ b/src/proof/arith_proof.h @@ -64,7 +64,7 @@ protected: ExprSet d_declarations; // all the variable/function declarations /** - * @brief Where farkas proofs of lemmas are stored. + * Where farkas proofs of lemmas are stored. */ proof::ArithProofRecorder d_recorder; @@ -86,6 +86,76 @@ public: std::ostream& os, const ProofLetMap& map) override; void printOwnedSort(Type type, std::ostream& os) override; + + /** + * Print a rational number in LFSC format. + * e.g. 5/8 or (~ 1/1) + * + * @param o ostream to print to. + * @param r the rational to print + */ + static void printRational(std::ostream& o, const Rational& r); + + /** + * Print a value of type poly_formula_norm + * + * @param o ostream to print to + * @param n node (asserted to be of the form [linear polynomial >= constant]) + */ + static void printLinearPolynomialPredicateNormalizer(std::ostream& o, + const Node& n); + + /** + * Print a value of type poly_norm + * + * @param o ostream to print to + * @param n node (asserted to be a linear polynomial) + */ + static void printLinearPolynomialNormalizer(std::ostream& o, const Node& n); + + /** + * Print a value of type poly_norm + * + * @param o ostream to print to + * @param n node (asserted to be a linear monomial) + */ + static void printLinearMonomialNormalizer(std::ostream& o, const Node& n); + + /** + * Print a LFSC rational + * + * @param o ostream to print to + * @param n node (asserted to be a const rational) + */ + static void printConstRational(std::ostream& o, const Node& n); + + /** + * print the pn_var normalizer for n (type poly_norm) + * + * @param o the ostream to print to + * @param n the node to print (asserted to be a variable) + */ + static void printVariableNormalizer(std::ostream& o, const Node& n); + /** + * print a proof of the lemma + * + * First, we print linearity witnesses, i.e. witnesses that each literal has + * the form: + * [linear polynomial] >= 0 OR + * [linear polynomial] > 0 + * + * Then we use those witnesses to prove that the above linearized constraints + * hold. + * + * Then we use the farkas coefficients to combine the literals into a + * variable-free contradiction. The literals may be a mix of strict and + * relaxed inequalities. + * + * @param lemma the set of literals disjoined in the lemma + * @param os stream to print the proof to + * @param paren global closing stream (unused) + * @param map let map (unused) + */ void printTheoryLemmaProof(std::vector& lemma, std::ostream& os, std::ostream& paren, diff --git a/src/proof/arith_proof_recorder.cpp b/src/proof/arith_proof_recorder.cpp index d654ea073..097fdb51e 100644 --- a/src/proof/arith_proof_recorder.cpp +++ b/src/proof/arith_proof_recorder.cpp @@ -30,17 +30,25 @@ ArithProofRecorder::ArithProofRecorder() : d_lemmasToFarkasCoefficients() void ArithProofRecorder::saveFarkasCoefficients( Node conflict, theory::arith::RationalVectorCP farkasCoefficients) { + // Verify that the conflict is a conjuction of (possibly negated) real bounds + // Verify that the conflict is a conjunciton ... Assert(conflict.getKind() == kind::AND); Assert(conflict.getNumChildren() == farkasCoefficients->size()); - for (size_t i = 0; i < conflict.getNumChildren(); ++i) + for (size_t i = 0, nchildren = conflict.getNumChildren(); i < nchildren; ++i) { const Node& child = conflict[i]; - Assert(child.getType().isBoolean() && child[0].getType().isReal()); + // ... of possibly negated ... + const Node& nonNegativeChild = + child.getKind() == kind::NOT ? child[0] : child; + // ... real bounds + Assert(nonNegativeChild.getType().isBoolean() + && nonNegativeChild[0].getType().isReal()); } Debug("pf::arith") << "Saved Farkas Coefficients:" << std::endl; if (Debug.isOn("pf::arith")) { - for (size_t i = 0; i < conflict.getNumChildren(); ++i) + for (size_t i = 0, nchildren = conflict.getNumChildren(); i < nchildren; + ++i) { const Node& child = conflict[i]; const Rational& r = (*farkasCoefficients)[i]; diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 352ba0f36..297e3de37 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -499,6 +499,35 @@ bool Constraint::hasFarkasProof() const { return getProofType() == FarkasAP; } +bool Constraint::hasSimpleFarkasProof() const +{ + Debug("constraints::hsfp") << "hasSimpleFarkasProof " << this << std::endl; + if (!hasFarkasProof()) + { + Debug("constraints::hsfp") << "There is no simple Farkas proof because " + "there is no farkas proof." + << std::endl; + return false; + } + const ConstraintRule& rule = getConstraintRule(); + AntecedentId antId = rule.d_antecedentEnd; + ConstraintCP antecdent = d_database->getAntecedent(antId); + while (antecdent != NullConstraint) + { + if (antecdent->getProofType() != AssumeAP) + { + Debug("constraints::hsfp") << "There is no simple Farkas proof b/c there " + "is an antecdent w/ rule "; + antecdent->getConstraintRule().print(Debug("constraints::hsfp")); + Debug("constraints::hsfp") << std::endl; + return false; + } + --antId; + antecdent = d_database->getAntecedent(antId); + } + return true; +} + bool Constraint::hasIntHoleProof() const { return getProofType() == IntHoleAP; } @@ -568,8 +597,9 @@ void ConstraintRule::print(std::ostream& out) const { out << d_constraint << std::endl; out << "d_proofType= " << d_proofType << ", " << std::endl; out << "d_antecedentEnd= "<< d_antecedentEnd << std::endl; - - if(d_constraint != NullConstraint){ + + if (d_constraint != NullConstraint && d_antecedentEnd != AntecedentIdSentinel) + { const ConstraintDatabase& database = d_constraint->getDatabase(); size_t coeffIterator = (coeffs != RationalVectorCPSentinel) ? coeffs->size()-1 : 0; @@ -597,7 +627,7 @@ void ConstraintRule::print(std::ostream& out) const { out << " * (" << *(d_constraint->getNegation()) << ")"; out << " [not d_constraint] " << endl; } - out << "}"; + out << "}"; } bool Constraint::wellFormedFarkasProof() const { @@ -1188,6 +1218,8 @@ void Constraint::impliedByIntHole(ConstraintCP a, bool nowInConflict){ Assert(!hasProof()); Assert(negationHasProof() == nowInConflict); Assert(a->hasProof()); + Debug("pf::arith") << "impliedByIntHole(" << this << ", " << a << ")" + << std::endl; d_database->d_antecedents.push_back(NullConstraint); d_database->d_antecedents.push_back(a); @@ -1339,6 +1371,7 @@ Node Constraint::externalExplainByAssertions(const ConstraintCPVec& b){ } Node Constraint::externalExplainConflict() const{ + Debug("pf::arith") << this << std::endl; Assert(inConflict()); NodeBuilder<> nb(kind::AND); externalExplainByAssertions(nb); @@ -1407,6 +1440,13 @@ void Constraint::externalExplain(NodeBuilder<>& nb, AssertionOrder order) const{ Assert(!isAssumption() || assertedToTheTheory()); Assert(!isInternalAssumption()); + if (Debug.isOn("pf::arith")) + { + Debug("pf::arith") << "Explaining: " << this << " with rule "; + getConstraintRule().print(Debug("pf::arith")); + Debug("pf::arith") << std::endl; + } + if(assertedBefore(order)){ nb << getWitness(); }else if(hasEqualityEngineProof()){ @@ -1417,6 +1457,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; 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 d411f2d34..51575bb2f 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -258,7 +258,7 @@ struct PerVariableDatabase{ struct ConstraintRule { ConstraintP d_constraint; ArithProofType d_proofType; - AntecedentId d_antecedentEnd; + AntecedentId d_antecedentEnd; /** * In this comment, we abbreviate ConstraintDatabase::d_antecedents @@ -266,37 +266,38 @@ struct ConstraintRule { * * This list is always empty if proofs are not enabled. * - * If proofs are enabled, the proof of constraint c at p in ans[p] of length n is - * (NullConstraint, ans[p-(n-1)], ... , ans[p-1], ans[p]) - * - * Farkas' proofs show a contradiction with the negation of c, c_not = c->getNegation(). + * If proofs are enabled, the proof of constraint c at p in ans[p] of length n + * is (NullConstraint, ans[p-(n-1)], ... , ans[p-1], ans[p]) + * + * Farkas' proofs show a contradiction with the negation of c, c_not = + * c->getNegation(). * - * We treat the position for NullConstraint (p-n) as the position for the farkas - * coefficient for so we pretend c_not is ans[p-n]. - * So this correlation for the constraints we are going to use: - * (c_not, ans[p-(n-1)], ... , ans[p-1], ans[p]) - * With the coefficients at positions: - * (fc[0], fc[1)], ... fc[n]) + * We treat the position for NullConstraint (p-n) as the position for the + * farkas coefficient for so we pretend c_not is ans[p-n]. So this correlation + * for the constraints we are going to use: (c_not, ans[p-n+(1)], ... , + * ans[p-n+(n-1)], ans[p-n+(n)]) With the coefficients at positions: (fc[0], + * fc[1)], ... fc[n]) * - * The index of the constraints in the proof are {i | i <= 0 <= n] } (with c_not being p-n). - * Partition the indices into L, U, and E, the lower bounds, the upper bounds and equalities. + * The index of the constraints in the proof are {i | i <= 0 <= n] } (with + * c_not being p-n). Partition the indices into L, U, and E, the lower bounds, + * the upper bounds and equalities. * - * We standardize the proofs to be upper bound oriented following the convention: - * A x <= b - * with the proof witness of the form - * (lambda) Ax <= (lambda) b and lambda >= 0. + * We standardize the proofs to be upper bound oriented following the + * convention: A x <= b with the proof witness of the form (lambda) Ax <= + * (lambda) b and lambda >= 0. * - * To accomplish this cleanly, the fc coefficients must be negative for lower bounds. - * The signs of equalities can be either positive or negative. + * To accomplish this cleanly, the fc coefficients must be negative for lower + * bounds. The signs of equalities can be either positive or negative. * * Thus the proof corresponds to (with multiplication over inequalities): * \sum_{u in U} fc[u] ans[p-n+u] + \sum_{e in E} fc[e] ans[p-n+e] * + \sum_{l in L} fc[l] ans[p-n+l] * |= 0 < 0 * where fc[u] > 0, fc[l] < 0, and fc[e] != 0 (i.e. it can be either +/-). - * + * * There is no requirement that the proof is minimal. - * We do however use all of the constraints by requiring non-zero coefficients. + * We do however use all of the constraints by requiring non-zero + * coefficients. */ #if IS_PROOFS_BUILD RationalVectorCP d_farkasCoefficients; @@ -346,88 +347,10 @@ struct ConstraintRule { }; /* class ConstraintRule */ class Constraint { -private: - /** The ArithVar associated with the constraint. */ - const ArithVar d_variable; - - /** The type of the Constraint. */ - const ConstraintType d_type; - - /** The DeltaRational value with the constraint. */ - const DeltaRational d_value; - - /** A pointer to the associated database for the Constraint. */ - ConstraintDatabase* d_database; - - /** - * The node to be communicated with the TheoryEngine. - * - * This is not context dependent, but may be set once. - * - * This must be set if the constraint canBePropagated(). - * This must be set if the constraint assertedToTheTheory(). - * Otherwise, this may be null(). - */ - Node d_literal; - - /** Pointer to the negation of the Constraint. */ - ConstraintP d_negation; - - /** - * This is true if the associated node can be propagated. - * - * This should be enabled if the node has been preregistered. - * - * Sat Context Dependent. - * This is initially false. - */ - bool d_canBePropagated; - - /** - * This is the order the constraint was asserted to the theory. - * If this has been set, the node can be used in conflicts. - * If this is c.d_assertedOrder < d.d_assertedOrder, then c can be used in the - * explanation of d. - * - * This should be set after the literal is dequeued by Theory::get(). - * - * Sat Context Dependent. - * This is initially AssertionOrderSentinel. - */ - AssertionOrder d_assertionOrder; - - /** - * This is guaranteed to be on the fact queue. - * For example if x + y = x + 1 is on the fact queue, then use this - */ - TNode d_witness; - - /** - * The position of the constraint in the constraint rule id. - * - * Sat Context Dependent. - * This is initially - */ - ConstraintRuleID d_crid; - - - /** - * True if the equality has been split. - * Only meaningful if ConstraintType == Equality. - * - * User Context Dependent. - * This is initially false. - */ - bool d_split; - - /** - * Position in sorted constraint set for the variable. - * Unset if d_type is Disequality. - */ - SortedConstraintMapIterator d_variablePosition; friend class ConstraintDatabase; + public: /** * This begins construction of a minimal constraint. * @@ -444,86 +367,6 @@ private: */ ~Constraint(); - /** Returns true if the constraint has been initialized. */ - bool initialized() const; - - /** - * This initializes the fields that cannot be set in the constructor due to - * circular dependencies. - */ - void initialize(ConstraintDatabase* db, SortedConstraintMapIterator v, ConstraintP negation); - - - - class ConstraintRuleCleanup { - public: - inline void operator()(ConstraintRule* crp){ - Assert(crp != NULL); - ConstraintP constraint = crp->d_constraint; - Assert(constraint->d_crid != ConstraintRuleIdSentinel); - constraint->d_crid = ConstraintRuleIdSentinel; - - PROOF(if(crp->d_farkasCoefficients != RationalVectorCPSentinel){ - delete crp->d_farkasCoefficients; - }); - } - }; - - class CanBePropagatedCleanup { - public: - inline void operator()(ConstraintP* p){ - ConstraintP constraint = *p; - Assert(constraint->d_canBePropagated); - constraint->d_canBePropagated = false; - } - }; - - class AssertionOrderCleanup { - public: - inline void operator()(ConstraintP* p){ - ConstraintP constraint = *p; - Assert(constraint->assertedToTheTheory()); - constraint->d_assertionOrder = AssertionOrderSentinel; - constraint->d_witness = TNode::null(); - Assert(!constraint->assertedToTheTheory()); - } - }; - - class SplitCleanup { - public: - inline void operator()(ConstraintP* p){ - ConstraintP constraint = *p; - Assert(constraint->d_split); - constraint->d_split = false; - } - }; - - /** - * Returns true if the node is safe to garbage collect. - * Both it and its negation must have no context dependent data set. - */ - bool safeToGarbageCollect() const; - - /** - * Returns true if the constraint has no context dependent data set. - */ - bool contextDependentDataIsSet() const; - - /** - * Returns true if the node correctly corresponds to the constraint that is - * being set. - */ - bool sanityChecking(Node n) const; - - /** Returns a reference to the map for d_variable. */ - SortedConstraintMap& constraintSet() const; - - /** Returns coefficients for the proofs for farkas cancellation. */ - static std::pair unateFarkasSigns(ConstraintCP a, ConstraintCP b); - - -public: - static ConstraintType constraintTypeOfComparison(const Comparison& cmp); inline ConstraintType getType() const { @@ -648,6 +491,26 @@ public: /** Returns true if the node has a Farkas' proof. */ bool hasFarkasProof() const; + /** + * @brief Returns whether this constraint is provable using a Farkas + * proof that has input assertions as its antecedents. + * + * An example of a constraint that has a simple Farkas proof: + * x <= 0 proven from x + y <= 0 and x - y <= 0. + * + * An example of a constraint that does not have a simple Farkas proof: + * x <= 0 proven from x + y <= 0 and x - y <= 0.5 for integers x, y + * (since integer reasoning is also required!). + * Another example of a constraint that might be proven without a simple + * Farkas proof: + * x < 0 proven from not(x == 0) and not(x > 0). + * + * This could be proven internally by the arithmetic theory using + * `TrichotomyAP` as the proof type. + * + */ + bool hasSimpleFarkasProof() const; + /** Returns true if the node has a int hole proof. */ bool hasIntHoleProof() const; @@ -735,22 +598,6 @@ public: */ Node externalExplainConflict() const; -private: - Node externalExplain(AssertionOrder order) const; - - /** - * Returns an explanation of that was assertedBefore(order). - * The constraint must have a proof. - * The constraint cannot be selfExplaining(). - * - * This is the minimum fringe of the implication tree - * s.t. every constraint is assertedBefore(order) or hasEqualityEngineProof(). - */ - void externalExplain(NodeBuilder<>& nb, AssertionOrder order) const; - - static Node externalExplain(const ConstraintCPVec& b, AssertionOrder order); - -public: /** The constraint is known to be true. */ inline bool hasProof() const { @@ -791,7 +638,6 @@ public: */ ConstraintP getFloor(); - static ConstraintP makeNegation(ArithVar v, ConstraintType t, const DeltaRational& r); const ValueCollection& getValueCollection() const; @@ -896,11 +742,109 @@ public: */ const ConstraintDatabase& getDatabase() const; -private: - /** Returns the constraint rule at the position. */ const ConstraintRule& getConstraintRule() const; - + + private: + /** Returns true if the constraint has been initialized. */ + bool initialized() const; + + /** + * This initializes the fields that cannot be set in the constructor due to + * circular dependencies. + */ + void initialize(ConstraintDatabase* db, + SortedConstraintMapIterator v, + ConstraintP negation); + + class ConstraintRuleCleanup + { + public: + inline void operator()(ConstraintRule* crp) + { + Assert(crp != NULL); + ConstraintP constraint = crp->d_constraint; + Assert(constraint->d_crid != ConstraintRuleIdSentinel); + constraint->d_crid = ConstraintRuleIdSentinel; + + PROOF(if (crp->d_farkasCoefficients != RationalVectorCPSentinel) { + delete crp->d_farkasCoefficients; + }); + } + }; + + class CanBePropagatedCleanup + { + public: + inline void operator()(ConstraintP* p) + { + ConstraintP constraint = *p; + Assert(constraint->d_canBePropagated); + constraint->d_canBePropagated = false; + } + }; + + class AssertionOrderCleanup + { + public: + inline void operator()(ConstraintP* p) + { + ConstraintP constraint = *p; + Assert(constraint->assertedToTheTheory()); + constraint->d_assertionOrder = AssertionOrderSentinel; + constraint->d_witness = TNode::null(); + Assert(!constraint->assertedToTheTheory()); + } + }; + + class SplitCleanup + { + public: + inline void operator()(ConstraintP* p) + { + ConstraintP constraint = *p; + Assert(constraint->d_split); + constraint->d_split = false; + } + }; + + /** + * Returns true if the node is safe to garbage collect. + * Both it and its negation must have no context dependent data set. + */ + bool safeToGarbageCollect() const; + + /** + * Returns true if the constraint has no context dependent data set. + */ + bool contextDependentDataIsSet() const; + + /** + * Returns true if the node correctly corresponds to the constraint that is + * being set. + */ + bool sanityChecking(Node n) const; + + /** Returns a reference to the map for d_variable. */ + SortedConstraintMap& constraintSet() const; + + /** Returns coefficients for the proofs for farkas cancellation. */ + static std::pair unateFarkasSigns(ConstraintCP a, ConstraintCP b); + + Node externalExplain(AssertionOrder order) const; + + /** + * Returns an explanation of that was assertedBefore(order). + * The constraint must have a proof. + * The constraint cannot be selfExplaining(). + * + * This is the minimum fringe of the implication tree + * s.t. every constraint is assertedBefore(order) or hasEqualityEngineProof(). + */ + void externalExplain(NodeBuilder<>& nb, AssertionOrder order) const; + + static Node externalExplain(const ConstraintCPVec& b, AssertionOrder order); + inline ArithProofType getProofType() const { return getConstraintRule().d_proofType; } @@ -934,7 +878,85 @@ private: */ bool wellFormedFarkasProof() const; - + + /** The ArithVar associated with the constraint. */ + const ArithVar d_variable; + + /** The type of the Constraint. */ + const ConstraintType d_type; + + /** The DeltaRational value with the constraint. */ + const DeltaRational d_value; + + /** A pointer to the associated database for the Constraint. */ + ConstraintDatabase* d_database; + + /** + * The node to be communicated with the TheoryEngine. + * + * This is not context dependent, but may be set once. + * + * This must be set if the constraint canBePropagated(). + * This must be set if the constraint assertedToTheTheory(). + * Otherwise, this may be null(). + */ + Node d_literal; + + /** Pointer to the negation of the Constraint. */ + ConstraintP d_negation; + + /** + * This is true if the associated node can be propagated. + * + * This should be enabled if the node has been preregistered. + * + * Sat Context Dependent. + * This is initially false. + */ + bool d_canBePropagated; + + /** + * This is the order the constraint was asserted to the theory. + * If this has been set, the node can be used in conflicts. + * If this is c.d_assertedOrder < d.d_assertedOrder, then c can be used in the + * explanation of d. + * + * This should be set after the literal is dequeued by Theory::get(). + * + * Sat Context Dependent. + * This is initially AssertionOrderSentinel. + */ + AssertionOrder d_assertionOrder; + + /** + * This is guaranteed to be on the fact queue. + * For example if x + y = x + 1 is on the fact queue, then use this + */ + TNode d_witness; + + /** + * The position of the constraint in the constraint rule id. + * + * Sat Context Dependent. + * This is initially + */ + ConstraintRuleID d_crid; + + /** + * True if the equality has been split. + * Only meaningful if ConstraintType == Equality. + * + * User Context Dependent. + * This is initially false. + */ + bool d_split; + + /** + * Position in sorted constraint set for the variable. + * Unset if d_type is Disequality. + */ + SortedConstraintMapIterator d_variablePosition; + }; /* class ConstraintValue */ std::ostream& operator<<(std::ostream& o, const Constraint& c); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 89550295a..48d1b0188 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -2138,6 +2138,7 @@ Node flattenAndSort(Node n){ /** Outputs conflicts to the output channel. */ void TheoryArithPrivate::outputConflicts(){ + Debug("arith::conflict") << "outputting conflicts" << std::endl; Assert(anyConflict()); static unsigned int conflicts = 0; @@ -2145,13 +2146,39 @@ void TheoryArithPrivate::outputConflicts(){ Assert(!d_conflicts.empty()); for(size_t i = 0, i_end = d_conflicts.size(); i < i_end; ++i){ ConstraintCP confConstraint = d_conflicts[i]; + bool hasProof = confConstraint->hasProof(); Assert(confConstraint->inConflict()); + const ConstraintRule& pf = confConstraint->getConstraintRule(); + if (Debug.isOn("arith::conflict")) + { + pf.print(std::cout); + std::cout << std::endl; + } Node conflict = confConstraint->externalExplainConflict(); ++conflicts; Debug("arith::conflict") << "d_conflicts[" << i << "] " << conflict - // << "("<hasFarkasProof() + && pf.d_farkasCoefficients->size() + == conflict.getNumChildren()) { + // The Farkas coefficients and the children of `conflict` seem to be in + // opposite orders... There is some relevant documentation in the + // comment for the d_farkasCoefficients field in "constraint.h" + // + // Anyways, we reverse the children in `conflict` here. + NodeBuilder<> conflictInFarkasCoefficientOrder(kind::AND); + for (size_t i = 0, nchildren = conflict.getNumChildren(); i < nchildren; + ++i) + { + conflictInFarkasCoefficientOrder + << conflict[conflict.getNumChildren() - i - 1]; + } + + Assert(conflict.getNumChildren() == pf.d_farkasCoefficients->size()); + d_containing.d_proofRecorder->saveFarkasCoefficients( + conflictInFarkasCoefficientOrder, pf.d_farkasCoefficients); + }) if(Debug.isOn("arith::normalize::external")){ conflict = flattenAndSort(conflict); Debug("arith::conflict") << "(normalized to) " << conflict << endl; @@ -2174,7 +2201,9 @@ void TheoryArithPrivate::outputConflicts(){ (d_containing.d_out)->conflict(bb); } } + void TheoryArithPrivate::outputLemma(TNode lem) { + Debug("arith::lemma") << "Arith Lemma: " << lem << std::endl; (d_containing.d_out)->lemma(lem); } @@ -4809,11 +4838,41 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C PROOF(d_farkasBuffer.clear()); RationalVectorP coeffs = NULLPROOF(&d_farkasBuffer); - + + // After invoking `propegateRow`: + // * coeffs[0] is for implied + // * coeffs[i+1] is for explain[i] d_linEq.propagateRow(explain, ridx, rowUp, implied, coeffs); if(d_tableau.getRowLength(ridx) <= options::arithPropAsLemmaLength()){ Node implication = implied->externalImplication(explain); Node clause = flattenImplication(implication); + PROOF(if (d_containing.d_proofRecorder + && coeffs != RationalVectorCPSentinel + && coeffs->size() == clause.getNumChildren()) { + Debug("arith::prop") << "implied : " << implied << std::endl; + Debug("arith::prop") << "implication: " << implication << std::endl; + Debug("arith::prop") << "coeff len: " << coeffs->size() << std::endl; + Debug("arith::prop") << "exp : " << explain << std::endl; + Debug("arith::prop") << "clause : " << clause << std::endl; + Debug("arith::prop") + << "clause len: " << clause.getNumChildren() << std::endl; + Debug("arith::prop") << "exp len: " << explain.size() << std::endl; + // Using the information from the above comment we assemble a conflict + // AND in coefficient order + NodeBuilder<> conflictInFarkasCoefficientOrder(kind::AND); + conflictInFarkasCoefficientOrder << implication[1].negate(); + for (const Node& antecedent : implication[0]) + { + Debug("arith::prop") << " ante: " << antecedent << std::endl; + conflictInFarkasCoefficientOrder << antecedent; + } + + Assert(coeffs != RationalVectorPSentinel); + Assert(conflictInFarkasCoefficientOrder.getNumChildren() + == coeffs->size()); + d_containing.d_proofRecorder->saveFarkasCoefficients( + conflictInFarkasCoefficientOrder, coeffs); + }) outputLemma(clause); }else{ Assert(!implied->negationHasProof()); -- cgit v1.2.3