#include <assert.h>
#include "printer/printers.h"
+#include "printer/AssortedPrinters.h"
namespace BEEV
{
return os;
}
- // FIXME: Made non-ref in the hope that it would work better.
- void lp(ASTNode node)
- {
- cout << lisp(node) << endl;
- }
-
- void lpvec(const ASTVec &vec)
- {
- vec[0].GetBeevMgr().AlreadyPrintedSet.clear();
- LispPrintVec(cout, vec, 0);
- cout << endl;
- }
-
// Copy constructor. Maintain _ref_count
ASTNode::ASTNode(const ASTNode &n) :
_int_node_ptr(n._int_node_ptr)
cout << NodeSize(a) << endl << endl;
}
- ostream &ASTNode::LispPrint(ostream &os, int indentation) const
- {
- printer::Lisp_Print(os, *this, indentation);
- }
-
- ostream &ASTNode::LispPrint_indent(ostream &os, int indentation) const
- {
- printer::Lisp_Print_indent(os, *this, indentation);
- }
-
- ostream& ASTNode::PL_Print(ostream &os, int indentation) const
- {
- printer::PL_Print(os, *this, indentation);
- }
-
unsigned int BeevMgr::NodeSize(const ASTNode& a, bool clearStatInfo)
{
if (clearStatInfo)
//Vector of ASTNodes, used for child nodes among other things.
typedef vector<ASTNode> ASTVec;
+ typedef unsigned int * CBV;
extern ASTVec _empty_ASTVec;
extern BeevMgr * globalBeevMgr_for_parser;
- typedef unsigned int * CBV;
-
/***************************************************************************/
/* Class ASTNode: Smart pointer to actual ASTNode internal datastructure. */
/***************************************************************************/
//FIXME: move to a more appropriate place
extern ASTNodeSet _parser_symbol_table;
- /***************************************************************************
- Class LispPrinter: iomanipulator for printing ASTNode or ASTVec
- ***************************************************************************/
- class LispPrinter
- {
-
- public:
- ASTNode _node;
-
- // number of spaces to print before first real character of
- // object.
- int _indentation;
-
- // FIXME: pass ASTNode by reference
- // Constructor to build the LispPrinter object
- LispPrinter(ASTNode node, int indentation) :
- _node(node), _indentation(indentation)
- {
- }
-
- friend ostream &operator<<(ostream &os, const LispPrinter &lp)
- {
- return lp._node.LispPrint(os, lp._indentation);
- }
- ;
-
- }; //End of ListPrinter
-
- //This is the IO manipulator. It builds an object of class
- //"LispPrinter" that has a special overloaded "<<" operator.
- inline LispPrinter lisp(const ASTNode &node, int indentation = 0)
- {
- LispPrinter lp(node, indentation);
- return lp;
- }
-
- /***************************************************************************/
- /* Class LispVecPrinter:iomanipulator for printing vector of ASTNodes */
- /***************************************************************************/
- class LispVecPrinter
- {
-
- public:
- const ASTVec * _vec;
- // number of spaces to print before first real
- // character of object.
- int _indentation;
-
- // Constructor to build the LispPrinter object
- LispVecPrinter(const ASTVec &vec, int indentation)
- {
- _vec = &vec;
- _indentation = indentation;
- }
-
- friend ostream &operator<<(ostream &os, const LispVecPrinter &lvp)
- {
- LispPrintVec(os, *lvp._vec, lvp._indentation);
- return os;
- }
- ;
- }; //End of Class ListVecPrinter
-
- //iomanipulator. builds an object of class "LisPrinter" that has a
- //special overloaded "<<" operator.
- inline LispVecPrinter lisp(const ASTVec &vec, int indentation = 0)
- {
- LispVecPrinter lvp(vec, indentation);
- return lvp;
- }
-
/***************************************************************************
* Class BeevMgr. This holds all "global" variables for the system, such as
* unique tables for the various kinds of nodes.
}
return (unsigned int) *((unsigned int *) n.GetBVConst());
} //end of GetUnsignedConst
-
}; // end namespace BEEV
#endif
//are no more axioms to add
//
//for each array, fetch its list of indices seen so far
- for (ASTNodeToVecMap::iterator iset = _arrayname_readindices.begin(), iset_end = _arrayname_readindices.end(); iset != iset_end; iset++)
+ for (ASTNodeToVecMap::iterator iset = _arrayname_readindices.begin(),
+ iset_end = _arrayname_readindices.end(); iset != iset_end; iset++)
{
ASTVec listOfIndices = iset->second;
//loop over the list of indices for the array and create LA, and add to q
- for (ASTVec::iterator it = listOfIndices.begin(), itend = listOfIndices.end(); it != itend; it++)
+ for (ASTVec::iterator it = listOfIndices.begin(),
+ itend = listOfIndices.end(); it != itend; it++)
{
if (BVCONST == it->GetKind())
{
//we have nonconst index here. create Leibnitz axiom for it
//w.r.t every index in listOfIndices
- for (ASTVec::iterator it1 = listOfIndices.begin(), itend1 = listOfIndices.end(); it1 != itend1; it1++)
+ for (ASTVec::iterator it1 = listOfIndices.begin(),
+ itend1 = listOfIndices.end(); it1 != itend1; it1++)
{
ASTNode compare_index = *it1;
//do not compare with yourself
//prepare for SAT LOOP
//first construct the antecedent for the LA axiom
- ASTNode eqOfIndices = (exprless(the_index, compare_index)) ? CreateSimplifiedEQ(the_index, compare_index) : CreateSimplifiedEQ(
- compare_index, the_index);
+ ASTNode eqOfIndices =
+ (exprless(the_index, compare_index)) ?
+ CreateSimplifiedEQ(the_index, compare_index) : CreateSimplifiedEQ(compare_index, the_index);
ASTNode arr_read2 = CreateTerm(READ, ArrName.GetValueWidth(), ArrName, compare_index);
//get the variable corresponding to the array_read2
//RemainingAxioms = CreateNode(AND,RemainingAxioms,LeibnitzAxiom);
RemainingAxiomsVec.push_back(LeibnitzAxiom);
}
- ASTNode FalseAxioms = (FalseAxiomsVec.size() > 1) ? CreateNode(AND, FalseAxiomsVec) : FalseAxiomsVec[0];
+ ASTNode FalseAxioms =
+ (FalseAxiomsVec.size() > 1) ?
+ CreateNode(AND, FalseAxiomsVec) : FalseAxiomsVec[0];
ASTNodeStats("adding false readaxioms to SAT: ", FalseAxioms);
//printf("spot 01\n");
int res2 = 2;
}
}
}
- ASTNode RemainingAxioms = (RemainingAxiomsVec.size() > 1) ? CreateNode(AND, RemainingAxiomsVec) : RemainingAxiomsVec[0];
+ ASTNode RemainingAxioms =
+ (RemainingAxiomsVec.size() > 1) ?
+ CreateNode(AND, RemainingAxiomsVec) : RemainingAxiomsVec[0];
ASTNodeStats("adding remaining readaxioms to SAT: ", RemainingAxioms);
return CallSAT_ResultCheck(newS, RemainingAxioms, orig_input);
} //end of SATBased_ArrayReadRefinement
}
}
- writeAxiom = (FalseAxioms.size() != 1) ? CreateNode(AND, FalseAxioms) : FalseAxioms[0];
+ writeAxiom =
+ (FalseAxioms.size() != 1) ?
+ CreateNode(AND, FalseAxioms) : FalseAxioms[0];
ASTNodeStats("adding false writeaxiom to SAT: ", writeAxiom);
int res2 = 2;
if (FalseAxioms.size() > oldFalseAxiomsSize)
return res2;
}
- writeAxiom = (RemainingAxioms.size() != 1) ? CreateNode(AND, RemainingAxioms) : RemainingAxioms[0];
+ writeAxiom =
+ (RemainingAxioms.size() != 1) ?
+ CreateNode(AND, RemainingAxioms) : RemainingAxioms[0];
ASTNodeStats("adding remaining writeaxiom to SAT: ", writeAxiom);
res2 = CallSAT_ResultCheck(newS, writeAxiom, orig_input);
if (2 != res2)
*/
}
- /*
- * 'finiteloop' is the finite loop to be expanded
- *
- * Every finiteloop has three parts:
- *
- * 0) Parameter Name
- *
- * 1) Parameter initialization
- *
- * 2) Parameter limit value
- *
- * 3) Increment formula
- *
- * 4) Formula Body
- *
- * ParamToCurrentValMap contains a map from parameters to their
- * current values in the recursion
- *
- * Nested FORs are allowed, but only the innermost loop can have a
- * formula in it
- *
- * STEPS:
- *
- * 0. Populate the top of the parameter stack with 'finiteloop'
- * parameter initial, limit and increment values
- *
- * 1. If formulabody in 'finiteloop' is another for loop, then
- * recurse
- *
- * 2. Else if current parameter value is less than limit value then
- *
- * Instantiate a singleformula
- *
- * Check if the formula is true in the current model
- *
- * If true, discard it
- *
- * If false, add it to the SAT solver to get a new model. Make
- * sure to update array index tables to facilitate array
- * read refinement later.
- *
- * 3. If control reaches here, it means one of the following
- * possibilities (We have instantiated all relevant formulas by
- * now):
- *
- * 3.1: We have UNSAT. Return UNSAT
- *
- * 3.2: We have SAT, and it is indeed a satisfying model
- */
int BeevMgr::Expand_FiniteLoop(const ASTNode& finiteloop,
ASTNodeMap* ParamToCurrentValMap) {
- //Make sure that the parameter is a variable
+ /*
+ * 'finiteloop' is the finite loop to be expanded
+ *
+ * Every finiteloop has three parts:
+ *
+ * 0) Parameter Name
+ *
+ * 1) Parameter initialization
+ *
+ * 2) Parameter limit value
+ *
+ * 3) Increment formula
+ *
+ * 4) Formula Body
+ *
+ * ParamToCurrentValMap contains a map from parameters to their
+ * current values in the recursion
+ *
+ * Nested FORs are allowed, but only the innermost loop can have a
+ * formula in it
+ *
+ * STEPS:
+ *
+ * 0. Populate the top of the parameter stack with 'finiteloop'
+ * parameter initial, limit and increment values
+ *
+ * 1. If formulabody in 'finiteloop' is another for loop, then
+ * recurse
+ *
+ * 2. Else if current parameter value is less than limit value then
+ *
+ * Instantiate a singleformula
+ *
+ * Check if the formula is true in the current model
+ *
+ * If true, discard it
+ *
+ * If false, add it to the SAT solver to get a new model. Make
+ * sure to update array index tables to facilitate array
+ * read refinement later.
+ *
+ * 3. If control reaches here, it means one of the following
+ * possibilities (We have instantiated all relevant formulas by
+ * now):
+ *
+ * 3.1: We have UNSAT. Return UNSAT
+ *
+ * 3.2: We have SAT, and it is indeed a satisfying model
+ */
+
+ //BVTypeCheck should have already checked the sanity of the input
+ //FOR-formula
ASTNode parameter = finiteloop[0];
int paramInit = GetUnsignedConst(finiteloop[1]);
int paramLimit = GetUnsignedConst(finiteloop[2]);
include ../../scripts/Makefile.common
#SRCS = AST.cpp ASTKind.cpp ASTUtil.cpp BitBlast.cpp SimpBool.cpp ToCNF.cpp DPLLMgr.cpp ToSAT.cpp Transform.cpp
-SRCS = AST.cpp ASTKind.cpp ASTUtil.cpp BitBlast.cpp SimpBool.cpp ToCNF.cpp ToSAT.cpp Transform.cpp AbstractionRefinement.cpp printer/SMTLIBPrinter.cpp printer/dotPrinter.cpp printer/CPrinter.cpp printer/PLPrinter.cpp printer/LispPrinter.cpp
+SRCS = AST.cpp ASTKind.cpp ASTUtil.cpp BitBlast.cpp SimpBool.cpp ToCNF.cpp ToSAT.cpp Transform.cpp AbstractionRefinement.cpp printer/AssortedPrinters.cpp printer/SMTLIBPrinter.cpp printer/dotPrinter.cpp printer/CPrinter.cpp printer/PLPrinter.cpp printer/LispPrinter.cpp
OBJS = $(SRCS:.cpp=.o)
CFLAGS += -I../sat/mtl -I../sat/core
return true;
else
return false;
- }
-
- // GLOBAL FUNCTION: Prints statistics from the MINISAT Solver
- void BeevMgr::PrintStats(MINISAT::Solver& s)
- {
- if (!stats_flag)
- return;
- double cpu_time = MINISAT::cpuTime();
- uint64_t mem_used = MINISAT::memUsed();
- reportf("restarts : %llu\n", s.starts);
- reportf("conflicts : %llu (%.0f /sec)\n", s.conflicts , s.conflicts /cpu_time);
- reportf("decisions : %llu (%.0f /sec)\n", s.decisions , s.decisions /cpu_time);
- reportf("propagations : %llu (%.0f /sec)\n", s.propagations, s.propagations/cpu_time);
- reportf("conflict literals : %llu (%4.2f %% deleted)\n", s.tot_literals,
- (s.max_literals - s.tot_literals)*100 / (double)s.max_literals);
- if (mem_used != 0)
- reportf("Memory used : %.2f MB\n", mem_used / 1048576.0);
- reportf("CPU time : %g s\n", cpu_time);
- }
-
- // Prints Satisfying assignment directly, for debugging.
- void BeevMgr::PrintSATModel(MINISAT::Solver& newS)
- {
- if (!newS.okay())
- FatalError("PrintSATModel: NO COUNTEREXAMPLE TO PRINT", ASTUndefined);
- // FIXME: Don't put tests like this in the print functions. The print functions
- // should print unconditionally. Put a conditional around the call if you don't
- // want them to print
- if (!(stats_flag && print_nodes_flag))
- return;
-
- int num_vars = newS.nVars();
- cout << "Satisfying assignment: " << endl;
- for (int i = 0; i < num_vars; i++)
- {
- if (newS.model[i] == MINISAT::l_True)
- {
- ASTNode s = _SATVar_to_AST[i];
- cout << s << endl;
- }
- else if (newS.model[i] == MINISAT::l_False)
- {
- ASTNode s = _SATVar_to_AST[i];
- cout << CreateNode(NOT, s) << endl;
- }
- }
- }
+ } //end of toSATandSolve()
// Looks up truth value of ASTNode SYMBOL in MINISAT satisfying assignment.
// Returns ASTTrue if true, ASTFalse if false or undefined.
CheckBBandCNFMemo.clear();
// Call recursive version that does the work.
return CheckBBandCNF_int(newS, form);
- }
+ } //End of CheckBBandCNF()
// Recursive body CheckBBandCNF
// FIXME: Modify this to just check if result is true, and print mismatch
}
return (CheckBBandCNFMemo[form] = result);
- }
+ } //end of CheckBBandCNF_int()
/*FUNCTION: constructs counterexample from MINISAT counterexample
* step1 : iterate through MINISAT counterexample and assemble the
"query evaluates to TRUE under counterexample: NOT OK", _current_query);
}
- /* FUNCTION: prints a counterexample for INVALID inputs. iterate
- * through the CounterExampleMap data structure and print it to
- * stdout
- */
- void BeevMgr::PrintCounterExample(bool t, std::ostream& os)
- {
- //global command-line option
- // FIXME: This should always print the counterexample. If you want
- // to turn it off, check the switch at the point of call.
- if (!print_counterexample_flag)
- {
- return;
- }
-
- //input is valid, no counterexample to print
- if (ValidFlag)
- {
- return;
- }
-
- //if this option is true then print the way dawson wants using a
- //different printer. do not use this printer.
- if (print_arrayval_declaredorder_flag)
- {
- return;
- }
-
- //t is true if SAT solver generated a counterexample, else it is
- //false
- if (!t)
- {
- cerr << "PrintCounterExample: No CounterExample to print: " << endl;
- return;
- }
-
- //os << "\nCOUNTEREXAMPLE: \n" << endl;
- ASTNodeMap::iterator it = CounterExampleMap.begin();
- ASTNodeMap::iterator itend = CounterExampleMap.end();
- for (; it != itend; it++)
- {
- ASTNode f = it->first;
- ASTNode se = it->second;
-
- if (ARRAY_TYPE == se.GetType())
- {
- FatalError("TermToConstTermUsingModel: entry in counterexample is an arraytype. bogus:", se);
- }
-
- //skip over introduced variables
- if (f.GetKind() == SYMBOL && (_introduced_symbols.find(f) != _introduced_symbols.end()))
- continue;
- if (f.GetKind() == SYMBOL || (f.GetKind() == READ && f[0].GetKind() == SYMBOL && f[1].GetKind() == BVCONST))
- {
- os << "ASSERT( ";
- f.PL_Print(os,0);
- os << " = ";
- if (BITVECTOR_TYPE == se.GetType())
- {
- TermToConstTermUsingModel(se, false).PL_Print(os, 0);
- }
- else
- {
- se.PL_Print(os, 0);
- }
- os << " );" << endl;
- }
- }
- //os << "\nEND OF COUNTEREXAMPLE" << endl;
- } //End of PrintCounterExample
-
- /* 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
- * not print anything. This function was specifically written for
- * Dawson Engler's group (bug finding research group at Stanford)
- */
- void BeevMgr::PrintCounterExample_InOrder(bool t)
- {
- //global command-line option to print counterexample. we do not
- //want both counterexample printers to print at the sametime.
- // FIXME: This should always print the counterexample. If you want
- // to turn it off, check the switch at the point of call.
- if (print_counterexample_flag)
- return;
-
- //input is valid, no counterexample to print
- if (ValidFlag)
- return;
-
- //print if the commandline option is '-q'. allows printing the
- //counterexample in order.
- if (!print_arrayval_declaredorder_flag)
- return;
-
- //t is true if SAT solver generated a counterexample, else it is
- //false
- if (!t)
- {
- cerr << "PrintCounterExample: No CounterExample to print: " << endl;
- return;
- }
-
- //vector to store the integer values
- std::vector<int> out_int;
- cout << "% ";
- for (ASTVec::iterator it = _special_print_set.begin(), itend = _special_print_set.end(); it != itend; it++)
- {
- if (ARRAY_TYPE == it->GetType())
- {
- //get the name of the variable
- const char * c = it->GetName();
- std::string ss(c);
- if (!(0 == strncmp(ss.c_str(), "ini_", 4)))
- continue;
- reverse(ss.begin(), ss.end());
-
- //cout << "debugging: " << ss;
- size_t pos = ss.find('_', 0);
- if (!((0 < pos) && (pos < ss.size())))
- continue;
-
- //get the associated length
- std::string sss = ss.substr(0, pos);
- reverse(sss.begin(), sss.end());
- int n = atoi(sss.c_str());
-
- it->PL_Print(cout, 2);
- for (int j = 0; j < n; j++)
- {
- ASTNode index = CreateBVConst(it->GetIndexWidth(), j);
- ASTNode readexpr = CreateTerm(READ, it->GetValueWidth(), *it, index);
- ASTNode val = GetCounterExample(t, readexpr);
- //cout << "ASSERT( ";
- //cout << " = ";
- out_int.push_back(GetUnsignedConst(val));
- //cout << "\n";
- }
- }
- }
- cout << endl;
- for (unsigned int jj = 0; jj < out_int.size(); jj++)
- cout << out_int[jj] << endl;
- cout << endl;
- } //End of PrintCounterExample_InOrder
-
/* FUNCTION: queries the CounterExampleMap object with 'expr' and
* returns the corresponding counterexample value.
*/
//##################################################
//##################################################
-
- void BeevMgr::printCacheStatus()
- {
- cerr << SimplifyMap->size() << endl;
- cerr << SimplifyNegMap->size() << endl;
- cerr << ReferenceCount->size() << endl;
- cerr << TermsAlreadySeenMap.size() << endl;
-
- cerr << SimplifyMap->bucket_count() << endl;
- cerr << SimplifyNegMap->bucket_count() << endl;
- cerr << ReferenceCount->bucket_count() << endl;
- cerr << TermsAlreadySeenMap.bucket_count() << endl;
-
-
-
- }
-
// FIXME: Don't use numeric codes. Use an enum type!
//Acceps a query, calls the SAT solver and generates Valid/InValid.
//if returned 0 then input is INVALID
cc += '0';
}
return CreateBVConst(cc.c_str(), 2);
- }
-
- //This function prints the output of the STP solver
- void BeevMgr::PrintOutput(bool true_iff_valid)
- {
- if (print_output_flag)
- {
- if (smtlib_parser_flag)
- {
- if (true_iff_valid && (BEEV::input_status == TO_BE_SATISFIABLE))
- {
- cerr << "Warning. Expected satisfiable, FOUND unsatisfiable" << endl;
- }
- else if (!true_iff_valid && (BEEV::input_status == TO_BE_UNSATISFIABLE))
- {
- cerr << "Warning. Expected unsatisfiable, FOUND satisfiable" << endl;
- }
- }
- }
-
- if (true_iff_valid)
- {
- ValidFlag = true;
- if (print_output_flag)
- {
- if (smtlib_parser_flag)
- cout << "unsat\n";
- else
- cout << "Valid.\n";
- }
- }
- else
- {
- ValidFlag = false;
- if (print_output_flag)
- {
- if (smtlib_parser_flag)
- cout << "sat\n";
- else
- cout << "Invalid.\n";
- }
- }
- }
-}
-; //end of namespace BEEV
+ } //end of BoolVectoBVConst()
+}; //end of namespace BEEV
projects / francis / stp.git / commitdiff