diff options
| -rw-r--r-- | src/proof/lean/lean_post_processor.cpp | 4 | ||||
| -rw-r--r-- | src/proof/verit/verit_post_processor.cpp | 21 | ||||
| -rw-r--r-- | src/smt/proof_final_callback.cpp | 2 | ||||
| -rw-r--r-- | src/theory/builtin/proof_checker.cpp | 5 | ||||
| -rw-r--r-- | src/theory/builtin/proof_checker.h | 8 |
5 files changed, 17 insertions, 23 deletions
diff --git a/src/proof/lean/lean_post_processor.cpp b/src/proof/lean/lean_post_processor.cpp index 092a69a15..960bd17f7 100644 --- a/src/proof/lean/lean_post_processor.cpp +++ b/src/proof/lean/lean_post_processor.cpp @@ -104,9 +104,7 @@ bool LeanProofPostprocessCallback::update(Node res, *cdp); break; } - default: - { - return false; + default: { return false; } }; return true; diff --git a/src/proof/verit/verit_post_processor.cpp b/src/proof/verit/verit_post_processor.cpp index bedb1ab8d..2bfb9fef2 100644 --- a/src/proof/verit/verit_post_processor.cpp +++ b/src/proof/verit/verit_post_processor.cpp @@ -445,17 +445,11 @@ bool VeritProofPostprocessCallback::update(Node res, vrule = VeritRule::EQUIV_SIMPLIFY; break; } - case kind::LT: - { - [[fallthrough]]; + case kind::LT: { [[fallthrough]]; } - case kind::GT: - { - [[fallthrough]]; + case kind::GT: { [[fallthrough]]; } - case kind::GEQ: - { - [[fallthrough]]; + case kind::GEQ: { [[fallthrough]]; } case kind::LEQ: { @@ -483,8 +477,7 @@ bool VeritProofPostprocessCallback::update(Node res, vrule = VeritRule::QUANTIFIER_SIMPLIFY; break; } - default: - { + default: { }; } return addVeritStep( @@ -998,7 +991,7 @@ bool VeritProofPostprocessCallback::update(Node res, return addVeritStep(vp2, VeritRule::NOT_NOT, {}, {}, *cdp) && addVeritStep(vp1, VeritRule::NOT_NOT, {}, {}, *cdp) && addVeritStepFromOr( - res, VeritRule::RESOLUTION, {vp1, vp2}, {}, *cdp); + res, VeritRule::RESOLUTION, {vp1, vp2}, {}, *cdp); } // ======== Equality resolution // Children: (P1:F1, P2:(= F1 F2)) @@ -1843,7 +1836,7 @@ bool VeritProofPostprocessCallback::update(Node res, && addVeritStep(vp3, VeritRule::RESOLUTION, {vp1, vp2}, {}, *cdp) && addVeritStep(vp4, VeritRule::REORDER, {vp3}, {}, *cdp) && addVeritStepFromOr( - res, VeritRule::DUPLICATED_LITERALS, {vp4}, {}, *cdp); + res, VeritRule::DUPLICATED_LITERALS, {vp4}, {}, *cdp); } // ======== CNF ITE Neg version 1 // Children: () @@ -1925,7 +1918,7 @@ bool VeritProofPostprocessCallback::update(Node res, && addVeritStep(vp3, VeritRule::RESOLUTION, {vp1, vp2}, {}, *cdp) && addVeritStep(vp4, VeritRule::REORDER, {vp3}, {}, *cdp) && addVeritStepFromOr( - res, VeritRule::DUPLICATED_LITERALS, {vp4}, {}, *cdp); + res, VeritRule::DUPLICATED_LITERALS, {vp4}, {}, *cdp); } //================================================= Equality rules diff --git a/src/smt/proof_final_callback.cpp b/src/smt/proof_final_callback.cpp index 46c9cad0d..1c80cf365 100644 --- a/src/smt/proof_final_callback.cpp +++ b/src/smt/proof_final_callback.cpp @@ -31,7 +31,7 @@ namespace smt { ProofFinalCallback::ProofFinalCallback(ProofNodeManager* pnm) : d_ruleCount(smtStatisticsRegistry().registerHistogram<PfRule>( - "finalProof::ruleCount")), + "finalProof::ruleCount")), d_instRuleIds( smtStatisticsRegistry().registerHistogram<theory::InferenceId>( "finalProof::instRuleId")), diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp index 2442aa82e..97e367f4e 100644 --- a/src/theory/builtin/proof_checker.cpp +++ b/src/theory/builtin/proof_checker.cpp @@ -33,7 +33,10 @@ namespace cvc5 { namespace theory { namespace builtin { -BuiltinProofRuleChecker::BuiltinProofRuleChecker(Env& env) : d_env(env), d_rdb(nullptr) {} +BuiltinProofRuleChecker::BuiltinProofRuleChecker(Env& env) + : d_env(env), d_rdb(nullptr) +{ +} void BuiltinProofRuleChecker::registerTo(ProofChecker* pc) { diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h index 6270c2b12..61ed7b09c 100644 --- a/src/theory/builtin/proof_checker.h +++ b/src/theory/builtin/proof_checker.h @@ -105,10 +105,10 @@ class BuiltinProofRuleChecker : public ProofRuleChecker * @return The substituted, rewritten form of n. */ Node applySubstitutionRewrite(Node n, - const std::vector<Node>& exp, - MethodId ids = MethodId::SB_DEFAULT, - MethodId ida = MethodId::SBA_SEQUENTIAL, - MethodId idr = MethodId::RW_REWRITE); + const std::vector<Node>& exp, + MethodId ids = MethodId::SB_DEFAULT, + MethodId ida = MethodId::SBA_SEQUENTIAL, + MethodId idr = MethodId::RW_REWRITE); /** get a TheoryId from a node, return false if we fail */ static bool getTheoryId(TNode n, TheoryId& tid); |