13 #if defined(__linux__) || \ 14 defined(__FreeBSD_kernel__) || \ 16 defined(__unix__) || \ 17 defined(__CYGWIN__) || \ 51 std::ios_base::out | std::ios_base::trunc);
85 command =
"boolector --smt2 " 92 command =
"cvc3 +model -lang smtlib -output-lang smtlib " 101 command =
"cvc4 -L smt2 " 110 command =
"mathsat -input=smt2" 111 " -preprocessor.toplevel_propagation=true" 112 " -preprocessor.simplification=7" 113 " -dpll.branching_random_frequency=0.01" 114 " -dpll.branching_random_invalidate_phase_cache=true" 115 " -dpll.restart_strategy=3" 116 " -dpll.glucose_var_activity=true" 117 " -dpll.glucose_learnt_minimization=true" 118 " -theory.bv.eager=true" 119 " -theory.bv.bit_blast_mode=1" 120 " -theory.bv.delay_propagated_eqs=true" 122 " -theory.fp.bit_blast_mode=2" 123 " -theory.arr.mode=1" 130 command =
"yices-smt2 " 137 command =
"z3 -smt2 " 147 #if defined(__linux__) || defined(__APPLE__) 151 int res=system(command.c_str());
154 error() <<
"error running SMT2 solver" <<
eom;
171 typedef std::unordered_map<irep_idt, irept> valuest;
178 if(parsed.
id()==
"sat")
180 else if(parsed.
id()==
"unsat")
182 else if(parsed.
id()==
"" &&
184 parsed.
get_sub().front().get_sub().size()==2)
197 else if(parsed.
id()==
"" &&
199 parsed.
get_sub().front().id()==
"error")
205 error() <<
"SMT2 solver returned error message:\n" 206 <<
"\t\"" << parsed.
get_sub()[1].id() <<
"\"" <<
eom;
215 const irept &value=values[conv_id];
216 assignment.second.value=
parse_rec(value, assignment.second.type);
irept smt2irep(std::istream &in)
std::stringstream stringstream
resultt read_result(std::istream &in)
virtual resultt dec_solve()
static mstreamt & eom(mstreamt &m)
identifier_mapt identifier_map
std::string temp_result_filename
const irep_idt & id() const
API to expression classes.
std::string temp_out_filename
Base class for tree-like data structures with sharing.
std::string convert_identifier(const irep_idt &identifier)
virtual std::string decision_procedure_text() const
std::string get_temporary_file(const std::string &prefix, const std::string &suffix)
Substitute for mkstemps (OpenBSD standard) for Windows, where it is unavailable.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
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 &)