Extended CEGIS refactorig processor factory interface.

Author: pkesseli

src/cegis/instrument/literals.h

@@ -17,7 +17,7 @@
 #define CEGIS_EXECUTE "__CPROVER_danger_execute"
 #define CEGIS_RESULT_OPS "__CPROVER_cegis_RESULT_OPS"
 #define CEGIS_MODULE "<builtin-library-cegis>"
-#define CEGIS_PREFIX "__CPROVER_cegis_"
+#define CEGIS_PREFIX CPROVER_PREFIX "cegis_"
 #define CEGIS_TMP_PREFIX CEGIS_PREFIX "tmp_"
 #define CEGIS_PRIME_SUFFIX "_prime"
 #define CEGIS_CONSTANT_PREFIX "CEGIS_CONSTANT_"

src/cegis/refactor/instructionset/create_cegis_processor.cpp

@@ -1,3 +1,5 @@
+#include <cegis/instrument/literals.h>
+
 #include <cegis/refactor/instructionset/create_cegis_processor.h>
 
 namespace
@@ -24,9 +26,12 @@ std::set<typet> collect_context_types(const goto_ranget &range)
   return collector.types;
 }
 
-void create_cegis_processor(const std::set<typet> &state_types,
+#define CEGIS_PROCESSOR_FUNCTION_PREFIX CEGIS_PREFIX "processor_"
+
+std::string create_cegis_processor(const std::set<typet> &state_types,
     const size_t var_slots_per_state_type, const std::set<typet> &context_types)
 {
+  std::string processor_name(CEGIS_PROCESSOR_FUNCTION_PREFIX);
   // TODO: Implement
   assert(false);
 }

src/cegis/refactor/instructionset/create_cegis_processor.h

@@ -32,11 +32,17 @@ std::set<typet> collect_context_types(const goto_ranget &range);
  *
  * @details
  *
+ * @param st
+ * @param gf
  * @param state_types
  * @param var_slots_per_state_type
  * @param context_types
+ *
+ * @return
  */
-void create_cegis_processor(
+std::string create_cegis_processor(
+    symbol_tablet &st,
+    goto_functionst &gf,
     const std::set<typet> &state_types,
     size_t var_slots_per_state_type,
     const std::set<typet> &context_types);

src/cegis/refactor/options/refactor_program.h

@@ -47,6 +47,7 @@ class refactor_programt
     goto_ranget spec_range;
     std::set<irep_idt> state_vars;
     std::set<typet> types;
+    std::string processor_function;
   };
 
   /**

src/cegis/refactor/preprocessing/refactor_preprocessing.cpp

@@ -30,9 +30,11 @@ void refactor_preprocessingt::operator()()
     break;
   }
   for (refactor_programt::sketcht &s : original_program.sketches)
+  {
     s.state_vars=collect_state_vars(s.spec_range.first, s.spec_range.second);
+    // TODO: construct_instruction_set(original_program); // Multiple?
+  }
   // TODO: Insert extern programs.
-  // TODO: construct_instruction_set(original_program); // Multiple?
   switch (type)
   {
   case refactoring_typet::NULL_OBJECT: