Replacing C-like input/output with C++ style code, some other changes

regression/ebmc/BDD2/main.sv

@@ -7,7 +7,7 @@ module main(input clk, input [31:0] a);
       counter=counter+a;
 
   initial counter=0;
-  
+
   my_prop1: assert property (counter<199); // should pass
   my_prop2: assert property (counter<198); // should fail
 

src/ebmc/ebmc_parse_options.cpp

@@ -257,6 +257,7 @@ void ebmc_parse_optionst::help()
     " --property <id>                   check the property with given ID\n"
     " -I path                           set include path\n"
     " --reset <expr>                    set up module reset\n"
+    " --verbosity <nr>                  set verbosity level (default: 6)\n"
     "\n"
     "Methods:\n"
     " --k-induction                     do k-induction with k=bound\n"

src/ic3/Makefile

@@ -23,7 +23,7 @@ INC_DIR = -I . -I build_prob -I seq_circ -I $(MINISAT_INC) -I $(CBMC)/src -I ../
 OBJ_DIR = .
 
 BUILD_PROB =   $(OBJ_DIR)/g3en_cnf.o  $(OBJ_DIR)/g0en_cnf.o $(OBJ_DIR)/g1en_cnf.o \
-               $(OBJ_DIR)/g2en_cnf.o $(OBJ_DIR)/assign_indexes.o $(OBJ_DIR)/build_arrays.o
+               $(OBJ_DIR)/g2en_cnf.o $(OBJ_DIR)/assign_indices.o $(OBJ_DIR)/build_arrays.o
 
 SEQ_CIRC = $(OBJ_DIR)/p1rint_blif.o $(OBJ_DIR)/p2rint_blif.o $(OBJ_DIR)/finish_gate.o \
            $(OBJ_DIR)/a2dd_gate.o  $(OBJ_DIR)/a3dd_gate.o  $(OBJ_DIR)/c2irc_util.o \
@@ -52,7 +52,7 @@ OBJ_ROOT = $(OBJ_DIR)/m5y_aiger_print.o \
 
 OBJ =      $(OBJ_ROOT) $(BUILD_PROB) $(SEQ_CIRC)
 
-H_FILES1 = m0ic3.hh dnf_io.hh  m2ethods.hh aux_types.hh i5nline.hh
+H_FILES1 = m0ic3.hh dnf_io.hh  m2ethods.hh aux_types.hh i5nline.hh s0hared_consts.hh
 H_FILES2 = ccircuit.hh ebmc_ic3_interface.hh more_fun_prot.hh
 $(OBJ_DIR)/%.o : %.cc  $(H_FILES1) $(H_FILES2)
 	$(CXX) -c $(CXXFLAGS)  $< -o $@

src/ic3/build_prob/assign_indexes.cc → src/ic3/build_prob/assign_indices.cc

@@ -88,10 +88,10 @@ void find_latch(Circuit *N,Gate &G,int &latch_ind)
 
 /*=============================================
 
-  A S S I G N _ V A R _ I N D E X E S
+  A S S I G N _ V A R _ I N D I C E S 
 
   =============================================*/
-void CompInfo::assign_var_indexes()
+void CompInfo::assign_var_indices()
 {
 
   Gate_to_var.assign(N->Gate_list.size(),-1);
@@ -101,4 +101,4 @@ void CompInfo::assign_var_indexes()
   }
 
   num_circ_vars = curr_index-1;
-} /* end of function assign_var_indexes */
+} /* end of function assign_var_indices */

src/ic3/build_prob/g0en_cnf.cc

@@ -17,24 +17,19 @@ Author: Eugene Goldberg, [email protected]
 #include "ccircuit.hh"
 #include "m0ic3.hh"
 
-int debug_flag=0;
-
 /*======================
 
   G E N _ C N F S
 
   =====================*/
 void  CompInfo::gen_cnfs(const char *fname,bool print_flag)
 {  
-  assign_var_indexes();
+  assign_var_indices();
 
-  char fname1[MAX_NAME];
 
   if (print_flag) {
     // print index file
-    strcpy(fname1,fname);
-    strcat(fname1,".ind");
-    print_var_indexes(fname1);
+    print_var_indices(std::string(fname)+".ind");
   }
 
   gen_initial_state_cubes();
@@ -108,11 +103,11 @@ void CompInfo::gen_out_fun(DNF &H,int shift,bool short_version)
 	add_truth_table_gate_cubes(H,gate_ind,shift);                 
 	break;
       case COMPLEX: 
-        printf("complex gates are not allowed\n");
-	exit(1);
+	M->error() << "complex gates are not allowed" << M->eom;
+	throw(ERROR1);
       default:   
-	printf("wrong gate type\n");
-	exit(1);
+	M->error() << "wrong gate type" << M->eom;
+	throw(ERROR1);
       }
   }
 
@@ -162,7 +157,7 @@ void  CompInfo::gen_initial_state_cubes()
 void  CompInfo::add_const_gate_cube(DNF &F,int gate_ind,int shift)
 {
 
-  // form indexes 
+  // form indices 
   Gate &G =  N->Gate_list[gate_ind];
 
   int var_ind = Gate_to_var[gate_ind] + shift;
@@ -171,7 +166,6 @@ void  CompInfo::add_const_gate_cube(DNF &F,int gate_ind,int shift)
   assert(G.F.size() < 2);
   if (G.F.size() == 1) C.push_back(var_ind + shift);
   else if (G.F.size() == 0) C.push_back(-(var_ind + shift));
-  if (debug_flag) std::cout << C << " 0\n";
 
   F.push_back(C);
 
@@ -186,34 +180,32 @@ void  CompInfo::add_const_gate_cube(DNF &F,int gate_ind,int shift)
 void CompInfo::add_buffer_gate_cubes(DNF &F,int gate_ind,int shift)
 {
 
-  // form indexes 
-  CUBE var_indexes;
+  // form indices 
+  CUBE var_indices;
   Gate &G = N->Gate_list[gate_ind];
 
 
   for (size_t i=0; i < G.Fanin_list.size();i++) {
     int gate_ind1 =  G.Fanin_list[i];
     int var_ind = Gate_to_var[gate_ind1];
-    var_indexes.push_back(var_ind);
+    var_indices.push_back(var_ind);
   }
 
   // add the output var
-  var_indexes.push_back(Gate_to_var[gate_ind]);
+  var_indices.push_back(Gate_to_var[gate_ind]);
 
   CUBE C;
   // first cube
-  if (G.Polarity[0] == 0)  C.push_back(var_indexes[0]+shift);  
-  else C.push_back(-(var_indexes[0]+shift));
-  C.push_back(-(var_indexes[1]+shift)); 
+  if (G.Polarity[0] == 0)  C.push_back(var_indices[0]+shift);  
+  else C.push_back(-(var_indices[0]+shift));
+  C.push_back(-(var_indices[1]+shift)); 
   F.push_back(C);
-  if (debug_flag) std::cout << C << " 0\n";
 
   // second cube
   C.clear();
-  if (G.Polarity[0] == 0)  C.push_back(-(var_indexes[0]+shift));  
-  else C.push_back(var_indexes[0]+shift);
-  C.push_back(var_indexes[1]+shift);
+  if (G.Polarity[0] == 0)  C.push_back(-(var_indices[0]+shift));  
+  else C.push_back(var_indices[0]+shift);
+  C.push_back(var_indices[1]+shift);
   F.push_back(C);
-  if (debug_flag) std::cout << C << " 0\n";
 
 } /* end of function add_buffer_gate_cubes */

src/ic3/build_prob/g1en_cnf.cc

@@ -43,30 +43,29 @@ void  CompInfo::add_or_gate_cubes(DNF &F,int gate_ind,int shift)
 {
 
 
-  // form indexes 
-  CUBE var_indexes;
+  // form indices 
+  CUBE var_indices;
   Gate &G =  N->Gate_list[gate_ind];
 
 
   for (size_t i=0; i < G.Fanin_list.size();i++) {
     int gate_ind1 = G.Fanin_list[i];
     int var_ind = Gate_to_var[gate_ind1];
-    var_indexes.push_back(var_ind);
+    var_indices.push_back(var_ind);
   }
 
 
   // add the output var
-  var_indexes.push_back(Gate_to_var[gate_ind]);
+  var_indices.push_back(Gate_to_var[gate_ind]);
 
   //
   // generate the long clause
   //
   CUBE C;
   for (size_t i=0; i <  G.Fanin_list.size();i++)
-    if (G.Polarity[i] == 0)   C.push_back(var_indexes[i]+shift); 
-    else C.push_back(-(var_indexes[i]+shift)); 
-  C.push_back(-(var_indexes.back()+shift));
-  if (debug_flag) std::cout << C << " 0\n";
+    if (G.Polarity[i] == 0)   C.push_back(var_indices[i]+shift); 
+    else C.push_back(-(var_indices[i]+shift)); 
+  C.push_back(-(var_indices.back()+shift));
   if (!empty_cube(C))  F.push_back(C);
 
   //
@@ -75,10 +74,9 @@ void  CompInfo::add_or_gate_cubes(DNF &F,int gate_ind,int shift)
   //
   for (size_t i=0; i < G.Fanin_list.size();i++)
     {C.clear();
-      if (G.Polarity[i] == 0)   C.push_back(-(var_indexes[i]+shift)); 
-      else C.push_back(var_indexes[i]+shift); 
-      C.push_back(var_indexes.back()+shift);
-      if (debug_flag) std::cout << C << " 0\n";
+      if (G.Polarity[i] == 0)   C.push_back(-(var_indices[i]+shift)); 
+      else C.push_back(var_indices[i]+shift); 
+      C.push_back(var_indices.back()+shift);
       if (!empty_cube(C)) F.push_back(C);
     }
 
@@ -93,29 +91,28 @@ void  CompInfo::add_or_gate_cubes(DNF &F,int gate_ind,int shift)
 void CompInfo::add_and_gate_cubes(DNF &F,int gate_ind,int shift)
 {
 
-  // form indexes 
-  CUBE var_indexes;
+  // form indices 
+  CUBE var_indices;
   Gate &G =  N->Gate_list[gate_ind];
 
   for (size_t i=0; i < G.Fanin_list.size();i++) {
     int gate_ind1 = G.Fanin_list[i];
     int var_ind = Gate_to_var[gate_ind1];
-    var_indexes.push_back(var_ind);
+    var_indices.push_back(var_ind);
   }
 
   // add the output var
-  var_indexes.push_back(Gate_to_var[gate_ind]);
+  var_indices.push_back(Gate_to_var[gate_ind]);
 
 
   //
   // generate the long clause
   //
   CUBE C;
   for (size_t i=0; i < G.Fanin_list.size();i++)
-    if (G.Polarity[i] == 0)   C.push_back(-(var_indexes[i]+shift)); 
-    else C.push_back(var_indexes[i]+shift); 
-  C.push_back(var_indexes.back()+shift);
-  if (debug_flag) std::cout << C << " 0\n";
+    if (G.Polarity[i] == 0)   C.push_back(-(var_indices[i]+shift)); 
+    else C.push_back(var_indices[i]+shift); 
+  C.push_back(var_indices.back()+shift);
   if (!empty_cube(C))  F.push_back(C);
 
   //
@@ -124,10 +121,9 @@ void CompInfo::add_and_gate_cubes(DNF &F,int gate_ind,int shift)
   //
   for (size_t i=0; i < G.Fanin_list.size();i++) {
     C.clear();
-    if (G.Polarity[i] == 0)   C.push_back(var_indexes[i]+shift); 
-    else C.push_back(-(var_indexes[i]+shift)); 
-    C.push_back(-(var_indexes.back()+shift));
-    if (debug_flag) std::cout << C << " 0\n";
+    if (G.Polarity[i] == 0)   C.push_back(var_indices[i]+shift); 
+    else C.push_back(-(var_indices[i]+shift)); 
+    C.push_back(-(var_indices.back()+shift));
     if (!empty_cube(C)) F.push_back(C);
   }
 
@@ -141,19 +137,19 @@ void CompInfo::add_and_gate_cubes(DNF &F,int gate_ind,int shift)
 void  CompInfo::add_truth_table_gate_cubes(DNF &F,int gate_ind,int shift)
 {
 
-  // form indexes 
-  CUBE var_indexes;
+  // form indices 
+  CUBE var_indices;
   Gate &G =  N->Gate_list[gate_ind];
 
 
   for (size_t i=0; i < G.Fanin_list.size();i++) {
     int gate_ind1 = G.Fanin_list[i];
     int var_ind = Gate_to_var[gate_ind1];
-    var_indexes.push_back(var_ind);
+    var_indices.push_back(var_ind);
   }
 
   // add the output var
-  var_indexes.push_back(Gate_to_var[gate_ind]);
+  var_indices.push_back(Gate_to_var[gate_ind]);
 
   CUBE TT(1 << G.ninputs);
   for (size_t i=0; i < TT.size(); i++)
@@ -170,10 +166,10 @@ void  CompInfo::add_truth_table_gate_cubes(DNF &F,int gate_ind,int shift)
     CUBE &C = D[i];
     CUBE C1;
     for (size_t j=0; j < C.size(); j++) {
-      C1.push_back(var_indexes[abs(C[j])-1]+shift);
+      C1.push_back(var_indices[abs(C[j])-1]+shift);
       if (C[j] > 0) C1[j] = -C1[j];
     }
-    C1.push_back(var_indexes.back()+shift);
+    C1.push_back(var_indices.back()+shift);
     if (!empty_cube(C1)) F.push_back(C1);
   }
 
@@ -184,10 +180,10 @@ void  CompInfo::add_truth_table_gate_cubes(DNF &F,int gate_ind,int shift)
       if (TT[i] == 1) continue;
       make_cube(i,G.ninputs,C);
       for (size_t j=0; j < C.size(); j++)
-	{C1.push_back(var_indexes[abs(C[j])-1]+shift);
+	{C1.push_back(var_indices[abs(C[j])-1]+shift);
 	  if (C[j] >  0) C1[j] = -C1[j];
 	}
-      C1.push_back(var_indexes.back()+shift);
+      C1.push_back(var_indices.back()+shift);
       C1.back() = -C1.back();
       if (!empty_cube(C1)) F.push_back(C1);
     }