From e4a3d7e78b72d4a8c6704f346540893bab4e00ef Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Wed, 21 Oct 2020 11:40:02 -0700 Subject: [PATCH] (proof-new) arith: dedup literals in flattenImpl (#5320) TheoryArithPrivte uses flattenImplication to turn implications into clauses. This commit ensures that said clause does not have duplicate terms. This is important because when we write proofs related to the clause, the proof machinery doesn't like duplicates. --- src/theory/arith/theory_arith_private.cpp | 25 +++++++++++++++++++---- 1 file changed, 21 insertions(+), 4 deletions(-) diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 4422bb2db..e4fa4a82c 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -4541,23 +4541,40 @@ bool TheoryArithPrivate::tryToPropagate(RowIndex ridx, bool rowUp, ArithVar v, b Node flattenImplication(Node imp){ NodeBuilder<> nb(kind::OR); + std::unordered_set included; Node left = imp[0]; Node right = imp[1]; if(left.getKind() == kind::AND){ for(Node::iterator i = left.begin(), iend = left.end(); i != iend; ++i) { - nb << (*i).negate(); + if (!included.count((*i).negate())) + { + nb << (*i).negate(); + included.insert((*i).negate()); + } } }else{ - nb << left.negate(); + if (!included.count(left.negate())) + { + nb << left.negate(); + included.insert(left.negate()); + } } if(right.getKind() == kind::OR){ for(Node::iterator i = right.begin(), iend = right.end(); i != iend; ++i) { - nb << *i; + if (!included.count(*i)) + { + nb << *i; + included.insert(*i); + } } }else{ - nb << right; + if (!included.count(right)) + { + nb << right; + included.insert(right); + } } return nb; -- 2.30.2