attribute stuff for Clark's array constants

diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index 50873a6a12ce16c6298b1ef9759462ed79d118f5..c51b0433a2c03d3eefca3ddab126ac70825014a5 100644 (file)
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -23,12 +23,21 @@
 #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
 
 #include "theory/rewriter.h"
-#include "type_enumerator.h"
+#include "theory/type_enumerator.h"
+#include "expr/attribute.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arrays {
 
+namespace attr {
+  struct ArrayConstantMostFrequentValueTag { };
+  struct ArrayConstantMostFrequentValueCountTag { };
+}/* CVC4::theory::arrays::attr namespace */
+
+typedef expr::Attribute<attr::ArrayConstantMostFrequentValueCountTag, uint64_t> ArrayConstantMostFrequentValueCountAttr;
+typedef expr::Attribute<attr::ArrayConstantMostFrequentValueTag, Node> ArrayConstantMostFrequentValueAttr;
+
 class TheoryArraysRewriter {
 
   static Node normalizeConstant(TNode node) {
@@ -113,6 +122,8 @@ class TheoryArraysRewriter {
     bool recompute = false;
     if (node[0].getKind() == kind::STORE) {
       // TODO: look up most frequent value and count
+      mostFrequentValue = node.getAttribute(ArrayConstantMostFrequentValueAttr());
+      mostFrequentValueCount = node.getAttribute(ArrayConstantMostFrequentValueCountAttr());
       if (!replacedValue.isNull() && mostFrequentValue == replacedValue) {
         recompute = true;
       }

diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index a535067d0e45810628ba7b307bc5db407b9983bb..2cad1fa439fecebd938bb0d9ab6beac43d5d9aa2 100644 (file)
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -21,6 +21,8 @@
 #ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
 #define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_TYPE_RULES_H
 
+#include "theory/arrays/theory_arrays_rewriter.h" // for array-constant attributes
+
 namespace CVC4 {
 namespace theory {
 namespace arrays {
@@ -120,6 +122,8 @@ struct ArrayStoreTypeRule {
     store = n[0];
     if (store.getKind() == kind::STORE) {
       // TODO: look up most frequent value and count
+      mostFrequentValue = n.getAttribute(ArrayConstantMostFrequentValueAttr());
+      mostFrequentValueCount = n.getAttribute(ArrayConstantMostFrequentValueCountAttr());
     }
 
     // Compute the most frequently written value for n
@@ -138,6 +142,8 @@ struct ArrayStoreTypeRule {
     }
 
     // TODO: store mostFrequentValue and mostFrequentValueCount for this node
+    n.setAttribute(ArrayConstantMostFrequentValueAttr(), mostFrequentValue);
+    n.setAttribute(ArrayConstantMostFrequentValueCountAttr(), mostFrequentValueCount);
     return true;
   }