From 7fa49bca62616dd34e2eda1c6eb1ceafc44923b7 Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Fri, 2 Oct 2009 22:37:12 +0000 Subject: [PATCH] minor edits git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@276 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/AST.h | 106 ++++++++++++++++++++++++-------------------------- 1 file changed, 51 insertions(+), 55 deletions(-) diff --git a/src/AST/AST.h b/src/AST/AST.h index d305ff1..c4dd01d 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -18,7 +18,6 @@ namespace BEEV { - void FatalError(const char * str, const ASTNode& a, int w = 0); void FatalError(const char * str); void SortByExprNum(ASTVec& c); @@ -27,39 +26,31 @@ namespace BEEV bool arithless(const ASTNode n1, const ASTNode n2); bool isAtomic(Kind k); - - /*************************************************************************** - * Typedef ASTNodeMap: This is a hash table from ASTNodes to ASTNodes. - * It is very convenient for attributes that are not speed-critical - **************************************************************************/ - // These are generally useful for storing ASTNodes or attributes thereof - // Hash table from ASTNodes to ASTNodes - typedef hash_map ASTNodeMap; - - typedef hash_map ASTNodeCountMap; - + typedef hash_map< + ASTNode, + ASTNode, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTNodeMap; + + typedef hash_map< + ASTNode, + int32_t, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTNodeCountMap; + + typedef hash_set< + ASTNode, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTNodeSet; + + typedef hash_multiset< + ASTNode, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTNodeMultiSet; + // Function to dump contents of ASTNodeMap ostream &operator<<(ostream &os, const ASTNodeMap &nmap); - /*************************************************************************** - Typedef ASTNodeSet: This is a hash set of ASTNodes. Very useful - for representing things like "visited nodes" - ***************************************************************************/ - typedef hash_set ASTNodeSet; - - typedef hash_multiset ASTNodeMultiSet; - - /*************************************************************************** * Class BeevMgr. This holds all "global" variables for the system, such as * unique tables for the various kinds of nodes. @@ -84,15 +75,37 @@ namespace BEEV static const int INITIAL_INTRODUCED_SYMBOLS_SIZE = 100; private: - // Typedef for unique Interior node table. - typedef hash_set ASTInteriorSet; + // Typedef for unique Interior node table. + typedef hash_set< + ASTInterior *, + ASTInterior::ASTInteriorHasher, + ASTInterior::ASTInteriorEqual> ASTInteriorSet; + // Typedef for unique Symbol node (leaf) table. - typedef hash_set ASTSymbolSet; + typedef hash_set< + ASTSymbol *, + ASTSymbol::ASTSymbolHasher, + ASTSymbol::ASTSymbolEqual> ASTSymbolSet; + + //Typedef for unique BVConst node (leaf) table. + typedef hash_set< + ASTBVConst *, + ASTBVConst::ASTBVConstHasher, + ASTBVConst::ASTBVConstEqual> ASTBVConstSet; + + // type of memo table. + typedef hash_map< + ASTNode, + ASTVec, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTNodeToVecMap; + + typedef hash_map< + ASTNode, + ASTNodeSet, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTNodeToSetMap; // Unique tables to share nodes whenever possible. ASTInteriorSet _interior_unique_table; @@ -100,25 +113,9 @@ namespace BEEV //during parsing/semantic analysis ASTSymbolSet _symbol_unique_table; - //Typedef for unique BVConst node (leaf) table. - typedef hash_set ASTBVConstSet; - //table to uniquefy bvconst ASTBVConstSet _bvconst_unique_table; - // type of memo table. - typedef hash_map ASTNodeToVecMap; - - typedef hash_map ASTNodeToSetMap; - // Memo table for bit blasted terms. If a node has already been // bitblasted, it is mapped to a vector of Boolean formulas for // the bits. @@ -852,7 +849,6 @@ namespace BEEV ~BeevMgr(); };//End of Class BeevMgr - class CompleteCounterExample { ASTNodeMap counterexample; -- 2.47.3