IC3: use property_checker interface

Author: kroening

src/ebmc/ebmc_parse_options.cpp

@@ -17,7 +17,6 @@ Author: Daniel Kroening, [email protected]
 #include "ebmc_base.h"
 #include "ebmc_error.h"
 #include "ebmc_version.h"
-#include "ic3_engine.h"
 #include "liveness_to_safety.h"
 #include "neural_liveness.h"
 #include "output_file.h"
@@ -155,11 +154,6 @@ int ebmc_parse_optionst::doit()
     if(cmdline.isset("random-trace") || cmdline.isset("random-waveform"))
       return random_trace(cmdline, ui_message_handler);
 
-#ifndef _WIN32
-    if(cmdline.isset("ic3"))
-      return do_ic3(cmdline, ui_message_handler);
-#endif
-
     if(cmdline.isset("neural-liveness"))
       return do_neural_liveness(cmdline, ui_message_handler);
 

src/ebmc/ic3_engine.h

@@ -6,8 +6,10 @@ Author: Eugene Goldberg, [email protected]
 
 \*******************************************************************/
 
-#include <util/cmdline.h>
-#include <util/ui_message.h>
-
-int do_ic3(const cmdlinet &, ui_message_handlert &);
+#include "property_checker.h"
 
+property_checker_resultt ic3_engine(
+  const cmdlinet &,
+  transition_systemt &,
+  ebmc_propertiest &,
+  message_handlert &);

src/ebmc/property_checker.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include "dimacs_writer.h"
 #include "ebmc_error.h"
 #include "ebmc_solver_factory.h"
+#include "ic3_engine.h"
 #include "k_induction.h"
 #include "netlist.h"
 #include "output_file.h"
@@ -378,6 +379,15 @@ property_checker_resultt property_checker(
       return k_induction(
         cmdline, transition_system, properties, message_handler);
     }
+    else if(cmdline.isset("ic3"))
+    {
+#ifdef _WIN32
+      throw ebmc_errort() << "No support for IC3 on Windows";
+#else
+      return ic3_engine(
+        cmdline, transition_system, properties, message_handler);
+#endif
+    }
     else
     {
       // default engine is word-level BMC

src/ic3/ebmc_ic3_interface.hh

@@ -7,17 +7,23 @@ class ic3_enginet
 public:
   ic3_enginet(
     const cmdlinet &_cmdline,
-    ui_message_handlert &_ui_message_handler)
-    : cmdline(_cmdline), message(_ui_message_handler)
+    transition_systemt &_transition_system,
+    ebmc_propertiest &_properties,
+    message_handlert &_message_handler)
+    : cmdline(_cmdline),
+      transition_system(_transition_system),
+      properties(_properties),
+      message(_message_handler)
   {
   }
 
 protected:
   const cmdlinet &cmdline;
+  transition_systemt &transition_system;
+  using propertyt = ebmc_propertiest::propertyt;
+  ebmc_propertiest &properties;
   messaget message;
 
-  using propertyt = ebmc_propertiest::propertyt;
-  ebmc_propertiest properties;
   netlistt netlist;
 
 public:
@@ -29,7 +35,7 @@ public:
   bool const0,const1;
   bool orig_names;
 
-  int operator()();
+  property_checker_resultt operator()();
   void read_ebmc_input();  
   void find_prop_lit();
   void ebmc_form_latches();

src/ic3/m1ain.cc

@@ -49,12 +49,14 @@ long long gcount = 0;
        D O _ I C 3
 
   ====================*/
-int do_ic3(const cmdlinet &cmdline,
-	   ui_message_handlert &ui_message_handler)
-
+property_checker_resultt ic3_engine(
+  const cmdlinet &cmdline,
+  transition_systemt &transition_system,
+  ebmc_propertiest &properties,
+  message_handlert &message_handler)
 {
-  return(ic3_enginet(cmdline,ui_message_handler)());
-} /* end of function do_ic3 */
+  return(ic3_enginet(cmdline, transition_system, properties, message_handler)());
+} /* end of function ic3_engine */
 
 bool ic3_supports_property(const exprt &expr)
 {
@@ -82,7 +84,7 @@ bool ic3_supports_property(const exprt &expr)
 
    (functionall call reloading)
   =================================*/
-int ic3_enginet::operator()()
+property_checker_resultt ic3_enginet::operator()()
 
 {
 
@@ -91,12 +93,6 @@ int ic3_enginet::operator()()
   read_parameters();
 
   try    {
-    auto transition_system =
-      get_transition_system(cmdline, message.get_message_handler());
-
-    properties = ebmc_propertiest::from_command_line(
-      cmdline, transition_system, message.get_message_handler());
-
     // possibly apply liveness-to-safety
     if(cmdline.isset("liveness-to-safety"))
       liveness_to_safety(transition_system, properties);