diff options
Diffstat (limited to 'stp/AST/ToSAT.cpp')
| -rw-r--r-- | stp/AST/ToSAT.cpp | 1385 |
1 files changed, 1385 insertions, 0 deletions
diff --git a/stp/AST/ToSAT.cpp b/stp/AST/ToSAT.cpp new file mode 100644 index 00000000..7a164c9c --- /dev/null +++ b/stp/AST/ToSAT.cpp @@ -0,0 +1,1385 @@ +/******************************************************************** + * AUTHORS: Vijay Ganesh, David L. Dill + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +// -*- c++ -*- +#include "AST.h" +#include "ASTUtil.h" +#include "../simplifier/bvsolver.h" +#include <math.h> + + +namespace BEEV { + /* FUNCTION: lookup or create a new MINISAT literal + * lookup or create new MINISAT Vars from the global MAP + * _ASTNode_to_SATVar. + */ + const MINISAT::Var BeevMgr::LookupOrCreateSATVar(MINISAT::Solver& newS, const ASTNode& n) { + ASTtoSATMap::iterator it; + MINISAT::Var v; + + //look for the symbol in the global map from ASTNodes to ints. if + //not found, create a S.newVar(), else use the existing one. + if((it = _ASTNode_to_SATVar.find(n)) == _ASTNode_to_SATVar.end()) { + v = newS.newVar(); + _ASTNode_to_SATVar[n] = v; + + //ASSUMPTION: I am assuming that the newS.newVar() call increments v + //by 1 each time it is called, and the initial value of a + //MINISAT::Var is 0. + _SATVar_to_AST.push_back(n); + } + else + v = it->second; + return v; + } + + /* 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 + * unsat. else continue. + */ + // FIXME: Still need to deal with TRUE/FALSE in clauses! + bool BeevMgr::toSATandSolve(MINISAT::Solver& newS, BeevMgr::ClauseList& cll) + { + CountersAndStats("SAT Solver"); + + //iterate through the list (conjunction) of ASTclauses cll + BeevMgr::ClauseList::const_iterator i = cll.begin(), iend = cll.end(); + + if(i == iend) + FatalError("toSATandSolve: Nothing to Solve",ASTUndefined); + + //turnOffSubsumption + newS.turnOffSubsumption(); + + // (*i) is an ASTVec-ptr which denotes an ASTclause + for(; i!=iend; i++) { + //Clause for the SATSolver + MINISAT::vec<MINISAT::Lit> satSolverClause; + + //now iterate through the internals of the ASTclause itself + ASTVec::const_iterator j = (*i)->begin(), jend = (*i)->end(); + //j is a disjunct in the ASTclause (*i) + for(;j!=jend;j++) { + + bool negate = (NOT == j->GetKind()) ? true : false; + ASTNode n = negate ? (*j)[0] : *j; + + //Lookup or create the MINISAT::Var corresponding to the Booelan + //ASTNode Variable, and push into sat Solver clause + MINISAT::Var v = LookupOrCreateSATVar(newS,n); + MINISAT::Lit l(v, negate); + satSolverClause.push(l); + } + newS.addClause(satSolverClause); + // clause printing. + // (printClause<MINISAT::vec<MINISAT::Lit> >)(satSolverClause); + // cout << " 0 "; + // cout << endl; + + if(newS.okay()) { + continue; + } + else { + PrintStats(newS.stats); + return false; + } + + if(!newS.simplifyDB(false)) { + PrintStats(newS.stats); + return false; + } + } + + // if input is UNSAT return false, else return true + if(!newS.simplifyDB(false)) { + PrintStats(newS.stats); + return false; + } + + //PrintActivityLevels_Of_SATVars("Before SAT:",newS); + //ChangeActivityLevels_Of_SATVars(newS); + //PrintActivityLevels_Of_SATVars("Before SAT and after initial bias:",newS); + newS.solve(); + //PrintActivityLevels_Of_SATVars("After SAT",newS); + + PrintStats(newS.stats); + if (newS.okay()) + return true; + else + return false; + } + + // GLOBAL FUNCTION: Prints statistics from the MINISAT Solver + void BeevMgr::PrintStats(MINISAT::SolverStats& s) { + if(!stats) + return; + double cpu_time = MINISAT::cpuTime(); + MINISAT::int64 mem_used = MINISAT::memUsed(); + reportf("restarts : %"I64_fmt"\n", s.starts); + reportf("conflicts : %-12"I64_fmt" (%.0f /sec)\n", s.conflicts , s.conflicts /cpu_time); + reportf("decisions : %-12"I64_fmt" (%.0f /sec)\n", s.decisions , s.decisions /cpu_time); + reportf("propagations : %-12"I64_fmt" (%.0f /sec)\n", s.propagations, s.propagations/cpu_time); + reportf("conflict literals : %-12"I64_fmt" (%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 && print_nodes)) + 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; + } + } + } + + + // Looks up truth value of ASTNode SYMBOL in MINISAT satisfying assignment. + // Returns ASTTrue if true, ASTFalse if false or undefined. + ASTNode BeevMgr::SymbolTruthValue(MINISAT::Solver &newS, ASTNode form) + { + MINISAT::Var satvar = _ASTNode_to_SATVar[form]; + if (newS.model[satvar] == MINISAT::l_True) { + return ASTTrue; + } + else if (newS.model[satvar] == MINISAT::l_False){ + // False + return ASTFalse; + } + else { + return (rand() > 4096) ? ASTTrue : ASTFalse; + } + } + + + // This function is for debugging problems with BitBlast and especially + // ToCNF. It evaluates the bit-blasted formula in the satisfying + // assignment. While doing that, it checks that every subformula has + // the same truth value as its representative literal, if it has one. + // If this condition is violated, it halts immediately (on the leftmost + // lowest term). + // Use CreateSimpForm to evaluate, even though it's expensive, so that + // we can use the partial truth assignment. + ASTNode BeevMgr::CheckBBandCNF(MINISAT::Solver& newS, ASTNode form) + { + // Clear memo table (in case newS has changed). + CheckBBandCNFMemo.clear(); + // Call recursive version that does the work. + return CheckBBandCNF_int(newS, form); + } + + // Recursive body CheckBBandCNF + // FIXME: Modify this to just check if result is true, and print mismatch + // if not. Might have a trace flag for the other stuff. + ASTNode BeevMgr::CheckBBandCNF_int(MINISAT::Solver& newS, ASTNode form) + { + + // cout << "++++++++++++++++" << endl << "CheckBBandCNF_int form = " << + // form << endl; + + ASTNodeMap::iterator memoit = CheckBBandCNFMemo.find(form); + if (memoit != CheckBBandCNFMemo.end()) { + // found it. Return memoized value. + return memoit->second; + } + + ASTNode result; // return value, to memoize. + + Kind k = form.GetKind(); + switch (k) { + case TRUE: + case FALSE: { + return form; + break; + } + case SYMBOL: + case BVGETBIT: { + // Look up the truth value + // ASTNode -> Sat -> Truthvalue -> ASTTrue or ASTFalse; + // FIXME: Could make up a fresh var in undefined case. + + result = SymbolTruthValue(newS, form); + + cout << "================" << endl << "Checking BB formula:" << form << endl; + cout << "----------------" << endl << "Result:" << result << endl; + + break; + } + default: { + // Evaluate the children recursively. + ASTVec eval_children; + ASTVec ch = form.GetChildren(); + ASTVec::iterator itend = ch.end(); + for(ASTVec::iterator it = ch.begin(); it < itend; it++) { + eval_children.push_back(CheckBBandCNF_int(newS, *it)); + } + result = CreateSimpForm(k, eval_children); + + cout << "================" << endl << "Checking BB formula:" << form << endl; + cout << "----------------" << endl << "Result:" << result << endl; + + ASTNode replit_eval; + // Compare with replit, if there is one. + ASTNodeMap::iterator replit_it = RepLitMap.find(form); + if (replit_it != RepLitMap.end()) { + ASTNode replit = RepLitMap[form]; + // Replit is symbol or not symbol. + if (SYMBOL == replit.GetKind()) { + replit_eval = SymbolTruthValue(newS, replit); + } + else { + // It's (NOT sym). Get value of sym and complement. + replit_eval = CreateSimpNot(SymbolTruthValue(newS, replit[0])); + } + + cout << "----------------" << endl << "Rep lit: " << replit << endl; + cout << "----------------" << endl << "Rep lit value: " << replit_eval << endl; + + if (result != replit_eval) { + // Hit the panic button. + FatalError("Truth value of BitBlasted formula disagrees with representative literal in CNF."); + } + } + else { + cout << "----------------" << endl << "No rep lit" << endl; + } + + } + } + + return (CheckBBandCNFMemo[form] = result); + } + + /*FUNCTION: constructs counterexample from MINISAT counterexample + * step1 : iterate through MINISAT counterexample and assemble the + * bits for each AST term. Store it in a map from ASTNode to vector + * of bools (bits). + * + * step2: Iterate over the map from ASTNodes->Vector-of-Bools and + * populate the CounterExampleMap data structure (ASTNode -> BVConst) + */ + void BeevMgr::ConstructCounterExample(MINISAT::Solver& newS) { + //iterate over MINISAT counterexample and construct a map from AST + //terms to vector of bools. We need this iteration step because + //MINISAT might return the various bits of a term out of + //order. Therfore, we need to collect all the bits and assemble + //them properly + + if(!newS.okay()) + return; + if(!construct_counterexample) + return; + + CopySolverMap_To_CounterExample(); + for (int i = 0; i < newS.nVars(); i++) { + //Make sure that the MINISAT::Var is defined + if (newS.model[i] != MINISAT::l_Undef) { + + //mapping from MINISAT::Vars to ASTNodes. We do not need to + //print MINISAT vars or CNF vars. + ASTNode s = _SATVar_to_AST[i]; + + //assemble the counterexample here + if(s.GetKind() == BVGETBIT && s[0].GetKind() == SYMBOL) { + ASTNode symbol = s[0]; + unsigned int symbolWidth = symbol.GetValueWidth(); + + //'v' is the map from bit-index to bit-value + hash_map<unsigned,bool> * v; + if(_ASTNode_to_Bitvector.find(symbol) == _ASTNode_to_Bitvector.end()) + _ASTNode_to_Bitvector[symbol] = new hash_map<unsigned,bool>(symbolWidth); + + //v holds the map from bit-index to bit-value + v = _ASTNode_to_Bitvector[symbol]; + + //kk is the index of BVGETBIT + unsigned int kk = GetUnsignedConst(s[1]); + + //Collect the bits of 'symbol' and store in v. Store in reverse order. + if(newS.model[i]==MINISAT::l_True) + (*v)[(symbolWidth-1) - kk] = true; + else + (*v)[(symbolWidth-1) - kk] = false; + } + else { + if(s.GetKind() == SYMBOL && s.GetType() == BOOLEAN_TYPE) { + const char * zz = s.GetName(); + //if the variables are not cnf variables then add them to the counterexample + if(0 != strncmp("cnf",zz,3) && 0 != strcmp("*TrueDummy*",zz)) { + if(newS.model[i]==MINISAT::l_True) + CounterExampleMap[s] = ASTTrue; + else + CounterExampleMap[s] = ASTFalse; + } + } + } + } + } + + //iterate over the ASTNode_to_Bitvector data-struct and construct + //the the aggregate value of the bitvector, and populate the + //CounterExampleMap datastructure + for(ASTtoBitvectorMap::iterator it=_ASTNode_to_Bitvector.begin(),itend=_ASTNode_to_Bitvector.end(); + it!=itend;it++) { + ASTNode var = it->first; + //debugging + //cerr << var; + if(SYMBOL != var.GetKind()) + FatalError("ConstructCounterExample: error while constructing counterexample: not a variable: ",var); + + //construct the bitvector value + hash_map<unsigned,bool> * w = it->second; + ASTNode value = BoolVectoBVConst(w, var.GetValueWidth()); + //debugging + //cerr << value; + + //populate the counterexample datastructure. add only scalars + //variables which were declared in the input and newly + //introduced variables for array reads + CounterExampleMap[var] = value; + } + + //In this loop, we compute the value of each array read, the + //corresponding ITE against the counterexample generated above. + for(ASTNodeMap::iterator it=_arrayread_ite.begin(),itend=_arrayread_ite.end(); + it!=itend;it++){ + //the array read + ASTNode arrayread = it->first; + ASTNode value_ite = _arrayread_ite[arrayread]; + + //convert it to a constant array-read and store it in the + //counter-example. First convert the index into a constant. then + //construct the appropriate array-read and store it in the + //counterexample + ASTNode arrayread_index = TermToConstTermUsingModel(arrayread[1]); + ASTNode key = CreateTerm(READ,arrayread.GetValueWidth(),arrayread[0],arrayread_index); + + //Get the ITE corresponding to the array-read and convert it + //to a constant against the model + ASTNode value = TermToConstTermUsingModel(value_ite); + //save the result in the counter_example + if(!CheckSubstitutionMap(key)) + CounterExampleMap[key] = value; + } + } //End of ConstructCounterExample + + // FUNCTION: accepts a non-constant term, and returns the + // corresponding constant term with respect to a model. + // + // term READ(A,i) is treated as follows: + // + //1. If (the boolean variable 'ArrayReadFlag' is true && ArrayRead + //1. has value in counterexample), then return the value of the + //1. arrayread. + // + //2. If (the boolean variable 'ArrayReadFlag' is true && ArrayRead + //2. doesn't have value in counterexample), then return the + //2. arrayread itself (normalized such that arrayread has a constant + //2. index) + // + //3. If (the boolean variable 'ArrayReadFlag' is false) && ArrayRead + //3. has a value in the counterexample then return the value of the + //3. arrayread. + // + //4. If (the boolean variable 'ArrayReadFlag' is false) && ArrayRead + //4. doesn't have a value in the counterexample then return 0 as the + //4. value of the arrayread. + ASTNode BeevMgr::TermToConstTermUsingModel(const ASTNode& t, bool ArrayReadFlag) { + Begin_RemoveWrites = false; + SimplifyWrites_InPlace_Flag = false; + //ASTNode term = SimplifyTerm(t); + ASTNode term = t; + Kind k = term.GetKind(); + + + //cerr << "Input to TermToConstTermUsingModel: " << term << endl; + if(!is_Term_kind(k)) { + FatalError("TermToConstTermUsingModel: The input is not a term: ",term); + } + if(k == WRITE) { + FatalError("TermToConstTermUsingModel: The input has wrong kind: WRITE : ",term); + } + if(k == SYMBOL && BOOLEAN_TYPE == term.GetType()) { + FatalError("TermToConstTermUsingModel: The input has wrong kind: Propositional variable : ",term); + } + + ASTNodeMap::iterator it1; + if((it1 = CounterExampleMap.find(term)) != CounterExampleMap.end()) { + ASTNode val = it1->second; + if(BVCONST != val.GetKind()) { + //CounterExampleMap has two maps rolled into + //one. SubstitutionMap and SolverMap. + // + //recursion is fine here. There are two maps that are checked + //here. One is the substitutionmap. We garuntee that the value + //of a key in the substitutionmap is always a constant. + // + //in the SolverMap we garuntee that "term" does not occur in + //the value part of the map + if(term == val) { + FatalError("TermToConstTermUsingModel: The input term is stored as-is " + "in the CounterExample: Not ok: ",term); + } + return TermToConstTermUsingModel(val,ArrayReadFlag); + } + else { + return val; + } + } + + ASTNode output; + switch(k) { + case BVCONST: + output = term; + break; + case SYMBOL: { + if(term.GetType() == ARRAY_TYPE) { + return term; + } + + //when all else fails set symbol values to some constant by + //default. if the variable is queried the second time then add 1 + //to and return the new value. + ASTNode zero = CreateZeroConst(term.GetValueWidth()); + output = zero; + break; + } + case READ: { + ASTNode arrName = term[0]; + ASTNode index = term[1]; + if(0 == arrName.GetIndexWidth()) { + FatalError("TermToConstTermUsingModel: array has 0 index width: ",arrName); + } + + //READ over a WRITE + if(WRITE == arrName.GetKind()) { + ASTNode wrtterm = Expand_ReadOverWrite_UsingModel(term, ArrayReadFlag); + if(wrtterm == term) { + FatalError("TermToConstTermUsingModel: Read_Over_Write term must be expanded into an ITE", term); + } + ASTNode rtterm = TermToConstTermUsingModel(wrtterm,ArrayReadFlag); + return rtterm; + } + //READ over an ITE + if(ITE == arrName.GetKind()) { + arrName = TermToConstTermUsingModel(arrName,ArrayReadFlag); + } + + ASTNode modelentry; + if(CounterExampleMap.find(index) != CounterExampleMap.end()) { + //index has a const value in the CounterExampleMap + ASTNode indexVal = CounterExampleMap[index]; + modelentry = CreateTerm(READ, arrName.GetValueWidth(), arrName, indexVal); + } + else { + //index does not have a const value in the CounterExampleMap. compute it. + ASTNode indexconstval = TermToConstTermUsingModel(index,ArrayReadFlag); + //update model with value of the index + //CounterExampleMap[index] = indexconstval; + modelentry = CreateTerm(READ,arrName.GetValueWidth(), arrName,indexconstval); + } + //modelentry is now an arrayread over a constant index + BVTypeCheck(modelentry); + + //if a value exists in the CounterExampleMap then return it + if(CounterExampleMap.find(modelentry) != CounterExampleMap.end()) { + output = TermToConstTermUsingModel(CounterExampleMap[modelentry],ArrayReadFlag); + } + else if(ArrayReadFlag) { + //return the array read over a constantindex + output = modelentry; + } + else { + //when all else fails set symbol values to some constant by + //default. if the variable is queried the second time then add 1 + //to and return the new value. + ASTNode zero = CreateZeroConst(modelentry.GetValueWidth()); + output = zero; + } + break; + } + case ITE: { + ASTNode condcompute = ComputeFormulaUsingModel(term[0]); + if(ASTTrue == condcompute) { + output = TermToConstTermUsingModel(term[1],ArrayReadFlag); + } + else if(ASTFalse == condcompute) { + output = TermToConstTermUsingModel(term[2],ArrayReadFlag); + } + else { + cerr << "TermToConstTermUsingModel: termITE: value of conditional is wrong: " << condcompute << endl; + FatalError(" TermToConstTermUsingModel: termITE: cannot compute ITE conditional against model: ",term); + } + break; + } + default: { + ASTVec c = term.GetChildren(); + ASTVec o; + for(ASTVec::iterator it=c.begin(),itend=c.end();it!=itend;it++) { + ASTNode ff = TermToConstTermUsingModel(*it,ArrayReadFlag); + o.push_back(ff); + } + output = CreateTerm(k,term.GetValueWidth(),o); + //output is a CONST expression. compute its value and store it + //in the CounterExampleMap + ASTNode oo = BVConstEvaluator(output); + //the return value + output = oo; + break; + } + } + + //when this flag is false, we should compute the arrayread to a + //constant. this constant is stored in the counter_example + //datastructure + if(!ArrayReadFlag) { + CounterExampleMap[term] = output; + } + + //cerr << "Output to TermToConstTermUsingModel: " << output << endl; + return output; + } //End of TermToConstTermUsingModel + + //Expands read-over-write by evaluating (readIndex=writeIndex) for + //every writeindex until, either it evaluates to TRUE or all + //(readIndex=writeIndex) evaluate to FALSE + ASTNode BeevMgr::Expand_ReadOverWrite_UsingModel(const ASTNode& term, bool arrayread_flag) { + if(READ != term.GetKind() && + WRITE != term[0].GetKind()) { + FatalError("RemovesWrites: Input must be a READ over a WRITE",term); + } + + ASTNode output; + ASTNodeMap::iterator it1; + if((it1 = CounterExampleMap.find(term)) != CounterExampleMap.end()) { + ASTNode val = it1->second; + if(BVCONST != val.GetKind()) { + //recursion is fine here. There are two maps that are checked + //here. One is the substitutionmap. We garuntee that the value + //of a key in the substitutionmap is always a constant. + if(term == val) { + FatalError("TermToConstTermUsingModel: The input term is stored as-is " + "in the CounterExample: Not ok: ",term); + } + return TermToConstTermUsingModel(val,arrayread_flag); + } + else { + return val; + } + } + + unsigned int width = term.GetValueWidth(); + ASTNode writeA = ASTTrue; + ASTNode newRead = term; + ASTNode readIndex = TermToConstTermUsingModel(newRead[1],false); + //iteratively expand read-over-write, and evaluate against the + //model at every iteration + do { + ASTNode write = newRead[0]; + writeA = write[0]; + ASTNode writeIndex = TermToConstTermUsingModel(write[1],false); + ASTNode writeVal = TermToConstTermUsingModel(write[2],false); + + ASTNode cond = ComputeFormulaUsingModel(CreateSimplifiedEQ(writeIndex,readIndex)); + if(ASTTrue == cond) { + //found the write-value. return it + output = writeVal; + CounterExampleMap[term] = output; + return output; + } + + newRead = CreateTerm(READ,width,writeA,readIndex); + } while(READ == newRead.GetKind() && WRITE == newRead[0].GetKind()); + + output = TermToConstTermUsingModel(newRead,arrayread_flag); + + //memoize + CounterExampleMap[term] = output; + return output; + } //Exand_ReadOverWrite_To_ITE_UsingModel() + + /* FUNCTION: accepts a non-constant formula, and checks if the + * formula is ASTTrue or ASTFalse w.r.t to a model + */ + ASTNode BeevMgr::ComputeFormulaUsingModel(const ASTNode& form) { + ASTNode in = form; + Kind k = form.GetKind(); + if(!(is_Form_kind(k) && BOOLEAN_TYPE == form.GetType())) { + FatalError(" ComputeConstFormUsingModel: The input is a non-formula: ", form); + } + + //cerr << "Input to ComputeFormulaUsingModel:" << form << endl; + ASTNodeMap::iterator it1; + if((it1 = ComputeFormulaMap.find(form)) != ComputeFormulaMap.end()) { + ASTNode res = it1->second; + if(ASTTrue == res || ASTFalse == res) { + return res; + } + else { + FatalError("ComputeFormulaUsingModel: The value of a formula must be TRUE or FALSE:", form); + } + } + + ASTNode t0,t1; + ASTNode output = ASTFalse; + switch(k) { + case TRUE: + case FALSE: + output = form; + break; + case SYMBOL: + if(BOOLEAN_TYPE != form.GetType()) + FatalError(" ComputeFormulaUsingModel: Non-Boolean variables are not formulas",form); + if(CounterExampleMap.find(form) != CounterExampleMap.end()) { + ASTNode counterexample_val = CounterExampleMap[form]; + if(!VarSeenInTerm(form,counterexample_val)) { + output = ComputeFormulaUsingModel(counterexample_val); + } + else { + output = counterexample_val; + } + } + else + output = ASTFalse; + break; + case EQ: + case NEQ: + case BVLT: + case BVLE: + case BVGT: + case BVGE: + case BVSLT: + case BVSLE: + case BVSGT: + case BVSGE: + //convert form[0] into a constant term + t0 = TermToConstTermUsingModel(form[0],false); + //convert form[0] into a constant term + t1 = TermToConstTermUsingModel(form[1],false); + output = BVConstEvaluator(CreateNode(k,t0,t1)); + + //evaluate formula to false if bvdiv execption occurs while + //counterexample is being checked during refinement. + if(bvdiv_exception_occured && + counterexample_checking_during_refinement) { + output = ASTFalse; + } + break; + case NAND: { + ASTNode o = ASTTrue; + for(ASTVec::const_iterator it=form.begin(),itend=form.end();it!=itend;it++) + if(ASTFalse == ComputeFormulaUsingModel(*it)) { + o = ASTFalse; + break; + } + if(o == ASTTrue) + output = ASTFalse; + else + output = ASTTrue; + break; + } + case NOR: { + ASTNode o = ASTFalse; + for(ASTVec::const_iterator it=form.begin(),itend=form.end();it!=itend;it++) + if(ASTTrue == ComputeFormulaUsingModel(*it)) { + o = ASTTrue; + break; + } + if(o == ASTTrue) + output = ASTFalse; + else + output = ASTTrue; + break; + } + case NOT: + if(ASTTrue == ComputeFormulaUsingModel(form[0])) + output = ASTFalse; + else + output = ASTTrue; + break; + case OR: + for(ASTVec::const_iterator it=form.begin(),itend=form.end();it!=itend;it++) + if(ASTTrue == ComputeFormulaUsingModel(*it)) + output = ASTTrue; + break; + case AND: + output = ASTTrue; + for(ASTVec::const_iterator it=form.begin(),itend=form.end();it!=itend;it++) { + if(ASTFalse == ComputeFormulaUsingModel(*it)) { + output = ASTFalse; + break; + } + } + break; + case XOR: + t0 = ComputeFormulaUsingModel(form[0]); + t1 = ComputeFormulaUsingModel(form[1]); + if((ASTTrue == t0 && ASTTrue == t1) || (ASTFalse == t0 && ASTFalse == t1)) + output = ASTFalse; + else + output = ASTTrue; + break; + case IFF: + t0 = ComputeFormulaUsingModel(form[0]); + t1 = ComputeFormulaUsingModel(form[1]); + if((ASTTrue == t0 && ASTTrue == t1) || (ASTFalse == t0 && ASTFalse == t1)) + output = ASTTrue; + else + output = ASTFalse; + break; + case IMPLIES: + t0 = ComputeFormulaUsingModel(form[0]); + t1 = ComputeFormulaUsingModel(form[1]); + if((ASTFalse == t0) || (ASTTrue == t0 && ASTTrue == t1)) + output = ASTTrue; + else + output = ASTFalse; + break; + case ITE: + t0 = ComputeFormulaUsingModel(form[0]); + if(ASTTrue == t0) + output = ComputeFormulaUsingModel(form[1]); + else if(ASTFalse == t0) + output = ComputeFormulaUsingModel(form[2]); + else + FatalError("ComputeFormulaUsingModel: ITE: something is wrong with the formula: ",form); + break; + default: + FatalError(" ComputeFormulaUsingModel: the kind has not been implemented", ASTUndefined); + break; + } + + //cout << "ComputeFormulaUsingModel output is:" << output << endl; + ComputeFormulaMap[form] = output; + return output; + } + + void BeevMgr::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! + + if(!check_counterexample) { + return; + } + + //input is valid, no counterexample to check + if(ValidFlag) + return; + + //t is true if SAT solver generated a counterexample, else it is false + if(!t) + FatalError("CheckCounterExample: No CounterExample to check", ASTUndefined); + const ASTVec c = GetAsserts(); + for(ASTVec::const_iterator it=c.begin(),itend=c.end();it!=itend;it++) + if(ASTFalse == ComputeFormulaUsingModel(*it)) + FatalError("CheckCounterExample:counterexample bogus:"\ + "assert evaluates to FALSE under counterexample: NOT OK",*it); + + if(ASTTrue == ComputeFormulaUsingModel(_current_query)) + FatalError("CheckCounterExample:counterexample bogus:"\ + "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) + 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) + 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) + 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) + 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. + */ + ASTNode BeevMgr::GetCounterExample(bool t, const ASTNode& expr) { + //input is valid, no counterexample to get + if(ValidFlag) + return ASTUndefined; + + if(BOOLEAN_TYPE == expr.GetType()) { + return ComputeFormulaUsingModel(expr); + } + + if(BVCONST == expr.GetKind()) { + return expr; + } + + ASTNodeMap::iterator it; + ASTNode output; + if((it = CounterExampleMap.find(expr)) != CounterExampleMap.end()) + output = TermToConstTermUsingModel(CounterExampleMap[expr],false); + else + output = CreateZeroConst(expr.GetValueWidth()); + return output; + } //End of GetCounterExample + + // 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 + //if returned 1 then input is VALID + //if returned 2 then ERROR + int BeevMgr::TopLevelSAT( const ASTNode& inputasserts, const ASTNode& query) { + /******start solving**********/ + ASTNode q = CreateNode(AND, inputasserts, CreateNode(NOT,query)); + ASTNode orig_input = q; + ASTNodeStats("input asserts and query: ", q); + + ASTNode newq = q; + //round of substitution, solving, and simplification. ensures that + //DAG is minimized as much as possibly, and ideally should + //garuntee that all liketerms in BVPLUSes have been combined. + BVSolver bvsolver(this); + SimplifyWrites_InPlace_Flag = false; + Begin_RemoveWrites = false; + start_abstracting = false; + TermsAlreadySeenMap.clear(); + do { + q = newq; + newq = CreateSubstitutionMap(newq); + //ASTNodeStats("after pure substitution: ", newq); + newq = SimplifyFormula_TopLevel(newq,false); + //ASTNodeStats("after simplification: ", newq); + //newq = bvsolver.TopLevelBVSolve(newq); + //ASTNodeStats("after solving: ", newq); + }while(q!=newq); + + ASTNodeStats("Before SimplifyWrites_Inplace begins: ", newq); + SimplifyWrites_InPlace_Flag = true; + Begin_RemoveWrites = false; + start_abstracting = false; + TermsAlreadySeenMap.clear(); + do { + q = newq; + //newq = CreateSubstitutionMap(newq); + //ASTNodeStats("after pure substitution: ", newq); + newq = SimplifyFormula_TopLevel(newq,false); + //ASTNodeStats("after simplification: ", newq); + newq = bvsolver.TopLevelBVSolve(newq); + //ASTNodeStats("after solving: ", newq); + }while(q!=newq); + ASTNodeStats("After SimplifyWrites_Inplace: ", newq); + + start_abstracting = (arraywrite_refinement) ? true : false; + SimplifyWrites_InPlace_Flag = false; + Begin_RemoveWrites = (start_abstracting) ? false : true; + if(start_abstracting) { + ASTNodeStats("before abstraction round begins: ", newq); + } + + TermsAlreadySeenMap.clear(); + do { + q = newq; + //newq = CreateSubstitutionMap(newq); + //Begin_RemoveWrites = true; + //ASTNodeStats("after pure substitution: ", newq); + newq = SimplifyFormula_TopLevel(newq,false); + //ASTNodeStats("after simplification: ", newq); + //newq = bvsolver.TopLevelBVSolve(newq); + //ASTNodeStats("after solving: ", newq); + }while(q!=newq); + + if(start_abstracting) { + ASTNodeStats("After abstraction: ", newq); + } + start_abstracting = false; + SimplifyWrites_InPlace_Flag = false; + Begin_RemoveWrites = false; + + newq = TransformFormula(newq); + ASTNodeStats("after transformation: ", newq); + TermsAlreadySeenMap.clear(); + + int res; + //solver instantiated here + MINISAT::Solver newS; + if(arrayread_refinement) { + counterexample_checking_during_refinement = true; + } + + //call SAT and check the result + res = CallSAT_ResultCheck(newS,newq,orig_input); + if(2 != res) { + CountersAndStats("print_func_stats"); + return res; + } + + res = SATBased_ArrayReadRefinement(newS,newq,orig_input); + if(2 != res) { + CountersAndStats("print_func_stats"); + return res; + } + + res = SATBased_ArrayWriteRefinement(newS,orig_input); + if(2 != res) { + CountersAndStats("print_func_stats"); + return res; + } + + res = SATBased_ArrayReadRefinement(newS,newq,orig_input); + if(2 != res) { + CountersAndStats("print_func_stats"); + return res; + } + + FatalError("TopLevelSAT: reached the end without proper conclusion:" + "either a divide by zero in the input or a bug in STP"); + //bogus return to make the compiler shut up + return 2; + } //End of TopLevelSAT + + //go over the list of indices for each array, and generate Leibnitz + //axioms. Then assert these axioms into the SAT solver. Check if the + //addition of the new constraints has made the bogus counterexample + //go away. if yes, return the correct answer. if no, continue adding + //Leibnitz axioms systematically. + // FIXME: What it really does is, for each array, loop over each index i. + // inside that loop, it finds all the true and false axioms with i as first + // index. When it's got them all, it adds the false axioms to the formula + // and re-solves, and returns if the result is correct. Otherwise, it + // goes on to the next index. + // If it gets through all the indices without a correct result (which I think + // is impossible, but this is pretty confusing), it then solves with all + // the true axioms, too. + // This is not the most obvious way to do it, and I don't know how it + // compares with other approaches (e.g., one false axiom at a time or + // all the false axioms each time). + int BeevMgr::SATBased_ArrayReadRefinement(MINISAT::Solver& newS, + const ASTNode& q, const ASTNode& orig_input) { + if(!arrayread_refinement) + FatalError("SATBased_ArrayReadRefinement: Control should not reach here"); + + ASTVec FalseAxiomsVec, RemainingAxiomsVec; + RemainingAxiomsVec.push_back(ASTTrue); + FalseAxiomsVec.push_back(ASTTrue); + + //in these loops we try to construct Leibnitz axioms and add it to + //the solve(). We add only those axioms that are false in the + //current counterexample. we keep adding the axioms until there + //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++) { + 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++) { + if(BVCONST == it->GetKind()) { + continue; + } + + ASTNode the_index = *it; + //get the arrayname + ASTNode ArrName = iset->first; + // if(SYMBOL != ArrName.GetKind()) + // FatalError("SATBased_ArrayReadRefinement: arrname is not a SYMBOL",ArrName); + ASTNode arr_read1 = CreateTerm(READ, ArrName.GetValueWidth(), ArrName, the_index); + //get the variable corresponding to the array_read1 + ASTNode arrsym1 = _arrayread_symbol[arr_read1]; + if(!(SYMBOL == arrsym1.GetKind() || BVCONST == arrsym1.GetKind())) + FatalError("TopLevelSAT: refinementloop:term arrsym1 corresponding to READ must be a var", arrsym1); + + //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++) { + ASTNode compare_index = *it1; + //do not compare with yourself + if(the_index == compare_index) + continue; + + //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 arr_read2 = CreateTerm(READ, ArrName.GetValueWidth(), ArrName, compare_index); + //get the variable corresponding to the array_read2 + ASTNode arrsym2 = _arrayread_symbol[arr_read2]; + if(!(SYMBOL == arrsym2.GetKind() || BVCONST == arrsym2.GetKind())) + FatalError("TopLevelSAT: refinement loop:" + "term arrsym2 corresponding to READ must be a var", arrsym2); + + ASTNode eqOfReads = CreateSimplifiedEQ(arrsym1,arrsym2); + //construct appropriate Leibnitz axiom + ASTNode LeibnitzAxiom = CreateNode(IMPLIES, eqOfIndices, eqOfReads); + if(ASTFalse == ComputeFormulaUsingModel(LeibnitzAxiom)) + //FalseAxioms = CreateNode(AND,FalseAxioms,LeibnitzAxiom); + FalseAxiomsVec.push_back(LeibnitzAxiom); + else + //RemainingAxioms = CreateNode(AND,RemainingAxioms,LeibnitzAxiom); + RemainingAxiomsVec.push_back(LeibnitzAxiom); + } + ASTNode FalseAxioms = (FalseAxiomsVec.size()>1) ? CreateNode(AND,FalseAxiomsVec) : FalseAxiomsVec[0]; + ASTNodeStats("adding false readaxioms to SAT: ", FalseAxioms); + int res2 = CallSAT_ResultCheck(newS,FalseAxioms,orig_input); + if(2!=res2) { + return res2; + } + } + } + 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 + + ASTNode BeevMgr::Create_ArrayWriteAxioms(const ASTNode& term, const ASTNode& newvar) { + if(READ != term.GetKind() && WRITE != term[0].GetKind()) { + FatalError("Create_ArrayWriteAxioms: Input must be a READ over a WRITE",term); + } + + ASTNode lhs = newvar; + ASTNode rhs = term; + ASTNode arraywrite_axiom = CreateSimplifiedEQ(lhs,rhs); + return arraywrite_axiom; + }//end of Create_ArrayWriteAxioms() + + int BeevMgr::SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, const ASTNode& orig_input) { + ASTNode writeAxiom; + ASTNodeMap::iterator it = ReadOverWrite_NewName_Map.begin(); + ASTNodeMap::iterator itend = ReadOverWrite_NewName_Map.end(); + //int count = 0; + //int num_write_axioms = ReadOverWrite_NewName_Map.size(); + + ASTVec FalseAxioms, RemainingAxioms; + FalseAxioms.push_back(ASTTrue); + RemainingAxioms.push_back(ASTTrue); + for(;it!=itend;it++) { + //Guided refinement starts here + ComputeFormulaMap.clear(); + writeAxiom = Create_ArrayWriteAxioms(it->first,it->second); + if(ASTFalse == ComputeFormulaUsingModel(writeAxiom)) { + writeAxiom = TransformFormula(writeAxiom); + FalseAxioms.push_back(writeAxiom); + } + else { + writeAxiom = TransformFormula(writeAxiom); + RemainingAxioms.push_back(writeAxiom); + } + } + + writeAxiom = (FalseAxioms.size() != 1) ? CreateNode(AND,FalseAxioms) : FalseAxioms[0]; + ASTNodeStats("adding false writeaxiom to SAT: ", writeAxiom); + int res2 = CallSAT_ResultCheck(newS,writeAxiom,orig_input); + if(2!=res2) { + return res2; + } + + 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) { + return res2; + } + + return 2; + } //end of SATBased_ArrayWriteRefinement + + //Check result after calling SAT FIXME: Document arguments in + //comments, and give them meaningful names. How is anyone supposed + //to know what "q" is? + int BeevMgr::CallSAT_ResultCheck(MINISAT::Solver& newS, + const ASTNode& q, const ASTNode& orig_input) { + //Bitblast, CNF, call SAT now + ASTNode BBFormula = BBForm(q); + //ASTNodeStats("after bitblasting", BBFormula); + ClauseList *cllp = ToCNF(BBFormula); + // if(stats && print_nodes) { + // cout << "\nClause list" << endl; + // PrintClauseList(cout, *cllp); + // cerr << "\n finished printing clauselist\n"; + // } + + bool sat = toSATandSolve(newS,*cllp); + // Temporary debugging call. + // CheckBBandCNF(newS, BBFormula); + + DeleteClauseList(cllp); + if(!sat) { + PrintOutput(true); + return 1; + } + else if(newS.okay()) { + CounterExampleMap.clear(); + ConstructCounterExample(newS); + if (stats && print_nodes) { + PrintSATModel(newS); + } + //check if the counterexample is good or not + ComputeFormulaMap.clear(); + if(counterexample_checking_during_refinement) + bvdiv_exception_occured = false; + ASTNode orig_result = ComputeFormulaUsingModel(orig_input); + if(!(ASTTrue == orig_result || ASTFalse == orig_result)) + FatalError("TopLevelSat: Original input must compute to true or false against model"); + +// if(!arrayread_refinement && !(ASTTrue == orig_result)) { +// print_counterexample = true; +// PrintCounterExample(true); +// FatalError("counterexample bogus : arrayread_refinement is switched off: " +// "EITHER all LA axioms have not been added OR bitblaster() or ToCNF()" +// "or satsolver() or counterexamplechecker() have a bug"); +// } + + // if the counterexample is indeed a good one, then return + // invalid + if(ASTTrue == orig_result) { + CheckCounterExample(newS.okay()); + PrintOutput(false); + PrintCounterExample(newS.okay()); + PrintCounterExample_InOrder(newS.okay()); + return 0; + } + // counterexample is bogus: flag it + else { + if(stats && print_nodes) { + cout << "Supposedly bogus one: \n"; + bool tmp = print_counterexample; + print_counterexample = true; + PrintCounterExample(true); + print_counterexample = tmp; + } + + return 2; + } + } + else { + PrintOutput(true); + return -100; + } + } //end of CALLSAT_ResultCheck + + + //FUNCTION: this function accepts a boolvector and returns a BVConst + ASTNode BeevMgr::BoolVectoBVConst(hash_map<unsigned,bool> * w, unsigned int l) { + unsigned len = w->size(); + if(l < len) + FatalError("BoolVectorBVConst : length of bitvector does not match hash_map size:",ASTUndefined,l); + std::string cc; + for(unsigned int jj = 0; jj < l; jj++) { + if((*w)[jj] == true) + cc += '1'; + else if((*w)[jj] == false) + cc += '0'; + else + cc += '0'; + } + return CreateBVConst(cc.c_str(),2); + } + + void BeevMgr::PrintActivityLevels_Of_SATVars(char * init_msg, MINISAT::Solver& newS) { + if(!print_sat_varorder) + return; + + ASTtoSATMap::iterator itbegin = _ASTNode_to_SATVar.begin(); + ASTtoSATMap::iterator itend = _ASTNode_to_SATVar.end(); + + cout << init_msg; + cout << ": Printing activity levels of variables\n"; + for(ASTtoSATMap::iterator it=itbegin;it!=itend;it++){ + cout << (it->second) << " : "; + (it->first).PL_Print(cout,0); + cout << " : "; + cout << newS.returnActivity(it->second) << endl; + } + } + + //this function biases the activity levels of MINISAT variables. + void BeevMgr::ChangeActivityLevels_Of_SATVars(MINISAT::Solver& newS) { + if(!variable_activity_optimize) + return; + + ASTtoSATMap::iterator itbegin = _ASTNode_to_SATVar.begin(); + ASTtoSATMap::iterator itend = _ASTNode_to_SATVar.end(); + + unsigned int index=1; + double base = 2; + for(ASTtoSATMap::iterator it=itbegin;it!=itend;it++){ + ASTNode n = it->first; + + if(BVGETBIT == n.GetKind() || NOT == n.GetKind()) { + if(BVGETBIT == n.GetKind()) + index = GetUnsignedConst(n[1]); + else if (NOT == n.GetKind() && BVGETBIT == n[0].GetKind()) + index = GetUnsignedConst(n[0][1]); + else + index = 0; + double initial_activity = pow(base,(double)index); + newS.updateInitialActivity(it->second,initial_activity); + } + else { + double initial_activity = pow(base,pow(base,(double)index)); + newS.updateInitialActivity(it->second,initial_activity); + } + } + } + + //This function prints the output of the STP solver + void BeevMgr::PrintOutput(bool true_iff_valid) { + //self-explanatory + if(true_iff_valid) { + ValidFlag = true; + if(print_output) { + if(smtlib_parser_enable) + cout << "unsat\n"; + else + cout << "Valid.\n"; + } + } + else { + ValidFlag = false; + if(print_output) { + if(smtlib_parser_enable) + cout << "sat\n"; + else + cout << "Invalid.\n"; + } + } + } +}; //end of namespace BEEV |