diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-23 23:33:52 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-23 23:33:52 +0000 |
commit | 23367b1eac54a17a060697b1cf187ad2cc2ff503 (patch) | |
tree | a77afa5623be2ffd408989918325974c7fb5b5bb /src/theory | |
parent | c0445cf73589150725ff287c1e76761268c60cec (diff) |
attribute stuff for Clark's array constants
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arrays/theory_arrays_rewriter.h | 13 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_type_rules.h | 6 |
2 files changed, 18 insertions, 1 deletions
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; } |