Added additional CEGIS control solution type

Additional solution type, to be configured for CAV paper.

Author: pkesseli

src/cegis/control/facade/rational_solution_configuration.cpp

@@ -0,0 +1,36 @@
+#include <goto-programs/goto_trace.h>
+
+#include <cegis/control/value/control_vars.h>
+#include <cegis/control/learn/nondet_solution.h>
+#include <cegis/control/facade/rational_solution_configuration.h>
+
+void nondeterminise_solution_configuration(symbol_tablet &st,
+    goto_functionst &gf)
+{
+  nondet_control_solution(st, gf);
+}
+
+namespace
+{
+const struct_exprt &find_solution(const goto_tracet &trace)
+{
+  for (const goto_trace_stept &step : trace.steps)
+  {
+    const exprt &lhs=step.full_lhs;
+    if (ID_symbol != lhs.id()) continue;
+    const std::string &id=id2string(to_symbol_expr(lhs).get_identifier());
+    if (CEGIS_CONTROL_SOLUTION_VAR_NAME != id) continue;
+    return to_struct_expr(step.full_lhs_value);
+  }
+  assert(!"Control solution not found in trace.");
+}
+}
+
+void convert(control_solutiont &current_candidate, const goto_tracet &trace)
+{
+}
+
+void show_candidate(messaget::mstreamt &os, const control_solutiont &candidate)
+{
+
+}

src/cegis/control/facade/rational_solution_configuration.h

@@ -0,0 +1,54 @@
+/*******************************************************************
+
+ Module: Counterexample-Guided Inductive Synthesis
+
+ Author: Daniel Kroening, [email protected]
+         Pascal Kesseli, [email protected]
+
+\*******************************************************************/
+
+#ifndef CEGIS_CONTROL_FACADE_RATIONAL_SOLUTION_CONFIGURATION_H_
+#define CEGIS_CONTROL_FACADE_RATIONAL_SOLUTION_CONFIGURATION_H_
+
+#include <util/message.h>
+
+/**
+ * @brief
+ *
+ * @details
+ */
+class rational_solution_configurationt
+{
+public:
+  /**
+   * @brief
+   *
+   * @details
+   *
+   * @param st
+   * @param gf
+   */
+  static void nondeterminise_solution_configuration(class symbol_tablet &st, class goto_functionst &gf);
+
+  /**
+   * @brief
+   *
+   * @details
+   *
+   * @param current_candidate
+   * @param trace
+   */
+  static void convert(class control_solutiont &current_candidate, const class goto_tracet &trace);
+
+  /**
+   * @brief
+   *
+   * @details
+   *
+   * @param os
+   * @param candidate
+   */
+  static void show_candidate(messaget::mstreamt &os, const control_solutiont &candidate);
+};
+
+#endif /* CEGIS_CONTROL_FACADE_RATIONAL_SOLUTION_CONFIGURATION_H_ */