diff --git a/src/api/cpp/cvc5_proof_rule_template.cpp b/src/api/cpp/cvc5_proof_rule_template.cpp index a8cc6e86310..10ec02e32c3 100644 --- a/src/api/cpp/cvc5_proof_rule_template.cpp +++ b/src/api/cpp/cvc5_proof_rule_template.cpp @@ -130,7 +130,8 @@ const char* toString(ProofRule rule) case ProofRule::QUANT_VAR_REORDERING: return "QUANT_VAR_REORDERING"; case ProofRule::EXISTS_STRING_LENGTH: return "EXISTS_STRING_LENGTH"; case ProofRule::EXISTS_INV_CONDITION: return "EXISTS_INV_CONDITION"; - case ProofRule::MACRO_EXISTS_INV_CONDITION: return "MACRO_EXISTS_INV_CONDITION"; + case ProofRule::MACRO_EXISTS_INV_CONDITION: + return "MACRO_EXISTS_INV_CONDITION"; //================================================= Sets rules case ProofRule::SETS_SINGLETON_INJ: return "SETS_SINGLETON_INJ"; case ProofRule::SETS_EXT: return "SETS_EXT"; diff --git a/src/expr/elim_witness_converter.h b/src/expr/elim_witness_converter.h index c4aef9f66f0..78226a77bda 100644 --- a/src/expr/elim_witness_converter.h +++ b/src/expr/elim_witness_converter.h @@ -29,7 +29,7 @@ namespace cvc5::internal { * Node converter to eliminate all terms of kind WITNESS. Each term replaced * in this way is captured by a skolem that witnesses the axiom for that * witness. - * + * * Witness terms are required to track their justification as part of their * AST. In particular, it is required that all terms of kind WITNESS are given * an instantiation attribute of the form: @@ -47,7 +47,7 @@ namespace cvc5::internal { * For each witness of this form, we replace the witness by its corresponding * skolem and collect its corresponding axiom, defining what lemma we can * assume about it, which can be retrieved via ::getAxioms in this class. - * + * * Note that we use WITNESS terms for two reasons: * (1) (witness x (= x t)) can naturally rewrite to t, which we wish to * infer when applicable by substitution + rewriting. diff --git a/src/theory/arith/arith_proof_rcons.cpp b/src/theory/arith/arith_proof_rcons.cpp index 226989606d8..6cd6d45b66d 100644 --- a/src/theory/arith/arith_proof_rcons.cpp +++ b/src/theory/arith/arith_proof_rcons.cpp @@ -15,16 +15,16 @@ #include "theory/arith/arith_proof_rcons.h" +#include "expr/term_context.h" +#include "proof/conv_proof_generator.h" #include "proof/proof.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_subs.h" -#include "proof/conv_proof_generator.h" -#include "expr/term_context.h" namespace cvc5::internal { namespace theory { namespace arith { - + /** * Arithmetic substitution term context. */ @@ -37,7 +37,7 @@ class ArithSubsTermContext : public TermContext /** Compute the value of the index^th child of t whose hash is tval */ uint32_t computeValue(TNode t, uint32_t tval, size_t index) const override { - if (tval==0) + if (tval == 0) { // if we should not traverse, return 1 if (!ArithSubs::shouldTraverse(t)) @@ -78,8 +78,12 @@ std::shared_ptr ArithProofRCons::getProofFor(Node fact) ArithSubs asubs; std::vector assumpsNoSolve; ArithSubsTermContext astc; - TConvProofGenerator tcnv(d_env, nullptr, TConvPolicy::FIXPOINT, TConvCachePolicy::NEVER, - "ArithRConsTConv", &astc); + TConvProofGenerator tcnv(d_env, + nullptr, + TConvPolicy::FIXPOINT, + TConvCachePolicy::NEVER, + "ArithRConsTConv", + &astc); Node tgtAssump; // prove false for (const Node& a : assumps) @@ -98,10 +102,10 @@ std::shared_ptr ArithProofRCons::getProofFor(Node fact) if (asr == d_false) { Trace("arith-proof-rcons") << "...success!" << std::endl; - if (a!=as) + if (a != as) { std::shared_ptr pfn = tcnv.getProofForRewriting(a); - Assert (pfn.getResult()[1]==as); + Assert(pfn.getResult()[1] == as); cdp.addProof(pfn); cdp.addStep(as, ProofRule::EQ_RESOLVE, {a, a.eqNode(as)}, {}); } @@ -129,14 +133,14 @@ std::shared_ptr ArithProofRCons::getProofFor(Node fact) Trace("arith-proof-rcons") << "...solved " << m.first << " = " << val << std::endl; Node eq = m.first.eqNode(val); - if (a!=as) + if (a != as) { std::shared_ptr pfn = tcnv.getProofForRewriting(a); - Assert (pfn.getResult()[1]==as); + Assert(pfn.getResult()[1] == as); cdp.addProof(pfn); cdp.addStep(as, ProofRule::EQ_RESOLVE, {a, a.eqNode(as)}, {}); } - if (as!=eq) + if (as != eq) { cdp.addStep(eq, ProofRule::MACRO_SR_PRED_TRANSFORM, {as}, {eq}); } @@ -165,14 +169,14 @@ std::shared_ptr ArithProofRCons::getProofFor(Node fact) Node as = asubs.applyArith(a); Node asr = rewrite(as); Trace("arith-proof-rcons") << "...have " << asr << std::endl; - if (a!=as) + if (a != as) { std::shared_ptr pfn = tcnv.getProofForRewriting(a); - Assert (pfn.getResult()[1]==as); + Assert(pfn.getResult()[1] == as); cdp.addProof(pfn); cdp.addStep(as, ProofRule::EQ_RESOLVE, {a, a.eqNode(as)}, {}); } - if (as!=asr) + if (as != asr) { cdp.addStep(asr, ProofRule::MACRO_SR_PRED_TRANSFORM, {as}, {asr}); } diff --git a/src/theory/arith/arith_subs.cpp b/src/theory/arith/arith_subs.cpp index c401e35316c..709cf3ec3d0 100644 --- a/src/theory/arith/arith_subs.cpp +++ b/src/theory/arith/arith_subs.cpp @@ -109,11 +109,9 @@ bool ArithSubs::shouldTraverse(const Node& n, bool traverseNlMult) { Kind k = n.getKind(); TheoryId ctid = theory::kindToTheoryId(k); - if ((ctid != THEORY_ARITH && ctid != THEORY_BOOL - && ctid != THEORY_BUILTIN) + if ((ctid != THEORY_ARITH && ctid != THEORY_BOOL && ctid != THEORY_BUILTIN) || isTranscendentalKind(k) - || (!traverseNlMult - && (k == Kind::NONLINEAR_MULT || k == Kind::IAND))) + || (!traverseNlMult && (k == Kind::NONLINEAR_MULT || k == Kind::IAND))) { return false; } diff --git a/src/theory/arith/arith_subs.h b/src/theory/arith/arith_subs.h index be3160d37d6..3799d0409c6 100644 --- a/src/theory/arith/arith_subs.h +++ b/src/theory/arith/arith_subs.h @@ -47,10 +47,10 @@ class ArithSubs : public Subs * @param traverseNlMult Whether to traverse applications of NONLINEAR_MULT. */ Node applyArith(const Node& n, bool traverseNlMult = true) const; - /** + /** * Should traverse, returns true if the above method traverses n. */ - static bool shouldTraverse(const Node& n, bool traverseNlMult = true); + static bool shouldTraverse(const Node& n, bool traverseNlMult = true); }; } // namespace arith