diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-23 19:33:18 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-08-24 00:33:18 +0000 |
commit | 3b76dcf208986709fefbd0978982de3fe8ecc626 (patch) | |
tree | d7dd101c4664ed59e9a268275eff14dfdebca094 /src/theory/arith/proof_checker.cpp | |
parent | fe655f21e7cea33e9057c46fc8b2573314cbf302 (diff) |
Uniform treatment of trusted theory inferences in proofs (#7044)
Makes it so that all theory-specific proof rules for this purpose are replaced by the generic THEORY_INFERENCE.
Diffstat (limited to 'src/theory/arith/proof_checker.cpp')
-rw-r--r-- | src/theory/arith/proof_checker.cpp | 22 |
1 files changed, 0 insertions, 22 deletions
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()); |