libTriton  version 1.0 build 1532
Public Member Functions | List of all members
triton::ast::TritonToBitwuzla Class Reference

Converts a Triton's AST to Bitwuzla's AST. More...

#include <tritonToBitwuzla.hpp>

Public Member Functions

TRITON_EXPORT TritonToBitwuzla (bool eval=false)
 Constructor. More...
 
TRITON_EXPORT ~TritonToBitwuzla ()
 Destructor. More...
 
TRITON_EXPORT const BitwuzlaTerm * convert (const SharedAbstractNode &node, Bitwuzla *bzla)
 Converts to Bitwuzla's AST. More...
 
TRITON_EXPORT const std::unordered_map< const BitwuzlaTerm *, triton::engines::symbolic::SharedSymbolicVariable > & getVariables (void) const
 Returns symbolic variables and its assosiated Bitwuzla terms to process the solver model. More...
 
TRITON_EXPORT const std::map< size_t, const BitwuzlaSort * > & getBitvectorSorts (void) const
 Returns bitvector sorts. More...
 

Detailed Description

Converts a Triton's AST to Bitwuzla's AST.

Definition at line 39 of file tritonToBitwuzla.hpp.

Constructor & Destructor Documentation

◆ TritonToBitwuzla()

triton::ast::TritonToBitwuzla::TritonToBitwuzla ( bool  eval = false)

Constructor.

Definition at line 22 of file tritonToBitwuzla.cpp.

◆ ~TritonToBitwuzla()

triton::ast::TritonToBitwuzla::~TritonToBitwuzla ( )

Destructor.

Definition at line 27 of file tritonToBitwuzla.cpp.

Member Function Documentation

◆ convert()

const BitwuzlaTerm * triton::ast::TritonToBitwuzla::convert ( const SharedAbstractNode node,
Bitwuzla *  bzla 
)

Converts to Bitwuzla's AST.

Definition at line 44 of file tritonToBitwuzla.cpp.

◆ getBitvectorSorts()

const std::map< size_t, const BitwuzlaSort * > & triton::ast::TritonToBitwuzla::getBitvectorSorts ( void  ) const

Returns bitvector sorts.

Definition at line 39 of file tritonToBitwuzla.cpp.

◆ getVariables()

const std::unordered_map< const BitwuzlaTerm *, triton::engines::symbolic::SharedSymbolicVariable > & triton::ast::TritonToBitwuzla::getVariables ( void  ) const

Returns symbolic variables and its assosiated Bitwuzla terms to process the solver model.

Definition at line 34 of file tritonToBitwuzla.cpp.


The documentation for this class was generated from the following files: