Clean up and document decision_proceduret

Complete documentation and reorder methods to make the interface
more readable.

Author: peterschrammel

src/solvers/prop/decision_procedure.cpp

@@ -14,3 +14,23 @@ Author: Daniel Kroening, [email protected]
 decision_proceduret::~decision_proceduret()
 {
 }
+
+literalt decision_proceduret::operator()(const exprt &expr)
+{
+  return convert(expr);
+}
+
+decision_proceduret::resultt decision_proceduret::operator()()
+{
+  return dec_solve();
+}
+
+void decision_proceduret::set_to_true(const exprt &expr)
+{
+  set_to(expr, true);
+}
+
+void decision_proceduret::set_to_false(const exprt &expr)
+{
+  set_to(expr, false);
+}

src/solvers/prop/decision_procedure.h

@@ -23,54 +23,59 @@ class tvt;
 class decision_proceduret
 {
 public:
-  virtual ~decision_proceduret();
+  /// For a Boolean expression \p expr, add the constraint 'expr' if \p value
+  /// is `true`, otherwise add 'not expr'
+  virtual void set_to(const exprt &expr, bool value) = 0;
 
-  // get a value from satisfying instance if satisfiable
-  // returns nil if not available
-  virtual exprt get(const exprt &expr) const=0;
+  /// For a Boolean expression \p expr, add the constraint 'expr'
+  void set_to_true(const exprt &expr);
 
-  // specialized variant of get
-  virtual tvt l_get(literalt) const = 0;
+  /// For a Boolean expression \p expr, add the constraint 'not expr'
+  void set_to_false(const exprt &expr);
 
-  // print satisfying assignment
-  virtual void print_assignment(std::ostream &out) const=0;
+  /// Convert a Boolean expression and return the corresponding literal
+  virtual literalt convert(const exprt &expr) = 0;
 
-  // add constraints
-  // the expression must be of Boolean type
-  virtual void set_to(const exprt &expr, bool value)=0;
+  /// Convert a Boolean expression and return the corresponding literal
+  literalt operator()(const exprt &);
 
-  void set_to_true(const exprt &expr)
-  { set_to(expr, true); }
+  /// Result of running the decision procedure
+  enum class resultt
+  {
+    D_SATISFIABLE,
+    D_UNSATISFIABLE,
+    D_ERROR
+  };
 
-  void set_to_false(const exprt &expr)
-  { set_to(expr, false); }
+  /// Run the decision procedure to solve the problem
+  resultt operator()();
 
-  // conversion to handle
-  virtual literalt convert(const exprt &expr) = 0;
+  /// Return \p expr with variables replaced by values from satisfying
+  /// assignment if available.
+  /// Return `nil` if not available
+  virtual exprt get(const exprt &expr) const = 0;
 
-  literalt operator()(const exprt &expr)
-  {
-    return convert(expr);
-  }
+  /// Return value of literal \p l from satisfying assignment.
+  /// Return tvt::UNKNOWN if not available
+  virtual tvt l_get(literalt l) const = 0;
 
-  // solve the problem
-  enum class resultt { D_SATISFIABLE, D_UNSATISFIABLE, D_ERROR };
+  /// Print satisfying assignment to \p out
+  virtual void print_assignment(std::ostream &out) const = 0;
 
-  resultt operator()()
-  {
-    return dec_solve();
-  }
-
-  // return a textual description of the decision procedure
-  virtual std::string decision_procedure_text() const=0;
+  /// Return a textual description of the decision procedure
+  virtual std::string decision_procedure_text() const = 0;
 
-  /// Returns the number of incremental solver calls
+  /// Return the number of incremental solver calls
   virtual std::size_t get_number_of_solver_calls() const = 0;
 
+  virtual ~decision_proceduret();
+
 protected:
+  /// Run the decision procedure to solve the problem
   virtual resultt dec_solve() = 0;
 };
 
+/// Push Boolean constraint \p src into decision procedure \p dest
 inline decision_proceduret &operator<<(
   decision_proceduret &dest,
   const exprt &src)