klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ExprSMTLIBLetPrinter.h
Go to the documentation of this file.
1 //===-- ExprSMTLIBLetPrinter.h ------------------------------------------*- C++
2 //-*-===//
3 //
4 // The KLEE Symbolic Virtual Machine
5 //
6 // This file is distributed under the University of Illinois Open Source
7 // License. See LICENSE.TXT for details.
8 //
9 //===----------------------------------------------------------------------===//
10 
11 #include "ExprSMTLIBPrinter.h"
12 #ifndef EXPRSMTLETPRINTER_H_
13 #define EXPRSMTLETPRINTER_H_
14 
15 namespace klee {
24 public:
26  virtual ~ExprSMTLIBLetPrinter() {}
27  virtual void generateOutput();
28 
29 protected:
30  virtual void scan(const ref<Expr> &e);
31  virtual void reset();
32  virtual void generateBindings();
33  void printExpression(const ref<Expr> &e,
34  ExprSMTLIBPrinter::SMTLIB_SORT expectedSort);
35  void printLetExpression();
36 
37 private:
39  std::map<const ref<Expr>, unsigned int> bindings;
40 
41  /* These are effectively expression counters.
42  * firstEO - first Occurrence of expression contains
43  * all expressions that occur once. It is
44  * only used to help us fill twoOrMoreOE
45  *
46  * twoOrMoreEO - Contains occur all expressions that
47  * that occur two or more times. These
48  * are the expressions that will be
49  * abbreviated by using (let () ()) expressions.
50  *
51  *
52  *
53  */
54  std::set<ref<Expr> > firstEO, twoOrMoreEO;
55 
57  static const char BINDING_PREFIX[];
58 
59  /* This is needed during un-abbreviated printing.
60  * Because we have overloaded printExpression()
61  * the parent will call it and will abbreviate
62  * when we don't want it to. This bool allows us
63  * to switch it on/off easily.
64  */
66 };
67 
71 }
72 
73 #endif /* EXPRSMTLETPRINTER_H_ */
ExprSMTLIBPrinter * createSMTLIBPrinter()
SMTLIB_SORT
Different supported SMTLIBv2 sorts (a.k.a type) in QF_AUFBV.
void printExpression(const ref< Expr > &e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort)
std::map< const ref< Expr >, unsigned int > bindings
Let expression binding number map.
std::set< ref< Expr > > firstEO
static const char BINDING_PREFIX[]
This is the prefix string used for all abbreviations in (let) expressions.
std::set< ref< Expr > > twoOrMoreEO
virtual void scan(const ref< Expr > &e)