Added missing CEGIS helpers.

Author: Pascal Kesseli

src/cegis/cegis-util/instruction_iterator.cpp

@@ -0,0 +1,79 @@
+#include <cegis/cegis-util/instruction_iterator.h>
+
+namespace
+{
+bool has_body(const goto_functionst::function_mapt::iterator &it,
+    const goto_functionst::function_mapt::const_iterator &end)
+{
+  if (end == it) return false;
+  return it->second.body_available();
+}
+}
+
+instr_iteratort::instr_iteratort()
+{
+}
+
+instr_iteratort::instr_iteratort(goto_functionst &gf) :
+    func_it(gf.function_map.begin()), func_end(gf.function_map.end())
+{
+  while (!has_body(func_it, func_end) && func_end != func_it)
+    ++func_it;
+  if (has_body(func_it, func_end))
+    prog_it=func_it->second.body.instructions.begin();
+}
+
+instr_iteratort &instr_iteratort::operator++()
+{
+  if (func_it->second.body.instructions.end() == prog_it) do
+  {
+    ++func_it;
+    if (func_end == func_it)
+    {
+      func_it=goto_functionst::function_mapt::iterator();
+      prog_it=goto_programt::targett();
+      break;
+    } else prog_it=func_it->second.body.instructions.begin();
+  } while (func_it->second.body.instructions.end() == prog_it);
+  else ++prog_it;
+  return *this;
+}
+
+instr_iteratort instr_iteratort::operator++(int)
+{
+  const instr_iteratort retval=*this;
+  operator ++();
+  return retval;
+}
+
+bool instr_iteratort::operator==(const instr_iteratort &other) const
+{
+  return func_it == other.func_it && prog_it == other.prog_it;
+}
+
+bool instr_iteratort::operator!=(const instr_iteratort &other) const
+{
+  return func_it != other.func_it && prog_it != other.prog_it;
+}
+
+instr_iteratort::reference instr_iteratort::operator*()
+{
+  return *prog_it;
+}
+
+instr_iteratort::pointer instr_iteratort::operator->()
+{
+  return &*prog_it;
+}
+
+instr_iteratort::operator goto_programt::targett() const
+{
+  return prog_it;
+}
+
+goto_programt::targett instr_iteratort::body_end() const
+{
+  return func_it->second.body.instructions.end();
+}
+
+const instr_iteratort instr_iteratort::end;

src/cegis/cegis-util/instruction_iterator.h

@@ -0,0 +1,125 @@
+/*******************************************************************
+
+ Module: Counterexample-Guided Inductive Synthesis
+
+ Author: Daniel Kroening, [email protected]
+         Pascal Kesseli, [email protected]
+
+ \*******************************************************************/
+
+#ifndef CEGIS_CEGIS_UTIL_INSTRUCTION_ITERATOR_H_
+#define CEGIS_CEGIS_UTIL_INSTRUCTION_ITERATOR_H_
+
+#include <iterator>
+
+#include <goto-programs/goto_functions.h>
+
+/**
+ * @brief
+ *
+ * @details
+ */
+class instr_iteratort: public std::iterator<std::input_iterator_tag,
+    goto_programt::instructiont>
+{
+  goto_functionst::function_mapt::iterator func_it;
+  const goto_functionst::function_mapt::const_iterator func_end;
+  goto_programt::targett prog_it;
+
+  /**
+   * @brief
+   *
+   * @details
+   */
+  explicit instr_iteratort();
+public:
+  /**
+   * @brief
+   *
+   * @details
+   *
+   * @param gf
+   */
+  explicit instr_iteratort(goto_functionst &gf);
+
+  /**
+   * @brief
+   *
+   * @details
+   *
+   * @return
+   */
+  instr_iteratort &operator++();
+
+  /**
+   * @brief
+   *
+   * @details
+   *
+   * @return
+   */
+  instr_iteratort operator++(int);
+
+  /**
+   * @brief
+   *
+   * @details
+   *
+   * @return
+   */
+  bool operator==(const instr_iteratort &other) const;
+
+  /**
+   * @brief
+   *
+   * @details
+   *
+   * @return
+   */
+  bool operator!=(const instr_iteratort &other) const;
+
+  /**
+   * @brief
+   *
+   * @details
+   *
+   * @return
+   */
+  reference operator*();
+
+  /**
+   * @brief
+   *
+   * @details
+   *
+   * @return
+   */
+  pointer operator->();
+
+  /**
+   * @brief
+   *
+   * @details
+   *
+   * @return
+   */
+  operator goto_programt::targett() const;
+
+  /**
+   * @brief
+   *
+   * @details
+   *
+   * @return
+   */
+  goto_programt::targett body_end() const;
+
+  /**
+   * @brief
+   *
+   * @details
+   */
+  static const instr_iteratort end;
+};
+
+#endif /* CEGIS_CEGIS_UTIL_INSTRUCTION_ITERATOR_H_ */