From: Gereon Kremer <gkremer@stanford.edu>
Date: Fri, 18 Dec 2020 15:25:06 +0000 (+0100)
Subject: Add proof checker for nl tangent lemma (#5704)
X-Git-Tag: cvc5-1.0.0~2422
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=879bc5c29cbfc8ebcfe69fcc9316dfdb1361ff1f;p=cvc5.git

Add proof checker for nl tangent lemma (#5704)

This PR is a follow-up to #5700 which lacked the proof checker for the proof that was added for nonlinear tangent plane lemmas.
---

diff --git a/src/theory/arith/nl/ext/proof_checker.cpp b/src/theory/arith/nl/ext/proof_checker.cpp
index 57ef378b6..8c594f1df 100644
--- a/src/theory/arith/nl/ext/proof_checker.cpp
+++ b/src/theory/arith/nl/ext/proof_checker.cpp
@@ -27,6 +27,7 @@ namespace nl {
 
 void ExtProofRuleChecker::registerTo(ProofChecker* pc)
 {
+  pc->registerChecker(PfRule::ARITH_MULT_TANGENT, this);
 }
 
 Node ExtProofRuleChecker::checkInternal(PfRule id,
@@ -44,6 +45,41 @@ Node ExtProofRuleChecker::checkInternal(PfRule id,
   {
     Trace("nl-ext-checker") << "\t" << c << std::endl;
   }
+  if (id == PfRule::ARITH_MULT_TANGENT)
+  {
+    Assert(children.empty());
+    Assert(args.size() == 6);
+    Assert(args[0].getType().isReal());
+    Assert(args[1].getType().isReal());
+    Assert(args[2].getType().isReal());
+    Assert(args[3].getType().isReal());
+    Assert(args[4].getType().isReal());
+    Assert(args[5].isConst() && args[5].getKind() == Kind::CONST_RATIONAL
+           && args[5].getConst<Rational>().isIntegral());
+    Node t = args[0];
+    Node x = args[1];
+    Node y = args[2];
+    Node a = args[3];
+    Node b = args[4];
+    int sgn = args[5].getConst<Rational>().getNumerator().sgn();
+    Assert(sgn == -1 || sgn == 1);
+    Node tplane = nm->mkNode(Kind::MINUS,
+                             nm->mkNode(Kind::PLUS,
+                                        nm->mkNode(Kind::MULT, b, x),
+                                        nm->mkNode(Kind::MULT, a, y)),
+                             nm->mkNode(Kind::MULT, a, b));
+    return nm->mkNode(
+        Kind::EQUAL,
+        nm->mkNode(sgn == -1 ? Kind::LEQ : Kind::GEQ, t, tplane),
+        nm->mkNode(
+            Kind::OR,
+            nm->mkNode(Kind::AND,
+                       nm->mkNode(Kind::LEQ, x, a),
+                       nm->mkNode(sgn == -1 ? Kind::GEQ : Kind::LEQ, y, b)),
+            nm->mkNode(Kind::AND,
+                       nm->mkNode(Kind::GEQ, x, a),
+                       nm->mkNode(sgn == -1 ? Kind::LEQ : Kind::GEQ, y, b))));
+  }
   return Node::null();
 }