--- /dev/null
+ # STP (Simple Theorem Prover) top level makefile
+ #
+ # To make in debug mode, type 'make "OPTIMIZE=-g"
+ # To make in optimized mode, type 'make "OPTIMIZE=-O3"
+
+
+include scripts/Makefile.common scripts/config.info
+
+BIN_DIR=$(PREFIX)/bin
+LIB_DIR=$(PREFIX)/lib
+INCLUDE_DIR=$(PREFIX)/include/stp
+
+SRC=src
+BINARIES=bin/stp
+LIBRARIES=lib/libstp.a
+HEADERS=$(SRC)/c_interface/*.h
+
+.PHONY: all
+all:
+ $(MAKE) -C $(SRC)/AST
+ $(MAKE) -C $(SRC)/sat core
+ $(MAKE) -C $(SRC)/simplifier
+ $(MAKE) -C $(SRC)/bitvec
+ $(MAKE) -C $(SRC)/c_interface
+ $(MAKE) -C $(SRC)/constantbv
+ $(MAKE) -C $(SRC)/parser
+ $(AR) rc libstp.a $(SRC)/AST/*.o $(SRC)/sat/*.a $(SRC)/simplifier/*.o $(SRC)/bitvec/*.o $(SRC)/constantbv/*.o \
+ $(SRC)/c_interface/*.o $(SRC)/parser/let-funcs.o $(SRC)/parser/parseCVC.o $(SRC)/parser/lexCVC.o
+ $(RANLIB) libstp.a
+ @mkdir -p lib
+ @mv libstp.a lib/
+ @echo ""
+ @echo "Compilation successful."
+ @echo "Type 'make install' to install STP."
+
+
+.PHONY: install
+install: all
+ @cp -f $(BINARIES) $(BIN_DIR)
+ @cp -f $(LIBRARIES) $(LIB_DIR)
+ @cp -f $(HEADERS) $(INCLUDE_DIR)
+ @echo "STP installed successfully."
+
+.PHONY: clean
+clean:
+ rm -rf *~
+ rm -rf *.a
+ rm -rf lib/*.a
+ rm -rf test/*~
+ rm -rf bin/*~
+ rm -rf bin/stp
+ rm -rf *.log
+ #rm -rf Makefile
+ #rm -rf config.info
+ rm -f TAGS
+ $(MAKE) clean -C $(SRC)/AST
+ $(MAKE) clean -C $(SRC)/sat
+ $(MAKE) clean -C $(SRC)/simplifier
+ $(MAKE) clean -C $(SRC)/bitvec
+ $(MAKE) clean -C $(SRC)/parser
+ $(MAKE) clean -C $(SRC)/c_interface
+ $(MAKE) clean -C $(SRC)/constantbv
+
+# this is make way too difficult because of the recursive Make junk, it
+# should be removed
+TAGS: FORCE
+ find . -name "*.[h]" -or -name "*.cpp" -or -name "*.C" | grep -v SCCS | etags -
+
+FORCE:
+
+# The higher the level, the more tests are run (3 = all)
+REGRESS_LEVEL=4
+REGRESS_TESTS=$(REGRESS_TESTS0)
+REGRESS_LOG = `date +%Y-%m-%d`"-regress.log"
+PROGNAME=bin/stp
+ALL_OPTIONS= -l $(REGRESS_LEVEL) $(PROGNAME) $(REGRESS_TESTS)
+
+.PHONY: regress
+regress:
+ @echo "*********************************************************" \
+ | tee -a $(REGRESS_LOG)
+ @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG)
+ @echo "*********************************************************" \
+ | tee -a $(REGRESS_LOG)
+ scripts/run_cvc_tests.pl $(ALL_OPTIONS) 2>&1 | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ]
+ @echo "*********************************************************" \
+ | tee -a $(REGRESS_LOG)
+ @echo "Output is saved in $(REGRESS_LOG)" | tee -a $(REGRESS_LOG)
+ @echo "*********************************************************" \
+ | tee -a $(REGRESS_LOG)
+
+# The higher the level, the more tests are run (3 = all)
+REGRESS_LEVEL=4
+REGRESS_TESTS=$(REGRESS_TESTS0)
+#REGRESS_LOG = `date +%Y-%m-%d`"-regress-bigarray.log"
+PROGNAME=bin/stp
+ALL_OPTIONS= -l $(REGRESS_LEVEL) $(PROGNAME) $(REGRESS_TESTS)
+
+.PHONY: regressbigarray
+regressbigarray:
+ @echo "*********************************************************" \
+ | tee -a $(REGRESS_LOG)
+ @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG)
+ @echo "*********************************************************" \
+ | tee -a $(REGRESS_LOG)
+ scripts/run_bigarray_tests.pl $(ALL_OPTIONS) 2>&1 | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ]
+ @echo "*********************************************************" \
+ | tee -a $(REGRESS_LOG)
+ @echo "Output is saved in $(REGRESS_LOG)" | tee -a $(REGRESS_LOG)
+ @echo "*********************************************************" \
+ | tee -a $(REGRESS_LOG)
+
+.PHONY: regress_smt
+regress_smt:
+ @echo "*********************************************************" \
+ | tee -a $(REGRESS_LOG)
+ @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG)
+ @echo "*********************************************************" \
+ | tee -a $(REGRESS_LOG)
+ scripts/run_smt_tests.pl $(ALL_OPTIONS) 2>&1 | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ]
+ @echo "*********************************************************" \
+ | tee -a $(REGRESS_LOG)
+ @echo "Output is saved in $(REGRESS_LOG)" | tee -a $(REGRESS_LOG)
+ @echo "*********************************************************" \
+ | tee -a $(REGRESS_LOG)
+
+
+.PHONY: regressall
+regressall:
+ $(MAKE) regress
+
+GRIND_LOG = `date +%Y-%m-%d`"-grind.log"
+GRINDPROG = valgrind --leak-check=full --undef-value-errors=no
+GRIND_TAR = $(BIN_DIR)/stp -d
+GRIND_CALL = -vc "$(GRINDPROG) $(GRIND_TAR)"
+GRIND_OPTIONS = -l $(REGRESS_LEVEL) -rt $(GRIND_CALL) $(REGRESS_TESTS)
+
+
+.PHONY: grind
+grind:
+
+ $(MAKE) install CFLAGS="-ggdb -pg -g"
+ @echo "*********************************************************" \
+ | tee -a $(GRIND_LOG)
+ @echo "Starting tests at" `date` | tee -a $(GRIND_LOG)
+ @echo "*********************************************************" \
+ | tee -a $(GRIND_LOG)
+ scripts/run_cvc_tests.pl $(GRIND_OPTIONS) 2>&1 | tee -a $(GRIND_LOG); [ $${PIPESTATUS[0]} -eq 0 ]
+ @echo "*********************************************************" \
+ | tee -a $(GRIND_LOG)
+ @echo "Output is saved in $(GRIND_LOG)" | tee -a $(GRIND_LOG)
+ @echo "*********************************************************" \
+ | tee -a $(GRIND_LOG)
\ No newline at end of file
.PHONY: all
all:
$(MAKE) -C $(SRC)/AST
- $(MAKE) -C $(SRC)/sat simp
+ $(MAKE) -C $(SRC)/sat core
$(MAKE) -C $(SRC)/simplifier
$(MAKE) -C $(SRC)/bitvec
$(MAKE) -C $(SRC)/c_interface
"lang" => "all",
"stppath" => "stp/bin",
#"vc" => $pwd . "/bin/yices -smt", # Program names
- "vc" => $pwd . "/bin/stp -d -f -m", # Program names
+ "vc" => $pwd . "/bin/stp -d -m", # Program names
#"vc" => "valgrind --leak-check=full /home/vganesh/stp/bin/stp", # Program names
"pfc" => "true",
"stptestpath" => "stp/smt_tests",
# Runtime limit; 0 = no limit
"time" => 60,
# Additional command line options to stp
- "stpOptions" => "-d -f");
+ "stpOptions" => "-d");
# Database of command line options. Initially, they are undefined
my %options = ();
//here
//
//collect statistics on certain functions
-bool stats = false;
+bool stats_flag = false;
//print DAG nodes
-bool print_nodes = false;
-//tentative global var to allow for variable activity optimization
-//in the SAT solver. deprecated.
-bool variable_activity_optimize = false;
+bool print_nodes_flag = false;
//run STP in optimized mode
-bool optimize = true;
+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 = true;
+bool arrayread_refinement_flag = true;
//flag to control write refinement
-bool arraywrite_refinement = true;
+bool arraywrite_refinement_flag = true;
//check the counterexample against the original input to STP
-bool check_counterexample = false;
+bool check_counterexample_flag = false;
//construct the counterexample in terms of original variable based
//on the counterexample returned by SAT solver
-bool construct_counterexample = true;
-bool print_counterexample = false;
-bool print_binary = false;
+bool construct_counterexample_flag = true;
+bool print_counterexample_flag = false;
+bool print_binary_flag = false;
//if this option is true then print the way dawson wants using a
//different printer. do not use this printer.
-bool print_arrayval_declaredorder = false;
+bool print_arrayval_declaredorder_flag = false;
//flag to decide whether to print "valid/invalid" or not
-bool print_output = false;
-//do linear search in the array values of an input array. experimental
-bool linear_search = false;
+bool print_output_flag = false;
//print the variable order chosen by the sat solver while it is
//solving.
-bool print_sat_varorder = false;
+bool print_sat_varorder_flag = false;
//turn on word level bitvector solver
-bool wordlevel_solve = true;
+bool wordlevel_solve_flag = true;
//turn off XOR flattening
-bool xor_flatten = false;
-
-//the smtlib parser has been turned on
-bool smtlib_parser_enable = false;
+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 = false;
+bool print_STPinput_back_flag = false;
enum inputStatus input_status = NOT_DECLARED;
//prints statistics for the ASTNode
void BeevMgr::ASTNodeStats(const char * c, const ASTNode& a)
{
- if (!stats)
+ if (!stats_flag)
return;
StatInfoSet.clear();
//print node size:
cout << endl << "Printing: " << c;
- if (print_nodes)
+ if (print_nodes_flag)
{
//a.PL_Print(cout,0);
//cout << endl;
unsigned char *res;
const char *prefix;
- if(print_binary) {
+ if(print_binary_flag) {
res = CONSTANTBV::BitVector_to_Bin(_bvconst);
if (c_friendly)
{
{
static function_counters s;
- if (stats)
+ if (stats_flag)
{
if (!strcmp(functionname, "print_func_stats"))
//here
//
//collect statistics on certain functions
- extern bool stats;
+ extern bool stats_flag;
//print DAG nodes
- extern bool print_nodes;
- //tentative global var to allow for variable activity optimization
- //in the SAT solver. deprecated.
- extern bool variable_activity_optimize;
+ extern bool print_nodes_flag;
//run STP in optimized mode
- extern bool optimize;
+ 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;
+ extern bool arrayread_refinement_flag;
//switch to control write refinements
- extern bool arraywrite_refinement;
+ extern bool arraywrite_refinement_flag;
//check the counterexample against the original input to STP
- extern bool check_counterexample;
+ 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;
- extern bool print_counterexample;
- extern bool print_binary;
+ extern bool construct_counterexample_flag;
+ extern bool print_counterexample_flag;
+ extern bool print_binary_flag;
//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;
+ extern bool print_arrayval_declaredorder_flag;
//flag to decide whether to print "valid/invalid" or not
- extern bool print_output;
- //do linear search in the array values of an input array. experimental
- extern bool linear_search;
+ extern bool print_output_flag;
//print the variable order chosen by the sat solver while it is
//solving.
- extern bool print_sat_varorder;
+ extern bool print_sat_varorder_flag;
//turn on word level bitvector solver
- extern bool wordlevel_solve;
+ extern bool wordlevel_solve_flag;
//XOR flattening optimizations.
- extern bool xor_flatten;
+ extern bool xor_flatten_flag;
//this flag indicates that the BVSolver() succeeded
- extern bool toplevel_solved;
- //the smtlib parser has been turned on
- extern bool smtlib_parser_enable;
+ extern bool toplevel_solved_flag;
//print the input back
- extern bool print_STPinput_back;
+ extern bool print_STPinput_back_flag;
+ //Flag to switch on the smtlib parser
+ extern bool smtlib_parser_flag;
enum inputStatus
{
ASTVec new_children;
ASTVec flat_children;
- if (xor_flatten)
+ if (xor_flatten_flag)
{
flat_children = FlattenKind(k, children);
}
ASTVec flat_children; // empty vector
ASTVec::const_iterator it_end = children.end();
- if (xor_flatten)
+ if (xor_flatten_flag)
{
flat_children = FlattenKind(XOR, children);
}
ASTNode BBFormula = BBForm(q);
CNFMgr* cm = new CNFMgr(this);
ClauseList* cl = cm->convertToCNF(BBFormula);
- if (stats)
+ if (stats_flag)
cerr << "Number of clauses:" << cl->size() << endl;
//PrintClauseList(cout, *cl);
bool sat = toSATandSolve(newS, *cl);
{
CounterExampleMap.clear();
ConstructCounterExample(newS);
- if (stats && print_nodes)
+ if (stats_flag && print_nodes_flag)
{
PrintSATModel(newS);
}
// counterexample is bogus: flag it
else
{
- if (stats && print_nodes)
+ if (stats_flag && print_nodes_flag)
{
cout << "Supposedly bogus one: \n";
- bool tmp = print_counterexample;
- print_counterexample = true;
+ bool tmp = print_counterexample_flag;
+ print_counterexample_flag = true;
PrintCounterExample(true);
- print_counterexample = tmp;
+ print_counterexample_flag = tmp;
}
return 2;
// GLOBAL FUNCTION: Prints statistics from the MINISAT Solver
void BeevMgr::PrintStats(MINISAT::Solver& s)
{
- if (!stats)
+ if (!stats_flag)
return;
double cpu_time = MINISAT::cpuTime();
uint64_t mem_used = MINISAT::memUsed();
// 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 && print_nodes))
+ if (!(stats_flag && print_nodes_flag))
return;
int num_vars = newS.nVars();
if (!newS.okay())
return;
- if (!construct_counterexample)
+ if (!construct_counterexample_flag)
return;
CopySolverMap_To_CounterExample();
// the flag in order to make it actualy happen!
printf("checking counterexample\n");
- if (!check_counterexample)
+ if (!check_counterexample_flag)
{
return;
}
//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)
+ if (!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)
+ if (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)
+ if (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)
+ if (!print_arrayval_declaredorder_flag)
return;
//t is true if SAT solver generated a counterexample, else it is
q = newq;
newq = CreateSubstitutionMap(newq);
//printf("##################################################\n");
- //ASTNodeStats("after pure substitution: ", newq);
+ ASTNodeStats("after pure substitution: ", newq);
newq = SimplifyFormula_TopLevel(newq, false);
- //ASTNodeStats("after simplification: ", newq);
+ ASTNodeStats("after simplification: ", newq);
newq = bvsolver.TopLevelBVSolve(newq);
- //ASTNodeStats("after solving: ", newq);
+ ASTNodeStats("after solving: ", newq);
} while (q != newq);
ASTNodeStats("Before SimplifyWrites_Inplace begins: ", newq);
{
q = newq;
newq = CreateSubstitutionMap(newq);
- //ASTNodeStats("after pure substitution: ", newq);
+ ASTNodeStats("after pure substitution: ", newq);
newq = SimplifyFormula_TopLevel(newq, false);
- //ASTNodeStats("after simplification: ", newq);
+ ASTNodeStats("after simplification: ", newq);
newq = bvsolver.TopLevelBVSolve(newq);
- //ASTNodeStats("after solving: ", newq);
+ ASTNodeStats("after solving: ", newq);
} while (q != newq);
ASTNodeStats("After SimplifyWrites_Inplace: ", newq);
- start_abstracting = (arraywrite_refinement) ? true : false;
+ start_abstracting = (arraywrite_refinement_flag) ? true : false;
SimplifyWrites_InPlace_Flag = false;
Begin_RemoveWrites = (start_abstracting) ? false : true;
if (start_abstracting)
int res;
//solver instantiated here
- MINISAT::SimpSolver newS;
- if (arrayread_refinement)
+ MINISAT::Solver newS;
+ if (arrayread_refinement_flag)
{
counterexample_checking_during_refinement = true;
}
// all the false axioms each time).
int BeevMgr::SATBased_ArrayReadRefinement(MINISAT::Solver& newS, const ASTNode& q, const ASTNode& orig_input) {
//printf("doing array read refinement\n");
- if (!arrayread_refinement)
+ if (!arrayread_refinement_flag)
FatalError("SATBased_ArrayReadRefinement: Control should not reach here");
ASTVec FalseAxiomsVec, RemainingAxiomsVec;
//This function prints the output of the STP solver
void BeevMgr::PrintOutput(bool true_iff_valid)
{
- //self-explanatory
- if (print_output)
+ if (print_output_flag)
{
- if (smtlib_parser_enable)
+ 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 && (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)
+ if (print_output_flag)
{
- if (smtlib_parser_enable)
+ if (smtlib_parser_flag)
cout << "unsat\n";
else
cout << "Valid.\n";
else
{
ValidFlag = false;
- if (print_output)
+ if (print_output_flag)
{
- if (smtlib_parser_enable)
+ if (smtlib_parser_flag)
cout << "sat\n";
else
cout << "Invalid.\n";
_introduced_symbols.insert(CurrentSymbol);
assert(BVTypeCheck(ite));
- if (arrayread_refinement)
+ if (arrayread_refinement_flag)
{
// ite is really a variable here; it is an ite in the
// else-branch
typedef BEEV::CompleteCounterExample* CompleteCEStar;
BEEV::ASTVec *decls = NULL;
//vector<BEEV::ASTNode *> created_exprs;
-bool cinterface_exprdelete_on = false;
+bool cinterface_exprdelete_on_flag = false;
/* GLOBAL FUNCTION: parser
*/
helpstring += "-c : construct counterexample\n";
helpstring += "-d : check counterexample\n";
helpstring += "-p : print counterexample\n";
+ helpstring += "-y : print counterexample in binary\n";
+ helpstring += "-b : STP input read back\n";
+ helpstring += "-x : flatten nested XORs\n";
helpstring += "-h : help\n";
+ helpstring += "-m : use the SMTLIB parser\n";
switch(c) {
case 'a' :
- BEEV::optimize = false;
- BEEV::wordlevel_solve = false;
+ BEEV::optimize_flag = false;
+ BEEV::wordlevel_solve_flag = false;
break;
case 'b':
- BEEV::print_STPinput_back = true;
+ BEEV::print_STPinput_back_flag = true;
break;
case 'c':
- BEEV::construct_counterexample = true;
+ BEEV::construct_counterexample_flag = true;
break;
case 'd':
- BEEV::construct_counterexample = true;
- BEEV::check_counterexample = true;
- break;
- case 'e':
- BEEV::variable_activity_optimize = true;
- break;
- case 'f':
- BEEV::smtlib_parser_enable = true;
+ BEEV::construct_counterexample_flag = true;
+ BEEV::check_counterexample_flag = true;
break;
case 'h':
cout << helpstring;
BEEV::FatalError("");
break;
- case 'l' :
- BEEV::linear_search = true;
- break;
case 'n':
- BEEV::print_output = true;
+ BEEV::print_output_flag = true;
break;
case 'p':
- BEEV::print_counterexample = true;
+ BEEV::print_counterexample_flag = true;
break;
case 'q':
- BEEV::print_arrayval_declaredorder = true;
+ BEEV::print_arrayval_declaredorder_flag = true;
break;
case 'r':
- BEEV::arrayread_refinement = false;
+ BEEV::arrayread_refinement_flag = false;
break;
case 's' :
- BEEV::stats = true;
+ BEEV::stats_flag = true;
break;
case 'u':
- BEEV::arraywrite_refinement = true;
+ BEEV::arraywrite_refinement_flag = true;
break;
case 'v' :
- BEEV::print_nodes = true;
+ BEEV::print_nodes_flag = true;
break;
case 'w':
- BEEV::wordlevel_solve = false;
+ BEEV::wordlevel_solve_flag = false;
break;
case 'x':
- cinterface_exprdelete_on = true;
+ cinterface_exprdelete_on_flag = true;
break;
case 'z':
- BEEV::print_sat_varorder = true;
+ BEEV::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 BeevMgr
VC vc_createValidityChecker(void) {
vc_setFlags('d');
-#ifdef NATIVE_C_ARITH
-#else
CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot();
if(0 != c) {
cout << CONSTANTBV::BitVector_Error(c) << endl;
return 0;
}
-#endif
bmstar bm = new BEEV::BeevMgr();
decls = new BEEV::ASTVec();
//created_exprs.clear();
// formate the state of the query
std::ostringstream os;
- BEEV::print_counterexample = true;
+ BEEV::print_counterexample_flag = true;
os << "COUNTEREXAMPLE BEGIN: \n";
b->PrintCounterExample(true,os);
os << "COUNTEREXAMPLE END: \n";
void vc_printCounterExample(VC vc) {
bmstar b = (bmstar)vc;
- BEEV::print_counterexample = true;
+ BEEV::print_counterexample_flag = true;
cout << "COUNTEREXAMPLE BEGIN: \n";
b->PrintCounterExample(true);
cout << "COUNTEREXAMPLE END: \n";
void vc_printCounterExampleFile(VC vc, int fd) {
fdostream os(fd);
bmstar b = (bmstar)vc;
- BEEV::print_counterexample = true;
+ BEEV::print_counterexample_flag = true;
os << "COUNTEREXAMPLE BEGIN: \n";
b->PrintCounterExample(true, os);
os << "COUNTEREXAMPLE END: \n";
counterexample : COUNTEREXAMPLE_TOK ';'
{
- BEEV::print_counterexample = true;
+ BEEV::print_counterexample_flag = true;
BEEV::globalBeevMgr_for_parser->PrintCounterExample(true);
}
;
helpstring += "-h : help\n";
helpstring += "-m : use the SMTLIB parser\n";
-
- bool smtlibParser = false;
-
for(int i=1; i < argc;i++) {
if(argv[i][0] == '-') {
switch(argv[i][1]) {
case 'a' :
- BEEV::optimize = false;
- BEEV::wordlevel_solve = false;
+ BEEV::optimize_flag = false;
break;
case 'b':
- BEEV::print_STPinput_back = true;
+ BEEV::print_STPinput_back_flag = true;
break;
case 'c':
- BEEV::construct_counterexample = true;
+ BEEV::construct_counterexample_flag = true;
break;
case 'd':
- BEEV::construct_counterexample = true;
- BEEV::check_counterexample = true;
- break;
- case 'e':
- BEEV::variable_activity_optimize = true;
- break;
- case 'f':
- BEEV::smtlib_parser_enable = true;
+ BEEV::construct_counterexample_flag = true;
+ BEEV::check_counterexample_flag = true;
break;
case 'h':
fprintf(stderr,usage,prog);
//BEEV::FatalError("");
return -1;
break;
- case 'l' :
- BEEV::linear_search = true;
- break;
case 'n':
- BEEV::print_output = true;
+ BEEV::print_output_flag = true;
break;
case 'm':
- smtlibParser=true;
+ BEEV::smtlib_parser_flag=true;
break;
case 'p':
- BEEV::print_counterexample = true;
+ BEEV::print_counterexample_flag = true;
break;
case 'y':
- BEEV::print_binary = true;
+ BEEV::print_binary_flag = true;
break;
case 'q':
- BEEV::print_arrayval_declaredorder = true;
+ BEEV::print_arrayval_declaredorder_flag = true;
break;
case 'r':
- BEEV::arrayread_refinement = false;
+ BEEV::arrayread_refinement_flag = false;
break;
case 's' :
- BEEV::stats = true;
+ BEEV::stats_flag = true;
break;
case 'u':
- BEEV::arraywrite_refinement = false;
+ BEEV::arraywrite_refinement_flag = false;
break;
case 'v' :
- BEEV::print_nodes = true;
+ BEEV::print_nodes_flag = true;
break;
case 'w':
- BEEV::wordlevel_solve = false;
+ BEEV::wordlevel_solve_flag = false;
break;
case 'x':
- BEEV::xor_flatten = true;
+ BEEV::xor_flatten_flag = true;
break;
case 'z':
- BEEV::print_sat_varorder = true;
+ BEEV::print_sat_varorder_flag = true;
break;
default:
fprintf(stderr,usage,prog);
} else {
infile = argv[i];
- if (smtlibParser)
+ if (BEEV::smtlib_parser_flag)
{
smtin = fopen(infile,"r");
if(smtin == NULL)
}
}
-#ifdef NATIVE_C_ARITH
-#else
CONSTANTBV::ErrCode c = CONSTANTBV::BitVector_Boot();
if(0 != c) {
cout << CONSTANTBV::BitVector_Error(c) << endl;
return 0;
}
-#endif
//want to print the output always from the commandline.
- BEEV::print_output = true;
+ BEEV::print_output_flag = true;
BEEV::globalBeevMgr_for_parser = new BEEV::BeevMgr();
BEEV::SingleBitOne = BEEV::globalBeevMgr_for_parser->CreateOneConst(1);
BEEV::SingleBitZero = BEEV::globalBeevMgr_for_parser->CreateZeroConst(1);
- //BEEV::smtlib_parser_enable = true;
-
- if (smtlibParser)
+
+ if (BEEV::smtlib_parser_flag)
smtparse();
else
cvcparse();
{
ASTNode eq = input;
//cerr << "Input to BVSolve_Odd()" << eq << endl;
- if (!(wordlevel_solve && EQ == eq.GetKind()))
+ if (!(wordlevel_solve_flag && EQ == eq.GetKind()))
{
return input;
}
output = ASTTrue;
break;
}
+// case READ:
+// {
+// if(BVCONST != lhs[1].GetKind() || READ != rhs.GetKind() ||
+// BVCONST != rhs[1].GetKind() || lhs == rhs)
+// {
+// return eq;
+// }
+// else
+// {
+// DoNotSolve_TheseVars.insert(lhs);
+// if (!_bm->UpdateSolverMap(lhs, rhs))
+// {
+// return eq;
+// }
+
+// output = ASTTrue;
+// break;
+// }
+// }
case BVEXTRACT:
{
ASTNode zero = _bm->CreateZeroConst(32);
- if (!(SYMBOL == lhs[0].GetKind() && BVCONST == lhs[1].GetKind() && zero == lhs[2] && !_bm->VarSeenInTerm(lhs[0], rhs) && !DoNotSolveThis(
- lhs[0])))
+ if (!(SYMBOL == lhs[0].GetKind() && BVCONST == lhs[1].GetKind() &&
+ zero == lhs[2] && !_bm->VarSeenInTerm(lhs[0], rhs) && !DoNotSolveThis(lhs[0])))
{
return eq;
}
//the formula
ASTNode BVSolver::TopLevelBVSolve(const ASTNode& input)
{
- if (!wordlevel_solve)
+ if (!wordlevel_solve_flag)
{
return input;
}
ASTNode solved = ASTFalse;
for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
{
- //_bm->ASTNodeStats("Printing before calling simplifyformula inside the solver:", *it);
- ASTNode aaa = (ASTTrue == solved && EQ == it->GetKind()) ? _bm->SimplifyFormula(*it, false) : *it;
- //ASTNode aaa = *it;
+ //_bm->ASTNodeStats("Printing before calling simplifyformula inside the solver:", *it);
+ ASTNode aaa = (ASTTrue == solved && EQ == it->GetKind()) ? _bm->SimplifyFormula(*it, false) : *it;
//_bm->ASTNodeStats("Printing after calling simplifyformula inside the solver:", aaa);
aaa = BVSolve_Odd(aaa);
//_bm->ASTNodeStats("Printing after oddsolver:", aaa);
{
ASTNode eq = input;
//cerr << "Input to BVSolve_Odd()" << eq << endl;
- if (!(wordlevel_solve && EQ == eq.GetKind()))
+ if (!(wordlevel_solve_flag && EQ == eq.GetKind()))
{
evenflag = false;
return eq;
//solve an eqn whose monomials have only even coefficients
ASTNode BVSolver::BVSolve_Even(const ASTNode& input)
{
- if (!wordlevel_solve)
+ if (!wordlevel_solve_flag)
{
return input;
}
//a is of the form READ(Arr,const), and b is const, or
//a is of the form var, and b is const
- if ((k1 == READ && a[0].GetKind() == SYMBOL && a[1].GetKind() == BVCONST) && (k2 == BVCONST))
+ if ((k1 == READ && a[0].GetKind() == SYMBOL && a[1].GetKind() == BVCONST &&
+ (k2 == BVCONST)))
+ // ||
+// k2 == READ && b[0].GetKind() == SYMBOL && b[1].GetKind() == BVCONST)))
return 1;
if (SYMBOL == k1 && (BVCONST == k2 || TRUE == k2 || FALSE == k2))
ASTNode BeevMgr::SimplifyFormula(const ASTNode& b, bool pushNeg)
{
- if (!optimize)
+ if (!optimize_flag)
return b;
Kind kind = b.GetKind();
ASTNode BeevMgr::SimplifyAtomicFormula(const ASTNode& a, bool pushNeg)
{
- if (!optimize)
+ if (!optimize_flag)
{
return a;
}
{
CountersAndStats("ITEOpts_InEqs");
- if (!(EQ == in.GetKind() && optimize))
+ if (!(EQ == in.GetKind() && optimize_flag))
{
return in;
}
Kind k1 = in1.GetKind();
Kind k2 = in2.GetKind();
- if (!optimize)
+ if (!optimize_flag)
{
return CreateNode(EQ, in1, in2);
}
ASTNode t1 = in1;
ASTNode t2 = in2;
CountersAndStats("CreateSimplifiedITE");
- if (!optimize)
+ if (!optimize_flag)
{
if (t1.GetValueWidth() != t2.GetValueWidth())
{
ASTNode t2 = in2;
CountersAndStats("CreateSimplifiedFormulaITE");
- if (optimize)
+ if (optimize_flag)
{
if (t0 == ASTTrue)
return t1;
ASTNode BeevMgr::SimplifyIteFormula(const ASTNode& b, bool pushNeg)
{
- if (!optimize)
+ if (!optimize_flag)
return b;
ASTNode output;
ASTNode inputterm(actualInputterm); // mutable local copy.
//cout << "SimplifyTerm: input: " << a << endl;
- if (!optimize)
+ if (!optimize_flag)
{
return inputterm;
}
ASTNode BeevMgr::SimplifyTermAux(const ASTNode& inputterm)
{
//cout << "SimplifyTerm: input: " << a << endl;
- if (!optimize)
+ if (!optimize_flag)
{
return inputterm;
}
//########################################
//########################################
- if (wordlevel_solve && CheckSolverMap(inputterm, output))
+ if (wordlevel_solve_flag && CheckSolverMap(inputterm, output))
{
return SimplifyTermAux(output);
}
//The big substitution function
ASTNode BeevMgr::CreateSubstitutionMap(const ASTNode& a)
{
- if (!optimize)
- return a;
+ if (!wordlevel_solve_flag)
+ return a;
ASTNode output = a;
//if the variable has been solved for, then simply return it
SortByArith(c);
FillUp_ArrReadIndex_Vec(c[0], c[1]);
- if (SYMBOL == c[0].GetKind() && VarSeenInTerm(c[0], SimplifyTermAux(c[1])))
+ ASTNode c1 = SimplifyTermAux(c[1]);
+ if (SYMBOL == c[0].GetKind() && VarSeenInTerm(c[0], c1))
{
return a;
}
- if (1 == TermOrder(c[0], c[1]) && READ == c[0].GetKind() && VarSeenInTerm(c[0][0], SimplifyTermAux(c[1])))
+ if (1 == TermOrder(c[0], c[1]) && READ == c[0].GetKind() && VarSeenInTerm(c[0][1], c1))
{
return a;
}
- bool updated = UpdateSubstitutionMap(c[0], SimplifyTermAux(c[1]));
+ bool updated = UpdateSubstitutionMap(c[0], c1);
output = updated ? ASTTrue : a;
return output;
}
projects / francis / stp.git / commitdiff