tritonToBitwuzla.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_TRITONTOBITWUZLA_H
#define TRITON_TRITONTOBITWUZLA_H
 
#include <map>
#include <unordered_map>
 
extern "C" {
#include <bitwuzla/c/bitwuzla.h>
}
 
#include <triton/ast.hpp>
#include <triton/dllexport.hpp>
#include <triton/tritonTypes.hpp>
 
 
 
namespace triton {
  namespace ast {
 
    class TritonToBitwuzla {
      public:
        TRITON_EXPORT TritonToBitwuzla(bool eval=false);
 
        TRITON_EXPORT ~TritonToBitwuzla();
 
        TRITON_EXPORT BitwuzlaTerm convert(const SharedAbstractNode& node, Bitwuzla* bzla);
 
        TRITON_EXPORT const std::unordered_map<BitwuzlaTerm, triton::engines::symbolic::SharedSymbolicVariable>& getVariables(void) const;
 
        TRITON_EXPORT const std::map<size_t, BitwuzlaSort>& getBitvectorSorts(void) const;
 
      private:
        std::unordered_map<SharedAbstractNode, BitwuzlaTerm> translatedNodes;
 
        std::unordered_map<BitwuzlaTerm, triton::engines::symbolic::SharedSymbolicVariable> variables;
 
        std::unordered_map<std::string, triton::ast::SharedAbstractNode> symbols;
 
        std::map<size_t, BitwuzlaSort> bvSorts;
 
        bool isEval;
 
        BitwuzlaTerm translate(const SharedAbstractNode& node, Bitwuzla* bzla);
    };
 
  };
};
 
#endif /* TRITON_TRITONTOBITWUZLA_H */