summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/arrays/theory_arrays_rewriter.h191
-rw-r--r--src/theory/arrays/theory_arrays_type_rules.h86
-rw-r--r--src/theory/quantifiers/inst_match.cpp6
3 files changed, 256 insertions, 27 deletions
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<bool>();
- 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<bool>();
+ }
+ 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<TNode> indices;
+ std::vector<TNode> 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<bool>();
+ }
+ 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<bool>();
+ }
+ 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<bool>();
+ }
+ 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<bool>();
+ }
+ 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<ArrayStoreAll>();
+ 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;
}
+
+}}}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback