CBMC
decision_procedure.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Decision Procedure Interface
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_SOLVERS_DECISION_PROCEDURE_H
13 #define CPROVER_SOLVERS_DECISION_PROCEDURE_H
14 
15 #include <iosfwd>
16 #include <string>
17 
18 class exprt;
19 
22 {
23 public:
26  virtual void set_to(const exprt &, bool value) = 0;
27 
29  void set_to_true(const exprt &);
30 
32  void set_to_false(const exprt &);
33 
41  virtual exprt handle(const exprt &) = 0;
42 
44  enum class resultt
45  {
48  D_ERROR
49  };
50 
54 
58  resultt operator()(const exprt &assumption);
59 
63  virtual exprt get(const exprt &) const = 0;
64 
66  virtual void print_assignment(std::ostream &out) const = 0;
67 
69  virtual std::string decision_procedure_text() const = 0;
70 
72  virtual std::size_t get_number_of_solver_calls() const = 0;
73 
74  virtual ~decision_proceduret();
75 
76 protected:
78  virtual resultt dec_solve(const exprt &assumption) = 0;
79 };
80 
83 operator<<(decision_proceduret &dest, const exprt &src)
84 {
85  dest.set_to_true(src);
86  return dest;
87 }
88 
89 #endif // CPROVER_SOLVERS_DECISION_PROCEDURE_H
An interface for a decision procedure for satisfiability problems.
virtual exprt get(const exprt &) const =0
Return expr with variables replaced by values from satisfying assignment if available.
resultt operator()()
Run the decision procedure to solve the problem This corresponds to SMT-LIB's check-sat.
void set_to_false(const exprt &)
For a Boolean expression expr, add the constraint 'not expr'.
virtual std::size_t get_number_of_solver_calls() const =0
Return the number of incremental solver calls.
virtual resultt dec_solve(const exprt &assumption)=0
Implementation of the decision procedure.
resultt
Result of running the decision procedure.
virtual void print_assignment(std::ostream &out) const =0
Print satisfying assignment to out.
virtual exprt handle(const exprt &)=0
Generate a handle, which is an expression that has the same value as the argument in any model that i...
void set_to_true(const exprt &)
For a Boolean expression expr, add the constraint 'expr'.
virtual void set_to(const exprt &, bool value)=0
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
virtual std::string decision_procedure_text() const =0
Return a textual description of the decision procedure.
Base class for all expressions.
Definition: expr.h:56
decision_proceduret & operator<<(decision_proceduret &dest, const exprt &src)
Add Boolean constraint src to decision procedure dest.
resultt
The result of goto verifying.
Definition: properties.h:45