cprover
smt2_solver.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: SMT2 Solver that uses boolbv and the default SAT solver
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include <fstream>
10 #include <iostream>
11 
12 #include "smt2_parser.h"
13 
14 #include <util/namespace.h>
15 #include <util/symbol_table.h>
16 #include <util/cout_message.h>
17 #include <util/simplify_expr.h>
18 #include <util/replace_symbol.h>
19 
20 #include <solvers/sat/satcheck.h>
22 
24 {
25 public:
27  std::istream &_in,
28  decision_proceduret &_solver):
29  smt2_parsert(_in),
30  solver(_solver)
31  {
32  }
33 
34 protected:
36 
37  void command(const std::string &) override;
38  void define_constants(const exprt &);
40 
41  std::set<irep_idt> constants_done;
42 };
43 
45 {
46  for(const auto &op : expr.operands())
47  define_constants(op);
48 
49  if(expr.id()==ID_symbol)
50  {
51  irep_idt identifier=to_symbol_expr(expr).get_identifier();
52 
53  // already done?
54  if(constants_done.find(identifier)!=constants_done.end())
55  return;
56 
57  constants_done.insert(identifier);
58 
59  auto f_it=id_map.find(identifier);
60 
61  if(f_it!=id_map.end())
62  {
63  const auto &f=f_it->second;
64 
65  if(f.type.id()!=ID_mathematical_function &&
66  f.definition.is_not_nil())
67  {
68  exprt def=f.definition;
70  define_constants(def); // recursive!
71  solver.set_to_true(equal_exprt(expr, def));
72  }
73  }
74  }
75 }
76 
78 {
79  for(exprt &op : expr.operands())
81 
82  if(expr.id()==ID_function_application)
83  {
84  auto &app=to_function_application_expr(expr);
85 
86  // look it up
87  irep_idt identifier=app.function().get_identifier();
88  auto f_it=id_map.find(identifier);
89 
90  if(f_it!=id_map.end())
91  {
92  const auto &f=f_it->second;
93 
94  DATA_INVARIANT(f.type.id()==ID_mathematical_function,
95  "type of function symbol must be mathematical_function_type");
96 
97  const auto f_type=
99 
100  DATA_INVARIANT(f_type.domain().size()==
101  app.arguments().size(),
102  "number of function parameters");
103 
104  replace_symbolt replace_symbol;
105 
106  std::map<irep_idt, exprt> parameter_map;
107  for(std::size_t i=0; i<f_type.domain().size(); i++)
108  {
109  const irep_idt p_identifier=
110  f_type.domain()[i].get_identifier();
111 
112  replace_symbol.insert(p_identifier, app.arguments()[i]);
113  }
114 
115  exprt body=f.definition;
116  replace_symbol(body);
118  expr=body;
119  }
120  }
121 }
122 
123 void smt2_solvert::command(const std::string &c)
124 {
125  try
126  {
127  if(c=="assert")
128  {
129  exprt e=expression();
130  if(e.is_not_nil())
131  {
133  define_constants(e);
134  solver.set_to_true(e);
135  }
136  }
137  else if(c=="check-sat")
138  {
139  switch(solver())
140  {
142  std::cout << "sat\n";
143  break;
144 
146  std::cout << "unsat\n";
147  break;
148 
150  std::cout << "error\n";
151  }
152  }
153  else if(c=="check-sat-assuming")
154  {
155  std::cout << "not yet implemented\n";
156  }
157  else if(c=="display")
158  {
159  // this is a command that Z3 appears to implement
160  exprt e=expression();
161  if(e.is_not_nil())
162  {
163  std::cout << e.pretty() << '\n'; // need to do an 'smt2_format'
164  }
165  }
166  else if(c=="simplify")
167  {
168  // this is a command that Z3 appears to implement
169  exprt e=expression();
170  if(e.is_not_nil())
171  {
172  const symbol_tablet symbol_table;
173  const namespacet ns(symbol_table);
174  exprt e_simplified=simplify_expr(e, ns);
175  std::cout << e.pretty() << '\n'; // need to do an 'smt2_format'
176  }
177  }
178  #if 0
179  // TODO:
180  | ( declare-const hsymboli hsorti )
181  | ( declare-datatype hsymboli hdatatype_deci)
182  | ( declare-datatypes ( hsort_deci n+1 ) ( hdatatype_deci n+1 ) )
183  | ( declare-fun hsymboli ( hsorti ??? ) hsorti )
184  | ( declare-sort hsymboli hnumerali )
185  | ( define-fun hfunction_def i )
186  | ( define-fun-rec hfunction_def i )
187  | ( define-funs-rec ( hfunction_deci n+1 ) ( htermi n+1 ) )
188  | ( define-sort hsymboli ( hsymboli ??? ) hsorti )
189  | ( echo hstringi )
190  | ( exit )
191  | ( get-assertions )
192  | ( get-assignment )
193  | ( get-info hinfo_flag i )
194  | ( get-model )
195  | ( get-option hkeywordi )
196  | ( get-proof )
197  | ( get-unsat-assumptions )
198  | ( get-unsat-core )
199  | ( get-value ( htermi + ) )
200  | ( pop hnumerali )
201  | ( push hnumerali )
202  | ( reset )
203  | ( reset-assertions )
204  | ( set-info hattributei )
205  | ( set-option hoptioni )
206  #endif
207  else
209  }
210  catch(const char *error)
211  {
212  std::cout << "error: " << error << '\n';
213  }
214  catch(const std::string &error)
215  {
216  std::cout << "error: " << error << '\n';
217  }
218 }
219 
220 int solver(std::istream &in)
221 {
222  symbol_tablet symbol_table;
223  namespacet ns(symbol_table);
224 
226  messaget message(message_handler);
227 
228  // this is our default verbosity
230 
231  satcheckt satcheck;
232  boolbvt boolbv(ns, satcheck);
233  satcheck.set_message_handler(message_handler);
235 
236  smt2_solvert smt2_solver(in, boolbv);
238 
239  smt2_solver.parse();
240 
241  if(!smt2_solver)
242  return 20;
243  else
244  return 0;
245 }
246 
247 int main(int argc, const char *argv[])
248 {
249  if(argc==1)
250  return solver(std::cin);
251 
252  if(argc!=2)
253  {
254  std::cerr << "usage: smt2_solver file\n";
255  return 1;
256  }
257 
258  std::ifstream in(argv[1]);
259  if(!in)
260  {
261  std::cerr << "failed to open " << argv[1] << '\n';
262  return 1;
263  }
264 
265  return solver(in);
266 }
bool is_not_nil() const
Definition: irep.h:103
smt2_solvert(std::istream &_in, decision_proceduret &_solver)
Definition: smt2_solver.cpp:26
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
exprt simplify_expr(const exprt &src, const namespacet &ns)
bool parse() override
Definition: smt2_parser.h:27
const irep_idt & get_identifier() const
Definition: std_expr.h:128
void define_constants(const exprt &)
Definition: smt2_solver.cpp:44
Definition: boolbv.h:31
equality
Definition: std_expr.h:1354
const irep_idt & id() const
Definition: irep.h:189
int solver(std::istream &in)
void expand_function_applications(exprt &)
Definition: smt2_solver.cpp:77
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast a generic exprt to a function_application_exprt.
Definition: std_expr.h:4585
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:148
std::set< irep_idt > constants_done
Definition: smt2_solver.cpp:41
int main(int argc, const char *argv[])
Author: Diffblue Ltd.
exprt expression()
id_mapt id_map
Definition: smt2_parser.h:44
virtual void command(const std::string &)
Base class for all expressions.
Definition: expr.h:42
void set_to_true(const exprt &expr)
void command(const std::string &) override
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
decision_proceduret & solver
Definition: smt2_solver.cpp:35
const mathematical_function_typet & to_mathematical_function_type(const typet &type)
Cast a generic typet to a mathematical_function_typet.
Definition: std_types.h:1799
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
operandst & operands()
Definition: expr.h:66
mstreamt & error()