diff options
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/constraint.cpp | 7 | ||||
-rw-r--r-- | src/theory/arith/pp_rewrite_eq.cpp | 5 | ||||
-rw-r--r-- | src/theory/arith/proof_checker.cpp | 22 |
3 files changed, 9 insertions, 25 deletions
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp index d8fc1c578..03db36bb5 100644 --- a/src/theory/arith/constraint.cpp +++ b/src/theory/arith/constraint.cpp @@ -29,6 +29,7 @@ #include "theory/arith/congruence_manager.h" #include "theory/arith/normal_form.h" #include "theory/arith/partial_model.h" +#include "theory/builtin/proof_checker.h" #include "theory/rewriter.h" using namespace std; @@ -1820,9 +1821,11 @@ std::shared_ptr<ProofNode> Constraint::externalExplain( } case ArithProofType::IntHoleAP: { - pf = pnm->mkNode(PfRule::INT_TRUST, + Node t = + builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_ARITH); + pf = pnm->mkNode(PfRule::THEORY_INFERENCE, children, - {getProofLiteral()}, + {getProofLiteral(), t}, getProofLiteral()); break; } diff --git a/src/theory/arith/pp_rewrite_eq.cpp b/src/theory/arith/pp_rewrite_eq.cpp index 45f972038..0f4d97b4d 100644 --- a/src/theory/arith/pp_rewrite_eq.cpp +++ b/src/theory/arith/pp_rewrite_eq.cpp @@ -16,6 +16,7 @@ #include "theory/arith/pp_rewrite_eq.h" #include "options/arith_options.h" +#include "theory/builtin/proof_checker.h" #include "theory/rewriter.h" namespace cvc5 { @@ -44,10 +45,12 @@ TrustNode PreprocessRewriteEq::ppRewriteEq(TNode atom) // don't need to rewrite terms since rewritten is not a non-standard op if (proofsEnabled()) { + Node t = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(THEORY_ARITH); return d_ppPfGen.mkTrustedRewrite( atom, rewritten, - d_pnm->mkNode(PfRule::INT_TRUST, {}, {atom.eqNode(rewritten)})); + d_pnm->mkNode( + PfRule::THEORY_INFERENCE, {}, {atom.eqNode(rewritten), t})); } return TrustNode::mkTrustRewrite(atom, rewritten, nullptr); } diff --git a/src/theory/arith/proof_checker.cpp b/src/theory/arith/proof_checker.cpp index 4e25ae76b..58de8e391 100644 --- a/src/theory/arith/proof_checker.cpp +++ b/src/theory/arith/proof_checker.cpp @@ -36,11 +36,8 @@ void ArithProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::INT_TIGHT_UB, this); pc->registerChecker(PfRule::INT_TIGHT_LB, this); pc->registerChecker(PfRule::ARITH_OP_ELIM_AXIOM, this); - pc->registerChecker(PfRule::ARITH_MULT_POS, this); pc->registerChecker(PfRule::ARITH_MULT_NEG, this); - // trusted rules - pc->registerTrustedChecker(PfRule::INT_TRUST, this, 2); } Node ArithProofRuleChecker::checkInternal(PfRule id, @@ -340,25 +337,6 @@ Node ArithProofRuleChecker::checkInternal(PfRule id, } // Check that all have the same constant: } - case PfRule::INT_TRUST: - { - if (Debug.isOn("arith::pf::check::trust")) - { - Debug("arith::pf::check::trust") << "Arith PfRule:" << id << std::endl; - Debug("arith::pf::check::trust") << " children: " << std::endl; - for (const auto& c : children) - { - Debug("arith::pf::check::trust") << " * " << c << std::endl; - } - Debug("arith::pf::check::trust") << " args:" << std::endl; - for (const auto& c : args) - { - Debug("arith::pf::check::trust") << " * " << c << std::endl; - } - } - Assert(args.size() == 1); - return args[0]; - } case PfRule::ARITH_OP_ELIM_AXIOM: { Assert(children.empty()); |