HomeSort by: relevance | last modified time | path
    Searched refs:SMTExpr (Results 1 - 3 of 3) sorted by relevancy

  /src/external/apache2/llvm/dist/llvm/include/llvm/Support/
SMTAPI.h 100 class SMTExpr {
102 SMTExpr() = default;
103 virtual ~SMTExpr() = default;
105 bool operator<(const SMTExpr &Other) const {
114 friend bool operator==(SMTExpr const &LHS, SMTExpr const &RHS) {
125 virtual bool equal_to(SMTExpr const &other) const = 0;
129 using SMTExprRef = const SMTExpr *;
  /src/external/apache2/llvm/dist/llvm/lib/Support/
Z3Solver.cpp 142 class Z3Expr : public SMTExpr {
150 Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) {
155 Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) {
181 bool equal_to(SMTExpr const &Other) const override {
195 static const Z3Expr &toZ3Expr(const SMTExpr &E) {
297 // Given an SMTExpr, adds/retrives it from the cache and returns
298 // an SMTExprRef to the SMTExpr in the cache
299 SMTExprRef newExprRef(const SMTExpr &Exp) {
915 LLVM_DUMP_METHOD void SMTExpr::dump() const { print(llvm::errs()); }
  /src/external/apache2/llvm/dist/clang/include/clang/StaticAnalyzer/Core/PathSensitive/
SMTConstraintManager.h 23 std::pair<clang::ento::SymbolRef, const llvm::SMTExpr *>>

Completed in 31 milliseconds