13 #if defined(__linux__) || \ 14 defined(__FreeBSD_kernel__) || \ 16 defined(__unix__) || \ 17 defined(__CYGWIN__) || \ 31 return "SMT1 "+
logic+
" using "+
32 (
solver==solvert::GENERIC?
"Generic":
33 solver==solvert::BOOLECTOR?
"Boolector":
34 solver==solvert::CVC3?
"CVC3":
35 solver==solvert::CVC4?
"CVC3":
36 solver==solvert::MATHSAT?
"MathSAT":
37 solver==solvert::OPENSMT?
"OpenSMT":
38 solver==solvert::YICES?
"Yices":
39 solver==solvert::Z3?
"Z3":
49 std::ios_base::out | std::ios_base::trunc);
80 case solvert::BOOLECTOR:
85 command =
"boolector --smt " 87 +
" --model --output " 92 command =
"cvc3 +model -lang smtlib -output-lang smtlib " 99 command =
"cvc4 -L smt1 " 105 case solvert::MATHSAT:
106 command =
"mathsat -model -input=smt" 111 case solvert::OPENSMT:
120 command =
"yices-smt --full-model " 137 #if defined(__linux__) || defined(__APPLE__) 141 int res=system(command.c_str());
144 error() <<
"error running SMT1 solver" <<
eom;
152 case solvert::BOOLECTOR:
159 error() <<
"no support for CVC4 with SMT1, use SMT2 instead" <<
eom;
162 case solvert::MATHSAT:
165 case solvert::OPENSMT:
174 case solvert::GENERIC:
176 error() <<
"Generic solver can't solve" <<
eom;
186 std::getline(in, line);
193 typedef std::unordered_map<std::string, valuet, string_hash> valuest;
196 while(std::getline(in, line))
198 std::size_t
pos=line.find(
' ');
199 if(pos!=std::string::npos && pos!=0)
201 std::string
id=std::string(line, 0, pos);
202 std::string value=std::string(line, pos+1, std::string::npos);
210 if(
id!=
"" &&
id[
id.size()-1]==
']')
212 std::size_t pos2=
id.find(
'[');
214 if(pos2!=std::string::npos)
216 std::string new_id=std::string(
id, 0, pos2);
217 std::string index=std::string(
id, pos2+1,
id.size()-pos2-2);
218 values[new_id].index_value_map[index]=value;
222 values[id].value=value;
228 for(identifier_mapt::iterator
233 it->second.value.make_nil();
235 const valuet &v=values[conv_id];
237 for(valuet::index_value_mapt::const_iterator
239 set_value(it->second, i_it->first, i_it->second);
249 std::string value=values[
"B"+std::to_string(v)].value;
257 else if(line==
"unsat")
260 error() <<
"Unexpected result from SMT-Solver: " << line <<
eom;
274 while(std::getline(in, line))
281 else if(line==
"unsat")
285 error() <<
"Unexpected result from SMT-Solver" <<
eom;
292 std::size_t
pos=src.find(
'[');
294 if(std::string(src, 0, 2)==
"bv" &&
295 pos!=std::string::npos &&
296 src[src.size()-1]==
']')
315 typedef std::unordered_map<std::string, valuet, string_hash> valuest;
318 while(std::getline(in, line))
322 else if(line==
"unsat")
324 else if(line.size()>=1 && line[0]==
'(')
329 std::size_t pos1=line.find(
' ');
330 std::size_t pos2=line.rfind(
' ');
331 if(pos1!=std::string::npos &&
332 pos2!=std::string::npos &&
335 std::string
id=std::string(line, pos1+1, pos2-pos1-1);
336 std::string value=std::string(line, pos2+1, line.size()-pos2-2);
341 std::size_t pos3=
id.rfind(
' ');
342 std::string index=std::string(pos3+1,
id.size()-pos3-1);
343 id=std::string(
id, 8, pos3-8);
347 values[id].value=value;
352 for(identifier_mapt::iterator
357 it->second.value.make_nil();
368 std::string value=values[
"B"+std::to_string(v)].value;
385 typedef std::unordered_map<std::string, std::string, string_hash> valuest;
388 while(std::getline(in, line))
392 else if(line==
"unsat")
396 std::size_t
pos=line.find(
" -> ");
397 if(pos!=std::string::npos)
398 values[std::string(line, 0, pos)]=
399 std::string(line, pos+4, std::string::npos);
403 for(identifier_mapt::iterator
408 it->second.value.make_nil();
410 std::string value=values[conv_id];
424 std::string value=values[
"B"+std::to_string(v)];
435 const std::string &value,
438 if(value.substr(0, 2)==
"bv")
440 std::string v=value.substr(2, value.find(
'[')-2);
441 size_t p = value.find(
'[')+1;
442 std::string w=value.substr(p, value.find(
']')-p);
447 if(type.
id()==ID_struct)
451 else if(type.
id()==ID_union)
464 else if(value.substr(0, 6)==
"(const")
466 std::string av = value.substr(7, value.length()-8);
481 else if(value.substr(0, 6)==
"(store")
483 size_t p1=value.rfind(
' ')+1;
484 size_t p2=value.rfind(
' ', p1-2)+1;
486 assert(p1!=std::string::npos && p2!=std::string::npos);
488 std::string elem = value.substr(p1, value.size()-p1-1);
489 std::string inx = value.substr(p2, p1-p2-1);
490 std::string array = value.substr(7, p2-8);
508 else if(value==
"false")
513 else if(value==
"true")
518 else if(value.substr(0, 8)==
"array_of")
523 while(fit!=
array_of_map.end() && fit->second!=id) fit++;
532 else if(type.
id()==ID_rational)
537 if(value.substr(0, 4)==
"val!")
557 typedef std::unordered_map<std::string, std::string, string_hash> valuest;
560 while(std::getline(in, line))
564 else if(line==
"unsat")
566 else if(line.find(
"Current scope level")!=std::string::npos ||
567 line.find(
"Variable Assignment")!=std::string::npos)
573 assert(line.substr(0, 13)==
" :assumption");
574 std::size_t
pos=line.find(
'(');
576 if(pos!=std::string::npos)
583 std::string ops = line.substr(pos+3, line.length()-pos-4);
584 std::size_t blank=ops.find(
' ');
585 var = ops.substr(0, blank);
586 val = ops.substr(blank+1, ops.length()-blank);
588 if((var.length()>=4 && var.substr(0, 4)==
"cvc3") ||
589 (val.length()>=4 && val.substr(0, 4)==
"cvc3") ||
592 else if((var.substr(0, 9)==
"array_of'") ||
593 (var.substr(0, 2)==
"bv" && val.substr(0, 2)!=
"bv"))
595 std::string t=var; var=val; val=t;
598 else if(line.substr(pos+1, 3)==
"not")
600 var = line.substr(pos+5, line.length()-pos-6);
605 var = line.substr(pos+1, line.length()-pos-2);
606 assert(var.find(
' ')==std::string::npos);
615 for(identifier_mapt::iterator
620 it->second.value.make_nil();
622 std::string value=values[conv_id];
626 if(value.substr(0, 2)==
"bv")
628 std::string v=value.substr(2, value.find(
'[')-2);
629 size_t p = value.find(
'[')+1;
630 std::string w=value.substr(p, value.find(
']')-p);
639 else if(value==
"false")
641 else if(value==
"true")
643 else if(value.substr(0, 8)==
"array_of")
648 while(fit!=
array_of_map.end() && fit->second!=id) fit++;
651 it->second.value = fit->first;
660 std::string value=values[
"B"+std::to_string(v)];
The type of an expression.
resultt read_result_opensmt(std::istream &in)
const mp_integer string2integer(const std::string &n, unsigned base)
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
index_value_mapt index_value_map
Unbounded, signed rational numbers.
void set_value(identifiert &identifier, const std::string &index, const std::string &value)
A constant literal expression.
static mstreamt & eom(mstreamt &m)
identifier_mapt identifier_map
const irep_idt & id() const
std::string temp_out_filename
void set_value(const irep_idt &value)
virtual resultt dec_solve()
The boolean constant true.
resultt read_result_mathsat(std::istream &in)
typet array_index_type() const
API to expression classes.
unsigned no_boolean_variables
array constructor from single element
std::vector< bool > boolean_assignment
virtual std::string decision_procedure_text() const
resultt read_result_z3(std::istream &in)
resultt read_result_cvc3(std::istream &in)
resultt read_result_boolector(std::istream &in)
read model produced by Boolector
The boolean constant false.
bool has_prefix(const std::string &s, const std::string &prefix)
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
array_of_mapt array_of_map
unsigned integer2unsigned(const mp_integer &n)
unsigned safe_string2unsigned(const std::string &str, int base)
resultt read_result_yices(std::istream &in)
std::string get_temporary_file(const std::string &prefix, const std::string &suffix)
Substitute for mkstemps (OpenBSD standard) for Windows, where it is unavailable.
Base class for all expressions.
Operator to update elements in structs and arrays.
const std::string integer2binary(const mp_integer &n, std::size_t width)
exprt binary2struct(const struct_typet &type, const std::string &binary) const
bool string_to_expr_z3(const typet &type, const std::string &value, exprt &e) const
const typet & subtype() const
exprt binary2union(const union_typet &type, const std::string &binary) const
std::string temp_result_filename
bool dec_solve_was_called
std::string mathsat_value(const std::string &src)
std::string convert_identifier(const irep_idt &identifier)