extract property_checker function

This extracts a function for selecting an engine and checking the given
properties.

The function only performs word-level and bit-level BMC at the moment; code
for triggering the other engines will move gradually.

Author: kroening

src/ebmc/Makefile

@@ -22,6 +22,7 @@ SRC = \
       neural_liveness.cpp \
       output_file.cpp \
       output_verilog.cpp \
+      property_checker.cpp \
       random_traces.cpp \
       ranking_function.cpp \
       report_results.cpp \

src/ebmc/ebmc_base.cpp

@@ -23,7 +23,6 @@ Author: Daniel Kroening, [email protected]
 #include <trans-word-level/trans_trace_word_level.h>
 #include <trans-word-level/unwind.h>
 
-#include "bmc.h"
 #include "dimacs_writer.h"
 #include "ebmc_error.h"
 #include "ebmc_solver_factory.h"
@@ -470,95 +469,3 @@ int ebmc_baset::do_compute_ct()
 
   return 0;
 }
-
-/*******************************************************************\
-
-Function: ebmc_baset::do_word_level_bmc
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-int ebmc_baset::do_word_level_bmc()
-{
-  auto solver_factory = ebmc_solver_factory(cmdline);
-
-  bool convert_only = cmdline.isset("smt2") || cmdline.isset("outfile") ||
-                      cmdline.isset("show-formula");
-
-  int result = 0;
-
-  try
-  {
-    if(cmdline.isset("max-bound"))
-    {
-      if(convert_only)
-        throw "please set a specific bound";
-
-      const std::size_t max_bound =
-        unsafe_string2size_t(cmdline.get_value("max-bound"));
-
-      for(bound = 1; bound <= max_bound; bound++)
-      {
-        message.status() << "Doing BMC with bound " << bound << messaget::eom;
-
-#if 0
-        const namespacet ns(transition_system.symbol_table);
-        CHECK_RETURN(trans_expr.has_value());
-        ::unwind(*trans_expr, *message_handler, solver, bound+1, ns, true);
-        result=finish_word_level_bmc(solver);
-#endif
-      }
-
-      const namespacet ns(transition_system.symbol_table);
-      report_results(cmdline, properties, ns, message.get_message_handler());
-    }
-    else
-    {
-      if(get_bound())
-        return 1;
-
-      if(!convert_only)
-        if(properties.properties.empty())
-          throw "no properties";
-
-      bmc(
-        bound,
-        convert_only,
-        transition_system,
-        properties,
-        solver_factory,
-        message.get_message_handler());
-
-      if(!convert_only)
-      {
-        const namespacet ns(transition_system.symbol_table);
-        report_results(cmdline, properties, ns, message.get_message_handler());
-        result = properties.exit_code();
-      }
-    }
-  }
-
-  catch(const char *e)
-  {
-    message.error() << e << messaget::eom;
-    return 10;
-  }
-
-  catch(const std::string &e)
-  {
-    message.error() << e << messaget::eom;
-    return 10;
-  }
-
-  catch(int)
-  {
-    return 10;
-  }
-
-  return result;
-}

src/ebmc/ebmc_base.h

@@ -64,7 +64,6 @@ class ebmc_baset
 public:
   int do_compute_ct();
   int do_bit_level_bmc();
-  int do_word_level_bmc();
 };
 
 #endif

src/ebmc/ebmc_parse_options.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]
 #include "k_induction.h"
 #include "liveness_to_safety.h"
 #include "neural_liveness.h"
+#include "property_checker.h"
 #include "random_traces.h"
 #include "ranking_function.h"
 #include "show_trans.h"
@@ -306,7 +307,11 @@ int ebmc_parse_optionst::doit()
       if(cmdline.isset("aig") || cmdline.isset("dimacs"))
         return ebmc_base.do_bit_level_bmc();
       else
-        return ebmc_base.do_word_level_bmc(); // default
+        return property_checker(
+          cmdline,
+          ebmc_base.transition_system,
+          ebmc_base.properties,
+          ui_message_handler);
     }
   }
   catch(const ebmc_errort &ebmc_error)

src/ebmc/ebmc_solver_factory.h

@@ -16,7 +16,7 @@ Author: Daniel Kroening, [email protected]
 #include <solvers/decision_procedure.h>
 #include <solvers/prop/prop.h>
 
-#include <iosfwd>
+#include <fstream>
 #include <memory>
 
 class ebmc_solvert final

src/ebmc/property_checker.cpp

@@ -0,0 +1,124 @@
+/*******************************************************************\
+
+Module: EBMC Property Checker
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "property_checker.h"
+
+#include <util/string2int.h>
+
+#include "bmc.h"
+#include "ebmc_error.h"
+#include "ebmc_solver_factory.h"
+#include "report_results.h"
+
+int word_level_bmc(
+  const cmdlinet &cmdline,
+  const transition_systemt &transition_system,
+  ebmc_propertiest &properties,
+  message_handlert &message_handler)
+{
+  auto solver_factory = ebmc_solver_factory(cmdline);
+
+  bool convert_only = cmdline.isset("smt2") || cmdline.isset("outfile") ||
+                      cmdline.isset("show-formula");
+
+  int result = 0;
+
+  try
+  {
+    if(cmdline.isset("max-bound"))
+    {
+      if(convert_only)
+        throw ebmc_errort() << "please set a specific bound";
+
+      const std::size_t max_bound =
+        unsafe_string2size_t(cmdline.get_value("max-bound"));
+
+      for(std::size_t bound = 1; bound <= max_bound; bound++)
+      {
+        messaget message{message_handler};
+        message.status() << "Doing BMC with bound " << bound << messaget::eom;
+
+#if 0
+        const namespacet ns(transition_system.symbol_table);
+        CHECK_RETURN(trans_expr.has_value());
+        ::unwind(*trans_expr, *message_handler, solver, bound+1, ns, true);
+        result=finish_word_level_bmc(solver);
+#endif
+      }
+
+      const namespacet ns(transition_system.symbol_table);
+      report_results(cmdline, properties, ns, message_handler);
+    }
+    else
+    {
+      std::size_t bound;
+
+      if(cmdline.isset("bound"))
+      {
+        bound = unsafe_string2unsigned(cmdline.get_value("bound"));
+      }
+      else
+      {
+        messaget message{message_handler};
+        message.warning() << "using default bound 1" << messaget::eom;
+        bound = 1;
+      }
+
+      if(!convert_only)
+        if(properties.properties.empty())
+          throw "no properties";
+
+      bmc(
+        bound,
+        convert_only,
+        transition_system,
+        properties,
+        solver_factory,
+        message_handler);
+
+      if(!convert_only)
+      {
+        const namespacet ns(transition_system.symbol_table);
+        report_results(cmdline, properties, ns, message_handler);
+        result = properties.exit_code();
+      }
+    }
+  }
+
+  catch(const char *e)
+  {
+    messaget message{message_handler};
+    message.error() << e << messaget::eom;
+    return 10;
+  }
+
+  catch(const std::string &e)
+  {
+    messaget message{message_handler};
+    message.error() << e << messaget::eom;
+    return 10;
+  }
+
+  catch(int)
+  {
+    return 10;
+  }
+
+  return result;
+}
+
+int property_checker(
+  const cmdlinet &cmdline,
+  const transition_systemt &transition_system,
+  ebmc_propertiest &properties,
+  message_handlert &message_handler)
+{
+  // default engine is word-level BMC
+  return word_level_bmc(
+    cmdline, transition_system, properties, message_handler);
+}

src/ebmc/property_checker.h

@@ -0,0 +1,21 @@
+/*******************************************************************\
+
+Module: EBMC Property Checker
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_EBMC_PROPERTY_CHECKER_H
+#define CPROVER_EBMC_PROPERTY_CHECKER_H
+
+#include "ebmc_properties.h"
+#include "transition_system.h"
+
+int property_checker(
+  const cmdlinet &,
+  const transition_systemt &,
+  ebmc_propertiest &,
+  message_handlert &);
+
+#endif