From 6e4a5a8c865469aebec9d070c8c1976fed68914a Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Sun, 31 May 2020 09:13:39 -0700 Subject: [PATCH] Do not cache operator eliminations in arith (#4542) Fixes #4525. The actual problem in the issue is not that the unsat core is satisfiable but that our unsat core check is not working as intended. Our unsat core check uses the same `ExprManager` as the main `SmtEngine` and thus also shares the same attributes for nodes. However, since we have a different `SmtEngine` instance for the check, we also have different instances of `TheoryArith`. This leads to the check failing due to the following: - Our only input assertion is `(> (cot 0.0) (/ 1 0)))`. - `TheoryArith::expandDefinition()` gets called on `(> (cot 0.0) (/ 1 0))` but nothing happens. - `TheoryArith::expandDefinition()` gets called on `(/ 1 0)`, which gets expanded as expected but no attribute is set because it happens in a simple `TheoryArith::eliminateOperators()` call. - `TheoryArith::expandDefinition()` on `(cot (/ 0 1))` first expands to `(/ 1 0)` (not cached) and then we expand it recursively to the expected term and cache `(/ 1 0) ---> (ite (= 0 0) (divByZero 1.0) (/ 1 0))`. Up to this point, things are suboptimal but there are no correctness issues. The problem starts when we do the same process in the unsat core check: - Our only input assertion is again `(> (cot 0.0) (/ 1 0)))`. - `TheoryArith::expandDefinition()` gets called on `(> (cot 0.0) (/ 1 0))` but nothing happens. - `TheoryArith::expandDefinition()` gets called on `(/ 1 0)`, which gets expanded as expected but no attribute is set or checked because it happens in a simple `TheoryArith::eliminateOperators()` call. Note that the skolem introduced here for the division-by-zero case is different from the skolem introduced above because this is in a different `TheoryArith` instance that does not know the existing skolems. - `TheoryArith::expandDefinition()` on `(cot (/ 0 1))` first expands to `(/ 1 0)` (not cached) and then we use the cache from our solving call to expand it `(/ 1 0) ---> (ite (= 0 0) (divByZero 1.0) (/ 1 0))`. Note that `divByZero` here is the skolem from the main solver. As a result, the preprocessed assertions mix skolems from the main `SmtEngine` with the `SmtEngine` of the unsat core check, making the constraints satisfiable. To solve this problem, this commit removes the caching-by-attribute mechanism. The reason for removing it is that it is currently ineffective (since most eliminations do not seem to be cached) and there are caches at other levels, e.g. when expanding definitions. If we deem the operator elimination to be a bottleneck, we can introduce a similar mechanism at the level of `TheoryArith`. --- src/theory/arith/theory_arith_private.cpp | 22 ++++------------------ test/regress/CMakeLists.txt | 1 + test/regress/regress0/arith/issue4525.smt2 | 4 ++++ 3 files changed, 9 insertions(+), 18 deletions(-) create mode 100644 test/regress/regress0/arith/issue4525.smt2 diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 09b6d742a..638f5250e 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1112,14 +1112,8 @@ void TheoryArithPrivate::checkNonLinearLogic(Node term) } } -struct ArithElimOpAttributeId -{ -}; -typedef expr::Attribute ArithElimOpAttribute; - Node TheoryArithPrivate::eliminateOperatorsRec(Node n) { - ArithElimOpAttribute aeoa; Trace("arith-elim") << "Begin elim: " << n << std::endl; NodeManager* nm = NodeManager::currentNM(); std::unordered_map visited; @@ -1138,18 +1132,11 @@ Node TheoryArithPrivate::eliminateOperatorsRec(Node n) } else if (it == visited.end()) { - if (cur.hasAttribute(aeoa)) - { - visited[cur] = cur.getAttribute(aeoa); - } - else + visited[cur] = Node::null(); + visit.push_back(cur); + for (const Node& cn : cur) { - visited[cur] = Node::null(); - visit.push_back(cur); - for (const Node& cn : cur) - { - visit.push_back(cn); - } + visit.push_back(cn); } } else if (it->second.isNull()) @@ -1180,7 +1167,6 @@ Node TheoryArithPrivate::eliminateOperatorsRec(Node n) // are defined in terms of other non-standard operators. ret = eliminateOperatorsRec(retElim); } - cur.setAttribute(aeoa, ret); visited[cur] = ret; } } while (!visit.empty()); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index fbf249e7f..38c60e0e3 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -37,6 +37,7 @@ set(regress_0_tests regress0/arith/issue3413.smt2 regress0/arith/issue3480.smt2 regress0/arith/issue3683.smt2 + regress0/arith/issue4525.smt2 regress0/arith/ite-lift.smt2 regress0/arith/leq.01.smtv1.smt2 regress0/arith/miplib.cvc diff --git a/test/regress/regress0/arith/issue4525.smt2 b/test/regress/regress0/arith/issue4525.smt2 new file mode 100644 index 000000000..ae7e00990 --- /dev/null +++ b/test/regress/regress0/arith/issue4525.smt2 @@ -0,0 +1,4 @@ +(set-logic QF_NRAT) +(assert (> (cot 0.0) (/ 1 0))) +(set-info :status unsat) +(check-sat) -- 2.30.2