llvm/llvm/include/llvm/Support/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 { … };

/// Shared pointer for SMTSorts, used by SMTSolver API.
SMTSortRef;

/// Generic base class for SMT exprs
class SMTExpr { … };

class SMTSolverStatistics { … };

/// Shared pointer for SMTExprs, used by SMTSolver API.
SMTExprRef;

/// 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 { … };

/// Shared pointer for SMTSolvers.
SMTSolverRef;

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

} // namespace llvm

#endif