} //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<pair<ASTNode,ASTNode> >::iterator it = bm.NodeLetVarVec.begin();
+ std::vector<pair<ASTNode,ASTNode> >::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 << "<undefined>";
+ 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
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))
{
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:
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;
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);
BeevMgr::~BeevMgr() {
ClearAllTables();
+
+ delete SimplifyMap;
+ delete SimplifyNegMap;
+ delete _letid_expr_map;
}
}; // end namespace
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; }
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;
// 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);
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);
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;
}
#endif
-
Expr vc_parseExpr(VC vc, char* infile) {
bmstar b = (bmstar)vc;
extern FILE* cvcin;
//! 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);
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);
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);
}
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;
return inputterm;
break;
}
+ assert(NULL != output);
+
//memoize
UpdateSimplifyMap(inputterm,output,false);
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
projects / francis / stp.git / commitdiff