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`.

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 09b6d742a36faa817d45b1296c29913142077c9b..638f5250ebcadea0601b58589a77661c3aaba302 100644 (file)
--- 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<ArithElimOpAttributeId, Node> ArithElimOpAttribute;
-
 Node TheoryArithPrivate::eliminateOperatorsRec(Node n)
 {
-  ArithElimOpAttribute aeoa;
   Trace("arith-elim") << "Begin elim: " << n << std::endl;
   NodeManager* nm = NodeManager::currentNM();
   std::unordered_map<Node, Node, TNodeHashFunction> 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 fbf249e7fbd5535251475a9ec8785b79df244a5c..38c60e0e3b7a501dbc5fbd34b269156ff17cf61f 100644 (file)
--- 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 (file)
index 0000000..ae7e009
--- /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)