cprover
smt2_dec.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "smt2_dec.h"
10 
11 #include <util/arith_tools.h>
12 #include <util/ieee_float.h>
13 #include <util/invariant.h>
14 #include <util/message.h>
15 #include <util/run.h>
16 #include <util/std_expr.h>
17 #include <util/std_types.h>
18 #include <util/tempfile.h>
19 
20 #include "smt2irep.h"
21 
23 {
24  // clang-format off
25  return "SMT2 " + logic + (use_FPA_theory ? " (with FPA)" : "") + " using " +
26  (solver==solvert::GENERIC?"Generic":
27  solver==solvert::BOOLECTOR?"Boolector":
28  solver==solvert::CPROVER_SMT2?"CPROVER SMT2":
29  solver==solvert::CVC3?"CVC3":
30  solver==solvert::CVC4?"CVC4":
31  solver==solvert::MATHSAT?"MathSAT":
32  solver==solvert::YICES?"Yices":
33  solver==solvert::Z3?"Z3":
34  "(unknown)");
35  // clang-format on
36 }
37 
39 {
41 
42  temporary_filet temp_file_problem("smt2_dec_problem_", ""),
43  temp_file_stdout("smt2_dec_stdout_", ""),
44  temp_file_stderr("smt2_dec_stderr_", "");
45 
46  {
47  // we write the problem into a file
48  std::ofstream problem_out(
49  temp_file_problem(), std::ios_base::out | std::ios_base::trunc);
50  problem_out << stringstream.str();
51  write_footer(problem_out);
52  }
53 
54  std::vector<std::string> argv;
55  std::string stdin_filename;
56 
57  switch(solver)
58  {
59  case solvert::BOOLECTOR:
60  argv = {"boolector", "--smt2", temp_file_problem(), "-m"};
61  break;
62 
64  argv = {"smt2_solver"};
65  stdin_filename = temp_file_problem();
66  break;
67 
68  case solvert::CVC3:
69  argv = {"cvc3",
70  "+model",
71  "-lang",
72  "smtlib",
73  "-output-lang",
74  "smtlib",
75  temp_file_problem()};
76  break;
77 
78  case solvert::CVC4:
79  // The flags --bitblast=eager --bv-div-zero-const help but only
80  // work for pure bit-vector formulas.
81  argv = {"cvc4", "-L", "smt2", temp_file_problem()};
82  break;
83 
84  case solvert::MATHSAT:
85  // The options below were recommended by Alberto Griggio
86  // on 10 July 2013
87 
88  argv = {"mathsat",
89  "-input=smt2",
90  "-preprocessor.toplevel_propagation=true",
91  "-preprocessor.simplification=7",
92  "-dpll.branching_random_frequency=0.01",
93  "-dpll.branching_random_invalidate_phase_cache=true",
94  "-dpll.restart_strategy=3",
95  "-dpll.glucose_var_activity=true",
96  "-dpll.glucose_learnt_minimization=true",
97  "-theory.bv.eager=true",
98  "-theory.bv.bit_blast_mode=1",
99  "-theory.bv.delay_propagated_eqs=true",
100  "-theory.fp.mode=1",
101  "-theory.fp.bit_blast_mode=2",
102  "-theory.arr.mode=1"};
103 
104  stdin_filename = temp_file_problem();
105  break;
106 
107  case solvert::YICES:
108  // command = "yices -smt -e " // Calling convention for older versions
109  // Convention for 2.2.1
110  argv = {"yices-smt2", temp_file_problem()};
111  break;
112 
113  case solvert::Z3:
114  argv = {"z3", "-smt2", temp_file_problem()};
115  break;
116 
117  case solvert::GENERIC:
118  UNREACHABLE;
119  }
120 
121  int res =
122  run(argv[0], argv, stdin_filename, temp_file_stdout(), temp_file_stderr());
123 
124  if(res<0)
125  {
127  log.error() << "error running SMT2 solver" << messaget::eom;
129  }
130 
131  std::ifstream in(temp_file_stdout());
132  return read_result(in);
133 }
134 
136 {
137  std::string line;
139 
140  boolean_assignment.clear();
142 
143  typedef std::unordered_map<irep_idt, irept> valuest;
144  valuest values;
145 
146  while(in)
147  {
148  auto parsed_opt = smt2irep(in, message_handler);
149 
150  if(!parsed_opt.has_value())
151  break;
152 
153  const auto &parsed = parsed_opt.value();
154 
155  if(parsed.id()=="sat")
157  else if(parsed.id()=="unsat")
159  else if(
160  parsed.id().empty() && parsed.get_sub().size() == 1 &&
161  parsed.get_sub().front().get_sub().size() == 2)
162  {
163  const irept &s0=parsed.get_sub().front().get_sub()[0];
164  const irept &s1=parsed.get_sub().front().get_sub()[1];
165 
166  // Examples:
167  // ( (B0 true) )
168  // ( (|__CPROVER_pipe_count#1| (_ bv0 32)) )
169  // ( (|some_integer| 0) )
170  // ( (|some_integer| (- 10)) )
171 
172  values[s0.id()]=s1;
173  }
174  else if(
175  parsed.id().empty() && parsed.get_sub().size() == 2 &&
176  parsed.get_sub().front().id() == "error")
177  {
178  // We ignore errors after UNSAT because get-value after check-sat
179  // returns unsat will give an error.
180  if(res!=resultt::D_UNSATISFIABLE)
181  {
183  log.error() << "SMT2 solver returned error message:\n"
184  << "\t\"" << parsed.get_sub()[1].id() << "\""
185  << messaget::eom;
187  }
188  }
189  }
190 
191  for(auto &assignment : identifier_map)
192  {
193  std::string conv_id=convert_identifier(assignment.first);
194  const irept &value=values[conv_id];
195  assignment.second.value=parse_rec(value, assignment.second.type);
196  }
197 
198  // Booleans
199  for(unsigned v=0; v<no_boolean_variables; v++)
200  {
201  const irept &value=values["B"+std::to_string(v)];
202  boolean_assignment[v]=(value.id()==ID_true);
203  }
204 
205  return res;
206 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
smt2_convt::solvert::CVC4
@ CVC4
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
smt2_convt::solver
solvert solver
Definition: smt2_conv.h:90
tempfile.h
smt2_convt::solvert::CPROVER_SMT2
@ CPROVER_SMT2
arith_tools.h
decision_proceduret::resultt::D_UNSATISFIABLE
@ D_UNSATISFIABLE
invariant.h
smt2_convt::solvert::MATHSAT
@ MATHSAT
s1
int8_t s1
Definition: bytecode_info.h:59
run
int run(const std::string &what, const std::vector< std::string > &argv)
Definition: run.cpp:49
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
messaget::eom
static eomt eom
Definition: message.h:297
run.h
smt2_convt::solvert::CVC3
@ CVC3
smt2_stringstreamt::stringstream
std::stringstream stringstream
Definition: smt2_dec.h:22
smt2_convt::solvert::BOOLECTOR
@ BOOLECTOR
smt2_dect::dec_solve
resultt dec_solve() override
Run the decision procedure to solve the problem.
Definition: smt2_dec.cpp:38
decision_proceduret::resultt::D_SATISFIABLE
@ D_SATISFIABLE
smt2_convt::number_of_solver_calls
std::size_t number_of_solver_calls
Definition: smt2_conv.h:95
smt2_convt::convert_identifier
std::string convert_identifier(const irep_idt &identifier)
Definition: smt2_conv.cpp:798
smt2_convt::solvert::YICES
@ YICES
smt2_convt::identifier_map
identifier_mapt identifier_map
Definition: smt2_conv.h:212
std_types.h
Pre-defined types.
smt2_dec.h
decision_proceduret::resultt::D_ERROR
@ D_ERROR
irept::id
const irep_idt & id() const
Definition: irep.h:407
decision_proceduret::resultt
resultt
Result of running the decision procedure.
Definition: decision_procedure.h:44
smt2_dect::read_result
resultt read_result(std::istream &in)
Definition: smt2_dec.cpp:135
smt2_dect::message_handler
message_handlert & message_handler
Definition: smt2_dec.h:46
smt2_dect::decision_procedure_text
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
Definition: smt2_dec.cpp:22
smt2_convt::use_FPA_theory
bool use_FPA_theory
Definition: smt2_conv.h:61
smt2_convt::logic
std::string logic
Definition: smt2_conv.h:89
smt2_convt::write_footer
void write_footer(std::ostream &)
Definition: smt2_conv.cpp:175
smt2_convt::parse_rec
exprt parse_rec(const irept &s, const typet &type)
Definition: smt2_conv.cpp:564
ieee_float.h
smt2_convt::no_boolean_variables
std::size_t no_boolean_variables
Definition: smt2_conv.h:236
irept::get_sub
subt & get_sub()
Definition: irep.h:467
smt2_convt::solvert::GENERIC
@ GENERIC
smt2irep
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
smt2_convt::solvert::Z3
@ Z3
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
smt2_convt::boolean_assignment
std::vector< bool > boolean_assignment
Definition: smt2_conv.h:237
message.h
smt2irep.h
std_expr.h
API to expression classes.
temporary_filet
Definition: tempfile.h:24