ebmc: offer k-induction interface

src/ebmc/k_induction.cpp

@@ -8,18 +8,21 @@ Author: Daniel Kroening, [email protected]
 
 #include "k_induction.h"
 
+#include <util/string2int.h>
+
 #include <trans-word-level/instantiate_word_level.h>
 #include <trans-word-level/property.h>
 #include <trans-word-level/trans_trace_word_level.h>
 #include <trans-word-level/unwind.h>
 
 #include "bmc.h"
-#include "ebmc_base.h"
 #include "ebmc_error.h"
 #include "ebmc_solver_factory.h"
 #include "liveness_to_safety.h"
 #include "report_results.h"
 
+#include <fstream>
+
 /*******************************************************************\
 
    Class: k_inductiont
@@ -28,26 +31,34 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-class k_inductiont:public ebmc_baset
+class k_inductiont
 {
 public:
   k_inductiont(
-    const cmdlinet &_cmdline,
-    ui_message_handlert &_ui_message_handler)
-    : ebmc_baset(_cmdline, _ui_message_handler),
-      ns{transition_system.symbol_table},
-      solver_factory(ebmc_solver_factory(_cmdline))
+    std::size_t _k,
+    const transition_systemt &_transition_system,
+    ebmc_propertiest &_properties,
+    const ebmc_solver_factoryt &_solver_factory,
+    message_handlert &_message_handler)
+    : k(_k),
+      transition_system(_transition_system),
+      properties(_properties),
+      solver_factory(_solver_factory),
+      message(_message_handler)
   {
   }
 
-  int operator()();
+  void operator()();
 
 protected:
-  namespacet ns;
-  ebmc_solver_factoryt solver_factory;
+  const std::size_t k;
+  const transition_systemt &transition_system;
+  ebmc_propertiest &properties;
+  const ebmc_solver_factoryt &solver_factory;
+  messaget message;
 
   void induction_base();
-  int induction_step();
+  void induction_step();
 };
 
 /*******************************************************************\
@@ -62,16 +73,20 @@ Function: do_k_induction
 
 \*******************************************************************/
 
-int do_k_induction(
-  const cmdlinet &cmdline,
-  ui_message_handlert &ui_message_handler)
+void k_induction(
+  std::size_t k,
+  const transition_systemt &transition_system,
+  ebmc_propertiest &properties,
+  const ebmc_solver_factoryt &solver_factory,
+  message_handlert &message_handler)
 {
-  return k_inductiont(cmdline, ui_message_handler)();
+  k_inductiont(
+    k, transition_system, properties, solver_factory, message_handler)();
 }
 
 /*******************************************************************\
 
-Function: k_inductiont::do_k_induction
+Function: do_k_induction
 
   Inputs:
 
@@ -81,45 +96,64 @@ Function: k_inductiont::do_k_induction
 
 \*******************************************************************/
 
-int k_inductiont::operator()()
+int do_k_induction(
+  const cmdlinet &cmdline,
+  ui_message_handlert &message_handler)
 {
-  if(get_bound()) return 1;
-
-  transition_system =
-    get_transition_system(cmdline, message.get_message_handler());
+  std::size_t k = [&cmdline, &message_handler]() -> std::size_t {
+    if(!cmdline.isset("bound"))
+    {
+      messaget message(message_handler);
+      message.warning() << "using 1-induction" << messaget::eom;
+      return 1;
+    }
+    else
+      return unsafe_string2unsigned(cmdline.get_value("bound"));
+  }();
 
-  auto result = get_properties();
-  if(result != -1)
-    return result;
+  auto transition_system = get_transition_system(cmdline, message_handler);
 
-  // liveness to safety translation, if requested
-  if(cmdline.isset("liveness-to-safety"))
-    liveness_to_safety(transition_system, properties);
+  auto properties = ebmc_propertiest::from_command_line(
+    cmdline, transition_system, message_handler);
 
   if(properties.properties.empty())
-  {
-    message.error() << "no properties" << messaget::eom;
-    return 1;
-  }
+    throw ebmc_errort() << "no properties";
 
-  // Check whether the properties are suitable for k-induction.
-  for(const auto &property : properties.properties)
-    if(property.requires_lasso_constraints())
-    {
-      throw ebmc_errort().with_location(property.location)
-        << "k-induction does not support liveness properties";
-    }
+  auto solver_factory = ebmc_solver_factory(cmdline);
+
+  k_induction(
+    k, transition_system, properties, solver_factory, message_handler);
+
+  const namespacet ns(transition_system.symbol_table);
+  report_results(cmdline, properties, ns, message_handler);
+
+  // We return '0' if all properties are proved,
+  // and '10' otherwise.
+  return properties.all_properties_proved() ? 0 : 10;
+}
 
+/*******************************************************************\
+
+Function: k_inductiont::operator()
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void k_inductiont::operator()()
+{
   // do induction base
   induction_base();
 
-  // do induction step
-  result=induction_step();
-
-  const namespacet ns(transition_system.symbol_table);
-  report_results(cmdline, properties, ns, message.get_message_handler());
+  // all properties refuted?
+  //  for(auto &property :
 
-  return result;
+  // do induction step
+  induction_step();
 }
 
 /*******************************************************************\
@@ -139,7 +173,7 @@ void k_inductiont::induction_base()
   message.status() << "Induction Base" << messaget::eom;
 
   bmc(
-    bound,
+    k,
     false,
     transition_system,
     properties,
@@ -159,11 +193,12 @@ Function: k_inductiont::induction_step
 
 \*******************************************************************/
 
-int k_inductiont::induction_step()
+void k_inductiont::induction_step()
 {
   message.status() << "Induction Step" << messaget::eom;
 
-  unsigned no_timeframes=bound+1;
+  const std::size_t no_timeframes = k + 1;
+  const namespacet ns(transition_system.symbol_table);
 
   for(auto &p_it : properties.properties)
   {
@@ -194,16 +229,14 @@ int k_inductiont::induction_step()
     if(property.id()!=ID_sva_always &&
        property.id()!=ID_AG)
     {
-      message.error()
-        << "unsupported property - only SVA always or AG implemented"
-        << messaget::eom;
-      return 1;
+      throw ebmc_errort()
+        << "unsupported property - only SVA always or AG implemented";
     }
 
     const exprt &p = to_unary_expr(property).op();
 
     // assumption: time frames 0,...,k-1
-    for(unsigned c=0; c<no_timeframes-1; c++)
+    for(std::size_t c = 0; c < no_timeframes - 1; c++)
     {
       exprt tmp=
         instantiate(p, c, no_timeframes-1, ns);
@@ -235,19 +268,10 @@ int k_inductiont::induction_step()
       break;
 
     case decision_proceduret::resultt::D_ERROR:
-      message.error() << "Error from decision procedure" << messaget::eom;
-      p_it.failure();
-      return 2;
+      throw ebmc_errort() << "Error from decision procedure";
 
     default:
-      message.error() << "Unexpected result from decision procedure"
-                      << messaget::eom;
-      p_it.failure();
-      return 1;
+      throw ebmc_errort() << "Unexpected result from decision procedure";
     }
   }
-
-  // We return '0' if all properties are proved,
-  // and '10' otherwise.
-  return properties.all_properties_proved() ? 0 : 10;
 }

src/ebmc/k_induction.h

@@ -12,6 +12,19 @@ Author: Daniel Kroening, [email protected]
 #include <util/cmdline.h>
 #include <util/ui_message.h>
 
+#include "ebmc_solver_factory.h"
+
 int do_k_induction(const cmdlinet &, ui_message_handlert &);
 
+class transition_systemt;
+class ebmc_propertiest;
+
+// Basic k-induction. The result is stored in the ebmc_propertiest argument.
+void k_induction(
+  std::size_t k,
+  const transition_systemt &,
+  ebmc_propertiest &,
+  const ebmc_solver_factoryt &,
+  message_handlert &);
+
 #endif