diff options
Diffstat (limited to 'src/theory')
| -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; } |