contrib/llvm/tools/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h

   1 //== SMTExpr.h --------------------------------------------------*- C++ -*--==//
   2 //
   3 //                     The LLVM Compiler Infrastructure
   4 //
   5 // This file is distributed under the University of Illinois Open Source
   6 // License. See LICENSE.TXT for details.
   7 //
   8 //===----------------------------------------------------------------------===//
   9 //
  10 //  This file defines a SMT generic Expr API, which will be the base class
  11 //  for every SMT solver expr specific class.
  12 //
  13 //===----------------------------------------------------------------------===//
  14
  15 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTEXPR_H
  16 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTEXPR_H
  17
  18 #include "clang/Basic/TargetInfo.h"
  19 #include "llvm/ADT/FoldingSet.h"
  20
  21 namespace clang {
  22 namespace ento {
  23
  24 /// Generic base class for SMT exprs
  25 class SMTExpr {
  26 public:
  27   SMTExpr() = default;
  28   virtual ~SMTExpr() = default;
  29
  30   bool operator<(const SMTExpr &Other) const {
  31     llvm::FoldingSetNodeID ID1, ID2;
  32     Profile(ID1);
  33     Other.Profile(ID2);
  34     return ID1 < ID2;
  35   }
  36
  37   virtual void Profile(llvm::FoldingSetNodeID &ID) const {
  38     static int Tag = 0;
  39     ID.AddPointer(&Tag);
  40   }
  41
  42   friend bool operator==(SMTExpr const &LHS, SMTExpr const &RHS) {
  43     return LHS.equal_to(RHS);
  44   }
  45
  46   virtual void print(raw_ostream &OS) const = 0;
  47
  48   LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
  49
  50 protected:
  51   /// Query the SMT solver and returns true if two sorts are equal (same kind
  52   /// and bit width). This does not check if the two sorts are the same objects.
  53   virtual bool equal_to(SMTExpr const &other) const = 0;
  54 };
  55
  56 /// Shared pointer for SMTExprs, used by SMTSolver API.
  57 using SMTExprRef = std::shared_ptr<SMTExpr>;
  58
  59 } // namespace ento
  60 } // namespace clang
  61
  62 #endif