From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 24 Jun 2020 17:41:03 +0000 (-0700)
Subject: [unconstrained] Fix gathering of visited-once vars (#4652)
X-Git-Tag: cvc5-1.0.0~3177
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=be607a9d420f79fa3e6a1f2c9b8c0e1b49cd34ee;p=cvc5.git

[unconstrained] Fix gathering of visited-once vars (#4652)

Fixes #4644. This commit fixes an issue where the set `d_unconstrained`
in the unconstrained simplification pass was not computed correctly. The
problem was that visiting the same term multiple times did not remove
the variables appearing in that term from the visited-once set. A simple
example that triggers the issue is the following:

```
(set-logic ALL)
(declare-fun a () Bool)
(declare-fun b () Bool)
(assert (not (= a b)))
(assert (= a (= a b)))
(check-sat)
```

After running `UnconstrainedSimplifier::visitAll()` on both assertions,
we end up with `[b]` as our `d_unconstrained` set. We end up inferring
the substitution `(= a b) --> b` and get `(not b)` and `b`, which is
unsat even though the original problem is sat.

This commit fixes the issue by visiting all the children of a node if we
visit a node for a second time. This makes sure that we remove any
children from the visisted-once set.
---

diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp
index e20403d2a..7d1f66d65 100644
--- a/src/preprocessing/passes/unconstrained_simplifier.cpp
+++ b/src/preprocessing/passes/unconstrained_simplifier.cpp
@@ -75,6 +75,16 @@ void UnconstrainedSimplifier::visitAll(TNode assertion)
         {
           d_unconstrained.erase(current);
         }
+        else
+        {
+          // Also erase the children from the visited-once set when we visit a
+          // node a second time, otherwise variables in this node are not
+          // erased from the set of unconstrained variables.
+          for (TNode childNode : current)
+          {
+            toVisit.push_back(unc_preprocess_stack_element(childNode, current));
+          }
+        }
       }
       ++find->second;
       continue;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index bb0f311d1..7863c5ec0 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1178,6 +1178,7 @@ set(regress_0_tests
   regress0/unconstrained/bvult5.smt2
   regress0/unconstrained/geq.smt2
   regress0/unconstrained/gt.smt2
+  regress0/unconstrained/issue4644.smt2
   regress0/unconstrained/ite.smt2
   regress0/unconstrained/leq.smt2
   regress0/unconstrained/lt.smt2
diff --git a/test/regress/regress0/unconstrained/issue4644.smt2 b/test/regress/regress0/unconstrained/issue4644.smt2
new file mode 100644
index 000000000..aeb2bfc84
--- /dev/null
+++ b/test/regress/regress0/unconstrained/issue4644.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --unconstrained-simp
+(set-logic ALL)
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(assert (distinct a c))
+(assert (= a b (= b c)))
+(set-info :status sat)
+(check-sat)