cprover
Loading...
Searching...
No Matches
decision_procedure.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Decision Procedure Interface
4
5Author: 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
18class exprt;
19
21{
22public:
25 virtual void set_to(const exprt &expr, bool value) = 0;
26
28 void set_to_true(const exprt &expr);
29
31 void set_to_false(const exprt &expr);
32
40 virtual exprt handle(const exprt &expr) = 0;
41
43 enum class resultt
44 {
48 };
49
52
56 virtual exprt get(const exprt &expr) const = 0;
57
59 virtual void print_assignment(std::ostream &out) const = 0;
60
62 virtual std::string decision_procedure_text() const = 0;
63
65 virtual std::size_t get_number_of_solver_calls() const = 0;
66
67 virtual ~decision_proceduret();
68
69protected:
71 virtual resultt dec_solve() = 0;
72};
73
76operator<<(decision_proceduret &dest, const exprt &src)
77{
78 dest.set_to_true(src);
79 return dest;
80}
81
82#endif // CPROVER_SOLVERS_DECISION_PROCEDURE_H
resultt operator()()
Run the decision procedure to solve the problem.
virtual std::size_t get_number_of_solver_calls() const =0
Return the number of incremental solver calls.
resultt
Result of running the decision procedure.
virtual void print_assignment(std::ostream &out) const =0
Print satisfying assignment to out.
virtual exprt get(const exprt &expr) const =0
Return expr with variables replaced by values from satisfying assignment if available.
virtual exprt handle(const exprt &expr)=0
Generate a handle, which is an expression that has the same value as the argument in any model that i...
void set_to_false(const exprt &expr)
For a Boolean expression expr, add the constraint 'not expr'.
void set_to_true(const exprt &expr)
For a Boolean expression expr, add the constraint 'expr'.
virtual void set_to(const exprt &expr, bool value)=0
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
virtual resultt dec_solve()=0
Run the decision procedure to solve the problem.
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