diffblue · tautschnig · Mar 28, 2025 · Mar 26, 2025 · Mar 26, 2025 · Mar 26, 2025
diff --git a/src/ic3/aux_types.hh b/src/ic3/aux_types.hh
@@ -6,8 +6,12 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 
 ******************************************************/
 
+#include <queue>
 #include <string>
 
+#include "minisat/core/Solver.h"
+#include "minisat/simp/SimpSolver.h"
+
 #ifndef UNUSED
 #ifdef _MSC_VER
 #define UNUSED

diff --git a/src/ic3/build_prob/g3en_cnf.cc b/src/ic3/build_prob/g3en_cnf.cc
@@ -5,18 +5,20 @@ Module: CNF Generation (Part 4)
 Author: Eugene Goldberg, eu.goldberg@gmail.com
 
 ******************************************************/
+#include <util/invariant.h>
+
+#include "ccircuit.hh"
+#include "dnf_io.hh"
+#include "m0ic3.hh"
+
+#include <algorithm>
 #include <iostream>
-#include <set>
 #include <map>
-#include <algorithm>
 #include <queue>
+#include <set>
 
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
-#include "dnf_io.hh"
-#include "ccircuit.hh"
-#include "m0ic3.hh"
-
 
 /*=======================================
 
@@ -48,7 +50,7 @@ void CompInfo::gen_constr_coi(CUBE &Gates,bool &tran_flag,bool &fun_flag,
 
   assert(Stack.size() == 1);
   Gate &G = N->get_gate(Stack.back());
-  assert(G.flags.label == 0);
+  INVARIANT(G.flags.label == 0, "Gate label should be zero.");
 
   CUBE Labelled;
 

diff --git a/src/ic3/dnf_io.hh b/src/ic3/dnf_io.hh
@@ -7,7 +7,14 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 
 ******************************************************/
 
+#ifndef DNF_IO_HH
+#define DNF_IO_HH
+
+#include <deque>
 #include <iosfwd>
+#include <map>
+#include <set>
+#include <vector>
 
 typedef std::vector<int> CUBE;
 typedef std::vector<CUBE> DNF;
@@ -20,11 +27,6 @@ typedef std::set<int> SCUBE;
 typedef DNF CNF;
 typedef std::vector <float> FltCube;
 
-
-#define BUF_SIZE 1000
-#define MAX_NUM 20
-
-
 /*========================
 
  C L A S S    comp_lits
@@ -72,4 +74,4 @@ void print_srt_dnf(DNF &D);
 void fprint_srt_dnf(DNF &D,char *fname);
 void fprint_srt_dnf(DNF &D,const char *fname);
 
-
+#endif
diff --git a/src/ic3/e4xclude_state.cc b/src/ic3/e4xclude_state.cc
@@ -6,16 +6,20 @@ Module:  Excludes a state from which a bad state is
 Author: Eugene Goldberg, eu.goldberg@gmail.com
 
 ******************************************************/
-#include <queue>
-#include <set>
-#include <map>
+#include <util/invariant.h>
+
+#include "ccircuit.hh"
+#include "dnf_io.hh"
+#include "m0ic3.hh"
+
 #include <algorithm>
 #include <iostream>
+#include <map>
+#include <queue>
+#include <set>
+
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
-#include "dnf_io.hh"
-#include "ccircuit.hh"
-#include "m0ic3.hh"
 
 /*=========================================
 
@@ -91,7 +95,7 @@ void CompInfo::form_res_cnf(CNF &G,int tf_ind,CUBE &St_cube)
   add_assumps1(Assmps,St_cube);
 
   bool sat_form = Slvr.Mst->solve(Assmps);
-  assert(sat_form == false);
+  INVARIANT(sat_form == false, "SAT check should fail here.");
   CLAUSE C;
   gen_assump_clause(C,Slvr,Assmps);
   G.push_back(C);

diff --git a/src/ic3/i1nit.cc b/src/ic3/i1nit.cc
@@ -5,16 +5,20 @@ Module: Initialization of IC3
 Author: Eugene Goldberg, eu.goldberg@gmail.com
 
 ******************************************************/
+#include <util/invariant.h>
+
+#include "ccircuit.hh"
+#include "dnf_io.hh"
+#include "m0ic3.hh"
+
+#include <algorithm>
 #include <iostream>
+#include <map>
 #include <queue>
 #include <set>
-#include <map>
-#include <algorithm>
+
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
-#include "dnf_io.hh"
-#include "ccircuit.hh"
-#include "m0ic3.hh"
 /*==============================
 
     C I _ I N I T
@@ -214,7 +218,7 @@ void CompInfo::form_cex()
     add_assumps1(Assmps,Cex[i]);     
     add_assumps1(Assmps,Inp_trace[i]);
     bool sat_form = check_sat2(Gen_sat,Assmps);
-    assert(sat_form);
+    INVARIANT(sat_form, "SAT check should fail here.");
     CUBE Nst,St;
     extr_cut_assgns1(Nst,Next_svars,Gen_sat);
     conv_to_pres_state(St,Nst);

diff --git a/src/ic3/i2nit_sat_solvers.cc b/src/ic3/i2nit_sat_solvers.cc
@@ -5,15 +5,19 @@ Module: Initialization of Sat-solvers (Part 1)
 Author: Eugene Goldberg, eu.goldberg@gmail.com
 
 ******************************************************/
+#include <util/invariant.h>
+
+#include "ccircuit.hh"
+#include "dnf_io.hh"
+#include "m0ic3.hh"
+
+#include <algorithm>
+#include <map>
 #include <queue>
 #include <set>
-#include <map>
-#include <algorithm>
+
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
-#include "dnf_io.hh"
-#include "ccircuit.hh"
-#include "m0ic3.hh"
 
 /*======================================
 
@@ -141,7 +145,8 @@ void CompInfo::init_lbs_sat_solver()
   for (size_t i=0; i < Fun_coi_lits.size(); i++) {
     int lit = Fun_coi_lits[i];
     int var_ind = abs(lit)-1;
-    assert (Var_info[var_ind].type == INTERN);
+    INVARIANT(
+      Var_info[var_ind].type == INTERN, "Type of literal should be INTERN");
     U.push_back(-lit);
   }
 

diff --git a/src/ic3/m0ic3.hh b/src/ic3/m0ic3.hh
@@ -5,6 +5,7 @@ Module: IC3 types
 Author: Eugene Goldberg, eu.goldberg@gmail.com
 
 ******************************************************/
+
 #include "aux_types.hh"
 
 extern int debug_flag;

diff --git a/src/ic3/m1ain.cc b/src/ic3/m1ain.cc
@@ -195,7 +195,7 @@ int CompInfo::run_ic3()
 
 
   bool ok = check_init_states();
-  assert(ok);
+  INVARIANT(ok, "Initial states should be defined via single literal.");
   assign_var_type();
   assign_value();
   get_runtime (usrtime0, systime0);
@@ -242,7 +242,7 @@ int CompInfo::run_ic3()
       print_fclauses();
     break;
   default:
-    assert(false);
+    UNREACHABLE;
   }
   if (statistics) {
     printf("*********\n");

diff --git a/src/ic3/my_printf.cc b/src/ic3/my_printf.cc
@@ -6,15 +6,18 @@ Module: Structuring the output of large numbers by
 Author: Eugene Goldberg, eu.goldberg@gmail.com
 
 ******************************************************/
+#include <util/invariant.h>
+
+#include "dnf_io.hh"
+
+#include <algorithm>
 #include <assert.h>
+#include <iostream>
+#include <map>
+#include <queue>
+#include <set>
 #include <stdarg.h>
 #include <stdio.h>
-#include <set>
-#include <algorithm>
-#include <queue>
-#include <map>
-#include <iostream>
-#include "dnf_io.hh"
 const int factor = 1000;
 
 /*================================================
@@ -65,7 +68,7 @@ void my_printf(const char *format,...)
     int c = *format++;
     if (c != '%') {printf("%c",c); continue;}
     int spec = *format++;
-    assert(spec == 'm');
+    INVARIANT(spec == 'm', "Character should be 'm' in format string.");
     int num = va_arg(ap,int);
     print_num_with_commas(num);      
     //    printf("%d",num);    

diff --git a/src/ic3/p5ick_lit.cc b/src/ic3/p5ick_lit.cc
@@ -6,17 +6,20 @@ Module:  Picking a literal to remove when generalizing
 Author: Eugene Goldberg, eu.goldberg@gmail.com
 
 ******************************************************/
-#include <queue>
-#include <set>
-#include <map>
+#include <util/invariant.h>
+
+#include "ccircuit.hh"
+#include "dnf_io.hh"
+#include "m0ic3.hh"
+
 #include <algorithm>
 #include <iostream>
+#include <map>
+#include <queue>
+#include <set>
+
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
-#include "dnf_io.hh"
-#include "ccircuit.hh"
-#include "m0ic3.hh"
-
 
 /*=============================
 
@@ -52,6 +55,5 @@ int CompInfo::fxd_ord_lit(CUBE &Curr,SCUBE &Tried)
       return(lit);
   }
 
-  assert(false); // shouldn't reach this line
-
+  UNREACHABLE;
 } /* end of function fxd_ord_lit */
diff --git a/src/ic3/r0ead_input.cc b/src/ic3/r0ead_input.cc
@@ -128,7 +128,8 @@ void ic3_enginet::form_inputs()
       CCUBE Name;
       if (orig_names) {
 	bool ok = form_orig_name(Name,lit);
-	assert(ok);}      
+  INVARIANT(ok, "Literal should have an original name.");
+      }
       else {
 	char Inp_name[MAX_NAME];
 	sprintf(Inp_name,"i%d",lit_val);   

diff --git a/src/ic3/r4ead_input.cc b/src/ic3/r4ead_input.cc
@@ -107,7 +107,7 @@ void ic3_enginet::form_latch_name(CCUBE &Latch_name,literalt &lit)
 {
   if (orig_names) {
     bool ok = form_orig_name(Latch_name,lit);
-    assert(ok);        
+    INVARIANT(ok, "Literal should have original name.");
     return; }
 
   char Buff[MAX_NAME];

diff --git a/src/ic3/s2horten_clause.cc b/src/ic3/s2horten_clause.cc
@@ -5,16 +5,20 @@ Module: Generalization of an inductive clause
 Author: Eugene Goldberg, eu.goldberg@gmail.com
 
 ******************************************************/
-#include <queue>
-#include <set>
-#include <map>
+#include <util/invariant.h>
+
+#include "ccircuit.hh"
+#include "dnf_io.hh"
+#include "m0ic3.hh"
+
 #include <algorithm>
 #include <iostream>
+#include <map>
+#include <queue>
+#include <set>
+
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
-#include "dnf_io.hh"
-#include "ccircuit.hh"
-#include "m0ic3.hh"
 
 /*==================================
 
@@ -86,8 +90,8 @@ void CompInfo::find_fixed_pnt(CLAUSE &C,CLAUSE &C0,SatSolver &Slvr,
     // run a SAT-check
 
     bool sat_form = check_sat2(Slvr,Assmps);
-  
-    assert(sat_form == false);
+
+    INVARIANT(sat_form == false, "SAT check should fail here.");
     CLAUSE B;
     gen_assump_clause(B,Slvr,Assmps);
     CLAUSE B1;

diff --git a/src/ic3/seq_circ/a4dd_spec_buffs.cc b/src/ic3/seq_circ/a4dd_spec_buffs.cc
@@ -6,18 +6,20 @@ Module: Treating the case when a gate feeds more
 Author: Eugene Goldberg, eu.goldberg@gmail.com
 
 ******************************************************/
+#include <util/invariant.h>
+
+#include "ccircuit.hh"
+#include "dnf_io.hh"
+
+#include <algorithm>
+#include <assert.h>
 #include <iostream>
-#include <vector>
-#include <set>
 #include <map>
-#include <algorithm>
 #include <queue>
-#include <assert.h>
-#include <string.h>
+#include <set>
 #include <stdio.h>
-#include "dnf_io.hh"
-#include "ccircuit.hh"
-
+#include <string.h>
+#include <vector>
 
 /*=========================================
 
@@ -121,7 +123,9 @@ int spec_buff_gate_ind(Circuit *N,int ind)
   int gate_ind = N->Pin_list[fake_name];
 
   Gate &G = N->get_gate(gate_ind);
-  assert(G.spec_buff_ind == ind);
+  INVARIANT(
+    G.spec_buff_ind == ind,
+    "Special buffer index of gate should be equal to value of `ind`");
 
   return(gate_ind);
 

diff --git a/src/ic3/seq_circ/ccircuit.hh b/src/ic3/seq_circ/ccircuit.hh
@@ -6,6 +6,9 @@ Module: Basic types (gate, circuit and so on)
 Author: Eugene Goldberg, eu.goldberg@gmail.com
 
 ******************************************************/
+
+#include "dnf_io.hh"
+
 struct ConstrGateInfo {
   unsigned neg_lit:1;
   unsigned fun_coi:1;