#OPTIMIZE = -g -pg # Debugging and gprof-style profiling
OPTIMIZE = -g # Debugging
-OPTIMIZE = -O3 -DNDEBUG # Maximum optimization
+OPTIMIZE = -O3 -DNDEBUG # Maximum optimization
#OPTIMIZE = -O3 -DNDEBUG -DLESSBYTES_PERNODE
CFLAGS_BASE = $(OPTIMIZE)
unsigned char *res;
const char *prefix;
- if(print_binary_flag) {
+ if((GlobalSTP->bm)->UserFlags.print_binary_flag) {
res = CONSTANTBV::BitVector_to_Bin(_bvconst);
if (c_friendly)
{
// -*- c++ -*-
#include "UsefulDefs.h"
+#include "../STPManager/STPManager.h"
#include "../main/Globals.h"
namespace BEEV
{
//this function accepts the name of a function (as a char *), and
//records some stats about it. if the input is "print_func_stats",
//the function will then print the stats that it has collected.
- void CountersAndStats(const char * functionname)
+ void CountersAndStats(const char * functionname, STPMgr * bm)
{
static function_counters s;
-
- if (stats_flag)
+ if (bm->UserFlags.stats_flag)
{
if (!strcmp(functionname, "print_func_stats"))
result = TranslateSignedDivModRem(result);
}
- if (division_by_zero_returns_one)
+ if (bm->UserFlags.division_by_zero_returns_one_flag)
{
// This is a difficult rule to introduce in other
// places because it's recursive. i.e. result is
Introduced_SymbolsSet.insert(CurrentSymbol);
assert(BVTypeCheck(ite));
- if (arrayread_refinement_flag)
+ if (bm->UserFlags.arrayread_refinement_flag)
{
// ite is really a variable here; it is an ite in the
// else-branch
//The big substitution function
ASTNode ArrayTransformer::CreateSubstitutionMap(const ASTNode& a)
{
- if (!wordlevel_solve_flag)
+ if (!bm->UserFlags.wordlevel_solve_flag)
return a;
ASTNode output = a;
// Constructor
ArrayTransformer(STPMgr * bm, Simplifier* s) :
- Arrayread_SymbolMap(INITIAL_TABLE_SIZE),
- Introduced_SymbolsSet(INITIAL_TABLE_SIZE),
+ Arrayread_SymbolMap(),
+ Introduced_SymbolsSet(),
bm(bm),
simp(s),
debug_transform(0)
{
- Arrayread_IteMap = new ASTNodeMap(INITIAL_TABLE_SIZE);
- Arrayname_ReadindicesMap = new ASTNodeToVecMap(INITIAL_TABLE_SIZE);
+ Arrayread_IteMap = new ASTNodeMap();
+ Arrayname_ReadindicesMap = new ASTNodeToVecMap();
runTimes = bm->GetRunTimes();
ASTTrue = bm->CreateNode(TRUE);
hash<char *>,
eqstr> function_counters;
#endif
-
- // Function that computes various kinds of statistics for the phases
- // of STP
- void CountersAndStats(const char * functionname);
}; //end of namespace
#endif
{
inputToSAT = simplified_solved_InputToSAT;
- if(optimize_flag)
+ if(bm->UserFlags.optimize_flag)
{
bm->GetRunTimes()->start(RunTimes::CreateSubstitutionMap);
bm->ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
}
- if(wordlevel_solve_flag)
+ if(bm->UserFlags.wordlevel_solve_flag)
{
simplified_solved_InputToSAT =
bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT);
{
inputToSAT = simplified_solved_InputToSAT;
- if(optimize_flag)
+ if(bm->UserFlags.optimize_flag)
{
bm->GetRunTimes()->start(RunTimes::CreateSubstitutionMap);
simplified_solved_InputToSAT =
bm->ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
}
- if(wordlevel_solve_flag)
+ if(bm->UserFlags.wordlevel_solve_flag)
{
simplified_solved_InputToSAT =
bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT);
bm->ASTNodeStats("After SimplifyWrites_Inplace: ",
simplified_solved_InputToSAT);
- bm->start_abstracting = (arraywrite_refinement_flag) ? true : false;
+ bm->start_abstracting =
+ (bm->UserFlags.arraywrite_refinement_flag) ? true : false;
bm->SimplifyWrites_InPlace_Flag = false;
bm->Begin_RemoveWrites = (bm->start_abstracting) ? false : true;
if (bm->start_abstracting)
MINISAT::Solver newS;
//MINISAT::SimpSolver newS;
//MINISAT::UnsoundSimpSolver newS;
- if (arrayread_refinement_flag)
+ if (bm->UserFlags.arrayread_refinement_flag)
{
bm->counterexample_checking_during_refinement = true;
}
orig_input);
if (SOLVER_UNDECIDED != res)
{
- CountersAndStats("print_func_stats");
+ CountersAndStats("print_func_stats", bm);
return res;
}
orig_input);
if (SOLVER_UNDECIDED != res)
{
- CountersAndStats("print_func_stats");
+ CountersAndStats("print_func_stats", bm);
return res;
}
Ctr_Example->SATBased_ArrayWriteRefinement(newS, orig_input);
if (SOLVER_UNDECIDED != res)
{
- CountersAndStats("print_func_stats");
+ CountersAndStats("print_func_stats", bm);
return res;
}
orig_input);
if (SOLVER_UNDECIDED != res)
{
- CountersAndStats("print_func_stats");
+ CountersAndStats("print_func_stats", bm);
return res;
}
//prints statistics for the ASTNode
void STPMgr::ASTNodeStats(const char * c, const ASTNode& a)
{
- if (!stats_flag)
+ if (!UserFlags.stats_flag)
return;
StatInfoSet.clear();
//print node size:
cout << endl << "Printing: " << c;
- if (print_nodes_flag)
+ if (UserFlags.print_nodes_flag)
{
//a.PL_Print(cout,0);
//cout << endl;
return newn;
}
- STPMgr::~STPMgr()
- {
- }
-
-
// GLOBAL FUNCTION: Prints statistics from the MINISAT Solver
void STPMgr::PrintStats(MINISAT::Solver& s)
{
- if (!stats_flag)
+ if (!UserFlags.stats_flag)
return;
double cpu_time = MINISAT::cpuTime();
uint64_t mem_used = MINISAT::memUsed();
#ifndef STPMGR_H
#define STPMGR_H
+#include "UserDefinedFlags.h"
#include "../AST/AST.h"
#include "../parser/let-funcs.h"
ASTBVConst::ASTBVConstHasher,
ASTBVConst::ASTBVConstEqual> ASTBVConstSet;
+ typedef HASHMAP<
+ ASTNode,
+ ASTNodeSet,
+ ASTNode::ASTNodeHasher,
+ ASTNode::ASTNodeEqual> ASTNodeToSetMap;
+
// Unique node tables that enables common subexpression sharing
ASTInteriorSet _interior_unique_table;
// Table to uniquefy bvconst
ASTBVConstSet _bvconst_unique_table;
- typedef HASHMAP<
- ASTNode,
- ASTNodeSet,
- ASTNode::ASTNodeHasher,
- ASTNode::ASTNodeEqual> ASTNodeToSetMap;
-
// Global for assigning new node numbers.
int _max_node_num;
// Ptr to class that reports on the running time of various parts
// of the code
RunTimes * runTimes;
-
+
/****************************************************************
* Private Member Functions *
****************************************************************/
/****************************************************************
* Public Flags *
- * FIXME: Make the private. Get rid of this inelegance *
- ****************************************************************/
+ ****************************************************************/
+ UserDefinedFlags UserFlags;
// This flag, when true, indicates that counterexample is being
// checked by the counterexample checker
// Constructor
STPMgr() :
- _symbol_unique_table(INITIAL_TABLE_SIZE),
- _bvconst_unique_table(INITIAL_TABLE_SIZE),
- _interior_unique_table(INITIAL_TABLE_SIZE),
+ _symbol_unique_table(),
+ _bvconst_unique_table(),
+ _interior_unique_table(),
+ UserFlags(),
_symbol_count(0)
{
_max_node_num = 0;
_current_query = ASTUndefined;
}
- //destructor
- ~STPMgr();
-
//Return ptr to let-variables manager (see parser/let-funcs.h)
LETMgr * GetLetMgr(void)
{
--- /dev/null
+// -*- c++ -*-
+/********************************************************************
+ * AUTHORS: Vijay Ganesh
+ *
+ * BEGIN DATE: November, 2005
+ *
+ * LICENSE: Please view LICENSE file in the home dir of this Program
+ ********************************************************************/
+#ifndef UDEFFLAGS_H
+#define UDEFFLAGS_H
+
+namespace BEEV
+{
+
+ /******************************************************************
+ * Struct UserDefFlags:
+ *
+ * Some userdefined variables that are set through commandline
+ * options.
+ ******************************************************************/
+
+ struct UserDefinedFlags {
+ public:
+ //collect statistics on certain functions
+ bool stats_flag;
+
+ //print DAG nodes
+ bool print_nodes_flag;
+
+ //run STP in optimized mode
+ bool optimize_flag;
+
+ //do sat refinement, i.e. underconstraint the problem, and feed to
+ //SAT. if this works, great. else, add a set of suitable constraints
+ //to re-constraint the problem correctly, and call SAT again, until
+ //all constraints have been added.
+ bool arrayread_refinement_flag;
+
+ //switch to control write refinements
+ bool arraywrite_refinement_flag;
+
+ //check the counterexample against the original input to STP
+ bool check_counterexample_flag;
+
+ //construct the counterexample in terms of original variable based
+ //on the counterexample returned by SAT solver
+ bool construct_counterexample_flag;
+ bool print_counterexample_flag;
+ bool print_binary_flag;
+
+ //Expands out the finite for-construct completely
+ bool expand_finitefor_flag;
+
+ //Determines the number of abstraction-refinement loop count for the
+ //for-construct
+ bool num_absrefine_flag;
+ int num_absrefine;
+
+ //if this option is true then print the way dawson wants using a
+ //different printer. do not use this printer.
+ bool print_arrayval_declaredorder_flag;
+
+ //flag to decide whether to print "valid/invalid" or not
+ bool print_output_flag;
+
+ //print the variable order chosen by the sat solver while it is
+ //solving.
+ bool print_sat_varorder_flag;
+
+ //turn on word level bitvector solver
+ bool wordlevel_solve_flag;
+
+ //XOR flattening optimizations.
+ bool xor_flatten_flag;
+
+ //this flag indicates that the BVSolver() succeeded
+ bool toplevel_solved_flag;
+
+ //print the input back
+ bool print_STPinput_back_flag;
+
+ //Flag to switch on the smtlib parser
+ bool smtlib_parser_flag;
+
+ bool division_by_zero_returns_one_flag;
+
+ bool quick_statistics_flag;
+
+ //CONSTRUCTOR
+ UserDefinedFlags()
+ {
+ //collect statistics on certain functions
+ stats_flag = false;
+
+ //print DAG nodes
+ print_nodes_flag = false;
+
+ //run STP in optimized mode
+ optimize_flag = true;
+
+ // Do sat refinement, i.e. underconstraint the problem, and feed to
+ // SAT. if this works, great. else, add a set of suitable
+ // constraints to re-constraint the problem correctly, and call SAT again,
+ // until all constraints have been added.
+ arrayread_refinement_flag = true;
+
+ //flag to control write refinement
+ arraywrite_refinement_flag = true;
+
+ //check the counterexample against the original input to STP
+ check_counterexample_flag = false;
+
+ //construct the counterexample in terms of original variable based
+ //on the counterexample returned by SAT solver
+ construct_counterexample_flag = true;
+ print_counterexample_flag = false;
+ print_binary_flag = false;
+
+ //Expands out the finite for-construct completely
+ expand_finitefor_flag = false;
+
+ //Determines the number of abstraction-refinement loop count for the
+ //for-construct
+ num_absrefine_flag = false;
+ int num_absrefine = 0;
+
+ //if this option is true then print the way dawson wants using a
+ //different printer. do not use this printer.
+ print_arrayval_declaredorder_flag = false;
+
+ //flag to decide whether to print "valid/invalid" or not
+ print_output_flag = false;
+
+ //print the variable order chosen by the sat solver while it is
+ //solving.
+ print_sat_varorder_flag = false;
+
+ //turn on word level bitvector solver
+ wordlevel_solve_flag = true;
+
+ //turn off XOR flattening
+ xor_flatten_flag = false;
+
+ //Flag to switch on the smtlib parser
+ smtlib_parser_flag = false;
+
+ //print the input back
+ print_STPinput_back_flag = false;
+
+ // If enabled. division, mod and remainder by zero will evaluate to
+ // 1.
+ division_by_zero_returns_one_flag = false;
+
+ quick_statistics_flag=false;
+ } //End of constructor for UserDefinedFlags
+
+ }; //End of struct UserDefinedFlags
+};//end of namespace
+
+#endif
* time or all the false axioms each time).
*****************************************************************/
SOLVER_RETURN_TYPE
- AbsRefine_CounterExample::SATBased_ArrayReadRefinement(MINISAT::Solver& SatSolver,
- const ASTNode& inputAlreadyInSAT,
- const ASTNode& original_input) {
+ AbsRefine_CounterExample::
+ SATBased_ArrayReadRefinement(MINISAT::Solver& SatSolver,
+ const ASTNode& inputAlreadyInSAT,
+ const ASTNode& original_input) {
//printf("doing array read refinement\n");
- if (!arrayread_refinement_flag)
+ if (!bm->UserFlags.arrayread_refinement_flag)
FatalError("SATBased_ArrayReadRefinement: Control should not reach here");
ASTVec FalseAxiomsVec, RemainingAxiomsVec;
if (!newS.okay())
return;
- if (!construct_counterexample_flag)
+ if (!bm->UserFlags.construct_counterexample_flag)
return;
CopySolverMap_To_CounterExample();
void AbsRefine_CounterExample::CheckCounterExample(bool t)
{
- // FIXME: Code is more useful if enable flags are check OUTSIDE the method.
- // If I want to check a counterexample somewhere, I don't want to have to set
- // the flag in order to make it actualy happen!
-
+ // FIXME: Code is more useful if enable flags are check OUTSIDE
+ // the method. If I want to check a counterexample somewhere, I
+ // don't want to have to set the flag in order to make it actualy
+ // happen!
printf("checking counterexample\n");
- if (!check_counterexample_flag)
+ if (!bm->UserFlags.check_counterexample_flag)
{
return;
}
// stdout
void AbsRefine_CounterExample::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)
+ //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 (!bm->UserFlags.print_counterexample_flag)
{
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)
+ if (bm->UserFlags.print_arrayval_declaredorder_flag)
{
return;
}
//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)
+ if (bm->UserFlags.print_counterexample_flag)
return;
//input is valid, no counterexample to print
//print if the commandline option is '-q'. allows printing the
//counterexample in order.
- if (!print_arrayval_declaredorder_flag)
+ if (!bm->UserFlags.print_arrayval_declaredorder_flag)
return;
//t is true if SAT solver generated a counterexample, else it is
{
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))
+ // 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 (!(bm->UserFlags.stats_flag
+ && bm->UserFlags.print_nodes_flag))
return;
int num_vars = newS.nVars();
{
CounterExampleMap.clear();
ConstructCounterExample(SatSolver);
- if (stats_flag && print_nodes_flag)
+ if (bm->UserFlags.stats_flag
+ && bm->UserFlags.print_nodes_flag)
{
PrintSATModel(SatSolver);
}
// counterexample is bogus: flag it
else
{
- if (stats_flag && print_nodes_flag)
+ if (bm->UserFlags.stats_flag
+ && bm->UserFlags.print_nodes_flag)
{
cout << "Supposedly bogus one: \n";
- bool tmp = print_counterexample_flag;
- print_counterexample_flag = true;
+ bool tmp = bm->UserFlags.print_counterexample_flag;
+ bm->UserFlags.print_counterexample_flag = true;
PrintCounterExample(true);
- print_counterexample_flag = tmp;
+ bm->UserFlags.print_counterexample_flag = tmp;
}
return SOLVER_UNDECIDED;
*/
extern int cvcparse(void*);
-void vc_setFlags(char c) {
+void vc_setFlags(VC vc, char c) {
+ bmstar b = (bmstar)(((stpstar)vc)->bm);
+
std::string helpstring = "Usage: stp [-option] [infile]\n\n";
- helpstring += "STP version: " + BEEV::version + "\n\n";
- helpstring += "-a : switch optimizations off (optimizations are ON by default)\n";
- helpstring += "-c : construct counterexample\n";
- helpstring += "-d : check counterexample\n";
- helpstring += "-e : expand finite-for construct\n";
- helpstring += "-f : number of abstraction-refinement loops\n";
- helpstring += "-h : help\n";
- helpstring += "-m : use the SMTLIB parser\n";
- helpstring += "-p : print counterexample\n";
- helpstring += "-r : switch refinement off (optimizations are ON by default)\n";
- helpstring += "-s : print function statistics\n";
- helpstring += "-v : print nodes \n";
- helpstring += "-w : switch wordlevel solver off (optimizations are ON by default)\n";
- helpstring += "-x : flatten nested XORs\n";
- helpstring += "-y : print counterexample in binary\n";
+ helpstring +=
+ "STP version: " + BEEV::version + "\n\n";
+ helpstring +=
+ "-a : switch optimizations off (optimizations are ON by default)\n";
+ helpstring +=
+ "-c : construct counterexample\n";
+ helpstring +=
+ "-d : check counterexample\n";
+ helpstring +=
+ "-e : expand finite-for construct\n";
+ helpstring +=
+ "-f : number of abstraction-refinement loops\n";
+ helpstring +=
+ "-h : help\n";
+ helpstring +=
+ "-m : use the SMTLIB parser\n";
+ helpstring +=
+ "-p : print counterexample\n";
+ helpstring +=
+ "-r : switch refinement off (optimizations are ON by default)\n";
+ helpstring +=
+ "-s : print function statistics\n";
+ helpstring +=
+ "-v : print nodes \n";
+ helpstring +=
+ "-w : switch wordlevel solver off (optimizations are ON by default)\n";
+ helpstring +=
+ "-x : flatten nested XORs\n";
+ helpstring +=
+ "-y : print counterexample in binary\n";
switch(c) {
case 'a' :
- BEEV::optimize_flag = false;
+ b->UserFlags.optimize_flag = false;
break;
case 'c':
- BEEV::construct_counterexample_flag = true;
+ b->UserFlags.construct_counterexample_flag = true;
break;
case 'd':
- BEEV::construct_counterexample_flag = true;
- BEEV::check_counterexample_flag = true;
+ b->UserFlags.construct_counterexample_flag = true;
+ b->UserFlags.check_counterexample_flag = true;
break;
case 'e':
- BEEV::expand_finitefor_flag = true;
+ b->UserFlags.expand_finitefor_flag = true;
break;
case 'f':
- BEEV::num_absrefine_flag = true;
- //BEEV::num_absrefine = atoi(argv[++i]);
+ b->UserFlags.num_absrefine_flag = true;
+ //b->UserFlags.num_absrefine = atoi(argv[++i]);
break;
case 'h':
fprintf(stderr,BEEV::usage,BEEV::prog);
//return -1;
break;
case 'n':
- BEEV::print_output_flag = true;
+ b->UserFlags.print_output_flag = true;
break;
case 'm':
- BEEV::smtlib_parser_flag=true;
- BEEV::division_by_zero_returns_one = true;
+ b->UserFlags.smtlib_parser_flag=true;
+ b->UserFlags.division_by_zero_returns_one_flag = true;
break;
case 'p':
- BEEV::print_counterexample_flag = true;
+ b->UserFlags.print_counterexample_flag = true;
break;
case 'q':
- BEEV::print_arrayval_declaredorder_flag = true;
+ b->UserFlags.print_arrayval_declaredorder_flag = true;
break;
case 'r':
- BEEV::arrayread_refinement_flag = false;
+ b->UserFlags.arrayread_refinement_flag = false;
break;
case 's' :
- BEEV::stats_flag = true;
+ b->UserFlags.stats_flag = true;
break;
case 'u':
- BEEV::arraywrite_refinement_flag = false;
+ b->UserFlags.arraywrite_refinement_flag = false;
break;
case 'v' :
- BEEV::print_nodes_flag = true;
+ b->UserFlags.print_nodes_flag = true;
break;
case 'w':
- BEEV::wordlevel_solve_flag = false;
+ b->UserFlags.wordlevel_solve_flag = false;
break;
case 'x':
- BEEV::xor_flatten_flag = true;
+ b->UserFlags.xor_flatten_flag = true;
break;
case 'y':
- BEEV::print_binary_flag = true;
+ b->UserFlags.print_binary_flag = true;
break;
case 'z':
- BEEV::print_sat_varorder_flag = true;
+ b->UserFlags.print_sat_varorder_flag = true;
break;
default:
std::string s = "C_interface: vc_setFlags: Unrecognized commandline flag:\n";
//Create a validity Checker. This is the global STPMgr
VC vc_createValidityChecker(void) {
- vc_setFlags('d');
CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot();
if(0 != c) {
cout << CONSTANTBV::BitVector_Error(c) << endl;
BEEV::GlobalSTP = stp;
decls = new BEEV::ASTVec();
//created_exprs.clear();
+ vc_setFlags(stp,'d');
return (VC)stp;
}
// print variable declarations
BEEV::ASTVec declsFromParser = (nodelist)b->ListOfDeclaredVars;
- for(BEEV::ASTVec::iterator it=declsFromParser.begin(),itend=declsFromParser.end(); it!=itend;it++) {
+ for(BEEV::ASTVec::iterator it=declsFromParser.begin(),
+ itend=declsFromParser.end(); it!=itend;it++) {
if(BEEV::BITVECTOR_TYPE == it->GetType()) {
const char* name = it->GetName();
unsigned int bitWidth = it->GetValueWidth();
}
static void vc_printVarDeclsToStream(VC vc, ostream &os) {
- for(BEEV::ASTVec::iterator i = decls->begin(),iend=decls->end();i!=iend;i++) {
+ for(BEEV::ASTVec::iterator i = decls->begin(),
+ iend=decls->end();i!=iend;i++) {
node a = *i;
switch(a.GetType()) {
case BEEV::BITVECTOR_TYPE:
BEEV::Simplifier * simp = new BEEV::Simplifier(b);
for(BEEV::ASTVec::iterator i=v.begin(),iend=v.end();i!=iend;i++) {
b->Begin_RemoveWrites = true;
- BEEV::ASTNode q = (simplify_print == 1) ? simp->SimplifyFormula_TopLevel(*i,false) : *i;
- q = (simplify_print == 1) ? simp->SimplifyFormula_TopLevel(q,false) : q;
+ BEEV::ASTNode q =
+ (simplify_print == 1) ?
+ simp->SimplifyFormula_TopLevel(*i,false) : *i;
+ q =
+ (simplify_print == 1) ?
+ simp->SimplifyFormula_TopLevel(q,false) : q;
b->Begin_RemoveWrites = false;
os << "ASSERT( ";
q.PL_Print(os);
vc_printAssertsToStream(vc, cout, simplify_print);
}
-void vc_printQueryStateToBuffer(VC vc, Expr e, char **buf, unsigned long *len, int simplify_print){
+void vc_printQueryStateToBuffer(VC vc, Expr e,
+ char **buf,
+ unsigned long *len, int simplify_print){
assert(vc);
assert(e);
assert(buf);
// formate the state of the query
std::ostringstream os;
- BEEV::print_counterexample_flag = true;
+ b->UserFlags.print_counterexample_flag = true;
os << "COUNTEREXAMPLE BEGIN: \n";
ce->PrintCounterExample(true,os);
os << "COUNTEREXAMPLE END: \n";
bmstar b = (bmstar)(((stpstar)vc)->bm);
ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example);
- BEEV::print_counterexample_flag = true;
+ b->UserFlags.print_counterexample_flag = true;
cout << "COUNTEREXAMPLE BEGIN: \n";
ce->PrintCounterExample(true);
cout << "COUNTEREXAMPLE END: \n";
cvcparse((void*)AssertsQuery);
BEEV::ASTNode asserts = (*(BEEV::ASTVec*)AssertsQuery)[0];
BEEV::ASTNode query = (*(BEEV::ASTVec*)AssertsQuery)[1];
- //b->TopLevelSTP(asserts, query);
+ //BEEV::GlobalSTP->TopLevelSTP(asserts, query);
node oo = b->CreateNode(BEEV::NOT,query);
node o = b->CreateNode(BEEV::AND,asserts,oo);
bmstar b = (bmstar)(((stpstar)vc)->bm);
ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example);
- BEEV::print_counterexample_flag = true;
+ b->UserFlags.print_counterexample_flag = true;
os << "COUNTEREXAMPLE BEGIN: \n";
ce->PrintCounterExample(true, os);
os << "COUNTEREXAMPLE END: \n";
* EXPRESSED OR IMPLIED. USE IT AT YOUR OWN RISK.
********************************************************************/
// -*- c++ -*-
+
#ifndef _cvcl__include__c_interface_h_
#define _cvcl__include__c_interface_h_
// h : help
// s : stats
// v : print nodes
- void vc_setFlags(char c);
+ void vc_setFlags(VC vc, char c);
//! Flags can be NULL
VC vc_createValidityChecker(void);
namespace BEEV
{
- //some global variables that are set through commandline options. it
- //is best that these variables remain global. Default values set
- //here
- //
- //collect statistics on certain functions
- bool stats_flag = false;
-
- //print DAG nodes
- bool print_nodes_flag = false;
-
- //run STP in optimized mode
- bool optimize_flag = true;
-
- //do sat refinement, i.e. underconstraint the problem, and feed to
- //SAT. if this works, great. else, add a set of suitable constraints
- //to re-constraint the problem correctly, and call SAT again, until
- //all constraints have been added.
- bool arrayread_refinement_flag = true;
-
- //flag to control write refinement
- bool arraywrite_refinement_flag = true;
-
- //check the counterexample against the original input to STP
- bool check_counterexample_flag = false;
-
- //construct the counterexample in terms of original variable based
- //on the counterexample returned by SAT solver
- bool construct_counterexample_flag = true;
- bool print_counterexample_flag = false;
- bool print_binary_flag = false;
-
- //Expands out the finite for-construct completely
- bool expand_finitefor_flag = false;
-
- //Determines the number of abstraction-refinement loop count for the
- //for-construct
- bool num_absrefine_flag = false;
- int num_absrefine = 0;
-
-
- //if this option is true then print the way dawson wants using a
- //different printer. do not use this printer.
- bool print_arrayval_declaredorder_flag = false;
-
- //flag to decide whether to print "valid/invalid" or not
- bool print_output_flag = false;
-
- //print the variable order chosen by the sat solver while it is
- //solving.
- bool print_sat_varorder_flag = false;
-
- //turn on word level bitvector solver
- bool wordlevel_solve_flag = true;
-
- //turn off XOR flattening
- bool xor_flatten_flag = false;
-
- //Flag to switch on the smtlib parser
- bool smtlib_parser_flag = false;
-
- //print the input back
- bool print_STPinput_back_flag = false;
-
- // If enabled. division, mod and remainder by zero will evaluate to
- // 1.
- bool division_by_zero_returns_one = false;
-
- bool quick_statistics_flag=false;
-
enum inputStatus input_status = NOT_DECLARED;
//global BEEVMGR for the parser. Use exclusively for parsing
STPMgr * ParserBM;
void (*vc_error_hdlr)(const char* err_msg) = NULL;
- /** This is reusable empty vector, for representing empty children
- arrays */
+
+ // This is reusable empty vector, for representing empty children
+ // arrays
ASTVec _empty_ASTVec;
- //Some global vars for the Main function.
+ //Some constant global vars for the Main function. Once they are
+ //set, these globals will remain constants. These vars are not used
+ //in the STP library.
const char * prog = "stp";
int linenum = 1;
const char * usage = "Usage: %s [-option] [infile]\n";
class BVSolver;
class STP;
- //some global variables that are set through commandline options. it
- //is best that these variables remain global. Default values set
- //here
- //
- //collect statistics on certain functions
- extern bool stats_flag;
-
- //print DAG nodes
- extern bool print_nodes_flag;
-
- //run STP in optimized mode
- extern bool optimize_flag;
-
- //do sat refinement, i.e. underconstraint the problem, and feed to
- //SAT. if this works, great. else, add a set of suitable constraints
- //to re-constraint the problem correctly, and call SAT again, until
- //all constraints have been added.
- extern bool arrayread_refinement_flag;
-
- //switch to control write refinements
- extern bool arraywrite_refinement_flag;
-
- //check the counterexample against the original input to STP
- extern bool check_counterexample_flag;
-
- //construct the counterexample in terms of original variable based
- //on the counterexample returned by SAT solver
- extern bool construct_counterexample_flag;
- extern bool print_counterexample_flag;
- extern bool print_binary_flag;
-
- //Expands out the finite for-construct completely
- extern bool expand_finitefor_flag;
-
- //Determines the number of abstraction-refinement loop count for the
- //for-construct
- extern bool num_absrefine_flag;
- extern int num_absrefine;
-
- //if this option is true then print the way dawson wants using a
- //different printer. do not use this printer.
- extern bool print_arrayval_declaredorder_flag;
-
- //flag to decide whether to print "valid/invalid" or not
- extern bool print_output_flag;
-
- //print the variable order chosen by the sat solver while it is
- //solving.
- extern bool print_sat_varorder_flag;
-
- //turn on word level bitvector solver
- extern bool wordlevel_solve_flag;
-
- //XOR flattening optimizations.
- extern bool xor_flatten_flag;
-
- //this flag indicates that the BVSolver() succeeded
- extern bool toplevel_solved_flag;
-
- //print the input back
- extern bool print_STPinput_back_flag;
-
- //Flag to switch on the smtlib parser
- extern bool smtlib_parser_flag;
-
- extern bool division_by_zero_returns_one;
-
- extern bool quick_statistics_flag;
+ /***************************************************************
+ * ENUM TYPES
+ *
+ ***************************************************************/
enum inputStatus
{
TO_BE_UNSATISFIABLE,
TO_BE_UNKNOWN // Specified in the input file as unknown.
};
- extern enum inputStatus input_status;
//return types for the GetType() function in ASTNode class
enum types
SOLVER_ERROR=-100
};
- //Useful global variables. Use for parsing only
- extern STP * GlobalSTP;
- extern STPMgr * ParserBM;
-
//Empty vector. Useful commonly used ASTNodes
extern std::vector<ASTNode> _empty_ASTVec;
extern ASTNode ASTFalse, ASTTrue, ASTUndefined;
- //Some global vars for the Main function.
+ //Useful global variables. Use for parsing only
+ extern STP * GlobalSTP;
+ extern STPMgr * ParserBM;
+
+ //Some constant global vars for the Main function. Once they are
+ //set, these globals will remain constants. These vars are not used
+ //in the STP library.
extern const char * prog;
extern int linenum;
extern const char * usage;
extern std::string helpstring;
extern const std::string version;
+ extern enum inputStatus input_status;
+
+
+ // Function that computes various kinds of statistics for the phases
+ // of STP
+ void CountersAndStats(const char * functionname, STPMgr * bm);
}; //end of namespace BEEV
#endif
switch(argv[i][1])
{
case 'a' :
- optimize_flag = false;
+ bm->UserFlags.optimize_flag = false;
break;
case 'b':
- print_STPinput_back_flag = true;
+ bm->UserFlags.print_STPinput_back_flag = true;
break;
case 'c':
- construct_counterexample_flag = true;
+ bm->UserFlags.construct_counterexample_flag = true;
break;
case 'd':
- construct_counterexample_flag = true;
- check_counterexample_flag = true;
+ bm->UserFlags.construct_counterexample_flag = true;
+ bm->UserFlags.check_counterexample_flag = true;
break;
case 'e':
- expand_finitefor_flag = true;
+ bm->UserFlags.expand_finitefor_flag = true;
break;
case 'f':
- num_absrefine_flag = true;
- num_absrefine = atoi(argv[++i]);
+ bm->UserFlags.num_absrefine_flag = true;
+ bm->UserFlags.num_absrefine = atoi(argv[++i]);
break;
case 'h':
fprintf(stderr,usage,prog);
return -1;
break;
case 'n':
- print_output_flag = true;
+ bm->UserFlags.print_output_flag = true;
break;
case 'm':
- smtlib_parser_flag=true;
- division_by_zero_returns_one = true;
+ bm->UserFlags.smtlib_parser_flag=true;
+ bm->UserFlags.division_by_zero_returns_one_flag = true;
break;
case 'p':
- print_counterexample_flag = true;
+ bm->UserFlags.print_counterexample_flag = true;
break;
case 'q':
- print_arrayval_declaredorder_flag = true;
+ bm->UserFlags.print_arrayval_declaredorder_flag = true;
break;
case 'r':
- arrayread_refinement_flag = false;
+ bm->UserFlags.arrayread_refinement_flag = false;
break;
case 's' :
- stats_flag = true;
+ bm->UserFlags.stats_flag = true;
break;
case 't':
- quick_statistics_flag = true;
+ bm->UserFlags.quick_statistics_flag = true;
break;
case 'u':
- arraywrite_refinement_flag = false;
+ bm->UserFlags.arraywrite_refinement_flag = false;
break;
case 'v' :
- print_nodes_flag = true;
+ bm->UserFlags.print_nodes_flag = true;
break;
case 'w':
- wordlevel_solve_flag = false;
+ bm->UserFlags.wordlevel_solve_flag = false;
break;
case 'x':
- xor_flatten_flag = true;
+ bm->UserFlags.xor_flatten_flag = true;
break;
case 'y':
- print_binary_flag = true;
+ bm->UserFlags.print_binary_flag = true;
break;
case 'z':
- print_sat_varorder_flag = true;
+ bm->UserFlags.print_sat_varorder_flag = true;
break;
default:
fprintf(stderr,usage,prog);
}
} else {
infile = argv[i];
- if (smtlib_parser_flag)
+ if (bm->UserFlags.smtlib_parser_flag)
{
smtin = fopen(infile,"r");
if(smtin == NULL)
}
//want to print the output always from the commandline.
- print_output_flag = true;
+ bm->UserFlags.print_output_flag = true;
ASTVec * AssertsQuery = new ASTVec;
CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot();
if(0 != c) {
}
bm->GetRunTimes()->start(RunTimes::Parsing);
- if (smtlib_parser_flag)
+ if (bm->UserFlags.smtlib_parser_flag)
{
smtparse((void*)AssertsQuery);
}
ASTNode asserts = (*(ASTVec*)AssertsQuery)[0];
ASTNode query = (*(ASTVec*)AssertsQuery)[1];
- if(print_STPinput_back_flag)
+ if(bm->UserFlags.print_STPinput_back_flag)
{
- if(smtlib_parser_flag)
+ if(bm->UserFlags.smtlib_parser_flag)
{
// don't pass the query. It's not returned by the smtlib
// parser.
} //end of PrintBack if
SOLVER_RETURN_TYPE ret = GlobalSTP->TopLevelSTP(asserts, query);
- if (quick_statistics_flag)
+ if (bm->UserFlags.quick_statistics_flag)
{
bm->GetRunTimes()->print();
}
counterexample : COUNTEREXAMPLE_TOK ';'
{
- print_counterexample_flag = true;
+ ParserBM->UserFlags.print_counterexample_flag = true;
(GlobalSTP->Ctr_Example)->PrintCounterExample(true);
}
;
//var
$2->SetIndexWidth($3.indexwidth);
$2->SetValueWidth($3.valuewidth);
- if(print_STPinput_back_flag)
+ if(ParserBM->UserFlags.print_STPinput_back_flag)
ParserBM->ListOfDeclaredVars.push_back(*$2);
}
| LPAREN_TOK FORMID_TOK RPAREN_TOK
//var
$2->SetIndexWidth(0);
$2->SetValueWidth(0);
- if(print_STPinput_back_flag)
+ if(ParserBM->UserFlags.print_STPinput_back_flag)
ParserBM->ListOfDeclaredVars.push_back(*$2);
}
;
break;
}
- // SBVREM : Result of rounding the quotient towards zero. i.e. (-10)/3, has a remainder of -1
- // SBVMOD : Result of rounding the quotient towards -infinity. i.e. (-10)/3, has a modulus of 2.
- // EXCEPT THAT if it divides exactly and the signs are different, then it's equal to the dividend.
+ // SBVREM : Result of rounding the quotient towards
+ // zero. i.e. (-10)/3, has a remainder of -1
+ //
+ // SBVMOD : Result of rounding the quotient towards
+ // -infinity. i.e. (-10)/3, has a modulus of 2. EXCEPT THAT
+ // if it divides exactly and the signs are different, then
+ // it's equal to the dividend.
case SBVDIV:
case SBVREM:
{
CBV quotient = CONSTANTBV::BitVector_Create(inputwidth, true);
CBV remainder = CONSTANTBV::BitVector_Create(inputwidth, true);
- if (division_by_zero_returns_one && CONSTANTBV::BitVector_is_empty(tmp1))
+ if (_bm->UserFlags.division_by_zero_returns_one_flag
+ && CONSTANTBV::BitVector_is_empty(tmp1))
{
// Expecting a division by zero. Just return one.
OutputNode = _bm->CreateOneConst(outputwidth);
}
else
{
- CONSTANTBV::ErrCode e = CONSTANTBV::BitVector_Divide(quotient, tmp0, tmp1, remainder);
+ CONSTANTBV::ErrCode e =
+ CONSTANTBV::BitVector_Divide(quotient, tmp0, tmp1, remainder);
if (e != 0)
{
tmp0 = CONSTANTBV::BitVector_Clone(tmp0);
tmp1 = CONSTANTBV::BitVector_Clone(tmp1);
- if (division_by_zero_returns_one && CONSTANTBV::BitVector_is_empty(tmp1))
+ if (_bm->UserFlags.division_by_zero_returns_one_flag
+ && CONSTANTBV::BitVector_is_empty(tmp1))
{
// Expecting a division by zero. Just return one.
OutputNode = _bm->CreateOneConst(outputwidth);
CBV quotient = CONSTANTBV::BitVector_Create(inputwidth, true);
CBV remainder = CONSTANTBV::BitVector_Create(inputwidth, true);
- if (division_by_zero_returns_one && CONSTANTBV::BitVector_is_empty(tmp1))
+ if (_bm->UserFlags.division_by_zero_returns_one_flag
+ && CONSTANTBV::BitVector_is_empty(tmp1))
{
// Expecting a division by zero. Just return one.
OutputNode = _bm->CreateOneConst(outputwidth);
if (it != itend)
{
output = it->second;
- CountersAndStats("Successful_CheckSimplifyMap");
+ CountersAndStats("Successful_CheckSimplifyMap", _bm);
return true;
}
ASTTrue :
(ASTTrue == it->second) ?
ASTFalse : _bm->CreateNode(NOT, it->second);
- CountersAndStats("2nd_Successful_CheckSimplifyMap");
+ CountersAndStats("2nd_Successful_CheckSimplifyMap", _bm);
return true;
}
if (it != itend)
{
//cerr << "found:" << *it << endl;
- CountersAndStats("Successful_CheckAlwaysTrueFormMap");
+ CountersAndStats("Successful_CheckAlwaysTrueFormMap", _bm);
return true;
}
bool pushNeg, ASTNodeMap* VarConstMap)
{
_bm->GetRunTimes()->start(RunTimes::SimplifyTopLevel);
- if (smtlib_parser_flag)
+ if (_bm->UserFlags.smtlib_parser_flag)
BuildReferenceCountMap(b);
ASTNode out = SimplifyFormula(b, pushNeg, VarConstMap);
ResetSimplifyMaps();
//takes care of some simple ITE Optimizations in the context of equations
ASTNode Simplifier::ITEOpt_InEqs(const ASTNode& in, ASTNodeMap* VarConstMap)
{
- CountersAndStats("ITEOpts_InEqs");
+ CountersAndStats("ITEOpts_InEqs", _bm);
if (!(EQ == in.GetKind()))
{
//return the constructed equality
ASTNode Simplifier::CreateSimplifiedEQ(const ASTNode& in1, const ASTNode& in2)
{
- CountersAndStats("CreateSimplifiedEQ");
+ CountersAndStats("CreateSimplifiedEQ", _bm);
Kind k1 = in1.GetKind();
Kind k2 = in2.GetKind();
ASTNode t0 = in0;
ASTNode t1 = in1;
ASTNode t2 = in2;
- CountersAndStats("CreateSimplifiedITE");
- if (!optimize_flag)
+ CountersAndStats("CreateSimplifiedITE", _bm);
+ if (!_bm->UserFlags.optimize_flag)
{
if (t1.GetValueWidth() != t2.GetValueWidth())
{
return _bm->CreateTerm(ITE, t1.GetValueWidth(), t0, t1, t2);
}
- ASTNode Simplifier::CreateSimplifiedFormulaITE(const ASTNode& in0, const ASTNode& in1, const ASTNode& in2)
+ ASTNode
+ Simplifier::
+ CreateSimplifiedFormulaITE(const ASTNode& in0,
+ const ASTNode& in1, const ASTNode& in2)
{
ASTNode t0 = in0;
ASTNode t1 = in1;
ASTNode t2 = in2;
- CountersAndStats("CreateSimplifiedFormulaITE");
+ CountersAndStats("CreateSimplifiedFormulaITE", _bm);
- if (optimize_flag)
+ if (_bm->UserFlags.optimize_flag)
{
if (t0 == ASTTrue)
return t1;
SimplifyMap = new ASTNodeMap(INITIAL_TABLE_SIZE);
SimplifyNegMap = new ASTNodeMap(INITIAL_TABLE_SIZE);
SolverMap = new ASTNodeMap(INITIAL_TABLE_SIZE);
- ReadOverWrite_NewName_Map = new ASTNodeMap(INITIAL_TABLE_SIZE);
- ReferenceCount = new ASTNodeCountMap(INITIAL_TABLE_SIZE);
+ ReadOverWrite_NewName_Map = new ASTNodeMap();
+ ReferenceCount = new ASTNodeCountMap();
ASTTrue = bm->CreateNode(TRUE);
ASTFalse = bm->CreateNode(FALSE);
CNFMgr* cm = new CNFMgr(bm);
ClauseList* cl = cm->convertToCNF(BBFormula);
- if (stats_flag)
+ if (bm->UserFlags.stats_flag)
{
cerr << "Number of clauses:" << cl->size() << endl;
}
{
bool true_iff_valid = (SOLVER_VALID == ret);
- if (print_output_flag)
+ if (bm->UserFlags.print_output_flag)
{
- if (smtlib_parser_flag)
+ if (bm->UserFlags.smtlib_parser_flag)
{
if (true_iff_valid &&
(input_status == TO_BE_SATISFIABLE))
{
- cerr << "Warning. Expected satisfiable, FOUND unsatisfiable" << endl;
+ cerr << "Warning. Expected satisfiable,"\
+ " FOUND unsatisfiable" << endl;
}
else if (!true_iff_valid &&
(input_status == TO_BE_UNSATISFIABLE))
{
- cerr << "Warning. Expected unsatisfiable, FOUND satisfiable" << endl;
+ cerr << "Warning. Expected unsatisfiable,"\
+ " FOUND satisfiable" << endl;
}
}
}
if (true_iff_valid)
{
bm->ValidFlag = true;
- if (print_output_flag)
+ if (bm->UserFlags.print_output_flag)
{
- if (smtlib_parser_flag)
+ if (bm->UserFlags.smtlib_parser_flag)
cout << "unsat\n";
else
cout << "Valid.\n";
else
{
bm->ValidFlag = false;
- if (print_output_flag)
+ if (bm->UserFlags.print_output_flag)
{
- if (smtlib_parser_flag)
+ if (bm->UserFlags.smtlib_parser_flag)
cout << "sat\n";
else
cout << "Invalid.\n";
* LICENSE: Please view LICENSE file in the home dir of this Program
********************************************************************/
-// Simplifying create methods for Boolean operations.
-// These are only very simple local simplifications.
+// Simplifying create methods for Boolean operations. These are only
+// very simple local simplifications.
-// This is somewhat redundant with Vijay's simplifier code. They
-// need to be merged.
-// FIXME: control with optimize flag.
+// This is somewhat redundant with Vijay's simplifier code. They need
+// to be merged. FIXME: control with optimize flag.
static bool _trace_simpbool = 0;
static bool _disable_simpbool = 0;
#include "../STPManager/STPManager.h"
// SMTLIB experimental hack. Try allocating a single stack here for
-// children to reduce growing of vectors.
-//BEEV::ASTVec child_stack;
+// children to reduce growing of vectors. BEEV::ASTVec child_stack;
namespace BEEV
{
//return CreateSimpForm(kind, child_stack);
}
- ASTNode STPMgr::CreateSimpForm(Kind kind, const ASTNode& child0, const ASTNode& child1)
+ ASTNode STPMgr::CreateSimpForm(Kind kind,
+ const ASTNode& child0, const ASTNode& child1)
{
ASTVec children;
//child_stack.clear(); // could just reset top pointer.
//return CreateSimpForm(kind, child_stack);
}
- ASTNode STPMgr::CreateSimpForm(Kind kind, const ASTNode& child0, const ASTNode& child1, const ASTNode& child2)
+ ASTNode STPMgr::CreateSimpForm(Kind kind,
+ const ASTNode& child0,
+ const ASTNode& child1, const ASTNode& child2)
{
ASTVec children;
//child_stack.clear(); // could just reset top pointer.
{
fflag = 1; // For selective debug printing (below).
// append grandchildren to children
- flat_children.insert(flat_children.end(), gchildren.begin(), gchildren.end());
+ flat_children.insert(flat_children.end(),
+ gchildren.begin(), gchildren.end());
}
else
{
return flat_children;
}
- ASTNode STPMgr::CreateSimpAndOr(bool IsAnd, const ASTNode& form1, const ASTNode& form2)
+ ASTNode STPMgr::CreateSimpAndOr(bool IsAnd,
+ const ASTNode& form1, const ASTNode& form2)
{
ASTVec children;
children.push_back(form1);
ASTVec new_children;
ASTVec flat_children;
- if (xor_flatten_flag)
+ if (UserFlags.xor_flatten_flag)
{
flat_children = FlattenKind(k, children);
}
ASTVec::const_iterator it_end = flat_children.end();
ASTVec::const_iterator next_it;
- for (ASTVec::const_iterator it = flat_children.begin(); it != it_end; it = next_it)
+ for (ASTVec::const_iterator it = flat_children.begin();
+ it != it_end; it = next_it)
{
next_it = it + 1;
bool nextexists = (next_it < it_end);
// drop it
// cout << "Dropping [" << it->GetNodeNum() << "]" << endl;
}
- else if (nextexists && (next_it->GetKind() == NOT) && ((*next_it)[0] == *it))
+ else if (nextexists && (next_it->GetKind() == NOT)
+ && ((*next_it)[0] == *it))
{
// form and negation -- return FALSE for AND, TRUE for OR.
retval = annihilator;
ASTVec flat_children; // empty vector
ASTVec::const_iterator it_end = children.end();
- if (xor_flatten_flag)
+ if (UserFlags.xor_flatten_flag)
{
flat_children = FlattenKind(XOR, children);
}
// so that it gets tossed, too.
*next_it = ASTFalse;
}
- else if (nextexists && (next_it->GetKind() == NOT) && ((*next_it)[0] == *it))
+ else if (nextexists && (next_it->GetKind() == NOT)
+ && ((*next_it)[0] == *it))
{
// x XOR NOT x = TRUE. Skip current, write "true" into next_it
// so that it gets tossed, too.
}
// FIXME: How do I know whether ITE is a formula or not?
- ASTNode STPMgr::CreateSimpFormITE(const ASTNode& child0, const ASTNode& child1, const ASTNode& child2)
+ ASTNode STPMgr::CreateSimpFormITE(const ASTNode& child0,
+ const ASTNode& child1,
+ const ASTNode& child2)
{
ASTNode retval;
if (_trace_simpbool)
{
- cout << "========" << endl << "CreateSimpFormITE " << child0 << child1 << child2 << endl;
+ cout << "========" << endl
+ << "CreateSimpFormITE "
+ << child0 << child1 << child2 << endl;
}
if (ASTTrue == child0)
}
/* FUNCTION: convert ASTClauses to MINISAT clauses and solve.
- * Accepts ASTClauses and converts them to MINISAT clauses. Then adds
- * the newly minted MINISAT clauses to the local SAT instance, and
- * calls solve(). If solve returns unsat, then stop and return
+ * Accepts ASTClauses and converts them to MINISAT clauses. Then
+ * adds the newly minted MINISAT clauses to the local SAT instance,
+ * and calls solve(). If solve returns unsat, then stop and return
* unsat. else continue.
*/
- // FIXME: Still need to deal with TRUE/FALSE in clauses!
- //
- //bool ToSAT::toSATandSolve(MINISAT::Solver& newS,
- //ClauseList& cll, ASTNodeToIntMap& heuristic)
bool ToSAT::toSATandSolve(MINISAT::Solver& newS, ClauseList& cll)
{
- CountersAndStats("SAT Solver");
+ CountersAndStats("SAT Solver", bm);
bm->GetRunTimes()->start(RunTimes::SendingToSAT);
./a10.out
11:
g++ $(CXXFLAGS) squares-leak.c -lstp -o a11.out
- ./a11.out
+# ./a11.out
12:
g++ $(CXXFLAGS) stp-counterex.c -lstp -o a12.out
./a12.out
#include "c_interface.h"
int main() {
VC vc = vc_createValidityChecker();
- vc_setFlags('n');
- vc_setFlags('d');
- vc_setFlags('p');
+ vc_setFlags(vc,'n');
+ vc_setFlags(vc,'d');
+ vc_setFlags(vc,'p');
Expr cvcl_array = vc_varExpr1(vc, "a",32,32);
Expr i = vc_varExpr1(vc, "i", 0, 8);
int main()
{
- vc_setFlags('v');
- vc_setFlags('s');
- vc_setFlags('n');
- //vc_setFlags('a');
- //vc_setFlags('w');
- //vc_setFlags('r');
VC vc = vc_createValidityChecker();
+ vc_setFlags(vc,'v');
+ vc_setFlags(vc,'s');
+ vc_setFlags(vc,'n');
+ //vc_setFlags(vc,'a');
+ //vc_setFlags(vc,'w');
+ //vc_setFlags(vc,'r');
+
//vc_push(vc);
Expr e12866 = vc_varExpr(vc, "at", vc_bvType(vc, 5));
Expr e12867 = e12866;
#include "c_interface.h"
#include <iostream>
int main() {
- vc_setFlags('w');
- //vc_setFlags('v');
- //vc_setFlags('s');
- //vc_setFlags('a');
- vc_setFlags('n');
VC vc = vc_createValidityChecker();
+ vc_setFlags(vc,'w');
+ //vc_setFlags(vc,'v');
+ //vc_setFlags(vc,'s');
+ //vc_setFlags(vc,'a');
+ vc_setFlags(vc,'n');
+
vc_push(vc);
Expr e5283955 = vc_varExpr(vc, "at", vc_bvType(vc, 5));
Expr e5283956 = e5283955;
E_table[35] = 3;
- vc_setFlags('n');
- vc_setFlags('d');
- vc_setFlags('p');
- vc_setFlags('r');
- vc_setFlags('a');
- vc_setFlags('w');
- vc_setFlags('y');
+ vc_setFlags(vc,'n');
+ vc_setFlags(vc,'d');
+ vc_setFlags(vc,'p');
+ vc_setFlags(vc,'r');
+ vc_setFlags(vc,'a');
+ vc_setFlags(vc,'w');
+ vc_setFlags(vc,'y');
//Parameteric Boolean X
Expr X = vc_varExpr1(vc, "X", 0, 0);
int main(int argc, char** argv) {
VC vc = vc_createValidityChecker();
- //vc_setFlags('n');
- //vc_setFlags('d');
- //vc_setFlags('p');
+ //vc_setFlags(vc,'n');
+ //vc_setFlags(vc,'d');
+ //vc_setFlags(vc,'p');
Expr c = vc_parseExpr(vc, argv[1]);
int main() {
for(int j=0;j < 3; j++) {
VC vc = vc_createValidityChecker();
- vc_setFlags('n');
- vc_setFlags('d');
- vc_setFlags('p');
- vc_setFlags('x');
+ vc_setFlags(vc,'n');
+ vc_setFlags(vc,'d');
+ vc_setFlags(vc,'p');
+ vc_setFlags(vc,'x');
Type bv8 = vc_bvType(vc, 8);
Expr a = vc_bvCreateMemoryArray(vc, "a");
int main() {
VC vc = vc_createValidityChecker();
- vc_setFlags('n');
- vc_setFlags('c');
- vc_setFlags('d');
- vc_setFlags('p');
+ vc_setFlags(vc,'n');
+ vc_setFlags(vc,'c');
+ vc_setFlags(vc,'d');
+ vc_setFlags(vc,'p');
Type bv8 = vc_bvType(vc, 8);
int main() {
VC vc = vc_createValidityChecker();
- vc_setFlags('n');
- vc_setFlags('d');
- vc_setFlags('p');
+ vc_setFlags(vc,'n');
+ vc_setFlags(vc,'d');
+ vc_setFlags(vc,'p');
Expr c = vc_parseExpr(vc,"./t.cvc");
int main() {
VC vc = vc_createValidityChecker();
- vc_setFlags('n');
- vc_setFlags('d');
- vc_setFlags('p');
+ vc_setFlags(vc,'n');
+ vc_setFlags(vc,'d');
+ vc_setFlags(vc,'p');
Expr ct_3 = vc_bvConstExprFromStr(vc,
"00000000000000000000000000000011");
int main() {
VC vc = vc_createValidityChecker();
- vc_setFlags('n');
- vc_setFlags('d');
- vc_setFlags('p');
- vc_setFlags('v');
- vc_setFlags('s');
- vc_setFlags('c');
+ vc_setFlags(vc,'n');
+ vc_setFlags(vc,'d');
+ vc_setFlags(vc,'p');
+ vc_setFlags(vc,'v');
+ vc_setFlags(vc,'s');
+ vc_setFlags(vc,'c');
vc_push(vc);
Type bv8 = vc_bvType(vc, 8);
int main() {
VC vc = vc_createValidityChecker();
- vc_setFlags('n');
- vc_setFlags('d');
- vc_setFlags('p');
- //vc_setFlags('v');
- //vc_setFlags('s');
+ vc_setFlags(vc,'n');
+ vc_setFlags(vc,'d');
+ vc_setFlags(vc,'p');
+ //vc_setFlags(vc,'v');
+ //vc_setFlags(vc,'s');
Type bv8 = vc_bvType(vc, 8);
int main() {
VC vc = vc_createValidityChecker();
- vc_setFlags('n');
- vc_setFlags('d');
- vc_setFlags('p');
+ vc_setFlags(vc,'n');
+ vc_setFlags(vc,'d');
+ vc_setFlags(vc,'p');
Type bv8 = vc_bvType(vc, 8);
Expr a = vc_bvCreateMemoryArray(vc, "a");
int main() {
for(int j=0;j < 3; j++) {
VC vc = vc_createValidityChecker();
- vc_setFlags('n');
- vc_setFlags('d');
- vc_setFlags('p');
- vc_setFlags('x');
+ vc_setFlags(vc,'n');
+ vc_setFlags(vc,'d');
+ vc_setFlags(vc,'p');
+ vc_setFlags(vc,'x');
Type bv8 = vc_bvType(vc, 8);
Expr a = vc_bvCreateMemoryArray(vc, "a");
int main() {
VC vc = vc_createValidityChecker();
- vc_setFlags('n');
- vc_setFlags('d');
- //vc_setFlags('p');
+ vc_setFlags(vc,'n');
+ vc_setFlags(vc,'d');
+ //vc_setFlags(vc,'p');
Type bv8 = vc_bvType(vc, 8);
int main() {
VC vc = vc_createValidityChecker();
- vc_setFlags('n');
- vc_setFlags('d');
- //vc_setFlags('p');
+ vc_setFlags(vc,'n');
+ vc_setFlags(vc,'d');
+ //vc_setFlags(vc,'p');
Type bv8 = vc_bvType(vc, 8);
int main() {
VC vc = vc_createValidityChecker();
- vc_setFlags('n');
- vc_setFlags('d');
+ vc_setFlags(vc,'n');
+ vc_setFlags(vc,'d');
// 8-bit variable 'x'
Expr x=vc_varExpr(vc,"x",vc_bvType(vc,8));
int main(int argc, char *argv[]) {
VC vc = vc_createValidityChecker();
- vc_setFlags('n');
- vc_setFlags('d');
- vc_setFlags('p');
+ vc_setFlags(vc,'n');
+ vc_setFlags(vc,'d');
+ vc_setFlags(vc,'p');
Expr nresp1 = vc_varExpr(vc, "nresp1", vc_bv32Type(vc));
Expr packet_get_int0 = vc_varExpr(vc, "packet_get_int0", vc_bv32Type(vc));
int main(int argc, char *argv[]) {
VC vc = vc_createValidityChecker();
- vc_setFlags('n');
- vc_setFlags('d');
- vc_setFlags('p');
+ vc_setFlags(vc,'n');
+ vc_setFlags(vc,'d');
+ vc_setFlags(vc,'p');
Expr nresp1 = vc_varExpr(vc, "nresp1", vc_bv32Type(vc));
Expr packet_get_int0 = vc_varExpr(vc, "packet_get_int0", vc_bv32Type(vc));
projects / francis / stp.git / commitdiff