#include <smt.hpp>

Inheritance diagram for ilasynth::Z3FixedpointAdapter:

Public Member Functions
	Z3FixedpointAdapter (z3::context &c, const std::string &suffix)

	~Z3FixedpointAdapter ()

Public Member Functions inherited from ilasynth::Z3ExprAdapter
	Z3ExprAdapter (z3::context &c, const std::string &suffix)

	Z3ExprAdapter (z3::context &c, const char *suffix)

virtual	~Z3ExprAdapter ()

virtual void	operator() (const Node *n)

z3::expr	getExpr (const Node *n)

z3::expr	getCnst (const Node *n)

z3::context &	ctx () const

void	clear ()

std::string	extractNumeralString (z3::model &m, const Node *r)

int	getNumeralInt (z3::model &m, const Node *r)

mp_int_t	getNumeralCppInt (z3::model &m, const Node *r)

bool	getBoolValue (z3::model &m, const Node *r)

template<typename T >
bool	getChoiceBool (z3::model &m, const ChoiceExpr< T > *op, int i)

void	setNameSuffix (const std::string &ns)

const std::string &	getNameSuffix () const

Additional Inherited Members
Public Types inherited from ilasynth::Z3ExprAdapter
typedef std::unordered_map< const Node *, z3::expr, decltype(&nodeHash), decltype(&nodeEqual)>	expr_map_t

Public Attributes inherited from ilasynth::Z3ExprAdapter
bool	simplify

Protected Member Functions inherited from ilasynth::Z3ExprAdapter
z3::expr	_getArg (const expr_map_t &m, const Node *n, int i)

z3::expr	getArgExpr (const Node *n, int i)

z3::expr	getArgCnst (const Node *n, int i)

void	_populateExprMap (const Node *n)

void	_populateCnstMap (const Node *n)

virtual z3::expr	getBoolVarExpr (const BoolVar *bv)

virtual z3::expr	getBoolOpExpr (const BoolOp *op)

virtual z3::expr	getChoiceExpr (const BoolChoice *op)

virtual z3::expr	getBitvectorVarExpr (const BitvectorVar *bvv)

virtual z3::expr	getBvOpExpr (const BitvectorOp *op)

virtual z3::expr	getChoiceExpr (const BitvectorChoice *op)

virtual z3::expr	getBVInRangeExpr (const BVInRange *op)

virtual z3::expr	getBVInRangeCnst (const BVInRange *op)

virtual z3::expr	getMemVarExpr (const MemVar *mv)

virtual z3::expr	getMemOpExpr (const MemOp *mw)

virtual z3::expr	getChoiceExpr (const MemChoice *op)

virtual z3::expr	getFuncVarExpr (const FuncVar *fv)

Protected Attributes inherited from ilasynth::Z3ExprAdapter
expr_map_t	exprmap

expr_map_t	cnstmap

z3::context &	c

std::string	suffix

std::string	name_suffix
	Added to every name. More...

Constructor & Destructor Documentation

◆ Z3FixedpointAdapter()

ilasynth::Z3FixedpointAdapter::Z3FixedpointAdapter	(	z3::context &	c,
		const std::string &	suffix
	)

inline

ilasynth::Z3FixedpointAdapter::~Z3FixedpointAdapter ( )

inline

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