From 9a3366475a85824f68a1e5bbc6d129992541412d Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 18 Oct 2024 09:49:11 -0500 Subject: [PATCH] More --- src/api/cpp/cvc5_proof_rule_template.cpp | 3 +- src/proof/conv_proof_generator.cpp | 15 +++--- src/proof/conv_proof_generator.h | 12 ++--- src/proof/trust_id.cpp | 3 +- src/smt/proof_post_processor.cpp | 4 +- src/theory/arith/arith_proof_utilities.cpp | 9 ++-- src/theory/arith/arith_proof_utilities.h | 4 +- .../nl/ext/arith_nl_compare_proof_gen.cpp | 46 ++++++++++++------- .../arith/nl/ext/arith_nl_compare_proof_gen.h | 14 ++++-- src/theory/arith/nl/ext/monomial_check.cpp | 27 ++++++----- src/theory/arith/nl/ext/monomial_check.h | 3 +- src/theory/arith/nl/ext/proof_checker.cpp | 2 +- 12 files changed, 86 insertions(+), 56 deletions(-) diff --git a/src/api/cpp/cvc5_proof_rule_template.cpp b/src/api/cpp/cvc5_proof_rule_template.cpp index 4164e8bd2fc..37f4e9861da 100644 --- a/src/api/cpp/cvc5_proof_rule_template.cpp +++ b/src/api/cpp/cvc5_proof_rule_template.cpp @@ -158,7 +158,8 @@ const char* toString(ProofRule rule) case ProofRule::MACRO_RE_ELIM: return "MACRO_RE_ELIM"; //================================================= Arith rules case ProofRule::MACRO_ARITH_SCALE_SUM_UB: return "MACRO_ARITH_SCALE_SUM_UB"; - case ProofRule::MACRO_ARITH_NL_COMPARISON: return "MACRO_ARITH_NL_COMPARISON"; + case ProofRule::MACRO_ARITH_NL_COMPARISON: + return "MACRO_ARITH_NL_COMPARISON"; case ProofRule::ARITH_SUM_UB: return "ARITH_SUM_UB"; case ProofRule::ARITH_TRICHOTOMY: return "ARITH_TRICHOTOMY"; case ProofRule::INT_TIGHT_LB: return "INT_TIGHT_LB"; diff --git a/src/proof/conv_proof_generator.cpp b/src/proof/conv_proof_generator.cpp index 780100133eb..0bc94ca2f8a 100644 --- a/src/proof/conv_proof_generator.cpp +++ b/src/proof/conv_proof_generator.cpp @@ -112,13 +112,14 @@ void TConvProofGenerator::addRewriteStep(Node t, } } -void TConvProofGenerator::addTrustedRewriteStep(Node t, - Node s, - TrustId id, - const std::vector& children, - const std::vector& args, - bool isPre, - uint32_t tctx) +void TConvProofGenerator::addTrustedRewriteStep( + Node t, + Node s, + TrustId id, + const std::vector& children, + const std::vector& args, + bool isPre, + uint32_t tctx) { std::vector targs; targs.push_back(mkTrustId(id)); diff --git a/src/proof/conv_proof_generator.h b/src/proof/conv_proof_generator.h index 58d439e5ca6..d4ddfbeee6b 100644 --- a/src/proof/conv_proof_generator.h +++ b/src/proof/conv_proof_generator.h @@ -174,12 +174,12 @@ class TConvProofGenerator : protected EnvObj, public ProofGenerator uint32_t tctx = 0); /** Same as above, but with a trusted step */ void addTrustedRewriteStep(Node t, - Node s, - TrustId id, - const std::vector& children, - const std::vector& args, - bool isPre = false, - uint32_t tctx = 0); + Node s, + TrustId id, + const std::vector& children, + const std::vector& args, + bool isPre = false, + uint32_t tctx = 0); /** Has rewrite step for term t */ bool hasRewriteStep(Node t, uint32_t tctx = 0, bool isPre = false) const; /** diff --git a/src/proof/trust_id.cpp b/src/proof/trust_id.cpp index 7c5f72c042d..b50da4e2bb4 100644 --- a/src/proof/trust_id.cpp +++ b/src/proof/trust_id.cpp @@ -38,7 +38,8 @@ const char* toString(TrustId id) case TrustId::ARITH_NL_COVERING_DIRECT: return "ARITH_NL_COVERING_DIRECT"; case TrustId::ARITH_NL_COVERING_RECURSIVE: return "ARITH_NL_COVERING_RECURSIVE"; - case TrustId::ARITH_NL_COMPARE_LIT_TRANSFORM: return "ARITH_NL_COMPARE_LIT_TRANSFORM"; + case TrustId::ARITH_NL_COMPARE_LIT_TRANSFORM: + return "ARITH_NL_COMPARE_LIT_TRANSFORM"; case TrustId::EXT_THEORY_REWRITE: return "EXT_THEORY_REWRITE"; case TrustId::REWRITE_NO_ELABORATE: return "REWRITE_NO_ELABORATE"; case TrustId::FLATTENING_REWRITE: return "FLATTENING_REWRITE"; diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 2234b86a6cd..7bd91b55607 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -970,8 +970,8 @@ Node ProofPostprocessCallback::expandMacros(ProofRule id, else if (id == ProofRule::MACRO_ARITH_NL_COMPARISON) { Node resc = theory::arith::expandMacroNlComparison(children, args, cdp); - //Assert(!resc.isNull()); - //Assert(res.isNull() || resc == res); + // Assert(!resc.isNull()); + // Assert(res.isNull() || resc == res); return resc; } else if (id == ProofRule::MACRO_STRING_INFERENCE) diff --git a/src/theory/arith/arith_proof_utilities.cpp b/src/theory/arith/arith_proof_utilities.cpp index 7ae2ea62f96..d3a81bdfb50 100644 --- a/src/theory/arith/arith_proof_utilities.cpp +++ b/src/theory/arith/arith_proof_utilities.cpp @@ -109,11 +109,12 @@ Node expandMacroSumUb(const std::vector& children, } Node expandMacroNlComparison(const std::vector& children, - const std::vector& args, - CDProof* cdp) + const std::vector& args, + CDProof* cdp) { - Trace("macro::arith") << "Comparsion prove: " << children << " => " << args[0] << std::endl; - //AlwaysAssert(false); + Trace("macro::arith") << "Comparsion prove: " << children << " => " << args[0] + << std::endl; + // AlwaysAssert(false); return Node::null(); } diff --git a/src/theory/arith/arith_proof_utilities.h b/src/theory/arith/arith_proof_utilities.h index 19476363e32..8fa4becac84 100644 --- a/src/theory/arith/arith_proof_utilities.h +++ b/src/theory/arith/arith_proof_utilities.h @@ -76,8 +76,8 @@ Node expandMacroSumUb(const std::vector& children, * @return The conclusion of the proof rule. */ Node expandMacroNlComparison(const std::vector& children, - const std::vector& args, - CDProof* cdp); + const std::vector& args, + CDProof* cdp); } // namespace arith } // namespace theory } // namespace cvc5::internal diff --git a/src/theory/arith/nl/ext/arith_nl_compare_proof_gen.cpp b/src/theory/arith/nl/ext/arith_nl_compare_proof_gen.cpp index d737d5362c9..9d5913d7ef3 100644 --- a/src/theory/arith/nl/ext/arith_nl_compare_proof_gen.cpp +++ b/src/theory/arith/nl/ext/arith_nl_compare_proof_gen.cpp @@ -15,24 +15,27 @@ #include "theory/arith/nl/ext/arith_nl_compare_proof_gen.h" -#include "theory/arith/arith_utilities.h" -#include "theory/arith/nl/ext/monomial_check.h" #include "expr/attribute.h" #include "proof/proof.h" +#include "theory/arith/arith_utilities.h" +#include "theory/arith/nl/ext/monomial_check.h" namespace cvc5::internal { namespace theory { namespace arith { namespace nl { -ArithNlCompareProofGenerator::ArithNlCompareProofGenerator(Env& env) : EnvObj(env) {} +ArithNlCompareProofGenerator::ArithNlCompareProofGenerator(Env& env) + : EnvObj(env) +{ +} ArithNlCompareProofGenerator::~ArithNlCompareProofGenerator() {} std::shared_ptr ArithNlCompareProofGenerator::getProofFor(Node fact) { - Assert (fact.getKind()==Kind::IMPLIES); + Assert(fact.getKind() == Kind::IMPLIES); std::vector exp; - if (fact[0].getKind()==Kind::AND) + if (fact[0].getKind() == Kind::AND) { exp.insert(exp.end(), fact[0].begin(), fact[0].end()); } @@ -41,7 +44,8 @@ std::shared_ptr ArithNlCompareProofGenerator::getProofFor(Node fact) exp.emplace_back(fact[0]); } Node conc = fact[1]; - Trace("arith-nl-compare") << "Comparsion prove: " << exp << " => " << conc << std::endl; + Trace("arith-nl-compare") + << "Comparsion prove: " << exp << " => " << conc << std::endl; // get the expected form of the literals CDProof cdp(d_env); std::vector expc; @@ -54,7 +58,7 @@ std::shared_ptr ArithNlCompareProofGenerator::getProofFor(Node fact) continue; } expc.emplace_back(ec); - if (e!=ec) + if (e != ec) { Node eeq = e.eqNode(ec); cdp.addTrustedStep(eeq, TrustId::ARITH_NL_COMPARE_LIT_TRANSFORM, {}, {}); @@ -62,10 +66,11 @@ std::shared_ptr ArithNlCompareProofGenerator::getProofFor(Node fact) } } Node concc = getCompareLit(conc); - Assert (!concc.isNull()); - Trace("arith-nl-compare") << "...processed prove: " << expc << " => " << concc << std::endl; + Assert(!concc.isNull()); + Trace("arith-nl-compare") + << "...processed prove: " << expc << " => " << concc << std::endl; cdp.addStep(concc, ProofRule::MACRO_ARITH_NL_COMPARISON, expc, {concc}); - if (conc!=concc) + if (conc != concc) { Node ceq = concc.eqNode(conc); cdp.addTrustedStep(ceq, TrustId::ARITH_NL_COMPARE_LIT_TRANSFORM, {}, {}); @@ -76,9 +81,13 @@ std::shared_ptr ArithNlCompareProofGenerator::getProofFor(Node fact) return cdp.getProofFor(fact); } -std::string ArithNlCompareProofGenerator::identify() const { return "ArithNlCompareProofGenerator"; } +std::string ArithNlCompareProofGenerator::identify() const +{ + return "ArithNlCompareProofGenerator"; +} -Node ArithNlCompareProofGenerator::mkLit(NodeManager* nm, Kind k, const Node& a, const Node& b, bool isAbsolute) +Node ArithNlCompareProofGenerator::mkLit( + NodeManager* nm, Kind k, const Node& a, const Node& b, bool isAbsolute) { Node au = a; Node bu = b; @@ -87,7 +96,7 @@ Node ArithNlCompareProofGenerator::mkLit(NodeManager* nm, Kind k, const Node& a, au = nm->mkNode(Kind::ABS, au); bu = nm->mkNode(Kind::ABS, bu); } - if (k==Kind::EQUAL) + if (k == Kind::EQUAL) { return mkEquality(au, bu); } @@ -97,9 +106,15 @@ Node ArithNlCompareProofGenerator::mkLit(NodeManager* nm, Kind k, const Node& a, struct ArithNlCompareLitAttributeId { }; -using ArithNlCompareLitAttribute = expr::Attribute; +using ArithNlCompareLitAttribute = + expr::Attribute; -void ArithNlCompareProofGenerator::setCompareLit(NodeManager* nm, Node olit, Kind k, const Node& a, const Node& b, bool isAbsolute) +void ArithNlCompareProofGenerator::setCompareLit(NodeManager* nm, + Node olit, + Kind k, + const Node& a, + const Node& b, + bool isAbsolute) { Node lit = mkLit(nm, k, a, b, isAbsolute); ArithNlCompareLitAttribute ancla; @@ -116,4 +131,3 @@ Node ArithNlCompareProofGenerator::getCompareLit(const Node& olit) } // namespace arith } // namespace theory } // namespace cvc5::internal - diff --git a/src/theory/arith/nl/ext/arith_nl_compare_proof_gen.h b/src/theory/arith/nl/ext/arith_nl_compare_proof_gen.h index 4ee6033e47c..9b6f75a72e5 100644 --- a/src/theory/arith/nl/ext/arith_nl_compare_proof_gen.h +++ b/src/theory/arith/nl/ext/arith_nl_compare_proof_gen.h @@ -16,8 +16,8 @@ #ifndef CVC5__THEORY__ARITH__NL__EXT__ARITH_NL_COMPARE_PROOF_GEN_H #define CVC5__THEORY__ARITH__NL__EXT__ARITH_NL_COMPARE_PROOF_GEN_H -#include "smt/env_obj.h" #include "proof/proof_generator.h" +#include "smt/env_obj.h" namespace cvc5::internal { namespace theory { @@ -26,7 +26,7 @@ namespace nl { class ArithNlCompareProofGenerator : protected EnvObj, public ProofGenerator { -public: + public: ArithNlCompareProofGenerator(Env& env); virtual ~ArithNlCompareProofGenerator(); /** @@ -35,9 +35,15 @@ class ArithNlCompareProofGenerator : protected EnvObj, public ProofGenerator /** identify */ std::string identify() const override; /** Make literal */ - static Node mkLit(NodeManager* nm, Kind k, const Node& a, const Node& b, bool isAbsolute); + static Node mkLit( + NodeManager* nm, Kind k, const Node& a, const Node& b, bool isAbsolute); /** */ - static void setCompareLit(NodeManager* nm, Node olit, Kind k, const Node& a, const Node& b, bool isAbsolute); + static void setCompareLit(NodeManager* nm, + Node olit, + Kind k, + const Node& a, + const Node& b, + bool isAbsolute); /** */ static Node getCompareLit(const Node& olit); }; diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp index 440bb767126..6a343ae7029 100644 --- a/src/theory/arith/nl/ext/monomial_check.cpp +++ b/src/theory/arith/nl/ext/monomial_check.cpp @@ -31,7 +31,11 @@ namespace arith { namespace nl { MonomialCheck::MonomialCheck(Env& env, ExtState* data) - : EnvObj(env), d_data(data), d_ancPfGen(env.isTheoryProofProducing() ? new ArithNlCompareProofGenerator(env) : nullptr) + : EnvObj(env), + d_data(data), + d_ancPfGen(env.isTheoryProofProducing() + ? new ArithNlCompareProofGenerator(env) + : nullptr) { d_order_points.push_back(d_data->d_neg_one); d_order_points.push_back(d_data->d_zero); @@ -426,17 +430,18 @@ bool MonomialCheck::compareMonomial( } } Node cob = ob; - if (ob==d_data->d_one) + if (ob == d_data->d_one) { cob = mkOne(oa.getType()); } Node conc = mkLit(oa, ob, status, true); - Node clem = nm->mkNode( - Kind::IMPLIES, nm->mkAnd(exp), conc); + Node clem = nm->mkNode(Kind::IMPLIES, nm->mkAnd(exp), conc); Trace("nl-ext-comp-lemma") << "comparison lemma : " << clem << std::endl; // use special proof generator - lem.emplace_back( - InferenceId::ARITH_NL_COMPARISON, clem, LemmaProperty::NONE, d_ancPfGen.get()); + lem.emplace_back(InferenceId::ARITH_NL_COMPARISON, + clem, + LemmaProperty::NONE, + d_ancPfGen.get()); cmp_infers[status][oa][ob] = clem; } return true; @@ -728,8 +733,8 @@ void MonomialCheck::assignOrderIds(std::vector& vars, Node MonomialCheck::mkLit(Node a, Node b, int status, bool isAbsolute) const { - NodeManager * nm = nodeManager(); - if (status<0) + NodeManager* nm = nodeManager(); + if (status < 0) { status = -status; Node tmp = a; @@ -770,13 +775,13 @@ Node MonomialCheck::mkLit(Node a, Node b, int status, bool isAbsolute) const Node negate_b = nm->mkNode(Kind::NEG, b); ret = a_is_nonnegative.iteNode( b_is_nonnegative.iteNode(nm->mkNode(k, a, b), - nm->mkNode(k, a, negate_b)), + nm->mkNode(k, a, negate_b)), b_is_nonnegative.iteNode(nm->mkNode(k, negate_a, b), - nm->mkNode(k, negate_a, negate_b))); + nm->mkNode(k, negate_a, negate_b))); } } // if proofs are enabled, we ensure we remember what the literal represents - if (d_ancPfGen!=nullptr) + if (d_ancPfGen != nullptr) { ArithNlCompareProofGenerator::setCompareLit(nm, ret, k, a, b, isAbsolute); } diff --git a/src/theory/arith/nl/ext/monomial_check.h b/src/theory/arith/nl/ext/monomial_check.h index 943f2dda1b1..56e0a810457 100644 --- a/src/theory/arith/nl/ext/monomial_check.h +++ b/src/theory/arith/nl/ext/monomial_check.h @@ -18,9 +18,9 @@ #include "expr/node.h" #include "smt/env_obj.h" +#include "theory/arith/nl/ext/arith_nl_compare_proof_gen.h" #include "theory/arith/nl/ext/monomial.h" #include "theory/theory_inference.h" -#include "theory/arith/nl/ext/arith_nl_compare_proof_gen.h" namespace cvc5::internal { namespace theory { @@ -77,6 +77,7 @@ class MonomialCheck : protected EnvObj /** Make literal */ static Node mkLit(NodeManager* nm, Kind k, Node a, Node b, bool isAbsolute); + private: /** In the following functions, status states a relationship * between two arithmetic terms, where: diff --git a/src/theory/arith/nl/ext/proof_checker.cpp b/src/theory/arith/nl/ext/proof_checker.cpp index 864a0fdc722..6eec554e6e8 100644 --- a/src/theory/arith/nl/ext/proof_checker.cpp +++ b/src/theory/arith/nl/ext/proof_checker.cpp @@ -152,7 +152,7 @@ Node ExtProofRuleChecker::checkInternal(ProofRule id, nm->mkNode(Kind::GEQ, x, a), nm->mkNode(sgn == -1 ? Kind::LEQ : Kind::GEQ, y, b)))); } - else if (id ==ProofRule::MACRO_ARITH_NL_COMPARISON) + else if (id == ProofRule::MACRO_ARITH_NL_COMPARISON) { return args[0]; }