From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Tue, 17 Nov 2020 13:43:15 +0000 (+0100)
Subject: Fix tangent plane lemmas (#5455)
X-Git-Tag: cvc5-1.0.0~2593
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3bbdafbc3f5683d04786efdd86db7f478f2ae522;p=cvc5.git

Fix tangent plane lemmas (#5455)

The previous refactoring of tangent plane lemmas introduced incorrect lemmas.
This PR fixes this issue and actually generated the lemmas described in the comment.
Fixes #5452.
---

diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp
index e57383adb..5235b7d43 100644
--- a/src/theory/arith/nl/ext/tangent_plane_check.cpp
+++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp
@@ -114,18 +114,22 @@ void TangentPlaneCheck::check(bool asWaitingLemmas)
                                                 nm->mkNode(Kind::MULT, b_v, a),
                                                 nm->mkNode(Kind::MULT, a_v, b)),
                                      nm->mkNode(Kind::MULT, a_v, b_v));
-            // construct the equivalent of the following lemmas:
+            // construct the following lemmas:
             // t <= tplane  <=>  ((a <= a_v ^ b >= b_v) v (a >= a_v ^ b <= b_v))
             // t >= tplane  <=>  ((a <= a_v ^ b <= b_v) v (a >= a_v ^ b >= b_v))
-            for (unsigned d = 0; d < 4; d++)
+
+            for (unsigned d = 0; d < 2; d++)
             {
-              Node aa =
-                  nm->mkNode(d == 0 || d == 3 ? Kind::GEQ : Kind::LEQ, a, a_v);
-              Node ab =
-                  nm->mkNode(d == 1 || d == 3 ? Kind::GEQ : Kind::LEQ, b, b_v);
-              Node conc = nm->mkNode(d <= 1 ? Kind::LEQ : Kind::GEQ, t, tplane);
-              Node tlem =
-                  nm->mkNode(Kind::EQUAL, nm->mkNode(Kind::AND, aa, ab), conc);
+              Node b1 = nm->mkNode(d == 0 ? Kind::GEQ : Kind::LEQ, b, b_v);
+              Node b2 = nm->mkNode(d == 0 ? Kind::LEQ : Kind::GEQ, b, b_v);
+              Node tlem = nm->mkNode(
+                  Kind::EQUAL,
+                  nm->mkNode(d == 0 ? Kind::LEQ : Kind::GEQ, t, tplane),
+                  nm->mkNode(
+                      Kind::OR,
+                      nm->mkNode(Kind::AND, nm->mkNode(Kind::LEQ, a, a_v), b1),
+                      nm->mkNode(
+                          Kind::AND, nm->mkNode(Kind::GEQ, a, a_v), b2)));
               Trace("nl-ext-tplanes")
                   << "Tangent plane lemma : " << tlem << std::endl;
               d_data->d_im.addPendingArithLemma(