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 
11 #include <util/message.h>
12 #include <util/std_expr.h>
13 
14 #include <memory>
15 #include <unordered_map>
16 #include <unordered_set>
17 
18 class smt_commandt;
19 class message_handlert;
20 class namespacet;
22 
25 {
26 public:
34  const namespacet &_ns,
35  std::unique_ptr<smt_base_solver_processt> solver_process,
36  message_handlert &message_handler);
37 
38  // Implementation of public decision_proceduret member functions.
39  exprt handle(const exprt &expr) override;
40  exprt get(const exprt &expr) const override;
41  void print_assignment(std::ostream &out) const override;
42  std::string decision_procedure_text() const override;
43  std::size_t get_number_of_solver_calls() const override;
44  void set_to(const exprt &expr, bool value) override;
45 
46  // Implementation of public stack_decision_proceduret member functions.
47  void push(const std::vector<exprt> &assumptions) override;
48  void push() override;
49  void pop() override;
50 
51 protected:
52  // Implementation of protected decision_proceduret member function.
53  resultt dec_solve() override;
56  void define_dependent_functions(const exprt &expr);
57  void ensure_handle_for_expr_defined(const exprt &expr);
58 
59  const namespacet &ns;
60 
62 
63  std::unique_ptr<smt_base_solver_processt> solver_process;
65 
66  class sequencet
67  {
68  size_t next_id = 0;
69 
70  public:
71  size_t operator()()
72  {
73  return next_id++;
74  }
76 
77  std::unordered_map<exprt, smt_identifier_termt, irep_hash>
79  std::unordered_map<exprt, smt_identifier_termt, irep_hash>
81 };
82 
83 #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
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
std::unordered_map< exprt, smt_identifier_termt, irep_hash > expression_identifiers
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 define_dependent_functions(const exprt &expr)
Defines any functions which expr depends on, which have not yet been defined, along with their depend...
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.
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
std::unordered_map< exprt, smt_identifier_termt, irep_hash > expression_handle_identifiers
std::unique_ptr< smt_base_solver_processt > solver_process
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'.
class smt2_incremental_decision_proceduret::sequencet handle_sequence
smt2_incremental_decision_proceduret(const namespacet &_ns, std::unique_ptr< smt_base_solver_processt > solver_process, message_handlert &message_handler)
Decision procedure with incremental solving with contexts and assumptions.
API to expression classes.