decision_proceduret::resultt
fault_localizationt::run_decision_procedure(prop_convt &prop_conv)
{
  status() << "Passing problem to "
               << prop_conv.decision_procedure_text() << eom;

  prop_conv.set_message_handler(bmc.get_message_handler());

  // stop the time
  absolute_timet sat_start=current_time();

  bmc.do_conversion();

  freeze_guards();

  status() << "Running " << prop_conv.decision_procedure_text()
               << eom;

  decision_proceduret::resultt dec_result=prop_conv.dec_solve();
  // output runtime

  {
    absolute_timet sat_stop=current_time();
    status() << "Runtime decision procedure: "
             << (sat_stop-sat_start) << "s" << eom;
  }

  return dec_result;
}

void symex_target_equationt::convert_assertions(
  prop_convt &prop_conv)
{
  // we find out if there is only _one_ assertion,
  // which allows for a simpler formula
  
  unsigned number_of_assertions=count_assertions();

  if(number_of_assertions==0)
    return;
    
  if(number_of_assertions==1)
  {
    for(SSA_stepst::iterator it=SSA_steps.begin();
        it!=SSA_steps.end(); it++)
      if(it->is_assert())
      {
        prop_conv.set_to_false(it->cond_expr);
        it->cond_literal=const_literal(false);
        return; // prevent further assumptions!
      }
      else if(it->is_assume())
        prop_conv.set_to_true(it->cond_expr);

    assert(false); // unreachable
  }

  bvt bv;

  bv.reserve(number_of_assertions);
  
  literalt assumption_literal=const_literal(true);

  for(SSA_stepst::iterator it=SSA_steps.begin();
      it!=SSA_steps.end(); it++)
    if(it->is_assert())
    {
      // do the expression
      literalt tmp_literal=prop_conv.convert(it->cond_expr);

      it->cond_literal=prop_conv.prop.limplies(assumption_literal, tmp_literal);

      bv.push_back(prop_conv.prop.lnot(it->cond_literal));
    }
    else if(it->is_assume())
      assumption_literal=
        prop_conv.prop.land(assumption_literal, it->cond_literal);

  if(!bv.empty())
    prop_conv.prop.lcnf(bv);
}

void symex_target_equationt::convert_guards(
  prop_convt &prop_conv)
{
  for(auto & it : SSA_steps)
  {
    if(it.ignore)
      it.guard_literal=const_literal(false);
    else
      it.guard_literal=prop_conv.convert(it.guard);
  }
}

literalt make_pos(
  const namespacet &ns,
  prop_convt &conv,
  const exprt &expr)
{
  exprt tmp_expr(expr);
  literalt l=conv.convert(tmp_expr);
  literalt tmp_lit=conv.prop.new_variable();
  conv.prop.set_equal(tmp_lit, l);
  assert(!tmp_lit.sign());
  return tmp_lit;
}

void symex_target_equationt::convert_decls(
  prop_convt &prop_conv) const
{
  for(const auto & it : SSA_steps)
  {
    if(it.is_decl() && !it.ignore)
    {
      // The result is not used, these have no impact on
      // the satisfiability of the formula.
      prop_conv.convert(it.cond_expr);
    }
  }
}

void symex_target_equationt::convert_goto_instructions(
  prop_convt &prop_conv)
{
  for(auto & it : SSA_steps)
  {
    if(it.is_goto())
    {
      if(it.ignore)
        it.cond_literal=const_literal(true);
      else
        it.cond_literal=prop_conv.convert(it.cond_expr);
    }
  }
}

void symex_target_equationt::convert_assumptions(
  prop_convt &prop_conv)
{
  for(SSA_stepst::iterator it=SSA_steps.begin();
      it!=SSA_steps.end(); it++)
  {
    if(it->is_assume())
    {
      if(it->ignore)
        it->cond_literal=const_literal(true);
      else
        it->cond_literal=prop_conv.convert(it->cond_expr);
    }
  }
}

void prop_conv_storet::constraintt::replay(prop_convt &dest) const
{
  switch(type)
  {
  case SET_TO:
    dest.set_to(expr, value);
    break;
  
  case CONVERT:
    //dest.prop.set_equal(dest.convert_rest(expr), literal);
    break;

  default:
    assert(false);
  }
}

symex_target_equationt::SSA_stepst::const_iterator
counterexample_beautificationt::get_failed_property(
  const prop_convt &prop_conv,
  const symex_target_equationt &equation)
{
  // find failed property

  for(symex_target_equationt::SSA_stepst::const_iterator
      it=equation.SSA_steps.begin();
      it!=equation.SSA_steps.end(); it++)
    if(it->is_assert() &&
       prop_conv.l_get(it->guard_literal).is_true() &&
       prop_conv.l_get(it->cond_literal).is_false())
      return it;

  assert(false);
  return equation.SSA_steps.end();
}

void counterexample_beautificationt::get_minimization_list(
  prop_convt &prop_conv,
  const symex_target_equationt &equation,
  minimization_listt &minimization_list)
{
  // ignore the ones that are assigned under false guards

  for(symex_target_equationt::SSA_stepst::const_iterator
      it=equation.SSA_steps.begin();
      it!=equation.SSA_steps.end(); it++)
  {
    if(it->is_assignment() &&
       it->assignment_type==symex_targett::assignment_typet::STATE)
    {
      if(!prop_conv.l_get(it->guard_literal).is_false())
      {
        const typet &type=it->ssa_lhs.type();

        if(type!=bool_typet())
        {
          // we minimize the absolute value, if applicable
          if(type.id()==ID_signedbv ||
             type.id()==ID_fixedbv ||
             type.id()==ID_floatbv)
          {
            abs_exprt abs_expr(it->ssa_lhs);
            minimization_list.insert(abs_expr);
          }
          else
            minimization_list.insert(it->ssa_lhs);
        }
      }
    }

    // reached failed assertion?
    if(it==failed)
      break;
  }
}

exprt build_full_lhs_rec(
  const prop_convt &prop_conv,
  const namespacet &ns,
  const exprt &src_original, // original identifiers
  const exprt &src_ssa)      // renamed identifiers
{
  if(src_ssa.id()!=src_original.id())
    return src_original;

  const irep_idt id=src_original.id();

  if(id==ID_index)
  {
    // get index value from src_ssa
    exprt index_value=prop_conv.get(to_index_expr(src_ssa).index());

    if(index_value.is_not_nil())
    {
      simplify(index_value, ns);
      index_exprt tmp=to_index_expr(src_original);
      tmp.index()=index_value;
      tmp.array()=
        build_full_lhs_rec(prop_conv, ns,
          to_index_expr(src_original).array(),
          to_index_expr(src_ssa).array());
      return tmp;
    }

    return src_original;
  }
  else if(id==ID_member)
  {
    member_exprt tmp=to_member_expr(src_original);
    tmp.struct_op()=build_full_lhs_rec(
      prop_conv, ns,
      to_member_expr(src_original).struct_op(),
      to_member_expr(src_ssa).struct_op());
  }
  else if(id==ID_if)
  {
    if_exprt tmp2=to_if_expr(src_original);

    tmp2.false_case()=build_full_lhs_rec(prop_conv, ns,
      tmp2.false_case(), to_if_expr(src_ssa).false_case());

    tmp2.true_case()=build_full_lhs_rec(prop_conv, ns,
      tmp2.true_case(), to_if_expr(src_ssa).true_case());

    exprt tmp=prop_conv.get(to_if_expr(src_ssa).cond());

    if(tmp.is_true())
      return tmp2.true_case();
    else if(tmp.is_false())
      return tmp2.false_case();
    else
      return tmp2;
  }
  else if(id==ID_typecast)
  {
    typecast_exprt tmp=to_typecast_expr(src_original);
    tmp.op()=build_full_lhs_rec(prop_conv, ns,
      to_typecast_expr(src_original).op(), to_typecast_expr(src_ssa).op());
    return tmp;
  }
  else if(id==ID_byte_extract_little_endian ||
          id==ID_byte_extract_big_endian)
  {
    exprt tmp=src_original;
    assert(tmp.operands().size()==2);
    tmp.op0()=build_full_lhs_rec(prop_conv, ns, tmp.op0(), src_ssa.op0());

    // re-write into big case-split

  }

  return src_original;
}

void build_goto_trace(
  const symex_target_equationt &target,
  symex_target_equationt::SSA_stepst::const_iterator end_step,
  const prop_convt &prop_conv,
  const namespacet &ns,
  goto_tracet &goto_trace)
{
  // We need to re-sort the steps according to their clock.
  // Furthermore, read-events need to occur before write
  // events with the same clock.

  typedef std::map<mp_integer, goto_tracet::stepst> time_mapt;
  time_mapt time_map;

  mp_integer current_time=0;

  for(symex_target_equationt::SSA_stepst::const_iterator
      it=target.SSA_steps.begin();
      it!=end_step;
      it++)
  {
    const symex_target_equationt::SSA_stept &SSA_step=*it;

    if(prop_conv.l_get(SSA_step.guard_literal)!=tvt(true))
      continue;

    if(it->is_constraint() ||
       it->is_spawn())
      continue;
    else if(it->is_atomic_begin())
    {
      // for atomic sections the timing can only be determined once we see
      // a shared read or write (if there is none, the time will be
      // reverted to the time before entering the atomic section); we thus
      // use a temporary negative time slot to gather all events
      current_time*=-1;
      continue;
    }
    else if(it->is_shared_read() || it->is_shared_write() ||
            it->is_atomic_end())
    {
      mp_integer time_before=current_time;

      if(it->is_shared_read() || it->is_shared_write())
      {
        // these are just used to get the time stamp
        exprt clock_value=prop_conv.get(
          symbol_exprt(partial_order_concurrencyt::rw_clock_id(it)));

        to_integer(clock_value, current_time);
      }
      else if(it->is_atomic_end() && current_time<0)
        current_time*=-1;

      assert(current_time>=0);
      // move any steps gathered in an atomic section

      if(time_before<0)
      {
        time_mapt::iterator entry=
          time_map.insert(std::make_pair(
              current_time,
              goto_tracet::stepst())).first;
        entry->second.splice(entry->second.end(), time_map[time_before]);
        time_map.erase(time_before);
      }

      continue;
    }

    // drop PHI and GUARD assignments altogether
    if(it->is_assignment() &&
       (SSA_step.assignment_type==symex_target_equationt::PHI ||
        SSA_step.assignment_type==symex_target_equationt::GUARD))
      continue;

    goto_tracet::stepst &steps=time_map[current_time];
    steps.push_back(goto_trace_stept());
    goto_trace_stept &goto_trace_step=steps.back();

    goto_trace_step.thread_nr=SSA_step.source.thread_nr;
    goto_trace_step.pc=SSA_step.source.pc;
    goto_trace_step.comment=SSA_step.comment;
    if(SSA_step.ssa_lhs.is_not_nil())
      goto_trace_step.lhs_object=ssa_exprt(SSA_step.ssa_lhs.get_original_expr());
    else
      goto_trace_step.lhs_object.make_nil();
    goto_trace_step.type=SSA_step.type;
    goto_trace_step.hidden=SSA_step.hidden;
    goto_trace_step.format_string=SSA_step.format_string;
    goto_trace_step.io_id=SSA_step.io_id;
    goto_trace_step.formatted=SSA_step.formatted;
    goto_trace_step.identifier=SSA_step.identifier;

    goto_trace_step.assignment_type=
      (it->is_assignment()&&
       (SSA_step.assignment_type==symex_targett::VISIBLE_ACTUAL_PARAMETER ||
        SSA_step.assignment_type==symex_targett::HIDDEN_ACTUAL_PARAMETER))?
      goto_trace_stept::ACTUAL_PARAMETER:
      goto_trace_stept::STATE;
//.........这里部分代码省略.........

void build_goto_trace(
  const symex_target_equationt &target,
  const prop_convt &prop_conv,
  const namespacet &ns,
  goto_tracet &goto_trace)
{
  // We need to re-sort the steps according to their clock.
  // Furthermore, read-events need to occur before write
  // events with the same clock.
  
  typedef std::map<mp_integer, goto_tracet::stepst> time_mapt;
  time_mapt time_map;
  
  mp_integer current_time=0;
  for(symex_target_equationt::SSA_stepst::const_iterator
      it=target.SSA_steps.begin();
      it!=target.SSA_steps.end();
      it++)
  {
    const symex_target_equationt::SSA_stept &SSA_step=*it;
    
    if(prop_conv.l_get(SSA_step.guard_literal)!=tvt(true))
      continue;

    if(it->is_constraint() ||
       it->is_spawn())
      continue;
    else if(it->is_atomic_begin())
    {
      // for atomic sections the timing can only be determined once we see
      // a shared read or write (if there is none, the time will be
      // reverted to the time before entering the atomic section); we thus
      // use a temporary negative time slot to gather all events
      current_time*=-1;
      continue;
    }
    else if(it->is_shared_read() || it->is_shared_write() ||
            it->is_atomic_end())
    {
      mp_integer time_before=current_time;

      if(it->is_shared_read() || it->is_shared_write())
      {
        // these are just used to get the time stamp
        exprt clock_value=prop_conv.get(
          symbol_exprt(partial_order_concurrencyt::rw_clock_id(it)));

        to_integer(clock_value, current_time);
      }
      else if(it->is_atomic_end() && current_time<0)
        current_time*=-1;

      assert(current_time>=0);
      // move any steps gathered in an atomic section

      if(time_before<0)
      {
        time_mapt::iterator entry=
          time_map.insert(std::make_pair(
              current_time,
              goto_tracet::stepst())).first;
        entry->second.splice(entry->second.end(), time_map[time_before]);
        time_map.erase(time_before);
      }

      continue;
    }

    // drop PHI and GUARD assignments altogether
    if(it->is_assignment() &&
       (SSA_step.assignment_type==symex_target_equationt::PHI ||
        SSA_step.assignment_type==symex_target_equationt::GUARD))
      continue;

    goto_tracet::stepst &steps=time_map[current_time];
    steps.push_back(goto_trace_stept());    
    goto_trace_stept &goto_trace_step=steps.back();
    
    goto_trace_step.thread_nr=SSA_step.source.thread_nr;
    goto_trace_step.pc=SSA_step.source.pc;
    goto_trace_step.comment=SSA_step.comment;
    goto_trace_step.lhs_object=SSA_step.original_lhs_object;
    goto_trace_step.type=SSA_step.type;
    goto_trace_step.hidden=SSA_step.hidden;
    goto_trace_step.format_string=SSA_step.format_string;
    goto_trace_step.io_id=SSA_step.io_id;
    goto_trace_step.formatted=SSA_step.formatted;
    goto_trace_step.identifier=SSA_step.identifier;

    goto_trace_step.assignment_type=
      (SSA_step.assignment_type==symex_targett::VISIBLE_ACTUAL_PARAMETER ||
       SSA_step.assignment_type==symex_targett::HIDDEN_ACTUAL_PARAMETER)?
      goto_trace_stept::ACTUAL_PARAMETER:
      goto_trace_stept::STATE;
    
    if(SSA_step.original_full_lhs.is_not_nil())
      goto_trace_step.full_lhs=
        build_full_lhs_rec(
          prop_conv, ns, SSA_step.original_full_lhs, SSA_step.ssa_full_lhs);
    
//.........这里部分代码省略.........