cprover
smt2_incremental_decision_procedure.h
Go to the documentation of this file.
1 // Author: Diffblue Ltd.
2 
5 
6 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
7 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
8 
10 
13 {
14 public:
18 
19  // Implementation of public decision_proceduret member functions.
20  exprt handle(const exprt &expr) override;
21  exprt get(const exprt &expr) const override;
22  void print_assignment(std::ostream &out) const override;
23  std::string decision_procedure_text() const override;
24  std::size_t get_number_of_solver_calls() const override;
25  void set_to(const exprt &expr, bool value) override;
26 
27  // Implementation of public stack_decision_proceduret member functions.
28  void push(const std::vector<exprt> &assumptions) override;
29  void push() override;
30  void pop() override;
31 
32 protected:
33  // Implementation of protected decision_proceduret member function.
34  resultt dec_solve() override;
35 
37  std::string solver_command;
39 };
40 
41 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
resultt
Result of running the decision procedure.
Base class for all expressions.
Definition: expr.h:54
exprt handle(const exprt &expr) override
Generate a handle, which is an expression that has the same value as the argument in any model that i...
resultt dec_solve() override
Run the decision procedure to solve the problem.
std::size_t get_number_of_solver_calls() const override
Return the number of incremental solver calls.
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
void push() override
Push a new context on the stack This context becomes a child context nested in the current context.
void pop() override
Pop whatever is on top of the stack.
std::string solver_command
This is where we store the solver command for reporting the solver used.
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
void set_to(const exprt &expr, bool value) override
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
Decision procedure with incremental solving with contexts and assumptions.