File Manager

003 File Manager

Current Path: /usr/src/contrib/llvm-project/llvm/include/llvm/Support

usr / src / contrib / llvm-project / llvm / include / llvm / Support /

📁 ..
📄 AArch64TargetParser.def(12.01 KB)
📄 AArch64TargetParser.h(4.89 KB)
📄 AMDGPUMetadata.h(17.98 KB)
📄 AMDHSAKernelDescriptor.h(7.63 KB)
📄 ARMAttributeParser.h(3.2 KB)
📄 ARMBuildAttributes.h(8.6 KB)
📄 ARMEHABI.h(3.72 KB)
📄 ARMTargetParser.def(18.94 KB)
📄 ARMTargetParser.h(8.76 KB)
📄 ARMWinEH.h(18.27 KB)
📄 AlignOf.h(1.56 KB)
📄 Alignment.h(12.95 KB)
📄 Allocator.h(16.54 KB)
📄 AllocatorBase.h(3.87 KB)
📄 ArrayRecycler.h(4.78 KB)
📄 Atomic.h(1.09 KB)
📄 AtomicOrdering.h(6.01 KB)
📄 Automaton.h(9.64 KB)
📄 Base64.h(1.84 KB)
📄 BinaryByteStream.h(9.14 KB)
📄 BinaryItemStream.h(3.63 KB)
📄 BinaryStream.h(3.75 KB)
📄 BinaryStreamArray.h(12.46 KB)
📄 BinaryStreamError.h(1.29 KB)
📄 BinaryStreamReader.h(11.01 KB)
📄 BinaryStreamRef.h(10.09 KB)
📄 BinaryStreamWriter.h(7.79 KB)
📄 BlockFrequency.h(2.41 KB)
📄 BranchProbability.h(7.92 KB)
📄 BuryPointer.h(1.03 KB)
📄 CBindingWrapping.h(1.86 KB)
📄 CFGDiff.h(9.95 KB)
📄 CFGUpdate.h(4.12 KB)
📄 COM.h(1004 B)
📄 CRC.h(1.63 KB)
📄 CachePruning.h(3.5 KB)
📄 Capacity.h(972 B)
📄 Casting.h(13.92 KB)
📄 CheckedArithmetic.h(3.71 KB)
📄 Chrono.h(5.78 KB)
📄 CodeGen.h(1.96 KB)
📄 CodeGenCoverage.h(1.18 KB)
📄 CommandLine.h(71.22 KB)
📄 Compiler.h(19.5 KB)
📄 Compression.h(1.39 KB)
📄 ConvertUTF.h(11.4 KB)
📄 CrashRecoveryContext.h(9.26 KB)
📄 DJB.h(1.05 KB)
📄 DOTGraphTraits.h(5.58 KB)
📄 DataExtractor.h(30.28 KB)
📄 DataTypes.h(775 B)
📄 Debug.h(4.7 KB)
📄 DebugCounter.h(7.01 KB)
📄 DynamicLibrary.h(5.77 KB)
📄 ELFAttributeParser.h(2.22 KB)
📄 ELFAttributes.h(1.02 KB)
📄 Endian.h(14.28 KB)
📄 EndianStream.h(1.93 KB)
📄 Errc.h(3.8 KB)
📄 Errno.h(1.45 KB)
📄 Error.h(43.82 KB)
📄 ErrorHandling.h(6.39 KB)
📄 ErrorOr.h(7.48 KB)
📄 ExtensibleRTTI.h(4.02 KB)
📄 FileCheck.h(6.69 KB)
📄 FileCollector.h(3.74 KB)
📄 FileOutputBuffer.h(3.36 KB)
📄 FileSystem.h(53.03 KB)
📄 FileUtilities.h(3.83 KB)
📄 Format.h(9.45 KB)
📄 FormatAdapters.h(3.38 KB)
📄 FormatCommon.h(2.05 KB)
📄 FormatProviders.h(15.27 KB)
📄 FormatVariadic.h(9.88 KB)
📄 FormatVariadicDetails.h(5.3 KB)
📄 FormattedStream.h(6.42 KB)
📄 GenericDomTree.h(30.89 KB)
📄 GenericDomTreeConstruction.h(63.42 KB)
📄 GenericIteratedDominanceFrontier.h(7.31 KB)
📄 GlobPattern.h(1.35 KB)
📄 GraphWriter.h(11.79 KB)
📄 Host.h(2.68 KB)
📄 InitLLVM.h(1.79 KB)
📄 ItaniumManglingCanonicalizer.h(3.17 KB)
📄 JSON.h(28.25 KB)
📄 KnownBits.h(8.35 KB)
📄 LEB128.h(5.74 KB)
📄 LineIterator.h(2.62 KB)
📄 Locale.h(223 B)
📄 LockFileManager.h(3.13 KB)
📄 LowLevelTypeImpl.h(11.94 KB)
📄 MD5.h(3.39 KB)
📄 MSVCErrorWorkarounds.h(2.62 KB)
📄 MachineValueType.h(42.37 KB)
📄 ManagedStatic.h(4.21 KB)
📄 MathExtras.h(32.81 KB)
📄 MemAlloc.h(3.21 KB)
📄 Memory.h(6.94 KB)
📄 MemoryBuffer.h(10.98 KB)
📄 MipsABIFlags.h(3.92 KB)
📄 Mutex.h(2.14 KB)
📄 NativeFormatting.h(1.64 KB)
📄 OnDiskHashTable.h(21.97 KB)
📄 OptimizedStructLayout.h(5.89 KB)
📄 Parallel.h(5.99 KB)
📄 Path.h(15.6 KB)
📄 PluginLoader.h(1.29 KB)
📄 PointerLikeTypeTraits.h(5.69 KB)
📄 PrettyStackTrace.h(4.45 KB)
📄 Printable.h(1.5 KB)
📄 Process.h(9.31 KB)
📄 Program.h(10.35 KB)
📄 RISCVAttributeParser.h(1.15 KB)
📄 RISCVAttributes.h(1.2 KB)
📄 RISCVTargetParser.def(446 B)
📄 RWMutex.h(5.65 KB)
📄 RandomNumberGenerator.h(2.29 KB)
📄 Recycler.h(3.47 KB)
📄 RecyclingAllocator.h(2.38 KB)
📄 Regex.h(4.37 KB)
📄 Registry.h(5.14 KB)
📄 ReverseIteration.h(360 B)
📄 SHA1.h(2.37 KB)
📄 SMLoc.h(1.78 KB)
📄 SMTAPI.h(16.33 KB)
📄 SaveAndRestore.h(1.02 KB)
📄 ScaledNumber.h(30.65 KB)
📄 ScopedPrinter.h(11.39 KB)
📄 Signals.h(5.22 KB)
📄 Signposts.h(1.29 KB)
📄 SmallVectorMemoryBuffer.h(2.28 KB)
📁 Solaris
📄 SourceMgr.h(10.37 KB)
📄 SpecialCaseList.h(6.01 KB)
📄 StringSaver.h(1.94 KB)
📄 SuffixTree.h(13.15 KB)
📄 SwapByteOrder.h(4.8 KB)
📄 SymbolRemappingReader.h(4.36 KB)
📄 SystemUtils.h(1.02 KB)
📄 TarWriter.h(941 B)
📄 TargetOpcodes.def(22.01 KB)
📄 TargetParser.h(4.08 KB)
📄 TargetRegistry.h(46.87 KB)
📄 TargetSelect.h(6.2 KB)
📄 TaskQueue.h(4.24 KB)
📄 ThreadLocal.h(2.08 KB)
📄 ThreadPool.h(3.44 KB)
📄 Threading.h(10.62 KB)
📄 TimeProfiler.h(3.46 KB)
📄 Timer.h(8.93 KB)
📄 ToolOutputFile.h(2.24 KB)
📄 TrailingObjects.h(15.19 KB)
📄 TrigramIndex.h(2.84 KB)
📄 TypeName.h(2.13 KB)
📄 TypeSize.h(8.53 KB)
📄 Unicode.h(2.5 KB)
📄 UnicodeCharRanges.h(3.27 KB)
📄 Valgrind.h(1.16 KB)
📄 VersionTuple.h(5.22 KB)
📄 VirtualFileSystem.h(28.28 KB)
📄 Watchdog.h(1.15 KB)
📄 Win64EH.h(4.82 KB)
📁 Windows
📄 WindowsError.h(541 B)
📄 WithColor.h(4.64 KB)
📄 X86DisassemblerDecoderCommon.h(29.39 KB)
📄 X86TargetParser.def(8.21 KB)
📄 X86TargetParser.h(3.57 KB)
📄 YAMLParser.h(16.29 KB)
📄 YAMLTraits.h(67.62 KB)
📄 circular_raw_ostream.h(4.97 KB)
📄 raw_os_ostream.h(1.29 KB)
📄 raw_ostream.h(20.82 KB)
📄 raw_sha1_ostream.h(1.29 KB)
📄 thread.h(1.33 KB)
📄 type_traits.h(6.75 KB)
📄 xxhash.h(1.92 KB)

Editing: SMTAPI.h

//===- SMTAPI.h -------------------------------------------------*- C++ -*-===//
//
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
// See https://llvm.org/LICENSE.txt for license information.
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
//
//===----------------------------------------------------------------------===//
//
//  This file defines a SMT generic Solver API, which will be the base class
//  for every SMT solver specific class.
//
//===----------------------------------------------------------------------===//

#ifndef LLVM_SUPPORT_SMTAPI_H
#define LLVM_SUPPORT_SMTAPI_H

#include "llvm/ADT/APFloat.h"
#include "llvm/ADT/APSInt.h"
#include "llvm/ADT/FoldingSet.h"
#include "llvm/Support/raw_ostream.h"
#include <memory>

namespace llvm {

/// Generic base class for SMT sorts
class SMTSort {
public:
  SMTSort() = default;
  virtual ~SMTSort() = default;

/// Returns true if the sort is a bitvector, calls isBitvectorSortImpl().
  virtual bool isBitvectorSort() const { return isBitvectorSortImpl(); }

/// Returns true if the sort is a floating-point, calls isFloatSortImpl().
  virtual bool isFloatSort() const { return isFloatSortImpl(); }

/// Returns true if the sort is a boolean, calls isBooleanSortImpl().
  virtual bool isBooleanSort() const { return isBooleanSortImpl(); }

/// Returns the bitvector size, fails if the sort is not a bitvector
  /// Calls getBitvectorSortSizeImpl().
  virtual unsigned getBitvectorSortSize() const {
    assert(isBitvectorSort() && "Not a bitvector sort!");
    unsigned Size = getBitvectorSortSizeImpl();
    assert(Size && "Size is zero!");
    return Size;
  };

/// Returns the floating-point size, fails if the sort is not a floating-point
  /// Calls getFloatSortSizeImpl().
  virtual unsigned getFloatSortSize() const {
    assert(isFloatSort() && "Not a floating-point sort!");
    unsigned Size = getFloatSortSizeImpl();
    assert(Size && "Size is zero!");
    return Size;
  };

virtual void Profile(llvm::FoldingSetNodeID &ID) const = 0;

bool operator<(const SMTSort &Other) const {
    llvm::FoldingSetNodeID ID1, ID2;
    Profile(ID1);
    Other.Profile(ID2);
    return ID1 < ID2;
  }

friend bool operator==(SMTSort const &LHS, SMTSort const &RHS) {
    return LHS.equal_to(RHS);
  }

virtual void print(raw_ostream &OS) const = 0;

LLVM_DUMP_METHOD void dump() const;

protected:
  /// Query the SMT solver and returns true if two sorts are equal (same kind
  /// and bit width). This does not check if the two sorts are the same objects.
  virtual bool equal_to(SMTSort const &other) const = 0;

/// Query the SMT solver and checks if a sort is bitvector.
  virtual bool isBitvectorSortImpl() const = 0;

/// Query the SMT solver and checks if a sort is floating-point.
  virtual bool isFloatSortImpl() const = 0;

/// Query the SMT solver and checks if a sort is boolean.
  virtual bool isBooleanSortImpl() const = 0;

/// Query the SMT solver and returns the sort bit width.
  virtual unsigned getBitvectorSortSizeImpl() const = 0;

/// Query the SMT solver and returns the sort bit width.
  virtual unsigned getFloatSortSizeImpl() const = 0;
};

/// Shared pointer for SMTSorts, used by SMTSolver API.
using SMTSortRef = const SMTSort *;

/// Generic base class for SMT exprs
class SMTExpr {
public:
  SMTExpr() = default;
  virtual ~SMTExpr() = default;

bool operator<(const SMTExpr &Other) const {
    llvm::FoldingSetNodeID ID1, ID2;
    Profile(ID1);
    Other.Profile(ID2);
    return ID1 < ID2;
  }

virtual void Profile(llvm::FoldingSetNodeID &ID) const = 0;

friend bool operator==(SMTExpr const &LHS, SMTExpr const &RHS) {
    return LHS.equal_to(RHS);
  }

virtual void print(raw_ostream &OS) const = 0;

LLVM_DUMP_METHOD void dump() const;

/// Shared pointer for SMTExprs, used by SMTSolver API.
using SMTExprRef = const SMTExpr *;

/// Generic base class for SMT Solvers
///
/// This class is responsible for wrapping all sorts and expression generation,
/// through the mk* methods. It also provides methods to create SMT expressions
/// straight from clang's AST, through the from* methods.
class SMTSolver {
public:
  SMTSolver() = default;
  virtual ~SMTSolver() = default;

LLVM_DUMP_METHOD void dump() const;

// Returns an appropriate floating-point sort for the given bitwidth.
  SMTSortRef getFloatSort(unsigned BitWidth) {
    switch (BitWidth) {
    case 16:
      return getFloat16Sort();
    case 32:
      return getFloat32Sort();
    case 64:
      return getFloat64Sort();
    case 128:
      return getFloat128Sort();
    default:;
    }
    llvm_unreachable("Unsupported floating-point bitwidth!");
  }

// Returns a boolean sort.
  virtual SMTSortRef getBoolSort() = 0;

// Returns an appropriate bitvector sort for the given bitwidth.
  virtual SMTSortRef getBitvectorSort(const unsigned BitWidth) = 0;

// Returns a floating-point sort of width 16
  virtual SMTSortRef getFloat16Sort() = 0;

// Returns a floating-point sort of width 32
  virtual SMTSortRef getFloat32Sort() = 0;

// Returns a floating-point sort of width 64
  virtual SMTSortRef getFloat64Sort() = 0;

// Returns a floating-point sort of width 128
  virtual SMTSortRef getFloat128Sort() = 0;

// Returns an appropriate sort for the given AST.
  virtual SMTSortRef getSort(const SMTExprRef &AST) = 0;

/// Given a constraint, adds it to the solver
  virtual void addConstraint(const SMTExprRef &Exp) const = 0;

/// Creates a bitvector addition operation
  virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a bitvector subtraction operation
  virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a bitvector multiplication operation
  virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a bitvector signed modulus operation
  virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a bitvector unsigned modulus operation
  virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a bitvector signed division operation
  virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a bitvector unsigned division operation
  virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a bitvector logical shift left operation
  virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a bitvector arithmetic shift right operation
  virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a bitvector logical shift right operation
  virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a bitvector negation operation
  virtual SMTExprRef mkBVNeg(const SMTExprRef &Exp) = 0;

/// Creates a bitvector not operation
  virtual SMTExprRef mkBVNot(const SMTExprRef &Exp) = 0;

/// Creates a bitvector xor operation
  virtual SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a bitvector or operation
  virtual SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a bitvector and operation
  virtual SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a bitvector unsigned less-than operation
  virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a bitvector signed less-than operation
  virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a bitvector unsigned greater-than operation
  virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a bitvector signed greater-than operation
  virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a bitvector unsigned less-equal-than operation
  virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a bitvector signed less-equal-than operation
  virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a bitvector unsigned greater-equal-than operation
  virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a bitvector signed greater-equal-than operation
  virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a boolean not operation
  virtual SMTExprRef mkNot(const SMTExprRef &Exp) = 0;

/// Creates a boolean equality operation
  virtual SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a boolean and operation
  virtual SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a boolean or operation
  virtual SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a boolean ite operation
  virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
                           const SMTExprRef &F) = 0;

/// Creates a bitvector sign extension operation
  virtual SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) = 0;

/// Creates a bitvector zero extension operation
  virtual SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) = 0;

/// Creates a bitvector extract operation
  virtual SMTExprRef mkBVExtract(unsigned High, unsigned Low,
                                 const SMTExprRef &Exp) = 0;

/// Creates a bitvector concat operation
  virtual SMTExprRef mkBVConcat(const SMTExprRef &LHS,
                                const SMTExprRef &RHS) = 0;

/// Creates a predicate that checks for overflow in a bitvector addition
  /// operation
  virtual SMTExprRef mkBVAddNoOverflow(const SMTExprRef &LHS,
                                       const SMTExprRef &RHS,
                                       bool isSigned) = 0;

/// Creates a predicate that checks for underflow in a signed bitvector
  /// addition operation
  virtual SMTExprRef mkBVAddNoUnderflow(const SMTExprRef &LHS,
                                        const SMTExprRef &RHS) = 0;

/// Creates a predicate that checks for overflow in a signed bitvector
  /// subtraction operation
  virtual SMTExprRef mkBVSubNoOverflow(const SMTExprRef &LHS,
                                       const SMTExprRef &RHS) = 0;

/// Creates a predicate that checks for underflow in a bitvector subtraction
  /// operation
  virtual SMTExprRef mkBVSubNoUnderflow(const SMTExprRef &LHS,
                                        const SMTExprRef &RHS,
                                        bool isSigned) = 0;

/// Creates a predicate that checks for overflow in a signed bitvector
  /// division/modulus operation
  virtual SMTExprRef mkBVSDivNoOverflow(const SMTExprRef &LHS,
                                        const SMTExprRef &RHS) = 0;

/// Creates a predicate that checks for overflow in a bitvector negation
  /// operation
  virtual SMTExprRef mkBVNegNoOverflow(const SMTExprRef &Exp) = 0;

/// Creates a predicate that checks for overflow in a bitvector multiplication
  /// operation
  virtual SMTExprRef mkBVMulNoOverflow(const SMTExprRef &LHS,
                                       const SMTExprRef &RHS,
                                       bool isSigned) = 0;

/// Creates a predicate that checks for underflow in a signed bitvector
  /// multiplication operation
  virtual SMTExprRef mkBVMulNoUnderflow(const SMTExprRef &LHS,
                                        const SMTExprRef &RHS) = 0;

/// Creates a floating-point negation operation
  virtual SMTExprRef mkFPNeg(const SMTExprRef &Exp) = 0;

/// Creates a floating-point isInfinite operation
  virtual SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) = 0;

/// Creates a floating-point isNaN operation
  virtual SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) = 0;

/// Creates a floating-point isNormal operation
  virtual SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) = 0;

/// Creates a floating-point isZero operation
  virtual SMTExprRef mkFPIsZero(const SMTExprRef &Exp) = 0;

/// Creates a floating-point multiplication operation
  virtual SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a floating-point division operation
  virtual SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a floating-point remainder operation
  virtual SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a floating-point addition operation
  virtual SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a floating-point subtraction operation
  virtual SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a floating-point less-than operation
  virtual SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a floating-point greater-than operation
  virtual SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a floating-point less-than-or-equal operation
  virtual SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a floating-point greater-than-or-equal operation
  virtual SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;

/// Creates a floating-point equality operation
  virtual SMTExprRef mkFPEqual(const SMTExprRef &LHS,
                               const SMTExprRef &RHS) = 0;

/// Creates a floating-point conversion from floatint-point to floating-point
  /// operation
  virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) = 0;

/// Creates a floating-point conversion from signed bitvector to
  /// floatint-point operation
  virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From,
                               const SMTSortRef &To) = 0;

/// Creates a floating-point conversion from unsigned bitvector to
  /// floatint-point operation
  virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From,
                               const SMTSortRef &To) = 0;

/// Creates a floating-point conversion from floatint-point to signed
  /// bitvector operation
  virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) = 0;

/// Creates a floating-point conversion from floatint-point to unsigned
  /// bitvector operation
  virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) = 0;

/// Creates a new symbol, given a name and a sort
  virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) = 0;

// Returns an appropriate floating-point rounding mode.
  virtual SMTExprRef getFloatRoundingMode() = 0;

// If the a model is available, returns the value of a given bitvector symbol
  virtual llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth,
                                    bool isUnsigned) = 0;

// If the a model is available, returns the value of a given boolean symbol
  virtual bool getBoolean(const SMTExprRef &Exp) = 0;

/// Constructs an SMTExprRef from a boolean.
  virtual SMTExprRef mkBoolean(const bool b) = 0;

/// Constructs an SMTExprRef from a finite APFloat.
  virtual SMTExprRef mkFloat(const llvm::APFloat Float) = 0;

/// Constructs an SMTExprRef from an APSInt and its bit width
  virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) = 0;

/// Given an expression, extract the value of this operand in the model.
  virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) = 0;

/// Given an expression extract the value of this operand in the model.
  virtual bool getInterpretation(const SMTExprRef &Exp,
                                 llvm::APFloat &Float) = 0;

/// Check if the constraints are satisfiable
  virtual Optional<bool> check() const = 0;

/// Push the current solver state
  virtual void push() = 0;

/// Pop the previous solver state
  virtual void pop(unsigned NumStates = 1) = 0;

/// Reset the solver and remove all constraints.
  virtual void reset() = 0;

/// Checks if the solver supports floating-points.
  virtual bool isFPSupported() = 0;

virtual void print(raw_ostream &OS) const = 0;
};

/// Shared pointer for SMTSolvers.
using SMTSolverRef = std::shared_ptr<SMTSolver>;

/// Convenience method to create and Z3Solver object
SMTSolverRef CreateZ3Solver();

} // namespace llvm

#endif

003 File Manager

Editing: SMTAPI.h

Upload File

Create Folder