cprover
Loading...
Searching...
No Matches
smt2_dec.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "smt2_dec.h"
10
11#include <util/invariant.h>
12#include <util/message.h>
13#include <util/run.h>
14#include <util/tempfile.h>
15
16#include "smt2irep.h"
17
19{
20 // clang-format off
21 return "SMT2 " + logic + (use_FPA_theory ? " (with FPA)" : "") + " using " +
22 (solver==solvert::GENERIC?"Generic":
23 solver==solvert::BOOLECTOR?"Boolector":
24 solver==solvert::CPROVER_SMT2?"CPROVER SMT2":
25 solver==solvert::CVC3?"CVC3":
26 solver==solvert::CVC4?"CVC4":
27 solver==solvert::MATHSAT?"MathSAT":
28 solver==solvert::YICES?"Yices":
29 solver==solvert::Z3?"Z3":
30 "(unknown)");
31 // clang-format on
32}
33
35{
37
38 temporary_filet temp_file_problem("smt2_dec_problem_", ""),
39 temp_file_stdout("smt2_dec_stdout_", ""),
40 temp_file_stderr("smt2_dec_stderr_", "");
41
42 const auto write_problem_to_file = [&](std::ofstream problem_out) {
44 stringstream.str(std::string{});
46 problem_out << cached_output.str() << stringstream.str();
47 stringstream.str(std::string{});
48 };
49 write_problem_to_file(std::ofstream(
50 temp_file_problem(), std::ios_base::out | std::ios_base::trunc));
51
52 std::vector<std::string> argv;
53 std::string stdin_filename;
54
55 switch(solver)
56 {
58 argv = {"boolector", "--smt2", temp_file_problem(), "-m"};
59 break;
60
62 argv = {"smt2_solver"};
63 stdin_filename = temp_file_problem();
64 break;
65
66 case solvert::CVC3:
67 argv = {"cvc3",
68 "+model",
69 "-lang",
70 "smtlib",
71 "-output-lang",
72 "smtlib",
73 temp_file_problem()};
74 break;
75
76 case solvert::CVC4:
77 // The flags --bitblast=eager --bv-div-zero-const help but only
78 // work for pure bit-vector formulas.
79 argv = {"cvc4", "-L", "smt2", temp_file_problem()};
80 break;
81
83 // The options below were recommended by Alberto Griggio
84 // on 10 July 2013
85
86 argv = {"mathsat",
87 "-input=smt2",
88 "-preprocessor.toplevel_propagation=true",
89 "-preprocessor.simplification=7",
90 "-dpll.branching_random_frequency=0.01",
91 "-dpll.branching_random_invalidate_phase_cache=true",
92 "-dpll.restart_strategy=3",
93 "-dpll.glucose_var_activity=true",
94 "-dpll.glucose_learnt_minimization=true",
95 "-theory.bv.eager=true",
96 "-theory.bv.bit_blast_mode=1",
97 "-theory.bv.delay_propagated_eqs=true",
98 "-theory.fp.mode=1",
99 "-theory.fp.bit_blast_mode=2",
100 "-theory.arr.mode=1"};
101
102 stdin_filename = temp_file_problem();
103 break;
104
105 case solvert::YICES:
106 // command = "yices -smt -e " // Calling convention for older versions
107 // Convention for 2.2.1
108 argv = {"yices-smt2", temp_file_problem()};
109 break;
110
111 case solvert::Z3:
112 argv = {"z3", "-smt2", temp_file_problem()};
113 break;
114
115 case solvert::GENERIC:
117 }
118
119 int res =
120 run(argv[0], argv, stdin_filename, temp_file_stdout(), temp_file_stderr());
121
122 if(res<0)
123 {
125 log.error() << "error running SMT2 solver" << messaget::eom;
127 }
128
129 std::ifstream in(temp_file_stdout());
130 return read_result(in);
131}
132
134{
135 std::string line;
137
138 boolean_assignment.clear();
140
141 typedef std::unordered_map<irep_idt, irept> valuest;
142 valuest parsed_values;
143
144 while(in)
145 {
146 auto parsed_opt = smt2irep(in, message_handler);
147
148 if(!parsed_opt.has_value())
149 break;
150
151 const auto &parsed = parsed_opt.value();
152
153 if(parsed.id()=="sat")
155 else if(parsed.id()=="unsat")
157 else if(parsed.id() == "unknown")
158 {
160 log.error() << "SMT2 solver returned \"unknown\"" << messaget::eom;
162 }
163 else if(
164 parsed.id().empty() && parsed.get_sub().size() == 1 &&
165 parsed.get_sub().front().get_sub().size() == 2)
166 {
167 const irept &s0=parsed.get_sub().front().get_sub()[0];
168 const irept &s1=parsed.get_sub().front().get_sub()[1];
169
170 // Examples:
171 // ( (B0 true) )
172 // ( (|__CPROVER_pipe_count#1| (_ bv0 32)) )
173 // ( (|some_integer| 0) )
174 // ( (|some_integer| (- 10)) )
175
176 parsed_values[s0.id()] = s1;
177 }
178 else if(
179 parsed.id().empty() && parsed.get_sub().size() == 2 &&
180 parsed.get_sub().front().id() == "error")
181 {
182 // We ignore errors after UNSAT because get-value after check-sat
183 // returns unsat will give an error.
184 if(res != resultt::D_UNSATISFIABLE)
185 {
186 const auto &message = id2string(parsed.get_sub()[1].id());
187 // Special case error handling
188 if(
189 solver == solvert::Z3 &&
190 message.find("must not contain quantifiers") != std::string::npos)
191 {
192 // We tried to "(get-value |XXXX|)" where |XXXX| is determined to
193 // include a quantified expression
194 // Nothing to do, this should be caught and value assigned by the
195 // set_to defaults later.
196 }
197 // Unhandled error, log the error and report it back up to caller
198 else
199 {
201 log.error() << "SMT2 solver returned error message:\n"
202 << "\t\"" << message << "\"" << messaget::eom;
204 }
205 }
206 }
207 }
208
209 // If the result is not satisfiable don't bother updating the assignments and
210 // values (since we didn't get any), just return.
211 if(res != resultt::D_SATISFIABLE)
212 return res;
213
214 for(auto &assignment : identifier_map)
215 {
216 std::string conv_id = convert_identifier(assignment.first);
217 const irept &value = parsed_values[conv_id];
218 assignment.second.value = parse_rec(value, assignment.second.type);
219 }
220
221 // Booleans
222 for(unsigned v=0; v<no_boolean_variables; v++)
223 {
224 const std::string boolean_identifier = "B" + std::to_string(v);
225 boolean_assignment[v] = [&]() {
226 const auto found_parsed_value = parsed_values.find(boolean_identifier);
227 if(found_parsed_value != parsed_values.end())
228 return found_parsed_value->second.id() == ID_true;
229 // Work out the value based on what set_to was called with.
230 const auto found_set_value =
231 set_values.find('|' + boolean_identifier + '|');
232 if(found_set_value != set_values.end())
233 return found_set_value->second;
234 // Old code used the computation
235 // const irept &value=values["B"+std::to_string(v)];
236 // boolean_assignment[v]=(value.id()==ID_true);
237 return parsed_values[boolean_identifier].id() == ID_true;
238 }();
239 }
240
241 return res;
242}
int8_t s1
Definition: bytecode_info.h:59
resultt
Result of running the decision procedure.
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:372
subt & get_sub()
Definition: irep.h:456
const irep_idt & id() const
Definition: irep.h:396
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
static eomt eom
Definition: message.h:297
std::size_t number_of_solver_calls
Definition: smt2_conv.h:96
void write_footer()
Writes the end of the SMT file to the smt_convt::out stream.
Definition: smt2_conv.cpp:185
bool use_FPA_theory
Definition: smt2_conv.h:60
std::string logic
Definition: smt2_conv.h:90
static std::string convert_identifier(const irep_idt &identifier)
Definition: smt2_conv.cpp:880
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...
Definition: smt2_conv.h:257
exprt parse_rec(const irept &s, const typet &type)
Definition: smt2_conv.cpp:638
std::vector< bool > boolean_assignment
Definition: smt2_conv.h:266
solvert solver
Definition: smt2_conv.h:91
identifier_mapt identifier_map
Definition: smt2_conv.h:237
std::size_t no_boolean_variables
Definition: smt2_conv.h:265
message_handlert & message_handler
Definition: smt2_dec.h:46
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
Definition: smt2_dec.cpp:18
resultt dec_solve() override
Run the decision procedure to solve the problem.
Definition: smt2_dec.cpp:34
resultt read_result(std::istream &in)
Definition: smt2_dec.cpp:133
std::stringstream cached_output
Everything except the footer is cached, so that output files can be rewritten with varying footers.
Definition: smt2_dec.h:50
std::stringstream stringstream
Definition: smt2_dec.h:22
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
int run(const std::string &what, const std::vector< std::string > &argv)
Definition: run.cpp:48
optionalt< 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...
Definition: smt2irep.cpp:91
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503