cprover
Loading...
Searching...
No Matches
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
18class smt_commandt;
20class namespacet;
22
25{
26public:
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
51protected:
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
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
Decision procedure with incremental solving with contexts and assumptions.
API to expression classes.