From 4410ff88895de6ed2242705f80c1a3ed38a58165 Mon Sep 17 00:00:00 2001 From: Andres Notzli Date: Tue, 9 May 2017 11:40:39 -0700 Subject: change --- src/theory/arrays/arrays_post.h | 80 +++++++++++++++++++++-------------------- src/theory/arrays/arrays_pre.h | 35 ++++++++++-------- 2 files changed, 61 insertions(+), 54 deletions(-) diff --git a/src/theory/arrays/arrays_post.h b/src/theory/arrays/arrays_post.h index 5dbf6a506..3e29d77f4 100644 --- a/src/theory/arrays/arrays_post.h +++ b/src/theory/arrays/arrays_post.h @@ -103,24 +103,24 @@ inline RewriteResponse arrays_post_rewrite6(TNode node, RewriteProof *proof) { Node rewritten_node = node[0]; return arrays_post_rewrite5(rewritten_node, proof); }; - if ((node[0]).getKind() == kind::STORE) { - if ((true) && (node[0][1] == node[1])) { - if (Proof) { - proof->registerRewrite(arrays_post_STORE_STORE_I_I); - }; - Node rewritten_node = - nm->mkNode(kind::STORE, node[0][0], node[0][1], node[2]); - return arrays_post_rewrite5(rewritten_node, proof); + if (((node[0]).getKind() == kind::STORE) && (true) && + (node[0][1] == node[1])) { + if (Proof) { + proof->registerRewrite(arrays_post_STORE_STORE_I_I); }; - if (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) == - nm->mkConst(true)) { - if (Proof) { - proof->registerRewrite(arrays_post_STORE_STORE_I_J); - }; - Node rewritten_node = - nm->mkNode(kind::STORE, node[0][0], node[1], node[2]); - return arrays_post_rewrite5(rewritten_node, proof); - } + Node rewritten_node = + nm->mkNode(kind::STORE, node[0][0], node[0][1], node[2]); + return arrays_post_rewrite5(rewritten_node, proof); + }; + if (((node[0]).getKind() == kind::STORE) && + (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) == + nm->mkConst(true))) { + if (Proof) { + proof->registerRewrite(arrays_post_STORE_STORE_I_J); + }; + Node rewritten_node = + nm->mkNode(kind::STORE, node[0][0], node[1], node[2]); + return arrays_post_rewrite5(rewritten_node, proof); } }; return arrays_post_rewrite4(node, proof); @@ -135,18 +135,19 @@ inline RewriteResponse arrays_post_rewrite7(TNode node, RewriteProof *proof) { template inline RewriteResponse arrays_post_rewrite8(TNode node, RewriteProof *proof) { NodeManager *nm = NodeManager::currentNM(); - if (((node).getKind() == kind::SELECT) && - ((node[0]).getKind() == kind::STORE)) { - if (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) == - nm->mkConst(false)) { + 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(rewritten_node, proof); }; - if ((((node[0][1]).isConst()) && ((node[1]).isConst())) && - ((node[0][1] != node[1]))) { + 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); }; @@ -167,28 +168,29 @@ template inline RewriteResponse arrays_post_rewrite10(TNode node, RewriteProof *proof) { NodeManager *nm = NodeManager::currentNM(); if ((node).getKind() == kind::SELECT) { - if ((node[0]).getKind() == kind::STORE) { - if ((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(rewritten_node, proof); + 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(rewritten_node, proof); + }; + if (((node[0]).getKind() == kind::STORE) && + (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) == + nm->mkConst(true))) { + if (Proof) { + proof->registerRewrite(arrays_post_SELECT_STORE_I_J); }; - if (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) == - nm->mkConst(true)) { - if (Proof) { - proof->registerRewrite(arrays_post_SELECT_STORE_I_J); - }; - Node rewritten_node = node[0][2]; - return arrays_post_rewrite9(rewritten_node, proof); - } + Node rewritten_node = node[0][2]; + return arrays_post_rewrite9(rewritten_node, proof); }; if (((node[0]).getKind() == kind::STORE_ALL) && (true)) { if (Proof) { proof->registerRewrite(arrays_post_SELECT_STORE_ALL); }; - Node rewritten_node = node[0][0]; + Node rewritten_node = + Node::fromExpr(node[0].getConst().getExpr()); return arrays_post_rewrite9(rewritten_node, proof); } }; diff --git a/src/theory/arrays/arrays_pre.h b/src/theory/arrays/arrays_pre.h index 7fabc17e6..a43b8fe7b 100644 --- a/src/theory/arrays/arrays_pre.h +++ b/src/theory/arrays/arrays_pre.h @@ -33,9 +33,9 @@ inline RewriteResponse arrays_pre_rewrite1(TNode node, RewriteProof *proof) { template inline RewriteResponse arrays_pre_rewrite2(TNode node, RewriteProof *proof) { NodeManager *nm = NodeManager::currentNM(); - if (((node).getKind() == kind::STORE) && - ((node[0]).getKind() == kind::STORE)) { - if ((true) && (node[0][1] == node[1])) { + if ((node).getKind() == kind::STORE) { + if (((node[0]).getKind() == kind::STORE) && (true) && + (node[0][1] == node[1])) { if (Proof) { proof->registerRewrite(arrays_pre_STORE_STORE_I_I); }; @@ -43,8 +43,9 @@ inline RewriteResponse arrays_pre_rewrite2(TNode node, RewriteProof *proof) { nm->mkNode(kind::STORE, node[0][0], node[0][1], node[2]); return arrays_pre_rewrite1(rewritten_node, proof); }; - if (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) == - nm->mkConst(true)) { + if (((node[0]).getKind() == kind::STORE) && + (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) == + nm->mkConst(true))) { if (Proof) { proof->registerRewrite(arrays_pre_STORE_STORE_I_J); }; @@ -98,7 +99,8 @@ inline RewriteResponse arrays_pre_rewrite6(TNode node, RewriteProof *proof) { if (Proof) { proof->registerRewrite(arrays_pre_SELECT_STORE_ALL); }; - Node rewritten_node = node[0][0]; + Node rewritten_node = + Node::fromExpr(node[0].getConst().getExpr()); return arrays_pre_rewrite5(rewritten_node, proof); }; return arrays_pre_rewrite4(node, proof); @@ -113,33 +115,36 @@ inline RewriteResponse arrays_pre_rewrite7(TNode node, RewriteProof *proof) { template inline RewriteResponse arrays_pre_rewrite8(TNode node, RewriteProof *proof) { NodeManager *nm = NodeManager::currentNM(); - if (((node).getKind() == kind::SELECT) && - ((node[0]).getKind() == kind::STORE)) { - if ((true) && (node[0][1] == node[1])) { + if ((node).getKind() == kind::SELECT) { + if (((node[0]).getKind() == kind::STORE) && (true) && + (node[0][1] == node[1])) { if (Proof) { proof->registerRewrite(arrays_pre_SELECT_STORE_I_I); }; Node rewritten_node = node[0][2]; return arrays_pre_rewrite7(rewritten_node, proof); }; - if (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) == - nm->mkConst(false)) { + 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_pre_SELECT_STORE_DIFF_I_J); }; Node rewritten_node = nm->mkNode(kind::SELECT, node[0][0], node[1]); return arrays_pre_rewrite7(rewritten_node, proof); }; - if (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) == - nm->mkConst(true)) { + if (((node[0]).getKind() == kind::STORE) && + (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) == + nm->mkConst(true))) { if (Proof) { proof->registerRewrite(arrays_pre_SELECT_STORE_I_J); }; Node rewritten_node = node[0][2]; return arrays_pre_rewrite7(rewritten_node, proof); }; - if ((((node[0][1]).isConst()) && ((node[1]).isConst())) && - ((node[0][1] != node[1]))) { + if (((node[0]).getKind() == kind::STORE) && + ((((node[0][1]).isConst()) && ((node[1]).isConst())) && + ((node[0][1] != node[1])))) { if (Proof) { proof->registerRewrite(arrays_pre_SELECT_STORE_DIFF_CONSTS); }; -- cgit v1.2.3