/******************************************************************** * 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 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 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 >)(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 * v; if(_ASTNode_to_Bitvector.find(symbol) == _ASTNode_to_Bitvector.end()) _ASTNode_to_Bitvector[symbol] = new hash_map(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 * 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 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 * 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