decision_procedure.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: Decision Procedure Interface
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_SOLVERS_DECISION_PROCEDURE_H
#define CPROVER_SOLVERS_DECISION_PROCEDURE_H
 
#include <iosfwd>
#include <string>
 
class exprt;
 
class decision_proceduret
{
public:
  virtual void set_to(const exprt &, bool value) = 0;
 
  void set_to_true(const exprt &);
 
  void set_to_false(const exprt &);
 
  virtual exprt handle(const exprt &) = 0;
 
  enum class resultt
  {
    D_SATISFIABLE,
    D_UNSATISFIABLE,
    D_ERROR
  };
 
  resultt operator()();
 
  resultt operator()(const exprt &assumption);
 
  virtual exprt get(const exprt &) const = 0;
 
  virtual void print_assignment(std::ostream &out) const = 0;
 
  virtual std::string decision_procedure_text() const = 0;
 
  virtual std::size_t get_number_of_solver_calls() const = 0;
 
  virtual ~decision_proceduret();
 
protected:
  virtual resultt dec_solve(const exprt &assumption) = 0;
};
 
inline decision_proceduret &
operator<<(decision_proceduret &dest, const exprt &src)
{
  dest.set_to_true(src);
  return dest;
}
 
#endif // CPROVER_SOLVERS_DECISION_PROCEDURE_H