diff options
| -rw-r--r-- | src/theory/arrays/arrays_post.h | 60 |
1 files changed, 23 insertions, 37 deletions
diff --git a/src/theory/arrays/arrays_post.h b/src/theory/arrays/arrays_post.h index 3e29d77f4..2d3bdaffe 100644 --- a/src/theory/arrays/arrays_post.h +++ b/src/theory/arrays/arrays_post.h @@ -136,45 +136,13 @@ template <bool Proof> inline RewriteResponse arrays_post_rewrite8(TNode node, RewriteProof *proof) { NodeManager *nm = NodeManager::currentNM(); if ((node).getKind() == kind::SELECT) { - if (((node[0]).getKind() == kind::STORE) && - (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) == - nm->mkConst(false))) { - if (Proof) { - proof->registerRewrite(arrays_post_SELECT_STORE_DIFF_I_J); - }; - Node rewritten_node = nm->mkNode(kind::SELECT, node[0][0], node[1]); - return arrays_post_rewrite7<Proof>(rewritten_node, proof); - }; - if (((node[0]).getKind() == kind::STORE) && - ((((node[0][1]).isConst()) && ((node[1]).isConst())) && - ((node[0][1] != node[1])))) { - if (Proof) { - proof->registerRewrite(arrays_post_SELECT_STORE_DIFF_CONSTS); - }; - Node rewritten_node = nm->mkNode(kind::SELECT, node[0][0], node[1]); - return arrays_post_rewrite7<Proof>(rewritten_node, proof); - } - }; - return arrays_post_rewrite6<Proof>(node, proof); -} - -template <bool Proof> -inline RewriteResponse arrays_post_rewrite9(TNode node, RewriteProof *proof) { - NodeManager *nm = NodeManager::currentNM(); - return RewriteResponse(REWRITE_DONE, node); -} - -template <bool Proof> -inline RewriteResponse arrays_post_rewrite10(TNode node, RewriteProof *proof) { - NodeManager *nm = NodeManager::currentNM(); - if ((node).getKind() == kind::SELECT) { if (((node[0]).getKind() == kind::STORE) && (true) && (node[0][1] == node[1])) { if (Proof) { proof->registerRewrite(arrays_post_SELECT_STORE_I_I); }; Node rewritten_node = node[0][2]; - return arrays_post_rewrite9<Proof>(rewritten_node, proof); + return arrays_post_rewrite7<Proof>(rewritten_node, proof); }; if (((node[0]).getKind() == kind::STORE) && (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) == @@ -183,7 +151,7 @@ inline RewriteResponse arrays_post_rewrite10(TNode node, RewriteProof *proof) { proof->registerRewrite(arrays_post_SELECT_STORE_I_J); }; Node rewritten_node = node[0][2]; - return arrays_post_rewrite9<Proof>(rewritten_node, proof); + return arrays_post_rewrite7<Proof>(rewritten_node, proof); }; if (((node[0]).getKind() == kind::STORE_ALL) && (true)) { if (Proof) { @@ -191,16 +159,34 @@ inline RewriteResponse arrays_post_rewrite10(TNode node, RewriteProof *proof) { }; Node rewritten_node = Node::fromExpr(node[0].getConst<ArrayStoreAll>().getExpr()); - return arrays_post_rewrite9<Proof>(rewritten_node, proof); + return arrays_post_rewrite7<Proof>(rewritten_node, proof); + }; + if (((node[0]).getKind() == kind::STORE) && + (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) == + nm->mkConst(false))) { + if (Proof) { + proof->registerRewrite(arrays_post_SELECT_STORE_DIFF_I_J); + }; + Node rewritten_node = nm->mkNode(kind::SELECT, node[0][0], node[1]); + return arrays_post_rewrite7<Proof>(rewritten_node, proof); + }; + if (((node[0]).getKind() == kind::STORE) && + ((((node[0][1]).isConst()) && ((node[1]).isConst())) && + ((node[0][1] != node[1])))) { + if (Proof) { + proof->registerRewrite(arrays_post_SELECT_STORE_DIFF_CONSTS); + }; + Node rewritten_node = nm->mkNode(kind::SELECT, node[0][0], node[1]); + return arrays_post_rewrite7<Proof>(rewritten_node, proof); } }; - return arrays_post_rewrite8<Proof>(node, proof); + return arrays_post_rewrite6<Proof>(node, proof); } template <bool Proof> inline RewriteResponse arrays_post_applyRules(TNode node, RewriteProof *proof) { - return arrays_post_rewrite10<Proof>(node, proof); + return arrays_post_rewrite8<Proof>(node, proof); } inline void arrays_post_printProof(bool use_cache, TheoryProofEngine *tp, |