diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-07 18:38:49 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-07 18:38:49 +0000 |
commit | b0deae79d8bae5051a85dc15e43e7b83bc8cf9ab (patch) | |
tree | d73fa7f9fb37077853f824dcecd2a1b8e4d22837 /src/theory | |
parent | ea5acaba821790dd240db779f2340fbe5fce0b8e (diff) |
Some items from the CVC4 public interface review:
* rename DeclarationScope to SymbolTable
* rename all HashStrategy -> HashFunction (which we often have anyways)
* remove CDCircList (no one is currently using it)
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/kinds | 4 | ||||
-rw-r--r-- | src/theory/arrays/array_info.h | 37 | ||||
-rw-r--r-- | src/theory/arrays/kinds | 2 | ||||
-rw-r--r-- | src/theory/booleans/kinds | 2 | ||||
-rw-r--r-- | src/theory/builtin/kinds | 12 | ||||
-rw-r--r-- | src/theory/bv/kinds | 18 | ||||
-rw-r--r-- | src/theory/datatypes/kinds | 4 | ||||
-rw-r--r-- | src/theory/ite_simplifier.h | 2 |
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; |