Lower-case invariant messages

Author: Petr Bauch

src/solvers/qbf/qbf_bdd_core.cpp

@@ -81,7 +81,6 @@ qbf_bdd_coret::~qbf_bdd_coret()
 tvt qbf_bdd_coret::l_get(literalt a) const
 {
   UNREACHABLE;
-  return tvt(false);
 }
 
 const std::string qbf_bdd_coret::solver_text()
@@ -126,7 +125,7 @@ propt::resultt qbf_bdd_coret::prop_solve()
     {
       INVARIANT(
         it->type == quantifiert::UNIVERSAL,
-        "Only handles quantified variables.");
+        "only handles quantified variables");
       #if 0
       std::cout << "BDD A: " << var << ", " <<
         matrix->nodeCount() << " nodes\n";
@@ -270,16 +269,16 @@ const exprt qbf_bdd_certificatet::f_get(literalt l)
 {
   quantifiert q;
   PRECONDITION_WITH_DIAGNOSTICS(
-    !find_quantifier(l, q), "No model for unquantified variables.");
+    !find_quantifier(l, q), "no model for unquantified variables");
 
   // universal?
   if(q.type==quantifiert::UNIVERSAL)
   {
-    INVARIANT(l.var_no() != 0, "Input literal wasn't properly initialized.");
+    INVARIANT(l.var_no() != 0, "input literal wasn't properly initialized");
     variable_mapt::const_iterator it=variable_map.find(l.var_no());
 
     INVARIANT(
-      it != variable_map.end(), "Variable not found in the variable map.");
+      it != variable_map.end(), "variable not found in the variable map");
 
     const exprt &sym=it->second.first;
     unsigned index=it->second.second;
@@ -296,7 +295,7 @@ const exprt qbf_bdd_certificatet::f_get(literalt l)
     // skolem functions for existentials
     INVARIANT(
       q.type == quantifiert::EXISTENTIAL,
-      "Only quantified literals are supported.");
+      "only quantified literals are supported");
 
     function_cachet::const_iterator it=function_cache.find(l.var_no());
     if(it!=function_cache.end())
@@ -315,7 +314,7 @@ const exprt qbf_bdd_certificatet::f_get(literalt l)
 
     INVARIANT(
       model_bdds[l.var_no()] != NULL,
-      "There must be a model BDD for the literal.");
+      "there must be a model BDD for the literal");
     BDD &model=*model_bdds[l.var_no()];
 
     #if 0

src/solvers/qbf/qbf_quantor.cpp

@@ -23,7 +23,6 @@ qbf_quantort::~qbf_quantort()
 tvt qbf_quantort::l_get(literalt) const
 {
   UNREACHABLE;
-  return tvt::unknown();
 }
 
 const std::string qbf_quantort::solver_text()

src/solvers/qbf/qbf_qube.cpp

@@ -25,7 +25,6 @@ qbf_qubet::~qbf_qubet()
 tvt qbf_qubet::l_get(literalt) const
 {
   UNREACHABLE;
-  return tvt(false);
 }
 
 const std::string qbf_qubet::solver_text()

src/solvers/qbf/qbf_skizzo.cpp

@@ -25,7 +25,6 @@ qbf_skizzot::~qbf_skizzot()
 tvt qbf_skizzot::l_get(literalt) const
 {
   UNREACHABLE;
-  return tvt(false);
 }
 
 const std::string qbf_skizzot::solver_text()

src/solvers/qbf/qbf_skizzo_core.cpp

@@ -197,7 +197,7 @@ bool qbf_skizzo_coret::get_certificate(void)
 
     INVARIANT_WITH_DIAGNOSTICS(
       line == "# QBM file, 1.3",
-      "A QBM file has to start with this exact string: ",
+      "QBM file has to start with this exact string: ",
       "# QBM file, 1.3");
 
     while(in)
@@ -217,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);
-    INVARIANT(n_e != 0, "There has to be at least one existential variable.");
+    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);
@@ -227,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));
-      INVARIANT(cur != 0, "Variable numbering starts with 1.");
+      INVARIANT(cur != 0, "variable numbering starts with 1");
 
       e_list[i]=cur;
       if(cur>e_max)
@@ -236,7 +236,7 @@ bool qbf_skizzo_coret::get_certificate(void)
       e_lists=e_lists.substr(space+1);
     }
 
-    INVARIANT(!result, "Existential mapping from sKizzo missing.");
+    INVARIANT(!result, "existential mapping from sKizzo missing");
 
     in.close();
 
@@ -273,8 +273,8 @@ bool qbf_skizzo_coret::get_certificate(void)
 
     INVARIANT(
       nroots == 2 * n_e,
-      "Valid QBM certificate should have twice as much roots as the "
-      "existential variables.");
+      "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

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

src/solvers/qbf/qbf_squolem_core.cpp

@@ -190,11 +190,11 @@ const exprt qbf_squolem_coret::f_get(literalt l)
   if(squolem->isUniversal(l.var_no()))
   {
     INVARIANT_WITH_DIAGNOSTICS(
-      l.var_no() != 0, "Unknown variable: ", std::to_string(l.var_no()));
+      l.var_no() != 0, "unknown variable: ", std::to_string(l.var_no()));
     variable_mapt::const_iterator it=variable_map.find(l.var_no());
 
     INVARIANT(
-      it != variable_map.end(), "Variable not found in the variable map.");
+      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

@@ -33,10 +33,10 @@ void qdimacs_cnft::write_prefix(std::ostream &out) const
 
     INVARIANT_WITH_DIAGNOSTICS(
       quantifier.var_no < no_variables(),
-      "Unknown variable: ",
+      "unknown variable: ",
       std::to_string(quantifier.var_no));
     // double quantification?
-    INVARIANT(!quantified[quantifier.var_no], "No double quantification.");
+    INVARIANT(!quantified[quantifier.var_no], "no double quantification");
     quantified[quantifier.var_no]=true;
 
     switch(quantifier.type)