43 temp_file_stdout(
"smt2_dec_stdout_",
""),
44 temp_file_stderr(
"smt2_dec_stderr_",
"");
46 const auto write_problem_to_file = [&](std::ofstream problem_out) {
62 write_problem_to_file(std::ofstream(
63 temp_file_problem(), std::ios_base::out | std::ios_base::trunc));
65 std::vector<std::string> argv;
66 std::string stdin_filename;
71 argv = {
"bitwuzla", temp_file_problem()};
75 argv = {
"boolector",
"--smt2", temp_file_problem(),
"-m"};
79 argv = {
"smt2_solver"};
80 stdin_filename = temp_file_problem();
96 argv = {
"cvc4",
"-L",
"smt2", temp_file_problem()};
100 argv = {
"cvc5",
"--lang",
"smtlib", temp_file_problem()};
109 "-preprocessor.toplevel_propagation=true",
110 "-preprocessor.simplification=7",
111 "-dpll.branching_random_frequency=0.01",
112 "-dpll.branching_random_invalidate_phase_cache=true",
113 "-dpll.restart_strategy=3",
114 "-dpll.glucose_var_activity=true",
115 "-dpll.glucose_learnt_minimization=true",
116 "-theory.bv.eager=true",
117 "-theory.bv.bit_blast_mode=1",
118 "-theory.bv.delay_propagated_eqs=true",
120 "-theory.fp.bit_blast_mode=2",
121 "-theory.arr.mode=1"};
123 stdin_filename = temp_file_problem();
129 argv = {
"yices-smt2", temp_file_problem()};
133 argv = {
"z3",
"-smt2", temp_file_problem()};
141 run(argv[0], argv, stdin_filename, temp_file_stdout(), temp_file_stderr());
150 std::ifstream in(temp_file_stdout());
156 if(src.size() >= 2 && src.front() ==
'|' && src.back() ==
'|')
157 return std::string(src, 1, src.size() - 2);
170 typedef std::unordered_map<irep_idt, irept> valuest;
171 valuest parsed_values;
177 if(!parsed_opt.has_value())
180 const auto &parsed = parsed_opt.value();
182 if(parsed.id()==
"sat")
184 else if(parsed.id()==
"unsat")
186 else if(parsed.id() ==
"unknown")
193 parsed.id().empty() && parsed.get_sub().size() == 1 &&
194 parsed.get_sub().front().get_sub().size() == 2)
197 const irept &
s1=parsed.get_sub().front().get_sub()[1];
205 parsed_values[s0.
id()] =
s1;
208 parsed.id().empty() && parsed.get_sub().size() == 2 &&
209 parsed.get_sub().front().id() ==
"error")
215 const auto &message =
id2string(parsed.get_sub()[1].id());
217 log.
error() <<
"SMT2 solver returned error message:\n"
232 const irept &value = parsed_values[conv_id];
233 assignment.second.value =
parse_rec(value, assignment.second.type);
239 const std::string boolean_identifier =
241 const auto found_parsed_value =
242 parsed_values.find(
drop_quotes(boolean_identifier));
243 if(found_parsed_value != parsed_values.end())
245 const irept &value = found_parsed_value->second;
247 if(value.
id() != ID_true && value.
id() != ID_false)
250 log.
error() <<
"SMT2 solver returned non-constant value for variable "
259 const auto found_set_value =
set_values.find(boolean_identifier);
267 const irept &value = parsed_values[boolean_identifier];
269 if(value.
id() != ID_true && value.
id() != ID_false)
273 <<
"SMT2 solver returned non-Boolean value for variable "
resultt
Result of running the decision procedure.
Base class for all expressions.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
const irep_idt & id() const
Class that provides messages with a built-in verbosity 'level'.
std::size_t number_of_solver_calls
void write_footer()
Writes the end of the SMT file to the smt_convt::out stream.
static std::string convert_identifier(const irep_idt &identifier)
std::unordered_map< irep_idt, bool > set_values
The values which boolean identifiers have been smt2_convt::set_to or in other words those which are a...
exprt parse_rec(const irept &s, const typet &type)
std::vector< bool > boolean_assignment
std::vector< literalt > assumptions
identifier_mapt identifier_map
std::size_t no_boolean_variables
literalt convert(const exprt &expr)
message_handlert & message_handler
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
resultt dec_solve(const exprt &) override
Implementation of the decision procedure.
resultt read_result(std::istream &in)
std::stringstream cached_output
Everything except the footer is cached, so that output files can be rewritten with varying footers.
std::stringstream stringstream
const std::string & id2string(const irep_idt &d)
int run(const std::string &what, const std::vector< std::string > &argv)
static std::string drop_quotes(std::string src)
std::optional< irept > smt2irep(std::istream &in, message_handlert &message_handler)
returns an irep for an SMT-LIB2 expression read from a given stream returns {} when EOF is encountere...
#define UNREACHABLE
This should be used to mark dead code.