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 {
39  temporary_filet temp_file_problem("smt2_dec_problem_", ""),
40  temp_file_stdout("smt2_dec_stdout_", ""),
41  temp_file_stderr("smt2_dec_stderr_", "");
42 
43  {
44  // we write the problem into a file
45  std::ofstream problem_out(
46  temp_file_problem(), std::ios_base::out | std::ios_base::trunc);
47  problem_out << stringstream.str();
48  write_footer(problem_out);
49  }
50 
51  std::vector<std::string> argv;
52  std::string stdin_filename;
53 
54  switch(solver)
55  {
56  case solvert::BOOLECTOR:
57  argv = {"boolector", "--smt2", temp_file_problem(), "-m"};
58  break;
59 
61  argv = {"smt2_solver"};
62  stdin_filename = temp_file_problem();
63  break;
64 
65  case solvert::CVC3:
66  argv = {"cvc3",
67  "+model",
68  "-lang",
69  "smtlib",
70  "-output-lang",
71  "smtlib",
72  temp_file_problem()};
73  break;
74 
75  case solvert::CVC4:
76  // The flags --bitblast=eager --bv-div-zero-const help but only
77  // work for pure bit-vector formulas.
78  argv = {"cvc4", "-L", "smt2", temp_file_problem()};
79  break;
80 
81  case solvert::MATHSAT:
82  // The options below were recommended by Alberto Griggio
83  // on 10 July 2013
84 
85  argv = {"mathsat",
86  "-input=smt2",
87  "-preprocessor.toplevel_propagation=true",
88  "-preprocessor.simplification=7",
89  "-dpll.branching_random_frequency=0.01",
90  "-dpll.branching_random_invalidate_phase_cache=true",
91  "-dpll.restart_strategy=3",
92  "-dpll.glucose_var_activity=true",
93  "-dpll.glucose_learnt_minimization=true",
94  "-theory.bv.eager=true",
95  "-theory.bv.bit_blast_mode=1",
96  "-theory.bv.delay_propagated_eqs=true",
97  "-theory.fp.mode=1",
98  "-theory.fp.bit_blast_mode=2",
99  "-theory.arr.mode=1"};
100 
101  stdin_filename = temp_file_problem();
102  break;
103 
104  case solvert::YICES:
105  // command = "yices -smt -e " // Calling convention for older versions
106  // Convention for 2.2.1
107  argv = {"yices-smt2", temp_file_problem()};
108  break;
109 
110  case solvert::Z3:
111  argv = {"z3", "-smt2", temp_file_problem()};
112  break;
113 
114  default:
115  UNREACHABLE;
116  }
117 
118  int res =
119  run(argv[0], argv, stdin_filename, temp_file_stdout(), temp_file_stderr());
120 
121  if(res<0)
122  {
123  error() << "error running SMT2 solver" << eom;
125  }
126 
127  std::ifstream in(temp_file_stdout());
128  return read_result(in);
129 }
130 
132 {
133  std::string line;
135 
136  boolean_assignment.clear();
138 
139  typedef std::unordered_map<irep_idt, irept> valuest;
140  valuest values;
141 
142  while(in)
143  {
144  irept parsed=smt2irep(in);
145 
146  if(parsed.id()=="sat")
148  else if(parsed.id()=="unsat")
150  else if(parsed.id()=="" &&
151  parsed.get_sub().size()==1 &&
152  parsed.get_sub().front().get_sub().size()==2)
153  {
154  const irept &s0=parsed.get_sub().front().get_sub()[0];
155  const irept &s1=parsed.get_sub().front().get_sub()[1];
156 
157  // Examples:
158  // ( (B0 true) )
159  // ( (|__CPROVER_pipe_count#1| (_ bv0 32)) )
160  // ( (|some_integer| 0) )
161  // ( (|some_integer| (- 10)) )
162 
163  values[s0.id()]=s1;
164  }
165  else if(parsed.id()=="" &&
166  parsed.get_sub().size()==2 &&
167  parsed.get_sub().front().id()=="error")
168  {
169  // We ignore errors after UNSAT because get-value after check-sat
170  // returns unsat will give an error.
171  if(res!=resultt::D_UNSATISFIABLE)
172  {
173  error() << "SMT2 solver returned error message:\n"
174  << "\t\"" << parsed.get_sub()[1].id() <<"\"" << eom;
176  }
177  }
178  }
179 
180  for(auto &assignment : identifier_map)
181  {
182  std::string conv_id=convert_identifier(assignment.first);
183  const irept &value=values[conv_id];
184  assignment.second.value=parse_rec(value, assignment.second.type);
185  }
186 
187  // Booleans
188  for(unsigned v=0; v<no_boolean_variables; v++)
189  {
190  const irept &value=values["B"+std::to_string(v)];
191  boolean_assignment[v]=(value.id()==ID_true);
192  }
193 
194  return res;
195 }
smt2_convt::solvert::CVC4
smt2_convt::solver
solvert solver
Definition: smt2_conv.h:133
tempfile.h
smt2_convt::solvert::CPROVER_SMT2
arith_tools.h
smt2_dect::decision_procedure_text
virtual std::string decision_procedure_text() const
Definition: smt2_dec.cpp:21
decision_proceduret::resultt::D_UNSATISFIABLE
smt2_convt::solvert::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:47
invariant.h
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
messaget::eom
static eomt eom
Definition: message.h:284
run.h
smt2_convt::solvert::CVC3
smt2_stringstreamt::stringstream
std::stringstream stringstream
Definition: smt2_dec.h:20
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
smt2_convt::solvert::BOOLECTOR
decision_proceduret::resultt::D_SATISFIABLE
smt2_convt::convert_identifier
std::string convert_identifier(const irep_idt &identifier)
Definition: smt2_conv.cpp:757
smt2irep
irept smt2irep(std::istream &in)
Definition: smt2irep.cpp:97
messaget::error
mstreamt & error() const
Definition: message.h:386
smt2_convt::solvert::YICES
smt2_convt::identifier_map
identifier_mapt identifier_map
Definition: smt2_conv.h:299
std_types.h
smt2_dec.h
decision_proceduret::resultt::D_ERROR
irept::id
const irep_idt & id() const
Definition: irep.h:259
decision_proceduret::resultt
resultt
Definition: decision_procedure.h:47
smt2_dect::read_result
resultt read_result(std::istream &in)
Definition: smt2_dec.cpp:131
smt2_convt::use_FPA_theory
bool use_FPA_theory
Definition: smt2_conv.h:110
smt2_convt::logic
std::string logic
Definition: smt2_conv.h:132
smt2_convt::write_footer
void write_footer(std::ostream &)
Definition: smt2_conv.cpp:96
smt2_convt::parse_rec
exprt parse_rec(const irept &s, const typet &type)
Definition: smt2_conv.cpp:449
ieee_float.h
smt2_convt::no_boolean_variables
std::size_t no_boolean_variables
Definition: smt2_conv.h:321
smt2_dect::dec_solve
virtual resultt dec_solve()
Definition: smt2_dec.cpp:37
irept::get_sub
subt & get_sub()
Definition: irep.h:317
smt2_convt::solvert::GENERIC
smt2_convt::solvert::Z3
irept
Base class for tree-like data structures with sharing.
Definition: irep.h:156
smt2_convt::boolean_assignment
std::vector< bool > boolean_assignment
Definition: smt2_conv.h:322
smt2irep.h
std_expr.h
temporary_filet
Definition: tempfile.h:23