43 temp_file_stdout(
"smt2_dec_stdout_",
""),
44 temp_file_stderr(
"smt2_dec_stderr_",
"");
48 std::ofstream problem_out(
49 temp_file_problem(), std::ios_base::out | std::ios_base::trunc);
54 std::vector<std::string> argv;
55 std::string stdin_filename;
60 argv = {
"boolector",
"--smt2", temp_file_problem(),
"-m"};
64 argv = {
"smt2_solver"};
65 stdin_filename = temp_file_problem();
81 argv = {
"cvc4",
"-L",
"smt2", temp_file_problem()};
90 "-preprocessor.toplevel_propagation=true",
91 "-preprocessor.simplification=7",
92 "-dpll.branching_random_frequency=0.01",
93 "-dpll.branching_random_invalidate_phase_cache=true",
94 "-dpll.restart_strategy=3",
95 "-dpll.glucose_var_activity=true",
96 "-dpll.glucose_learnt_minimization=true",
97 "-theory.bv.eager=true",
98 "-theory.bv.bit_blast_mode=1",
99 "-theory.bv.delay_propagated_eqs=true",
101 "-theory.fp.bit_blast_mode=2",
102 "-theory.arr.mode=1"};
104 stdin_filename = temp_file_problem();
110 argv = {
"yices-smt2", temp_file_problem()};
114 argv = {
"z3",
"-smt2", temp_file_problem()};
122 run(argv[0], argv, stdin_filename, temp_file_stdout(), temp_file_stderr());
131 std::ifstream in(temp_file_stdout());
143 typedef std::unordered_map<irep_idt, irept> valuest;
150 if(!parsed_opt.has_value())
153 const auto &parsed = parsed_opt.value();
155 if(parsed.id()==
"sat")
157 else if(parsed.id()==
"unsat")
160 parsed.id().empty() && parsed.get_sub().size() == 1 &&
161 parsed.get_sub().front().get_sub().size() == 2)
175 parsed.id().empty() && parsed.get_sub().size() == 2 &&
176 parsed.get_sub().front().id() ==
"error")
183 log.error() <<
"SMT2 solver returned error message:\n"
184 <<
"\t\"" << parsed.get_sub()[1].id() <<
"\""
194 const irept &value=values[conv_id];
195 assignment.second.value=
parse_rec(value, assignment.second.type);