new decision_proceduret interface

Author: Daniel Kroening

src/goto-checker/solver_factory.h

@@ -16,6 +16,8 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <solvers/smt2/smt2_dec.h>
 
+#include <fstream>
+
 class message_handlert;
 class namespacet;
 class optionst;

src/goto-instrument/accelerate/scratch_program.cpp

@@ -13,7 +13,7 @@ Author: Matt Lewis
 
 #include <util/fixedbv.h>
 
-#include <solvers/prop/decision_procedure.h>
+#include <solvers/decision_procedure.h>
 
 #include <goto-symex/slice.h>
 

src/solvers/Makefile

@@ -79,6 +79,7 @@ SRC = $(BOOLEFORCE_SRC) \
       $(PICOSAT_SRC) \
       $(SQUOLEM2_SRC) \
       $(CADICAL_SRC) \
+      decision_procedure.cpp \
       flattening/arrays.cpp \
       flattening/boolbv.cpp \
       flattening/boolbv_abs.cpp \
@@ -144,12 +145,12 @@ SRC = $(BOOLEFORCE_SRC) \
       bdd/miniBDD/miniBDD.cpp \
       prop/bdd_expr.cpp \
       prop/cover_goals.cpp \
-      prop/decision_procedure.cpp \
       prop/literal.cpp \
       prop/prop_minimize.cpp \
       prop/prop.cpp \
       prop/prop_conv.cpp \
       prop/prop_conv_solver.cpp \
+      prop/prop_decision_procedure.cpp \
       qbf/qbf_quantor.cpp \
       qbf/qbf_qube.cpp \
       qbf/qbf_qube_core.cpp \

src/solvers/prop/decision_procedure.cpp renamed to src/solvers/decision_procedure.cpp

@@ -9,16 +9,13 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Decision Procedure Interface
 
-#ifndef CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_H
-#define CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_H
+#ifndef CPROVER_SOLVERS_DECISION_PROCEDURE_H
+#define CPROVER_SOLVERS_DECISION_PROCEDURE_H
 
 #include <iosfwd>
 #include <string>
 
-#include "literal.h"
-
 class exprt;
-class tvt;
 
 class decision_proceduret
 {
@@ -33,9 +30,6 @@ class decision_proceduret
   /// For a Boolean expression \p expr, add the constraint 'not expr'
   void set_to_false(const exprt &expr);
 
-  /// Convert a Boolean expression and return the corresponding literal
-  virtual literalt convert(const exprt &expr) = 0;
-
   /// Result of running the decision procedure
   enum class resultt
   {
@@ -52,10 +46,6 @@ class decision_proceduret
   /// Return `nil` if not available
   virtual exprt get(const exprt &expr) const = 0;
 
-  /// Return value of literal \p l from satisfying assignment.
-  /// Return tvt::UNKNOWN if not available
-  virtual tvt l_get(literalt l) const = 0;
-
   /// Print satisfying assignment to \p out
   virtual void print_assignment(std::ostream &out) const = 0;
 
@@ -80,4 +70,4 @@ operator<<(decision_proceduret &dest, const exprt &src)
   return dest;
 }
 
-#endif // CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_H
+#endif // CPROVER_SOLVERS_DECISION_PROCEDURE_H

src/solvers/prop/decision_procedure.h renamed to src/solvers/decision_procedure.h

@@ -14,8 +14,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <list>
 
-#include "decision_procedure.h"
 #include "literal.h"
+#include "prop_decision_procedure.h"
 
 class message_handlert;
 class prop_convt;

src/solvers/prop/cover_goals.h

@@ -10,18 +10,16 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_SOLVERS_PROP_PROP_CONV_H
 #define CPROVER_SOLVERS_PROP_PROP_CONV_H
 
-#include "decision_procedure.h"
+#include "prop_decision_procedure.h"
 
 // API that provides a "handle" in the form of a literalt
 // for expressions.
 
-class prop_convt:public decision_proceduret
+class prop_convt : public prop_decision_proceduret
 {
 public:
   virtual ~prop_convt() { }
 
-  using decision_proceduret::operator();
-
   // incremental solving
   virtual void set_frozen(literalt a);
   virtual void set_frozen(const bvt &);

src/solvers/prop/prop_conv.h

@@ -16,11 +16,11 @@ Author: Daniel Kroening, [email protected]
 #include <util/message.h>
 #include <util/std_expr.h>
 
-#include "decision_procedure.h"
 #include "literal.h"
 #include "literal_expr.h"
 #include "prop.h"
 #include "prop_conv.h"
+#include "prop_decision_procedure.h"
 #include "solver_resource_limits.h"
 
 class prop_conv_solvert : public prop_convt, public solver_resource_limitst

src/solvers/prop/prop_conv_solver.h

@@ -0,0 +1,13 @@
+/*******************************************************************\
+
+Module: Decision Procedure Interface with Propositional Handles
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Decision Procedure Interface with Propositional Handles
+
+#include "prop_decision_procedure.h"
+

src/solvers/prop/prop_decision_procedure.cpp

@@ -0,0 +1,32 @@
+/*******************************************************************\
+
+Module: Decision Procedure Interface with Propositional Handles
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+/// \file
+/// Decision Procedure Interface with Propositional Handles
+
+#ifndef CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_H
+#define CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_H
+
+#include "../decision_procedure.h"
+
+#include "literal.h"
+
+#include <util/threeval.h>
+
+class prop_decision_proceduret : public decision_proceduret
+{
+public:
+  /// Convert a Boolean expression and return the corresponding literal
+  virtual literalt convert(const exprt &expr) = 0;
+
+  /// Return value of literal \p l from satisfying assignment.
+  /// Return tvt::UNKNOWN if not available
+  virtual tvt l_get(literalt l) const = 0;
+};
+
+#endif // CPROVER_SOLVERS_PROP_DECISION_PROCEDURE_H

src/solvers/prop/prop_decision_procedure.h

@@ -18,6 +18,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "smt2irep.h"
 
+#include <fstream>
+
 std::string smt2_dect::decision_procedure_text() const
 {
   // clang-format off

src/solvers/smt2/smt2_dec.cpp

@@ -14,8 +14,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/message.h>
 
-#include <fstream>
-
 class smt2_stringstreamt
 {
 protected: