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::BITWUZLA?"Bitwuzla":
24 solver==solvert::BOOLECTOR?"Boolector":
25 solver==solvert::CPROVER_SMT2?"CPROVER SMT2":
26 solver==solvert::CVC3?"CVC3":
27 solver==solvert::CVC4?"CVC4":
28 solver==solvert::CVC5?"CVC5":
29 solver==solvert::MATHSAT?"MathSAT":
30 solver==solvert::YICES?"Yices":
31 solver==solvert::Z3?"Z3":
32 "(unknown)");
33 // clang-format on
34}
35
37{
39
40 temporary_filet temp_file_problem("smt2_dec_problem_", ""),
41 temp_file_stdout("smt2_dec_stdout_", ""),
42 temp_file_stderr("smt2_dec_stderr_", "");
43
44 const auto write_problem_to_file = [&](std::ofstream problem_out) {
46 stringstream.str(std::string{});
48 problem_out << cached_output.str() << stringstream.str();
49 stringstream.str(std::string{});
50 };
51 write_problem_to_file(std::ofstream(
52 temp_file_problem(), std::ios_base::out | std::ios_base::trunc));
53
54 std::vector<std::string> argv;
55 std::string stdin_filename;
56
57 switch(solver)
58 {
60 argv = {"bitwuzla", temp_file_problem()};
61 break;
62
64 argv = {"boolector", "--smt2", temp_file_problem(), "-m"};
65 break;
66
68 argv = {"smt2_solver"};
69 stdin_filename = temp_file_problem();
70 break;
71
72 case solvert::CVC3:
73 argv = {"cvc3",
74 "+model",
75 "-lang",
76 "smtlib",
77 "-output-lang",
78 "smtlib",
79 temp_file_problem()};
80 break;
81
82 case solvert::CVC4:
83 // The flags --bitblast=eager --bv-div-zero-const help but only
84 // work for pure bit-vector formulas.
85 argv = {"cvc4", "-L", "smt2", temp_file_problem()};
86 break;
87
88 case solvert::CVC5:
89 argv = {"cvc5", "--lang", "smtlib", temp_file_problem()};
90 break;
91
93 // The options below were recommended by Alberto Griggio
94 // on 10 July 2013
95
96 argv = {"mathsat",
97 "-input=smt2",
98 "-preprocessor.toplevel_propagation=true",
99 "-preprocessor.simplification=7",
100 "-dpll.branching_random_frequency=0.01",
101 "-dpll.branching_random_invalidate_phase_cache=true",
102 "-dpll.restart_strategy=3",
103 "-dpll.glucose_var_activity=true",
104 "-dpll.glucose_learnt_minimization=true",
105 "-theory.bv.eager=true",
106 "-theory.bv.bit_blast_mode=1",
107 "-theory.bv.delay_propagated_eqs=true",
108 "-theory.fp.mode=1",
109 "-theory.fp.bit_blast_mode=2",
110 "-theory.arr.mode=1"};
111
112 stdin_filename = temp_file_problem();
113 break;
114
115 case solvert::YICES:
116 // command = "yices -smt -e " // Calling convention for older versions
117 // Convention for 2.2.1
118 argv = {"yices-smt2", temp_file_problem()};
119 break;
120
121 case solvert::Z3:
122 argv = {"z3", "-smt2", temp_file_problem()};
123 break;
124
125 case solvert::GENERIC:
127 }
128
129 int res =
130 run(argv[0], argv, stdin_filename, temp_file_stdout(), temp_file_stderr());
131
132 if(res<0)
133 {
135 log.error() << "error running SMT2 solver" << messaget::eom;
137 }
138
139 std::ifstream in(temp_file_stdout());
140 return read_result(in);
141}
142
143static std::string drop_quotes(std::string src)
144{
145 if(src.size() >= 2 && src.front() == '|' && src.back() == '|')
146 return std::string(src, 1, src.size() - 2);
147 else
148 return src;
149}
150
152{
153 std::string line;
155
156 boolean_assignment.clear();
158
159 typedef std::unordered_map<irep_idt, irept> valuest;
160 valuest parsed_values;
161
162 while(in)
163 {
164 auto parsed_opt = smt2irep(in, message_handler);
165
166 if(!parsed_opt.has_value())
167 break;
168
169 const auto &parsed = parsed_opt.value();
170
171 if(parsed.id()=="sat")
173 else if(parsed.id()=="unsat")
175 else if(parsed.id() == "unknown")
176 {
178 log.error() << "SMT2 solver returned \"unknown\"" << messaget::eom;
180 }
181 else if(
182 parsed.id().empty() && parsed.get_sub().size() == 1 &&
183 parsed.get_sub().front().get_sub().size() == 2)
184 {
185 const irept &s0=parsed.get_sub().front().get_sub()[0];
186 const irept &s1=parsed.get_sub().front().get_sub()[1];
187
188 // Examples:
189 // ( (B0 true) )
190 // ( (|__CPROVER_pipe_count#1| (_ bv0 32)) )
191 // ( (|some_integer| 0) )
192 // ( (|some_integer| (- 10)) )
193
194 parsed_values[s0.id()] = s1;
195 }
196 else if(
197 parsed.id().empty() && parsed.get_sub().size() == 2 &&
198 parsed.get_sub().front().id() == "error")
199 {
200 // We ignore errors after UNSAT because get-value after check-sat
201 // returns unsat will give an error.
202 if(res != resultt::D_UNSATISFIABLE)
203 {
204 const auto &message = id2string(parsed.get_sub()[1].id());
206 log.error() << "SMT2 solver returned error message:\n"
207 << "\t\"" << message << "\"" << messaget::eom;
209 }
210 }
211 }
212
213 // If the result is not satisfiable don't bother updating the assignments and
214 // values (since we didn't get any), just return.
215 if(res != resultt::D_SATISFIABLE)
216 return res;
217
218 for(auto &assignment : identifier_map)
219 {
220 std::string conv_id = drop_quotes(convert_identifier(assignment.first));
221 const irept &value = parsed_values[conv_id];
222 assignment.second.value = parse_rec(value, assignment.second.type);
223 }
224
225 // Booleans
226 for(unsigned v=0; v<no_boolean_variables; v++)
227 {
228 const std::string boolean_identifier =
229 convert_identifier("B" + std::to_string(v));
230 boolean_assignment[v] = [&]() {
231 const auto found_parsed_value =
232 parsed_values.find(drop_quotes(boolean_identifier));
233 if(found_parsed_value != parsed_values.end())
234 {
235 return found_parsed_value->second.id() == ID_true;
236 }
237 // Work out the value based on what set_to was called with.
238 const auto found_set_value = set_values.find(boolean_identifier);
239 if(found_set_value != set_values.end())
240 return found_set_value->second;
241 // Old code used the computation
242 // const irept &value=values["B"+std::to_string(v)];
243 // boolean_assignment[v]=(value.id()==ID_true);
244 return parsed_values[boolean_identifier].id() == ID_true;
245 }();
246 }
247
248 return res;
249}
int8_t s1
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:107
void write_footer()
Writes the end of the SMT file to the smt_convt::out stream.
bool use_FPA_theory
Definition smt2_conv.h:63
std::string logic
Definition smt2_conv.h:98
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...
Definition smt2_conv.h:274
exprt parse_rec(const irept &s, const typet &type)
std::vector< bool > boolean_assignment
Definition smt2_conv.h:283
solvert solver
Definition smt2_conv.h:99
identifier_mapt identifier_map
Definition smt2_conv.h:254
std::size_t no_boolean_variables
Definition smt2_conv.h:282
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:36
resultt read_result(std::istream &in)
Definition smt2_dec.cpp:151
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
static std::string drop_quotes(std::string src)
Definition smt2_dec.cpp:143
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:525