void component_exprt::gen_loc_var(
    exprt &loc_var,
    const exprt &expr, 
    std::string suffix)
{
  std::string base;
  if (expr.id()==ID_symbol)
    base="."+id2string(to_symbol_expr(expr).get_identifier());
  else if (expr.id()==ID_constant)
    base=".const";
  else if (expr.id()==ID_typecast)
  {
    base=".typecast__"+id2string(expr.type().id());
    if (expr.type().id()==ID_signedbv)
    {
      base=base+i2string(to_signedbv_type(expr.type()).get_width());
    }
    else if (expr.type().id()==ID_unsignedbv)
    {
      base=base+i2string(to_unsignedbv_type(expr.type()).get_width());
    }
  }
  else if(id_maps.find(expr.id())!=id_maps.end())
    base=".OPERATOR."+id_maps[expr.id()];
  else
    base=".OPERATOR."+id2string(expr.id());
  std::string final_name="L."+id2string(source_location.get_line())+"."+i2string(instruction_number)+"_"+i2string(component_cnt)+"_"+i2string(unique_identifier)+base+suffix;
  //typet type(ID_integer);
  //exprt loc_var(ID_symbol, type);
  to_symbol_expr(loc_var).set_identifier(final_name);
}

propt::resultt qbf_squolem_coret::prop_solve()
{
  {
    std::string msg=
      "Squolem: "+
      i2string(no_variables())+" variables, "+
      i2string(no_clauses())+" clauses";
    messaget::status() << msg << messaget::eom;
  }

  squolem->endOfOriginals();
  bool result = squolem->decide();

  if(result)
  {
    messaget::status() << "Squolem: VALID" << messaget::eom;
    return P_SATISFIABLE;
  }
  else
  {
    messaget::status() << "Squolem: INVALID" << messaget::eom;
    return P_UNSATISFIABLE;
  }

  return P_ERROR;
}

void simulator_loop_detectiont::get_fresh_induction_parameter(
    exprt &parameter)
{
  symbol_exprt parameter_expr(uint_type());

  bool found;
  do 
  {
    parameter_index++;
    parameter_expr.set_identifier("c::N$"+i2string(parameter_index));
    parameter_expr.set("induction_symbol", true);

    try 
    {
      concrete_model.ns.lookup(parameter_expr);
      found = true;
    }
    catch (std::string ex) 
    {
      found = false;
    }
  }
  while (found);

  symbolt sym;

  sym.name = parameter_expr.get_identifier();
  sym.base_name = "N$"+i2string(parameter_index);
  sym.module = ID_C;

  shadow_context.add (sym);

  parameter = parameter_expr;
}

propt::resultt qbf_bdd_coret::prop_solve()
{
  {
    std::string msg=
      solver_text() + ": "+
      i2string(no_variables())+" variables, "+
      i2string(matrix->nodeCount())+" nodes";
    messaget::status(msg);
  }

  model_bdds.resize(no_variables()+1, NULL);

  // Eliminate variables
  for(quantifierst::const_reverse_iterator it=quantifiers.rbegin();
      it!=quantifiers.rend();
      it++)
  {
    unsigned var=it->var_no;

    if(it->type==quantifiert::EXISTENTIAL)
    {
      #if 0
      std::cout << "BDD E: " << var << ", " <<
        matrix->nodeCount() << " nodes" << std::endl;
      #endif

      BDD* model = new BDD();
      const BDD &varbdd=*bdd_variable_map[var];
      *model = matrix->AndAbstract(varbdd.Xnor(bdd_manager->bddOne()),
                                   varbdd);
      model_bdds[var]=model;

      *matrix = matrix->ExistAbstract(*bdd_variable_map[var]);
    }
    else if(it->type==quantifiert::UNIVERSAL)
    {
      #if 0
      std::cout << "BDD A: " << var << ", " <<
        matrix->nodeCount() << " nodes" << std::endl;
      #endif

      *matrix = matrix->UnivAbstract(*bdd_variable_map[var]);
    }
    else
      throw ("Unquantified variable");
  }

  if(*matrix==bdd_manager->bddOne())
  {
    compress_certificate();
    return P_SATISFIABLE;
  }
  else if(*matrix==bdd_manager->bddZero())
  {
    model_bdds.clear();
    return P_UNSATISFIABLE;
  }
  else
    return P_ERROR;
}

std::string get_temporary_file(
  const std::string &prefix,
  const std::string &suffix)
{
  #ifdef _WIN32
  TCHAR lpTempPathBuffer[MAX_PATH];
  DWORD dwRetVal;

  dwRetVal = GetTempPath(MAX_PATH,          // length of the buffer
                         lpTempPathBuffer); // buffer for path 

  if (dwRetVal > MAX_PATH || (dwRetVal == 0))
    throw "GetTempPath failed";

  std::string t_template=
    std::string(lpTempPathBuffer)+"\\"+prefix+
    i2string(getpid())+".XXXXXX"+suffix;
  #else
  std::string t_template=
    "/tmp/"+prefix+i2string(getpid())+".XXXXXX"+suffix;
  #endif

  char *t_ptr=strdup(t_template.c_str());
  
  int fd=my_mkstemps(t_ptr, suffix.size());

  if(fd<0)
    throw "mkstemps failed";  
    
  close(fd);

  std::string result=std::string(t_ptr);  
  free(t_ptr);
  return result;
}

std::string cpp_typecheckt::class_template_identifier(
  const irep_idt &base_name,
  const template_typet &template_type,
  const cpp_template_args_non_tct &partial_specialization_args)
{
  std::string identifier=
    cpp_scopes.current_scope().prefix+
    "template."+id2string(base_name) + "<";

  int counter=0;

  // these are probably not needed -- templates
  // should be unique in a namespace
  for(template_typet::template_parameterst::const_iterator
      it=template_type.template_parameters().begin();
      it!=template_type.template_parameters().end();
      it++)
  {
    if(counter!=0) identifier+=',';
  
    if(it->id()==ID_type)
      identifier+="Type"+i2string(counter);
    else
      identifier+="Non_Type"+i2string(counter);

    counter++;
  }

  identifier += ">";
  
  if(!partial_specialization_args.arguments().empty())
  {
    identifier+="_specialized_to_<";
  
    counter=0;
    for(cpp_template_args_non_tct::argumentst::const_iterator
        it=partial_specialization_args.arguments().begin();
        it!=partial_specialization_args.arguments().end();
        it++, counter++)
    {  
      if(counter!=0) identifier+=',';
      
      // These are not yet typechecked, as they may depend
      // on unassigned template parameters.

      if(it->id()==ID_type || it->id()=="ambiguous")
        identifier+=cpp_type2name(it->type());
      else
        identifier+=cpp_expr2name(*it);
    }
    
    identifier+='>';
  }
  
  return identifier;
}

std::string abstract_independencet::pretty() const
{
	std::string result;
	
	result+="N"+i2string(current->number)+"/"
				+"N"+i2string(ancestor->number)+"/"
				+"N"+i2string(mover->number);
				
	return result;
}

std::string cvc_propt::cvc_literal(literalt l)
{
  if(l==const_literal(false))
    return "FALSE";
  else if(l==const_literal(true))
    return "TRUE";

  if(l.sign())
    return "(NOT l"+i2string(l.var_no())+")";  

  return "l"+i2string(l.var_no());
}

void modelcheckert::get_variable_names(
    const abstract_modelt &abstract_model)
{
    variable_names.resize(abstract_model.variables.size());

    for(unsigned i=0;
            i<abstract_model.variables.size();
            i++)
    {
        variable_names[i]="b"+i2string(i);

        std::string description=
            abstract_model.variables[i].description;

        // do some substitution
        substitute(description, " ", "_");
        substitute(description, "==", "eq");
        substitute(description, "!=", "neq");
        substitute(description, ">=", "ge");
        substitute(description, "<=", "le");
        substitute(description, ">>", "shr");
        substitute(description, "<<", "shl");
        substitute(description, "<", "lt");
        substitute(description, ">", "gt");
        substitute(description, "&", "amp");
        substitute(description, "|", "or");
        substitute(description, "+", "plus");
        substitute(description, "-", "minus");
        substitute(description, "*", "deref_");

        if(is_variable_name(description))
            variable_names[i]+="_"+description;
    }
}

void local_SSAt::build_transfer(locationt loc)
{
  if(loc->is_assign())
  {
    const code_assignt &code_assign=to_code_assign(loc->code);

    exprt deref_lhs=dereference(code_assign.lhs(), loc);
    exprt deref_rhs=dereference(code_assign.rhs(), loc);

    assign_rec(deref_lhs, deref_rhs, true_exprt(), loc);
  }
  else if(loc->is_function_call())
  {
    const code_function_callt &code_function_call=
      to_code_function_call(loc->code);
      
    const exprt &lhs=code_function_call.lhs();
      
    if(lhs.is_not_nil())
    {
      exprt deref_lhs=dereference(lhs, loc);
    
      // generate a symbol for rhs
      irep_idt identifier="ssa::return_value"+i2string(loc->location_number);
      symbol_exprt rhs(identifier, code_function_call.lhs().type());
      
      assign_rec(deref_lhs, rhs, true_exprt(), loc);
    }
  }
}

tvt z3_propt::l_get(literalt a) const
{
  tvt result=tvt(false);
  std::string literal;
  Z3_ast z3_literal;
  size_t found;

  if(a.is_true())
    return tvt(true);
  else if(a.is_false())
    return tvt(false);

  literal = "l"+i2string(a.var_no());

  map_prop_varst::const_iterator cache_result=map_prop_vars.find(literal.c_str());
  if(cache_result!=map_prop_vars.end())
  {
    //std::cout << "Cache hit on " << cache_result->first << "\n";
	z3_literal = cache_result->second;
    Z3_app app = Z3_to_app(z3_ctx, z3_literal);
    Z3_func_decl d = Z3_get_app_decl(z3_ctx, app);
    literal = Z3_func_decl_to_string(z3_ctx, d);

    found=literal.find("true");

    if (found!=std::string::npos)
      result=tvt(true);
    else
      result=tvt(false);
  }

  if (a.sign()) result=!result;

  return result;
}

BtorExp* boolector_propt::convert_literal(unsigned l)
{
#ifdef DEBUG
  std::cout << "\n" << __FUNCTION__ << "[" << __LINE__ << "]" << "\n";
#endif

  std::string literal_s;

  literal_cachet::const_iterator cache_result=literal_cache.find(l);
  if(cache_result!=literal_cache.end())
  {
    //std::cout << "Cache hit on " << cache_result->first << "\n";
    return cache_result->second;
  }

  BtorExp* result;

  literal_s = "l"+i2string(l);
  result = boolector_var(boolector_ctx, 1, literal_s.c_str());

  // insert into cache
  literal_cache.insert(std::pair<unsigned, BtorExp*>(l, result));

  return result;
}

std::string bv_refinementt::approximationt::as_string() const
{
  #if 0
  return from_expr(expr);
  #else
  return i2string(id_nr)+"/"+id2string(expr.id());
  #endif
}

void termination_baset::replace_nondet_sideeffects(exprt &expr)
{
  if(expr.id()=="sideeffect" &&
     expr.get("statement")=="nondet")
  {
    symbolt symbol;
    symbol.name=std::string("termination::nondet")+i2string(++nondet_counter);
    symbol.base_name=std::string("nondet")+i2string(nondet_counter);
    symbol.type=expr.type();

    expr=symbol_expr(symbol);
    shadow_context.move(symbol);
  }
  else
    Forall_operands(it, expr)
      replace_nondet_sideeffects(*it);
}

cvc_temp_filet::cvc_temp_filet()
{
  temp_out_filename="cvc_dec_out_"+i2string(getpid())+".tmp";

  temp_out.open(
    temp_out_filename.c_str(),
    std::ios_base::out | std::ios_base::trunc);
}

    ACE_TString PrepareIntegerArray(const std::vector<int>& array)
    {
        ACE_TString s;
        for(int i=0;i<(int)array.size()-1;i++)
        {
            s = s + i2string(array[i]) + ACE_TEXT(",");
        }
        ACE_TString res;
        if(array.size()>0)
        {
            res = ACE_TEXT("[") + s + i2string(array[array.size()-1]) + ACE_TEXT("]");
        }
        else
            res = ACE_TEXT("[]");

        return res;
    }

propt::resultt satcheck_minisat1_baset::prop_solve()
{
  assert(status!=ERROR);

  {
    std::string msg=
      i2string(_no_variables)+" variables, "+
      i2string(solver->nClauses())+" clauses";
    messaget::status(msg);
  }
  
  add_variables();

  solver->simplifyDB();
  
  std::string msg;

  if(empty_clause_added)
  {
    msg="empty clause: negated claim is UNSATISFIABLE, i.e., holds";
  }
  else if(!solver->okay())
  {
    msg="SAT checker inconsistent: negated claim is UNSATISFIABLE, i.e., holds";
  }
  else
  {
    vec<Lit> MiniSat_assumptions;
    convert(assumptions, MiniSat_assumptions);

    if(solver->solve(MiniSat_assumptions))
    {
      msg="SAT checker: negated claim is SATISFIABLE, i.e., does not hold";
      messaget::status(msg);
      status=SAT;
      return P_SATISFIABLE;
    }
    else
      msg="SAT checker: negated claim is UNSATISFIABLE, i.e., holds";
  }

  messaget::status(msg);
  status=UNSAT;
  return P_UNSATISFIABLE;
}

decision_proceduret::resultt smt1_dect::read_result_z3(std::istream &in)
{
  std::string line;
  decision_proceduret::resultt res = D_ERROR;

  smt1_prop.reset_assignment();

  typedef hash_map_cont<std::string, std::string, string_hash> valuest;
  valuest values;

  while(str_getline(in, line))
  {
    if(line=="sat")
      res = D_SATISFIABLE;
    else if(line=="unsat")
      res = D_UNSATISFIABLE;
    else
    {
      std::size_t pos=line.find(" -> ");
      if(pos!=std::string::npos)
        values[std::string(line, 0, pos)]=
          std::string(line, pos+4, std::string::npos);
    }
  }

  for(identifier_mapt::iterator
      it=identifier_map.begin();
      it!=identifier_map.end();
      it++)
  {
    it->second.value.make_nil();
    std::string conv_id=convert_identifier(it->first);
    std::string value=values[conv_id];
    if(value=="") continue;

//    std::cout << it->first << " := " << value << std::endl;

    exprt e;
    if(string_to_expr_z3(it->second.type, value, e))
    {
//      std::cout << "E: " << e << std::endl;
      it->second.value=e;
    }
    else
      set_value(it->second, value);
  }

  // Booleans
  for(unsigned v=0; v<smt1_prop.no_variables(); v++)
  {
    std::string value=values["B"+i2string(v)];
    if(value=="") continue;
    smt1_prop.set_assignment(literalt(v, false), value=="true");
  }

  return res;
}

decision_proceduret::resultt bv_refinementt::dec_solve()
{
  // do the usual post-processing
  status() << "BV-Refinement: post-processing" << eom;
  post_process();

  debug() << "Solving with " << prop.solver_text() << eom;
  
  unsigned iteration=0;
  
  // now enter the loop
  while(true)
  {
    iteration++;
  
    status() << "BV-Refinement: iteration " << iteration << eom;

    // output the very same information in a structured fashion
    if(ui==ui_message_handlert::XML_UI)
    {
      xmlt xml("refinement-iteration");
      xml.data=i2string(iteration);
      std::cout << xml << '\n';
    }

    switch(prop_solve())
    {
    case D_SATISFIABLE:
      check_SAT();
      if(!progress)
      {
        status() << "BV-Refinement: got SAT, and it simulates => SAT" << eom;
        status() << "Total iterations: " << iteration << eom;
        return D_SATISFIABLE;
      }
      else
        status() << "BV-Refinement: got SAT, and it is spurious, refining" << eom;
      break;

    case D_UNSATISFIABLE:
      check_UNSAT();
      if(!progress)
      {
        status() << "BV-Refinement: got UNSAT, and the proof passes => UNSAT" << eom;
        status() << "Total iterations: " << iteration << eom;
        return D_UNSATISFIABLE;
      }
      else
        status() << "BV-Refinement: got UNSAT, and the proof fails, refining" << eom;
      break;
    
    default:
      return D_ERROR;
    }
  }
}

std::string get_temporary_file(
  const std::string &prefix,
  const std::string &suffix)
{
  #ifdef _WIN32
  char lpTempPathBuffer[MAX_PATH];
  DWORD dwRetVal;

  dwRetVal = GetTempPathA(MAX_PATH,          // length of the buffer
                          lpTempPathBuffer); // buffer for path 

  if (dwRetVal > MAX_PATH || (dwRetVal == 0))
    throw "GetTempPath failed";

  // the path returned by GetTempPath ends with a backslash
  std::string t_template=
    std::string(lpTempPathBuffer)+prefix+
    i2string(getpid())+".XXXXXX"+suffix;
  #else
  std::string dir="/tmp/";
  const char *TMPDIR_env=getenv("TMPDIR");
  if(TMPDIR_env!=0)
    dir=TMPDIR_env;
  if(*dir.rbegin()!='/') dir+='/';

  std::string t_template=
    dir+prefix+i2string(getpid())+".XXXXXX"+suffix;
  #endif

  char *t_ptr=strdup(t_template.c_str());
  
  int fd=mkstemps(t_ptr, suffix.size());

  if(fd<0)
    throw "mkstemps failed";  
    
  close(fd);

  std::string result=std::string(t_ptr);  
  free(t_ptr);
  return result;
}