Ic3 bugs: removed bugs, added new features

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

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

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

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

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

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

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

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

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

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

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"

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)"

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 \

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.
 
 
 

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
 
 };
 

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; 

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;

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);    
 

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 */

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);

src/ic3/e1xclude_state.cc

@@ -44,35 +44,34 @@ void CompInfo::exclude_state_cube(CNF &G,int &min_tf,CUBE &St0_cube,CUBE &Inps0)
       printf("Pr_queue.size() = %d\n",(int) Pr_queue.size());
     }
 
-    int obl_tf = Pr_queue.top().tf_ind;
+    int curr_tf = Pr_queue.top().tf_ind;
     int tbl_ind = Pr_queue.top().tbl_ind;
 
     if (verbose > 1)
-      printf("obl_tf = %d, tbl_ind = %d, min_tf = %d\n",obl_tf,tbl_ind, min_tf);
+      printf("curr_tf = %d, tbl_ind = %d, min_tf = %d\n",curr_tf,tbl_ind, min_tf);
 
     CUBE St_cube  =  Obl_table[tbl_ind].St_cb;
     char st_descr = Obl_table[tbl_ind].st_descr;
 
 
-    if (obl_tf == 0) 
+    if (curr_tf == 0) 
       if (cont_init_states(St_cube)) return;
 
     int dist = Obl_table[tbl_ind].dist;
     int st_ind = tf_lind + 1 - dist;
-
-    curr_tf = obl_tf;
+
     int succ_ind = Obl_table[tbl_ind].succ_ind;
-
-    bool ok = oblig_is_active(obl_tf+1,St_cube);
+  
+    bool ok = oblig_is_active(curr_tf+1,St_cube);
 
     if (!ok) {
       if (st_descr == OLD_STATE) triv_old_st_cnt++;
       Pr_queue.pop();     
-      if (succ_ind < 0) form_res_cnf(G,obl_tf+1,St_cube);
+      if (succ_ind < 0) form_res_cnf(G,curr_tf+1,St_cube);
       continue;}
 
 
-    if (obl_tf < min_tf) min_tf = obl_tf;
+    if (curr_tf < min_tf) min_tf = curr_tf;
 
 
 
@@ -87,21 +86,30 @@ void CompInfo::exclude_state_cube(CNF &G,int &min_tf,CUBE &St0_cube,CUBE &Inps0)
 	std::cout  << C << std::endl;
       }
 
-
-      if (obl_tf + 2 < tf_lind + 1) {
-	CUBE Inps = Obl_table[tbl_ind].Inp_assgn;
-	add_new_elem(St_cube,Inps,obl_tf+2,dist,succ_ind,OLD_STATE);
+      if (succ_ind == -1) 
+	G.push_back(C);
+
+  // the set of obligations is not empty yet
+
+      int tf_ind1 = curr_tf+1;
+
+      if (standard_mode)
+	tf_ind1 = push_on_the_fly(curr_tf+1,C,st_descr);
+
+      add_fclause1(C,tf_ind1,st_descr);
+
+      if (standard_mode) {
+	if (tf_ind1 <= tf_lind) {
+	  CUBE Inps = Obl_table[tbl_ind].Inp_assgn;
+	  add_new_elem(St_cube,Inps,tf_ind1,dist,succ_ind,OLD_STATE);
+	}
       }
+      else
+	if (tf_ind1 < tf_lind) {
+	  CUBE Inps = Obl_table[tbl_ind].Inp_assgn;
+	  add_new_elem(St_cube,Inps,tf_ind1+1,dist,succ_ind,OLD_STATE);
+	}
 
-
-      if (succ_ind == -1) {
-	G.push_back(C);
-	add_fclause1(C,curr_tf+1,st_descr);	 
-	continue;
-      } 
-
-      // the set of obligations is not empty yet      
-      add_fclause1(C,curr_tf+1,st_descr);
       continue;
     }
 

src/ic3/e2xclude_state.cc

@@ -69,6 +69,7 @@ bool CompInfo::find_ind_subclause_cti(CLAUSE &C,SatSolver &Slvr,
     }
 
     // inductive clause is not found yet
+    if (standard_mode) return(false);
     CUBE St;
     extr_cut_assgns1(St,Pres_svars,Slvr);
 
@@ -151,7 +152,7 @@ void CompInfo::adjust_clause1(CLAUSE &C,CUBE &St)
     printf("%*c",9,' ');
     printf("expand_clause\n");
   }
-  htable_lits.change_marker(); // increment or reset the hash table marker 
+  htable_lits.change_marker(); 
   htable_lits.started_using();
 
   int marker = htable_lits.marker;