diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-10-14 11:37:54 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-14 13:37:54 -0500 |
| commit | 155e35ec2b38771917312d35f784a2e35b4b41d3 (patch) | |
| tree | a2eb6ddce3d5aade46d6c9282509b51be147be91 | |
| parent | 9380d6fa2691da1bd8ce7c5501fde1e972ca7d3f (diff) | |
(proof-new) debug statements & docs for INT_TRUST (#5259)
| -rw-r--r-- | src/theory/arith/proof_checker.cpp | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/src/theory/arith/proof_checker.cpp b/src/theory/arith/proof_checker.cpp index 35c4a2e69..a28eb02df 100644 --- a/src/theory/arith/proof_checker.cpp +++ b/src/theory/arith/proof_checker.cpp @@ -33,8 +33,9 @@ void ArithProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::ARITH_TRICHOTOMY, this); pc->registerChecker(PfRule::INT_TIGHT_UB, this); pc->registerChecker(PfRule::INT_TIGHT_LB, this); - pc->registerChecker(PfRule::INT_TRUST, this); pc->registerChecker(PfRule::ARITH_OP_ELIM_AXIOM, this); + // trusted rules + pc->registerTrustedChecker(PfRule::INT_TRUST, this, 2); } Node ArithProofRuleChecker::checkInternal(PfRule id, @@ -252,6 +253,20 @@ Node ArithProofRuleChecker::checkInternal(PfRule id, } 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]; } |