Andrew Walbran | 16937d0 | 2019-10-22 13:54:20 +0100 | [diff] [blame] | 1 | //===- SMTAPI.h -------------------------------------------------*- C++ -*-===// |
Andrew Scull | cdfcccc | 2018-10-05 20:58:37 +0100 | [diff] [blame] | 2 | // |
Andrew Walbran | 16937d0 | 2019-10-22 13:54:20 +0100 | [diff] [blame] | 3 | // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. |
| 4 | // See https://llvm.org/LICENSE.txt for license information. |
| 5 | // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception |
Andrew Scull | cdfcccc | 2018-10-05 20:58:37 +0100 | [diff] [blame] | 6 | // |
| 7 | //===----------------------------------------------------------------------===// |
| 8 | // |
| 9 | // This file defines a SMT generic Solver API, which will be the base class |
| 10 | // for every SMT solver specific class. |
| 11 | // |
| 12 | //===----------------------------------------------------------------------===// |
| 13 | |
Andrew Walbran | 3d2c197 | 2020-04-07 12:24:26 +0100 | [diff] [blame] | 14 | #ifndef LLVM_SUPPORT_SMTAPI_H |
| 15 | #define LLVM_SUPPORT_SMTAPI_H |
Andrew Scull | cdfcccc | 2018-10-05 20:58:37 +0100 | [diff] [blame] | 16 | |
Andrew Walbran | 3d2c197 | 2020-04-07 12:24:26 +0100 | [diff] [blame] | 17 | #include "llvm/ADT/APFloat.h" |
Andrew Scull | 0372a57 | 2018-11-16 15:47:06 +0000 | [diff] [blame] | 18 | #include "llvm/ADT/APSInt.h" |
Andrew Walbran | 16937d0 | 2019-10-22 13:54:20 +0100 | [diff] [blame] | 19 | #include "llvm/ADT/FoldingSet.h" |
Andrew Walbran | 3d2c197 | 2020-04-07 12:24:26 +0100 | [diff] [blame] | 20 | #include "llvm/Support/raw_ostream.h" |
| 21 | #include <memory> |
Andrew Scull | cdfcccc | 2018-10-05 20:58:37 +0100 | [diff] [blame] | 22 | |
Andrew Walbran | 3d2c197 | 2020-04-07 12:24:26 +0100 | [diff] [blame] | 23 | namespace llvm { |
Andrew Scull | cdfcccc | 2018-10-05 20:58:37 +0100 | [diff] [blame] | 24 | |
Andrew Walbran | 16937d0 | 2019-10-22 13:54:20 +0100 | [diff] [blame] | 25 | /// Generic base class for SMT sorts |
| 26 | class SMTSort { |
| 27 | public: |
| 28 | SMTSort() = default; |
| 29 | virtual ~SMTSort() = default; |
| 30 | |
| 31 | /// Returns true if the sort is a bitvector, calls isBitvectorSortImpl(). |
| 32 | virtual bool isBitvectorSort() const { return isBitvectorSortImpl(); } |
| 33 | |
| 34 | /// Returns true if the sort is a floating-point, calls isFloatSortImpl(). |
| 35 | virtual bool isFloatSort() const { return isFloatSortImpl(); } |
| 36 | |
| 37 | /// Returns true if the sort is a boolean, calls isBooleanSortImpl(). |
| 38 | virtual bool isBooleanSort() const { return isBooleanSortImpl(); } |
| 39 | |
| 40 | /// Returns the bitvector size, fails if the sort is not a bitvector |
| 41 | /// Calls getBitvectorSortSizeImpl(). |
| 42 | virtual unsigned getBitvectorSortSize() const { |
| 43 | assert(isBitvectorSort() && "Not a bitvector sort!"); |
| 44 | unsigned Size = getBitvectorSortSizeImpl(); |
| 45 | assert(Size && "Size is zero!"); |
| 46 | return Size; |
| 47 | }; |
| 48 | |
| 49 | /// Returns the floating-point size, fails if the sort is not a floating-point |
| 50 | /// Calls getFloatSortSizeImpl(). |
| 51 | virtual unsigned getFloatSortSize() const { |
| 52 | assert(isFloatSort() && "Not a floating-point sort!"); |
| 53 | unsigned Size = getFloatSortSizeImpl(); |
| 54 | assert(Size && "Size is zero!"); |
| 55 | return Size; |
| 56 | }; |
| 57 | |
| 58 | virtual void Profile(llvm::FoldingSetNodeID &ID) const = 0; |
| 59 | |
| 60 | bool operator<(const SMTSort &Other) const { |
| 61 | llvm::FoldingSetNodeID ID1, ID2; |
| 62 | Profile(ID1); |
| 63 | Other.Profile(ID2); |
| 64 | return ID1 < ID2; |
| 65 | } |
| 66 | |
| 67 | friend bool operator==(SMTSort const &LHS, SMTSort const &RHS) { |
| 68 | return LHS.equal_to(RHS); |
| 69 | } |
| 70 | |
| 71 | virtual void print(raw_ostream &OS) const = 0; |
| 72 | |
Andrew Walbran | 3d2c197 | 2020-04-07 12:24:26 +0100 | [diff] [blame] | 73 | LLVM_DUMP_METHOD void dump() const; |
Andrew Walbran | 16937d0 | 2019-10-22 13:54:20 +0100 | [diff] [blame] | 74 | |
| 75 | protected: |
| 76 | /// Query the SMT solver and returns true if two sorts are equal (same kind |
| 77 | /// and bit width). This does not check if the two sorts are the same objects. |
| 78 | virtual bool equal_to(SMTSort const &other) const = 0; |
| 79 | |
| 80 | /// Query the SMT solver and checks if a sort is bitvector. |
| 81 | virtual bool isBitvectorSortImpl() const = 0; |
| 82 | |
| 83 | /// Query the SMT solver and checks if a sort is floating-point. |
| 84 | virtual bool isFloatSortImpl() const = 0; |
| 85 | |
| 86 | /// Query the SMT solver and checks if a sort is boolean. |
| 87 | virtual bool isBooleanSortImpl() const = 0; |
| 88 | |
| 89 | /// Query the SMT solver and returns the sort bit width. |
| 90 | virtual unsigned getBitvectorSortSizeImpl() const = 0; |
| 91 | |
| 92 | /// Query the SMT solver and returns the sort bit width. |
| 93 | virtual unsigned getFloatSortSizeImpl() const = 0; |
| 94 | }; |
| 95 | |
| 96 | /// Shared pointer for SMTSorts, used by SMTSolver API. |
| 97 | using SMTSortRef = const SMTSort *; |
| 98 | |
| 99 | /// Generic base class for SMT exprs |
| 100 | class SMTExpr { |
| 101 | public: |
| 102 | SMTExpr() = default; |
| 103 | virtual ~SMTExpr() = default; |
| 104 | |
| 105 | bool operator<(const SMTExpr &Other) const { |
| 106 | llvm::FoldingSetNodeID ID1, ID2; |
| 107 | Profile(ID1); |
| 108 | Other.Profile(ID2); |
| 109 | return ID1 < ID2; |
| 110 | } |
| 111 | |
| 112 | virtual void Profile(llvm::FoldingSetNodeID &ID) const = 0; |
| 113 | |
| 114 | friend bool operator==(SMTExpr const &LHS, SMTExpr const &RHS) { |
| 115 | return LHS.equal_to(RHS); |
| 116 | } |
| 117 | |
| 118 | virtual void print(raw_ostream &OS) const = 0; |
| 119 | |
Andrew Walbran | 3d2c197 | 2020-04-07 12:24:26 +0100 | [diff] [blame] | 120 | LLVM_DUMP_METHOD void dump() const; |
Andrew Walbran | 16937d0 | 2019-10-22 13:54:20 +0100 | [diff] [blame] | 121 | |
| 122 | protected: |
| 123 | /// Query the SMT solver and returns true if two sorts are equal (same kind |
| 124 | /// and bit width). This does not check if the two sorts are the same objects. |
| 125 | virtual bool equal_to(SMTExpr const &other) const = 0; |
| 126 | }; |
| 127 | |
| 128 | /// Shared pointer for SMTExprs, used by SMTSolver API. |
| 129 | using SMTExprRef = const SMTExpr *; |
| 130 | |
Andrew Scull | cdfcccc | 2018-10-05 20:58:37 +0100 | [diff] [blame] | 131 | /// Generic base class for SMT Solvers |
| 132 | /// |
| 133 | /// This class is responsible for wrapping all sorts and expression generation, |
| 134 | /// through the mk* methods. It also provides methods to create SMT expressions |
| 135 | /// straight from clang's AST, through the from* methods. |
| 136 | class SMTSolver { |
| 137 | public: |
| 138 | SMTSolver() = default; |
| 139 | virtual ~SMTSolver() = default; |
| 140 | |
Andrew Walbran | 3d2c197 | 2020-04-07 12:24:26 +0100 | [diff] [blame] | 141 | LLVM_DUMP_METHOD void dump() const; |
Andrew Scull | cdfcccc | 2018-10-05 20:58:37 +0100 | [diff] [blame] | 142 | |
| 143 | // Returns an appropriate floating-point sort for the given bitwidth. |
| 144 | SMTSortRef getFloatSort(unsigned BitWidth) { |
| 145 | switch (BitWidth) { |
| 146 | case 16: |
| 147 | return getFloat16Sort(); |
| 148 | case 32: |
| 149 | return getFloat32Sort(); |
| 150 | case 64: |
| 151 | return getFloat64Sort(); |
| 152 | case 128: |
| 153 | return getFloat128Sort(); |
| 154 | default:; |
| 155 | } |
| 156 | llvm_unreachable("Unsupported floating-point bitwidth!"); |
| 157 | } |
| 158 | |
Andrew Scull | cdfcccc | 2018-10-05 20:58:37 +0100 | [diff] [blame] | 159 | // Returns a boolean sort. |
| 160 | virtual SMTSortRef getBoolSort() = 0; |
| 161 | |
| 162 | // Returns an appropriate bitvector sort for the given bitwidth. |
| 163 | virtual SMTSortRef getBitvectorSort(const unsigned BitWidth) = 0; |
| 164 | |
| 165 | // Returns a floating-point sort of width 16 |
| 166 | virtual SMTSortRef getFloat16Sort() = 0; |
| 167 | |
| 168 | // Returns a floating-point sort of width 32 |
| 169 | virtual SMTSortRef getFloat32Sort() = 0; |
| 170 | |
| 171 | // Returns a floating-point sort of width 64 |
| 172 | virtual SMTSortRef getFloat64Sort() = 0; |
| 173 | |
| 174 | // Returns a floating-point sort of width 128 |
| 175 | virtual SMTSortRef getFloat128Sort() = 0; |
| 176 | |
| 177 | // Returns an appropriate sort for the given AST. |
| 178 | virtual SMTSortRef getSort(const SMTExprRef &AST) = 0; |
| 179 | |
Andrew Scull | cdfcccc | 2018-10-05 20:58:37 +0100 | [diff] [blame] | 180 | /// Given a constraint, adds it to the solver |
| 181 | virtual void addConstraint(const SMTExprRef &Exp) const = 0; |
| 182 | |
| 183 | /// Creates a bitvector addition operation |
| 184 | virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 185 | |
| 186 | /// Creates a bitvector subtraction operation |
| 187 | virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 188 | |
| 189 | /// Creates a bitvector multiplication operation |
| 190 | virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 191 | |
| 192 | /// Creates a bitvector signed modulus operation |
| 193 | virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 194 | |
| 195 | /// Creates a bitvector unsigned modulus operation |
| 196 | virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 197 | |
| 198 | /// Creates a bitvector signed division operation |
| 199 | virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 200 | |
| 201 | /// Creates a bitvector unsigned division operation |
| 202 | virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 203 | |
| 204 | /// Creates a bitvector logical shift left operation |
| 205 | virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 206 | |
| 207 | /// Creates a bitvector arithmetic shift right operation |
| 208 | virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 209 | |
| 210 | /// Creates a bitvector logical shift right operation |
| 211 | virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 212 | |
| 213 | /// Creates a bitvector negation operation |
| 214 | virtual SMTExprRef mkBVNeg(const SMTExprRef &Exp) = 0; |
| 215 | |
| 216 | /// Creates a bitvector not operation |
| 217 | virtual SMTExprRef mkBVNot(const SMTExprRef &Exp) = 0; |
| 218 | |
| 219 | /// Creates a bitvector xor operation |
| 220 | virtual SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 221 | |
| 222 | /// Creates a bitvector or operation |
| 223 | virtual SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 224 | |
| 225 | /// Creates a bitvector and operation |
| 226 | virtual SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 227 | |
| 228 | /// Creates a bitvector unsigned less-than operation |
| 229 | virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 230 | |
| 231 | /// Creates a bitvector signed less-than operation |
| 232 | virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 233 | |
| 234 | /// Creates a bitvector unsigned greater-than operation |
| 235 | virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 236 | |
| 237 | /// Creates a bitvector signed greater-than operation |
| 238 | virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 239 | |
| 240 | /// Creates a bitvector unsigned less-equal-than operation |
| 241 | virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 242 | |
| 243 | /// Creates a bitvector signed less-equal-than operation |
| 244 | virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 245 | |
| 246 | /// Creates a bitvector unsigned greater-equal-than operation |
| 247 | virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 248 | |
| 249 | /// Creates a bitvector signed greater-equal-than operation |
| 250 | virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 251 | |
| 252 | /// Creates a boolean not operation |
| 253 | virtual SMTExprRef mkNot(const SMTExprRef &Exp) = 0; |
| 254 | |
| 255 | /// Creates a boolean equality operation |
| 256 | virtual SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 257 | |
| 258 | /// Creates a boolean and operation |
| 259 | virtual SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 260 | |
| 261 | /// Creates a boolean or operation |
| 262 | virtual SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 263 | |
| 264 | /// Creates a boolean ite operation |
| 265 | virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T, |
| 266 | const SMTExprRef &F) = 0; |
| 267 | |
| 268 | /// Creates a bitvector sign extension operation |
| 269 | virtual SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) = 0; |
| 270 | |
| 271 | /// Creates a bitvector zero extension operation |
| 272 | virtual SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) = 0; |
| 273 | |
| 274 | /// Creates a bitvector extract operation |
| 275 | virtual SMTExprRef mkBVExtract(unsigned High, unsigned Low, |
| 276 | const SMTExprRef &Exp) = 0; |
| 277 | |
| 278 | /// Creates a bitvector concat operation |
| 279 | virtual SMTExprRef mkBVConcat(const SMTExprRef &LHS, |
| 280 | const SMTExprRef &RHS) = 0; |
| 281 | |
Andrew Walbran | 3d2c197 | 2020-04-07 12:24:26 +0100 | [diff] [blame] | 282 | /// Creates a predicate that checks for overflow in a bitvector addition |
| 283 | /// operation |
| 284 | virtual SMTExprRef mkBVAddNoOverflow(const SMTExprRef &LHS, |
| 285 | const SMTExprRef &RHS, |
| 286 | bool isSigned) = 0; |
| 287 | |
| 288 | /// Creates a predicate that checks for underflow in a signed bitvector |
| 289 | /// addition operation |
| 290 | virtual SMTExprRef mkBVAddNoUnderflow(const SMTExprRef &LHS, |
| 291 | const SMTExprRef &RHS) = 0; |
| 292 | |
| 293 | /// Creates a predicate that checks for overflow in a signed bitvector |
| 294 | /// subtraction operation |
| 295 | virtual SMTExprRef mkBVSubNoOverflow(const SMTExprRef &LHS, |
| 296 | const SMTExprRef &RHS) = 0; |
| 297 | |
| 298 | /// Creates a predicate that checks for underflow in a bitvector subtraction |
| 299 | /// operation |
| 300 | virtual SMTExprRef mkBVSubNoUnderflow(const SMTExprRef &LHS, |
| 301 | const SMTExprRef &RHS, |
| 302 | bool isSigned) = 0; |
| 303 | |
| 304 | /// Creates a predicate that checks for overflow in a signed bitvector |
| 305 | /// division/modulus operation |
| 306 | virtual SMTExprRef mkBVSDivNoOverflow(const SMTExprRef &LHS, |
| 307 | const SMTExprRef &RHS) = 0; |
| 308 | |
| 309 | /// Creates a predicate that checks for overflow in a bitvector negation |
| 310 | /// operation |
| 311 | virtual SMTExprRef mkBVNegNoOverflow(const SMTExprRef &Exp) = 0; |
| 312 | |
| 313 | /// Creates a predicate that checks for overflow in a bitvector multiplication |
| 314 | /// operation |
| 315 | virtual SMTExprRef mkBVMulNoOverflow(const SMTExprRef &LHS, |
| 316 | const SMTExprRef &RHS, |
| 317 | bool isSigned) = 0; |
| 318 | |
| 319 | /// Creates a predicate that checks for underflow in a signed bitvector |
| 320 | /// multiplication operation |
| 321 | virtual SMTExprRef mkBVMulNoUnderflow(const SMTExprRef &LHS, |
| 322 | const SMTExprRef &RHS) = 0; |
| 323 | |
Andrew Scull | cdfcccc | 2018-10-05 20:58:37 +0100 | [diff] [blame] | 324 | /// Creates a floating-point negation operation |
| 325 | virtual SMTExprRef mkFPNeg(const SMTExprRef &Exp) = 0; |
| 326 | |
| 327 | /// Creates a floating-point isInfinite operation |
| 328 | virtual SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) = 0; |
| 329 | |
| 330 | /// Creates a floating-point isNaN operation |
| 331 | virtual SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) = 0; |
| 332 | |
| 333 | /// Creates a floating-point isNormal operation |
| 334 | virtual SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) = 0; |
| 335 | |
| 336 | /// Creates a floating-point isZero operation |
| 337 | virtual SMTExprRef mkFPIsZero(const SMTExprRef &Exp) = 0; |
| 338 | |
| 339 | /// Creates a floating-point multiplication operation |
| 340 | virtual SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 341 | |
| 342 | /// Creates a floating-point division operation |
| 343 | virtual SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 344 | |
| 345 | /// Creates a floating-point remainder operation |
| 346 | virtual SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 347 | |
| 348 | /// Creates a floating-point addition operation |
| 349 | virtual SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 350 | |
| 351 | /// Creates a floating-point subtraction operation |
| 352 | virtual SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 353 | |
| 354 | /// Creates a floating-point less-than operation |
| 355 | virtual SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 356 | |
| 357 | /// Creates a floating-point greater-than operation |
| 358 | virtual SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 359 | |
| 360 | /// Creates a floating-point less-than-or-equal operation |
| 361 | virtual SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 362 | |
| 363 | /// Creates a floating-point greater-than-or-equal operation |
| 364 | virtual SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0; |
| 365 | |
| 366 | /// Creates a floating-point equality operation |
| 367 | virtual SMTExprRef mkFPEqual(const SMTExprRef &LHS, |
| 368 | const SMTExprRef &RHS) = 0; |
| 369 | |
| 370 | /// Creates a floating-point conversion from floatint-point to floating-point |
| 371 | /// operation |
| 372 | virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) = 0; |
| 373 | |
Andrew Scull | cdfcccc | 2018-10-05 20:58:37 +0100 | [diff] [blame] | 374 | /// Creates a floating-point conversion from signed bitvector to |
| 375 | /// floatint-point operation |
Andrew Scull | 0372a57 | 2018-11-16 15:47:06 +0000 | [diff] [blame] | 376 | virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From, |
| 377 | const SMTSortRef &To) = 0; |
Andrew Scull | cdfcccc | 2018-10-05 20:58:37 +0100 | [diff] [blame] | 378 | |
| 379 | /// Creates a floating-point conversion from unsigned bitvector to |
| 380 | /// floatint-point operation |
Andrew Scull | 0372a57 | 2018-11-16 15:47:06 +0000 | [diff] [blame] | 381 | virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From, |
| 382 | const SMTSortRef &To) = 0; |
| 383 | |
| 384 | /// Creates a floating-point conversion from floatint-point to signed |
| 385 | /// bitvector operation |
| 386 | virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) = 0; |
| 387 | |
| 388 | /// Creates a floating-point conversion from floatint-point to unsigned |
| 389 | /// bitvector operation |
| 390 | virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) = 0; |
Andrew Scull | cdfcccc | 2018-10-05 20:58:37 +0100 | [diff] [blame] | 391 | |
| 392 | /// Creates a new symbol, given a name and a sort |
| 393 | virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) = 0; |
| 394 | |
| 395 | // Returns an appropriate floating-point rounding mode. |
| 396 | virtual SMTExprRef getFloatRoundingMode() = 0; |
| 397 | |
| 398 | // If the a model is available, returns the value of a given bitvector symbol |
| 399 | virtual llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth, |
| 400 | bool isUnsigned) = 0; |
| 401 | |
| 402 | // If the a model is available, returns the value of a given boolean symbol |
| 403 | virtual bool getBoolean(const SMTExprRef &Exp) = 0; |
| 404 | |
| 405 | /// Constructs an SMTExprRef from a boolean. |
| 406 | virtual SMTExprRef mkBoolean(const bool b) = 0; |
| 407 | |
| 408 | /// Constructs an SMTExprRef from a finite APFloat. |
| 409 | virtual SMTExprRef mkFloat(const llvm::APFloat Float) = 0; |
| 410 | |
| 411 | /// Constructs an SMTExprRef from an APSInt and its bit width |
| 412 | virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) = 0; |
| 413 | |
| 414 | /// Given an expression, extract the value of this operand in the model. |
| 415 | virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) = 0; |
| 416 | |
| 417 | /// Given an expression extract the value of this operand in the model. |
| 418 | virtual bool getInterpretation(const SMTExprRef &Exp, |
| 419 | llvm::APFloat &Float) = 0; |
| 420 | |
Andrew Scull | cdfcccc | 2018-10-05 20:58:37 +0100 | [diff] [blame] | 421 | /// Check if the constraints are satisfiable |
Andrew Scull | 0372a57 | 2018-11-16 15:47:06 +0000 | [diff] [blame] | 422 | virtual Optional<bool> check() const = 0; |
Andrew Scull | cdfcccc | 2018-10-05 20:58:37 +0100 | [diff] [blame] | 423 | |
| 424 | /// Push the current solver state |
| 425 | virtual void push() = 0; |
| 426 | |
| 427 | /// Pop the previous solver state |
| 428 | virtual void pop(unsigned NumStates = 1) = 0; |
| 429 | |
| 430 | /// Reset the solver and remove all constraints. |
Andrew Walbran | 16937d0 | 2019-10-22 13:54:20 +0100 | [diff] [blame] | 431 | virtual void reset() = 0; |
| 432 | |
| 433 | /// Checks if the solver supports floating-points. |
| 434 | virtual bool isFPSupported() = 0; |
Andrew Scull | cdfcccc | 2018-10-05 20:58:37 +0100 | [diff] [blame] | 435 | |
| 436 | virtual void print(raw_ostream &OS) const = 0; |
| 437 | }; |
| 438 | |
| 439 | /// Shared pointer for SMTSolvers. |
| 440 | using SMTSolverRef = std::shared_ptr<SMTSolver>; |
| 441 | |
| 442 | /// Convenience method to create and Z3Solver object |
Andrew Scull | 0372a57 | 2018-11-16 15:47:06 +0000 | [diff] [blame] | 443 | SMTSolverRef CreateZ3Solver(); |
Andrew Scull | cdfcccc | 2018-10-05 20:58:37 +0100 | [diff] [blame] | 444 | |
Andrew Walbran | 3d2c197 | 2020-04-07 12:24:26 +0100 | [diff] [blame] | 445 | } // namespace llvm |
Andrew Scull | cdfcccc | 2018-10-05 20:58:37 +0100 | [diff] [blame] | 446 | |
| 447 | #endif |