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/run.h>
15 #include <util/std_expr.h>
16 #include <util/std_types.h>
17 #include <util/tempfile.h>
18 
19 #include "smt2irep.h"
20 
22 {
23  // clang-format off
24  return "SMT2 " + logic + (use_FPA_theory ? " (with FPA)" : "") + " using " +
25  (solver==solvert::GENERIC?"Generic":
26  solver==solvert::BOOLECTOR?"Boolector":
27  solver==solvert::CPROVER_SMT2?"CPROVER SMT2":
28  solver==solvert::CVC3?"CVC3":
29  solver==solvert::CVC4?"CVC4":
30  solver==solvert::MATHSAT?"MathSAT":
31  solver==solvert::YICES?"Yices":
32  solver==solvert::Z3?"Z3":
33  "(unknown)");
34  // clang-format on
35 }
36 
38 {
40 
41  temporary_filet temp_file_problem("smt2_dec_problem_", ""),
42  temp_file_stdout("smt2_dec_stdout_", ""),
43  temp_file_stderr("smt2_dec_stderr_", "");
44 
45  {
46  // we write the problem into a file
47  std::ofstream problem_out(
48  temp_file_problem(), std::ios_base::out | std::ios_base::trunc);
49  problem_out << stringstream.str();
50  write_footer(problem_out);
51  }
52 
53  std::vector<std::string> argv;
54  std::string stdin_filename;
55 
56  switch(solver)
57  {
58  case solvert::BOOLECTOR:
59  argv = {"boolector", "--smt2", temp_file_problem(), "-m"};
60  break;
61 
63  argv = {"smt2_solver"};
64  stdin_filename = temp_file_problem();
65  break;
66 
67  case solvert::CVC3:
68  argv = {"cvc3",
69  "+model",
70  "-lang",
71  "smtlib",
72  "-output-lang",
73  "smtlib",
74  temp_file_problem()};
75  break;
76 
77  case solvert::CVC4:
78  // The flags --bitblast=eager --bv-div-zero-const help but only
79  // work for pure bit-vector formulas.
80  argv = {"cvc4", "-L", "smt2", temp_file_problem()};
81  break;
82 
83  case solvert::MATHSAT:
84  // The options below were recommended by Alberto Griggio
85  // on 10 July 2013
86 
87  argv = {"mathsat",
88  "-input=smt2",
89  "-preprocessor.toplevel_propagation=true",
90  "-preprocessor.simplification=7",
91  "-dpll.branching_random_frequency=0.01",
92  "-dpll.branching_random_invalidate_phase_cache=true",
93  "-dpll.restart_strategy=3",
94  "-dpll.glucose_var_activity=true",
95  "-dpll.glucose_learnt_minimization=true",
96  "-theory.bv.eager=true",
97  "-theory.bv.bit_blast_mode=1",
98  "-theory.bv.delay_propagated_eqs=true",
99  "-theory.fp.mode=1",
100  "-theory.fp.bit_blast_mode=2",
101  "-theory.arr.mode=1"};
102 
103  stdin_filename = temp_file_problem();
104  break;
105 
106  case solvert::YICES:
107  // command = "yices -smt -e " // Calling convention for older versions
108  // Convention for 2.2.1
109  argv = {"yices-smt2", temp_file_problem()};
110  break;
111 
112  case solvert::Z3:
113  argv = {"z3", "-smt2", temp_file_problem()};
114  break;
115 
116  case solvert::GENERIC:
117  UNREACHABLE;
118  }
119 
120  int res =
121  run(argv[0], argv, stdin_filename, temp_file_stdout(), temp_file_stderr());
122 
123  if(res<0)
124  {
125  error() << "error running SMT2 solver" << 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 values;
143 
144  while(in)
145  {
146  auto parsed_opt = smt2irep(in, get_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(
158  parsed.id().empty() && parsed.get_sub().size() == 1 &&
159  parsed.get_sub().front().get_sub().size() == 2)
160  {
161  const irept &s0=parsed.get_sub().front().get_sub()[0];
162  const irept &s1=parsed.get_sub().front().get_sub()[1];
163 
164  // Examples:
165  // ( (B0 true) )
166  // ( (|__CPROVER_pipe_count#1| (_ bv0 32)) )
167  // ( (|some_integer| 0) )
168  // ( (|some_integer| (- 10)) )
169 
170  values[s0.id()]=s1;
171  }
172  else if(
173  parsed.id().empty() && parsed.get_sub().size() == 2 &&
174  parsed.get_sub().front().id() == "error")
175  {
176  // We ignore errors after UNSAT because get-value after check-sat
177  // returns unsat will give an error.
178  if(res!=resultt::D_UNSATISFIABLE)
179  {
180  error() << "SMT2 solver returned error message:\n"
181  << "\t\"" << parsed.get_sub()[1].id() <<"\"" << eom;
183  }
184  }
185  }
186 
187  for(auto &assignment : identifier_map)
188  {
189  std::string conv_id=convert_identifier(assignment.first);
190  const irept &value=values[conv_id];
191  assignment.second.value=parse_rec(value, assignment.second.type);
192  }
193 
194  // Booleans
195  for(unsigned v=0; v<no_boolean_variables; v++)
196  {
197  const irept &value=values["B"+std::to_string(v)];
198  boolean_assignment[v]=(value.id()==ID_true);
199  }
200 
201  return res;
202 }
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:85
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:37
decision_proceduret::resultt::D_SATISFIABLE
@ D_SATISFIABLE
smt2_convt::number_of_solver_calls
std::size_t number_of_solver_calls
Definition: smt2_conv.h:90
smt2_convt::convert_identifier
std::string convert_identifier(const irep_idt &identifier)
Definition: smt2_conv.cpp:776
messaget::error
mstreamt & error() const
Definition: message.h:399
smt2_convt::solvert::YICES
@ YICES
smt2_convt::identifier_map
identifier_mapt identifier_map
Definition: smt2_conv.h:207
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:418
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:133
smt2_dect::decision_procedure_text
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
Definition: smt2_dec.cpp:21
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
smt2_convt::use_FPA_theory
bool use_FPA_theory
Definition: smt2_conv.h:59
smt2_convt::logic
std::string logic
Definition: smt2_conv.h:84
smt2_convt::write_footer
void write_footer(std::ostream &)
Definition: smt2_conv.cpp:163
smt2_convt::parse_rec
exprt parse_rec(const irept &s, const typet &type)
Definition: smt2_conv.cpp:542
ieee_float.h
smt2_convt::no_boolean_variables
std::size_t no_boolean_variables
Definition: smt2_conv.h:229
irept::get_sub
subt & get_sub()
Definition: irep.h:477
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:394
smt2_convt::boolean_assignment
std::vector< bool > boolean_assignment
Definition: smt2_conv.h:230
smt2irep.h
std_expr.h
API to expression classes.
temporary_filet
Definition: tempfile.h:24