From be607a9d420f79fa3e6a1f2c9b8c0e1b49cd34ee Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 24 Jun 2020 10:41:03 -0700 Subject: [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. --- src/preprocessing/passes/unconstrained_simplifier.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'src/preprocessing/passes') 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; -- cgit v1.2.3