39 temp_file_stdout(
"smt2_dec_stdout_",
""),
40 temp_file_stderr(
"smt2_dec_stderr_",
"");
42 const auto write_problem_to_file = [&](std::ofstream problem_out) {
49 write_problem_to_file(std::ofstream(
50 temp_file_problem(), std::ios_base::out | std::ios_base::trunc));
52 std::vector<std::string> argv;
53 std::string stdin_filename;
58 argv = {
"boolector",
"--smt2", temp_file_problem(),
"-m"};
62 argv = {
"smt2_solver"};
63 stdin_filename = temp_file_problem();
79 argv = {
"cvc4",
"-L",
"smt2", temp_file_problem()};
88 "-preprocessor.toplevel_propagation=true",
89 "-preprocessor.simplification=7",
90 "-dpll.branching_random_frequency=0.01",
91 "-dpll.branching_random_invalidate_phase_cache=true",
92 "-dpll.restart_strategy=3",
93 "-dpll.glucose_var_activity=true",
94 "-dpll.glucose_learnt_minimization=true",
95 "-theory.bv.eager=true",
96 "-theory.bv.bit_blast_mode=1",
97 "-theory.bv.delay_propagated_eqs=true",
99 "-theory.fp.bit_blast_mode=2",
100 "-theory.arr.mode=1"};
102 stdin_filename = temp_file_problem();
108 argv = {
"yices-smt2", temp_file_problem()};
112 argv = {
"z3",
"-smt2", temp_file_problem()};
120 run(argv[0], argv, stdin_filename, temp_file_stdout(), temp_file_stderr());
129 std::ifstream in(temp_file_stdout());
141 typedef std::unordered_map<irep_idt, irept> valuest;
142 valuest parsed_values;
148 if(!parsed_opt.has_value())
151 const auto &parsed = parsed_opt.value();
153 if(parsed.id()==
"sat")
155 else if(parsed.id()==
"unsat")
157 else if(parsed.id() ==
"unknown")
160 log.error() <<
"SMT2 solver returned \"unknown\"" <<
messaget::eom;
164 parsed.id().empty() && parsed.get_sub().size() == 1 &&
165 parsed.get_sub().front().get_sub().size() == 2)
176 parsed_values[s0.
id()] =
s1;
179 parsed.id().empty() && parsed.get_sub().size() == 2 &&
180 parsed.get_sub().front().id() ==
"error")
186 const auto &message =
id2string(parsed.get_sub()[1].id());
190 message.find(
"must not contain quantifiers") != std::string::npos)
201 log.error() <<
"SMT2 solver returned error message:\n"
217 const irept &value = parsed_values[conv_id];
218 assignment.second.value =
parse_rec(value, assignment.second.type);
226 const auto found_parsed_value = parsed_values.find(boolean_identifier);
227 if(found_parsed_value != parsed_values.end())
228 return found_parsed_value->second.id() == ID_true;
230 const auto found_set_value =
231 set_values.find(
'|' + boolean_identifier +
'|');
233 return found_set_value->second;
237 return parsed_values[boolean_identifier].id() == ID_true;