void ASTNode::MarkAlreadyPrinted() const
{
- // FIXME: Fetching BeevMgr is annoying. Can we put this in lispprinter class?
BeevMgr &bm = GetBeevMgr();
bm.AlreadyPrintedSet.insert(*this);
}
//
//2. Letize its childNodes
- //FIXME: Fetching BeevMgr is annoying. Can we put this in
- //some kind of a printer class
bm.PLPrintNodeSet.insert(ccc);
//debugging
//cerr << ccc;
exit(-1);
//assert(0);
}
-
- //Variable Order Printer: A global function which converts a MINISAT
- //var into a ASTNODE var. It then prints this var along with
- //variable order dcisions taken by MINISAT.
- void Convert_MINISATVar_To_ASTNode_Print(int minisat_var, int decision_level, int polarity)
- {
- BEEV::ASTNode vv = globalBeevMgr_for_parser->_SATVar_to_AST[minisat_var];
- cout << spaces(decision_level);
- if (polarity)
- {
- cout << "!";
- }
- printer::PL_Print(cout,vv, 0);
- cout << endl;
- }
-
+
void SortByExprNum(ASTVec& v)
{
sort(v.begin(), v.end(), exprless);
bool isAtomic(Kind kind)
{
- if (TRUE == kind || FALSE == kind || EQ == kind || NEQ == kind || BVLT == kind || BVLE == kind || BVGT == kind || BVGE == kind || BVSLT == kind
- || BVSLE == kind || BVSGT == kind || BVSGE == kind || SYMBOL == kind || BVGETBIT == kind)
+ if (TRUE == kind || FALSE == kind ||
+ EQ == kind || NEQ == kind ||
+ BVLT == kind || BVLE == kind ||
+ BVGT == kind || BVGE == kind ||
+ BVSLT == kind || BVSLE == kind ||
+ BVSGT == kind || BVSGE == kind ||
+ SYMBOL == kind || BVGETBIT == kind)
return true;
return false;
}
delete ReferenceCount;
}
-}
-; // end namespace
+}; // end namespace beev
}
} //end of arithless
- // Internal lisp-form printer that does not clear _node_print_table
- //ostream &LispPrint1(ostream &os, int indentation) const;
-
// For lisp DAG printing. Has it been printed already, so we can
// just print the node number?
bool IsAlreadyPrinted() const;
ostream& LispPrint(ostream &os, int indentation = 0) const;
ostream &LispPrint_indent(ostream &os, int indentation) const;
-
//Presentation Language Printer
ostream& PL_Print(ostream &os, int indentation = 0) const;
class ASTInteriorEqual
{
public:
- bool operator()(const ASTInterior *int_node_ptr1, const ASTInterior *int_node_ptr2) const
+ bool operator()(const ASTInterior *int_node_ptr1,
+ const ASTInterior *int_node_ptr2) const
{
return (*int_node_ptr1 == *int_node_ptr2);
}
};
// Used in Equality class for hash tables
- friend bool operator==(const ASTInterior &int_node1, const ASTInterior &int_node2)
+ friend bool operator==(const ASTInterior &int_node1,
+ const ASTInterior &int_node2)
{
- return (int_node1._kind == int_node2._kind) && (int_node1._children == int_node2._children);
+ return (int_node1._kind == int_node2._kind) &&
+ (int_node1._children == int_node2._children);
}
// Call this when deleting a node that has been stored in the
virtual void CleanUp();
// Returns kinds. "lispprinter" handles printing of parenthesis
- // and childnodes.
- // (c_friendly is for printing hex. numbers that C compilers will accept)
+ // and childnodes. (c_friendly is for printing hex. numbers that C
+ // compilers will accept)
virtual void nodeprint(ostream& os, bool c_friendly = false)
{
os << _kind_names[_kind];
private:
// Typedef for unique Interior node table.
- typedef hash_set<ASTInterior *, ASTInterior::ASTInteriorHasher, ASTInterior::ASTInteriorEqual> ASTInteriorSet;
+ typedef hash_set<ASTInterior *,
+ ASTInterior::ASTInteriorHasher,
+ ASTInterior::ASTInteriorEqual> ASTInteriorSet;
// Typedef for unique Symbol node (leaf) table.
- typedef hash_set<ASTSymbol *, ASTSymbol::ASTSymbolHasher, ASTSymbol::ASTSymbolEqual> ASTSymbolSet;
+ typedef hash_set<ASTSymbol *,
+ ASTSymbol::ASTSymbolHasher,
+ ASTSymbol::ASTSymbolEqual> ASTSymbolSet;
// Unique tables to share nodes whenever possible.
ASTInteriorSet _interior_unique_table;
ASTSymbolSet _symbol_unique_table;
//Typedef for unique BVConst node (leaf) table.
- typedef hash_set<ASTBVConst *, ASTBVConst::ASTBVConstHasher, ASTBVConst::ASTBVConstEqual> ASTBVConstSet;
+ typedef hash_set<ASTBVConst *,
+ ASTBVConst::ASTBVConstHasher,
+ ASTBVConst::ASTBVConstEqual> ASTBVConstSet;
//table to uniquefy bvconst
ASTBVConstSet _bvconst_unique_table;
// type of memo table.
- typedef hash_map<ASTNode, ASTVec, ASTNode::ASTNodeHasher, ASTNode::ASTNodeEqual> ASTNodeToVecMap;
+ typedef hash_map<ASTNode,
+ ASTVec,
+ ASTNode::ASTNodeHasher,
+ ASTNode::ASTNodeEqual> ASTNodeToVecMap;
- typedef hash_map<ASTNode, ASTNodeSet, ASTNode::ASTNodeHasher, ASTNode::ASTNodeEqual> ASTNodeToSetMap;
+ typedef hash_map<ASTNode,
+ ASTNodeSet,
+ ASTNode::ASTNodeHasher,
+ ASTNode::ASTNodeEqual> ASTNodeToSetMap;
// Memo table for bit blasted terms. If a node has already been
// bitblasted, it is mapped to a vector of Boolean formulas for
// Simplifying create functions
ASTNode CreateSimpForm(Kind kind, ASTVec &children);
ASTNode CreateSimpForm(Kind kind, const ASTNode& child0);
- ASTNode CreateSimpForm(Kind kind, const ASTNode& child0, const ASTNode& child1);
- ASTNode CreateSimpForm(Kind kind, const ASTNode& child0, const ASTNode& child1, const ASTNode& child2);
+ ASTNode CreateSimpForm(Kind kind,
+ const ASTNode& child0, const ASTNode& child1);
+ ASTNode CreateSimpForm(Kind kind, const ASTNode& child0,
+ const ASTNode& child1, const ASTNode& child2);
ASTNode CreateSimpNot(const ASTNode& form);
// not in AST.h
ASTNode CreateSimpXor(const ASTNode& form1, const ASTNode& form2);
ASTNode CreateSimpXor(ASTVec &children);
- ASTNode CreateSimpAndOr(bool isAnd, const ASTNode& form1, const ASTNode& form2);
+ ASTNode CreateSimpAndOr(bool isAnd,
+ const ASTNode& form1, const ASTNode& form2);
ASTNode CreateSimpAndOr(bool IsAnd, ASTVec &children);
- ASTNode CreateSimpFormITE(const ASTNode& child0, const ASTNode& child1, const ASTNode& child2);
+ ASTNode CreateSimpFormITE(const ASTNode& child0,
+ const ASTNode& child1, const ASTNode& child2);
// Declarations of BitBlaster functions (BitBlast.cpp)
public:
// Create and return an interior ASTNode
ASTNode CreateNode(Kind kind, const ASTVec &children = _empty_ASTVec);
- ASTNode CreateNode(Kind kind, const ASTNode& child0, const ASTVec &children = _empty_ASTVec);
+ ASTNode CreateNode(Kind kind, const ASTNode& child0,
+ const ASTVec &children = _empty_ASTVec);
- ASTNode CreateNode(Kind kind, const ASTNode& child0, const ASTNode& child1, const ASTVec &children = _empty_ASTVec);
+ ASTNode CreateNode(Kind kind, const ASTNode& child0,
+ const ASTNode& child1, const ASTVec &children = _empty_ASTVec);
- ASTNode CreateNode(Kind kind, const ASTNode& child0, const ASTNode& child1, const ASTNode& child2, const ASTVec &children = _empty_ASTVec);
+ ASTNode CreateNode(Kind kind, const ASTNode& child0,
+ const ASTNode& child1, const ASTNode& child2,
+ const ASTVec &children = _empty_ASTVec);
// Create and return an ASTNode for a term
inline ASTNode CreateTerm(Kind kind, unsigned int width, const ASTVec &children = _empty_ASTVec)
return n;
}
- inline ASTNode CreateTerm(Kind kind, unsigned int width, const ASTNode& child0, const ASTVec &children = _empty_ASTVec)
+ inline ASTNode CreateTerm(Kind kind, unsigned int width,
+ const ASTNode& child0, const ASTVec &children = _empty_ASTVec)
{
if (!is_Term_kind(kind))
FatalError("CreateTerm: Illegal kind to CreateTerm:", ASTUndefined, kind);
return n;
}
- inline ASTNode CreateTerm(Kind kind, unsigned int width, const ASTNode& child0, const ASTNode& child1, const ASTVec &children = _empty_ASTVec)
+ inline ASTNode CreateTerm(Kind kind, unsigned int width,
+ const ASTNode& child0, const ASTNode& child1,
+ const ASTVec &children = _empty_ASTVec)
{
if (!is_Term_kind(kind))
FatalError("CreateTerm: Illegal kind to CreateTerm:", ASTUndefined, kind);
void ClearAllTables(void);
void ClearAllCaches(void);
- int BeforeSAT_ResultCheck(const ASTNode& q);
- int CallSAT_ResultCheck(MINISAT::Solver& newS, const ASTNode& q, const ASTNode& orig_input);
- int SATBased_ArrayReadRefinement(MINISAT::Solver& newS, const ASTNode& q, const ASTNode& orig_input);
- int SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, const ASTNode& orig_input);
+ int BeforeSAT_ResultCheck(const ASTNode& q);
+ int CallSAT_ResultCheck(MINISAT::Solver& newS, const ASTNode& q, const ASTNode& orig_input);
+ int SATBased_ArrayReadRefinement(MINISAT::Solver& newS, const ASTNode& q, const ASTNode& orig_input);
+ int SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, const ASTNode& orig_input);
- int SATBased_FiniteLoop_Refinement(MINISAT::Solver& newS, const ASTNode& orig_input);
- int Expand_FiniteLoop(const ASTNode& finiteloop, ASTNodeMap* ParamToCurrentValMap);
+ int SATBased_FiniteLoop_Refinement(MINISAT::Solver& newS, const ASTNode& orig_input);
+ void Expand_FiniteLoop(const ASTNode& finiteloop, ASTNodeMap* ParamToCurrentValMap);
ASTNode FiniteLoop_Extract_SingleFormula(const ASTNode& finiteloop_formulabody,
ASTNodeMap* VarConstMap);
void CountersAndStats(const char * functionname);
//global function which accepts an integer and looks up the
- //corresponding ASTNode and prints a char* of that ASTNode
+ //corresponding ASTNode and prints a string of that ASTNode
void Convert_MINISATVar_To_ASTNode_Print(int minisat_var,
int decision, int polarity=0);
}; // end namespace.
*/
}
- int BeevMgr::Expand_FiniteLoop(const ASTNode& finiteloop,
+ void BeevMgr::Expand_FiniteLoop(const ASTNode& finiteloop,
ASTNodeMap* ParamToCurrentValMap) {
/*
* 'finiteloop' is the finite loop to be expanded
(*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue);
//Go recursively thru' all the FOR-constructs.
- if(FOR == formulabody.GetKind()) {
- while(paramCurrentValue < paramLimit) {
- Expand_FiniteLoop(formulabody, ParamToCurrentValMap);
- paramCurrentValue = paramCurrentValue + paramIncrement;
+ if(FOR == formulabody.GetKind())
+ {
+ while(paramCurrentValue < paramLimit)
+ {
+ Expand_FiniteLoop(formulabody, ParamToCurrentValMap);
+ paramCurrentValue = paramCurrentValue + paramIncrement;
- //Update ParamToCurrentValMap with parameter and its current
- //value
- //
- //FIXME: Possible leak since I am not freeing the previous
- //'value' for the same 'key'
- (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue);
- } //end of While
- }
- else {
+ //Update ParamToCurrentValMap with parameter and its current
+ //value
+ //
+ //FIXME: Possible leak since I am not freeing the previous
+ //'value' for the same 'key'
+ (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue);
+ } //end of While
+ }
+ else
+ {
//Expand the leaf level FOR-construct completely
for(;
paramCurrentValue < paramLimit;
- paramCurrentValue = paramCurrentValue + paramIncrement) {
- ASTNode currentformula =
+ paramCurrentValue = paramCurrentValue + paramIncrement)
+ {
+ ASTNode currentFormula =
FiniteLoop_Extract_SingleFormula(formulabody, ParamToCurrentValMap);
//Check the currentformula against the model, and add it to the
//SAT solver if it is false against the model
+ ASTNode formulaInModel = ComputeFormulaUsingModel(currentFormula);
+
+ int result = 0;
+ if(ASTFalse == formulaInModel) {
+ //result = CallSAT_ResultCheck(newS, currentFormula, orig_input);
+ }
//Update ParamToCurrentValMap with parameter and its current
//value
//############################################################
- void BeevMgr::PrintClauseList(ostream& os, BeevMgr::ClauseList& cll)
- {
- int num_clauses = cll.size();
- os << "Clauses: " << endl << "=========================================" << endl;
- for (int i = 0; i < num_clauses; i++)
- {
- os << "Clause " << i << endl << "-------------------------------------------" << endl;
- LispPrintVecSpecial(os, *cll[i], 0);
- os << endl << "-------------------------------------------" << endl;
- }
- }
-
void BeevMgr::DeleteClauseList(BeevMgr::ClauseList *cllp)
{
BeevMgr::ClauseList::const_iterator iend = cllp->end();
bvdiv_exception_occured = false;
ASTNode orig_result = ComputeFormulaUsingModel(orig_input);
if (!(ASTTrue == orig_result || ASTFalse == orig_result))
- FatalError("TopLevelSat: Original input must compute to true or false against model");
-
- // if(!arrayread_refinement && !(ASTTrue == orig_result)) {
- // print_counterexample = true;
- // PrintCounterExample(true);
- // FatalError("counterexample bogus : arrayread_refinement is switched off: "
- // "EITHER all LA axioms have not been added OR bitblaster() or ToCNF()"
- // "or satsolver() or counterexamplechecker() have a bug");
- // }
+ FatalError("TopLevelSat: Original input must compute to "\
+ "true or false against model");
// if the counterexample is indeed a good one, then return
// invalid
} //End of PrintCounterExample
-/* iterate through the CounterExampleMap data structure and print it
+ /* iterate through the CounterExampleMap data structure and print it
* to stdout. this function prints only the declared array variables
* IN the ORDER in which they were declared. It also assumes that
* the variables are of the form 'varname_number'. otherwise it will
}
}
} //end of PrintOutput()
+
+
+ void BeevMgr::PrintClauseList(ostream& os, BeevMgr::ClauseList& cll)
+ {
+ int num_clauses = cll.size();
+ os << "Clauses: " << endl << "=========================================" << endl;
+ for (int i = 0; i < num_clauses; i++)
+ {
+ os << "Clause " << i << endl << "-------------------------------------------" << endl;
+ LispPrintVecSpecial(os, *cll[i], 0);
+ os << endl << "-------------------------------------------" << endl;
+ }
+ } //end of PrintClauseList()
+
+ //Variable Order Printer: A global function which converts a MINISAT
+ //var into a ASTNODE var. It then prints this var along with
+ //variable order dcisions taken by MINISAT.
+ void Convert_MINISATVar_To_ASTNode_Print(int minisat_var,
+ int decision_level, int polarity)
+ {
+ BEEV::ASTNode vv = globalBeevMgr_for_parser->_SATVar_to_AST[minisat_var];
+ cout << spaces(decision_level);
+ if (polarity)
+ {
+ cout << "!";
+ }
+ printer::PL_Print(cout,vv, 0);
+ cout << endl;
+ }
+
};//end of namespace BEEV
namespace printer
{
-using std::string;
-using namespace BEEV;
-
-// 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
-// functionality, e.g.,:
-// FatalError("C_Print1: printing not implemented for this kind: ",*this);
-
-// helper function for printing C code (copied from PL_Print1())
-void C_Print1(ostream& os, const ASTNode n, int indentation, bool letize)
-{
-
- unsigned int upper, lower, num_bytes;
- Kind LHSkind, RHSkind;
-
- //os << spaces(indentation);
- //os << endl << spaces(indentation);
- if (!n.IsDefined())
- {
- os << "<undefined>";
- return;
- }
-
- //if this node is present in the letvar Map, then print the letvar
- BeevMgr &bm = n.GetBeevMgr();
-
- //this is to print letvars for shared subterms inside the printing
- //of "(LET v0 = term1, v1=term1@term2,...
- if ((bm.NodeLetVarMap1.find(n) != bm.NodeLetVarMap1.end()) && !letize)
- {
- C_Print1(os, (bm.NodeLetVarMap1[n]), indentation, letize);
- return;
- }
-
- //this is to print letvars for shared subterms inside the actual
- //term to be printed
- if ((bm.NodeLetVarMap.find(n) != bm.NodeLetVarMap.end()) && letize)
- {
- C_Print1(os, (bm.NodeLetVarMap[n]), indentation, letize);
- return;
- }
-
- //otherwise print it normally
- Kind kind = n.GetKind();
- const ASTVec &c = n.GetChildren();
- switch (kind)
- {
- case BVGETBIT:
- FatalError("C_Print1: printing not implemented for this kind: ", n);
- C_Print1(os, c[0], indentation, letize);
- os << "{";
- C_Print1(os, c[1], indentation, letize);
- os << "}";
- break;
- case BITVECTOR:
- FatalError("C_Print1: printing not implemented for this kind: ", n);
- os << "BITVECTOR(";
- unsigned char * str;
- str = CONSTANTBV::BitVector_to_Hex(c[0].GetBVConst());
- os << str << ")";
- CONSTANTBV::BitVector_Dispose(str);
- break;
- case BOOLEAN:
- FatalError("C_Print1: printing not implemented for this kind: ", n);
- os << "BOOLEAN";
- break;
- case FALSE:
- os << "0";
- break;
- case TRUE:
- os << "1";
- break;
- case BVCONST:
- case SYMBOL:
- // print in C friendly format:
- n.nodeprint(os, true);
- break;
- case READ:
- C_Print1(os, c[0], indentation, letize);
- os << "[";
- C_Print1(os, c[1], indentation, letize);
- os << "]";
- break;
- case WRITE:
- os << "(";
- C_Print1(os, c[0], indentation, letize);
- os << " WITH [";
- C_Print1(os, c[1], indentation, letize);
- os << "] := ";
- C_Print1(os, c[2], indentation, letize);
- os << ")";
- os << endl;
- break;
- case BVUMINUS:
- os << kind << "( ";
- C_Print1(os, c[0], indentation, letize);
- os << ")";
- break;
- case NOT:
- os << "!(";
- C_Print1(os, c[0], indentation, letize);
- os << ") " << endl;
- break;
- case BVNEG:
- os << " ~(";
- C_Print1(os, c[0], indentation, letize);
- os << ")";
- break;
- case BVCONCAT:
- FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features
- os << "(";
- C_Print1(os, c[0], indentation, letize);
- os << " @ ";
- C_Print1(os, c[1], indentation, letize);
- os << ")" << endl;
- break;
- case BVOR:
- os << "(";
- C_Print1(os, c[0], indentation, letize);
- os << " | ";
- C_Print1(os, c[1], indentation, letize);
- os << ")";
- break;
- case BVAND:
- os << "(";
- C_Print1(os, c[0], indentation, letize);
- os << " & ";
- C_Print1(os, c[1], indentation, letize);
- os << ")";
- break;
- case BVEXTRACT:
-
- // we only accept indices that are byte-aligned
- // (e.g., [15:8], [23:16])
- // and round down to byte indices rather than bit indices
- upper = GetUnsignedConst(c[1]);
- lower = GetUnsignedConst(c[2]);
- assert(upper > lower);
- assert(lower % 8 == 0);
- assert((upper + 1) % 8 == 0);
- num_bytes = (upper - lower + 1) / 8;
- assert (num_bytes > 0);
-
- // for multi-byte extraction, use the ADDRESS
- if (num_bytes > 1)
- {
- os << "&";
- C_Print1(os, c[0], indentation, letize);
- os << "[" << lower / 8 << "]";
- }
- // for single-byte extraction, use the VALUE
- else
- {
- C_Print1(os, c[0], indentation, letize);
- os << "[" << lower / 8 << "]";
- }
-
- break;
- case BVLEFTSHIFT:
- FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features
- os << "(";
- C_Print1(os, c[0], indentation, letize);
- os << " << ";
- os << GetUnsignedConst(c[1]);
- os << ")";
- break;
- case BVRIGHTSHIFT:
- FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features
- os << "(";
- C_Print1(os, c[0], indentation, letize);
- os << " >> ";
- os << GetUnsignedConst(c[1]);
- os << ")";
- break;
- case BVMULT:
- case BVSUB:
- case BVPLUS:
- case SBVDIV:
- case SBVREM:
- case BVDIV:
- case BVMOD:
- os << kind << "(";
- os << n.GetValueWidth();
- for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++)
- {
- os << ", " << endl;
- C_Print1(os, *it, indentation, letize);
- }
- os << ")" << endl;
- break;
- case ITE:
- os << "if (";
- C_Print1(os, c[0], indentation, letize);
- os << ")" << endl;
- os << "{";
- C_Print1(os, c[1], indentation, letize);
- os << endl << "} else {";
- C_Print1(os, c[2], indentation, letize);
- os << endl << "}";
- break;
- case BVLT:
- // convert to UNSIGNED before doing comparison!
- os << "((unsigned char)";
- C_Print1(os, c[0], indentation, letize);
- os << " < ";
- os << "(unsigned char)";
- C_Print1(os, c[1], indentation, letize);
- os << ")";
- break;
- case BVLE:
- // convert to UNSIGNED before doing comparison!
- os << "((unsigned char)";
- C_Print1(os, c[0], indentation, letize);
- os << " <= ";
- os << "(unsigned char)";
- C_Print1(os, c[1], indentation, letize);
- os << ")";
- break;
- case BVGT:
- // convert to UNSIGNED before doing comparison!
- os << "((unsigned char)";
- C_Print1(os, c[0], indentation, letize);
- os << " > ";
- os << "(unsigned char)";
- C_Print1(os, c[1], indentation, letize);
- os << ")";
- break;
- case BVGE:
- // convert to UNSIGNED before doing comparison!
- os << "((unsigned char)";
- C_Print1(os, c[0], indentation, letize);
- os << " >= ";
- os << "(unsigned char)";
- C_Print1(os, c[1], indentation, letize);
- os << ")";
- break;
- case BVXOR:
- case BVNAND:
- case BVNOR:
- case BVXNOR:
- FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features
- break;
- case BVSLT:
- // convert to SIGNED before doing comparison!
- os << "((signed char)";
- C_Print1(os, c[0], indentation, letize);
- os << " < ";
- os << "(signed char)";
- C_Print1(os, c[1], indentation, letize);
- os << ")";
- break;
- case BVSLE:
- // convert to SIGNED before doing comparison!
- os << "((signed char)";
- C_Print1(os, c[0], indentation, letize);
- os << " <= ";
- os << "(signed char)";
- C_Print1(os, c[1], indentation, letize);
- os << ")";
- break;
- case BVSGT:
- // convert to SIGNED before doing comparison!
- os << "((signed char)";
- C_Print1(os, c[0], indentation, letize);
- os << " > ";
- os << "(signed char)";
- C_Print1(os, c[1], indentation, letize);
- os << ")";
- break;
- case BVSGE:
- // convert to SIGNED before doing comparison!
- os << "((signed char)";
- C_Print1(os, c[0], indentation, letize);
- os << " >= ";
- os << "(signed char)";
- C_Print1(os, c[1], indentation, letize);
- os << ")";
- break;
- case EQ:
- // tricky tricky ... if it's a single-byte comparison,
- // simply do ==, but if it's multi-byte, must do memcmp
- LHSkind = c[0].GetKind();
- RHSkind = c[1].GetKind();
-
- num_bytes = 0;
-
- // try to figure out whether it's a single-byte or multi-byte
- // comparison
- if (LHSkind == BVEXTRACT)
- {
- upper = GetUnsignedConst(c[0].GetChildren()[1]);
- lower = GetUnsignedConst(c[0].GetChildren()[2]);
- num_bytes = (upper - lower + 1) / 8;
- }
- else if (RHSkind == BVEXTRACT)
- {
- upper = GetUnsignedConst(c[1].GetChildren()[1]);
- lower = GetUnsignedConst(c[1].GetChildren()[2]);
- num_bytes = (upper - lower + 1) / 8;
- }
-
- if (num_bytes > 1)
- {
- os << "(memcmp(";
- C_Print1(os, c[0], indentation, letize);
- os << ", ";
- C_Print1(os, c[1], indentation, letize);
- os << ", ";
- os << num_bytes;
- os << ") == 0)";
- }
- else if (num_bytes == 1)
- {
- os << "(";
- C_Print1(os, c[0], indentation, letize);
- os << " == ";
- C_Print1(os, c[1], indentation, letize);
- os << ")";
- }
- else
- {
- FatalError("C_Print1: ugh problem in implementing ==");
- }
-
- break;
- case NEQ:
- C_Print1(os, c[0], indentation, letize);
- os << " != ";
- C_Print1(os, c[1], indentation, letize);
- os << endl;
- break;
- case AND:
- case OR:
- case NAND:
- case NOR:
- case XOR:
- {
- os << "(";
- C_Print1(os, c[0], indentation, letize);
- ASTVec::const_iterator it = c.begin();
- ASTVec::const_iterator itend = c.end();
-
- it++;
- for (; it != itend; it++)
- {
- switch (kind)
- {
- case AND:
- os << " && ";
- break;
- case OR:
- os << " || ";
- break;
- case NAND:
- FatalError("unsupported boolean type in C_Print1");
- break;
- case NOR:
- FatalError("unsupported boolean type in C_Print1");
- break;
- case XOR:
- FatalError("unsupported boolean type in C_Print1");
- break;
- default:
- FatalError("unsupported boolean type in C_Print1");
- }
- C_Print1(os, *it, indentation, letize);
- }
- os << ")";
- break;
- }
- case IFF:
- FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features
- os << "(";
- os << "(";
- C_Print1(os, c[0], indentation, letize);
- os << ")";
- os << " <=> ";
- os << "(";
- C_Print1(os, c[1], indentation, letize);
- os << ")";
- os << ")";
- os << endl;
- break;
- case IMPLIES:
- FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features
- os << "(";
- os << "(";
- C_Print1(os, c[0], indentation, letize);
- os << ")";
- os << " => ";
- os << "(";
- C_Print1(os, c[1], indentation, letize);
- os << ")";
- os << ")";
- os << endl;
- break;
- case BVSX:
- FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features
-
- os << kind << "(";
- C_Print1(os, c[0], indentation, letize);
- os << ",";
- os << n.GetValueWidth();
- os << ")" << endl;
- break;
- default:
- //remember to use LispPrinter here. Otherwise this function will
- //go into an infinite loop. Recall that "<<" is overloaded to
- //the lisp printer. FatalError uses lispprinter
- FatalError("C_Print1: printing not implemented for this kind: ", n);
- break;
- }
-} //end of C_Print1()
-
-
-//two pass algorithm:
-//
-//1. In the first pass, letize this Node, N: i.e. if a node
-//1. appears more than once in N, then record this fact.
-//
-//2. In the second pass print a "global let" and then print N
-//2. as follows: Every occurence of a node occuring more than
-//2. once is replaced with the corresponding let variable.
-ostream& C_Print(ostream &os, const ASTNode n, int indentation)
-{
- // Clear the PrintMap
- BeevMgr& bm = n.GetBeevMgr();
- bm.PLPrintNodeSet.clear();
- bm.NodeLetVarMap.clear();
- bm.NodeLetVarVec.clear();
- bm.NodeLetVarMap1.clear();
-
- //pass 1: letize the node
- n.LetizeNode();
-
- unsigned int lower, upper, num_bytes = 0;
-
- //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();
-
- // start a new block to create new static scope
- os << "{" << endl;
-
- for (; it != itend; it++)
- {
-
- // see if it's a BVEXTRACT, and if so, whether it's multi-byte
- if (it->second.GetKind() == BVEXTRACT)
- {
- upper = GetUnsignedConst(it->second.GetChildren()[1]);
- lower = GetUnsignedConst(it->second.GetChildren()[2]);
- num_bytes = (upper - lower + 1) / 8;
- assert(num_bytes > 0);
- }
-
- //print the let var first
- if (num_bytes > 1)
- {
- // for multi-byte assignment, use 'memcpy' and array notation
- os << "unsigned char ";
- C_Print1(os, it->first, indentation, false);
- os << "[" << num_bytes << "]; ";
- os << "memcpy(";
- C_Print1(os, it->first, indentation, false);
- os << ", ";
- //print the expr
- C_Print1(os, it->second, indentation, false);
- os << ", " << num_bytes << ");";
- }
- else
- {
- // for single-byte assignment, use '='
- os << "unsigned char ";
- C_Print1(os, it->first, indentation, false);
- os << " = ";
- //print the expr
- C_Print1(os, it->second, indentation, false);
- os << ";" << endl;
- }
-
- //update the second map for proper printing of LET
- bm.NodeLetVarMap1[it->second] = it->first;
- }
-
- os << endl << "stp_assert ";
- C_Print1(os, n, indentation, true);
-
- os << ";" << endl << "}";
- }
- else
- {
- os << "stp_assert ";
- C_Print1(os, n, indentation, false);
- os << ";";
- }
- //os << " )";
- //os << " ";
-
- return os;
-} //end of C_Print()
+ using std::string;
+ using namespace BEEV;
+
+ // 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
+ // functionality, e.g.,:
+ // FatalError("C_Print1: printing not implemented for this kind: ",*this);
+
+ // helper function for printing C code (copied from PL_Print1())
+ void C_Print1(ostream& os, const ASTNode n, int indentation, bool letize)
+ {
+
+ unsigned int upper, lower, num_bytes;
+ Kind LHSkind, RHSkind;
+
+ //os << spaces(indentation);
+ //os << endl << spaces(indentation);
+ if (!n.IsDefined())
+ {
+ os << "<undefined>";
+ return;
+ }
+
+ //if this node is present in the letvar Map, then print the letvar
+ BeevMgr &bm = n.GetBeevMgr();
+
+ //this is to print letvars for shared subterms inside the printing
+ //of "(LET v0 = term1, v1=term1@term2,...
+ if ((bm.NodeLetVarMap1.find(n) != bm.NodeLetVarMap1.end()) && !letize)
+ {
+ C_Print1(os, (bm.NodeLetVarMap1[n]), indentation, letize);
+ return;
+ }
+
+ //this is to print letvars for shared subterms inside the actual
+ //term to be printed
+ if ((bm.NodeLetVarMap.find(n) != bm.NodeLetVarMap.end()) && letize)
+ {
+ C_Print1(os, (bm.NodeLetVarMap[n]), indentation, letize);
+ return;
+ }
+
+ //otherwise print it normally
+ Kind kind = n.GetKind();
+ const ASTVec &c = n.GetChildren();
+ switch (kind)
+ {
+ case BVGETBIT:
+ FatalError("C_Print1: printing not implemented for this kind: ", n);
+ C_Print1(os, c[0], indentation, letize);
+ os << "{";
+ C_Print1(os, c[1], indentation, letize);
+ os << "}";
+ break;
+ case BITVECTOR:
+ FatalError("C_Print1: printing not implemented for this kind: ", n);
+ os << "BITVECTOR(";
+ unsigned char * str;
+ str = CONSTANTBV::BitVector_to_Hex(c[0].GetBVConst());
+ os << str << ")";
+ CONSTANTBV::BitVector_Dispose(str);
+ break;
+ case BOOLEAN:
+ FatalError("C_Print1: printing not implemented for this kind: ", n);
+ os << "BOOLEAN";
+ break;
+ case FALSE:
+ os << "0";
+ break;
+ case TRUE:
+ os << "1";
+ break;
+ case BVCONST:
+ case SYMBOL:
+ // print in C friendly format:
+ n.nodeprint(os, true);
+ break;
+ case READ:
+ C_Print1(os, c[0], indentation, letize);
+ os << "[";
+ C_Print1(os, c[1], indentation, letize);
+ os << "]";
+ break;
+ case WRITE:
+ os << "(";
+ C_Print1(os, c[0], indentation, letize);
+ os << " WITH [";
+ C_Print1(os, c[1], indentation, letize);
+ os << "] := ";
+ C_Print1(os, c[2], indentation, letize);
+ os << ")";
+ os << endl;
+ break;
+ case BVUMINUS:
+ os << kind << "( ";
+ C_Print1(os, c[0], indentation, letize);
+ os << ")";
+ break;
+ case NOT:
+ os << "!(";
+ C_Print1(os, c[0], indentation, letize);
+ os << ") " << endl;
+ break;
+ case BVNEG:
+ os << " ~(";
+ C_Print1(os, c[0], indentation, letize);
+ os << ")";
+ break;
+ case BVCONCAT:
+ FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features
+ os << "(";
+ C_Print1(os, c[0], indentation, letize);
+ os << " @ ";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")" << endl;
+ break;
+ case BVOR:
+ os << "(";
+ C_Print1(os, c[0], indentation, letize);
+ os << " | ";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ break;
+ case BVAND:
+ os << "(";
+ C_Print1(os, c[0], indentation, letize);
+ os << " & ";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ break;
+ case BVEXTRACT:
+
+ // we only accept indices that are byte-aligned
+ // (e.g., [15:8], [23:16])
+ // and round down to byte indices rather than bit indices
+ upper = GetUnsignedConst(c[1]);
+ lower = GetUnsignedConst(c[2]);
+ assert(upper > lower);
+ assert(lower % 8 == 0);
+ assert((upper + 1) % 8 == 0);
+ num_bytes = (upper - lower + 1) / 8;
+ assert (num_bytes > 0);
+
+ // for multi-byte extraction, use the ADDRESS
+ if (num_bytes > 1)
+ {
+ os << "&";
+ C_Print1(os, c[0], indentation, letize);
+ os << "[" << lower / 8 << "]";
+ }
+ // for single-byte extraction, use the VALUE
+ else
+ {
+ C_Print1(os, c[0], indentation, letize);
+ os << "[" << lower / 8 << "]";
+ }
+
+ break;
+ case BVLEFTSHIFT:
+ FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features
+ os << "(";
+ C_Print1(os, c[0], indentation, letize);
+ os << " << ";
+ os << GetUnsignedConst(c[1]);
+ os << ")";
+ break;
+ case BVRIGHTSHIFT:
+ FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features
+ os << "(";
+ C_Print1(os, c[0], indentation, letize);
+ os << " >> ";
+ os << GetUnsignedConst(c[1]);
+ os << ")";
+ break;
+ case BVMULT:
+ case BVSUB:
+ case BVPLUS:
+ case SBVDIV:
+ case SBVREM:
+ case BVDIV:
+ case BVMOD:
+ os << kind << "(";
+ os << n.GetValueWidth();
+ for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++)
+ {
+ os << ", " << endl;
+ C_Print1(os, *it, indentation, letize);
+ }
+ os << ")" << endl;
+ break;
+ case ITE:
+ os << "if (";
+ C_Print1(os, c[0], indentation, letize);
+ os << ")" << endl;
+ os << "{";
+ C_Print1(os, c[1], indentation, letize);
+ os << endl << "} else {";
+ C_Print1(os, c[2], indentation, letize);
+ os << endl << "}";
+ break;
+ case BVLT:
+ // convert to UNSIGNED before doing comparison!
+ os << "((unsigned char)";
+ C_Print1(os, c[0], indentation, letize);
+ os << " < ";
+ os << "(unsigned char)";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ break;
+ case BVLE:
+ // convert to UNSIGNED before doing comparison!
+ os << "((unsigned char)";
+ C_Print1(os, c[0], indentation, letize);
+ os << " <= ";
+ os << "(unsigned char)";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ break;
+ case BVGT:
+ // convert to UNSIGNED before doing comparison!
+ os << "((unsigned char)";
+ C_Print1(os, c[0], indentation, letize);
+ os << " > ";
+ os << "(unsigned char)";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ break;
+ case BVGE:
+ // convert to UNSIGNED before doing comparison!
+ os << "((unsigned char)";
+ C_Print1(os, c[0], indentation, letize);
+ os << " >= ";
+ os << "(unsigned char)";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ break;
+ case BVXOR:
+ case BVNAND:
+ case BVNOR:
+ case BVXNOR:
+ FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features
+ break;
+ case BVSLT:
+ // convert to SIGNED before doing comparison!
+ os << "((signed char)";
+ C_Print1(os, c[0], indentation, letize);
+ os << " < ";
+ os << "(signed char)";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ break;
+ case BVSLE:
+ // convert to SIGNED before doing comparison!
+ os << "((signed char)";
+ C_Print1(os, c[0], indentation, letize);
+ os << " <= ";
+ os << "(signed char)";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ break;
+ case BVSGT:
+ // convert to SIGNED before doing comparison!
+ os << "((signed char)";
+ C_Print1(os, c[0], indentation, letize);
+ os << " > ";
+ os << "(signed char)";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ break;
+ case BVSGE:
+ // convert to SIGNED before doing comparison!
+ os << "((signed char)";
+ C_Print1(os, c[0], indentation, letize);
+ os << " >= ";
+ os << "(signed char)";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ break;
+ case EQ:
+ // tricky tricky ... if it's a single-byte comparison,
+ // simply do ==, but if it's multi-byte, must do memcmp
+ LHSkind = c[0].GetKind();
+ RHSkind = c[1].GetKind();
+
+ num_bytes = 0;
+
+ // try to figure out whether it's a single-byte or multi-byte
+ // comparison
+ if (LHSkind == BVEXTRACT)
+ {
+ upper = GetUnsignedConst(c[0].GetChildren()[1]);
+ lower = GetUnsignedConst(c[0].GetChildren()[2]);
+ num_bytes = (upper - lower + 1) / 8;
+ }
+ else if (RHSkind == BVEXTRACT)
+ {
+ upper = GetUnsignedConst(c[1].GetChildren()[1]);
+ lower = GetUnsignedConst(c[1].GetChildren()[2]);
+ num_bytes = (upper - lower + 1) / 8;
+ }
+
+ if (num_bytes > 1)
+ {
+ os << "(memcmp(";
+ C_Print1(os, c[0], indentation, letize);
+ os << ", ";
+ C_Print1(os, c[1], indentation, letize);
+ os << ", ";
+ os << num_bytes;
+ os << ") == 0)";
+ }
+ else if (num_bytes == 1)
+ {
+ os << "(";
+ C_Print1(os, c[0], indentation, letize);
+ os << " == ";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ }
+ else
+ {
+ FatalError("C_Print1: ugh problem in implementing ==");
+ }
+
+ break;
+ case NEQ:
+ C_Print1(os, c[0], indentation, letize);
+ os << " != ";
+ C_Print1(os, c[1], indentation, letize);
+ os << endl;
+ break;
+ case AND:
+ case OR:
+ case NAND:
+ case NOR:
+ case XOR:
+ {
+ os << "(";
+ C_Print1(os, c[0], indentation, letize);
+ ASTVec::const_iterator it = c.begin();
+ ASTVec::const_iterator itend = c.end();
+
+ it++;
+ for (; it != itend; it++)
+ {
+ switch (kind)
+ {
+ case AND:
+ os << " && ";
+ break;
+ case OR:
+ os << " || ";
+ break;
+ case NAND:
+ FatalError("unsupported boolean type in C_Print1");
+ break;
+ case NOR:
+ FatalError("unsupported boolean type in C_Print1");
+ break;
+ case XOR:
+ FatalError("unsupported boolean type in C_Print1");
+ break;
+ default:
+ FatalError("unsupported boolean type in C_Print1");
+ }
+ C_Print1(os, *it, indentation, letize);
+ }
+ os << ")";
+ break;
+ }
+ case IFF:
+ FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features
+ os << "(";
+ os << "(";
+ C_Print1(os, c[0], indentation, letize);
+ os << ")";
+ os << " <=> ";
+ os << "(";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ os << ")";
+ os << endl;
+ break;
+ case IMPLIES:
+ FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features
+ os << "(";
+ os << "(";
+ C_Print1(os, c[0], indentation, letize);
+ os << ")";
+ os << " => ";
+ os << "(";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ os << ")";
+ os << endl;
+ break;
+ case BVSX:
+ FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features
+
+ os << kind << "(";
+ C_Print1(os, c[0], indentation, letize);
+ os << ",";
+ os << n.GetValueWidth();
+ os << ")" << endl;
+ break;
+ default:
+ //remember to use LispPrinter here. Otherwise this function will
+ //go into an infinite loop. Recall that "<<" is overloaded to
+ //the lisp printer. FatalError uses lispprinter
+ FatalError("C_Print1: printing not implemented for this kind: ", n);
+ break;
+ }
+ } //end of C_Print1()
+
+
+ //two pass algorithm:
+ //
+ //1. In the first pass, letize this Node, N: i.e. if a node
+ //1. appears more than once in N, then record this fact.
+ //
+ //2. In the second pass print a "global let" and then print N
+ //2. as follows: Every occurence of a node occuring more than
+ //2. once is replaced with the corresponding let variable.
+ ostream& C_Print(ostream &os, const ASTNode n, int indentation)
+ {
+ // Clear the PrintMap
+ BeevMgr& bm = n.GetBeevMgr();
+ bm.PLPrintNodeSet.clear();
+ bm.NodeLetVarMap.clear();
+ bm.NodeLetVarVec.clear();
+ bm.NodeLetVarMap1.clear();
+
+ //pass 1: letize the node
+ n.LetizeNode();
+
+ unsigned int lower, upper, num_bytes = 0;
+
+ //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();
+
+ // start a new block to create new static scope
+ os << "{" << endl;
+
+ for (; it != itend; it++)
+ {
+
+ // see if it's a BVEXTRACT, and if so, whether it's multi-byte
+ if (it->second.GetKind() == BVEXTRACT)
+ {
+ upper = GetUnsignedConst(it->second.GetChildren()[1]);
+ lower = GetUnsignedConst(it->second.GetChildren()[2]);
+ num_bytes = (upper - lower + 1) / 8;
+ assert(num_bytes > 0);
+ }
+
+ //print the let var first
+ if (num_bytes > 1)
+ {
+ // for multi-byte assignment, use 'memcpy' and array notation
+ os << "unsigned char ";
+ C_Print1(os, it->first, indentation, false);
+ os << "[" << num_bytes << "]; ";
+ os << "memcpy(";
+ C_Print1(os, it->first, indentation, false);
+ os << ", ";
+ //print the expr
+ C_Print1(os, it->second, indentation, false);
+ os << ", " << num_bytes << ");";
+ }
+ else
+ {
+ // for single-byte assignment, use '='
+ os << "unsigned char ";
+ C_Print1(os, it->first, indentation, false);
+ os << " = ";
+ //print the expr
+ C_Print1(os, it->second, indentation, false);
+ os << ";" << endl;
+ }
+
+ //update the second map for proper printing of LET
+ bm.NodeLetVarMap1[it->second] = it->first;
+ }
+
+ os << endl << "stp_assert ";
+ C_Print1(os, n, indentation, true);
+
+ os << ";" << endl << "}";
+ }
+ else
+ {
+ os << "stp_assert ";
+ C_Print1(os, n, indentation, false);
+ os << ";";
+ }
+ //os << " )";
+ //os << " ";
+
+ return os;
+ } //end of C_Print()
}
namespace printer
{
-using std::string;
-using namespace BEEV;
+ using std::string;
+ using namespace BEEV;
-ostream &Lisp_Print_indent(ostream &os, const ASTNode& n,int indentation);
+ ostream &Lisp_Print_indent(ostream &os, const ASTNode& n,int indentation);
-/** Internal function to print in lisp format. Assume newline
- and indentation printed already before first line. Recursive
- calls will have newline & indent, though */
-ostream &Lisp_Print1(ostream &os, const ASTNode& n, int indentation)
-{
- if (!n.IsDefined())
- {
- os << "<undefined>";
- return os;
- }
- Kind kind = n.GetKind();
- // FIXME: figure out how to avoid symbols with same names as kinds.
- // if (kind == READ) {
- // const ASTVec &children = GetChildren();
- // children[0].LispPrint1(os, indentation);
- // os << "[" << children[1] << "]";
- // } else
- if (kind == BVGETBIT)
- {
- const ASTVec &children = n.GetChildren();
- // child 0 is a symbol. Print without the NodeNum.
- os << n.GetNodeNum() << ":";
+ /** Internal function to print in lisp format. Assume newline
+ and indentation printed already before first line. Recursive
+ calls will have newline & indent, though */
+ ostream &Lisp_Print1(ostream &os, const ASTNode& n, int indentation)
+ {
+ if (!n.IsDefined())
+ {
+ os << "<undefined>";
+ return os;
+ }
+ Kind kind = n.GetKind();
+ // FIXME: figure out how to avoid symbols with same names as kinds.
+ // if (kind == READ) {
+ // const ASTVec &children = GetChildren();
+ // children[0].LispPrint1(os, indentation);
+ // os << "[" << children[1] << "]";
+ // } else
+ if (kind == BVGETBIT)
+ {
+ const ASTVec &children = n.GetChildren();
+ // child 0 is a symbol. Print without the NodeNum.
+ os << n.GetNodeNum() << ":";
- children[0].nodeprint(os,true);
- os << "{";
- children[1].nodeprint(os,true);
- os << "}";
- }
- else if (kind == NOT)
- {
- const ASTVec &children = n.GetChildren();
- os << n.GetNodeNum() << ":";
- os << "(NOT ";
- Lisp_Print1(os,children[0], indentation);
- os << ")";
- }
- else if (n.Degree() == 0)
- {
- // Symbol or a kind with no children print as index:NAME if shared,
- // even if they have been printed before.
- os << n.GetNodeNum() << ":";
- n.nodeprint(os,true);
- // os << "(" << _int_node_ptr->_ref_count << ")";
- // os << "{" << GetValueWidth() << "}";
- }
- else if (n.IsAlreadyPrinted())
- {
- // print non-symbols as "[index]" if seen before.
- os << "[" << n.GetNodeNum() << "]";
- // << "(" << _int_node_ptr->_ref_count << ")";
- }
- else
- {
- n.MarkAlreadyPrinted();
- const ASTVec &children = n.GetChildren();
- os << n.GetNodeNum() << ":"
- //<< "(" << _int_node_ptr->_ref_count << ")"
- << "(" << kind << " ";
- // os << "{" << GetValueWidth() << "}";
- ASTVec::const_iterator iend = children.end();
- for (ASTVec::const_iterator i = children.begin(); i != iend; i++)
- {
- Lisp_Print_indent(os, *i, indentation + 2);
- }
- os << ")";
- }
- return os;
-}
+ children[0].nodeprint(os,true);
+ os << "{";
+ children[1].nodeprint(os,true);
+ os << "}";
+ }
+ else if (kind == NOT)
+ {
+ const ASTVec &children = n.GetChildren();
+ os << n.GetNodeNum() << ":";
+ os << "(NOT ";
+ Lisp_Print1(os,children[0], indentation);
+ os << ")";
+ }
+ else if (n.Degree() == 0)
+ {
+ // Symbol or a kind with no children print as index:NAME if shared,
+ // even if they have been printed before.
+ os << n.GetNodeNum() << ":";
+ n.nodeprint(os,true);
+ // os << "(" << _int_node_ptr->_ref_count << ")";
+ // os << "{" << GetValueWidth() << "}";
+ }
+ else if (n.IsAlreadyPrinted())
+ {
+ // print non-symbols as "[index]" if seen before.
+ os << "[" << n.GetNodeNum() << "]";
+ // << "(" << _int_node_ptr->_ref_count << ")";
+ }
+ else
+ {
+ n.MarkAlreadyPrinted();
+ const ASTVec &children = n.GetChildren();
+ os << n.GetNodeNum() << ":"
+ //<< "(" << _int_node_ptr->_ref_count << ")"
+ << "(" << kind << " ";
+ // os << "{" << GetValueWidth() << "}";
+ ASTVec::const_iterator iend = children.end();
+ for (ASTVec::const_iterator i = children.begin(); i != iend; i++)
+ {
+ Lisp_Print_indent(os, *i, indentation + 2);
+ }
+ os << ")";
+ }
+ return os;
+ }
-// Print in lisp format
-ostream &Lisp_Print(ostream &os, const ASTNode& n, int indentation)
-{
- // Clear the PrintMap
- BeevMgr& bm = n.GetBeevMgr();
- bm.AlreadyPrintedSet.clear();
- Lisp_Print_indent(os, n, indentation);
- printf("\n");
- return os;
-}
+ // Print in lisp format
+ ostream &Lisp_Print(ostream &os, const ASTNode& n, int indentation)
+ {
+ // Clear the PrintMap
+ BeevMgr& bm = n.GetBeevMgr();
+ bm.AlreadyPrintedSet.clear();
+ Lisp_Print_indent(os, n, indentation);
+ printf("\n");
+ return os;
+ }
-// Print newline and indentation, then print the thing.
-ostream &Lisp_Print_indent(ostream &os, const ASTNode& n,int indentation)
-{
- os << endl << spaces(indentation);
- Lisp_Print1(os, n, indentation);
- return os;
-}
+ // Print newline and indentation, then print the thing.
+ ostream &Lisp_Print_indent(ostream &os, const ASTNode& n,int indentation)
+ {
+ os << endl << spaces(indentation);
+ Lisp_Print1(os, n, indentation);
+ return os;
+ }
}
namespace printer
{
-using std::string;
-using namespace BEEV;
+ using std::string;
+ using namespace BEEV;
-void PL_Print1(ostream& os, const ASTNode& n,int indentation, bool letize)
-{
- //os << spaces(indentation);
- //os << endl << spaces(indentation);
- if (!n.IsDefined())
- {
- os << "<undefined>";
- return;
- }
+ void PL_Print1(ostream& os, const ASTNode& n,int indentation, bool letize)
+ {
+ //os << spaces(indentation);
+ //os << endl << spaces(indentation);
+ if (!n.IsDefined())
+ {
+ os << "<undefined>";
+ return;
+ }
- //if this node is present in the letvar Map, then print the letvar
- BeevMgr &bm = n.GetBeevMgr();
+ //if this node is present in the letvar Map, then print the letvar
+ BeevMgr &bm = n.GetBeevMgr();
- //this is to print letvars for shared subterms inside the printing
- //of "(LET v0 = term1, v1=term1@term2,...
- if ((bm.NodeLetVarMap1.find(n) != bm.NodeLetVarMap1.end()) && !letize)
- {
- PL_Print1(os, (bm.NodeLetVarMap1[n]), indentation, letize);
- return;
- }
+ //this is to print letvars for shared subterms inside the printing
+ //of "(LET v0 = term1, v1=term1@term2,...
+ if ((bm.NodeLetVarMap1.find(n) != bm.NodeLetVarMap1.end()) && !letize)
+ {
+ PL_Print1(os, (bm.NodeLetVarMap1[n]), indentation, letize);
+ return;
+ }
- //this is to print letvars for shared subterms inside the actual
- //term to be printed
- if ((bm.NodeLetVarMap.find(n) != bm.NodeLetVarMap.end()) && letize)
- {
- PL_Print1(os, (bm.NodeLetVarMap[n]), indentation, letize);
- return;
- }
+ //this is to print letvars for shared subterms inside the actual
+ //term to be printed
+ if ((bm.NodeLetVarMap.find(n) != bm.NodeLetVarMap.end()) && letize)
+ {
+ PL_Print1(os, (bm.NodeLetVarMap[n]), indentation, letize);
+ return;
+ }
- //otherwise print it normally
- Kind kind = n.GetKind();
- const ASTVec &c = n.GetChildren();
- switch (kind)
- {
- case BVGETBIT:
- PL_Print1(os, c[0], indentation, letize);
- os << "{";
- PL_Print1(os, c[1],indentation, letize);
- os << "}";
- break;
- case BITVECTOR:
- os << "BITVECTOR(";
- unsigned char * str;
- str = CONSTANTBV::BitVector_to_Hex(c[0].GetBVConst());
- os << str << ")";
- CONSTANTBV::BitVector_Dispose(str);
- break;
- case BOOLEAN:
- os << "BOOLEAN";
- break;
- case FALSE:
- case TRUE:
- os << kind;
- break;
- case BVCONST:
- case SYMBOL:
- n.nodeprint(os, true);
- break;
- case READ:
- PL_Print1(os, c[0], indentation, letize);
- os << "[";
- PL_Print1(os, c[1], indentation, letize);
- os << "]";
- break;
- case WRITE:
- os << "(";
- PL_Print1(os, c[0], indentation, letize);
- os << " WITH [";
- PL_Print1(os, c[1], indentation, letize);
- os << "] := ";
- PL_Print1(os, c[2], indentation, letize);
- os << ")";
- os << endl;
- break;
- case BVUMINUS:
- os << kind << "( ";
- PL_Print1(os, c[0], indentation, letize);
- os << ")";
- break;
- case NOT:
- os << "NOT(";
- PL_Print1(os, c[0], indentation, letize);
- os << ") " << endl;
- break;
- case BVNEG:
- os << " ~(";
- PL_Print1(os, c[0], indentation, letize);
- os << ")";
- break;
- case BVCONCAT:
- os << "(";
- PL_Print1(os, c[0], indentation, letize);
- os << " @ ";
- PL_Print1(os, c[1], indentation, letize);
- os << ")" << endl;
- break;
- case BVOR:
- os << "(";
- PL_Print1(os, c[0], indentation, letize);
- os << " | ";
- PL_Print1(os, c[1], indentation, letize);
- os << ")";
- break;
- case BVAND:
- os << "(";
- PL_Print1(os, c[0], indentation, letize);
- os << " & ";
- PL_Print1(os, c[1], indentation, letize);
- os << ")";
- break;
- case BVEXTRACT:
- PL_Print1(os, c[0], indentation, letize);
- os << "[";
- os << GetUnsignedConst(c[1]);
- os << ":";
- os << GetUnsignedConst(c[2]);
- os << "]";
- break;
- case BVLEFTSHIFT:
- os << "(";
- PL_Print1(os, c[0], indentation, letize);
- os << " << ";
- os << GetUnsignedConst(c[1]);
- os << ")";
- break;
- case BVRIGHTSHIFT:
- os << "(";
- PL_Print1(os, c[0], indentation, letize);
- os << " >> ";
- os << GetUnsignedConst(c[1]);
- os << ")";
- break;
- case BVMULT:
- case BVSUB:
- case BVPLUS:
- case SBVDIV:
- case SBVREM:
- case BVDIV:
- case BVMOD:
- os << kind << "(";
- os << n.GetValueWidth();
- for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++)
- {
- os << ", " << endl;
- PL_Print1(os, *it, indentation, letize);
- }
- os << ")" << endl;
- break;
- case ITE:
- os << "IF(";
- PL_Print1(os, c[0], indentation, letize);
- os << ")" << endl;
- os << "THEN ";
- PL_Print1(os, c[1], indentation, letize);
- os << endl << "ELSE ";
- PL_Print1(os, c[2], indentation, letize);
- os << endl << "ENDIF";
- break;
- case BVLT:
- case BVLE:
- case BVGT:
- case BVGE:
- case BVXOR:
- case BVNAND:
- case BVNOR:
- case BVXNOR:
- os << kind << "(";
- PL_Print1(os, c[0], indentation, letize);
- os << ",";
- PL_Print1(os, c[1], indentation, letize);
- os << ")" << endl;
- break;
- case BVSLT:
- os << "SBVLT" << "(";
- PL_Print1(os, c[0], indentation, letize);
- os << ",";
- PL_Print1(os, c[1], indentation, letize);
- os << ")" << endl;
- break;
- case BVSLE:
- os << "SBVLE" << "(";
- PL_Print1(os, c[0], indentation, letize);
- os << ",";
- PL_Print1(os, c[1], indentation, letize);
- os << ")" << endl;
- break;
- case BVSGT:
- os << "SBVGT" << "(";
- PL_Print1(os, c[0], indentation, letize);
- os << ",";
- PL_Print1(os, c[1], indentation, letize);
- os << ")" << endl;
- break;
- case BVSGE:
- os << "SBVGE" << "(";
- PL_Print1(os, c[0], indentation, letize);
- os << ",";
- PL_Print1(os, c[1], indentation, letize);
- os << ")" << endl;
- break;
- case EQ:
- PL_Print1(os,c[0], indentation, letize);
- os << " = ";
- PL_Print1(os, c[1], indentation, letize);
- os << endl;
- break;
- case NEQ:
- PL_Print1(os, c[0], indentation, letize);
- os << " /= ";
- PL_Print1(os, c[1], indentation, letize);
- os << endl;
- break;
- case AND:
- case OR:
- case NAND:
- case NOR:
- case XOR:
- {
- os << "(";
- PL_Print1(os, c[0], indentation, letize);
- ASTVec::const_iterator it = c.begin();
- ASTVec::const_iterator itend = c.end();
+ //otherwise print it normally
+ Kind kind = n.GetKind();
+ const ASTVec &c = n.GetChildren();
+ switch (kind)
+ {
+ case BVGETBIT:
+ PL_Print1(os, c[0], indentation, letize);
+ os << "{";
+ PL_Print1(os, c[1],indentation, letize);
+ os << "}";
+ break;
+ case BITVECTOR:
+ os << "BITVECTOR(";
+ unsigned char * str;
+ str = CONSTANTBV::BitVector_to_Hex(c[0].GetBVConst());
+ os << str << ")";
+ CONSTANTBV::BitVector_Dispose(str);
+ break;
+ case BOOLEAN:
+ os << "BOOLEAN";
+ break;
+ case FALSE:
+ case TRUE:
+ os << kind;
+ break;
+ case BVCONST:
+ case SYMBOL:
+ n.nodeprint(os, true);
+ break;
+ case READ:
+ PL_Print1(os, c[0], indentation, letize);
+ os << "[";
+ PL_Print1(os, c[1], indentation, letize);
+ os << "]";
+ break;
+ case WRITE:
+ os << "(";
+ PL_Print1(os, c[0], indentation, letize);
+ os << " WITH [";
+ PL_Print1(os, c[1], indentation, letize);
+ os << "] := ";
+ PL_Print1(os, c[2], indentation, letize);
+ os << ")";
+ os << endl;
+ break;
+ case BVUMINUS:
+ os << kind << "( ";
+ PL_Print1(os, c[0], indentation, letize);
+ os << ")";
+ break;
+ case NOT:
+ os << "NOT(";
+ PL_Print1(os, c[0], indentation, letize);
+ os << ") " << endl;
+ break;
+ case BVNEG:
+ os << " ~(";
+ PL_Print1(os, c[0], indentation, letize);
+ os << ")";
+ break;
+ case BVCONCAT:
+ os << "(";
+ PL_Print1(os, c[0], indentation, letize);
+ os << " @ ";
+ PL_Print1(os, c[1], indentation, letize);
+ os << ")" << endl;
+ break;
+ case BVOR:
+ os << "(";
+ PL_Print1(os, c[0], indentation, letize);
+ os << " | ";
+ PL_Print1(os, c[1], indentation, letize);
+ os << ")";
+ break;
+ case BVAND:
+ os << "(";
+ PL_Print1(os, c[0], indentation, letize);
+ os << " & ";
+ PL_Print1(os, c[1], indentation, letize);
+ os << ")";
+ break;
+ case BVEXTRACT:
+ PL_Print1(os, c[0], indentation, letize);
+ os << "[";
+ os << GetUnsignedConst(c[1]);
+ os << ":";
+ os << GetUnsignedConst(c[2]);
+ os << "]";
+ break;
+ case BVLEFTSHIFT:
+ os << "(";
+ PL_Print1(os, c[0], indentation, letize);
+ os << " << ";
+ os << GetUnsignedConst(c[1]);
+ os << ")";
+ break;
+ case BVRIGHTSHIFT:
+ os << "(";
+ PL_Print1(os, c[0], indentation, letize);
+ os << " >> ";
+ os << GetUnsignedConst(c[1]);
+ os << ")";
+ break;
+ case BVMULT:
+ case BVSUB:
+ case BVPLUS:
+ case SBVDIV:
+ case SBVREM:
+ case BVDIV:
+ case BVMOD:
+ os << kind << "(";
+ os << n.GetValueWidth();
+ for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++)
+ {
+ os << ", " << endl;
+ PL_Print1(os, *it, indentation, letize);
+ }
+ os << ")" << endl;
+ break;
+ case ITE:
+ os << "IF(";
+ PL_Print1(os, c[0], indentation, letize);
+ os << ")" << endl;
+ os << "THEN ";
+ PL_Print1(os, c[1], indentation, letize);
+ os << endl << "ELSE ";
+ PL_Print1(os, c[2], indentation, letize);
+ os << endl << "ENDIF";
+ break;
+ case BVLT:
+ case BVLE:
+ case BVGT:
+ case BVGE:
+ case BVXOR:
+ case BVNAND:
+ case BVNOR:
+ case BVXNOR:
+ os << kind << "(";
+ PL_Print1(os, c[0], indentation, letize);
+ os << ",";
+ PL_Print1(os, c[1], indentation, letize);
+ os << ")" << endl;
+ break;
+ case BVSLT:
+ os << "SBVLT" << "(";
+ PL_Print1(os, c[0], indentation, letize);
+ os << ",";
+ PL_Print1(os, c[1], indentation, letize);
+ os << ")" << endl;
+ break;
+ case BVSLE:
+ os << "SBVLE" << "(";
+ PL_Print1(os, c[0], indentation, letize);
+ os << ",";
+ PL_Print1(os, c[1], indentation, letize);
+ os << ")" << endl;
+ break;
+ case BVSGT:
+ os << "SBVGT" << "(";
+ PL_Print1(os, c[0], indentation, letize);
+ os << ",";
+ PL_Print1(os, c[1], indentation, letize);
+ os << ")" << endl;
+ break;
+ case BVSGE:
+ os << "SBVGE" << "(";
+ PL_Print1(os, c[0], indentation, letize);
+ os << ",";
+ PL_Print1(os, c[1], indentation, letize);
+ os << ")" << endl;
+ break;
+ case EQ:
+ PL_Print1(os,c[0], indentation, letize);
+ os << " = ";
+ PL_Print1(os, c[1], indentation, letize);
+ os << endl;
+ break;
+ case NEQ:
+ PL_Print1(os, c[0], indentation, letize);
+ os << " /= ";
+ PL_Print1(os, c[1], indentation, letize);
+ os << endl;
+ break;
+ case AND:
+ case OR:
+ case NAND:
+ case NOR:
+ case XOR:
+ {
+ os << "(";
+ PL_Print1(os, c[0], indentation, letize);
+ ASTVec::const_iterator it = c.begin();
+ ASTVec::const_iterator itend = c.end();
- it++;
- for (; it != itend; it++)
- {
- os << " " << kind << " ";
- PL_Print1(os, *it, indentation, letize);
- os << endl;
- }
- os << ")";
- break;
- }
- case IFF:
- os << "(";
- os << "(";
- PL_Print1(os, c[0], indentation, letize);
- os << ")";
- os << " <=> ";
- os << "(";
- PL_Print1(os,c[1], indentation, letize);
- os << ")";
- os << ")";
- os << endl;
- break;
- case IMPLIES:
- os << "(";
- os << "(";
- PL_Print1(os, c[0], indentation, letize);
- os << ")";
- os << " => ";
- os << "(";
- PL_Print1(os, c[1], indentation, letize);
- os << ")";
- os << ")";
- os << endl;
- break;
- case BVSX:
- case BVZX:
- os << kind << "(";
- PL_Print1(os, c[0], indentation, letize);
- os << ",";
- os << n.GetValueWidth();
- os << ")" << endl;
- break;
- default:
- //remember to use LispPrinter here. Otherwise this function will
- //go into an infinite loop. Recall that "<<" is overloaded to
- //the lisp printer. FatalError uses lispprinter
- FatalError("PL_Print1: printing not implemented for this kind: ", n);
- break;
- }
-} //end of PL_Print1()
+ it++;
+ for (; it != itend; it++)
+ {
+ os << " " << kind << " ";
+ PL_Print1(os, *it, indentation, letize);
+ os << endl;
+ }
+ os << ")";
+ break;
+ }
+ case IFF:
+ os << "(";
+ os << "(";
+ PL_Print1(os, c[0], indentation, letize);
+ os << ")";
+ os << " <=> ";
+ os << "(";
+ PL_Print1(os,c[1], indentation, letize);
+ os << ")";
+ os << ")";
+ os << endl;
+ break;
+ case IMPLIES:
+ os << "(";
+ os << "(";
+ PL_Print1(os, c[0], indentation, letize);
+ os << ")";
+ os << " => ";
+ os << "(";
+ PL_Print1(os, c[1], indentation, letize);
+ os << ")";
+ os << ")";
+ os << endl;
+ break;
+ case BVSX:
+ case BVZX:
+ os << kind << "(";
+ PL_Print1(os, c[0], indentation, letize);
+ os << ",";
+ os << n.GetValueWidth();
+ os << ")" << endl;
+ break;
+ default:
+ //remember to use LispPrinter here. Otherwise this function will
+ //go into an infinite loop. Recall that "<<" is overloaded to
+ //the lisp printer. FatalError uses lispprinter
+ FatalError("PL_Print1: printing not implemented for this kind: ", n);
+ break;
+ }
+ } //end of PL_Print1()
-//print in PRESENTATION LANGUAGE
-//
-//two pass algorithm:
-//
-//1. In the first pass, letize this Node, N: i.e. if a node
-//1. appears more than once in N, then record this fact.
-//
-//2. In the second pass print a "global let" and then print N
-//2. as follows: Every occurence of a node occuring more than
-//2. once is replaced with the corresponding let variable.
-ostream& PL_Print(ostream &os, const ASTNode& n, int indentation)
-{
- // Clear the PrintMap
- BeevMgr& bm = n.GetBeevMgr();
- bm.PLPrintNodeSet.clear();
- bm.NodeLetVarMap.clear();
- bm.NodeLetVarVec.clear();
- bm.NodeLetVarMap1.clear();
+ //print in PRESENTATION LANGUAGE
+ //
+ //two pass algorithm:
+ //
+ //1. In the first pass, letize this Node, N: i.e. if a node
+ //1. appears more than once in N, then record this fact.
+ //
+ //2. In the second pass print a "global let" and then print N
+ //2. as follows: Every occurence of a node occuring more than
+ //2. once is replaced with the corresponding let variable.
+ ostream& PL_Print(ostream &os, const ASTNode& n, int indentation)
+ {
+ // Clear the PrintMap
+ BeevMgr& bm = n.GetBeevMgr();
+ bm.PLPrintNodeSet.clear();
+ bm.NodeLetVarMap.clear();
+ bm.NodeLetVarVec.clear();
+ bm.NodeLetVarMap1.clear();
- //pass 1: letize the node
- n.LetizeNode();
+ //pass 1: letize the node
+ n.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();
+ //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
- PL_Print1(os, it->first, indentation, false);
- os << " = ";
- //print the expr
- PL_Print1(os, it->second, indentation, false);
+ os << "(LET ";
+ //print the let var first
+ PL_Print1(os, it->first, indentation, false);
+ os << " = ";
+ //print the expr
+ PL_Print1(os, it->second, indentation, false);
- //update the second map for proper printing of LET
- bm.NodeLetVarMap1[it->second] = it->first;
+ //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
- PL_Print1(os, it->first, indentation, false);
- os << " = ";
- //print the expr
- PL_Print1(os, it->second, indentation, false);
+ for (it++; it != itend; it++)
+ {
+ os << "," << endl;
+ //print the let var first
+ PL_Print1(os, it->first, indentation, false);
+ os << " = ";
+ //print the expr
+ PL_Print1(os, it->second, indentation, false);
- //update the second map for proper printing of LET
- bm.NodeLetVarMap1[it->second] = it->first;
- }
+ //update the second map for proper printing of LET
+ bm.NodeLetVarMap1[it->second] = it->first;
+ }
- os << " IN " << endl;
- PL_Print1(os, n, indentation, true);
- os << ") ";
- }
- else
- PL_Print1(os,n, indentation, false);
- //os << " )";
- os << " ";
- return os;
-} //end of PL_Print()
+ os << " IN " << endl;
+ PL_Print1(os, n, indentation, true);
+ os << ") ";
+ }
+ else
+ PL_Print1(os,n, indentation, false);
+ //os << " )";
+ os << " ";
+ return os;
+ } //end of PL_Print()
}
namespace printer
{
-using std::string;
-using namespace BEEV;
+ using std::string;
+ using namespace BEEV;
-string functionToSMTLIBName(const BEEV::Kind k);
-void SMTLIB_Print1(ostream& os, const BEEV::ASTNode n, int indentation, bool letize);
+ string functionToSMTLIBName(const BEEV::Kind k);
+ void SMTLIB_Print1(ostream& os, const BEEV::ASTNode n, int indentation, bool letize);
-void outputBitVec(const ASTNode n, ostream& os)
-{
- Kind k = n.GetKind();
- const ASTVec &c = n.GetChildren();
- ASTNode op;
+ void outputBitVec(const ASTNode n, ostream& os)
+ {
+ Kind k = n.GetKind();
+ const ASTVec &c = n.GetChildren();
+ ASTNode op;
- if (BITVECTOR == k)
- {
- op = c[0];
- }
- else if (BVCONST == k)
- {
- op = n;
- }
- else
- FatalError("nsadfsdaf");
+ if (BITVECTOR == k)
+ {
+ op = c[0];
+ }
+ else if (BVCONST == k)
+ {
+ op = n;
+ }
+ else
+ FatalError("nsadfsdaf");
- // CONSTANTBV::BitVector_to_Dec returns a signed representation by default.
- // Prepend with zero to convert to unsigned.
+ // CONSTANTBV::BitVector_to_Dec returns a signed representation by default.
+ // Prepend with zero to convert to unsigned.
- os << "bv";
- CBV unsign = CONSTANTBV::BitVector_Concat(n.GetBeevMgr().CreateZeroConst(1).GetBVConst(), op.GetBVConst());
- unsigned char * str = CONSTANTBV::BitVector_to_Dec(unsign);
- CONSTANTBV::BitVector_Destroy(unsign);
- os << str << "[" << op.GetValueWidth() << "]";
- CONSTANTBV::BitVector_Dispose(str);
-}
+ os << "bv";
+ CBV unsign = CONSTANTBV::BitVector_Concat(n.GetBeevMgr().CreateZeroConst(1).GetBVConst(), op.GetBVConst());
+ unsigned char * str = CONSTANTBV::BitVector_to_Dec(unsign);
+ CONSTANTBV::BitVector_Destroy(unsign);
+ os << str << "[" << op.GetValueWidth() << "]";
+ CONSTANTBV::BitVector_Dispose(str);
+ }
-void SMTLIB_Print1(ostream& os, const ASTNode n, int indentation, bool letize)
-{
- //os << spaces(indentation);
- //os << endl << spaces(indentation);
- if (!n.IsDefined())
- {
- os << "<undefined>";
- return;
- }
+ void SMTLIB_Print1(ostream& os, const ASTNode n, int indentation, bool letize)
+ {
+ //os << spaces(indentation);
+ //os << endl << spaces(indentation);
+ if (!n.IsDefined())
+ {
+ os << "<undefined>";
+ return;
+ }
- //if this node is present in the letvar Map, then print the letvar
- BeevMgr &bm = n.GetBeevMgr();
+ //if this node is present in the letvar Map, then print the letvar
+ BeevMgr &bm = n.GetBeevMgr();
- //this is to print letvars for shared subterms inside the printing
- //of "(LET v0 = term1, v1=term1@term2,...
- if ((bm.NodeLetVarMap1.find(n) != bm.NodeLetVarMap1.end()) && !letize)
- {
- SMTLIB_Print1(os, (bm.NodeLetVarMap1[n]), indentation, letize);
- return;
- }
+ //this is to print letvars for shared subterms inside the printing
+ //of "(LET v0 = term1, v1=term1@term2,...
+ if ((bm.NodeLetVarMap1.find(n) != bm.NodeLetVarMap1.end()) && !letize)
+ {
+ SMTLIB_Print1(os, (bm.NodeLetVarMap1[n]), indentation, letize);
+ return;
+ }
- //this is to print letvars for shared subterms inside the actual
- //term to be printed
- if ((bm.NodeLetVarMap.find(n) != bm.NodeLetVarMap.end()) && letize)
- {
- SMTLIB_Print1(os, (bm.NodeLetVarMap[n]), indentation, letize);
- return;
- }
+ //this is to print letvars for shared subterms inside the actual
+ //term to be printed
+ if ((bm.NodeLetVarMap.find(n) != bm.NodeLetVarMap.end()) && letize)
+ {
+ SMTLIB_Print1(os, (bm.NodeLetVarMap[n]), indentation, letize);
+ return;
+ }
- //otherwise print it normally
- Kind kind = n.GetKind();
- const ASTVec &c = n.GetChildren();
- switch (kind)
- {
- case BITVECTOR:
- case BVCONST:
- outputBitVec(n, os);
- break;
+ //otherwise print it normally
+ Kind kind = n.GetKind();
+ const ASTVec &c = n.GetChildren();
+ switch (kind)
+ {
+ case BITVECTOR:
+ case BVCONST:
+ outputBitVec(n, os);
+ break;
- case SYMBOL:
- n.nodeprint(os);
- break;
- case FALSE:
- os << "false";
- break;
- case TRUE:
- os << "true";
- break;
+ case SYMBOL:
+ n.nodeprint(os);
+ break;
+ case FALSE:
+ os << "false";
+ break;
+ case TRUE:
+ os << "true";
+ break;
- case BVSX:
- case BVZX:
- {
- unsigned int amount = GetUnsignedConst(c[1]);
- if (BVZX == kind)
- os << "(zero_extend[";
- else
- os << "(sign_extend[";
+ case BVSX:
+ case BVZX:
+ {
+ unsigned int amount = GetUnsignedConst(c[1]);
+ if (BVZX == kind)
+ os << "(zero_extend[";
+ else
+ os << "(sign_extend[";
- os << amount << "]";
- SMTLIB_Print1(os, c[0], indentation, letize);
- os << ")";
- }
- break;
- case BVEXTRACT:
- {
- unsigned int upper = GetUnsignedConst(c[1]);
- unsigned int lower = GetUnsignedConst(c[2]);
- assert(upper >= lower);
- os << "(extract[" << upper << ":" << lower << "] ";
- SMTLIB_Print1(os, c[0], indentation, letize);
- os << ")";
- }
- break;
- default:
- {
- os << "(" << functionToSMTLIBName(kind);
+ os << amount << "]";
+ SMTLIB_Print1(os, c[0], indentation, letize);
+ os << ")";
+ }
+ break;
+ case BVEXTRACT:
+ {
+ unsigned int upper = GetUnsignedConst(c[1]);
+ unsigned int lower = GetUnsignedConst(c[2]);
+ assert(upper >= lower);
+ os << "(extract[" << upper << ":" << lower << "] ";
+ SMTLIB_Print1(os, c[0], indentation, letize);
+ os << ")";
+ }
+ break;
+ default:
+ {
+ os << "(" << functionToSMTLIBName(kind);
- ASTVec::const_iterator iend = c.end();
- for (ASTVec::const_iterator i = c.begin(); i != iend; i++)
- {
- os << " ";
- SMTLIB_Print1(os, *i, 0, letize);
- }
+ ASTVec::const_iterator iend = c.end();
+ for (ASTVec::const_iterator i = c.begin(); i != iend; i++)
+ {
+ os << " ";
+ SMTLIB_Print1(os, *i, 0, letize);
+ }
- os << ")";
- }
- }
-}
+ os << ")";
+ }
+ }
+ }
-// copied from Presentation Langauge printer.
-ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation)
-{
- // Clear the PrintMap
- BeevMgr& bm = n.GetBeevMgr();
- bm.PLPrintNodeSet.clear();
- bm.NodeLetVarMap.clear();
- bm.NodeLetVarVec.clear();
- bm.NodeLetVarMap1.clear();
+ // copied from Presentation Langauge printer.
+ ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation)
+ {
+ // Clear the PrintMap
+ BeevMgr& bm = n.GetBeevMgr();
+ bm.PLPrintNodeSet.clear();
+ bm.NodeLetVarMap.clear();
+ bm.NodeLetVarVec.clear();
+ bm.NodeLetVarMap1.clear();
- //pass 1: letize the node
- n.LetizeNode();
+ //pass 1: letize the node
+ n.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();
+ //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
- SMTLIB_Print1(os, it->first, indentation, false);
- os << " = ";
- //print the expr
- SMTLIB_Print1(os, it->second, indentation, false);
+ os << "(LET ";
+ //print the let var first
+ SMTLIB_Print1(os, it->first, indentation, false);
+ os << " = ";
+ //print the expr
+ SMTLIB_Print1(os, it->second, indentation, false);
- //update the second map for proper printing of LET
- bm.NodeLetVarMap1[it->second] = it->first;
+ //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
- SMTLIB_Print1(os, it->first, indentation, false);
- os << " = ";
- //print the expr
- SMTLIB_Print1(os, it->second, indentation, false);
+ for (it++; it != itend; it++)
+ {
+ os << "," << endl;
+ //print the let var first
+ SMTLIB_Print1(os, it->first, indentation, false);
+ os << " = ";
+ //print the expr
+ SMTLIB_Print1(os, it->second, indentation, false);
- //update the second map for proper printing of LET
- bm.NodeLetVarMap1[it->second] = it->first;
- }
+ //update the second map for proper printing of LET
+ bm.NodeLetVarMap1[it->second] = it->first;
+ }
- os << " IN " << endl;
- SMTLIB_Print1(os, n, indentation, true);
- os << ") ";
- }
- else
- SMTLIB_Print1(os, n, indentation, false);
+ os << " IN " << endl;
+ SMTLIB_Print1(os, n, indentation, true);
+ os << ") ";
+ }
+ else
+ SMTLIB_Print1(os, n, indentation, false);
- os << endl;
- return os;
-}
+ os << endl;
+ return os;
+ }
-string functionToSMTLIBName(const Kind k)
-{
- switch (k)
- {
- case AND:
- case BVAND:
- case BVNAND:
- case BVNOR:
- case BVOR:
- case BVSGE:
- case BVSGT:
- case BVSLE:
- case BVSLT:
- case BVSUB:
- case BVXOR:
- case ITE:
- case NAND:
- case NOR:
- case NOT:
- case OR:
- case XOR:
- case IFF:
- return _kind_names[k];
+ string functionToSMTLIBName(const Kind k)
+ {
+ switch (k)
+ {
+ case AND:
+ case BVAND:
+ case BVNAND:
+ case BVNOR:
+ case BVOR:
+ case BVSGE:
+ case BVSGT:
+ case BVSLE:
+ case BVSLT:
+ case BVSUB:
+ case BVXOR:
+ case ITE:
+ case NAND:
+ case NOR:
+ case NOT:
+ case OR:
+ case XOR:
+ case IFF:
+ return _kind_names[k];
- case BVCONCAT:
- return "concat";
- case BVDIV:
- return "bvudiv";
- case BVGT:
- return "bvugt";
- case BVGE:
- return "bvuge";
- case BVLE:
- return "bvule";
- case BVLEFTSHIFT:
- return "bvshl";
- case BVLT:
- return "bvult";
- case BVMOD:
- return "bvurem";
- case BVMULT:
- return "bvmul";
- case BVNEG:
- return "bvnot"; // CONFUSSSSINNG. (1/2)
- case BVPLUS:
- return "bvadd";
- case BVRIGHTSHIFT:
- return "bvlshr"; // logical
- case BVSRSHIFT:
- return "bvashr"; // arithmetic.
- case BVUMINUS:
- return "bvneg"; // CONFUSSSSINNG. (2/2)
- case EQ:
- return "=";
- case READ:
- return "select";
- case WRITE:
- return "store";
- case SBVDIV:
- return "bvsdiv";
- case SBVREM:
- return "bvsrem";
+ case BVCONCAT:
+ return "concat";
+ case BVDIV:
+ return "bvudiv";
+ case BVGT:
+ return "bvugt";
+ case BVGE:
+ return "bvuge";
+ case BVLE:
+ return "bvule";
+ case BVLEFTSHIFT:
+ return "bvshl";
+ case BVLT:
+ return "bvult";
+ case BVMOD:
+ return "bvurem";
+ case BVMULT:
+ return "bvmul";
+ case BVNEG:
+ return "bvnot"; // CONFUSSSSINNG. (1/2)
+ case BVPLUS:
+ return "bvadd";
+ case BVRIGHTSHIFT:
+ return "bvlshr"; // logical
+ case BVSRSHIFT:
+ return "bvashr"; // arithmetic.
+ case BVUMINUS:
+ return "bvneg"; // CONFUSSSSINNG. (2/2)
+ case EQ:
+ return "=";
+ case READ:
+ return "select";
+ case WRITE:
+ return "store";
+ case SBVDIV:
+ return "bvsdiv";
+ case SBVREM:
+ return "bvsrem";
- default:
- {
- cerr << "Unknown name when outputting:";
- FatalError(_kind_names[k]);
- return ""; // to quieten compiler/
- }
- }
-}
+ default:
+ {
+ cerr << "Unknown name when outputting:";
+ FatalError(_kind_names[k]);
+ return ""; // to quieten compiler/
+ }
+ }
+ }
}
namespace printer
{
-using std::string;
-using namespace BEEV;
+ using std::string;
+ using namespace BEEV;
-void outputBitVec(const ASTNode n, ostream& os);
+ void outputBitVec(const ASTNode n, ostream& os);
-void Dot_Print1(ostream &os, const ASTNode n, hash_set<int> *alreadyOutput)
-{
+ void Dot_Print1(ostream &os, const ASTNode n, hash_set<int> *alreadyOutput)
+ {
- // check if this node has already been printed. If so return.
- if (alreadyOutput->find(n.GetNodeNum()) != alreadyOutput->end())
- return;
-
- alreadyOutput->insert(n.GetNodeNum());
-
- os << "n" << n.GetNodeNum() << "[label =\"";
- switch (n.GetKind())
- {
- case SYMBOL:
- n.nodeprint(os);
- break;
-
- case BITVECTOR:
- case BVCONST:
- outputBitVec(n, os);
- break;
-
- default:
- os << _kind_names[n.GetKind()];
- }
-
- os << "\"];" << endl;
-
- // print the edges to each child.
- ASTVec ch = n.GetChildren();
- ASTVec::iterator itend = ch.end();
- int i = 0;
- for (ASTVec::iterator it = ch.begin(); it < itend; it++)
- {
- os << "n" << n.GetNodeNum() << " -> " << "n" << it->GetNodeNum() << "[label=" << i++ << "];" << endl;
- }
-
- // print each of the children.
- for (ASTVec::iterator it = ch.begin(); it < itend; it++)
- {
- Dot_Print1(os, *it, alreadyOutput);
- }
-}
+ // check if this node has already been printed. If so return.
+ if (alreadyOutput->find(n.GetNodeNum()) != alreadyOutput->end())
+ return;
-ostream& Dot_Print(ostream &os, const ASTNode n)
-{
+ alreadyOutput->insert(n.GetNodeNum());
- os << "digraph G{" << endl;
+ os << "n" << n.GetNodeNum() << "[label =\"";
+ switch (n.GetKind())
+ {
+ case SYMBOL:
+ n.nodeprint(os);
+ break;
- // create hashmap to hold integers (node numbers).
- hash_set<int> alreadyOutput;
+ case BITVECTOR:
+ case BVCONST:
+ outputBitVec(n, os);
+ break;
- Dot_Print1(os, n, &alreadyOutput);
+ default:
+ os << _kind_names[n.GetKind()];
+ }
- os << "}" << endl;
+ os << "\"];" << endl;
- return os;
-}
+ // print the edges to each child.
+ ASTVec ch = n.GetChildren();
+ ASTVec::iterator itend = ch.end();
+ int i = 0;
+ for (ASTVec::iterator it = ch.begin(); it < itend; it++)
+ {
+ os << "n" << n.GetNodeNum() << " -> " << "n" << it->GetNodeNum() << "[label=" << i++ << "];" << endl;
+ }
+
+ // print each of the children.
+ for (ASTVec::iterator it = ch.begin(); it < itend; it++)
+ {
+ Dot_Print1(os, *it, alreadyOutput);
+ }
+ }
+
+ ostream& Dot_Print(ostream &os, const ASTNode n)
+ {
+
+ os << "digraph G{" << endl;
+
+ // create hashmap to hold integers (node numbers).
+ hash_set<int> alreadyOutput;
+
+ Dot_Print1(os, n, &alreadyOutput);
+
+ os << "}" << endl;
+
+ return os;
+ }
}
namespace printer
{
-ostream& Dot_Print(ostream &os, const BEEV::ASTNode n);
+ ostream& Dot_Print(ostream &os, const BEEV::ASTNode n);
-ostream& SMTLIB_Print(ostream &os, const BEEV::ASTNode n, const int indentation = 0);
-ostream& C_Print(ostream &os, const BEEV::ASTNode n, const int indentation = 0);
-ostream& PL_Print(ostream &os, const BEEV::ASTNode& n, int indentation=0);
+ ostream& SMTLIB_Print(ostream &os, const BEEV::ASTNode n, const int indentation = 0);
+ ostream& C_Print(ostream &os, const BEEV::ASTNode n, const int indentation = 0);
+ ostream& PL_Print(ostream &os, const BEEV::ASTNode& n, int indentation=0);
-ostream& Lisp_Print(ostream &os, const BEEV::ASTNode& n, int indentation=0);
-ostream& Lisp_Print_indent(ostream &os, const BEEV::ASTNode& n,int indentation=0);
+ ostream& Lisp_Print(ostream &os, const BEEV::ASTNode& n, int indentation=0);
+ ostream& Lisp_Print_indent(ostream &os, const BEEV::ASTNode& n,int indentation=0);
}
projects / francis / stp.git / commitdiff