New IC3: AIG-based IC3/PDR engine using CBMC SAT solvers

Add a new IC3/PDR model checking engine in src/new-ic3/ that operates
directly on the AIG netlist from trans-netlist, using CBMC's SAT
solvers. Invoked with --new-ic3.

The implementation follows the standard IC3/PDR algorithm:
- Incremental frame-based invariant learning
- Proof obligations with priority queue
- MIC generalization (literal dropping)
- Frame propagation with convergence check
- Dedicated is_inductive check for clause pushing

Uses satcheck_no_simplifiert to avoid preprocessing interactions
with gate_and encoding.

Known limitation: the default netlist encoding (convert_trans_to_netlist)
can produce AIGs where some properties appear spuriously 1-inductive.
Using --simple-netlist avoids this. Performance is limited by
non-incremental SAT solving (new solver per query).

Author: kroening

src/Makefile

@@ -1,5 +1,5 @@
 DIRS = ebmc hw-cbmc temporal-logic trans-word-level trans-netlist \
-       verilog vhdl smvlang ic3 aiger vlindex
+       verilog vhdl smvlang ic3 aiger vlindex new-ic3
 
 CPROVER_DIR:=../lib/cbmc/src
 
@@ -15,7 +15,7 @@ $(patsubst %, %.dir, $(DIRS)):
 vhdl.dir: cprover.dir
 
 ebmc.dir: trans-word-level.dir trans-netlist.dir verilog.dir vhdl.dir \
-      smvlang.dir aiger.dir temporal-logic.dir cprover.dir
+      smvlang.dir aiger.dir temporal-logic.dir cprover.dir new-ic3.dir
 
 ifneq ($(BUILD_ENV),MSVC)
 ebmc.dir: ic3.dir

src/ebmc/Makefile

@@ -56,7 +56,8 @@ OBJ+= $(CPROVER_DIR)/util/util$(LIBEXT) \
       ../trans-word-level/trans-word-level$(LIBEXT) \
       ../aiger/aiger$(LIBEXT) \
       ../smvlang/smvlang$(LIBEXT) \
-      ../verilog/verilog$(LIBEXT)
+      ../verilog/verilog$(LIBEXT) \
+      ../new-ic3/new-ic3$(LIBEXT)
 
 ifneq ($(BUILD_ENV),MSVC)
 OBJ += ../ic3/libic3$(LIBEXT)

src/ebmc/ebmc_parse_options.cpp

@@ -420,6 +420,7 @@ void ebmc_parse_optionst::help()
     "    {y--constr}                 \t use constraints specified in 'file.cnstr'\n"
     "    {y--new-mode}               \t new mode is switched on\n"
     "    {y--aiger}                  \t print out the instance in aiger format\n"
+    " {y--new-ic3}                   \t use new IC3 engine (AIG-based)\n"
     " {y--random-traces}             \t generate random traces\n"
     "    {y--traces} {unumber}       \t generate the given number of traces\n"
     "    {y--random-seed} {unumber}  \t use the given random seed\n"

src/ebmc/ebmc_parse_options.h

@@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "ebmc_version.h"
 
-class ebmc_parse_optionst:public parse_options_baset
+class ebmc_parse_optionst : public parse_options_baset
 {
 public:
   virtual int doit();
@@ -38,7 +38,7 @@ class ebmc_parse_optionst:public parse_options_baset
         "(reset):(ignore-initial)(initial-zero)"
         "(version)(verilog-rtl)(verilog-netlist)"
         "(compute-interpolant)(interpolation)(interpolation-vmcai)"
-        "(ic3)(property):(constr)(h)(new-mode)(aiger)"
+        "(ic3)(new-ic3)(property):(constr)(h)(new-mode)(aiger)"
         "(interpolation-word)(interpolator):(bdd)"
         "(ranking-function):"
         "(smt2)(bitwuzla)(boolector)(cvc3)(cvc4)(cvc5)(mathsat)(yices)(z3)"
@@ -60,11 +60,13 @@ class ebmc_parse_optionst:public parse_options_baset
   {
   }
 
-  virtual ~ebmc_parse_optionst() { }
-  
+  virtual ~ebmc_parse_optionst()
+  {
+  }
+
 protected:
   void register_languages();
-  
+
   ui_message_handlert ui_message_handler;
 };
 

src/ebmc/property_checker.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <util/output_file.h>
 #include <util/string2int.h>
 
+#include <new-ic3/new_ic3_engine.h>
 #include <solvers/sat/satcheck.h>
 #include <trans-netlist/trans_trace_netlist.h>
 #include <trans-netlist/unwind_netlist.h>
@@ -368,18 +369,18 @@ property_checker_resultt property_checker(
   ebmc_propertiest &properties,
   message_handlert &message_handler)
 {
-  bool use_heuristic_engine = !cmdline.isset("bdd") && !cmdline.isset("aig") &&
-                              !cmdline.isset("k-induction") &&
-                              !cmdline.isset("ic3") && !cmdline.isset("bound");
+  bool use_heuristic_engine =
+    !cmdline.isset("bdd") && !cmdline.isset("aig") &&
+    !cmdline.isset("k-induction") && !cmdline.isset("ic3") &&
+    !cmdline.isset("new-ic3") && !cmdline.isset("bound");
 
   if(cmdline.isset("k-induction") || use_heuristic_engine)
   {
     // The step case of k-induction can't do $past
     instrument_past(transition_system, properties);
   }
 
-  auto result = [&]() -> property_checker_resultt
-  {
+  auto result = [&]() -> property_checker_resultt {
     if(cmdline.isset("bdd") || cmdline.isset("show-bdds"))
     {
       return bdd_engine(
@@ -405,6 +406,11 @@ property_checker_resultt property_checker(
         cmdline, transition_system, properties, message_handler);
 #endif
     }
+    else if(cmdline.isset("new-ic3"))
+    {
+      return new_ic3_engine(
+        cmdline, transition_system, properties, message_handler);
+    }
     else if(cmdline.isset("bound"))
     {
       // word-level BMC

src/new-ic3/Makefile

@@ -0,0 +1,13 @@
+SRC = new_ic3_engine.cpp \
+      #empty line
+
+include ../config.inc
+include ../common
+
+all: new-ic3$(LIBEXT)
+
+clean:
+	$(RM) *.o *.d new-ic3$(LIBEXT)
+
+new-ic3$(LIBEXT): $(OBJ)
+	$(LINKLIB)