solverEngine.hpp

Go to the documentation of this file.

 
/*
**  Copyright (C) - Triton
**
**  This program is under the terms of the Apache License 2.0.
*/
 
#ifndef TRITON_SOLVERENGINE_HPP
#define TRITON_SOLVERENGINE_HPP
 
#include <iostream>
#include <memory>
#include <unordered_map>
#include <vector>
 
#include <triton/ast.hpp>
#include <triton/config.hpp>
#include <triton/dllexport.hpp>
#include <triton/solverEnums.hpp>
#include <triton/solverInterface.hpp>
#include <triton/solverModel.hpp>
#include <triton/tritonTypes.hpp>
#ifdef TRITON_Z3_INTERFACE
  #include <triton/z3Solver.hpp>
#endif
#ifdef TRITON_BITWUZLA_INTERFACE
  #include <triton/bitwuzlaSolver.hpp>
#endif
 
 
 
namespace triton {
  namespace engines {
    namespace solver {
      class SolverEngine {
        protected:
          triton::engines::solver::solver_e kind;
 
          std::unique_ptr<triton::engines::solver::SolverInterface> solver;
 
        public:
          TRITON_EXPORT SolverEngine();
 
          TRITON_EXPORT triton::engines::solver::solver_e getSolver(void) const;
 
          TRITON_EXPORT const triton::engines::solver::SolverInterface* getSolverInstance(void) const;
 
          TRITON_EXPORT void setSolver(triton::engines::solver::solver_e kind);
 
          TRITON_EXPORT void setCustomSolver(triton::engines::solver::SolverInterface* customSolver);
 
          TRITON_EXPORT bool isValid(void) const;
 
 
          TRITON_EXPORT std::unordered_map<triton::usize, SolverModel> getModel(const triton::ast::SharedAbstractNode& node, triton::engines::solver::status_e* status = nullptr, triton::uint32 timeout = 0, triton::uint32* solvingTime = nullptr) const;
 
 
          TRITON_EXPORT std::vector<std::unordered_map<triton::usize, SolverModel>> getModels(const triton::ast::SharedAbstractNode& node, triton::uint32 limit, triton::engines::solver::status_e* status = nullptr, triton::uint32 timeout = 0, triton::uint32* solvingTime = nullptr) const;
 
          TRITON_EXPORT bool isSat(const triton::ast::SharedAbstractNode& node, triton::engines::solver::status_e* status = nullptr, triton::uint32 timeout = 0, triton::uint32* solvingTime = nullptr) const;
 
          TRITON_EXPORT std::string getName(void) const;
 
          TRITON_EXPORT void setTimeout(triton::uint32 ms);
 
          TRITON_EXPORT void setMemoryLimit(triton::uint32 mem);
      };
 
    };
  };
};
 
#endif /* TRITON_SOLVERINTERFACE_HPP */