diff options
Diffstat (limited to 'stp/AST/ToSAT.cpp')
| -rw-r--r-- | stp/AST/ToSAT.cpp | 1386 |
1 files changed, 0 insertions, 1386 deletions
diff --git a/stp/AST/ToSAT.cpp b/stp/AST/ToSAT.cpp deleted file mode 100644 index 3ad21f93..00000000 --- a/stp/AST/ToSAT.cpp +++ /dev/null @@ -1,1386 +0,0 @@ -/******************************************************************** - * 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. - */ - 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(); - printf("restarts : %"I64_fmt"\n", s.starts); - printf("conflicts : %-12"I64_fmt" (%.0f /sec)\n", s.conflicts , s.conflicts /cpu_time); - printf("decisions : %-12"I64_fmt" (%.0f /sec)\n", s.decisions , s.decisions /cpu_time); - printf("propagations : %-12"I64_fmt" (%.0f /sec)\n", s.propagations, s.propagations/cpu_time); - printf("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) printf("Memory used : %.2f MB\n", mem_used / 1048576.0); - printf("CPU time : %g s\n", cpu_time); - fflush(stdout); - } - - // 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 |