Merge pull request diffblue#2402 from tautschnig/vs-no-dummy

Remove dummy implementations from propt

Author: Daniel Kroening

src/solvers/prop/prop.cpp

@@ -8,32 +8,13 @@ Author: Daniel Kroening, [email protected]
 
 #include "prop.h"
 
-#include <cassert>
-
 /// asserts a==b in the propositional formula
 void propt::set_equal(literalt a, literalt b)
 {
   lcnf(a, !b);
   lcnf(!a, b);
 }
 
-void propt::set_assignment(literalt a, bool value)
-{
-  assert(false);
-}
-
-void propt::copy_assignment_from(const propt &src)
-{
-  assert(false);
-}
-
-/// \return true iff the given literal is part of the final conflict
-bool propt::is_in_conflict(literalt l) const
-{
-  assert(false);
-  return false;
-}
-
 /// generates a bitvector of given width with new variables
 /// \return bitvector
 bvt propt::new_variables(std::size_t width)

src/solvers/prop/prop.h

@@ -98,13 +98,13 @@ class propt:public messaget
 
   // satisfying assignment
   virtual tvt l_get(literalt a) const=0;
-  virtual void set_assignment(literalt a, bool value);
-  virtual void copy_assignment_from(const propt &prop);
+  virtual void set_assignment(literalt a, bool value) = 0;
 
-  // Returns true if an assumption is in the final conflict.
-  // Note that only literals that are assumptions (see set_assumptions)
-  // may be queried.
-  virtual bool is_in_conflict(literalt l) const;
+  /// Returns true if an assumption is in the final conflict.
+  /// Note that only literals that are assumptions (see set_assumptions)
+  /// may be queried.
+  /// \return true iff the given literal is part of the final conflict
+  virtual bool is_in_conflict(literalt l) const = 0;
   virtual bool has_is_in_conflict() const { return false; }
 
   // an incremental solver may remove any variables that aren't frozen

src/solvers/sat/dimacs_cnf.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "dimacs_cnf.h"
 
+#include <util/invariant.h>
 #include <util/magic.h>
 
 #include <iostream>
@@ -18,6 +19,17 @@ dimacs_cnft::dimacs_cnft():break_lines(false)
 {
 }
 
+void dimacs_cnft::set_assignment(literalt a, bool value)
+{
+  UNIMPLEMENTED;
+}
+
+bool dimacs_cnft::is_in_conflict(literalt l) const
+{
+  UNREACHABLE;
+  return false;
+}
+
 dimacs_cnf_dumpt::dimacs_cnf_dumpt(std::ostream &_out):out(_out)
 {
 }

src/solvers/sat/dimacs_cnf.h

@@ -24,11 +24,14 @@ class dimacs_cnft:public cnf_clause_listt
 
   // dummy functions
 
-  virtual const std::string solver_text()
+  const std::string solver_text() override
   {
     return "DIMACS CNF";
   }
 
+  void set_assignment(literalt a, bool value) override;
+  bool is_in_conflict(literalt l) const override;
+
 protected:
   void write_problem_line(std::ostream &out);
   void write_clauses(std::ostream &out);

unit/miniBDD_new.cpp

@@ -163,6 +163,17 @@ class bdd_propt:public propt
 
   bool has_set_to() const override { return false; }
   bool cnf_handled_well() const override { return false; }
+
+  void set_assignment(literalt, bool) override
+  {
+    UNIMPLEMENTED;
+  }
+
+  bool is_in_conflict(literalt) const override
+  {
+    UNREACHABLE;
+    return false;
+  }
 };
 
 SCENARIO("miniBDD", "[core][solver][miniBDD]")