22
33#include " smt2_incremental_decision_procedure.h"
44
5+ #include < solvers/smt2_incremental/convert_expr_to_smt.h>
6+ #include < solvers/smt2_incremental/smt_commands.h>
7+ #include < solvers/smt2_incremental/smt_core_theory.h>
8+ #include < solvers/smt2_incremental/smt_solver_process.h>
9+ #include < solvers/smt2_incremental/smt_terms.h>
510#include < util/expr.h>
11+ #include < util/namespace.h>
12+ #include < util/range.h>
13+ #include < util/std_expr.h>
14+ #include < util/string_utils.h>
15+ #include < util/symbol.h>
16+
17+ #include < stack>
18+
19+ // / \brief Find all sub expressions of the given \p expr which need to be
20+ // / expressed as separate smt commands.
21+ // / \return A collection of sub expressions, which need to be expressed as
22+ // / separate smt commands. This collection is in traversal order. It will
23+ // / include duplicate subexpressions, which need to be removed by the caller
24+ // / in order to avoid duplicate definitions.
25+ // / \note This pass over \p expr is tightly coupled to the implementation of
26+ // / `convert_expr_to_smt`. This is because any sub expressions which
27+ // / `convert_expr_to_smt` translates into function applications, must also be
28+ // / returned by this`gather_dependent_expressions` function.
29+ static std::vector<exprt> gather_dependent_expressions (const exprt &expr)
30+ {
31+ std::vector<exprt> dependent_expressions;
32+ expr.visit_pre ([&](const exprt &expr_node) {
33+ if (can_cast_expr<symbol_exprt>(expr_node))
34+ {
35+ dependent_expressions.push_back (expr_node);
36+ }
37+ });
38+ return dependent_expressions;
39+ }
40+
41+ // / \brief Defines any functions which \p expr depends on, which have not yet
42+ // / been defined, along with their dependencies in turn.
43+ void smt2_incremental_decision_proceduret::define_dependent_functions (
44+ const exprt &expr)
45+ {
46+ std::unordered_set<exprt, irep_hash> seen_expressions =
47+ make_range (expression_identifiers)
48+ .map ([](const std::pair<exprt, smt_identifier_termt> &expr_identifier) {
49+ return expr_identifier.first ;
50+ });
51+ std::stack<exprt> to_be_defined;
52+ const auto dependencies_needed = [&](const exprt &expr) {
53+ bool result = false ;
54+ for (const auto &dependency : gather_dependent_expressions (expr))
55+ {
56+ if (!seen_expressions.insert (dependency).second )
57+ continue ;
58+ result = true ;
59+ to_be_defined.push (dependency);
60+ }
61+ return result;
62+ };
63+ dependencies_needed (expr);
64+ while (!to_be_defined.empty ())
65+ {
66+ const exprt current = to_be_defined.top ();
67+ if (dependencies_needed (current))
68+ continue ;
69+ if (const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(current))
70+ {
71+ const irep_idt &identifier = symbol_expr->get_identifier ();
72+ const symbolt *symbol = nullptr ;
73+ if (ns.lookup (identifier, symbol) || symbol->value .is_nil ())
74+ {
75+ const smt_declare_function_commandt function{
76+ smt_identifier_termt (
77+ identifier, convert_type_to_smt_sort (symbol_expr->type ())),
78+ {}};
79+ expression_identifiers.emplace (*symbol_expr, function.identifier ());
80+ solver_process->send (function);
81+ }
82+ else
83+ {
84+ if (dependencies_needed (symbol->value ))
85+ continue ;
86+ const smt_define_function_commandt function{
87+ symbol->name , {}, convert_expr_to_smt (symbol->value )};
88+ expression_identifiers.emplace (*symbol_expr, function.identifier ());
89+ solver_process->send (function);
90+ }
91+ }
92+ to_be_defined.pop ();
93+ }
94+ }
695
796smt2_incremental_decision_proceduret::smt2_incremental_decision_proceduret (
8- std::string solver_command)
9- : solver_command{std::move (solver_command)}, number_of_solver_calls{0 }
97+ const namespacet &_ns,
98+ std::unique_ptr<smt_base_solver_processt> _solver_process,
99+ message_handlert &message_handler)
100+ : ns{_ns},
101+ number_of_solver_calls{0 },
102+ solver_process (std::move(_solver_process)),
103+ log{message_handler}
104+ {
105+ solver_process->send (
106+ smt_set_option_commandt{smt_option_produce_modelst{true }});
107+ solver_process->send (smt_set_logic_commandt{
108+ smt_logic_quantifier_free_uninterpreted_functions_bit_vectorst{}});
109+ }
110+
111+ void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined (
112+ const exprt &expr)
10113{
114+ if (
115+ expression_handle_identifiers.find (expr) !=
116+ expression_handle_identifiers.cend ())
117+ {
118+ return ;
119+ }
120+
121+ define_dependent_functions (expr);
122+ smt_define_function_commandt function{
123+ " B" std::to_string (handle_sequence ()), {}, convert_expr_to_smt (expr)};
124+ expression_handle_identifiers.emplace (expr, function.identifier ());
125+ solver_process->send (function);
11126}
12127
13128exprt smt2_incremental_decision_proceduret::handle (const exprt &expr)
14129{
130+ log .debug () << " `handle` -\n " pretty (2 , 0 ) << messaget::eom;
131+ ensure_handle_for_expr_defined (expr);
15132 return expr;
16133}
17134
@@ -29,7 +146,7 @@ void smt2_incremental_decision_proceduret::print_assignment(
29146std::string
30147smt2_incremental_decision_proceduret::decision_procedure_text () const
31148{
32- return " incremental SMT2 solving via \" " solver_command + " \" "
149+ return " incremental SMT2 solving via " solver_process-> description () ;
33150}
34151
35152std::size_t
@@ -40,9 +157,22 @@ smt2_incremental_decision_proceduret::get_number_of_solver_calls() const
40157
41158void smt2_incremental_decision_proceduret::set_to (const exprt &expr, bool value)
42159{
43- UNIMPLEMENTED_FEATURE (
44- " `set_to` (" " true" " false" " ):\n "
45- expr.pretty (2 , 0 ));
160+ PRECONDITION (can_cast_type<bool_typet>(expr.type ()));
161+ log .debug () << " `set_to` (" " true" " false"
162+ << " ) -\n " pretty (2 , 0 ) << messaget::eom;
163+
164+ define_dependent_functions (expr);
165+ auto converted_term = [&]() -> smt_termt {
166+ const auto expression_handle_identifier =
167+ expression_handle_identifiers.find (expr);
168+ if (expression_handle_identifier != expression_handle_identifiers.cend ())
169+ return expression_handle_identifier->second ;
170+ else
171+ return convert_expr_to_smt (expr);
172+ }();
173+ if (!value)
174+ converted_term = smt_core_theoryt::make_not (converted_term);
175+ solver_process->send (smt_assert_commandt{converted_term});
46176}
47177
48178void smt2_incremental_decision_proceduret::push (
@@ -69,5 +199,7 @@ void smt2_incremental_decision_proceduret::pop()
69199decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve ()
70200{
71201 ++number_of_solver_calls;
72- UNIMPLEMENTED_FEATURE (" solving."
202+ solver_process->send (smt_check_sat_commandt{});
203+ const smt_responset result = solver_process->receive_response ();
204+ UNIMPLEMENTED_FEATURE (" handling solver response."
73205}
0 commit comments