Cleanup error handling in solvers/qbf

Author: Petr Bauch

src/solvers/qbf/qbf_bdd_core.cpp

@@ -8,10 +8,10 @@ Author: CM Wintersteiger
 
 #include <solvers/prop/literal.h>
 
-#include <cassert>
 #include <fstream>
 
 #include <util/arith_tools.h>
+#include <util/invariant.h>
 #include <util/std_expr.h>
 
 #include <cuddObj.hh> // CUDD Library
@@ -80,7 +80,7 @@ qbf_bdd_coret::~qbf_bdd_coret()
 
 tvt qbf_bdd_coret::l_get(literalt a) const
 {
-  assert(false);
+  UNREACHABLE;
   return tvt(false);
 }
 
@@ -122,17 +122,18 @@ propt::resultt qbf_bdd_coret::prop_solve()
 
       *matrix=matrix->ExistAbstract(*bdd_variable_map[var]);
     }
-    else if(it->type==quantifiert::UNIVERSAL)
+    else
     {
+      INVARIANT(
+        it->type == quantifiert::UNIVERSAL,
+        "Only handles quantified variables.");
       #if 0
       std::cout << "BDD A: " << var << ", " <<
         matrix->nodeCount() << " nodes\n";
       #endif
 
       *matrix=matrix->UnivAbstract(*bdd_variable_map[var]);
     }
-    else
-      throw "unquantified variable";
   }
 
   if(*matrix==bdd_manager->bddOne())
@@ -151,12 +152,12 @@ propt::resultt qbf_bdd_coret::prop_solve()
 
 bool qbf_bdd_coret::is_in_core(literalt l) const
 {
-  throw "nyi";
+  UNIMPLEMENTED;
 }
 
 qdimacs_coret::modeltypet qbf_bdd_coret::m_get(literalt a) const
 {
-  throw "nyi";
+  UNIMPLEMENTED;
 }
 
 literalt qbf_bdd_coret::new_variable()
@@ -268,17 +269,17 @@ void qbf_bdd_coret::compress_certificate(void)
 const exprt qbf_bdd_certificatet::f_get(literalt l)
 {
   quantifiert q;
-  if(!find_quantifier(l, q))
-    throw "no model for unquantified variable";
+  PRECONDITION_WITH_DIAGNOSTICS(
+    !find_quantifier(l, q), "No model for unquantified variables.");
 
   // universal?
   if(q.type==quantifiert::UNIVERSAL)
   {
-    assert(l.var_no()!=0);
+    INVARIANT(l.var_no() != 0, "Input literal wasn't properly initialized.");
     variable_mapt::const_iterator it=variable_map.find(l.var_no());
 
-    if(it==variable_map.end())
-      throw "variable map error";
+    INVARIANT(
+      it != variable_map.end(), "Variable not found in the variable map.");
 
     const exprt &sym=it->second.first;
     unsigned index=it->second.second;
@@ -293,7 +294,9 @@ const exprt qbf_bdd_certificatet::f_get(literalt l)
   else
   {
     // skolem functions for existentials
-    assert(q.type==quantifiert::EXISTENTIAL);
+    INVARIANT(
+      q.type == quantifiert::EXISTENTIAL,
+      "Only quantified literals are supported.");
 
     function_cachet::const_iterator it=function_cache.find(l.var_no());
     if(it!=function_cache.end())
@@ -310,7 +313,9 @@ const exprt qbf_bdd_certificatet::f_get(literalt l)
 
     // no cached function, so construct one
 
-    assert(model_bdds[l.var_no()]!=NULL);
+    INVARIANT(
+      model_bdds[l.var_no()] != NULL,
+      "There must be a model BDD for the literal.");
     BDD &model=*model_bdds[l.var_no()];
 
     #if 0

src/solvers/qbf/qbf_quantor.cpp

@@ -8,9 +8,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "qbf_quantor.h"
 
-#include <cassert>
 #include <cstdlib>
 #include <fstream>
+#include <util/invariant.h>
 
 qbf_quantort::qbf_quantort()
 {
@@ -22,7 +22,7 @@ qbf_quantort::~qbf_quantort()
 
 tvt qbf_quantort::l_get(literalt) const
 {
-  assert(false);
+  UNREACHABLE;
   return tvt::unknown();
 }
 

src/solvers/qbf/qbf_qube.cpp

@@ -8,9 +8,9 @@ Author: CM Wintersteiger
 
 #include "qbf_qube.h"
 
-#include <cassert>
 #include <cstdlib>
 #include <fstream>
+#include <util/invariant.h>
 
 qbf_qubet::qbf_qubet()
 {
@@ -24,7 +24,7 @@ qbf_qubet::~qbf_qubet()
 
 tvt qbf_qubet::l_get(literalt) const
 {
-  assert(false);
+  UNREACHABLE;
   return tvt(false);
 }
 

src/solvers/qbf/qbf_qube_core.cpp

@@ -8,10 +8,10 @@ Author: CM Wintersteiger
 
 #include "qbf_qube_core.h"
 
-#include <cassert>
 #include <cstdlib>
-#include <fstream>
 #include <cstring>
+#include <fstream>
+#include <util/invariant.h>
 
 #include <util/mp_arith.h>
 
@@ -131,10 +131,10 @@ propt::resultt qbf_qube_coret::prop_solve()
 
 bool qbf_qube_coret::is_in_core(literalt) const
 {
-  throw "not supported";
+  UNIMPLEMENTED;
 }
 
 qdimacs_coret::modeltypet qbf_qube_coret::m_get(literalt) const
 {
-  throw "not supported";
+  UNIMPLEMENTED;
 }

src/solvers/qbf/qbf_qube_core.h

@@ -11,6 +11,7 @@ Author: CM Wintersteiger
 #define CPROVER_SOLVERS_QBF_QBF_QUBE_CORE_H
 
 #include "qdimacs_core.h"
+#include <util/invariant.h>
 
 class qbf_qube_coret:public qdimacs_coret
 {
@@ -51,7 +52,7 @@ class qbf_qube_coret:public qdimacs_coret
 
   virtual const exprt f_get(literalt)
   {
-    throw "qube does not support full certificates.";
+    INVARIANT(false, "qube does not support full certificates.");
   }
 };
 

src/solvers/qbf/qbf_skizzo.cpp

@@ -8,9 +8,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "qbf_skizzo.h"
 
-#include <cassert>
 #include <cstdlib>
 #include <fstream>
+#include <util/invariant.h>
 
 qbf_skizzot::qbf_skizzot()
 {
@@ -24,7 +24,7 @@ qbf_skizzot::~qbf_skizzot()
 
 tvt qbf_skizzot::l_get(literalt) const
 {
-  assert(false);
+  UNREACHABLE;
   return tvt(false);
 }
 

src/solvers/qbf/qbf_skizzo_core.cpp

@@ -6,9 +6,8 @@ Author: CM Wintersteiger
 
 \*******************************************************************/
 
-
-#include <cassert>
 #include <fstream>
+#include <util/invariant.h>
 
 #include <util/string2int.h>
 
@@ -132,12 +131,12 @@ propt::resultt qbf_skizzo_coret::prop_solve()
 
 bool qbf_skizzo_coret::is_in_core(literalt l) const
 {
-  throw "nyi";
+  UNIMPLEMENTED;
 }
 
 qdimacs_coret::modeltypet qbf_skizzo_coret::m_get(literalt a) const
 {
-  throw "nyi";
+  UNIMPLEMENTED;
 }
 
 bool qbf_skizzo_coret::get_certificate(void)
@@ -196,7 +195,10 @@ bool qbf_skizzo_coret::get_certificate(void)
     std::string line;
     std::getline(in, line);
 
-    assert(line=="# QBM file, 1.3");
+    INVARIANT_WITH_DIAGNOSTICS(
+      line == "# QBM file, 1.3",
+      "A QBM file has to start with this exact string: ",
+      "# QBM file, 1.3");
 
     while(in)
     {
@@ -215,7 +217,7 @@ bool qbf_skizzo_coret::get_certificate(void)
     size_t ob=line.find('[');
     std::string n_es=line.substr(ob+1, line.find(']')-ob-1);
     n_e=unsafe_string2int(n_es);
-    assert(n_e!=0);
+    INVARIANT(n_e != 0, "There has to be at least one existential variable.");
 
     e_list.resize(n_e);
     std::string e_lists=line.substr(line.find(':')+2);
@@ -225,7 +227,7 @@ bool qbf_skizzo_coret::get_certificate(void)
       size_t space=e_lists.find(' ');
 
       int cur=unsafe_string2int(e_lists.substr(0, space));
-      assert(cur!=0);
+      INVARIANT(cur != 0, "Variable numbering starts with 1.");
 
       e_list[i]=cur;
       if(cur>e_max)
@@ -234,8 +236,7 @@ bool qbf_skizzo_coret::get_certificate(void)
       e_lists=e_lists.substr(space+1);
     }
 
-    if(!result)
-      throw "existential mapping from sKizzo missing";
+    INVARIANT(!result, "Existential mapping from sKizzo missing.");
 
     in.close();
 
@@ -270,7 +271,10 @@ bool qbf_skizzo_coret::get_certificate(void)
         NULL,
         &bdds);
 
-    assert(nroots=2*n_e); // ozziKs documentation guarantees that.
+    INVARIANT(
+      nroots == 2 * n_e,
+      "Valid QBM certificate should have twice as much roots as the "
+      "existential variables.");
 
     model_bdds.resize(e_max+1, NULL);
 

src/solvers/qbf/qbf_squolem.cpp

@@ -23,7 +23,8 @@ qbf_squolemt::~qbf_squolemt()
 
 tvt qbf_squolemt::l_get(literalt a) const
 {
-  assert(false);
+  UNREACHABLE;
+  return tvt(false);
 }
 
 const std::string qbf_squolemt::solver_text()

src/solvers/qbf/qbf_squolem_core.cpp

@@ -189,11 +189,12 @@ const exprt qbf_squolem_coret::f_get(literalt l)
 {
   if(squolem->isUniversal(l.var_no()))
   {
-    assert(l.var_no()!=0);
+    INVARIANT_WITH_DIAGNOSTICS(
+      l.var_no() != 0, "Unknown variable: ", std::to_string(l.var_no()));
     variable_mapt::const_iterator it=variable_map.find(l.var_no());
 
-    if(it==variable_map.end())
-      throw "variable map error";
+    INVARIANT(
+      it != variable_map.end(), "Variable not found in the variable map.");
 
     const exprt &sym=it->second.first;
     unsigned index=it->second.second;

src/solvers/qbf/qdimacs_cnf.cpp

@@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "qdimacs_cnf.h"
 
 #include <iostream>
-#include <cassert>
+#include <util/invariant.h>
 
 void qdimacs_cnft::write_qdimacs_cnf(std::ostream &out)
 {
@@ -31,9 +31,12 @@ void qdimacs_cnft::write_prefix(std::ostream &out) const
   {
     const quantifiert &quantifier=*it;
 
-    assert(quantifier.var_no<no_variables());
+    INVARIANT_WITH_DIAGNOSTICS(
+      quantifier.var_no < no_variables(),
+      "Unknown variable: ",
+      std::to_string(quantifier.var_no));
     // double quantification?
-    assert(!quantified[quantifier.var_no]);
+    INVARIANT(!quantified[quantifier.var_no], "No double quantification.");
     quantified[quantifier.var_no]=true;
 
     switch(quantifier.type)
@@ -47,7 +50,7 @@ void qdimacs_cnft::write_prefix(std::ostream &out) const
       break;
 
     default:
-      assert(false);
+      UNREACHABLE;
     }
 
     out << " " << quantifier.var_no << " 0\n";