diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-06-24 10:41:03 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-24 12:41:03 -0500 |
commit | be607a9d420f79fa3e6a1f2c9b8c0e1b49cd34ee (patch) | |
tree | 415a032372b68c4de093a5b493ed71b8a7fc6d3d /src | |
parent | feea2d248ebe0c024c9c5ed14a9f0bf34b06c146 (diff) |
[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.
Diffstat (limited to 'src')
-rw-r--r-- | src/preprocessing/passes/unconstrained_simplifier.cpp | 10 |
1 files changed, 10 insertions, 0 deletions
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; |