Merge pull request #1036 from mgudemann/fix/unused-vars-in-assert

Fix unused variables that only appear in `assert`

Author: tautschnig

src/ic3/aux_types.hh

@@ -6,8 +6,12 @@ Author: Eugene Goldberg, [email protected]
 
 ******************************************************/
 
+#include <queue>
 #include <string>
 
+#include "minisat/core/Solver.h"
+#include "minisat/simp/SimpSolver.h"
+
 #ifndef UNUSED
 #ifdef _MSC_VER
 #define UNUSED

src/ic3/build_prob/g3en_cnf.cc

@@ -5,18 +5,20 @@ Module: CNF Generation (Part 4)
 Author: Eugene Goldberg, [email protected]
 
 ******************************************************/
+#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;
 

src/ic3/dnf_io.hh

@@ -7,7 +7,14 @@ Author: Eugene Goldberg, [email protected]
 
 ******************************************************/
 
+#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

src/ic3/e4xclude_state.cc

@@ -6,16 +6,20 @@ Module:  Excludes a state from which a bad state is
 Author: Eugene Goldberg, [email protected]
 
 ******************************************************/
-#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);

src/ic3/i1nit.cc

@@ -5,16 +5,20 @@ Module: Initialization of IC3
 Author: Eugene Goldberg, [email protected]
 
 ******************************************************/
+#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);

src/ic3/i2nit_sat_solvers.cc

@@ -5,15 +5,19 @@ Module: Initialization of Sat-solvers (Part 1)
 Author: Eugene Goldberg, [email protected]
 
 ******************************************************/
+#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);
   }
 

src/ic3/m0ic3.hh

@@ -5,6 +5,7 @@ Module: IC3 types
 Author: Eugene Goldberg, [email protected]
 
 ******************************************************/
+
 #include "aux_types.hh"
 
 extern int debug_flag;

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

src/ic3/my_printf.cc

@@ -6,15 +6,18 @@ Module: Structuring the output of large numbers by
 Author: Eugene Goldberg, [email protected]
 
 ******************************************************/
+#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);    

src/ic3/p5ick_lit.cc

@@ -6,17 +6,20 @@ Module:  Picking a literal to remove when generalizing
 Author: Eugene Goldberg, [email protected]
 
 ******************************************************/
-#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 */