diffblue · eigold · Jun 29, 2017 · May 24, 2017 · May 24, 2017 · May 24, 2017
diff --git a/regression/ebmc/ic3/exmp1/test.desc b/regression/ebmc/ic3/exmp1/test.desc
@@ -2,6 +2,6 @@ CORE
 pdtvispeterson.sv
 --ic3
 ^property HOLDS
-^verification is ok
+^inductive invariant verification is ok
 --
-^verification failed
+^inductive invariant verification failed
diff --git a/regression/ebmc/ic3/exmp2/test.desc b/regression/ebmc/ic3/exmp2/test.desc
@@ -2,6 +2,6 @@ CORE
 bobcount.sv
 --ic3
 ^property HOLDS
-^verification is ok
+^inductive invariant verification is ok
 --
-^verification failed
+^inductive invariant verification failed
diff --git a/regression/ebmc/ic3/exmp3/test.desc b/regression/ebmc/ic3/exmp3/test.desc
@@ -2,6 +2,6 @@ CORE
 viseisenberg.sv
 --ic3
 ^property FAILED
-^verification is ok
+^cex verification is ok
 --
-^verification failed
+^cex verification failed
diff --git a/regression/ebmc/ic3/exmp4/test.desc b/regression/ebmc/ic3/exmp4/test.desc
@@ -2,6 +2,6 @@ CORE
 visbakery.sv
 --ic3
 ^property FAILED
-^verification is ok
+^cex verification is ok
 --
-^verification failed
+^cex verification failed
diff --git a/regression/ebmc/ic3/exmp5/test.desc b/regression/ebmc/ic3/exmp5/test.desc
@@ -2,6 +2,6 @@ CORE
 ringp0.sv
 --ic3
 ^property FAILED
-^verification is ok
+^cex verification is ok
 --
-^verification failed
+^cex verification failed
diff --git a/regression/ebmc/ic3/exmp6/test.desc b/regression/ebmc/ic3/exmp6/test.desc
@@ -2,6 +2,6 @@ CORE
 eijks208o.sv
 --ic3
 ^property HOLDS
-^verification is ok
+^inductive invariant verification is ok
 --
-^verification failed
+^inductive invariant verification failed
diff --git a/regression/ebmc/ic3/exmp7/test.desc b/regression/ebmc/ic3/exmp7/test.desc
@@ -1,7 +1,7 @@
 CORE
 bobmiterbm1multi.sv
---ic3 --prop 1032
+--ic3 --property bobmiterbm1multi.property.1033
 ^property HOLDS
-^verification is ok
+^inductive invariant verification is ok
 --
-^verification failed
+^inductive invariant verification failed
diff --git a/regression/ebmc/ic3/exmp8/test.desc b/regression/ebmc/ic3/exmp8/test.desc
@@ -1,7 +1,7 @@
 CORE
 bobmiterbm1multi.sv
---ic3 --prop 1079
+--ic3 --property bobmiterbm1multi.property.1080
 ^property FAILED
-^verification is ok
+^cex verification is ok
 --
-^verification failed
+^cex verification failed
diff --git a/regression/ebmc/ic3/exmp9/test.desc b/regression/ebmc/ic3/exmp9/test.desc
@@ -1,7 +1,7 @@
 CORE
 sm98a7multi.sv
---ic3 --prop 1 --constr
+--ic3 --property sm98a7multi.property.2 --constr
 ^property FAILED
-^verification is ok
+^cex verification is ok
 --
-^verification failed
+^cex verification failed
diff --git a/regression/ebmc/ic3/non_inductive1/test.desc b/regression/ebmc/ic3/non_inductive1/test.desc
@@ -1,6 +1,7 @@
 CORE
 non_inductive.sv
---ic3 --prop 0
+--ic3 --property main.property.p0
 ^property HOLDS$
-^verification is ok
+^inductive invariant verification is ok
 --
+^inductive invariant verification failed
diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile
@@ -9,7 +9,7 @@ SRC = diameter.cpp main.cpp diatest.cpp show_properties.cpp \
 OBJ+= $(CBMC)/src/util/util$(LIBEXT) \
       $(CBMC)/src/langapi/langapi$(LIBEXT) \
       $(CBMC)/src/ansi-c/string_constant$(OBJEXT) \
-      $(CBMC)/src/ansi-c/c_types$(OBJEXT) \
+      $(CBMC)/src/util/c_types$(OBJEXT) \
       $(CBMC)/src/solvers/solvers$(LIBEXT) \
       $(CBMC)/src/big-int/big-int$(LIBEXT) \
       ../trans-netlist/trans-netlist$(LIBEXT) \

diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp
@@ -262,8 +262,12 @@ void ebmc_parse_optionst::help()
     " --k-induction                     do k-induction with k=bound\n"
     " --bdd                             use (unbounded) BDD engine\n"
     " --ic3 [options]                   use IC3 engine with options described below\n"
-    "       --prop <nr>                   check property number <nr>\n"
-    "       --constr                      use constraints specified in 'file.cnstr'\n"
+    "       --property <nm>                  check property named <nm>\n"
+    "       --constr                         use constraints specified in 'file.cnstr'\n"
+    "       --h                              print out help information\n"
+    "       --new-mode                       new mode is switched on\n"
+    "       --aiger                          print out the instance in aiger format\n"
+
     //" --interpolation                   use bit-level interpolants\n"
     //" --interpolation-word              use word-level interpolants\n"
     //" --diameter                        perform recurrence diameter test\n"

diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h
@@ -32,7 +32,7 @@ class ebmc_parse_optionst:public parse_options_baset
     "(reset):"
     "(version)(verilog-rtl)(verilog-netlist)"
     "(compute-interpolant)(interpolation)(interpolation-vmcai)"
-    "(ic3)(prop):(constr)(h)"
+    "(ic3)(property):(constr)(h)(new-mode)(aiger)"
     "(interpolation-word)(interpolator):(bdd)"
     "(smt1)(smt2)(boolector)(z3)(cvc4)(yices)(mathsat)(prover)(lifter)"
     "(aig)(stop-induction)(stop-minimize)(start):(coverage)(naive)"

diff --git a/src/hw-cbmc/hw_cbmc_parse_options.cpp b/src/hw-cbmc/hw_cbmc_parse_options.cpp
@@ -250,6 +250,9 @@ Function: hw_cbmc_parse_optionst::help
 
 void hw_cbmc_parse_optionst::help()
 {
+  std::cout <<
+    "* *  hw-cbmc is protected in part by U.S. patent 7,225,417  * *";
+
   cbmc_parse_optionst::help();
 
   std::cout <<

diff --git a/src/ic3/Makefile b/src/ic3/Makefile
@@ -30,7 +30,8 @@ SEQ_CIRC = $(OBJ_DIR)/p1rint_blif.o $(OBJ_DIR)/p2rint_blif.o $(OBJ_DIR)/finish_g
            $(OBJ_DIR)/circuit.o $(OBJ_DIR)/a4dd_spec_buffs.o  $(OBJ_DIR)/a5dd_spec_buffs.o  \
            $(OBJ_DIR)/l0ast_touch.o $(OBJ_DIR)/l1ast_touch.o 
 
-OBJ_ROOT = $(OBJ_DIR)/r7ead_input.o $(OBJ_DIR)/r6ead_input.o  \
+OBJ_ROOT = $(OBJ_DIR)/m5y_aiger_print.o \
+           $(OBJ_DIR)/m4y_aiger_print.o  $(OBJ_DIR)/r7ead_input.o $(OBJ_DIR)/r6ead_input.o  \
            $(OBJ_DIR)/g2ate_ord.o $(OBJ_DIR)/i4nit_sat_solvers.o $(OBJ_DIR)/l1ift_states.o \
            $(OBJ_DIR)/r5ead_input.o  $(OBJ_DIR)/r4ead_input.o $(OBJ_DIR)/c4oi.o \
            $(OBJ_DIR)/c5tg.o $(OBJ_DIR)/c2tg.o $(OBJ_DIR)/r3ead_input.o \

diff --git a/src/ic3/README b/src/ic3/README
@@ -2,12 +2,8 @@
    a variation of Aaron Bradley's IC3.  It is incorporated into
    ebmc. To invoke IC3, run
 
-   ebmc verilog_file --ic3
+   ebmc verilog_file --ic3 [options]
 
-*) Integration is not over yet. This current version is missing two
-   features that has been implemented in the stand-alone version.
-   The current version assumes that the input verilog file specifies
-   only one property and has no constraints.
 
 
 

diff --git a/src/ic3/aux_types.hh b/src/ic3/aux_types.hh
@@ -98,27 +98,39 @@ struct OblTableElem {
 typedef std::vector <OblTableElem> OblTable;
 
 
+
 //
 //  PrQueue
 //
 struct PqElem {
-  int tf_ind; // time frame index
+  int tf_ind; // time frame index, the same value as in OblTableElem
+  int dist; //  the same value as in OblTableElem
   int tbl_ind; // index of this element in 'Obl_table'
+  int sort_mode; // specifies the sorting mode
 };
 
 
-class pq_compare
-{
+class pq_compare {
 public:
   bool operator() (PqElem &A, PqElem &B)
   {
-    return (A.tf_ind  > B.tf_ind);
+    if (A.tf_ind  > B.tf_ind) return(true);
+    if (A.tf_ind  < B.tf_ind) return(false);
+    if (A.dist > B.dist) return(true);
+    if (A.sort_mode == 0) return(false);
+    if (A.sort_mode == 1) {
+      if (A.tbl_ind > B.tbl_ind) return(true);
+      else return(false);}
+    assert(A.sort_mode == 2);
+    if (A.tbl_ind < B.tbl_ind) return(true);
+    else return(false);
   }
 };
 
 typedef std::priority_queue<PqElem,std::vector <PqElem>, pq_compare> PrQueue;
 
 
+
 //
 //   ClauseInfo
 //
@@ -172,7 +184,10 @@ struct TimeFrame
 
   int num_rcnt_ctis; // number of Cti-s generated in the current time frame 
                      // when processing the latest time frame
-
+
+  int num_seen_cls; // number of new cti or ctg clauses that are already in formula F
+  int num_redund_cls; // number of new cti/ctg clauses that are already in formula F
+                      // and cannot be added to any time frame
 
 };
 

diff --git a/src/ic3/build_prob/g0en_cnf.cc b/src/ic3/build_prob/g0en_cnf.cc
@@ -86,8 +86,8 @@ void CompInfo::gen_out_fun(DNF &H,int shift,bool short_version)
     if (G.gate_type == INPUT) continue;
     if (G.gate_type == LATCH) continue;
 // skip the gates that are not part of the output function
-    if (G.flags.output_function == 0) 
-      if (G.flags.fun_constr == 0) continue; 
+    if (G.flags.output_function == 0)
+       if ((G.flags.fun_constr == 0) && (G.flags.tran_constr == 0)) 
     if (short_version)
 // skip the gates that are shared by transition relation and out function
       if (G.flags.transition) continue; 

diff --git a/src/ic3/build_prob/g2en_cnf.cc b/src/ic3/build_prob/g2en_cnf.cc
@@ -202,7 +202,9 @@ void CompInfo::set_constr_flag()
     bool tran_flag,fun_flag;
 
     gen_constr_coi(Gates,tran_flag,fun_flag,Stack);
-    assert(tran_flag || fun_flag);
+    tran_flag = true;
+    fun_flag = true;  
+
     mark_constr_gates(Gates,tran_flag,fun_flag);
     if (tran_flag) Constr_gates[gate_ind].tran_coi = 1;
     else Constr_gates[gate_ind].tran_coi = 0;

diff --git a/src/ic3/build_prob/g3en_cnf.cc b/src/ic3/build_prob/g3en_cnf.cc
@@ -66,10 +66,10 @@ void CompInfo::gen_constr_coi(CUBE &Gates,bool &tran_flag,bool &fun_flag,
       fun_flag = true;
       skip = true;
     }
-    if (G.flags.transition > 0) {
+
+    if (G.flags.transition > 0) 
       tran_flag = true;
-      skip = true;
-    }
+
     if (skip) continue;
     Gates.push_back(gate_ind);    
 

diff --git a/src/ic3/c0ex.cc b/src/ic3/c0ex.cc
@@ -59,6 +59,9 @@ bool CompInfo::check_one_state_cex()
 
   add_bad_states(Gen_sat);
 
+  // add constraints
+  accept_constrs(Gen_sat);
+
 
   bool sat_form = check_sat1(Gen_sat);
   bool ok = true;
@@ -157,13 +160,34 @@ void CompInfo::add_neg_prop(SatSolver &Slvr)
   accept_new_clause(Slvr,C);
 } /* end of function add_neg_prop */
 
-/*=====================================
+/*==================================
 
-  A D D _ B A D _ S T A T E S
+    A D D _ B A D _ S T A T E S
 
-  ====================================*/
+  ================================*/
 void CompInfo::add_bad_states(SatSolver &Slvr)
 {
   add_neg_prop(Slvr);
 
 } /* end of function add_bad_states */
+
+/*===================================
+
+    A C C E P T _ C O N S T R S
+
+ ==================================*/
+void CompInfo::accept_constrs(SatSolver &Slvr)
+{
+  for (size_t i=0; i < Constr_ilits.size(); i++) {
+    CLAUSE U;
+    U.push_back(Constr_ilits[i]);
+    accept_new_clause(Slvr,U);
+  }
+
+  SCUBE::iterator pnt;
+  for (pnt = Constr_nilits.begin(); pnt != Constr_nilits.end(); pnt++) {
+    CLAUSE U;
+    U.push_back(*pnt);
+    accept_new_clause(Slvr,U);
+  }
+} /* end of function add_bad_states */
diff --git a/src/ic3/c2tg.cc b/src/ic3/c2tg.cc
@@ -78,3 +78,21 @@ int CompInfo::latest_succ_tf_ind(int tf_ind,CLAUSE &C)
 
   return(tf_lind);
 } /* end of function latest_succ_tf_ind */
+
+/*=======================================
+
+         F O R M _ N X T _ C U B E
+
+  =====================================*/
+void CompInfo::form_nxt_cube(CUBE &Nxt_cube,CLAUSE &C)
+{
+
+  for (size_t i=0;i < C.size(); i++) {
+    int var_ind = abs(C[i])-1;
+    int nxt_var_ind = Pres_to_next[var_ind];
+    assert(nxt_var_ind >=0);
+    int lit = (C[i] > 0)?-(nxt_var_ind+1):(nxt_var_ind+1);
+    Nxt_cube.push_back(lit);
+  }
+
+} /* end of function form_nxt_cube */
diff --git a/src/ic3/c5tg.cc b/src/ic3/c5tg.cc
@@ -81,8 +81,11 @@ void CompInfo::lift_ctg_state(CUBE &Ctg_cube,CUBE &Ctg_st,CUBE &Inps,
   add_assumps1(Assmps,Inps);
 
 
-  Mlit act_lit;  
-  add_cls_excl_st_cube(act_lit,Lgs_sat,Nst_cube);
+  Mlit act_lit;
+  if (standard_mode) 
+    add_cls_excl_st_cube(act_lit,Lgs_sat,Nst_cube,false);
+  else
+    add_cls_excl_st_cube(act_lit,Lgs_sat,Nst_cube,true);
 
   Assmps.push(act_lit);
   add_assumps2(Assmps,Ctg_st);