Added CAV CEGIS control front-end

Added second CEGIS control front-end for CAV benchmarks.

Author: pkesseli

src/cegis/Makefile

@@ -46,12 +46,14 @@ SRC = danger/meta/meta_variable_names.cpp danger/facade/danger_runner.cpp danger
       jsa/genetic/jsa_source_provider.cpp jsa/genetic/dynamic_jsa_test_runner.cpp jsa/genetic/random_jsa_mutate.cpp \
       jsa/genetic/random_jsa_cross.cpp jsa/genetic/jsa_genetic_convert.cpp jsa/genetic/jsa_random.cpp \
       jsa/genetic/solution_helper.cpp jsa/genetic/jsa_serialiser.cpp jsa/genetic/jsa_paragon_wrapper.cpp \
-      control/facade/control_runner.cpp control/learn/rational_solution_configuration.cpp \
+      control/facade/control_runner.cpp \
+      control/learn/print_control_solution.cpp \
+      control/learn/rational_solution_configuration.cpp control/learn/vector_solution_configuration.cpp \
       control/preprocessing/control_preprocessing.cpp control/preprocessing/propagate_controller_sizes.cpp \
       control/options/control_program.cpp \
       control/learn/nondet_solution.cpp \
       control/simplify/remove_unused_elements.cpp \
-      control/verify/control_symex_verify.cpp control/verify/insert_solution.cpp \
+      control/verify/insert_solution.cpp control/verify/zero_solutions.cpp \
       control/value/float_helper.cpp control/value/control_types.cpp \
       refactor/environment/instrument_state_vars.cpp \
       refactor/instructionset/create_cegis_processor.cpp refactor/instructionset/execute_cegis_program.cpp \

src/cegis/control/facade/control_runner.cpp

@@ -5,35 +5,48 @@
 #include <cegis/facade/runner_helper.h>
 #include <cegis/instrument/instrument_var_ops.h>
 #include <cegis/control/value/control_types.h>
+#include <cegis/control/value/control_vector_solution.h>
 #include <cegis/control/preprocessing/control_preprocessing.h>
 #include <cegis/control/preprocessing/propagate_controller_sizes.h>
 #include <cegis/control/learn/control_symex_learn.h>
 #include <cegis/control/learn/rational_solution_configuration.h>
+#include <cegis/control/learn/vector_solution_configuration.h>
 #include <cegis/control/verify/control_symex_verify.h>
+#include <cegis/control/verify/zero_solutions.h>
 #include <cegis/control/facade/control_runner.h>
 
-int run_control(optionst &o, messaget::mstreamt &result,
-    const symbol_tablet &st, const goto_functionst &gf)
+// XXX: Debug
+#include <iostream>
+// XXX: Debug
+
+namespace
+{
+template<class solution_configt, class zero_solutiont>
+int run(optionst &o, messaget::mstreamt &result, const symbol_tablet &st,
+    const goto_functionst &gf, const zero_solutiont &default_solution)
 {
   control_preprocessingt prep(st, gf);
   const control_programt &program=prep.get_program();
-  typedef control_symex_learnt<rational_solution_configurationt> control_learnt;
+  typedef control_symex_learnt<solution_configt> control_learnt;
   control_learnt lcfg(program);
-  const std::function<void(control_solutiont &)> default_solution=
-      [&st](control_solutiont &solution)
-      { if (!solution.a.operands().empty()) return;
-        const symbol_typet &type=control_solution_type(st);
-        const source_locationt loc(default_cegis_source_location());
-        const namespacet ns(st);
-        null_message_handlert msg;
-        const exprt zero(zero_initializer(type, loc, ns, msg));
-        const struct_exprt zero_struct=to_struct_expr(zero);
-        solution.a=get_a_controller_comp(ns, zero_struct);
-        solution.b=get_b_controller_comp(ns, zero_struct);
-      };
-  cegis_symex_learnt<control_preprocessingt, control_learnt> learn(o,
-      prep, lcfg, default_solution);
-  control_symex_verifyt vcfg(program);
-  cegis_symex_verifyt<control_symex_verifyt> oracle(o, vcfg);
+  cegis_symex_learnt<control_preprocessingt, control_learnt> learn(o, prep,
+      lcfg, default_solution);
+  typedef control_symex_verifyt<typename solution_configt::solutiont> verifyt;
+  verifyt vcfg(program);
+  cegis_symex_verifyt<verifyt> oracle(o, vcfg);
   return run_cegis_with_statistics_wrapper(result, o, learn, oracle, prep);
 }
+}
+
+int run_control(optionst &o, messaget::mstreamt &result,
+    const symbol_tablet &st, const goto_functionst &gf)
+{
+  const bool is_vector_solution=is_vector_solution_config(st);
+  if (is_vector_solution_config(st))
+  {
+    const zero_vector_solutiont def(st);
+    return run<vector_solution_configurationt>(o, result, st, gf, def);
+  }
+  const zero_rational_solutiont def(st);
+  return run<rational_solution_configurationt>(o, result, st, gf, def);
+}

src/cegis/control/learn/control_symex_learn.h

@@ -29,7 +29,7 @@ class control_symex_learnt
 public:
   typedef control_counterexamplet counterexamplet;
   typedef control_counterexamplest counterexamplest;
-  typedef control_solutiont candidatet;
+  typedef typename solution_configt::solutiont candidatet;
   /**
    * @brief
    *

src/cegis/control/learn/rational_solution_configuration.cpp

@@ -7,6 +7,10 @@
 #include <cegis/control/preprocessing/propagate_controller_sizes.h>
 #include <cegis/control/preprocessing/control_preprocessing.h>
 
+// XXX: Debug
+#include <iostream>
+// XXX: Debug
+
 control_preprocessingt::control_preprocessingt(const symbol_tablet &st,
     const goto_functionst &gf) :
     control_program(st, gf)
@@ -15,11 +19,12 @@ control_preprocessingt::control_preprocessingt(const symbol_tablet &st,
 
 namespace
 {
-const char * const excluded_functions[]=
-    { "verify_stability_closedloop_using_dslib", "check_stability_closedloop",
-        "fxp_double_to_fxp", "fxp_to_double", "ft_closedloop_series",
-        "poly_mult", "poly_sum", "internal_pow", "fxp_check",
-        "fxp_control_floatt_to_fxp", "main", "validation" };
+const char * const excluded_functions[]= {
+    "verify_stability_closedloop_using_dslib", "check_stability_closedloop",
+    "fxp_double_to_fxp", "fxp_to_double", "ft_closedloop_series", "poly_mult",
+    "poly_sum", "internal_pow", "fxp_check", "fxp_control_floatt_to_fxp",
+    "main", "validation", "double_matrix_multiplication", "double_sub_matrix",
+    "check_stability" };
 
 bool is_meta(const goto_programt::const_targett pos)
 {
@@ -45,6 +50,12 @@ void control_preprocessingt::operator ()()
   goto_programt::targetst &locs=control_program.counterexample_locations;
   goto_programt &body=get_entry_body(gf);
   collect_counterexample_locations(locs, body, is_meta);
+  // XXX: Debug
+  for (const goto_programt::const_targett target : locs)
+  {
+    std::cout << "<ce>" << target->code.pretty() << "</ce>" << std::endl;
+  }
+  // XXX: Debug
   propagate_controller_sizes(st, gf);
 }
 

src/cegis/control/learn/rational_solution_configuration.h

@@ -6,15 +6,31 @@
 #include <cegis/cegis-util/program_helper.h>
 #include <cegis/control/value/control_vars.h>
 
-const exprt &get_controller_comp(const namespacet &ns,
-    const struct_exprt &value, const char * const comp)
+namespace
+{
+template<class struct_exprt_typet, class exprt_typet>
+exprt_typet &get_comp(const namespacet &ns, struct_exprt_typet &value,
+    const char * const comp)
 {
   const struct_typet &type=to_struct_type(ns.follow(value.type()));
   const struct_typet::componentst &comps=type.components();
   for (size_t i=0; i < comps.size(); ++i)
     if (id2string(comps[i].get_name()) == comp) return value.operands()[i];
   assert(!"Solution component not found.");
 }
+}
+
+const exprt &get_controller_comp(const namespacet &ns,
+    const struct_exprt &value, const char * const comp)
+{
+  return get_comp<const struct_exprt, const exprt>(ns, value, comp);
+}
+
+exprt &get_controller_comp(const namespacet &ns, struct_exprt &value,
+    const char * const comp)
+{
+  return get_comp<struct_exprt, exprt>(ns, value, comp);
+}
 
 const array_exprt &get_a_controller_comp(const namespacet &ns,
     const struct_exprt &value)
@@ -30,6 +46,13 @@ const array_exprt &get_b_controller_comp(const namespacet &ns,
       get_controller_comp(ns, value, CEGIS_CONTROL_B_MEMBER_NAME));
 }
 
+const array_exprt &get_K_controller_comp(const namespacet &ns,
+    const struct_exprt &value)
+{
+  return to_array_expr(
+      get_controller_comp(ns, value, CEGIS_CONTROL_K_MEMBER_NAME));
+}
+
 namespace
 {
 const exprt &get_a_size(const namespacet &ns, const struct_exprt &value)
@@ -79,6 +102,7 @@ class replace_sizes_visitort: public expr_visitort
 
 void propagate_controller_sizes(const symbol_tablet &st, goto_functionst &gf)
 {
+  if (!st.has_symbol(CEGIS_CONTROL_SOLUTION_VAR_NAME)) return;
   const symbolt &symbol=st.lookup(CEGIS_CONTROL_SOLUTION_VAR_NAME);
   const struct_exprt &controller_value=to_struct_expr(symbol.value);
   const namespacet ns(st);

src/cegis/control/preprocessing/control_preprocessing.cpp

@@ -26,6 +26,20 @@ const exprt &get_controller_comp(
     const struct_exprt &value,
     const char * const comp);
 
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param ns
+ * @param value
+ * @param comp
+ */
+exprt &get_controller_comp(
+    const namespacet &ns,
+    struct_exprt &value,
+    const char * const comp);
+
 /**
  * @brief
  *
@@ -54,6 +68,20 @@ const array_exprt &get_b_controller_comp(
     const namespacet &ns,
     const struct_exprt &value);
 
+/**
+ * @brief
+ *
+ * @details
+ *
+ * @param ns
+ * @param value
+ *
+ * @return
+ */
+const array_exprt &get_K_controller_comp(
+    const namespacet &ns,
+    const struct_exprt &value);
+
 /**
  * @brief
  *

src/cegis/control/preprocessing/propagate_controller_sizes.cpp

@@ -9,6 +9,11 @@ const symbol_typet &control_solution_type(const symbol_tablet &st)
   return to_symbol_type(st.lookup(CEGIS_CONTROL_SOLUTION_VAR_NAME).type);
 }
 
+const symbol_typet &control_vector_solution_type(const symbol_tablet &st)
+{
+  return to_symbol_type(st.lookup(CEGIS_CONTROL_VECTOR_SOLUTION_VAR_NAME).type);
+}
+
 namespace
 {
 const struct_typet::componentt &get_comp(const symbol_tablet &st,