diff options
Diffstat (limited to 'src/theory/arrays')
-rw-r--r-- | src/theory/arrays/Makefile | 4 | ||||
-rw-r--r-- | src/theory/arrays/Makefile.am | 22 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_rewriter.cpp | 49 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_rewriter.h | 16 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays_type_rules.h | 8 |
5 files changed, 59 insertions, 40 deletions
diff --git a/src/theory/arrays/Makefile b/src/theory/arrays/Makefile deleted file mode 100644 index bce529db0..000000000 --- a/src/theory/arrays/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../.. -srcdir = src/theory/arrays - -include $(topdir)/Makefile.subdir diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am deleted file mode 100644 index 77f102cf8..000000000 --- a/src/theory/arrays/Makefile.am +++ /dev/null @@ -1,22 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libarrays.la - -libarrays_la_SOURCES = \ - theory_arrays_type_rules.h \ - type_enumerator.h \ - theory_arrays_rewriter.h \ - theory_arrays.h \ - theory_arrays.cpp \ - union_find.h \ - union_find.cpp \ - array_info.h \ - array_info.cpp \ - static_fact_manager.h \ - static_fact_manager.cpp - -EXTRA_DIST = \ - kinds diff --git a/src/theory/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp new file mode 100644 index 000000000..d926cd7a2 --- /dev/null +++ b/src/theory/arrays/theory_arrays_rewriter.cpp @@ -0,0 +1,49 @@ +/********************* */ +/*! \file theory_arrays_rewriter.cpp + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "expr/attribute.h" +#include "theory/arrays/theory_arrays_rewriter.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; + +Node getMostFrequentValue(TNode store) { + return store.getAttribute(ArrayConstantMostFrequentValueAttr()); +} +uint64_t getMostFrequentValueCount(TNode store) { + return store.getAttribute(ArrayConstantMostFrequentValueCountAttr()); +} + +void setMostFrequentValue(TNode store, TNode value) { + return store.setAttribute(ArrayConstantMostFrequentValueAttr(), value); +} +void setMostFrequentValueCount(TNode store, uint64_t count) { + return store.setAttribute(ArrayConstantMostFrequentValueCountAttr(), count); +} + +}/* CVC4::theory::arrays namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 5df06bda8..388769412 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -22,19 +22,15 @@ #include "theory/rewriter.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; +Node getMostFrequentValue(TNode store); +uint64_t getMostFrequentValueCount(TNode store); +void setMostFrequentValue(TNode store, TNode value); +void setMostFrequentValueCount(TNode store, uint64_t count); static inline Node mkEqNode(Node a, Node b) { return a.getType().isBoolean() ? a.iffNode(b) : a.eqNode(b); @@ -132,8 +128,8 @@ public: unsigned mostFrequentValueCount = 0; store = node[0]; if (store.getKind() == kind::STORE) { - mostFrequentValue = store.getAttribute(ArrayConstantMostFrequentValueAttr()); - mostFrequentValueCount = store.getAttribute(ArrayConstantMostFrequentValueCountAttr()); + mostFrequentValue = getMostFrequentValue(store); + mostFrequentValueCount = getMostFrequentValueCount(store); } // Compute the most frequently written value for n diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h index b16b62f69..9f7bdfd4a 100644 --- a/src/theory/arrays/theory_arrays_type_rules.h +++ b/src/theory/arrays/theory_arrays_type_rules.h @@ -127,8 +127,8 @@ struct ArrayStoreTypeRule { unsigned mostFrequentValueCount = 0; store = n[0]; if (store.getKind() == kind::STORE) { - mostFrequentValue = store.getAttribute(ArrayConstantMostFrequentValueAttr()); - mostFrequentValueCount = store.getAttribute(ArrayConstantMostFrequentValueCountAttr()); + mostFrequentValue = getMostFrequentValue(store); + mostFrequentValueCount = getMostFrequentValueCount(store); } // Compute the most frequently written value for n @@ -145,8 +145,8 @@ struct ArrayStoreTypeRule { (compare == Cardinality::EQUAL && (!(defaultValue < mostFrequentValue)))) { return false; } - n.setAttribute(ArrayConstantMostFrequentValueAttr(), mostFrequentValue); - n.setAttribute(ArrayConstantMostFrequentValueCountAttr(), mostFrequentValueCount); + setMostFrequentValue(n, mostFrequentValue); + setMostFrequentValueCount(n, mostFrequentValueCount); return true; } |