From: trevor_hansen Date: Wed, 28 Jul 2010 02:05:38 +0000 (+0000) Subject: Refactoring. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=8cd95a8aae91bea7497fcbe01ad0b9c942d13bb3;p=francis%2Fstp.git Refactoring. * CreateSymbol now takes the indexWidth and the valueWidth. * I've removed most of the calls to setIndexWidth. * CreateSymbol has been moved into the NodeFactory class. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@956 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/AST/ASTNode.cpp b/src/AST/ASTNode.cpp index 3e2e83b..26bad1d 100644 --- a/src/AST/ASTNode.cpp +++ b/src/AST/ASTNode.cpp @@ -266,9 +266,7 @@ namespace BEEV ostringstream oss; oss << "let_k_" << sz; - ASTNode CurrentSymbol = bm->CreateSymbol(oss.str().c_str()); - CurrentSymbol.SetValueWidth(this->GetValueWidth()); - CurrentSymbol.SetIndexWidth(this->GetIndexWidth()); + ASTNode CurrentSymbol = bm->CreateSymbol(oss.str().c_str(),this->GetIndexWidth(),this->GetValueWidth()); /* If for some reason the variable being created here is * already declared by the user then the printed output will * not be a legal input to the system. too bad. I refuse to diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp index e5f2601..6b85311 100644 --- a/src/AST/ArrayTransformer.cpp +++ b/src/AST/ArrayTransformer.cpp @@ -418,7 +418,7 @@ namespace BEEV els = TransformTerm(els); result = simp->CreateSimplifiedTermITE(cond, thn, els); } - result.SetIndexWidth(term.GetIndexWidth()); + assert(result.GetIndexWidth() ==term.GetIndexWidth()); break; } default: @@ -437,8 +437,7 @@ namespace BEEV if (c!=o) { - result = nf->CreateTerm(k, width, o); - result.SetIndexWidth(indexwidth); + result = nf->CreateArrayTerm(k,indexwidth, width, o); } else result = term; diff --git a/src/AST/NodeFactory/HashingNodeFactory.h b/src/AST/NodeFactory/HashingNodeFactory.h index 809826c..ce1d92b 100644 --- a/src/AST/NodeFactory/HashingNodeFactory.h +++ b/src/AST/NodeFactory/HashingNodeFactory.h @@ -11,10 +11,9 @@ namespace BEEV class HashingNodeFactory : public NodeFactory { - BEEV::STPMgr& bm; public: HashingNodeFactory(BEEV::STPMgr& bm_) - : bm(bm_) + :NodeFactory(bm_) { } diff --git a/src/AST/NodeFactory/NodeFactory.cpp b/src/AST/NodeFactory/NodeFactory.cpp index 756191a..ff7af9b 100644 --- a/src/AST/NodeFactory/NodeFactory.cpp +++ b/src/AST/NodeFactory/NodeFactory.cpp @@ -1,5 +1,6 @@ #include "ASTKind.h" #include "AST.h" +#include "../../STPManager/STPManager.h" NodeFactory::~NodeFactory() { @@ -103,3 +104,11 @@ BEEV::ASTNode NodeFactory::CreateArrayTerm(Kind kind, unsigned int index, return result; } + +ASTNode NodeFactory::CreateSymbol(const char * const name, unsigned indexWidth, unsigned valueWidth) +{ + ASTNode n = bm.LookupOrCreateSymbol(name); + n.SetIndexWidth(indexWidth); + n.SetValueWidth(valueWidth); + return n; +} diff --git a/src/AST/NodeFactory/NodeFactory.h b/src/AST/NodeFactory/NodeFactory.h index 1317ad9..e09934d 100644 --- a/src/AST/NodeFactory/NodeFactory.h +++ b/src/AST/NodeFactory/NodeFactory.h @@ -10,6 +10,7 @@ namespace BEEV class ASTNode; typedef std::vector ASTVec; extern ASTVec _empty_ASTVec; +class STPMgr; } using BEEV::ASTNode; @@ -19,7 +20,12 @@ using BEEV::_empty_ASTVec; class NodeFactory { +protected: + BEEV::STPMgr& bm; + public: + NodeFactory(BEEV::STPMgr& bm_) : bm(bm_){} + virtual ~NodeFactory(); virtual BEEV::ASTNode CreateTerm(Kind kind, unsigned int width, @@ -31,6 +37,7 @@ public: virtual BEEV::ASTNode CreateNode(Kind kind, const BEEV::ASTVec& children) =0; + ASTNode CreateSymbol(const char * const name, unsigned indexWidth, unsigned valueWidth); ASTNode CreateTerm(Kind kind, unsigned int width, const ASTNode& child0, const ASTVec &children = _empty_ASTVec); diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.h b/src/AST/NodeFactory/SimplifyingNodeFactory.h index c5ce410..75ddeab 100644 --- a/src/AST/NodeFactory/SimplifyingNodeFactory.h +++ b/src/AST/NodeFactory/SimplifyingNodeFactory.h @@ -30,7 +30,6 @@ class SimplifyingNodeFactory: public NodeFactory private: NodeFactory& hashing; - BEEV::STPMgr& bm; // Only here until the const evaluator is pulled out. const ASTNode& ASTTrue; const ASTNode& ASTFalse; @@ -57,7 +56,7 @@ public: SimplifyingNodeFactory(NodeFactory& raw_, BEEV::STPMgr& bm_) - :hashing(raw_), bm(bm_), ASTTrue(bm.ASTTrue), ASTFalse(bm.ASTFalse), ASTUndefined(bm.ASTUndefined) + :hashing(raw_), NodeFactory(bm_), ASTTrue(bm_.ASTTrue), ASTFalse(bm_.ASTFalse), ASTUndefined(bm_.ASTUndefined) { } ; diff --git a/src/AST/NodeFactory/TypeChecker.h b/src/AST/NodeFactory/TypeChecker.h index dd23762..840bf17 100644 --- a/src/AST/NodeFactory/TypeChecker.h +++ b/src/AST/NodeFactory/TypeChecker.h @@ -17,10 +17,9 @@ using BEEV::STPMgr; class TypeChecker : public NodeFactory { NodeFactory& f; -STPMgr& bm; public: - TypeChecker(NodeFactory& f_, STPMgr& bm_) : f(f_), bm(bm_) + TypeChecker(NodeFactory& f_, STPMgr& bm_) : f(f_), NodeFactory(bm) {} BEEV::ASTNode CreateTerm(BEEV::Kind kind, unsigned int width, const BEEV::ASTVec &children); diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp index 207e9e9..dd11064 100644 --- a/src/STPManager/STPManager.cpp +++ b/src/STPManager/STPManager.cpp @@ -89,11 +89,11 @@ namespace BEEV //////////////////////////////////////////////////////////////// // STPMgr member functions to create ASTSymbol and ASTBVConst //////////////////////////////////////////////////////////////// - ASTNode STPMgr::CreateSymbol(const char * const name) + ASTNode STPMgr::LookupOrCreateSymbol(const char * const name) { - ASTSymbol temp_sym(name); + ASTSymbol temp_sym(name); ASTNode n(LookupOrCreateSymbol(temp_sym)); - return n; + return n; } // FIXME: _name is now a constant field, and this assigns to it @@ -666,10 +666,8 @@ namespace BEEV std::string ccc(d); c += "_solver_" + ccc; - ASTNode CurrentSymbol = CreateSymbol(c.c_str()); + ASTNode CurrentSymbol = CreateSymbol(c.c_str(),0,n); assert(0 !=n); - CurrentSymbol.SetValueWidth(n); - CurrentSymbol.SetIndexWidth(0); return CurrentSymbol; } //end of NewVar() @@ -733,9 +731,7 @@ namespace BEEV str += "("; str += outNum.str(); str += ")"; - ASTNode CurrentSymbol = CreateSymbol(str.c_str()); - CurrentSymbol.SetValueWidth(0); - CurrentSymbol.SetIndexWidth(0); + ASTNode CurrentSymbol = CreateSymbol(str.c_str(),0,0); return CurrentSymbol; } // End of NewParameterized_BooleanVar() diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h index c7dc7ec..7bb4770 100644 --- a/src/STPManager/STPManager.h +++ b/src/STPManager/STPManager.h @@ -256,7 +256,7 @@ namespace BEEV ****************************************************************/ // Create and return an ASTNode for a symbol - ASTNode CreateSymbol(const char * const name); + ASTNode LookupOrCreateSymbol(const char * const name); // Create and return an ASTNode for a symbol Width is number of // bits. @@ -273,6 +273,12 @@ namespace BEEV * Create Node functions * ****************************************************************/ + inline ASTNode CreateSymbol(const char * const name, unsigned indexWidth, unsigned valueWidth) + { + return defaultNodeFactory->CreateSymbol(name,indexWidth,valueWidth); + } + + // Create and return an interior ASTNode inline BEEV::ASTNode CreateNode(BEEV::Kind kind, const BEEV::ASTVec& children = _empty_ASTVec) { @@ -305,6 +311,11 @@ namespace BEEV return defaultNodeFactory->CreateTerm(kind,width,children); } + inline BEEV::ASTNode CreateArrayTerm(BEEV::Kind kind, unsigned int indexWidth, unsigned int width, const BEEV::ASTVec &children =_empty_ASTVec) + { + return defaultNodeFactory->CreateArrayTerm(kind,indexWidth, width,children); + } + inline ASTNode CreateTerm(Kind kind, unsigned int width, const ASTNode& child0, const ASTVec &children = _empty_ASTVec) { return defaultNodeFactory->CreateTerm(kind, width, child0, children); @@ -382,10 +393,7 @@ namespace BEEV char d[32 + prefix.length()]; sprintf(d, "%s_%d", prefix.c_str(), _symbol_count++); - BEEV::ASTNode CurrentSymbol = CreateSymbol(d); - CurrentSymbol.SetValueWidth(valueWidth); - CurrentSymbol.SetIndexWidth(indexWidth); - + BEEV::ASTNode CurrentSymbol = CreateSymbol(d,indexWidth,valueWidth); return CurrentSymbol; } diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index 577f43a..d0569b8 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -668,9 +668,7 @@ Expr vc_varExpr1(VC vc, const char* name, int indexwidth, int valuewidth) { bmstar b = (bmstar)(((stpstar)vc)->bm); - node o = b->CreateSymbol(name); - o.SetIndexWidth(indexwidth); - o.SetValueWidth(valuewidth); + node o = b->CreateSymbol(name,indexwidth,valuewidth); nodestar output = new node(o); ////if(cinterface_exprdelete_on) created_exprs.push_back(output); @@ -685,24 +683,29 @@ Expr vc_varExpr(VC vc, const char * name, Type type) { bmstar b = (bmstar)(((stpstar)vc)->bm); nodestar a = (nodestar)type; - node o = b->CreateSymbol(name); + unsigned indexWidth; + unsigned valueWidth; + switch(a->GetKind()) { case BEEV::BITVECTOR: - o.SetIndexWidth(0); - o.SetValueWidth((*a)[0].GetUnsignedConst()); + indexWidth = 0; + valueWidth = (*a)[0].GetUnsignedConst(); break; case BEEV::ARRAY: - o.SetIndexWidth((*a)[0].GetUnsignedConst()); - o.SetValueWidth((*a)[1].GetUnsignedConst()); + indexWidth = (*a)[0].GetUnsignedConst(); + valueWidth = (*a)[1].GetUnsignedConst(); break; case BEEV::BOOLEAN: - o.SetIndexWidth(0); - o.SetValueWidth(0); + indexWidth = 0; + valueWidth = 0; break; default: BEEV::FatalError("CInterface: vc_varExpr: Unsupported type",*a); break; + } + node o = b->CreateSymbol(name,indexWidth,valueWidth); + nodestar output = new node(o); ////if(cinterface_exprdelete_on) created_exprs.push_back(output); BVTypeCheck(*output); diff --git a/src/parser/CVC.lex b/src/parser/CVC.lex index deb231c..fc26be2 100644 --- a/src/parser/CVC.lex +++ b/src/parser/CVC.lex @@ -122,7 +122,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) "POP" { return POP_TOK;} (({LETTER})|(_)({ANYTHING}))({ANYTHING})* { - BEEV::ASTNode nptr = (BEEV::ParserBM)->CreateSymbol(yytext); + BEEV::ASTNode nptr = parserInterface->LookupOrCreateSymbol(yytext); // Check valuesize to see if it's a prop var. I don't like doing // type determination in the lexer, but it's easier than rewriting diff --git a/src/parser/CVC.y b/src/parser/CVC.y index c5dedc0..1d20fcd 100644 --- a/src/parser/CVC.y +++ b/src/parser/CVC.y @@ -659,14 +659,14 @@ Formula : '(' Formula ')' | TRUELIT_TOK { $$ = new ASTNode(parserInterface->CreateNode(TRUE)); - $$->SetIndexWidth(0); - $$->SetValueWidth(0); + assert($$->GetIndexWidth() == 0); + assert($$->GetValueWidth() == 0); } | FALSELIT_TOK { $$ = new ASTNode(parserInterface->CreateNode(FALSE)); - $$->SetIndexWidth(0); - $$->SetValueWidth(0); + assert($$->GetIndexWidth() == 0); + assert($$->GetValueWidth() == 0); } | LET_TOK LetDecls IN_TOK Formula diff --git a/src/parser/ParserInterface.h b/src/parser/ParserInterface.h index b14be07..89569d8 100644 --- a/src/parser/ParserInterface.h +++ b/src/parser/ParserInterface.h @@ -87,9 +87,9 @@ public: return bm.CreateBVConst(width, bvconst); } - ASTNode CreateSymbol(const char * const name) + ASTNode LookupOrCreateSymbol(const char * const name) { - return bm.CreateSymbol(name); + return bm.LookupOrCreateSymbol(name); } }; } diff --git a/src/parser/smtlib.lex b/src/parser/smtlib.lex index 40362b7..4326f44 100644 --- a/src/parser/smtlib.lex +++ b/src/parser/smtlib.lex @@ -220,7 +220,7 @@ bit{DIGIT}+ { "boolbv" { return BOOL_TO_BV_TOK;} (({LETTER})|(_)({ANYTHING}))({ANYTHING})* { - BEEV::ASTNode nptr = parserInterface->CreateSymbol(smttext); + BEEV::ASTNode nptr = parserInterface->LookupOrCreateSymbol(smttext); // Check valuesize to see if it's a prop var. I don't like doing // type determination in the lexer, but it's easier than rewriting diff --git a/src/parser/smtlib2.lex b/src/parser/smtlib2.lex index 1c821b0..edeae9c 100644 --- a/src/parser/smtlib2.lex +++ b/src/parser/smtlib2.lex @@ -68,7 +68,7 @@ if (s[0] == '|' && s[str.size()-1] == '|') str = str.substr(1,str.length()-2); - BEEV::ASTNode nptr = BEEV::parserInterface->CreateSymbol(str.c_str()); + BEEV::ASTNode nptr = BEEV::parserInterface->LookupOrCreateSymbol(str.c_str()); // Check valuesize to see if it's a prop var. I don't like doing // type determination in the lexer, but it's easier than rewriting diff --git a/src/printer/SMTLIBPrinter.cpp b/src/printer/SMTLIBPrinter.cpp index 18ccb27..5932df3 100644 --- a/src/printer/SMTLIBPrinter.cpp +++ b/src/printer/SMTLIBPrinter.cpp @@ -151,9 +151,7 @@ static string tolower(const char * name) oss << "?let_k_" << sz; ASTNode CurrentSymbol = n.GetSTPMgr()->CreateSymbol( - oss.str().c_str()); - CurrentSymbol.SetValueWidth(n.GetValueWidth()); - CurrentSymbol.SetIndexWidth(n.GetIndexWidth()); + oss.str().c_str(),n.GetIndexWidth(), n.GetValueWidth()); /* If for some reason the variable being created here is * already declared by the user then the printed output will * not be a legal input to the system. too bad. I refuse to diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp index 7cda322..1f24bf7 100644 --- a/src/simplifier/SubstitutionMap.cpp +++ b/src/simplifier/SubstitutionMap.cpp @@ -215,7 +215,7 @@ ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, if (n.GetIndexWidth() != 0) { const ASTNode& r = it->second; - r.SetIndexWidth(n.GetIndexWidth()); + assert(r.GetIndexWidth() == n.GetIndexWidth()); assert(BVTypeCheck(r)); ASTNode replaced = replace(r, fromTo, cache,nf); if (replaced != r) @@ -264,10 +264,10 @@ ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo, // If the index and value width aren't saved, they are reset sometimes (??) const unsigned int indexWidth = n.GetIndexWidth(); const unsigned int valueWidth = n.GetValueWidth(); - result = nf->CreateTerm(n.GetKind(), n.GetValueWidth(), + result = nf->CreateArrayTerm(n.GetKind(),indexWidth, n.GetValueWidth(), children); - result.SetValueWidth(valueWidth); - result.SetIndexWidth(indexWidth); + assert(result.GetValueWidth() == valueWidth); + } else result = n; diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index dab3a50..26bb1ee 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -966,6 +966,7 @@ namespace BEEV return nf->CreateNode(EQ, in1, in2); } + // nb. this is sometimes used to build array terms. //accepts cond == t1, then part is t2, and else part is t3 ASTNode Simplifier::CreateSimplifiedTermITE(const ASTNode& in0, const ASTNode& in1, @@ -989,7 +990,7 @@ namespace BEEV FatalError("CreateSimplifiedTermITE: "\ "the lengths of the two branches don't match", t1); } - return nf->CreateTerm(ITE, t1.GetValueWidth(), t0, t1, t2); + return nf->CreateArrayTerm(ITE, t1.GetIndexWidth(),t1.GetValueWidth(), t0, t1, t2); } if (t0 == ASTTrue) @@ -1009,7 +1010,7 @@ namespace BEEV return t2; } - return nf->CreateTerm(ITE, t1.GetValueWidth(), t0, t1, t2); + return nf->CreateArrayTerm(ITE, t1.GetIndexWidth(),t1.GetValueWidth(), t0, t1, t2); } ASTNode @@ -1690,8 +1691,7 @@ namespace BEEV assert(v.size() > 0); if (v != actualInputterm.GetChildren()) // short-cut. { - output = nf->CreateTerm(k, inputValueWidth, v); - output.SetIndexWidth(actualInputterm.GetIndexWidth()); + output = nf->CreateArrayTerm(k,actualInputterm.GetIndexWidth(), inputValueWidth, v); } else output = actualInputterm; @@ -3321,7 +3321,7 @@ namespace BEEV SimplifyFormula(term[0],VarConstMap), SimplifyArrayTerm(term[1], VarConstMap), SimplifyArrayTerm(term[2], VarConstMap)); - output.SetIndexWidth(iw); + assert(output.GetIndexWidth() == iw); } break; case WRITE: { @@ -3330,8 +3330,7 @@ namespace BEEV ASTNode idx = SimplifyTerm(term[1]); ASTNode val = SimplifyTerm(term[2]); - output = nf->CreateTerm(WRITE, term.GetValueWidth(), array, idx, val); - output.SetIndexWidth(iw); // save the value and set, otherwise it sometimes fails. + output = nf->CreateArrayTerm(WRITE,iw, term.GetValueWidth(), array, idx, val); } break; diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp index 9f87cbf..d3e3141 100644 --- a/src/to-sat/ToCNF.cpp +++ b/src/to-sat/ToCNF.cpp @@ -561,15 +561,9 @@ namespace BEEV ostringstream oss; oss << "cnf" << "{" << varphi.GetNodeNum() << "}"; - psi = bm->CreateSymbol(oss.str().c_str()); - - //######################################## - // step 2, set widths appropriately - //######################################## - - psi.SetValueWidth(varphi.GetValueWidth()); - psi.SetIndexWidth(varphi.GetIndexWidth()); + psi = bm->CreateSymbol(oss.str().c_str(),varphi.GetIndexWidth(),varphi.GetValueWidth()); + //######################################## // step 3, recurse over children //######################################## @@ -609,7 +603,7 @@ namespace BEEV ostringstream oss; oss << "cnf" << "{" << varphi.GetNodeNum() << "}"; - ASTNode psi = bm->CreateSymbol(oss.str().c_str()); + ASTNode psi = bm->CreateSymbol(oss.str().c_str(),0,0); //######################################## // step 2, add defs @@ -640,7 +634,7 @@ namespace BEEV ostringstream oss; oss << "cnf" << "{" << varphi.GetNodeNum() << "}"; - ASTNode psi = bm->CreateSymbol(oss.str().c_str()); + ASTNode psi = bm->CreateSymbol(oss.str().c_str(),0,0); //######################################## // step 2, add defs @@ -707,7 +701,7 @@ namespace BEEV ostringstream oss; oss << "cnf" << "{" << varphi.GetNodeNum() << "}"; - ASTNode psi = bm->CreateSymbol(oss.str().c_str()); + ASTNode psi = bm->CreateSymbol(oss.str().c_str(),0,0); //######################################## // step 3, add defs @@ -918,14 +912,14 @@ namespace BEEV ClauseList* defs) { ASTNode dummy_false_var = - bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*")); + bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*",0,0)); info[varphi]->clausespos = SINGLETON(dummy_false_var); } //End of convertFormulaToCNFPosFALSE() void CNFMgr::convertFormulaToCNFPosTRUE(const ASTNode& varphi, ClauseList* defs) { - ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*"); + ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*",0,0); info[varphi]->clausespos = SINGLETON(dummy_true_var); } //End of convertFormulaToCNFPosTRUE @@ -1292,7 +1286,7 @@ namespace BEEV void CNFMgr::convertFormulaToCNFNegFALSE(const ASTNode& varphi, ClauseList* defs) { - ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*"); + ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*",0,0); info[varphi]->clausesneg = SINGLETON(dummy_true_var); } //End of convertFormulaToCNFNegFALSE() @@ -1300,7 +1294,7 @@ namespace BEEV ClauseList* defs) { ASTNode dummy_false_var = - bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*")); + bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*",0,0)); info[varphi]->clausesneg = SINGLETON(dummy_false_var); } //End of convertFormulaToCNFNegTRUE() @@ -1773,7 +1767,7 @@ namespace BEEV { bm->GetRunTimes()->start(RunTimes::CNFConversion); scanFormula(varphi, true, false); - ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*"); + ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*",0,0); ClauseList* defs = SINGLETON(dummy_true_var); convertFormulaToCNF(varphi, defs); ClauseList* top = info[varphi]->clausespos;