From: trevor_hansen Date: Tue, 24 Jan 2012 00:49:15 +0000 (+0000) Subject: Refactor. Automatically layout code. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=2265f8d017a8db82dd6947af162b4f8e5f97703a;p=francis%2Fstp.git Refactor. Automatically layout code. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1518 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/cpp_interface/cpp_interface.h b/src/cpp_interface/cpp_interface.h index f1b80d8..3b2f3af 100644 --- a/src/cpp_interface/cpp_interface.h +++ b/src/cpp_interface/cpp_interface.h @@ -1,4 +1,3 @@ - #ifndef CPP_INTERFACE_H_ #define CPP_INTERFACE_H_ @@ -12,243 +11,263 @@ namespace BEEV { -using BEEV::STPMgr; - + using BEEV::STPMgr; // There's no BVTypeCheck() function. Use a typechecking node factory instead. -class Cpp_interface -{ - STPMgr& bm; - //boost::object_pool node_pool; - bool alreadyWarned; - bool print_success; -public: - LETMgr letMgr; - NodeFactory* nf; - - Cpp_interface(STPMgr &bm_, NodeFactory* factory) - : bm(bm_), - nf(factory), - letMgr(bm.ASTUndefined) - { - assert(nf != NULL); - alreadyWarned = false; - cache.push_back(Entry(SOLVER_UNDECIDED)); - symbols.push_back(ASTVec()); - print_success=false; - } - - const ASTVec GetAsserts(void) - { - return bm.GetAsserts(); - } + class Cpp_interface + { + STPMgr& bm; + //boost::object_pool node_pool; + bool alreadyWarned; + bool print_success; + public: + LETMgr letMgr; + NodeFactory* nf; + + Cpp_interface(STPMgr &bm_, NodeFactory* factory) : + bm(bm_), nf(factory), letMgr(bm.ASTUndefined) + { + assert(nf != NULL); + alreadyWarned = false; + cache.push_back(Entry(SOLVER_UNDECIDED)); + symbols.push_back(ASTVec()); + print_success = false; + } - UserDefinedFlags& getUserFlags() - { - return bm.UserFlags; - } + const ASTVec + GetAsserts(void) + { + return bm.GetAsserts(); + } - void AddAssert(const ASTNode& assert) - { - bm.AddAssert(assert); - } + UserDefinedFlags& + getUserFlags() + { + return bm.UserFlags; + } - void AddQuery(const ASTNode& q) + void + AddAssert(const ASTNode& assert) { - bm.AddQuery(q); + bm.AddAssert(assert); } - //NODES// - ASTNode CreateNode(BEEV::Kind kind, const BEEV::ASTVec& children = _empty_ASTVec) + void + AddQuery(const ASTNode& q) { - return nf->CreateNode(kind,children); + bm.AddQuery(q); } - ASTNode CreateNode(BEEV::Kind kind, const BEEV::ASTNode n0, const BEEV::ASTNode n1) + //NODES// + ASTNode + CreateNode(BEEV::Kind kind, const BEEV::ASTVec& children = _empty_ASTVec) { - if (n0.GetIndexWidth() > 0 && !alreadyWarned) - { - cerr << "Warning: Parsing a term that uses array extensionality. STP doesn't handle array extensionality." << endl; - alreadyWarned = true; - } - return nf->CreateNode(kind,n0,n1); + return nf->CreateNode(kind, children); } + ASTNode + CreateNode(BEEV::Kind kind, const BEEV::ASTNode n0, const BEEV::ASTNode n1) + { + if (n0.GetIndexWidth() > 0 && !alreadyWarned) + { + cerr << "Warning: Parsing a term that uses array extensionality. STP doesn't handle array extensionality." + << endl; + alreadyWarned = true; + } + return nf->CreateNode(kind, n0, n1); + } // These belong in the node factory.. //TERMS// - ASTNode CreateZeroConst(unsigned int width) + ASTNode + CreateZeroConst(unsigned int width) { - return bm.CreateZeroConst(width); + return bm.CreateZeroConst(width); } - ASTNode CreateOneConst(unsigned int width) + ASTNode + CreateOneConst(unsigned int width) { - return bm.CreateOneConst(width); + return bm.CreateOneConst(width); } - ASTNode CreateBVConst(string& strval, int base, int bit_width) + ASTNode + CreateBVConst(string& strval, int base, int bit_width) { - return bm.CreateBVConst(strval, base, bit_width); + return bm.CreateBVConst(strval, base, bit_width); } - ASTNode CreateBVConst(const char* const strval, int base) + ASTNode + CreateBVConst(const char* const strval, int base) { - return bm.CreateBVConst(strval, base); + return bm.CreateBVConst(strval, base); } - ASTNode CreateBVConst(unsigned int width, unsigned long long int bvconst) + ASTNode + CreateBVConst(unsigned int width, unsigned long long int bvconst) { - return bm.CreateBVConst(width, bvconst); + return bm.CreateBVConst(width, bvconst); } - ASTNode LookupOrCreateSymbol(const char * const name) + ASTNode + LookupOrCreateSymbol(const char * const name) { - return bm.LookupOrCreateSymbol(name); + return bm.LookupOrCreateSymbol(name); } - ASTNode LookupOrCreateSymbol(string name) + ASTNode + LookupOrCreateSymbol(string name) { - return bm.LookupOrCreateSymbol(name.c_str()); + return bm.LookupOrCreateSymbol(name.c_str()); } - bool LookupSymbol(const char * const name, ASTNode& output) + bool + LookupSymbol(const char * const name, ASTNode& output) { - return bm.LookupSymbol(name,output); + return bm.LookupSymbol(name, output); } - bool isSymbolAlreadyDeclared(char* name) + bool + isSymbolAlreadyDeclared(char* name) { - return bm.LookupSymbol(name); + return bm.LookupSymbol(name); } - void setPrintSuccess(bool ps) + void + setPrintSuccess(bool ps) { - print_success= ps; + print_success = ps; } - - bool isSymbolAlreadyDeclared(string name) - { - return bm.LookupSymbol(name.c_str()); - } + bool + isSymbolAlreadyDeclared(string name) + { + return bm.LookupSymbol(name.c_str()); + } // Create the node, then "new" it. - ASTNode * newNode(const Kind k, const ASTNode& n0, const ASTNode& n1) + ASTNode * + newNode(const Kind k, const ASTNode& n0, const ASTNode& n1) { - return newNode(CreateNode(k,n0,n1)); + return newNode(CreateNode(k, n0, n1)); } // Create the node, then "new" it. - ASTNode * newNode(const Kind k, const int width, const ASTNode& n0, const ASTNode& n1) + ASTNode * + newNode(const Kind k, const int width, const ASTNode& n0, const ASTNode& n1) { - return newNode(nf->CreateTerm(k,width,n0,n1)); + return newNode(nf->CreateTerm(k, width, n0, n1)); } - // On testcase20 it took about 4.2 seconds to parse using the standard allocator and the pool allocator. - ASTNode * newNode(const ASTNode& copyIn) - { - return new ASTNode(copyIn); - //return node_pool.construct(copyIn); - } - - void deleteNode(ASTNode *n) - { - delete n; - //node_pool.destroy(n); - } - - struct Entry - { - explicit Entry( SOLVER_RETURN_TYPE result_) - { - result = result_; - } - - SOLVER_RETURN_TYPE result; - ASTNode node; - - void print() - { - if (result == SOLVER_UNSATISFIABLE) - cerr << "u"; - else if (result == SOLVER_SATISFIABLE) - cerr << "s"; - else if (result == SOLVER_UNDECIDED) - cerr << "?"; - } - }; - vector cache; - vector > symbols; - - void - addSymbol(ASTNode &s) - { - symbols.back().push_back(s); - letMgr._parser_symbol_table.insert(s); - } - - void - success() - { - if (print_success) - { - cout << "success" << endl; - flush(cout); - } - } + ASTNode * + newNode(const ASTNode& copyIn) + { + return new ASTNode(copyIn); + //return node_pool.construct(copyIn); + } - void - pop() - { - if (symbols.size() ==0) - FatalError("Popping from an empty stack."); - if (symbols.size() ==1) - FatalError("Can't pop away the default base element."); - - assert(symbols.size() == cache.size()); - cache.erase(cache.end()-1); - ASTVec & current = symbols.back(); - for (int i=0; i < current.size() ;i++) - letMgr._parser_symbol_table.erase(current[i]); - symbols.erase(symbols.end()-1); - } + void + deleteNode(ASTNode *n) + { + delete n; + //node_pool.destroy(n); + } + + struct Entry + { + explicit + Entry(SOLVER_RETURN_TYPE result_) + { + result = result_; + } + + SOLVER_RETURN_TYPE result; + ASTNode node; + + void + print() + { + if (result == SOLVER_UNSATISFIABLE) + cerr << "u"; + else if (result == SOLVER_SATISFIABLE) + cerr << "s"; + else if (result == SOLVER_UNDECIDED) + cerr << "?"; + } + }; + vector cache; + vector > symbols; - void - push() + void + addSymbol(ASTNode &s) + { + symbols.back().push_back(s); + letMgr._parser_symbol_table.insert(s); + } + + void + success() + { + if (print_success) { - // If the prior one is unsatisiable then the new one will be too. - if (cache.size() > 1 && cache.back().result == SOLVER_UNSATISFIABLE) - cache.push_back(Entry(SOLVER_UNSATISFIABLE)); - else - cache.push_back(Entry(SOLVER_UNDECIDED)); - - symbols.push_back(ASTVec()); - assert(symbols.size() == cache.size()); + cout << "success" << endl; + flush(cout); } + } - void printStatus() - { - for (int i=0; i < cache.size();i++) + void + pop() + { + if (symbols.size() == 0) + FatalError("Popping from an empty stack."); + if (symbols.size() == 1) + FatalError("Can't pop away the default base element."); + + assert(symbols.size() == cache.size()); + cache.erase(cache.end() - 1); + ASTVec & current = symbols.back(); + for (int i = 0; i < current.size(); i++) + letMgr._parser_symbol_table.erase(current[i]); + symbols.erase(symbols.end() - 1); + } + + void + push() + { + // If the prior one is unsatisiable then the new one will be too. + if (cache.size() > 1 && cache.back().result == SOLVER_UNSATISFIABLE) + cache.push_back(Entry(SOLVER_UNSATISFIABLE)); + else + cache.push_back(Entry(SOLVER_UNDECIDED)); + + symbols.push_back(ASTVec()); + assert(symbols.size() == cache.size()); + } + + void + printStatus() + { + for (int i = 0; i < cache.size(); i++) { cache[i].print(); } - cerr<< endl; - } + cerr << endl; + } void checkSat(vector & assertionsSMT2); - void cleanUp() + void + cleanUp() { letMgr.cleanupParserSymbolTable(); cache.clear(); symbols.clear(); } -}; + }; } #endif /* PARSERINTERFACE_H_ */