void convert( const goto_programt &program, irept &irep )
{
  irep.id("goto-program");
  irep.get_sub().reserve(program.instructions.size());
  for (goto_programt::instructionst::const_iterator it=
          program.instructions.begin();
       it!=program.instructions.end();
       it++)
  {
    irep.get_sub().push_back(irept());
    convert(*it, irep.get_sub().back());
  }
}

/// To convert to JSON from an irep structure by recurssively generating JSON
/// for the different sub trees.
/// \param irep: The irep structure to turn into json
/// \param json: The json object to be filled up.
void json_irept::convert_from_irep(const irept &irep, jsont &json) const
{
  json_objectt &irep_object=json.make_object();
  if(irep.id()!=ID_nil)
    irep_object["id"]=json_stringt(irep.id_string());

  convert_sub_tree("sub", irep.get_sub(), irep_object);
  convert_named_sub_tree("namedSub", irep.get_named_sub(), irep_object);
  if(include_comments)
  {
    convert_named_sub_tree("comment", irep.get_comments(), irep_object);
  }
}

int irept::compare(const irept &i) const
{
  int r;

  r=id().compare(i.id());
  if(r!=0) return r;

  const subt::size_type size=get_sub().size(),
        i_size=i.get_sub().size();
  if(size<i_size) return -1;
  if(size>i_size) return 1;

  {
    irept::subt::const_iterator it1, it2;

    for(it1=get_sub().begin(),
        it2=i.get_sub().begin();
        it1!=get_sub().end() && it2!=i.get_sub().end();
        it1++,
        it2++)
    {
      r=it1->compare(*it2);
      if(r!=0) return r;
    }

    assert(it1==get_sub().end() && it2==i.get_sub().end());
  }

  const named_subt::size_type n_size=get_named_sub().size(),
        i_n_size=i.get_named_sub().size();
  if(n_size<i_n_size) return -1;
  if(n_size>i_n_size) return 1;

  {
    irept::named_subt::const_iterator it1, it2;

    for(it1=get_named_sub().begin(),
        it2=i.get_named_sub().begin();
        it1!=get_named_sub().end() && it2!=i.get_named_sub().end();
        it1++,
        it2++)
    {
      r=it1->first.compare(it2->first);
      if(r!=0) return r;

      r=it1->second.compare(it2->second);
      if(r!=0) return r;
    }

    assert(it1==get_named_sub().end() &&
           it2==i.get_named_sub().end());
  }

  // equal
  return 0;
}

unsigned irep_hash_container_baset::number(const irept &irep)
{ 
  // the ptr-hash provides a speedup of up to 3x
  
  ptr_hasht::const_iterator it=ptr_hash.find(&irep.read());
  
  if(it!=ptr_hash.end())
    return it->second;

  packedt packed;
  pack(irep, packed);
  unsigned id=numbering.number(packed);
  
  ptr_hash[&irep.read()]=id;
  
  return id;
}

void irept::move_to_named_sub(const irep_namet &name, irept &irep)
{
#ifdef SHARING
    detatch();
#endif
    add(name).swap(irep);
    irep.clear();
}

void jsa_serialisert::operator()(irept &sdu,
    const jsa_genetic_solutiont &entity) const
{
  sdu.set(FITNESS, entity.fitness);
  irept invariant;
  irept::subt &invariant_instructions=invariant.get_sub();
  for (const jsa_genetic_solutiont::invariantt::value_type &instr : entity.invariant)
  {
    irept instruction;
    instruction.set(OPCODE, instr.opcode);
    invariant_instructions.push_back(instruction);
  }
  sdu.set(INVARIANT, invariant);
  irept predicates;
  irept::subt &predicates_list=predicates.get_sub();
  for (const jsa_genetic_solutiont::predicatet &predicate : entity.predicates)
  {
    irept pred;
    irept::subt &predicate_instructions=pred.get_sub();
    for (const jsa_genetic_solutiont::predicatet::value_type &instr : predicate)
    {
      irept instruction;
      instruction.set(OPCODE, instr.opcode);
      instruction.set(OP0, instr.op0);
      instruction.set(OP1, instr.op1);
      instruction.set(RESULT_OP, instr.result_op);
      predicate_instructions.push_back(instruction);
    }
    predicates_list.push_back(pred);
  }
  sdu.set(PREDICATES, predicates);
  irept query;
  irept::subt &query_instructions=query.get_sub();
  for (const jsa_genetic_solutiont::queryt::value_type &instr : entity.query)
  {
    irept instruction;
    instruction.set(OPCODE, instr.opcode);
    instruction.set(OP0, instr.op0);
    instruction.set(OP1, instr.op1);
    query_instructions.push_back(instruction);
  }
  sdu.set(QUERY, query);
}

void jsa_serialisert::operator()(jsa_genetic_solutiont &entity,
    const irept &sdu) const
{
  entity.fitness=jsa_genetic_solutiont::fitnesst(sdu.get_long_long(FITNESS));
  const irept::named_subt &named_sub=sdu.get_named_sub();
  typedef irept::named_subt::const_iterator const_iterator;
  const const_iterator invariant=named_sub.find(INVARIANT);
  assert(named_sub.end() != invariant);
  for (const irept &instruction : invariant->second.get_sub())
  {
    jsa_genetic_solutiont::invariantt::value_type instr;
    instr.opcode=__CPROVER_jsa_opcodet(instruction.get_long_long(OPCODE));
    entity.invariant.push_back(instr);
  }
  const const_iterator predicates=named_sub.find(PREDICATES);
  assert(named_sub.end() != predicates);
  for (const irept &predicate : predicates->second.get_sub())
  {
    jsa_genetic_solutiont::predicatet pred;
    for (const irept &instruction : predicate.get_sub())
    {
      jsa_genetic_solutiont::predicatet::value_type instr;
      instr.opcode=__CPROVER_jsa_opcodet(instruction.get_long_long(OPCODE));
      instr.op0=__CPROVER_jsa_opt(instruction.get_long_long(OP0));
      instr.op1=__CPROVER_jsa_opt(instruction.get_long_long(OP1));
      instr.result_op=__CPROVER_jsa_opt(instruction.get_long_long(RESULT_OP));
      pred.push_back(instr);
    }
    entity.predicates.push_back(pred);
  }
  const const_iterator query=named_sub.find(QUERY);
  assert(named_sub.end() != query);
  for (const irept &instruction : query->second.get_sub())
  {
    jsa_genetic_solutiont::queryt::value_type instr;
    instr.opcode=__CPROVER_jsa_opcodet(instruction.get_long_long(OPCODE));
    instr.op0=__CPROVER_jsa_opt(instruction.get_long_long(OP0));
    instr.op1=__CPROVER_jsa_opt(instruction.get_long_long(OP1));
    entity.query.push_back(instr);
  }
}

bool ordering(const irept &X, const irept &Y)
{
    return X.compare(Y)<0;

#if 0
    if(X.data<Y.data) return true;
    if(Y.data<X.data) return false;

    if(X.sub.size()<Y.sub.size()) return true;
    if(Y.sub.size()<X.sub.size()) return false;

    {
        irept::subt::const_iterator it1, it2;

        for(it1=X.sub.begin(),
                it2=Y.sub.begin();
                it1!=X.sub.end() && it2!=Y.sub.end();
                it1++,
                it2++)
        {
            if(ordering(*it1, *it2)) return true;
            if(ordering(*it2, *it1)) return false;
        }

        assert(it1==X.sub.end() && it2==Y.sub.end());
    }

    if(X.named_sub.size()<Y.named_sub.size()) return true;
    if(Y.named_sub.size()<X.named_sub.size()) return false;

    {
        irept::named_subt::const_iterator it1, it2;

        for(it1=X.named_sub.begin(),
                it2=Y.named_sub.begin();
                it1!=X.named_sub.end() && it2!=Y.named_sub.end();
                it1++,
                it2++)
        {
            if(it1->first<it2->first) return true;
            if(it2->first<it1->first) return false;

            if(ordering(it1->second, it2->second)) return true;
            if(ordering(it2->second, it1->second)) return false;
        }

        assert(it1==X.named_sub.end() && it2==Y.named_sub.end());
    }

    return false;
#endif
}

void irep_hash_container_baset::pack(
  const irept &irep,
  packedt &packed)
{
  const irept::subt &sub=irep.get_sub();
  const irept::named_subt &named_sub=irep.get_named_sub();
  const irept::named_subt &comments=irep.get_comments();

  packed.reserve(
    1+1+sub.size()+named_sub.size()*2+
    (full?comments.size()*2:0));
  
  packed.push_back(irep_id_hash()(irep.id()));

  packed.push_back(sub.size());  
  forall_irep(it, sub)
    packed.push_back(number(*it));

  packed.push_back(named_sub.size());
  forall_named_irep(it, named_sub)
  {
    packed.push_back(irep_id_hash()(it->first)); // id
    packed.push_back(number(it->second)); // sub-irep
  }

/// Deserialize a JSON irep representation.
/// \param input: json object to convert
/// \return result - irep equivalent of input
void json_irept::convert_from_json(const jsont &in, irept &out) const
{
  std::vector<std::string> have_keys;
  for(const auto &keyval : in.object)
    have_keys.push_back(keyval.first);
  std::sort(have_keys.begin(), have_keys.end());
  if(have_keys!=std::vector<std::string>{"comment", "id", "namedSub", "sub"})
    throw "irep JSON representation is missing one of needed keys: "
      "'id', 'sub', 'namedSub', 'comment'";

  out.id(in["id"].value);

  for(const auto &sub : in["sub"].array)
  {
    out.get_sub().push_back(irept());
    convert_from_json(sub, out.get_sub().back());
  }

  for(const auto &named_sub : in["namedSub"].object)
    convert_from_json(named_sub.second, out.add(named_sub.first));

  for(const auto &comment : in["comment"].object)
    convert_from_json(comment.second, out.add(comment.first));
}

bool full_eq(const irept &i1, const irept &i2)
{
#ifdef SHARING
    if(i1.data==i2.data) return true;
#endif

    if(i1.id()!=i2.id()) return false;

    const irept::subt &i1_sub=i1.get_sub();
    const irept::subt &i2_sub=i2.get_sub();
    const irept::named_subt &i1_named_sub=i1.get_named_sub();
    const irept::named_subt &i2_named_sub=i2.get_named_sub();
    const irept::named_subt &i1_comments=i1.get_comments();
    const irept::named_subt &i2_comments=i2.get_comments();

    if(i1_sub.size()      !=i2_sub.size()) return false;
    if(i1_named_sub.size()!=i2_named_sub.size()) return false;
    if(i1_comments.size() !=i2_comments.size()) return false;

    for(unsigned i=0; i<i1_sub.size(); i++)
        if(!full_eq(i1_sub[i], i2_sub[i]))
            return false;

    {
        irept::named_subt::const_iterator i1_it=i1_named_sub.begin();
        irept::named_subt::const_iterator i2_it=i2_named_sub.begin();

        for(; i1_it!=i1_named_sub.end(); i1_it++, i2_it++)
            if(i1_it->first!=i2_it->first ||
                    !full_eq(i1_it->second, i2_it->second))
                return false;
    }

    {
        irept::named_subt::const_iterator i1_it=i1_comments.begin();
        irept::named_subt::const_iterator i2_it=i2_comments.begin();

        for(; i1_it!=i1_comments.end(); i1_it++, i2_it++)
            if(i1_it->first!=i2_it->first ||
                    !full_eq(i1_it->second, i2_it->second))
                return false;
    }

    return true;
}

void goto_convertt::convert_java_try_catch(
  const codet &code,
  goto_programt &dest)
{
  assert(!code.operands().empty());

  // add the CATCH instruction to 'dest'
  goto_programt::targett catch_instruction=dest.add_instruction();
  catch_instruction->make_catch();
  catch_instruction->code.set_statement(ID_catch);
  catch_instruction->source_location=code.source_location();
  catch_instruction->function=code.source_location().get_function();

  // the CATCH instruction is annotated with a list of exception IDs
  const irept exceptions=code.op0().find(ID_exception_list);
  if(exceptions.is_not_nil())
  {
    irept::subt exceptions_sub=exceptions.get_sub();
    irept::subt &exception_list=
      catch_instruction->code.add(ID_exception_list).get_sub();
    exception_list.resize(exceptions_sub.size());
    for(size_t i=0; i<exceptions_sub.size(); ++i)
      exception_list[i].id(exceptions_sub[i].id());
  }

  // the CATCH instruction is also annotated with a list of handle labels
  const irept handlers=code.op0().find(ID_label);
  if(handlers.is_not_nil())
  {
    irept::subt handlers_sub=handlers.get_sub();
    irept::subt &handlers_list=
      catch_instruction->code.add(ID_label).get_sub();
    handlers_list.resize(handlers_sub.size());
    for(size_t i=0; i<handlers_sub.size(); ++i)
      handlers_list[i].id(handlers_sub[i].id());
  }

  // the CATCH instruction may also signal a handler
  if(code.op0().has_operands())
  {
    catch_instruction->code.get_sub().resize(1);
    catch_instruction->code.get_sub()[0]=code.op0().op0();
  }

  // add a SKIP target for the end of everything
  goto_programt end;
  goto_programt::targett end_target=end.add_instruction();
  end_target->make_skip();
  end_target->source_location=code.source_location();
  end_target->function=code.source_location().get_function();

  // add the end-target
  dest.destructive_append(end);
}

bool operator==(const irept &i1, const irept &i2)
{
#ifdef SHARING
    if(i1.data==i2.data) return true;
#endif

    if(i1.id()!=i2.id()) return false;

    if(i1.get_sub()!=i2.get_sub()) return false; // recursive call

    if(i1.get_named_sub()!=i2.get_named_sub()) return false; // recursive call

    // comments are NOT checked

    return true;
}

void namespace_baset::follow_symbol(irept &irep) const
{
  while(irep.id()==ID_symbol)
  {
    const symbolt &symbol=lookup(irep);

    if(symbol.is_type)
    {
      if(symbol.type.is_nil())
        return;
      else
        irep=symbol.type;
    }
    else
    {
      if(symbol.value.is_nil())
        return;
      else
        irep=symbol.value;
    }
  }
}

bool operator==(const irept &i1, const irept &i2)
{
  #ifdef IREP_HASH_STATS
  ++irep_cmp_cnt;
  #endif
  #ifdef SHARING
  if(i1.data==i2.data) return true;
  #endif

  if(i1.id()!=i2.id() ||
     i1.get_sub()!=i2.get_sub() || // recursive call
     i1.get_named_sub()!=i2.get_named_sub()) // recursive call
  {
    #ifdef IREP_HASH_STATS
    ++irep_cmp_ne_cnt;
    #endif
    return false;
  }

  // comments are NOT checked

  return true;
}

void get_code(const irept &location, std::string &dest)
{
  dest = "";

  const irep_idt &file = location.file();
  const irep_idt &line = location.line();

  if(file == "" || line == "")
    return;

  std::ifstream in(file.c_str());

  if(!in)
    return;

  int line_int = atoi(line.c_str());

  int line_start = line_int - 3, line_end = line_int + 3;

  if(line_start <= 1)
    line_start = 1;

  // skip line_start-1 lines

  for(int l = 0; l < line_start - 1; l++)
  {
    std::string tmp;
    std::getline(in, tmp);
  }

  // read till line_end

  std::list<linet> lines;

  for(int l = line_start; l <= line_end && in; l++)
  {
    lines.emplace_back();

    std::string &line = lines.back().text;
    std::getline(in, line);

    if(!line.empty() && line[line.size() - 1] == '\r')
      line.resize(line.size() - 1);

    lines.back().line_number = l;
  }

  // remove empty lines at the end and at the beginning

  for(std::list<linet>::iterator it = lines.begin(); it != lines.end();)
  {
    if(is_empty_str(it->text))
      it = lines.erase(it);
    else
      break;
  }

  for(std::list<linet>::iterator it = lines.end(); it != lines.begin();)
  {
    it--;

    if(is_empty_str(it->text))
      it = lines.erase(it);
    else
      break;
  }

  // strip space
  strip_space(lines);

  // build dest

  for(auto &line : lines)
  {
    std::string line_no = i2string(line.line_number);

    while(line_no.size() < 4)
      line_no = " " + line_no;

    std::string tmp = line_no + "  " + escape_latex(line.text, true);

    if(line.line_number == line_int)
      tmp = emphasize(tmp);

    dest += tmp + "\n";
  }
}