From 3bbdafbc3f5683d04786efdd86db7f478f2ae522 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 17 Nov 2020 14:43:15 +0100 Subject: [PATCH] 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. --- .../arith/nl/ext/tangent_plane_check.cpp | 22 +++++++++++-------- 1 file changed, 13 insertions(+), 9 deletions(-) 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( -- 2.30.2