path: root/stp/AST/ToSAT.cpp

/********************************************************************
 * 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