From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Mon, 16 Nov 2020 17:51:58 +0000 (+0100)
Subject: Refactor tangent plane lemmas (#5449)
X-Git-Tag: cvc5-1.0.0~2594
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2b504cd20b7cbbd0a3e7473162c7640907faf04d;p=cvc5.git

Refactor tangent plane lemmas (#5449)

The original lemma only proposed an implication for the tangent plane lemmas, while our implementation adds the inverse implication as well (in a somewhat verbose way).
This PR replaces this by simply constructing the equivalence.
---

diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp
index ff66be0e4..e57383adb 100644
--- a/src/theory/arith/nl/ext/tangent_plane_check.cpp
+++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp
@@ -114,8 +114,9 @@ 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));
-            // conjuncts of the tangent plane lemma
-            std::vector<Node> tplaneConj;
+            // construct the equivalent of 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++)
             {
               Node aa =
@@ -123,68 +124,13 @@ void TangentPlaneCheck::check(bool asWaitingLemmas)
               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::OR, aa.negate(), ab.negate(), conc);
+              Node tlem =
+                  nm->mkNode(Kind::EQUAL, nm->mkNode(Kind::AND, aa, ab), conc);
               Trace("nl-ext-tplanes")
                   << "Tangent plane lemma : " << tlem << std::endl;
-              tplaneConj.push_back(tlem);
+              d_data->d_im.addPendingArithLemma(
+                  tlem, InferenceId::NL_TANGENT_PLANE, asWaitingLemmas);
             }
-
-            // tangent plane reverse implication
-
-            // t <= tplane -> ( (a <= a_v ^ b >= b_v) v
-            // (a >= a_v ^ b <= b_v) ).
-            // in clause form, the above becomes
-            // t <= tplane -> a <= a_v v b <= b_v.
-            // t <= tplane -> b >= b_v v a >= a_v.
-            Node a_leq_av = nm->mkNode(Kind::LEQ, a, a_v);
-            Node b_leq_bv = nm->mkNode(Kind::LEQ, b, b_v);
-            Node a_geq_av = nm->mkNode(Kind::GEQ, a, a_v);
-            Node b_geq_bv = nm->mkNode(Kind::GEQ, b, b_v);
-
-            Node t_leq_tplane = nm->mkNode(Kind::LEQ, t, tplane);
-            Node a_leq_av_or_b_leq_bv =
-                nm->mkNode(Kind::OR, a_leq_av, b_leq_bv);
-            Node b_geq_bv_or_a_geq_av =
-                nm->mkNode(Kind::OR, b_geq_bv, a_geq_av);
-            Node ub_reverse1 = nm->mkNode(
-                Kind::OR, t_leq_tplane.negate(), a_leq_av_or_b_leq_bv);
-            Trace("nl-ext-tplanes")
-                << "Tangent plane lemma (reverse) : " << ub_reverse1
-                << std::endl;
-            tplaneConj.push_back(ub_reverse1);
-            Node ub_reverse2 = nm->mkNode(
-                Kind::OR, t_leq_tplane.negate(), b_geq_bv_or_a_geq_av);
-            Trace("nl-ext-tplanes")
-                << "Tangent plane lemma (reverse) : " << ub_reverse2
-                << std::endl;
-            tplaneConj.push_back(ub_reverse2);
-
-            // t >= tplane -> ( (a <= a_v ^ b <= b_v) v
-            // (a >= a_v ^ b >= b_v) ).
-            // in clause form, the above becomes
-            // t >= tplane -> a <= a_v v b >= b_v.
-            // t >= tplane -> b >= b_v v a <= a_v
-            Node t_geq_tplane = nm->mkNode(Kind::GEQ, t, tplane);
-            Node a_leq_av_or_b_geq_bv =
-                nm->mkNode(Kind::OR, a_leq_av, b_geq_bv);
-            Node a_geq_av_or_b_leq_bv =
-                nm->mkNode(Kind::OR, a_geq_av, b_leq_bv);
-            Node lb_reverse1 = nm->mkNode(
-                Kind::OR, t_geq_tplane.negate(), a_leq_av_or_b_geq_bv);
-            Trace("nl-ext-tplanes")
-                << "Tangent plane lemma (reverse) : " << lb_reverse1
-                << std::endl;
-            tplaneConj.push_back(lb_reverse1);
-            Node lb_reverse2 = nm->mkNode(
-                Kind::OR, t_geq_tplane.negate(), a_geq_av_or_b_leq_bv);
-            Trace("nl-ext-tplanes")
-                << "Tangent plane lemma (reverse) : " << lb_reverse2
-                << std::endl;
-            tplaneConj.push_back(lb_reverse2);
-
-            Node tlem = nm->mkAnd(tplaneConj);
-            d_data->d_im.addPendingArithLemma(
-                tlem, InferenceId::NL_TANGENT_PLANE, asWaitingLemmas);
           }
         }
       }