40 temp_file_stdout(
"smt2_dec_stdout_",
""),
41 temp_file_stderr(
"smt2_dec_stderr_",
"");
45 std::ofstream problem_out(
46 temp_file_problem(), std::ios_base::out | std::ios_base::trunc);
51 std::vector<std::string> argv;
52 std::string stdin_filename;
57 argv = {
"boolector",
"--smt2", temp_file_problem(),
"-m"};
61 argv = {
"smt2_solver"};
62 stdin_filename = temp_file_problem();
78 argv = {
"cvc4",
"-L",
"smt2", temp_file_problem()};
87 "-preprocessor.toplevel_propagation=true",
88 "-preprocessor.simplification=7",
89 "-dpll.branching_random_frequency=0.01",
90 "-dpll.branching_random_invalidate_phase_cache=true",
91 "-dpll.restart_strategy=3",
92 "-dpll.glucose_var_activity=true",
93 "-dpll.glucose_learnt_minimization=true",
94 "-theory.bv.eager=true",
95 "-theory.bv.bit_blast_mode=1",
96 "-theory.bv.delay_propagated_eqs=true",
98 "-theory.fp.bit_blast_mode=2",
99 "-theory.arr.mode=1"};
101 stdin_filename = temp_file_problem();
107 argv = {
"yices-smt2", temp_file_problem()};
111 argv = {
"z3",
"-smt2", temp_file_problem()};
119 run(argv[0], argv, stdin_filename, temp_file_stdout(), temp_file_stderr());
123 error() <<
"error running SMT2 solver" <<
eom;
127 std::ifstream in(temp_file_stdout());
139 typedef std::unordered_map<irep_idt, irept> valuest;
146 if(parsed.
id()==
"sat")
148 else if(parsed.
id()==
"unsat")
150 else if(parsed.
id()==
"" &&
152 parsed.
get_sub().front().get_sub().size()==2)
165 else if(parsed.
id()==
"" &&
167 parsed.
get_sub().front().id()==
"error")
173 error() <<
"SMT2 solver returned error message:\n" 174 <<
"\t\"" << parsed.
get_sub()[1].id() <<
"\"" <<
eom;
183 const irept &value=values[conv_id];
184 assignment.second.value=
parse_rec(value, assignment.second.type);
irept smt2irep(std::istream &in)
std::stringstream stringstream
resultt read_result(std::istream &in)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
virtual resultt dec_solve()
identifier_mapt identifier_map
const irep_idt & id() const
API to expression classes.
int run(const std::string &what, const std::vector< std::string > &argv)
Base class for tree-like data structures with sharing.
std::string convert_identifier(const irep_idt &identifier)
virtual std::string decision_procedure_text() const
#define UNREACHABLE
This should be used to mark dead code.
std::size_t no_boolean_variables
exprt parse_rec(const irept &s, const typet &type)
std::vector< bool > boolean_assignment
void write_footer(std::ostream &)