diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-05-19 11:31:42 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-05-19 11:31:42 -0700 |
commit | eebfe6389321c24329d9b58f699ad67486cc30e0 (patch) | |
tree | bad5241cde1df28cc61cd6a596eafa6fd28a6f15 /src | |
parent | 3b50dfe623f44e97d85449fa2a7566e81c639b47 (diff) |
Make SolveEq and PlusCombineLikeTerms idempotent (#4438)
Fixes #3692 and an assertion failure that came up during the test runs
for SMT-COMP. The bit-vector rewrites `SolveEq` and
`PlusCombineLikeTerms` were not always idempotent. At a high level,
`SolveEq` combines common terms from two sides of an equality and
`PlusCombineLikeTerms` combines common terms within an addition.
However, in doing so, these rewrites were reordering the operands of the
bit-vector addition based on the node ids of the terms that were
multiplied with their coefficients. Consider the addition `3 * x * y + 5
* y * z` (the bit-width does not matter). `PlusCombineLikeTerms` would
reorder this addition to `5 * y * z + 3 * x * y` if the node id of `y *
z` was smaller than the node id of `x * y`. The issue is that node ids
are not fixed for a given term: If we have a term `x * y` and that term
reaches ref count 0, we may get a different id for that same term if we
recreate it later on. When terms reach ref count 0, we don't immediately
delete them but add them to our set of zombies to be deleted whenever
the list of zombies grows larger than some fixed size. When applying
`SolveEq` and `PlusCombineLikeTerms` multiple times (even in direct
succession without doing anything else), the node order may change
because some of the terms like `x * y` may be zombies while others have
been deleted and get new ids, leading to the relative order of node ids
changing. I suspect that we could construct a case where we get into an
infinite rewrite loop.
This commit addresses the issue as follows: It does not perform the
rewrites `SolveEq` and `PlusCombineLikeTerms` if none of the operands
change. This makes the rewrites idempotent. Note however that we are
still not guaranteeing that a term has the same rewritten form
throughout an execution because the node ids may change if the term has
been freed in the meantime. However, this limitation is consistent with
other rewrites such as the reordering of equalities.
I am including the minimized test case from our run on SMT-LIB. I am
ommittin the test case from #3692 because I couldn't trigger it on
master (not surprising since the issue requires very specific
circumstances to actually occur). However, I was able to reproduce the
issue on the CVC4 version mentioned in the issue and confirmed that this
fix worked for that older version.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 33 |
1 files changed, 29 insertions, 4 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index a7638325c..cd705e27e 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -385,7 +385,7 @@ inline Node RewriteRule<PlusCombineLikeTerms>::apply(TNode node) std::map<Node, BitVector> factorToCoefficient; // combine like-terms - for (unsigned i = 0; i < node.getNumChildren(); ++i) + for (size_t i = 0, n = node.getNumChildren(); i < n; ++i) { TNode current = node[i]; updateCoefMap(current, size, factorToCoefficient, constSum); @@ -406,7 +406,18 @@ inline Node RewriteRule<PlusCombineLikeTerms>::apply(TNode node) children.push_back(utils::mkConst(constSum)); } - unsigned csize = children.size(); + size_t csize = children.size(); + if (csize == node.getNumChildren()) + { + // If we couldn't combine any terms, we don't perform the rewrite. This is + // important because we are otherwise reordering terms in the addition + // based on the node ids of the terms that are multiplied with the + // coefficients. Due to garbage collection we may see different id orders + // for those nodes even when we perform one rewrite directly after the + // other, so the rewrite wouldn't be idempotent. + return node; + } + return csize == 0 ? utils::mkZero(size) : utils::mkNaryNode(kind::BITVECTOR_PLUS, children); @@ -687,6 +698,14 @@ inline Node RewriteRule<SolveEq>::apply(TNode node) termRight = iRight->first; } + // Changed tracks whether there have been any changes to the coefficients or + // constants of the left- or right-hand side. We perform a rewrite only if + // that is the case. This is important because we are otherwise reordering + // terms in the addition based on the node ids of the terms that are + // multiplied with the coefficients. Due to garbage collection we may see + // different id orders for those nodes even when we perform one rewrite + // directly after the other, so the rewrite wouldn't be idempotent. + bool changed = false; bool incLeft, incRight; while (iLeft != iLeftEnd || iRight != iRightEnd) @@ -714,6 +733,7 @@ inline Node RewriteRule<SolveEq>::apply(TNode node) addToChildren(termRight, size, coeffRight - coeffLeft, childrenRight); } incLeft = incRight = true; + changed = true; } if (incLeft) { @@ -743,6 +763,7 @@ inline Node RewriteRule<SolveEq>::apply(TNode node) // they are if (rightConst != zero) { + changed |= (leftConst != zero); rightConst = rightConst - leftConst; leftConst = zero; if (rightConst != zero) @@ -770,6 +791,7 @@ inline Node RewriteRule<SolveEq>::apply(TNode node) // constant childrenRight.push_back(utils::mkConst(-leftConst)); childrenLeft.pop_back(); + changed = true; } if (childrenLeft.size() == 0) @@ -787,6 +809,7 @@ inline Node RewriteRule<SolveEq>::apply(TNode node) // constant newLeft = utils::mkConst(-rightConst); childrenRight.pop_back(); + changed = true; } else { @@ -807,8 +830,10 @@ inline Node RewriteRule<SolveEq>::apply(TNode node) newRight = utils::mkNaryNode(kind::BITVECTOR_PLUS, childrenRight); } - // Assert(newLeft == Rewriter::rewrite(newLeft)); - // Assert(newRight == Rewriter::rewrite(newRight)); + if (!changed) + { + return node; + } if (newLeft == newRight) { |