From 155e35ec2b38771917312d35f784a2e35b4b41d3 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Wed, 14 Oct 2020 11:37:54 -0700 Subject: (proof-new) debug statements & docs for INT_TRUST (#5259) --- src/theory/arith/proof_checker.cpp | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) (limited to 'src/theory/arith/proof_checker.cpp') 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]; } -- cgit v1.2.3