cprover
smt2_incremental_decision_procedure.cpp
Go to the documentation of this file.
1 // Author: Diffblue Ltd.
2 
4 
5 #include <util/expr.h>
6 
8  std::string solver_command)
9  : solver_command{std::move(solver_command)}, number_of_solver_calls{0}
10 {
11 }
12 
14 {
15  return expr;
16 }
17 
19 {
20  UNIMPLEMENTED_FEATURE("`get` of:\n " + expr.pretty(2, 0));
21 }
22 
24  std::ostream &out) const
25 {
26  UNIMPLEMENTED_FEATURE("printing of assignments.");
27 }
28 
29 std::string
31 {
32  return "incremental SMT2 solving via \"" + solver_command + "\"";
33 }
34 
35 std::size_t
37 {
39 }
40 
42 {
44  "`set_to` (" + std::string{value ? "true" : "false"} + "):\n " +
45  expr.pretty(2, 0));
46 }
47 
49  const std::vector<exprt> &assumptions)
50 {
51  for(const auto &assumption : assumptions)
52  {
54  "pushing of assumption:\n " + assumption.pretty(2, 0));
55  }
56  UNIMPLEMENTED_FEATURE("`push` of empty assumptions.");
57 }
58 
60 {
61  UNIMPLEMENTED_FEATURE("`push`.");
62 }
63 
65 {
66  UNIMPLEMENTED_FEATURE("`pop`.");
67 }
68 
70 {
72  UNIMPLEMENTED_FEATURE("solving.");
73 }
UNIMPLEMENTED_FEATURE
#define UNIMPLEMENTED_FEATURE(FEATURE)
Definition: invariant.h:517
irept::pretty
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
smt2_incremental_decision_proceduret::push
void push() override
Push a new context on the stack This context becomes a child context nested in the current context.
Definition: smt2_incremental_decision_procedure.cpp:59
smt2_incremental_decision_proceduret::decision_procedure_text
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
Definition: smt2_incremental_decision_procedure.cpp:30
exprt
Base class for all expressions.
Definition: expr.h:54
smt2_incremental_decision_proceduret::dec_solve
resultt dec_solve() override
Run the decision procedure to solve the problem.
Definition: smt2_incremental_decision_procedure.cpp:69
smt2_incremental_decision_proceduret::get_number_of_solver_calls
std::size_t get_number_of_solver_calls() const override
Return the number of incremental solver calls.
Definition: smt2_incremental_decision_procedure.cpp:36
expr.h
smt2_incremental_decision_proceduret::print_assignment
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
Definition: smt2_incremental_decision_procedure.cpp:23
smt2_incremental_decision_proceduret::number_of_solver_calls
size_t number_of_solver_calls
Definition: smt2_incremental_decision_procedure.h:38
smt2_incremental_decision_proceduret::get
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
Definition: smt2_incremental_decision_procedure.cpp:18
smt2_incremental_decision_procedure.h
Decision procedure with incremental SMT2 solving.
decision_proceduret::resultt
resultt
Result of running the decision procedure.
Definition: decision_procedure.h:44
smt2_incremental_decision_proceduret::handle
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...
Definition: smt2_incremental_decision_procedure.cpp:13
smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret
smt2_incremental_decision_proceduret(std::string solver_command)
Definition: smt2_incremental_decision_procedure.cpp:7
smt2_incremental_decision_proceduret::pop
void pop() override
Pop whatever is on top of the stack.
Definition: smt2_incremental_decision_procedure.cpp:64
smt2_incremental_decision_proceduret::set_to
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'.
Definition: smt2_incremental_decision_procedure.cpp:41
smt2_incremental_decision_proceduret::solver_command
std::string solver_command
This is where we store the solver command for reporting the solver used.
Definition: smt2_incremental_decision_procedure.h:37