libTriton  version 0.6 build 1389
Public Member Functions | List of all members
triton::engines::solver::SolverInterface Interface Referenceabstract

This interface is used to interface with solvers. More...

#include <solverInterface.hpp>

Inheritance diagram for triton::engines::solver::SolverInterface:

Public Member Functions

virtual TRITON_EXPORT ~SolverInterface ()
 Destructor.
 
virtual TRITON_EXPORT std::map< triton::uint32, SolverModelgetModel (const triton::ast::SharedAbstractNode &node) const =0
 Computes and returns a model from a symbolic constraint. More...
 
virtual TRITON_EXPORT std::list< std::map< triton::uint32, SolverModel > > getModels (const triton::ast::SharedAbstractNode &node, triton::uint32 limit) const =0
 Computes and returns several models from a symbolic constraint. The limit is the max number of models returned. More...
 
virtual TRITON_EXPORT bool isSat (const triton::ast::SharedAbstractNode &node) const =0
 Returns true if an expression is satisfiable.
 
virtual TRITON_EXPORT std::string getName (void) const =0
 Returns the name of the solver.
 

Detailed Description

This interface is used to interface with solvers.

Definition at line 44 of file solverInterface.hpp.

Member Function Documentation

◆ getModel()

virtual TRITON_EXPORT std::map<triton::uint32, SolverModel> triton::engines::solver::SolverInterface::getModel ( const triton::ast::SharedAbstractNode node) const
pure virtual

Computes and returns a model from a symbolic constraint.

map of symbolic variable id -> model

item1: symbolic variable id
item2: model

Implemented in triton::engines::solver::Z3Solver.

◆ getModels()

virtual TRITON_EXPORT std::list<std::map<triton::uint32, SolverModel> > triton::engines::solver::SolverInterface::getModels ( const triton::ast::SharedAbstractNode node,
triton::uint32  limit 
) const
pure virtual

Computes and returns several models from a symbolic constraint. The limit is the max number of models returned.

list of map of symbolic variable id -> model

item1: symbolic variable id
item2: model

Implemented in triton::engines::solver::Z3Solver.


The documentation for this interface was generated from the following file: