13 #if defined(__linux__) || \ 14 defined(__FreeBSD_kernel__) || \ 16 defined(__unix__) || \ 17 defined(__CYGWIN__) || \ 51 temp_out_filename.c_str(),
52 std::ios_base::out | std::ios_base::trunc);
59 if(temp_out_filename!=
"")
60 unlink(temp_out_filename.c_str());
62 if(temp_result_filename!=
"")
63 unlink(temp_result_filename.c_str());
86 command =
"boolector --smt2 " 93 command =
"cvc3 +model -lang smtlib -output-lang smtlib " 102 command =
"cvc4 -L smt2 " 111 command =
"mathsat -input=smt2" 112 " -preprocessor.toplevel_propagation=true" 113 " -preprocessor.simplification=7" 114 " -dpll.branching_random_frequency=0.01" 115 " -dpll.branching_random_invalidate_phase_cache=true" 116 " -dpll.restart_strategy=3" 117 " -dpll.glucose_var_activity=true" 118 " -dpll.glucose_learnt_minimization=true" 119 " -theory.bv.eager=true" 120 " -theory.bv.bit_blast_mode=1" 121 " -theory.bv.delay_propagated_eqs=true" 123 " -theory.fp.bit_blast_mode=2" 124 " -theory.arr.mode=1" 139 command =
"yices-smt2 " 146 command =
"z3 -smt2 " 156 #if defined(__linux__) || defined(__APPLE__) 160 int res=system(command.c_str());
163 error() <<
"error running SMT2 solver" <<
eom;
180 typedef std::unordered_map<irep_idt, irept, irep_id_hash> valuest;
187 if(parsed.
id()==
"sat")
189 else if(parsed.
id()==
"unsat")
191 else if(parsed.
id()==
"" &&
193 parsed.
get_sub().front().get_sub().size()==2)
204 else if(parsed.
id()==
"" &&
206 parsed.
get_sub().front().id()==
"error")
212 error() <<
"SMT2 solver returned error message:\n" 213 <<
"\t\"" << parsed.
get_sub()[1].id() <<
"\"" <<
eom;
219 for(identifier_mapt::iterator
225 const irept &value=values[conv_id];
226 it->second.value=
parse_rec(value, it->second.type);
232 const irept &value=values[
"B"+std::to_string(v)];
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
unsigned no_boolean_variables
std::string get_temporary_file(const std::string &prefix, const std::string &suffix)
Substitute for mkstemps (OpenBSD standard) for Windows, where it is unavailable.
exprt parse_rec(const irept &s, const typet &type)
std::vector< bool > boolean_assignment
void write_footer(std::ostream &)