From: trevor_hansen Date: Sat, 18 Apr 2009 15:23:04 +0000 (+0000) Subject: Simplifications to speed up convert-tiff2jpg-query-1831.smt by >100,000 times. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=439c511e86728f4f12cb8434617b758d47ffd910;p=francis%2Fstp.git Simplifications to speed up convert-tiff2jpg-query-1831.smt by >100,000 times. * Some SMT-LIB format outputting of expression. * Parsing arbitary length bitvector input strings via the C-interface. * No more memory leaks from the _letid_expr_map & co. * const& to reduce copy constructor usage in BVTypeCheck. * Checks for equality on some fixed bits. e.g. (= bv0[16] (concat bv1[15] x)) == false. * Reduces multiplications with leading 1's to a minus. e.g. 255*x == -1*x. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@68 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/AST/AST.cpp b/AST/AST.cpp index 1549353..d61f0ca 100644 --- a/AST/AST.cpp +++ b/AST/AST.cpp @@ -686,6 +686,177 @@ namespace BEEV { } //end of PL_Print1() + // copied from Presentation Langauge printer. + ostream& ASTNode::SMTLIB_Print(ostream &os, int indentation) const { + // Clear the PrintMap + BeevMgr& bm = GetBeevMgr(); + bm.PLPrintNodeSet.clear(); + bm.NodeLetVarMap.clear(); + bm.NodeLetVarVec.clear(); + bm.NodeLetVarMap1.clear(); + + //pass 1: letize the node + LetizeNode(); + + //pass 2: + // + //2. print all the let variables and their counterpart expressions + //2. as follows (LET var1 = expr1, var2 = expr2, ... + // + //3. Then print the Node itself, replacing every occurence of + //3. expr1 with var1, expr2 with var2, ... + //os << "("; + if(0 < bm.NodeLetVarMap.size()) { + //ASTNodeMap::iterator it=bm.NodeLetVarMap.begin(); + //ASTNodeMap::iterator itend=bm.NodeLetVarMap.end(); + std::vector >::iterator it = bm.NodeLetVarVec.begin(); + std::vector >::iterator itend = bm.NodeLetVarVec.end(); + + os << "(LET "; + //print the let var first + it->first.SMTLIB_Print1(os,indentation,false); + os << " = "; + //print the expr + it->second.SMTLIB_Print1(os,indentation,false); + + //update the second map for proper printing of LET + bm.NodeLetVarMap1[it->second] = it->first; + + for(it++;it!=itend;it++) { + os << "," << endl; + //print the let var first + it->first.SMTLIB_Print1(os,indentation,false); + os << " = "; + //print the expr + it->second.SMTLIB_Print1(os,indentation,false); + + //update the second map for proper printing of LET + bm.NodeLetVarMap1[it->second] = it->first; + } + + os << " IN " << endl; + SMTLIB_Print1(os,indentation, true); + os << ") "; + } + else + SMTLIB_Print1(os,indentation, false); + return os; + } + + + + + +void ASTNode::SMTLIB_Print1(ostream& os, + int indentation, + bool letize) const +{ + //os << spaces(indentation); + //os << endl << spaces(indentation); + if (!IsDefined()) { + os << ""; + return; + } + + //if this node is present in the letvar Map, then print the letvar + BeevMgr &bm = GetBeevMgr(); + + //this is to print letvars for shared subterms inside the printing + //of "(LET v0 = term1, v1=term1@term2,... + if((bm.NodeLetVarMap1.find(*this) != bm.NodeLetVarMap1.end()) && !letize) { + (bm.NodeLetVarMap1[*this]).SMTLIB_Print1(os,indentation,letize); + return; + } + + //this is to print letvars for shared subterms inside the actual + //term to be printed + if((bm.NodeLetVarMap.find(*this) != bm.NodeLetVarMap.end()) && letize) { + (bm.NodeLetVarMap[*this]).SMTLIB_Print1(os,indentation,letize); + return; + } + + //otherwise print it normally + Kind kind = GetKind(); + const ASTVec &c = GetChildren(); + switch(kind) + { + case BITVECTOR: // Not sure how this is differen to a BVCONST?? + {os << "bv"; + unsigned char * str; + str = CONSTANTBV::BitVector_to_Dec(c[0].GetBVConst()); + os << str << "[" << c[0].GetValueWidth() << "]"; + CONSTANTBV::BitVector_Dispose(str); + } + break; + case BVCONST: + { + os << "bv"; + unsigned char * str; + str = CONSTANTBV::BitVector_to_Dec(GetBVConst()); + os << str << "[" << GetValueWidth() << "]"; + CONSTANTBV::BitVector_Dispose(str); + } + break; + case SYMBOL: + _int_node_ptr->nodeprint(os); + break; + case FALSE: + os << "false"; + break; + case TRUE: + os << "true"; + break; + case BVEXTRACT: + { + unsigned int upper = GetUnsignedConst(c[1]); + unsigned int lower = GetUnsignedConst(c[2]); + assert(upper > lower); + os << "(extract[" << upper << ":" << lower << "] "; + c[0].SMTLIB_Print1(os,indentation,letize); + os << ")"; + } + default: + { + os << "(" << functionToSMTLIBName(kind); + + ASTVec::const_iterator iend = c.end(); + for (ASTVec::const_iterator i = c.begin(); i != iend; i++) + { + os << " "; + i->SMTLIB_Print1(os,0,letize); + } + + os << ")"; + } + } +} + +string ASTNode::functionToSMTLIBName(const Kind k) const +{ + switch(k) + { + case AND: + case OR: + case NAND: + case NOR: + case XOR: + case BVAND: + case BVNEG: + case ITE: + case BVOR: + case NOT: + return _kind_names[k]; + + case BVMULT: return "bvmul"; + case WRITE: return "store"; + case EQ: return "="; + case BVCONCAT: return "concat"; + + default: + FatalError(_kind_names[k]); + } +} + // printer for C code (copied from PL_Print()) // TODO: this does not fully implement printing of all of the STP // language - FatalError calls inserted for unimplemented @@ -1303,7 +1474,7 @@ namespace BEEV { return CreateBVConst(bv,width); } - ASTNode BeevMgr::CreateBVConst(string*& strval, unsigned int base, size_t bit_width) { + ASTNode BeevMgr::CreateBVConst(string*& strval, int base, int bit_width) { if(!(2 == base || 10 == base || 16 == base)) { @@ -1661,7 +1832,7 @@ namespace BEEV { void BeevMgr::BVTypeCheck(const ASTNode& n) { Kind k = n.GetKind(); //The children of bitvector terms are in turn bitvectors. - ASTVec v = n.GetChildren(); + const ASTVec& v = n.GetChildren(); if(is_Term_kind(k)) { switch(k) { case BVCONST: @@ -1707,7 +1878,7 @@ namespace BEEV { if(!(v.size() >= 2)) FatalError("BVTypeCheck:bitwise Booleans and BV arith operators must have atleast two arguments\n",n); unsigned int width = n.GetValueWidth(); - for(ASTVec::iterator it=v.begin(),itend=v.end();it!=itend;it++){ + for(ASTVec::const_iterator it=v.begin(),itend=v.end();it!=itend;it++){ if(width != it->GetValueWidth()) { cerr << "BVTypeCheck:Operands of bitwise-Booleans and BV arith operators must be of equal length\n"; cerr << n << endl; @@ -1737,7 +1908,7 @@ namespace BEEV { break; default: - for(ASTVec::iterator it=v.begin(),itend=v.end();it!=itend;it++) + for(ASTVec::const_iterator it=v.begin(),itend=v.end();it!=itend;it++) if(BITVECTOR_TYPE != it->GetType()) { cerr << "The type is: " << it->GetType() << endl; FatalError("BVTypeCheck:ChildNodes of bitvector-terms must be bitvectors\n",n); @@ -2162,6 +2333,10 @@ namespace BEEV { BeevMgr::~BeevMgr() { ClearAllTables(); + + delete SimplifyMap; + delete SimplifyNegMap; + delete _letid_expr_map; } }; // end namespace diff --git a/AST/AST.h b/AST/AST.h index c46c960..4ec8e7f 100644 --- a/AST/AST.h +++ b/AST/AST.h @@ -123,6 +123,8 @@ namespace BEEV { return ((size_t) node1._int_node_ptr) < ((size_t) node2._int_node_ptr); } + string functionToSMTLIBName(const Kind k) const; + public: //Check if it points to a null node bool IsNull () const { return _int_node_ptr == NULL; } @@ -299,6 +301,9 @@ namespace BEEV { ostream& C_Print(ostream &os, int indentation = 0) const; void C_Print1(ostream &os, int indentation = 0, bool b = false) const; + ostream& SMTLIB_Print(ostream &os, int indentation) const; + void SMTLIB_Print1(ostream& os, int indentation, bool letize) const; + //Construct let variables for shared subterms void LetizeNode(void) const; @@ -1383,7 +1388,7 @@ namespace BEEV { // Create and return an ASTNode for a symbol // Width is number of bits. - ASTNode CreateBVConst(string*& strval, unsigned int base, size_t bit_width); + ASTNode CreateBVConst(string*& strval, int base, int bit_width); ASTNode CreateBVConst(unsigned int width, unsigned long long int bvconst); ASTNode CreateZeroConst(unsigned int width); ASTNode CreateOneConst(unsigned int width); diff --git a/c_interface/c_interface.cpp b/c_interface/c_interface.cpp index b8882d5..32be6ec 100644 --- a/c_interface/c_interface.cpp +++ b/c_interface/c_interface.cpp @@ -134,6 +134,16 @@ void vc_printExpr(VC vc, Expr e) { q.PL_Print(cout); } +char * vc_printSMTLIB(VC vc, Expr e) +{ + stringstream ss; + ((nodestar)e)->SMTLIB_Print(ss,0); + string s = ss.str(); + char *copy = strdup(s.c_str()); + return copy; + +} + // prints Expr 'e' to stdout as C code void vc_printExprCCode(VC vc, Expr e) { BEEV::ASTNode q = (*(nodestar)e); @@ -738,6 +748,18 @@ Type vc_bv32Type(VC vc) { return vc_bvType(vc,32); } +Expr vc_bvConstExprFromDecStr(VC vc, const size_t width, char* decimalInput ) { + bmstar b = (bmstar)vc; + + string *param = new string(decimalInput); + // funny type to get it to compile. fix later when I understand what this does. + node n = b->CreateBVConst((string*&)param, (int)10,(int)width); + b->BVTypeCheck(n); + nodestar output = new node(n); + delete param; + return output; +} + Expr vc_bvConstExprFromStr(VC vc, char* binary_repr) { bmstar b = (bmstar)vc; @@ -1436,7 +1458,6 @@ static char *val_to_binary_str(unsigned nbits, unsigned long long val) { } #endif - Expr vc_parseExpr(VC vc, char* infile) { bmstar b = (bmstar)vc; extern FILE* cvcin; diff --git a/c_interface/c_interface.h b/c_interface/c_interface.h index 35afbd6..7b1b51b 100644 --- a/c_interface/c_interface.h +++ b/c_interface/c_interface.h @@ -120,6 +120,9 @@ extern "C" { //! Prints 'e' to stdout as C code void vc_printExprCCode(VC vc, Expr e); + //! print in smtlib format + char * vc_printSMTLIB(VC vc, Expr e); + //! Prints 'e' into an open file descriptor 'fd' void vc_printExprFile(VC vc, Expr e, int fd); @@ -203,6 +206,7 @@ extern "C" { Type vc_bvType(VC vc, int no_bits); Type vc_bv32Type(VC vc); + Expr vc_bvConstExprFromDecStr(VC vc, const size_t width, char* decimalInput ); Expr vc_bvConstExprFromStr(VC vc, char* binary_repr); Expr vc_bvConstExprFromInt(VC vc, int n_bits, unsigned int value); Expr vc_bvConstExprFromLL(VC vc, int n_bits, unsigned long long value); diff --git a/simplifier/simplifier.cpp b/simplifier/simplifier.cpp index 7725305..ff0e4dc 100644 --- a/simplifier/simplifier.cpp +++ b/simplifier/simplifier.cpp @@ -537,6 +537,48 @@ namespace BEEV { if(BVCONST == k1 && BVCONST == k2) return ASTFalse; + // can concat have multiple children? + // so (= (concat bv1[24] x ) bv0[32]) == false + if((BVCONCAT==k1 && BVCONST== k2) ||(BVCONCAT==k2 && BVCONST== k1) ) + { + ASTNode concat = (k1 == BVCONCAT)? in1: in2; + ASTNode constant = (k1 == BVCONST)? in1: in2; + + if(concat.GetChildren().size() == 2 && + (BVCONST == concat.GetChildren()[0].GetKind() || BVCONST == concat.GetChildren()[1].GetKind())) + { + int start; + CBV partial; + int partialWidth; + ASTNode other; + + if (BVCONST == concat.GetChildren()[0].GetKind()) + { + start = concat.GetChildren()[1].GetValueWidth(); + partial = concat.GetChildren()[0].GetBVConst(); + partialWidth = concat.GetChildren()[0].GetValueWidth(); + other = concat.GetChildren()[1]; + } + else + { + start = 0; + partial = concat.GetChildren()[1].GetBVConst(); + partialWidth = concat.GetChildren()[1].GetValueWidth(); + other = concat.GetChildren()[0]; + } + + CBV complete = constant.GetBVConst(); + + for (int i = 0; i < partialWidth; i++) + if (CONSTANTBV::BitVector_bit_test(partial,i) != CONSTANTBV::BitVector_bit_test(complete,i+start)) + return ASTFalse; + + // if we get to here then the two constants in the equality are the same. Remove the constants. + + return CreateNode(EQ,other,CreateTerm(BVEXTRACT,other.GetValueWidth(),constant,CreateBVConst(32, partialWidth+other.GetValueWidth()-1),CreateBVConst(32,partialWidth))); + } + } + //last resort is to CreateNode return CreateNode(EQ,in1,in2); } @@ -1063,11 +1105,63 @@ namespace BEEV { output = inputterm; break; case BVMULT: - case BVPLUS:{ - if(BVMULT == k && 2 != inputterm.Degree()) { - FatalError("SimplifyTerm: We assume that BVMULT is binary",inputterm); + { + if(2 != inputterm.Degree()) + { + FatalError("SimplifyTerm: We assume that BVMULT is binary",inputterm); } + // Described nicely by Warren, Hacker's Delight pg 135. + // Turn sequences of one bits into subtractions. + // 28*x == 32x - 4x (two instructions), rather than 16x+ 8x+ 4x. + // When fully implemented. I.e. supporting sequences of 1 anywhere. + // Other simplifications will try to fold these back in. So need to be careful + // about when the simplifications are applied. But in this version it won't + // be simplified down by anything else. + + + // This (temporary) version only simplifies if all the left most bits are set. + // All the leftmost bits being set simplifies very nicely down. + const ASTNode& n0 = inputterm.GetChildren()[0]; + const ASTNode& n1 = inputterm.GetChildren()[1]; + + if (BVCONST == n0.GetKind() || BVCONST == n1.GetKind()) + { + // assuming that if both are constants it is handled already. + assert(BVCONST == n0.GetKind() ^ BVCONST == n1.GetKind()); + + CBV constant = (BVCONST == n0.GetKind())? n0.GetBVConst(): n1.GetBVConst(); + ASTNode other = (BVCONST == n0.GetKind())? n1: n0; + + int startSequence = 0; + for (unsigned int i = 0; i < inputValueWidth; i++) + { + if (!CONSTANTBV::BitVector_bit_test(constant,i)) + startSequence = i; + } + + if((inputValueWidth - startSequence) > 3) + { + // turn off all bits from "startSequence to the end", then add one. + CBV maskedPlusOne = CONSTANTBV::BitVector_Create(inputValueWidth,true); + for (int i=0; i < startSequence;i++) + { + if (!CONSTANTBV::BitVector_bit_test(constant,i)) // swap + CONSTANTBV::BitVector_Bit_On(maskedPlusOne, i); + } + CONSTANTBV::BitVector_increment(maskedPlusOne); + ASTNode& temp = CreateTerm(BVMULT,inputValueWidth, CreateBVConst(maskedPlusOne,inputValueWidth),other); + output = CreateTerm(BVNEG, inputValueWidth, temp); + } + } + if(NULL == output) + output = inputterm; + + } + break; + + case BVPLUS:{ + ASTVec c = FlattenOneLevel(inputterm).GetChildren(); SortByArith(c); ASTVec constkids, nonconstkids; @@ -1643,6 +1737,8 @@ namespace BEEV { return inputterm; break; } + assert(NULL != output); + //memoize UpdateSimplifyMap(inputterm,output,false); @@ -2298,7 +2394,7 @@ namespace BEEV { return output; } - ASTVec c = a.GetChildren(); + const ASTVec& c = a.GetChildren(); //map from variables to vector of constants ASTNodeToVecMap vars_to_consts; //vector to hold constants