From: Alex Ozdemir <aozdemir@hmc.edu>
Date: Wed, 14 Oct 2020 18:37:54 +0000 (-0700)
Subject: (proof-new) debug statements & docs for INT_TRUST (#5259)
X-Git-Tag: cvc5-1.0.0~2709
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=155e35ec2b38771917312d35f784a2e35b4b41d3;p=cvc5.git

(proof-new) debug statements & docs for INT_TRUST (#5259)
---

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];
     }