6#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
7#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT2_INCREMENTAL_DECISION_PROCEDURE_H
15#include <unordered_map>
16#include <unordered_set>
44 void set_to(
const exprt &expr,
bool value)
override;
47 void push(
const std::vector<exprt> &assumptions)
override;
77 std::unordered_map<exprt, smt_identifier_termt, irep_hash>
79 std::unordered_map<exprt, smt_identifier_termt, irep_hash>
resultt
Result of running the decision procedure.
Base class for all expressions.
Class that provides messages with a built-in verbosity 'level'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
size_t number_of_solver_calls
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 ensure_handle_for_expr_defined(const exprt &expr)
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.