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