summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arith/kinds4
-rw-r--r--src/theory/arrays/array_info.h37
-rw-r--r--src/theory/arrays/kinds2
-rw-r--r--src/theory/booleans/kinds2
-rw-r--r--src/theory/builtin/kinds12
-rw-r--r--src/theory/bv/kinds18
-rw-r--r--src/theory/datatypes/kinds4
-rw-r--r--src/theory/ite_simplifier.h2
8 files changed, 30 insertions, 51 deletions
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 7883bd92b..b9fac6e20 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -38,7 +38,7 @@ sort INTEGER_TYPE \
constant SUBRANGE_TYPE \
::CVC4::SubrangeBounds \
- ::CVC4::SubrangeBoundsHashStrategy \
+ ::CVC4::SubrangeBoundsHashFunction \
"util/subrange_bound.h" \
"the type of an integer subrange"
cardinality SUBRANGE_TYPE \
@@ -51,7 +51,7 @@ well-founded SUBRANGE_TYPE \
constant CONST_RATIONAL \
::CVC4::Rational \
- ::CVC4::RationalHashStrategy \
+ ::CVC4::RationalHashFunction \
"util/rational.h" \
"a multiple-precision rational constant"
diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h
index b34232b8f..e847a238d 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -2,28 +2,10 @@
/*! \file array_info.h
** \verbatim
** Original author: lianah
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): dejan, barrett
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** 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
- **/
-
-/*! \file array_info.h
- ** \verbatim
- ** Original author: lianah
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
@@ -31,14 +13,13 @@
**
** \brief Contains additional classes to store context dependent information
** for each term of type array
- **
- **
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__ARRAYS__ARRAY_INFO_H
#define __CVC4__THEORY__ARRAYS__ARRAY_INFO_H
+
#include "util/backtrackable.h"
#include "context/cdlist.h"
#include "context/cdhashmap.h"
@@ -58,7 +39,7 @@ typedef context::CDList<TNode> CTNodeList;
typedef quad<TNode, TNode, TNode, TNode> RowLemmaType;
struct RowLemmaTypeHashFunction {
- size_t operator()(const RowLemmaType& q ) const {
+ size_t operator()(const RowLemmaType& q) const {
TNode n1 = q.first;
TNode n2 = q.second;
TNode n3 = q.third;
@@ -92,7 +73,6 @@ public:
indices = new(true)CTNodeList(c);
stores = new(true)CTNodeList(c);
in_stores = new(true)CTNodeList(c);
-
}
~Info() {
@@ -115,7 +95,7 @@ public:
Trace("arrays-info")<<" in_stores ";
printList(in_stores);
}
-};
+};/* class Info */
typedef __gnu_cxx::hash_map<Node, Info*, NodeHashFunction> CNodeInfoMap;
@@ -202,7 +182,7 @@ public:
StatisticsRegistry::registerStat(&d_tableSize);
}
- ~ArrayInfo(){
+ ~ArrayInfo() {
CNodeInfoMap::iterator it = info_map.begin();
for( ; it != info_map.end(); it++ ) {
if((*it).second!= emptyInfo) {
@@ -255,8 +235,7 @@ public:
* a should be the canonical representative of b
*/
void mergeInfo(const TNode a, const TNode b);
-};
-
+};/* class ArrayInfo */
}/* CVC4::theory::arrays namespace */
}/* CVC4::theory namespace */
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 7386ec5c2..ef237e351 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -32,7 +32,7 @@ operator STORE 3 "array store"
# storeall t e is \all i in indexType(t) <= e
constant STORE_ALL \
::CVC4::ArrayStoreAll \
- ::CVC4::ArrayStoreAllHashStrategy \
+ ::CVC4::ArrayStoreAllHashFunction \
"util/array_store_all.h" \
"array store-all"
diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds
index 92a9a937f..4d748ca59 100644
--- a/src/theory/booleans/kinds
+++ b/src/theory/booleans/kinds
@@ -20,7 +20,7 @@ sort BOOLEAN_TYPE \
constant CONST_BOOLEAN \
bool \
- ::CVC4::BoolHashStrategy \
+ ::CVC4::BoolHashFunction \
"util/bool.h" \
"truth and falsity"
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 57baa82cd..6bb175db3 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -122,7 +122,7 @@
# to define it. Hasher is a hash functor type defined like this:
#
# struct MyHashFcn {
-# static size_t hash(const T& val);
+# size_t operator()(const T& val) const;
# };
#
# For consistency, constants taking a non-void payload should
@@ -267,7 +267,7 @@ well-founded SORT_TYPE \
constant UNINTERPRETED_CONSTANT \
::CVC4::UninterpretedConstant \
- ::CVC4::UninterpretedConstantHashStrategy \
+ ::CVC4::UninterpretedConstantHashFunction \
"util/uninterpreted_constant.h" \
"The kind of nodes representing uninterpreted constants"
typerule UNINTERPRETED_CONSTANT ::CVC4::theory::builtin::UninterpretedConstantTypeRule
@@ -281,7 +281,7 @@ enumerator SORT_TYPE \
# you'll get a special, singleton (BUILTIN EQUAL) Node.
constant BUILTIN \
::CVC4::Kind \
- ::CVC4::kind::KindHashStrategy \
+ ::CVC4::kind::KindHashFunction \
"expr/kind.h" \
"The kind of nodes representing built-in operators"
@@ -296,7 +296,7 @@ operator TUPLE 2: "a tuple"
constant TYPE_CONSTANT \
::CVC4::TypeConstant \
- ::CVC4::TypeConstantHashStrategy \
+ ::CVC4::TypeConstantHashFunction \
"expr/kind.h" \
"basic types"
operator FUNCTION_TYPE 2: "function type"
@@ -325,7 +325,7 @@ sort STRING_TYPE \
"String type"
constant CONST_STRING \
::std::string \
- ::CVC4::StringHashStrategy \
+ ::CVC4::StringHashFunction \
"util/hash.h" \
"a string of characters"
typerule CONST_STRING ::CVC4::theory::builtin::StringConstantTypeRule
@@ -337,7 +337,7 @@ typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule
constant SUBTYPE_TYPE \
::CVC4::Predicate \
- ::CVC4::PredicateHashStrategy \
+ ::CVC4::PredicateHashFunction \
"util/predicate.h" \
"predicate subtype"
cardinality SUBTYPE_TYPE \
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index 36e27c66c..765f6bc59 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -14,7 +14,7 @@ rewriter ::CVC4::theory::bv::TheoryBVRewriter "theory/bv/theory_bv_rewriter.h"
constant BITVECTOR_TYPE \
::CVC4::BitVectorSize \
- "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSize >" \
+ "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorSize >" \
"util/bitvector.h" \
"bit-vector type"
cardinality BITVECTOR_TYPE \
@@ -23,7 +23,7 @@ cardinality BITVECTOR_TYPE \
constant CONST_BITVECTOR \
::CVC4::BitVector \
- ::CVC4::BitVectorHashStrategy \
+ ::CVC4::BitVectorHashFunction \
"util/bitvector.h" \
"a fixed-width bit-vector constant"
@@ -63,43 +63,43 @@ operator BITVECTOR_SGE 2 "signed greater than or equal"
constant BITVECTOR_BITOF_OP \
::CVC4::BitVectorBitOf \
- ::CVC4::BitVectorBitOfHashStrategy \
+ ::CVC4::BitVectorBitOfHashFunction \
"util/bitvector.h" \
"operator for the bit-vector boolean bit extract"
constant BITVECTOR_EXTRACT_OP \
::CVC4::BitVectorExtract \
- ::CVC4::BitVectorExtractHashStrategy \
+ ::CVC4::BitVectorExtractHashFunction \
"util/bitvector.h" \
"operator for the bit-vector extract"
constant BITVECTOR_REPEAT_OP \
::CVC4::BitVectorRepeat \
- "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorRepeat >" \
+ "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRepeat >" \
"util/bitvector.h" \
"operator for the bit-vector repeat"
constant BITVECTOR_ZERO_EXTEND_OP \
::CVC4::BitVectorZeroExtend \
- "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorZeroExtend >" \
+ "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorZeroExtend >" \
"util/bitvector.h" \
"operator for the bit-vector zero-extend"
constant BITVECTOR_SIGN_EXTEND_OP \
::CVC4::BitVectorSignExtend \
- "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSignExtend >" \
+ "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorSignExtend >" \
"util/bitvector.h" \
"operator for the bit-vector sign-extend"
constant BITVECTOR_ROTATE_LEFT_OP \
::CVC4::BitVectorRotateLeft \
- "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorRotateLeft >" \
+ "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRotateLeft >" \
"util/bitvector.h" \
"operator for the bit-vector rotate left"
constant BITVECTOR_ROTATE_RIGHT_OP \
::CVC4::BitVectorRotateRight \
- "::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorRotateRight >" \
+ "::CVC4::UnsignedHashFunction< ::CVC4::BitVectorRotateRight >" \
"util/bitvector.h" \
"operator for the bit-vector rotate right"
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index e66cc3454..58c8fb5d2 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -44,7 +44,7 @@ parameterized APPLY_TESTER TESTER_TYPE 1: "tester application"
constant DATATYPE_TYPE \
::CVC4::Datatype \
- "::CVC4::DatatypeHashStrategy" \
+ "::CVC4::DatatypeHashFunction" \
"util/datatype.h" \
"datatype type"
cardinality DATATYPE_TYPE \
@@ -72,7 +72,7 @@ parameterized APPLY_TYPE_ASCRIPTION ASCRIPTION_TYPE 1 \
"type ascription, for datatype constructor applications"
constant ASCRIPTION_TYPE \
::CVC4::AscriptionType \
- ::CVC4::AscriptionTypeHashStrategy \
+ ::CVC4::AscriptionTypeHashFunction \
"util/ascription_type.h" \
"a type parameter for type ascription"
diff --git a/src/theory/ite_simplifier.h b/src/theory/ite_simplifier.h
index fb42909e0..cba5c7051 100644
--- a/src/theory/ite_simplifier.h
+++ b/src/theory/ite_simplifier.h
@@ -69,7 +69,7 @@ class ITESimplifier {
hash ^= 0x9e3779b9 + NodeHashFunction().operator()(pair.second) + (hash << 6) + (hash >> 2);
return hash;
}
- };
+ };/* struct ITESimplifier::NodePairHashFunction */
typedef std::hash_map<NodePair, Node, NodePairHashFunction> NodePairMap;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback