From b849961a85b61a29b13f8f58aa8ed7fff3c902a4 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 21 Sep 2021 22:39:32 -0700 Subject: Eliminate arithmetic proof macros (#7226) This PR eliminates some macros for arithmetic proofs, that only slightly simplified access to the produce-proofs option. Now that static access is deprecated, these checks needed to be implemented differently anyway. --- src/CMakeLists.txt | 1 - src/theory/arith/callbacks.cpp | 43 ++++---- src/theory/arith/callbacks.h | 6 +- src/theory/arith/constraint.cpp | 149 ++++++++++++++++----------- src/theory/arith/constraint.h | 81 +++++++-------- src/theory/arith/linear_equality.cpp | 6 +- src/theory/arith/linear_equality.h | 161 +++++++++++++++--------------- src/theory/arith/proof_macros.h | 32 ------ src/theory/arith/simplex.cpp | 3 +- src/theory/arith/theory_arith_private.cpp | 19 ++-- 10 files changed, 255 insertions(+), 246 deletions(-) delete mode 100644 src/theory/arith/proof_macros.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 8053340e8..5dbaa3349 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -509,7 +509,6 @@ libcvc5_add_sources( theory/arith/pp_rewrite_eq.h theory/arith/proof_checker.cpp theory/arith/proof_checker.h - theory/arith/proof_macros.h theory/arith/rewrites.cpp theory/arith/rewrites.h theory/arith/simplex.cpp diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp index 0c0a4959d..5b529ab7d 100644 --- a/src/theory/arith/callbacks.cpp +++ b/src/theory/arith/callbacks.cpp @@ -20,7 +20,6 @@ #include "expr/skolem_manager.h" #include "proof/proof_node.h" -#include "theory/arith/proof_macros.h" #include "theory/arith/theory_arith_private.h" namespace cvc5 { @@ -73,11 +72,12 @@ void RaiseConflict::raiseConflict(ConstraintCP c, InferenceId id) const{ d_ta.raiseConflict(c, id); } -FarkasConflictBuilder::FarkasConflictBuilder() - : d_farkas() - , d_constraints() - , d_consequent(NullConstraint) - , d_consequentSet(false) +FarkasConflictBuilder::FarkasConflictBuilder(bool produceProofs) + : d_farkas(), + d_constraints(), + d_consequent(NullConstraint), + d_consequentSet(false), + d_produceProofs(produceProofs) { reset(); } @@ -94,17 +94,20 @@ void FarkasConflictBuilder::reset(){ d_consequent = NullConstraint; d_constraints.clear(); d_consequentSet = false; - ARITH_PROOF(d_farkas.clear()); + if (d_produceProofs) + { + d_farkas.clear(); + } Assert(!underConstruction()); } /* Adds a constraint to the constraint under construction. */ void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc){ Assert( - !ARITH_PROOF_ON() + !d_produceProofs || (!underConstruction() && d_constraints.empty() && d_farkas.empty()) || (underConstruction() && d_constraints.size() + 1 == d_farkas.size())); - Assert(ARITH_PROOF_ON() || d_farkas.empty()); + Assert(d_produceProofs || d_farkas.empty()); Assert(c->isTrue()); if(d_consequent == NullConstraint){ @@ -112,14 +115,17 @@ void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc){ } else { d_constraints.push_back(c); } - ARITH_PROOF(d_farkas.push_back(fc)); - Assert(!ARITH_PROOF_ON() || d_constraints.size() + 1 == d_farkas.size()); - Assert(ARITH_PROOF_ON() || d_farkas.empty()); + if (d_produceProofs) + { + d_farkas.push_back(fc); + } + Assert(!d_produceProofs || d_constraints.size() + 1 == d_farkas.size()); + Assert(d_produceProofs || d_farkas.empty()); } void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc, const Rational& mult){ Assert(!mult.isZero()); - if (ARITH_PROOF_ON() && !mult.isOne()) + if (d_produceProofs && !mult.isOne()) { Rational prod = fc * mult; addConstraint(c, prod); @@ -142,7 +148,10 @@ void FarkasConflictBuilder::makeLastConsequent(){ ConstraintCP last = d_constraints.back(); d_constraints.back() = d_consequent; d_consequent = last; - ARITH_PROOF(std::swap(d_farkas.front(), d_farkas.back())); + if (d_produceProofs) + { + std::swap(d_farkas.front(), d_farkas.back()); + } d_consequentSet = true; } @@ -155,14 +164,14 @@ ConstraintCP FarkasConflictBuilder::commitConflict(){ Assert(underConstruction()); Assert(!d_constraints.empty()); Assert( - !ARITH_PROOF_ON() + !d_produceProofs || (!underConstruction() && d_constraints.empty() && d_farkas.empty()) || (underConstruction() && d_constraints.size() + 1 == d_farkas.size())); - Assert(ARITH_PROOF_ON() || d_farkas.empty()); + Assert(d_produceProofs || d_farkas.empty()); Assert(d_consequentSet); ConstraintP not_c = d_consequent->getNegation(); - RationalVectorCP coeffs = ARITH_NULLPROOF(&d_farkas); + RationalVectorCP coeffs = d_produceProofs ? &d_farkas : nullptr; not_c->impliedByFarkas(d_constraints, coeffs, true ); reset(); diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h index c8249a9fc..049b621c3 100644 --- a/src/theory/arith/callbacks.h +++ b/src/theory/arith/callbacks.h @@ -122,12 +122,14 @@ private: ConstraintCPVec d_constraints; ConstraintCP d_consequent; bool d_consequentSet; -public: + bool d_produceProofs; + + public: /** * Constructs a new FarkasConflictBuilder. */ - FarkasConflictBuilder(); + FarkasConflictBuilder(bool produceProofs); /** * Adds an antecedent constraint to the conflict under construction diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index 03db36bb5..defcc8aff 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -22,8 +22,10 @@ #include #include "base/output.h" +#include "options/smt_options.h" #include "proof/eager_proof_generator.h" #include "proof/proof_node_manager.h" +#include "smt/env.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/congruence_manager.h" @@ -39,6 +41,37 @@ namespace cvc5 { namespace theory { namespace arith { +ConstraintRule::ConstraintRule() + : d_constraint(NullConstraint), + d_proofType(NoAP), + d_antecedentEnd(AntecedentIdSentinel) +{ + d_farkasCoefficients = RationalVectorCPSentinel; +} + +ConstraintRule::ConstraintRule(ConstraintP con, ArithProofType pt) + : d_constraint(con), d_proofType(pt), d_antecedentEnd(AntecedentIdSentinel) +{ + d_farkasCoefficients = RationalVectorCPSentinel; +} +ConstraintRule::ConstraintRule(ConstraintP con, + ArithProofType pt, + AntecedentId antecedentEnd) + : d_constraint(con), d_proofType(pt), d_antecedentEnd(antecedentEnd) +{ + d_farkasCoefficients = RationalVectorCPSentinel; +} + +ConstraintRule::ConstraintRule(ConstraintP con, + ArithProofType pt, + AntecedentId antecedentEnd, + RationalVectorCP coeffs) + : d_constraint(con), d_proofType(pt), d_antecedentEnd(antecedentEnd) +{ + Assert(con->isProofProducing() || coeffs == RationalVectorCPSentinel); + d_farkasCoefficients = coeffs; +} + /** Given a simplifiedKind this returns the corresponding ConstraintType. */ //ConstraintType constraintTypeOfLiteral(Kind k); ConstraintType Constraint::constraintTypeOfComparison(const Comparison& cmp){ @@ -72,19 +105,23 @@ ConstraintType Constraint::constraintTypeOfComparison(const Comparison& cmp){ } } -Constraint::Constraint(ArithVar x, ConstraintType t, const DeltaRational& v) - : d_variable(x), - d_type(t), - d_value(v), - d_database(NULL), - d_literal(Node::null()), - d_negation(NullConstraint), - d_canBePropagated(false), - d_assertionOrder(AssertionOrderSentinel), - d_witness(TNode::null()), - d_crid(ConstraintRuleIdSentinel), - d_split(false), - d_variablePosition() +Constraint::Constraint(ArithVar x, + ConstraintType t, + const DeltaRational& v, + bool produceProofs) + : d_variable(x), + d_type(t), + d_value(v), + d_database(NULL), + d_literal(Node::null()), + d_negation(NullConstraint), + d_canBePropagated(false), + d_assertionOrder(AssertionOrderSentinel), + d_witness(TNode::null()), + d_crid(ConstraintRuleIdSentinel), + d_split(false), + d_variablePosition(), + d_produceProofs(produceProofs) { Assert(!initialized()); } @@ -542,7 +579,7 @@ bool Constraint::hasSimpleFarkasProof() const { Debug("constraints::hsfp") << "There is no simple Farkas proof b/c there " "is an antecdent w/ rule "; - a->getConstraintRule().print(Debug("constraints::hsfp")); + a->getConstraintRule().print(Debug("constraints::hsfp"), d_produceProofs); Debug("constraints::hsfp") << std::endl; } @@ -576,7 +613,7 @@ bool Constraint::hasTrichotomyProof() const { void Constraint::printProofTree(std::ostream& out, size_t depth) const { - if (ARITH_PROOF_ON()) + if (d_produceProofs) { const ConstraintRule& rule = getConstraintRule(); out << std::string(2 * depth, ' ') << "* " << getVariable() << " ["; @@ -662,18 +699,16 @@ bool Constraint::sanityChecking(Node n) const { } } -void ConstraintRule::debugPrint() const { - print(std::cerr); -} +void ConstraintRule::debugPrint() const { print(std::cerr, false); } ConstraintCP ConstraintDatabase::getAntecedent (AntecedentId p) const { Assert(p < d_antecedents.size()); return d_antecedents[p]; } - -void ConstraintRule::print(std::ostream& out) const { - RationalVectorCP coeffs = ARITH_NULLPROOF(d_farkasCoefficients); +void ConstraintRule::print(std::ostream& out, bool produceProofs) const +{ + RationalVectorCP coeffs = produceProofs ? d_farkasCoefficients : nullptr; out << "{ConstraintRule, "; out << d_constraint << std::endl; out << "d_proofType= " << d_proofType << ", " << std::endl; @@ -724,11 +759,11 @@ bool Constraint::wellFormedFarkasProof() const { ConstraintCP antecedent = d_database->d_antecedents[p]; if(antecedent == NullConstraint) { return false; } - if (!ARITH_PROOF_ON()) + if (!d_produceProofs) { return cr.d_farkasCoefficients == RationalVectorCPSentinel; } - Assert(ARITH_PROOF_ON()); + Assert(d_produceProofs); if(cr.d_farkasCoefficients == RationalVectorCPSentinel){ return false; } if(cr.d_farkasCoefficients->size() < 2){ return false; } @@ -828,7 +863,11 @@ bool Constraint::wellFormedFarkasProof() const { && rhs.sgn() < 0; } -ConstraintP Constraint::makeNegation(ArithVar v, ConstraintType t, const DeltaRational& r){ +ConstraintP Constraint::makeNegation(ArithVar v, + ConstraintType t, + const DeltaRational& r, + bool produceProofs) +{ switch(t){ case LowerBound: { @@ -837,12 +876,12 @@ ConstraintP Constraint::makeNegation(ArithVar v, ConstraintType t, const DeltaRa Assert(r.getInfinitesimalPart() == 1); // make (not (v > r)), which is (v <= r) DeltaRational dropInf(r.getNoninfinitesimalPart(), 0); - return new Constraint(v, UpperBound, dropInf); + return new Constraint(v, UpperBound, dropInf, produceProofs); }else{ Assert(r.infinitesimalSgn() == 0); // make (not (v >= r)), which is (v < r) DeltaRational addInf(r.getNoninfinitesimalPart(), -1); - return new Constraint(v, UpperBound, addInf); + return new Constraint(v, UpperBound, addInf, produceProofs); } } case UpperBound: @@ -852,40 +891,35 @@ ConstraintP Constraint::makeNegation(ArithVar v, ConstraintType t, const DeltaRa Assert(r.getInfinitesimalPart() == -1); // make (not (v < r)), which is (v >= r) DeltaRational dropInf(r.getNoninfinitesimalPart(), 0); - return new Constraint(v, LowerBound, dropInf); + return new Constraint(v, LowerBound, dropInf, produceProofs); }else{ Assert(r.infinitesimalSgn() == 0); // make (not (v <= r)), which is (v > r) DeltaRational addInf(r.getNoninfinitesimalPart(), 1); - return new Constraint(v, LowerBound, addInf); + return new Constraint(v, LowerBound, addInf, produceProofs); } } - case Equality: - return new Constraint(v, Disequality, r); - case Disequality: - return new Constraint(v, Equality, r); - default: - Unreachable(); - return NullConstraint; + case Equality: return new Constraint(v, Disequality, r, produceProofs); + case Disequality: return new Constraint(v, Equality, r, produceProofs); + default: Unreachable(); return NullConstraint; } } -ConstraintDatabase::ConstraintDatabase(context::Context* satContext, - context::Context* userContext, +ConstraintDatabase::ConstraintDatabase(Env& env, const ArithVariables& avars, ArithCongruenceManager& cm, RaiseConflict raiseConflict, - EagerProofGenerator* pfGen, - ProofNodeManager* pnm) - : d_varDatabases(), - d_toPropagate(satContext), - d_antecedents(satContext, false), - d_watches(new Watches(satContext, userContext)), + EagerProofGenerator* pfGen) + : EnvObj(env), + d_varDatabases(), + d_toPropagate(context()), + d_antecedents(context(), false), + d_watches(new Watches(context(), userContext())), d_avariables(avars), d_congruenceManager(cm), - d_satContext(satContext), d_pfGen(pfGen), - d_pnm(pnm), + d_pnm(d_env.isTheoryProofProducing() ? d_env.getProofNodeManager() + : nullptr), d_raiseConflict(raiseConflict), d_one(1), d_negOne(-1) @@ -938,8 +972,9 @@ ConstraintP ConstraintDatabase::getConstraint(ArithVar v, ConstraintType t, cons if(vc.hasConstraintOfType(t)){ return vc.getConstraintOfType(t); }else{ - ConstraintP c = new Constraint(v, t, r); - ConstraintP negC = Constraint::makeNegation(v, t, r); + ConstraintP c = new Constraint(v, t, r, options().smt.produceProofs); + ConstraintP negC = + Constraint::makeNegation(v, t, r, options().smt.produceProofs); SortedConstraintMapIterator negPos; if(t == Equality || t == Disequality){ @@ -1139,7 +1174,8 @@ ConstraintP ConstraintDatabase::addLiteral(TNode literal){ DeltaRational posDR = posCmp.normalizedDeltaRational(); - ConstraintP posC = new Constraint(v, posType, posDR); + ConstraintP posC = + new Constraint(v, posType, posDR, options().smt.produceProofs); Debug("arith::constraint") << "addliteral( literal ->" << literal << ")" << endl; Debug("arith::constraint") << "addliteral( posC ->" << posC << ")" << endl; @@ -1170,7 +1206,8 @@ ConstraintP ConstraintDatabase::addLiteral(TNode literal){ ConstraintType negType = Constraint::constraintTypeOfComparison(negCmp); DeltaRational negDR = negCmp.normalizedDeltaRational(); - ConstraintP negC = new Constraint(v, negType, negDR); + ConstraintP negC = + new Constraint(v, negType, negDR, options().smt.produceProofs); SortedConstraintMapIterator negI; @@ -1270,7 +1307,7 @@ void Constraint::impliedByUnate(ConstraintCP imp, bool nowInConflict){ AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1; RationalVectorP coeffs; - if (ARITH_PROOF_ON()) + if (d_produceProofs) { std::pair sgns = unateFarkasSigns(getNegation(), imp); @@ -1294,7 +1331,7 @@ void Constraint::impliedByUnate(ConstraintCP imp, bool nowInConflict){ } if(Debug.isOn("constraints::wffp") && !wellFormedFarkasProof()){ - getConstraintRule().print(Debug("constraints::wffp")); + getConstraintRule().print(Debug("constraints::wffp"), d_produceProofs); } Assert(wellFormedFarkasProof()); } @@ -1418,8 +1455,8 @@ void Constraint::impliedByFarkas(const ConstraintCPVec& a, RationalVectorCP coef Assert(negationHasProof() == nowInConflict); Assert(allHaveProof(a)); - Assert(ARITH_PROOF_ON() == (coeffs != RationalVectorCPSentinel)); - Assert(!ARITH_PROOF_ON() || coeffs->size() == a.size() + 1); + Assert(d_produceProofs == (coeffs != RationalVectorCPSentinel)); + Assert(!d_produceProofs || coeffs->size() == a.size() + 1); Assert(a.size() >= 1); @@ -1432,7 +1469,7 @@ void Constraint::impliedByFarkas(const ConstraintCPVec& a, RationalVectorCP coef AntecedentId antecedentEnd = d_database->d_antecedents.size() - 1; RationalVectorCP coeffsCopy; - if (ARITH_PROOF_ON()) + if (d_produceProofs) { Assert(coeffs != RationalVectorCPSentinel); coeffsCopy = new RationalVector(*coeffs); @@ -1448,7 +1485,7 @@ void Constraint::impliedByFarkas(const ConstraintCPVec& a, RationalVectorCP coef Debug("constraint::conflictCommit") << "inConflict@impliedByFarkas " << this << std::endl; } if(Debug.isOn("constraints::wffp") && !wellFormedFarkasProof()){ - getConstraintRule().print(Debug("constraints::wffp")); + getConstraintRule().print(Debug("constraints::wffp"), d_produceProofs); } Assert(wellFormedFarkasProof()); } @@ -1661,7 +1698,7 @@ std::shared_ptr Constraint::externalExplain( { this->printProofTree(Debug("arith::pf::tree")); Debug("pf::arith::explain") << "Explaining: " << this << " with rule "; - getConstraintRule().print(Debug("pf::arith::explain")); + getConstraintRule().print(Debug("pf::arith::explain"), d_produceProofs); Debug("pf::arith::explain") << std::endl; } Assert(hasProof()); diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index f6306049b..1262181db 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -87,11 +87,11 @@ #include "context/cdqueue.h" #include "expr/node.h" #include "proof/trust_node.h" +#include "smt/env_obj.h" #include "theory/arith/arithvar.h" #include "theory/arith/callbacks.h" #include "theory/arith/constraint_forward.h" #include "theory/arith/delta_rational.h" -#include "theory/arith/proof_macros.h" #include "util/statistics_stats.h" namespace cvc5 { @@ -310,39 +310,18 @@ struct ConstraintRule { * coefficients. */ RationalVectorCP d_farkasCoefficients; - ConstraintRule() - : d_constraint(NullConstraint) - , d_proofType(NoAP) - , d_antecedentEnd(AntecedentIdSentinel) - { - d_farkasCoefficients = RationalVectorCPSentinel; - } - - ConstraintRule(ConstraintP con, ArithProofType pt) - : d_constraint(con) - , d_proofType(pt) - , d_antecedentEnd(AntecedentIdSentinel) - { - d_farkasCoefficients = RationalVectorCPSentinel; - } - ConstraintRule(ConstraintP con, ArithProofType pt, AntecedentId antecedentEnd) - : d_constraint(con) - , d_proofType(pt) - , d_antecedentEnd(antecedentEnd) - { - d_farkasCoefficients = RationalVectorCPSentinel; - } - ConstraintRule(ConstraintP con, ArithProofType pt, AntecedentId antecedentEnd, RationalVectorCP coeffs) - : d_constraint(con) - , d_proofType(pt) - , d_antecedentEnd(antecedentEnd) - { - Assert(ARITH_PROOF_ON() || coeffs == RationalVectorCPSentinel); - d_farkasCoefficients = coeffs; - } - - void print(std::ostream& out) const; + ConstraintRule(); + ConstraintRule(ConstraintP con, ArithProofType pt); + ConstraintRule(ConstraintP con, + ArithProofType pt, + AntecedentId antecedentEnd); + ConstraintRule(ConstraintP con, + ArithProofType pt, + AntecedentId antecedentEnd, + RationalVectorCP coeffs); + + void print(std::ostream& out, bool produceProofs) const; void debugPrint() const; }; /* class ConstraintRule */ @@ -359,7 +338,10 @@ class Constraint { * Because of circular dependencies a Constraint is not fully valid until * initialize has been called on it. */ - Constraint(ArithVar x, ConstraintType t, const DeltaRational& v); + Constraint(ArithVar x, + ConstraintType t, + const DeltaRational& v, + bool produceProofs); /** * Destructor for a constraint. @@ -492,6 +474,9 @@ class Constraint { /** Returns true if the node is an assumption.*/ bool isAssumption() const; + /** Whether we produce proofs */ + bool isProofProducing() const { return d_produceProofs; } + /** Set the constraint to have an EqualityEngine proof. */ void setEqualityEngineProof(); bool hasEqualityEngineProof() const; @@ -662,7 +647,10 @@ class Constraint { */ ConstraintP getFloor(); - static ConstraintP makeNegation(ArithVar v, ConstraintType t, const DeltaRational& r); + static ConstraintP makeNegation(ArithVar v, + ConstraintType t, + const DeltaRational& r, + bool produceProofs); const ValueCollection& getValueCollection() const; @@ -799,12 +787,13 @@ class Constraint { ConstraintP constraint = crp->d_constraint; Assert(constraint->d_crid != ConstraintRuleIdSentinel); constraint->d_crid = ConstraintRuleIdSentinel; - ARITH_PROOF({ + if (constraint->isProofProducing()) + { if (crp->d_farkasCoefficients != RationalVectorCPSentinel) { delete crp->d_farkasCoefficients; } - }); + } } }; @@ -890,7 +879,7 @@ class Constraint { inline RationalVectorCP getFarkasCoefficients() const { - return ARITH_NULLPROOF(getConstraintRule().d_farkasCoefficients); + return d_produceProofs ? getConstraintRule().d_farkasCoefficients : nullptr; } void debugPrint() const; @@ -993,6 +982,9 @@ class Constraint { */ SortedConstraintMapIterator d_variablePosition; + /** Whether to produce proofs, */ + bool d_produceProofs; + }; /* class ConstraintValue */ std::ostream& operator<<(std::ostream& o, const Constraint& c); @@ -1003,9 +995,9 @@ std::ostream& operator<<(std::ostream& o, const ValueCollection& c); std::ostream& operator<<(std::ostream& o, const ConstraintCPVec& v); std::ostream& operator<<(std::ostream& o, const ArithProofType); - -class ConstraintDatabase { -private: +class ConstraintDatabase : protected EnvObj +{ + private: /** * The map from ArithVars to their unique databases. * When the vector changes size, we cannot allow the maps to move so this @@ -1105,7 +1097,6 @@ private: ArithCongruenceManager& d_congruenceManager; - const context::Context * const d_satContext; /** Owned by the TheoryArithPrivate, used here. */ EagerProofGenerator* d_pfGen; /** Owned by the TheoryArithPrivate, used here. */ @@ -1120,13 +1111,11 @@ private: friend class Constraint; public: - ConstraintDatabase(context::Context* satContext, - context::Context* userContext, + ConstraintDatabase(Env& env, const ArithVariables& variables, ArithCongruenceManager& dm, RaiseConflict conflictCallBack, - EagerProofGenerator* pfGen, - ProofNodeManager* pnm); + EagerProofGenerator* pfGen); ~ConstraintDatabase(); diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp index 47dd208c1..8e7588847 100644 --- a/src/theory/arith/linear_equality.cpp +++ b/src/theory/arith/linear_equality.cpp @@ -482,7 +482,9 @@ const Tableau::Entry* LinearEqualityModule::rowLacksBound(RowIndex ridx, bool ro return NULL; } -void LinearEqualityModule::propagateBasicFromRow(ConstraintP c){ +void LinearEqualityModule::propagateBasicFromRow(ConstraintP c, + bool produceProofs) +{ Assert(c != NullConstraint); Assert(c->isUpperBound() || c->isLowerBound()); Assert(!c->assertedToTheTheory()); @@ -493,7 +495,7 @@ void LinearEqualityModule::propagateBasicFromRow(ConstraintP c){ RowIndex ridx = d_tableau.basicToRowIndex(basic); ConstraintCPVec bounds; - RationalVectorP coeffs = ARITH_NULLPROOF(new RationalVector()); + RationalVectorP coeffs = produceProofs ? new RationalVector() : nullptr; propagateRow(bounds, ridx, upperBound, c, coeffs); c->impliedByFarkas(bounds, coeffs, false); c->tryToPropagate(); diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h index 7195a6583..9a08530ec 100644 --- a/src/theory/arith/linear_equality.h +++ b/src/theory/arith/linear_equality.h @@ -417,87 +417,86 @@ public: * The constraint on a basic variable b is implied by the constraints * on its row. This is a wrapper for propagateRow(). */ - void propagateBasicFromRow(ConstraintP c); - - /** - * Let v be the variable for the constraint c. - * Exports either the explanation of an upperbound or a lower bound - * of v using the other variables in the row. - * - * If farkas != RationalVectorPSentinel, this function additionally - * stores the farkas coefficients of the constraints stored in into. - * Position 0 is the coefficient of v. - * Position i > 0, corresponds to the order of the other constraints. - */ - void propagateRow(ConstraintCPVec& into - , RowIndex ridx - , bool rowUp - , ConstraintP c - , RationalVectorP farkas); - - /** - * Computes the value of a basic variable using the assignments - * of the values of the variables in the basic variable's row tableau. - * This can compute the value using either: - * - the the current assignment (useSafe=false) or - * - the safe assignment (useSafe = true). - */ - DeltaRational computeRowValue(ArithVar x, bool useSafe) const; - - /** - * A PreferenceFunction takes a const ref to the SimplexDecisionProcedure, - * and 2 ArithVar variables and returns one of the ArithVar variables - * potentially using the internals of the SimplexDecisionProcedure. - */ - - ArithVar noPreference(ArithVar x, ArithVar y) const{ - return x; - } - - /** - * minVarOrder is a PreferenceFunction for selecting the smaller of the 2 - * ArithVars. This PreferenceFunction is used during the VarOrder stage of - * findModel. - */ - ArithVar minVarOrder(ArithVar x, ArithVar y) const; - - /** - * minColLength is a PreferenceFunction for selecting the variable with the - * smaller row count in the tableau. - * - * This is a heuristic rule and should not be used during the VarOrder - * stage of findModel. - */ - ArithVar minColLength(ArithVar x, ArithVar y) const; - - /** - * minRowLength is a PreferenceFunction for selecting the variable with the - * smaller row count in the tableau. - * - * This is a heuristic rule and should not be used during the VarOrder - * stage of findModel. - */ - ArithVar minRowLength(ArithVar x, ArithVar y) const; - - /** - * minBoundAndRowCount is a PreferenceFunction for preferring a variable - * without an asserted bound over variables with an asserted bound. - * If both have bounds or both do not have bounds, - * the rule falls back to minRowCount(...). - * - * This is a heuristic rule and should not be used during the VarOrder - * stage of findModel. - */ - ArithVar minBoundAndColLength(ArithVar x, ArithVar y) const; - - - template - inline bool isAcceptableSlack(int sgn, ArithVar nonbasic) const { - return - ( above && sgn < 0 && d_variables.strictlyBelowUpperBound(nonbasic)) || - ( above && sgn > 0 && d_variables.strictlyAboveLowerBound(nonbasic)) || - (!above && sgn > 0 && d_variables.strictlyBelowUpperBound(nonbasic)) || - (!above && sgn < 0 && d_variables.strictlyAboveLowerBound(nonbasic)); + void propagateBasicFromRow(ConstraintP c, bool produceProofs); + + /** + * Let v be the variable for the constraint c. + * Exports either the explanation of an upperbound or a lower bound + * of v using the other variables in the row. + * + * If farkas != RationalVectorPSentinel, this function additionally + * stores the farkas coefficients of the constraints stored in into. + * Position 0 is the coefficient of v. + * Position i > 0, corresponds to the order of the other constraints. + */ + void propagateRow(ConstraintCPVec& into, + RowIndex ridx, + bool rowUp, + ConstraintP c, + RationalVectorP farkas); + + /** + * Computes the value of a basic variable using the assignments + * of the values of the variables in the basic variable's row tableau. + * This can compute the value using either: + * - the the current assignment (useSafe=false) or + * - the safe assignment (useSafe = true). + */ + DeltaRational computeRowValue(ArithVar x, bool useSafe) const; + + /** + * A PreferenceFunction takes a const ref to the SimplexDecisionProcedure, + * and 2 ArithVar variables and returns one of the ArithVar variables + * potentially using the internals of the SimplexDecisionProcedure. + */ + + ArithVar noPreference(ArithVar x, ArithVar y) const { return x; } + + /** + * minVarOrder is a PreferenceFunction for selecting the smaller of the 2 + * ArithVars. This PreferenceFunction is used during the VarOrder stage of + * findModel. + */ + ArithVar minVarOrder(ArithVar x, ArithVar y) const; + + /** + * minColLength is a PreferenceFunction for selecting the variable with the + * smaller row count in the tableau. + * + * This is a heuristic rule and should not be used during the VarOrder + * stage of findModel. + */ + ArithVar minColLength(ArithVar x, ArithVar y) const; + + /** + * minRowLength is a PreferenceFunction for selecting the variable with the + * smaller row count in the tableau. + * + * This is a heuristic rule and should not be used during the VarOrder + * stage of findModel. + */ + ArithVar minRowLength(ArithVar x, ArithVar y) const; + + /** + * minBoundAndRowCount is a PreferenceFunction for preferring a variable + * without an asserted bound over variables with an asserted bound. + * If both have bounds or both do not have bounds, + * the rule falls back to minRowCount(...). + * + * This is a heuristic rule and should not be used during the VarOrder + * stage of findModel. + */ + ArithVar minBoundAndColLength(ArithVar x, ArithVar y) const; + + template + inline bool isAcceptableSlack(int sgn, ArithVar nonbasic) const + { + return (above && sgn < 0 && d_variables.strictlyBelowUpperBound(nonbasic)) + || (above && sgn > 0 && d_variables.strictlyAboveLowerBound(nonbasic)) + || (!above && sgn > 0 + && d_variables.strictlyBelowUpperBound(nonbasic)) + || (!above && sgn < 0 + && d_variables.strictlyAboveLowerBound(nonbasic)); } /** diff --git a/src/theory/arith/proof_macros.h b/src/theory/arith/proof_macros.h deleted file mode 100644 index c794c3b00..000000000 --- a/src/theory/arith/proof_macros.h +++ /dev/null @@ -1,32 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Alex Ozdemir, Aina Niemetz - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Macros which run code when the old or new proof system is enabled, - * or unsat cores are enabled. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__THEORY__ARITH__PROOF_MACROS_H -#define CVC5__THEORY__ARITH__PROOF_MACROS_H - -#include "options/smt_options.h" - -#define ARITH_PROOF(x) \ - if (cvc5::options::produceProofs()) \ - { \ - x; \ - } -#define ARITH_NULLPROOF(x) (cvc5::options::produceProofs()) ? x : NULL -#define ARITH_PROOF_ON() cvc5::options::produceProofs() - -#endif // CVC5__THEORY__ARITH__PROOF_MACROS_H diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 781f132d7..ed81f9e78 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -18,6 +18,7 @@ #include "base/output.h" #include "options/arith_options.h" +#include "options/smt_options.h" #include "theory/arith/constraint.h" #include "theory/arith/error_set.h" #include "theory/arith/linear_equality.h" @@ -49,7 +50,7 @@ SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq, { d_heuristicRule = options::arithErrorSelectionRule(); d_errorSet.setSelectionRule(d_heuristicRule); - d_conflictBuilder = new FarkasConflictBuilder(); + d_conflictBuilder = new FarkasConflictBuilder(options::produceProofs()); } SimplexDecisionProcedure::~SimplexDecisionProcedure(){ diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index c0c51f7da..8e6bb6ccc 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -37,6 +37,7 @@ #include "expr/skolem_manager.h" #include "options/arith_options.h" #include "options/base_options.h" +#include "options/smt_options.h" #include "preprocessing/util/ite_utilities.h" #include "proof/proof_generator.h" #include "proof/proof_node_manager.h" @@ -97,13 +98,11 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, : nullptr), d_checker(), d_pfGen(new EagerProofGenerator(d_pnm, userContext())), - d_constraintDatabase(context(), - userContext(), + d_constraintDatabase(d_env, d_partialModel, d_congruenceManager, RaiseConflict(*this), - d_pfGen.get(), - d_pnm), + d_pfGen.get()), d_qflraStatus(Result::SAT_UNKNOWN), d_unknownsInARow(0), d_hasDoneWorkSinceCut(false), @@ -1749,7 +1748,7 @@ void TheoryArithPrivate::outputConflicts(){ const ConstraintRule& pf = confConstraint->getConstraintRule(); if (Debug.isOn("arith::conflict")) { - pf.print(std::cout); + pf.print(std::cout, options().smt.produceProofs); std::cout << std::endl; } if (Debug.isOn("arith::pf::tree")) @@ -4130,7 +4129,7 @@ bool TheoryArithPrivate::propagateCandidateBound(ArithVar basic, bool upperBound } if(!assertedToTheTheory && canBePropagated && !hasProof ){ - d_linEq.propagateBasicFromRow(bestImplied); + d_linEq.propagateBasicFromRow(bestImplied, options().smt.produceProofs); // I think this can be skipped if canBePropagated is true //d_learnedBounds.push(bestImplied); if(Debug.isOn("arith::prop")){ @@ -4435,8 +4434,12 @@ bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, C if( !assertedToTheTheory && canBePropagated && !hasProof ){ ConstraintCPVec explain; - ARITH_PROOF(d_farkasBuffer.clear()); - RationalVectorP coeffs = ARITH_NULLPROOF(&d_farkasBuffer); + if (options().smt.produceProofs) + { + d_farkasBuffer.clear(); + } + RationalVectorP coeffs = + options().smt.produceProofs ? &d_farkasBuffer : nullptr; // After invoking `propegateRow`: // * coeffs[0] is for implied -- cgit v1.2.3