liveness engine

Author: kroening

src/ebmc/Makefile

@@ -19,6 +19,7 @@ SRC = \
       k_induction.cpp \
       liveness_to_safety.cpp \
       live_signal.cpp \
+      liveness_engine.cpp \
       main.cpp \
       netlist.cpp \
       neural_liveness.cpp \

src/ebmc/ebmc_parse_options.h

@@ -40,6 +40,7 @@ class ebmc_parse_optionst:public parse_options_baset
         "(compute-interpolant)(interpolation)(interpolation-vmcai)"
         "(ic3)(property):(constr)(h)(new-mode)(aiger)"
         "(interpolation-word)(interpolator):(bdd)"
+        "(liveness)"
         "(ranking-function):"
         "(smt2)(bitwuzla)(boolector)(cvc3)(cvc4)(cvc5)(mathsat)(yices)(z3)"
         "(minisat)(cadical)"

src/ebmc/liveness_engine.cpp

@@ -0,0 +1,18 @@
+/*******************************************************************\
+
+Module: Liveness Engine
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include "liveness_engine.h"
+
+property_checker_resultt liveness_engine(
+  const cmdlinet &cmdline,
+  transition_systemt &transition_system,
+  ebmc_propertiest &properties,
+  message_handlert &message_handler)
+{
+  return property_checker_resultt{properties};
+}

src/ebmc/liveness_engine.h

@@ -0,0 +1,20 @@
+/*******************************************************************\
+
+Module: Liveness Engine
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_EBMC_LIVENESS_ENGINE_H
+#define CPROVER_EBMC_LIVENESS_ENGINE_H
+
+#include "property_checker.h"
+
+property_checker_resultt liveness_engine(
+  const cmdlinet &,
+  transition_systemt &,
+  ebmc_propertiest &,
+  message_handlert &);
+
+#endif

src/ebmc/property_checker.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #include "ebmc_error.h"
 #include "ebmc_solver_factory.h"
 #include "k_induction.h"
+#include "liveness_engine.h"
 #include "netlist.h"
 #include "output_file.h"
 #include "report_results.h"
@@ -378,6 +379,11 @@ property_checker_resultt property_checker(
       return k_induction(
         cmdline, transition_system, properties, message_handler);
     }
+    else if(cmdline.isset("liveness"))
+    {
+      return liveness_engine(
+        cmdline, transition_system, properties, message_handler);
+    }
     else
     {
       // default engine is word-level BMC