From b422b152b4a21400f200cc5133e43fc7073a08a1 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 24 Jun 2020 00:06:23 -0700 Subject: [unconstrained] Fix gathering of visited-once vars 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. --- src/preprocessing/passes/unconstrained_simplifier.cpp | 10 ++++++++++ test/regress/CMakeLists.txt | 1 + test/regress/regress0/unconstrained/issue4644.smt2 | 9 +++++++++ 3 files changed, 20 insertions(+) create mode 100644 test/regress/regress0/unconstrained/issue4644.smt2 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) -- cgit v1.2.3