Merge pull request #650 from diffblue/move_k_induction

Move k-induction invocation
diffblue · Aug 30, 2024 · c60cabb · c60cabb
2 parents 89a8255 + 133e0a4
commit c60cabb
Show file tree

Hide file tree

Showing 4 changed files with 18 additions and 16 deletions.
diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp
@@ -18,7 +18,6 @@ Author: Daniel Kroening, [email protected]
 #include "ebmc_error.h"
 #include "ebmc_version.h"
 #include "ic3_engine.h"
-#include "k_induction.h"
 #include "liveness_to_safety.h"
 #include "neural_liveness.h"
 #include "property_checker.h"
@@ -160,9 +159,6 @@ int ebmc_parse_optionst::doit()
       return do_ic3(cmdline, ui_message_handler);
 #endif
 
-    if(cmdline.isset("k-induction"))
-      return do_k_induction(cmdline, ui_message_handler);
-
     if(cmdline.isset("neural-liveness"))
       return do_neural_liveness(cmdline, ui_message_handler);
 

diff --git a/src/ebmc/k_induction.cpp b/src/ebmc/k_induction.cpp
@@ -85,7 +85,7 @@ class k_inductiont
 
 /*******************************************************************\
 
-Function: do_k_induction
+Function: k_induction
 
   Inputs:
 
@@ -108,7 +108,7 @@ void k_induction(
 
 /*******************************************************************\
 
-Function: do_k_induction
+Function: k_induction
 
   Inputs:
 
@@ -118,9 +118,11 @@ Function: do_k_induction
 
 \*******************************************************************/
 
-int do_k_induction(
+int k_induction(
   const cmdlinet &cmdline,
-  ui_message_handlert &message_handler)
+  transition_systemt &transition_system,
+  ebmc_propertiest &properties,
+  message_handlert &message_handler)
 {
   std::size_t k = [&cmdline, &message_handler]() -> std::size_t {
     if(!cmdline.isset("bound"))
@@ -133,11 +135,6 @@ int do_k_induction(
       return unsafe_string2unsigned(cmdline.get_value("bound"));
   }();
 
-  auto transition_system = get_transition_system(cmdline, message_handler);
-
-  auto properties = ebmc_propertiest::from_command_line(
-    cmdline, transition_system, message_handler);
-
   if(properties.properties.empty())
     throw ebmc_errort() << "no properties";
 

diff --git a/src/ebmc/k_induction.h b/src/ebmc/k_induction.h
@@ -10,15 +10,19 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_EBMC_K_INDUCTION_H
 
 #include <util/cmdline.h>
-#include <util/ui_message.h>
+#include <util/message.h>
 
 #include "ebmc_solver_factory.h"
 
-int do_k_induction(const cmdlinet &, ui_message_handlert &);
-
 class transition_systemt;
 class ebmc_propertiest;
 
+int k_induction(
+  const cmdlinet &,
+  transition_systemt &,
+  ebmc_propertiest &,
+  message_handlert &);
+
 // Basic k-induction. The result is stored in the ebmc_propertiest argument.
 void k_induction(
   std::size_t k,

diff --git a/src/ebmc/property_checker.cpp b/src/ebmc/property_checker.cpp
@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include "dimacs_writer.h"
 #include "ebmc_error.h"
 #include "ebmc_solver_factory.h"
+#include "k_induction.h"
 #include "output_file.h"
 #include "report_results.h"
 
@@ -388,6 +389,10 @@ int property_checker(
     return bit_level_bmc(
       cmdline, transition_system, properties, message_handler);
   }
+  else if(cmdline.isset("k-induction"))
+  {
+    return k_induction(cmdline, transition_system, properties, message_handler);
+  }
   else
   {
     // default engine is word-level BMC