bitwuzlaSolver.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_BITWUZLASOLVER_H
#define TRITON_BITWUZLASOLVER_H
 
#include <chrono>
#include <string>
#include <unordered_map>
#include <vector>
 
extern "C" {
#include <bitwuzla/c/bitwuzla.h>
}
 
#include <triton/ast.hpp>
#include <triton/dllexport.hpp>
#include <triton/solverEnums.hpp>
#include <triton/solverInterface.hpp>
#include <triton/solverModel.hpp>
#include <triton/symbolicExpression.hpp>
#include <triton/tritonTypes.hpp>
 
 
 
namespace triton {
  namespace engines {
    namespace solver {
 
      class BitwuzlaSolver : public SolverInterface {
        private:
          triton::uint512 fromBvalueToUint512(const char* value) const;
 
          struct SolverParams {
            SolverParams(int64_t timeout, size_t memory_limit): timeout(timeout), memory_limit(memory_limit) {
            }
 
            std::chrono::time_point<std::chrono::system_clock> start = std::chrono::system_clock::now();    
            triton::engines::solver::status_e status = triton::engines::solver::UNKNOWN;                    
            int64_t timeout;                                                                                
            size_t  memory_limit;                                                                           
            int64_t last_mem_check = -1;                                                                    
          };
 
          triton::uint32 timeout;
 
          triton::uint32 memoryLimit;
 
        public:
          TRITON_EXPORT BitwuzlaSolver();
 
 
          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::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);
 
          static int32_t terminateCallback(void* state);
 
          static void abortCallback(const char* msg);
      };
 
    };
  };
};
 
#endif /* TRITON_BITWUZLASOLVER_H */