From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 23 Aug 2012 23:33:52 +0000 (+0000)
Subject: attribute stuff for Clark's array constants
X-Git-Tag: cvc5-1.0.0~7851
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=23367b1eac54a17a060697b1cf187ad2cc2ff503;p=cvc5.git

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 50873a6a1..c51b0433a 100644
--- 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 a535067d0..2cad1fa43 100644
--- 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;
   }