fixed one of the problems with conversion of verilog to internal repr…

…es. of ic3

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

src/ic3/ebmc_ic3_interface.hh

@@ -43,7 +43,7 @@ public:
   void print_lit1(unsigned var,bool sign);
   void print_lit2(unsigned var,bool sign);
   void print_nodes();
-  void print_var_map();
+  void print_var_map(std::ostream &out);
   void form_orig_names();
   void form_neg_orig_name(CCUBE &Name,literalt &next_lit);
   bool form_orig_name(CCUBE &Name,literalt &lit,bool subtract = false);
@@ -58,6 +58,10 @@ public:
   void store_constraints(const std::string &fname);
   void read_constraints(const std::string &fname);
   void add_pseudo_inps(Circuit *N);
+  void print_lit(std::ostream& out,literalt a);
+  std::string print_string(const irep_idt &id);
+  void add_verilog_conv_constrs();
+
 protected:
   netlistt netlist;
 

src/ic3/m1ain.cc

@@ -80,9 +80,9 @@ int ic3_enginet::operator()()
   orig_names = false;
 
   // print_nodes();
-  // print_var_map();
+  // print_var_map(std::cout);
   read_ebmc_input();
-  //print_blif3("tst.blif",Ci.N);
+  // print_blif3("tst.blif",Ci.N);
   if (cmdline.isset("aiger")) {
     printf("converting to aiger format\n");
     Ci.print_aiger_format();

src/ic3/m2ethods.hh

@@ -187,6 +187,7 @@ void print_files(char *root);
 int init_ind_cls();
 void form_nxt_cube(CUBE &Nxt_cube,CLAUSE &C);
 int push_on_the_fly(int last_ind,CLAUSE &C,char st_desc);
+void accept_constrs(SatSolver &Slvr);
 //
 //  form CNF formulas
 void add_or_gate_cubes(DNF &F,int gate_ind,int shift);

src/ic3/r0ead_input.cc

@@ -137,10 +137,6 @@ void ic3_enginet::form_inputs()
 } /* end of function form_inputs */
 
 
-
-
-
-
 /*=================================
 
        F O R M _ T A B L E
@@ -189,10 +185,6 @@ void CompInfo::form_max_pres_svar() {
   max_pres_svar = max;
 } /* end of function form_max_pres_svar */
 
-
-
-
-
 /*===================================
 
       F O R M _ V A R _ N U M S
@@ -209,3 +201,20 @@ void CompInfo::form_var_nums()
   max_num_vars = max_num_vars0 + num_prop_vars; // we need to take into account
   // that property needs to be specified in two time frames
 } /* end of function form_var_nums */
+
+/*================================================
+
+   A D D _ V E R I L O G _ C O N V _ C O N S T R S
+
+  ================================================*/
+void ic3_enginet::add_verilog_conv_constrs()
+{
+
+  for(literalt lit : netlist.constraints) {
+    if (lit.is_constant()) continue;
+    std::cout << "constraint literal " << lit.get() << "\n";
+     Ci.Init_clits.insert(lit.get());
+  }
+
+
+} /* end of function add_verlig_conv_constrs */

src/ic3/r1ead_input.cc

@@ -63,6 +63,9 @@ void ic3_enginet::find_prop_lit()
 
   if (prop_l.is_false()) Ci.const_flags = Ci.const_flags | 1;
   else if (prop_l.is_true()) Ci.const_flags = Ci.const_flags | 2;
+
+  // print_lit(std::cout,prop_l);
+  // printf("\n");
 
 } /* end of function find_prop_lit */
 

src/ic3/r4ead_input.cc

@@ -21,6 +21,8 @@ Author: Eugene Goldberg, [email protected]
 #include "m0ic3.hh"
 
 #include "ebmc_ic3_interface.hh"
+
+
 /*=========================================
 
       U P D _ G A T E _ C O N S T R S
@@ -84,6 +86,7 @@ int CompInfo::upd_gate_constr_tbl(int lit,int gate_ind)
 void ic3_enginet::store_constraints(const std::string &fname)
 {
 
+  add_verilog_conv_constrs();
   if (Ci.constr_flag == false) return;
 
   read_constraints(fname);
@@ -241,7 +244,7 @@ void ic3_enginet::gen_ist_lits(bvt &Ist_lits)
       continue;
     if (var_num >= Nodes.size()) {
       p();
-      printf("var_num = %d\n",var_num);
+      printf("var_num = %zd\n",var_num);
       printf("Nodes.size() = %zu\n",Nodes.size());
       exit(100);
     }

src/ic3/r6ead_input.cc

@@ -152,6 +152,7 @@ void ic3_enginet::form_orig_names()
 void ic3_enginet::print_nodes()
 {
 
+  printf("\n-----  Nodes ------\n");
   aigt::nodest &Nodes = netlist.nodes;
   for (size_t i=0; i <= Nodes.size(); i++) {  
     aigt::nodet &Nd = Nodes[i];

src/ic3/r7ead_input.cc

@@ -23,37 +23,85 @@ Author: Eugene Goldberg, [email protected]
 #include <ebmc/ebmc_base.h>
 #include "ebmc_ic3_interface.hh"
 
+
 /*=====================================
 
        P R I N T _ V A R _ M A P
 
-  =====================================*/
-void ic3_enginet::print_var_map()
+ =====================================*/
+void ic3_enginet::print_var_map(std::ostream &out)
 {
 
 
-  var_mapt &vm = netlist.var_map;
+  printf("\n-----  Var Map ------\n");
 
+  var_mapt &vm = netlist.var_map;
   for(var_mapt::mapt::const_iterator it=vm.map.begin();
-      it!=vm.map.end(); it++)    {
-    const var_mapt::vart &var=it->second;
-    if (var.is_input()) printf("input: ");
-    else if (var.is_latch()) printf("latch: ");
-    else if (var.is_nondet()) printf("nondet: ");
-    else if (var.is_wire()) printf("wire:" );
-    else assert(false);
-
-    for (size_t j=0; j < var.bits.size(); j++) {
-      if (j > 0) printf(", ");
-      literalt lit =var.bits[j].current;
-      unsigned lit_val = lit.get();
-      printf("[%zu] = %u",j,lit_val);
+      it!=vm.map.end(); it++)
+    {
+      const var_mapt::vart &var=it->second;
+
+      for(std::size_t i=0; i<var.bits.size(); i++)
+	{
+	  out << "  " << it->first;
+	  if(var.bits.size()!=1) out << "[" << i << "]";
+	  out << "=";
+
+	  literalt l_c=var.bits[i].current;
+
+	  if(l_c.is_true())
+	    out << "true";
+	  else if(l_c.is_false())
+	    out << "false";
+	  else
+	    {
+	      if(l_c.sign()) out << "!";
+	      out << l_c.var_no();
+	    }
+
+	  if(var.vartype==var_mapt::vart::vartypet::LATCH)
+	    {
+	      out << "->";
+
+	      literalt l_n=var.bits[i].next;
+
+	      if(l_n.is_true())
+		out << "true";
+	      else if(l_n.is_false())
+		out << "false";
+	      else
+		{
+		  if(l_n.sign()) out << "!";
+		  out << l_n.var_no();
+		}
+	    }
+
+	  out << " ";
+
+	  switch(var.vartype)
+	    {
+	    case var_mapt::vart::vartypet::INPUT: out << "(input)"; break;
+	    case var_mapt::vart::vartypet::LATCH: out << "(latch)"; break;
+	    case var_mapt::vart::vartypet::NONDET: out << "(nondet)"; break;
+	    case var_mapt::vart::vartypet::WIRE:  out << "(wire)"; break;
+	    case var_mapt::vart::vartypet::OUTPUT:out << "(output)"; break;
+	    case var_mapt::vart::vartypet::UNDEF: out << "(?)"; break;
+	    }
+
+	  out << '\n';
+	}
     }
-    printf("\n");
-  }
+
+  out << '\n'
+      << "Total no. of variable bits: " << vm.reverse_map.size() << '\n'
+      << "Total no. of latch bits: " << vm.latches.size() << '\n'
+      << "Total no. of nondet bits: " << vm.nondets.size() << '\n'
+      << "Total no. of input bits: " << vm.inputs.size() << '\n'
+      << "Total no. of output bits: " << vm.outputs.size() << '\n';
+
 
 
-} /* end of function print_var_map */
+    } /* end of function print_var_map */
 /*=========================================
 
         A D D _ P S E U D O _ I N P S

src/ic3/v0erify.cc

@@ -161,6 +161,7 @@ bool CompInfo::ver_ini_states(CNF &H)
 
   accept_new_clauses(Gen_sat,Ist);  
 
+  accept_constrs(Gen_sat);
   bool ok = ver_prop();
   if (!ok) return(false);