z3Solver.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_Z3SOLVER_H
#define TRITON_Z3SOLVER_H
 
#include <string>
#include <unordered_map>
#include <vector>
#include <z3++.h>
#include <z3_api.h>
 
#include <triton/ast.hpp>
#include <triton/dllexport.hpp>
#include <triton/solverEnums.hpp>
#include <triton/solverInterface.hpp>
#include <triton/solverModel.hpp>
#include <triton/tritonTypes.hpp>
 
 
 
namespace triton {
  namespace engines {
    namespace solver {
 
      class Z3Solver : public SolverInterface {
          static z3::expr mk_or(z3::expr_vector args);
 
        private:
          triton::uint32 timeout;
 
          triton::uint32 memoryLimit;
 
          void writeBackStatus(z3::solver& solver, z3::check_result res, triton::engines::solver::status_e* status) const;
 
        public:
          TRITON_EXPORT Z3Solver();
 
 
          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 triton::ast::SharedAbstractNode simplify(const triton::ast::SharedAbstractNode& node) const;
 
          TRITON_EXPORT triton::uint512 evaluate(const triton::ast::SharedAbstractNode& node) const;
 
          TRITON_EXPORT std::string getName(void) const;
 
          TRITON_EXPORT void setTimeout(triton::uint32 ms);
 
          TRITON_EXPORT void setMemoryLimit(triton::uint32 mem);
      };
 
    };
  };
};
 
#endif /* TRITON_Z3SOLVER_H */