From: Clark Barrett Date: Sun, 19 Aug 2012 02:08:15 +0000 (+0000) Subject: 1. Fix for inst_match.cpp to allow compilation on fedora X-Git-Tag: cvc5-1.0.0~7862 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e8e85053afba60bd6060cb07c52c88c316d73b30;p=cvc5.git 1. Fix for inst_match.cpp to allow compilation on fedora 2. Initial implementation of computeIsConst for arrays - still needs additional checks based on cardinality 3. Finally fixed pre-competition bug in array rewriter 4. Still to come: array rewrites for constants and STORE_ALL --- diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index c6ef5cd25..ba2baab2c 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -62,26 +62,76 @@ public: if (value.getKind() == kind::SELECT && value[0] == store && value[1] == node[1]) { + Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << store << std::endl; return RewriteResponse(REWRITE_DONE, store); } if (store.getKind() == kind::STORE) { // store(store(a,i,v),j,w) - Node eqRewritten = Rewriter::rewrite(store[1].eqNode(node[1])); - if (eqRewritten.getKind() == kind::CONST_BOOLEAN) { - bool val = eqRewritten.getConst(); - NodeManager* nm = NodeManager::currentNM(); - if (val) { - // store(store(a,i,v),i,w) = store(a,i,w) - Node newNode = nm->mkNode(kind::STORE, store[0], store[1], value); - return RewriteResponse(REWRITE_AGAIN_FULL, newNode); + TNode index = node[1]; + bool val; + if (index == store[1]) { + val = true; + } + else if (index.isConst() && store[1].isConst()) { + val = false; + } + else { + Node eqRewritten = Rewriter::rewrite(store[1].eqNode(index)); + if (eqRewritten.getKind() != kind::CONST_BOOLEAN) { + Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << node << std::endl; + return RewriteResponse(REWRITE_DONE, node); } - else if (node[1] < store[1]) { - // store(store(a,i,v),j,w) = store(store(a,j,w),i,v) - // IF i != j and j comes before i in the ordering - Node newNode = nm->mkNode(kind::STORE, store[0], node[1], value); - newNode = nm->mkNode(kind::STORE, newNode, store[1], store[2]); - return RewriteResponse(REWRITE_AGAIN_FULL, newNode); + val = eqRewritten.getConst(); + } + NodeManager* nm = NodeManager::currentNM(); + if (val) { + // store(store(a,i,v),i,w) = store(a,i,w) + Node result = nm->mkNode(kind::STORE, store[0], index, value); + Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << result << std::endl; + return RewriteResponse(REWRITE_DONE, result); + } + else if (index < store[1]) { + // store(store(a,i,v),j,w) = store(store(a,j,w),i,v) + // IF i != j and j comes before i in the ordering + std::vector indices; + std::vector elements; + indices.push_back(store[1]); + elements.push_back(store[2]); + store = store[0]; + Node n; + while (store.getKind() == kind::STORE) { + if (index == store[1]) { + val = true; + } + else if (index.isConst() && store[1].isConst()) { + val = false; + } + else { + n = Rewriter::rewrite(store[1].eqNode(index)); + if (n.getKind() != kind::CONST_BOOLEAN) { + break; + } + val = n.getConst(); + } + if (val) { + store = store[0]; + break; + } + else if (!(index < store[1])) { + break; + } + indices.push_back(store[1]); + elements.push_back(store[2]); + store = store[0]; + } + n = nm->mkNode(kind::STORE, store, index, value); + while (!indices.empty()) { + n = nm->mkNode(kind::STORE, n, indices.back(), elements.back()); + indices.pop_back(); + elements.pop_back(); } + Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl; + return RewriteResponse(REWRITE_DONE, n); } } break; @@ -89,10 +139,12 @@ public: case kind::EQUAL: case kind::IFF: { if(node[0] == node[1]) { + Trace("arrays-postrewrite") << "Arrays::postRewrite returning true" << std::endl; return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); } if (node[0] > node[1]) { Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]); + Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << newNode << std::endl; return RewriteResponse(REWRITE_DONE, newNode); } break; @@ -100,12 +152,119 @@ public: default: break; } - + Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << node << std::endl; return RewriteResponse(REWRITE_DONE, node); } static inline RewriteResponse preRewrite(TNode node) { - Trace("arrays-prerewrite") << "Arrays::preRewrite " << node << std::endl; + Trace("arrays-prerewrite") << "Arrays::preRewrite start " << node << std::endl; + switch (node.getKind()) { + case kind::SELECT: { + TNode store = node[0]; + if (store.getKind() == kind::STORE) { + // select(store(a,i,v),j) + TNode index = node[1]; + bool val; + if (index == store[1]) { + val = true; + } + else if (index.isConst() && store[1].isConst()) { + val = false; + } + else { + Node eqRewritten = Rewriter::rewrite(store[1].eqNode(index)); + if (eqRewritten.getKind() != kind::CONST_BOOLEAN) { + break; + } + val = eqRewritten.getConst(); + } + if (val) { + // select(store(a,i,v),i) = v + Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << store[2] << std::endl; + return RewriteResponse(REWRITE_DONE, store[2]); + } + else { + // select(store(a,i,v),j) = select(a,j) if i /= j + store = store[0]; + Node n; + while (store.getKind() == kind::STORE) { + if (index == store[1]) { + val = true; + } + else if (index.isConst() && store[1].isConst()) { + val = false; + } + else { + n = Rewriter::rewrite(store[1].eqNode(index)); + if (n.getKind() != kind::CONST_BOOLEAN) { + break; + } + val = n.getConst(); + } + if (val) { + Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << store[2] << std::endl; + return RewriteResponse(REWRITE_DONE, store[2]); + } + store = store[0]; + } + n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index); + Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << n << std::endl; + return RewriteResponse(REWRITE_DONE, n); + } + } + break; + } + case kind::STORE: { + TNode store = node[0]; + TNode value = node[2]; + // store(a,i,select(a,i)) = a + if (value.getKind() == kind::SELECT && + value[0] == store && + value[1] == node[1]) { + Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << store << std::endl; + return RewriteResponse(REWRITE_DONE, store); + } + if (store.getKind() == kind::STORE) { + // store(store(a,i,v),j,w) + TNode index = node[1]; + bool val; + if (index == store[1]) { + val = true; + } + else if (index.isConst() && store[1].isConst()) { + val = false; + } + else { + Node eqRewritten = Rewriter::rewrite(store[1].eqNode(index)); + if (eqRewritten.getKind() != kind::CONST_BOOLEAN) { + Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << node << std::endl; + return RewriteResponse(REWRITE_DONE, node); + } + val = eqRewritten.getConst(); + } + NodeManager* nm = NodeManager::currentNM(); + if (val) { + // store(store(a,i,v),i,w) = store(a,i,w) + Node newNode = nm->mkNode(kind::STORE, store[0], index, value); + Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << newNode << std::endl; + return RewriteResponse(REWRITE_DONE, newNode); + } + } + break; + } + case kind::EQUAL: + case kind::IFF: { + if(node[0] == node[1]) { + Trace("arrays-prerewrite") << "Arrays::preRewrite returning true" << std::endl; + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); + } + break; + } + default: + break; + } + + Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << node << std::endl; return RewriteResponse(REWRITE_DONE, node); } diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index b130b78fd..9c678d6ce 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -71,16 +71,82 @@ struct ArrayStoreTypeRule { Assert(n.getKind() == kind::STORE); NodeManagerScope nms(nodeManager); - // TODO: test ordering of stores, and ultimate application to a store-all - // ALSO: ensure uniqueness of form (e.g. one constant of the array sort - // BOOL->INT can be represented as - // [false->0, default=1] - // and also - // [true->1, default=0] - // ..but by contract of isConst(), only one of these can be considered - // a "const" expression. - - return false; + TNode store = n[0]; + TNode index = n[1]; + TNode value = n[2]; + + // A constant must have only constant children and be in normal form + // If any child is non-const, this is not a constant + if (!store.isConst() || !index.isConst() || !value.isConst()) { + return false; + } + + // If store indices are not in order, not in normal form + if (store.getKind() == kind::STORE && index < store[1]) { + return false; + } + + // Compute the number of nested stores + Integer depth = 1; + while (store.getKind() == kind::STORE) { + store = store[0]; + depth += 1; + } + + // Get the default value in the STORE_ALL object at the bottom of the nested stores + Assert(store.getKind() == kind::STORE_ALL); + ArrayStoreAll storeAll = store.getConst(); + TNode defaultValue /* = storeAll.getExpr().getTNode()*/ ; + + // If writing to default value, not in normal form + if (defaultValue == value) { + return false; + } + + // Get the cardinality of the index type + Cardinality indexCard = index.getType().getCardinality(); + + // If cardinality is infinite, ok - in normal form + if (indexCard.isInfinite()) { + return true; + } + + /* + Assert(depth <= indexCard); + + // If number of stores is equal to cardinality of index type, + // then the default value is overridden at all indices. Our normal form + // requires that the most frequent value is the default value. + if (depth == indexCard) { + return false; + } + + // If the number of stores is less than half of the cardinality, then we + // know the default value is the most frequent value, so in normal form + if (depth*2 < indexCard) { + return true; + } + Integer defaultCount = indexCard - depth; + + // Have to compare number of occurrences of value with defaultValue + store = n[0]; + depth = 1; + while (store.getKind() == kind::STORE) { + if (store[2] == value) { + depth += 1; + } + store = store[0]; + } + + // If value occurs more frequently than the default value or the same + // and is less than defaultValue, then this is not in normal form + if (depth > defaultCount || + (depth == defaultCount && value < defaultValue)) { + return false; + } + */ + + return true; } };/* struct ArrayStoreTypeRule */ diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 271e04968..14a84ea72 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -31,8 +31,10 @@ using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; -using namespace CVC4::theory::inst; +namespace CVC4 { +namespace theory { +namespace inst { InstMatch::InstMatch() { } @@ -878,3 +880,5 @@ int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){ } return qe->addInstantiation( f, m ) ? 1 : 0; } + +}}}