klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ExprPPrinter.h
Go to the documentation of this file.
1 //===-- ExprPPrinter.h ------------------------------------------*- C++ -*-===//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 
10 #ifndef KLEE_EXPRPPRINTER_H
11 #define KLEE_EXPRPPRINTER_H
12 
13 #include "klee/Expr.h"
14 
15 namespace llvm {
16  class raw_ostream;
17 }
18 namespace klee {
19  class ConstraintManager;
20 
21  class ExprPPrinter {
22  protected:
24 
25  public:
26  static ExprPPrinter *create(llvm::raw_ostream &os);
27 
28  virtual ~ExprPPrinter() {}
29 
30  virtual void setNewline(const std::string &newline) = 0;
31  virtual void setForceNoLineBreaks(bool forceNoLineBreaks) = 0;
32  virtual void reset() = 0;
33  virtual void scan(const ref<Expr> &e) = 0;
34  virtual void print(const ref<Expr> &e, unsigned indent=0) = 0;
35 
36  // utility methods
37 
38  template<class Container>
39  void scan(Container c) {
40  scan(c.begin(), c.end());
41  }
42 
43  template<class InputIterator>
44  void scan(InputIterator it, InputIterator end) {
45  for (; it!=end; ++it)
46  scan(*it);
47  }
48 
51  static void printOne(llvm::raw_ostream &os, const char *message,
52  const ref<Expr> &e);
53 
61  static void printSingleExpr(llvm::raw_ostream &os, const ref<Expr> &e);
62 
63  static void printConstraints(llvm::raw_ostream &os,
64  const ConstraintManager &constraints);
65 
66  static void printQuery(llvm::raw_ostream &os,
67  const ConstraintManager &constraints,
68  const ref<Expr> &q,
69  const ref<Expr> *evalExprsBegin = 0,
70  const ref<Expr> *evalExprsEnd = 0,
71  const Array * const* evalArraysBegin = 0,
72  const Array * const* evalArraysEnd = 0,
73  bool printArrayDecls = true);
74  };
75 
76 }
77 
78 #endif
virtual ~ExprPPrinter()
Definition: ExprPPrinter.h:28
virtual void reset()=0
void scan(Container c)
Definition: ExprPPrinter.h:39
int const char * message
Definition: klee.h:68
static void printOne(llvm::raw_ostream &os, const char *message, const ref< Expr > &e)
virtual void print(const ref< Expr > &e, unsigned indent=0)=0
virtual void setForceNoLineBreaks(bool forceNoLineBreaks)=0
virtual void scan(const ref< Expr > &e)=0
static void printSingleExpr(llvm::raw_ostream &os, const ref< Expr > &e)
static ExprPPrinter * create(llvm::raw_ostream &os)
virtual void setNewline(const std::string &newline)=0
void scan(InputIterator it, InputIterator end)
Definition: ExprPPrinter.h:44
static void printQuery(llvm::raw_ostream &os, const ConstraintManager &constraints, const ref< Expr > &q, const ref< Expr > *evalExprsBegin=0, const ref< Expr > *evalExprsEnd=0, const Array *const *evalArraysBegin=0, const Array *const *evalArraysEnd=0, bool printArrayDecls=true)
static void printConstraints(llvm::raw_ostream &os, const ConstraintManager &constraints)