1 //== SMTSort.h --------------------------------------------------*- C++ -*--==//
3 // The LLVM Compiler Infrastructure
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
8 //===----------------------------------------------------------------------===//
10 // This file defines a SMT generic Sort API, which will be the base class
11 // for every SMT solver sort specific class.
13 //===----------------------------------------------------------------------===//
15 #ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSORT_H
16 #define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTSORT_H
18 #include "clang/Basic/TargetInfo.h"
23 /// Generic base class for SMT sorts
27 virtual ~SMTSort() = default;
29 /// Returns true if the sort is a bitvector, calls isBitvectorSortImpl().
30 virtual bool isBitvectorSort() const { return isBitvectorSortImpl(); }
32 /// Returns true if the sort is a floating-point, calls isFloatSortImpl().
33 virtual bool isFloatSort() const { return isFloatSortImpl(); }
35 /// Returns true if the sort is a boolean, calls isBooleanSortImpl().
36 virtual bool isBooleanSort() const { return isBooleanSortImpl(); }
38 /// Returns the bitvector size, fails if the sort is not a bitvector
39 /// Calls getBitvectorSortSizeImpl().
40 virtual unsigned getBitvectorSortSize() const {
41 assert(isBitvectorSort() && "Not a bitvector sort!");
42 unsigned Size = getBitvectorSortSizeImpl();
43 assert(Size && "Size is zero!");
47 /// Returns the floating-point size, fails if the sort is not a floating-point
48 /// Calls getFloatSortSizeImpl().
49 virtual unsigned getFloatSortSize() const {
50 assert(isFloatSort() && "Not a floating-point sort!");
51 unsigned Size = getFloatSortSizeImpl();
52 assert(Size && "Size is zero!");
56 friend bool operator==(SMTSort const &LHS, SMTSort const &RHS) {
57 return LHS.equal_to(RHS);
60 virtual void print(raw_ostream &OS) const = 0;
62 LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
65 /// Query the SMT solver and returns true if two sorts are equal (same kind
66 /// and bit width). This does not check if the two sorts are the same objects.
67 virtual bool equal_to(SMTSort const &other) const = 0;
69 /// Query the SMT solver and checks if a sort is bitvector.
70 virtual bool isBitvectorSortImpl() const = 0;
72 /// Query the SMT solver and checks if a sort is floating-point.
73 virtual bool isFloatSortImpl() const = 0;
75 /// Query the SMT solver and checks if a sort is boolean.
76 virtual bool isBooleanSortImpl() const = 0;
78 /// Query the SMT solver and returns the sort bit width.
79 virtual unsigned getBitvectorSortSizeImpl() const = 0;
81 /// Query the SMT solver and returns the sort bit width.
82 virtual unsigned getFloatSortSizeImpl() const = 0;
85 /// Shared pointer for SMTSorts, used by SMTSolver API.
86 using SMTSortRef = std::shared_ptr<SMTSort>;