cprover
smt2_incremental_decision_procedure.cpp
Go to the documentation of this file.
1 // Author: Diffblue Ltd.
2 
4 
12 #include <util/expr.h>
13 #include <util/namespace.h>
14 #include <util/nodiscard.h>
15 #include <util/range.h>
16 #include <util/std_expr.h>
17 #include <util/string_utils.h>
18 #include <util/symbol.h>
19 
20 #include <stack>
21 
25  smt_base_solver_processt &solver_process,
26  const smt_commandt &command)
27 {
28  solver_process.send(command);
29  auto response = solver_process.receive_response();
30  if(response.cast<smt_success_responset>())
31  return solver_process.receive_response();
32  else
33  return response;
34 }
35 
38 {
39  if(const auto error = response.cast<smt_error_responset>())
40  {
41  return "SMT solver returned an error message - " +
42  id2string(error->message());
43  }
44  if(response.cast<smt_unsupported_responset>())
45  {
46  return {"SMT solver does not support given command."};
47  }
48  return {};
49 }
50 
61 static std::vector<exprt> gather_dependent_expressions(const exprt &expr)
62 {
63  std::vector<exprt> dependent_expressions;
64  expr.visit_pre([&](const exprt &expr_node) {
65  if(can_cast_expr<symbol_exprt>(expr_node))
66  {
67  dependent_expressions.push_back(expr_node);
68  }
69  });
70  return dependent_expressions;
71 }
72 
76  const exprt &expr)
77 {
78  std::unordered_set<exprt, irep_hash> seen_expressions =
80  .map([](const std::pair<exprt, smt_identifier_termt> &expr_identifier) {
81  return expr_identifier.first;
82  });
83  std::stack<exprt> to_be_defined;
84  const auto push_dependencies_needed = [&](const exprt &expr) {
85  bool result = false;
86  for(const auto &dependency : gather_dependent_expressions(expr))
87  {
88  if(!seen_expressions.insert(dependency).second)
89  continue;
90  result = true;
91  to_be_defined.push(dependency);
92  }
93  return result;
94  };
95  push_dependencies_needed(expr);
96  while(!to_be_defined.empty())
97  {
98  const exprt current = to_be_defined.top();
99  if(push_dependencies_needed(current))
100  continue;
101  if(const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(current))
102  {
103  const irep_idt &identifier = symbol_expr->get_identifier();
104  const symbolt *symbol = nullptr;
105  if(ns.lookup(identifier, symbol) || symbol->value.is_nil())
106  {
107  const smt_declare_function_commandt function{
109  identifier, convert_type_to_smt_sort(symbol_expr->type())),
110  {}};
111  expression_identifiers.emplace(*symbol_expr, function.identifier());
112  solver_process->send(function);
113  }
114  else
115  {
116  if(push_dependencies_needed(symbol->value))
117  continue;
118  const smt_define_function_commandt function{
119  symbol->name, {}, convert_expr_to_smt(symbol->value)};
120  expression_identifiers.emplace(*symbol_expr, function.identifier());
121  solver_process->send(function);
122  }
123  }
124  to_be_defined.pop();
125  }
126 }
127 
129  const namespacet &_ns,
130  std::unique_ptr<smt_base_solver_processt> _solver_process,
131  message_handlert &message_handler)
132  : ns{_ns},
133  number_of_solver_calls{0},
134  solver_process(std::move(_solver_process)),
135  log{message_handler}
136 {
137  solver_process->send(
140  smt_logic_quantifier_free_uninterpreted_functions_bit_vectorst{}});
141 }
142 
144  const exprt &expr)
145 {
146  if(
147  expression_handle_identifiers.find(expr) !=
149  {
150  return;
151  }
152 
156  expression_handle_identifiers.emplace(expr, function.identifier());
157  solver_process->send(function);
158 }
159 
161 {
162  log.debug() << "`handle` -\n " << expr.pretty(2, 0) << messaget::eom;
164  return expr;
165 }
166 
168  const exprt &expr,
169  const std::unordered_map<exprt, smt_identifier_termt, irep_hash>
170  &expression_handle_identifiers,
171  const std::unordered_map<exprt, smt_identifier_termt, irep_hash>
172  &expression_identifiers)
173 {
174  const auto handle_find_result = expression_handle_identifiers.find(expr);
175  if(handle_find_result != expression_handle_identifiers.cend())
176  return handle_find_result->second;
177  const auto expr_find_result = expression_identifiers.find(expr);
178  if(expr_find_result != expression_identifiers.cend())
179  return expr_find_result->second;
180  return {};
181 }
182 
184 {
185  log.debug() << "`get` - \n " + expr.pretty(2, 0) << messaget::eom;
186  optionalt<smt_termt> descriptor =
188  if(!descriptor)
189  {
190  if(gather_dependent_expressions(expr).empty())
191  {
192  descriptor = convert_expr_to_smt(expr);
193  }
194  else
195  {
196  const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(expr);
197  INVARIANT(
198  symbol_expr, "Unhandled expressions are expected to be symbols");
199  // Note this case is currently expected to be encountered during trace
200  // generation for -
201  // * Steps which were removed via --slice-formula.
202  // * Getting concurrency clock values.
203  // The below implementation which returns the given expression was chosen
204  // based on the implementation of `smt2_convt::get` in the non-incremental
205  // smt2 decision procedure.
206  log.warning()
207  << "`get` attempted for unknown symbol, with identifier - \n"
208  << symbol_expr->get_identifier() << messaget::eom;
209  return expr;
210  }
211  }
212  const smt_get_value_commandt get_value_command{*descriptor};
213  const smt_responset response =
214  get_response_to_command(*solver_process, get_value_command);
215  const auto get_value_response = response.cast<smt_get_value_responset>();
216  if(!get_value_response)
217  {
218  throw analysis_exceptiont{
219  "Expected get-value response from solver, but received - " +
220  response.pretty()};
221  }
222  if(get_value_response->pairs().size() > 1)
223  {
224  throw analysis_exceptiont{
225  "Expected single valuation pair in get-value response from solver, but "
226  "received multiple pairs - " +
227  response.pretty()};
228  }
230  get_value_response->pairs()[0].get().value(), expr.type());
231 }
232 
234  std::ostream &out) const
235 {
236  UNIMPLEMENTED_FEATURE("printing of assignments.");
237 }
238 
239 std::string
241 {
242  return "incremental SMT2 solving via " + solver_process->description();
243 }
244 
245 std::size_t
247 {
248  return number_of_solver_calls;
249 }
250 
252 {
254  log.debug() << "`set_to` (" << std::string{value ? "true" : "false"}
255  << ") -\n " << expr.pretty(2, 0) << messaget::eom;
256 
258  auto converted_term = [&]() -> smt_termt {
259  const auto expression_handle_identifier =
261  if(expression_handle_identifier != expression_handle_identifiers.cend())
262  return expression_handle_identifier->second;
263  else
264  return convert_expr_to_smt(expr);
265  }();
266  if(!value)
267  converted_term = smt_core_theoryt::make_not(converted_term);
268  solver_process->send(smt_assert_commandt{converted_term});
269 }
270 
272  const std::vector<exprt> &assumptions)
273 {
274  for(const auto &assumption : assumptions)
275  {
277  "pushing of assumption:\n " + assumption.pretty(2, 0));
278  }
279  UNIMPLEMENTED_FEATURE("`push` of empty assumptions.");
280 }
281 
283 {
284  UNIMPLEMENTED_FEATURE("`push`.");
285 }
286 
288 {
289  UNIMPLEMENTED_FEATURE("`pop`.");
290 }
291 
292 NODISCARD
294  const smt_check_sat_response_kindt &response_kind)
295 {
296  if(response_kind.cast<smt_sat_responset>())
298  if(response_kind.cast<smt_unsat_responset>())
300  if(response_kind.cast<smt_unknown_responset>())
302  UNREACHABLE;
303 }
304 
306 {
308  const smt_responset result =
310  if(const auto check_sat_response = result.cast<smt_check_sat_responset>())
311  {
312  if(check_sat_response->kind().cast<smt_unknown_responset>())
313  log.error() << "SMT2 solver returned \"unknown\"" << messaget::eom;
314  return lookup_decision_procedure_result(check_sat_response->kind());
315  }
316  if(const auto problem = get_problem_messages(result))
317  throw analysis_exceptiont{*problem};
318  throw analysis_exceptiont{"Unexpected kind of response from SMT solver."};
319 }
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
resultt
Result of running the decision procedure.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
void visit_pre(std::function< void(exprt &)>)
Definition: expr.cpp:245
typet & type()
Return the type of the expression.
Definition: expr.h:82
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
bool is_nil() const
Definition: irep.h:376
mstreamt & error() const
Definition: message.h:399
mstreamt & warning() const
Definition: message.h:404
mstreamt & debug() const
Definition: message.h:429
static eomt eom
Definition: message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
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)
virtual smt_responset receive_response()=0
virtual void send(const smt_commandt &command)=0
Converts given SMT2 command to SMT2 string and sends it to the solver process.
const sub_classt * cast() const &
static const smt_function_application_termt::factoryt< nott > make_not
Stores identifiers in unescaped and unquoted form.
Definition: smt_terms.h:81
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:495
const sub_classt * cast() const &
Symbol table entry.
Definition: symbol.h:28
irep_idt name
The unique identifier.
Definition: symbol.h:40
exprt value
Initial value of symbol.
Definition: symbol.h:34
exprt construct_value_expr_from_smt(const smt_termt &value_term, const typet &type_to_construct)
Given a value_term and a type_to_construct, this function constructs a value exprt with a value based...
static smt_sortt convert_type_to_smt_sort(const bool_typet &type)
static smt_termt convert_expr_to_smt(const symbol_exprt &symbol_expr)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
#define NODISCARD
Definition: nodiscard.h:22
nonstd::optional< T > optionalt
Definition: optional.h:35
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
static smt_responset get_response_to_command(smt_base_solver_processt &solver_process, const smt_commandt &command)
Issues a command to the solving process which is expected to optionally return a success status follo...
static optionalt< std::string > get_problem_messages(const smt_responset &response)
static std::vector< exprt > gather_dependent_expressions(const exprt &expr)
Find all sub expressions of the given expr which need to be expressed as separate smt commands.
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
static NODISCARD decision_proceduret::resultt lookup_decision_procedure_result(const smt_check_sat_response_kindt &response_kind)
Decision procedure with incremental SMT2 solving.
#define UNIMPLEMENTED_FEATURE(FEATURE)
Definition: invariant.h:517
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.
bool can_cast_expr< symbol_exprt >(const exprt &base)
Definition: std_expr.h:173
bool can_cast_type< bool_typet >(const typet &base)
Definition: std_types.h:44
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Symbol table entry.