Added generic stubs to CEGIS refactoring.

Author: pkesseli

regression/cegis/cegis_refactor_benchmark_01/ITaxCalculator.class

@@ -0,0 +1,31 @@
+interface ITaxCalculator {
+  double addTaxes(double price);
+}
+class UsaTaxCalculator implements ITaxCalculator {
+  public double addTaxes(double price) {
+    return price * 1.25;
+  }
+}
+class NullTaxCalculator implements ITaxCalculator {
+  public double addTaxes(double price) {
+    return price;
+  }
+}
+
+public class Runner {
+void sale(ITaxCalculator calc, double price) {
+  if (calc != null)
+    price = calc.addTaxes(price);
+}
+void print(ITaxCalculator calc, double price) {
+  double percentage;
+  if (calc == null)
+    percentage=0;
+  else
+    percentage=calc.addTaxes(100.0) - 100.0;
+  
+  System.out.print("Tax rate: ");
+  System.out.print(percentage);
+  System.out.println('%');
+}
+}

regression/cegis/cegis_refactor_benchmark_01/NullTaxCalculator.class

@@ -53,6 +53,7 @@ SRC = danger/meta/meta_variable_names.cpp danger/facade/danger_runner.cpp danger
       control/simplify/remove_unused_elements.cpp \
       control/verify/control_symex_verify.cpp control/verify/insert_solution.cpp \
       control/value/float_helper.cpp control/value/control_types.cpp \
+      refactor/environment/instrument_state_vars.cpp refactor/instructionset/create_cegis_processor.cpp \
       wordsize/restrict_bv_size.cpp value/program_individual_serialisation.cpp value/assignments_printer.cpp \
       seed/literals_seed.cpp \
       genetic/instruction_set_info_factory.cpp genetic/random_mutate.cpp genetic/random_cross.cpp \

regression/cegis/cegis_refactor_benchmark_01/Runner.class

@@ -0,0 +1,8 @@
+#include <cegis/refactor/environment/instrument_state_vars.h>
+
+void instrument_state_vars(const goto_programt::const_targett first,
+    const goto_programt::const_targett last)
+{
+  // TODO: Implement
+  assert(false);
+}

regression/cegis/cegis_refactor_benchmark_01/Runner.java

@@ -0,0 +1,27 @@
+/*******************************************************************
+
+ Module: Counterexample-Guided Inductive Synthesis
+
+ Author: Daniel Kroening, [email protected]
+         Pascal Kesseli, [email protected]
+
+ \*******************************************************************/
+
+#ifndef CEGIS_REFACTOR_ENVIRONMENT_INSTRUMENT_STATE_VARS_H_
+#define CEGIS_REFACTOR_ENVIRONMENT_INSTRUMENT_STATE_VARS_H_
+
+#include <goto-programs/goto_program.h>
+
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param first
+ * @param last
+ */
+void instrument_state_vars(
+    goto_programt::const_targett first,
+    goto_programt::const_targett last);
+
+#endif /* CEGIS_REFACTOR_ENVIRONMENT_INSTRUMENT_STATE_VARS_H_ */

regression/cegis/cegis_refactor_benchmark_01/UsaTaxCalculator.class

@@ -0,0 +1,7 @@
+#include <cegis/refactor/instructionset/create_cegis_processor.h>
+
+void create_cegis_processor(const std::set<typet> &state_types,
+    const size_t var_slots_per_state_type, const std::set<typet> &context_types)
+{
+
+}

src/cegis/Makefile

@@ -0,0 +1,31 @@
+/*******************************************************************
+
+ Module: Counterexample-Guided Inductive Synthesis
+
+ Author: Daniel Kroening, [email protected]
+         Pascal Kesseli, [email protected]
+
+ \*******************************************************************/
+
+#ifndef CEGIS_REFACTOR_INSTRUCTIONSET_CREATE_CEGIS_PROCESSOR_H_
+#define CEGIS_REFACTOR_INSTRUCTIONSET_CREATE_CEGIS_PROCESSOR_H_
+
+#include <set>
+
+#include <util/type.h>
+
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param state_types
+ * @param var_slots_per_state_type
+ * @param context_types
+ */
+void create_cegis_processor(
+    const std::set<typet> &state_types,
+    size_t var_slots_per_state_type,
+    const std::set<typet> &context_types);
+
+#endif /* CEGIS_REFACTOR_INSTRUCTIONSET_CREATE_CEGIS_PROCESSOR_H_ */