Replace assert with INVARIANT for variables used only there

This replaces instances of the form

```
x = f(..);
assert(x);
```

with

```
x = f(..);
INVARIANT(x, "...");
```

Author: mgudemann

src/ic3/build_prob/g3en_cnf.cc

@@ -10,6 +10,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <map>
 #include <algorithm>
 #include <queue>
+#include <util/invariant.h>
 
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
@@ -48,7 +49,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;
 

src/ic3/e4xclude_state.cc

@@ -11,6 +11,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <map>
 #include <algorithm>
 #include <iostream>
+#include <util/invariant.h>
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
 #include "dnf_io.hh"
@@ -91,7 +92,8 @@ 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);

src/ic3/i1nit.cc

@@ -10,6 +10,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <set>
 #include <map>
 #include <algorithm>
+#include <util/invariant.h>
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
 #include "dnf_io.hh"
@@ -214,7 +215,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);

src/ic3/i2nit_sat_solvers.cc

@@ -9,6 +9,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <set>
 #include <map>
 #include <algorithm>
+#include <util/invariant.h>
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
 #include "dnf_io.hh"
@@ -141,7 +142,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);
   }
 

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

src/ic3/my_printf.cc

@@ -14,6 +14,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <queue>
 #include <map>
 #include <iostream>
+#include <util/invariant.h>
 #include "dnf_io.hh"
 const int factor = 1000;
 
@@ -65,7 +66,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);    

src/ic3/p5ick_lit.cc

@@ -11,6 +11,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <map>
 #include <algorithm>
 #include <iostream>
+#include <util/invariant.h>
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
 #include "dnf_io.hh"

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

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

src/ic3/s2horten_clause.cc

@@ -10,6 +10,7 @@ Author: Eugene Goldberg, eu.goldberg@gmail.com
 #include <map>
 #include <algorithm>
 #include <iostream>
+#include <util/invariant.h>
 #include "minisat/core/Solver.h"
 #include "minisat/simp/SimpSolver.h"
 #include "dnf_io.hh"
@@ -87,7 +88,7 @@ void CompInfo::find_fixed_pnt(CLAUSE &C,CLAUSE &C0,SatSolver &Slvr,
 
     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;