Cleanup error handling in solvers/qbf #2961

xbauch · 2018-09-14T16:44:59Z

No description provided.

allredj

Passed Diffblue compatibility checks (cbmc commit: 6a24c2c).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/84858721

peterschrammel · 2018-09-17T17:06:20Z

src/solvers/qbf/qbf_bdd_core.cpp

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


Why is this required here and not below, eg in m_get?

peterschrammel · 2018-09-17T17:06:55Z

src/solvers/qbf/qbf_bdd_core.cpp

    {
+      INVARIANT(
+        it->type == quantifiert::UNIVERSAL,
+        "Only handles quantified variables.");


start with lower case (several occurrences)

xbauch · 2018-09-18T14:44:24Z

Lower cases and full stops fixed, redundant return statements removed.

allredj

Passed Diffblue compatibility checks (cbmc commit: fb13b74).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85159051

tautschnig · 2018-09-18T21:54:39Z

src/solvers/qbf/qbf_bdd_core.cpp

@@ -310,7 +312,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,


While at it: please use nullptr instead of NULL

tautschnig · 2018-09-18T21:55:01Z

src/solvers/qbf/qbf_quantor.cpp

 #include <cstdlib>
 #include <fstream>
+#include <util/invariant.h>


Nit-pick: add a blank line before this include.

tautschnig · 2018-09-18T21:55:20Z

src/solvers/qbf/qbf_qube.cpp

 #include <cstdlib>
 #include <fstream>
+#include <util/invariant.h>


Nit-pick: add a blank line before this include.

tautschnig · 2018-09-18T21:55:29Z

src/solvers/qbf/qbf_qube_core.cpp

 #include <cstring>
+#include <fstream>
+#include <util/invariant.h>


Move one line down to group with the mp_arith.h include

tautschnig · 2018-09-18T21:56:12Z

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>


Nit-pick: add a blank line before this include.

tautschnig · 2018-09-18T21:56:22Z

src/solvers/qbf/qbf_skizzo.cpp

 #include <cstdlib>
 #include <fstream>
+#include <util/invariant.h>


Nit-pick: add a blank line before this include.

tautschnig · 2018-09-18T21:56:29Z

src/solvers/qbf/qbf_skizzo_core.cpp

 #include <fstream>
+#include <util/invariant.h>


Nit-pick: add a blank line before this include.

tautschnig · 2018-09-18T21:57:42Z

src/solvers/qbf/qbf_skizzo_core.cpp

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


Remove the negation, i.e., the invariant is result, not !result

tautschnig · 2018-09-18T21:58:00Z

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>


Nit-pick: add a blank line before this include.

xbauch · 2018-09-19T07:53:14Z

Added blank lines before util/invariant.h includes, fixed the skizzo invariant condition typo.

tautschnig

Looks good to me, please squash and rebase.

xbauch · 2018-09-19T09:23:26Z

Squashed and rebased.

allredj

Passed Diffblue compatibility checks (cbmc commit: 706a529).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/85264387

xbauch requested review from chrisr-diffblue, kroening, peterschrammel, smowton and tautschnig as code owners September 14, 2018 16:44

allredj reviewed Sep 14, 2018

View reviewed changes

peterschrammel reviewed Sep 17, 2018

View reviewed changes

allredj reviewed Sep 18, 2018

View reviewed changes

tautschnig requested changes Sep 18, 2018

View reviewed changes

tautschnig approved these changes Sep 19, 2018

View reviewed changes

tautschnig assigned xbauch Sep 19, 2018

tautschnig added the Needs rebase label Sep 19, 2018

Cleanup error handling in solvers/qbf

706a529

xbauch force-pushed the cleanup_qbf branch from 3fffb36 to 706a529 Compare September 19, 2018 09:22

tautschnig removed the Needs rebase label Sep 19, 2018

xbauch merged commit 13d40b0 into diffblue:develop Sep 19, 2018

allredj reviewed Sep 19, 2018

View reviewed changes

xbauch deleted the cleanup_qbf branch December 4, 2018 08:57

Cleanup error handling in solvers/qbf #2961

Cleanup error handling in solvers/qbf #2961

Uh oh!

Conversation

xbauch commented Sep 14, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

xbauch commented Sep 18, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

xbauch commented Sep 19, 2018

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

xbauch commented Sep 19, 2018

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!