diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-07 11:30:00 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-07 16:02:56 -0400 |
| commit | 0d8c1936b8b8159af5f6688e63d74a806f48ac75 (patch) | |
| tree | db0ac86baefc3f93e363f797a379ba9fdc0eb68c /src/theory/arrays | |
| parent | 931b5641dfffcd3779239e014406aa057e21e0f7 (diff) | |
Fix for bug 517.
Diffstat (limited to 'src/theory/arrays')
| -rw-r--r-- | src/theory/arrays/theory_arrays_rewriter.h | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 18bbef8cf..5df06bda8 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -36,6 +36,10 @@ namespace attr { typedef expr::Attribute<attr::ArrayConstantMostFrequentValueCountTag, uint64_t> ArrayConstantMostFrequentValueCountAttr; typedef expr::Attribute<attr::ArrayConstantMostFrequentValueTag, Node> ArrayConstantMostFrequentValueAttr; +static inline Node mkEqNode(Node a, Node b) { + return a.getType().isBoolean() ? a.iffNode(b) : a.eqNode(b); +} + class TheoryArraysRewriter { static Node normalizeConstant(TNode node) { return normalizeConstant(node, node[1].getType().getCardinality()); @@ -244,7 +248,7 @@ public: val = false; } else { - n = Rewriter::rewrite(store[1].eqNode(index)); + n = Rewriter::rewrite(mkEqNode(store[1], index)); if (n.getKind() != kind::CONST_BOOLEAN) { break; } @@ -301,7 +305,7 @@ public: val = false; } else { - Node eqRewritten = Rewriter::rewrite(store[1].eqNode(index)); + Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index)); if (eqRewritten.getKind() != kind::CONST_BOOLEAN) { Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << node << std::endl; return RewriteResponse(REWRITE_DONE, node); @@ -340,7 +344,7 @@ public: val = false; } else { - n = Rewriter::rewrite(store[1].eqNode(index)); + n = Rewriter::rewrite(mkEqNode(store[1], index)); if (n.getKind() != kind::CONST_BOOLEAN) { break; } @@ -416,7 +420,7 @@ public: val = false; } else { - n = Rewriter::rewrite(store[1].eqNode(index)); + n = Rewriter::rewrite(mkEqNode(store[1], index)); if (n.getKind() != kind::CONST_BOOLEAN) { break; } @@ -466,7 +470,7 @@ public: val = false; } else { - Node eqRewritten = Rewriter::rewrite(store[1].eqNode(index)); + Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index)); if (eqRewritten.getKind() != kind::CONST_BOOLEAN) { break; } |