From 2b504cd20b7cbbd0a3e7473162c7640907faf04d Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 16 Nov 2020 18:51:58 +0100 Subject: [PATCH] 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. --- .../arith/nl/ext/tangent_plane_check.cpp | 68 ++----------------- 1 file changed, 7 insertions(+), 61 deletions(-) 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 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); } } } -- 2.30.2