CBMC
smt2irep.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_SOLVERS_SMT2_SMT2IREP_H
11 #define CPROVER_SOLVERS_SMT2_SMT2IREP_H
12 
13 #include <iosfwd>
14 
15 #include <util/optional.h>
16 
17 class irept;
18 class message_handlert;
19 
22 optionalt<irept> smt2irep(std::istream &, message_handlert &);
23 
24 #endif // CPROVER_SOLVERS_SMT2_SMT2IREP_H
optional.h
smt2irep
optionalt< irept > smt2irep(std::istream &, message_handlert &)
returns an irep for an SMT-LIB2 expression read from a given stream returns {} when EOF is encountere...
Definition: smt2irep.cpp:91
message_handlert
Definition: message.h:27
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:359