//== SMTConstraintManager.h -------------------------------------*- C++ -*--==//
//
//                     The LLVM Compiler Infrastructure
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
//
//  This file defines a SMT generic API, which will be the base class for
//  every SMT solver specific class.
//
//===----------------------------------------------------------------------===//

#ifndef LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H
#define LLVM_CLANG_STATICANALYZER_CORE_PATHSENSITIVE_SMTCONSTRAINTMANAGER_H

#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h"

namespace clang {
namespace ento {

class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
  SMTSolverRef &Solver;

public:
  SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB,
                       SMTSolverRef &S)
      : SimpleConstraintManager(SE, SB), Solver(S) {}
  virtual ~SMTConstraintManager() = default;

  //===------------------------------------------------------------------===//
  // Implementation for interface from SimpleConstraintManager.
  //===------------------------------------------------------------------===//

  ProgramStateRef assumeSym(ProgramStateRef state, SymbolRef Sym,
                            bool Assumption) override;

  ProgramStateRef assumeSymInclusiveRange(ProgramStateRef State, SymbolRef Sym,
                                          const llvm::APSInt &From,
                                          const llvm::APSInt &To,
                                          bool InRange) override;

  ProgramStateRef assumeSymUnsupported(ProgramStateRef State, SymbolRef Sym,
                                       bool Assumption) override;

  //===------------------------------------------------------------------===//
  // Implementation for interface from ConstraintManager.
  //===------------------------------------------------------------------===//

  ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;

  const llvm::APSInt *getSymVal(ProgramStateRef State,
                                SymbolRef Sym) const override;

  /// Dumps SMT formula
  LLVM_DUMP_METHOD void dump() const { Solver->dump(); }

protected:
  // Check whether a new model is satisfiable, and update the program state.
  virtual ProgramStateRef assumeExpr(ProgramStateRef State, SymbolRef Sym,
                                     const SMTExprRef &Exp) = 0;

  /// Given a program state, construct the logical conjunction and add it to
  /// the solver
  virtual void addStateConstraints(ProgramStateRef State) const = 0;

  // Generate and check a Z3 model, using the given constraint.
  ConditionTruthVal checkModel(ProgramStateRef State,
                               const SMTExprRef &Exp) const;
}; // end class SMTConstraintManager

} // namespace ento
} // namespace clang

#endif