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 c6ef5cd2541f45ea75e94443995a254a0891f726..ba2baab2c09a7abbf2c5262ce1b5eb939a281c72 100644 (file)
--- 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 b130b78fd8b0b2ea61edeb7695d069b125e2e4af..9c678d6cedfe601a114b94b1bbd5eaaf22aae2d8 100644 (file)
--- 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 271e04968dfb78badb5246a4a13251096eefd45f..14a84ea723eaccb41ff0ccde97d37b5af269e445 100644 (file)
--- 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;
 }
+
+}}}