ilasynth::Z3ExprRewritingAdapter Class Reference

#include <smt.hpp>

Inheritance diagram for ilasynth::Z3ExprRewritingAdapter:

Public Member Functions
	Z3ExprRewritingAdapter (z3::context &c, const DistInput *di, const std::string &suffix)
	Z3ExprRewritingAdapter (z3::context &c, const DistInput *di, const char *suffix)
	~Z3ExprRewritingAdapter ()
z3::expr	getIOCnst (const Node *n, const py::object &result)
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

Protected Member Functions
virtual z3::expr	getBoolVarExpr (const BoolVar *bv)
virtual z3::expr	getBitvectorVarExpr (const BitvectorVar *bvv)
virtual z3::expr	getMemVarExpr (const MemVar *mv)
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	getBoolOpExpr (const BoolOp *op)
virtual z3::expr	getChoiceExpr (const BoolChoice *op)
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	getMemOpExpr (const MemOp *mw)
virtual z3::expr	getChoiceExpr (const MemChoice *op)
virtual z3::expr	getFuncVarExpr (const FuncVar *fv)

Protected Attributes
const DistInput *	distInp
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...

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

Constructor & Destructor Documentation

Z3ExprRewritingAdapter() [1/2]

ilasynth::Z3ExprRewritingAdapter::Z3ExprRewritingAdapter	(	z3::context &	c,
		const DistInput *	di,
		const std::string &	suffix
	)

Z3ExprRewritingAdapter() [2/2]

ilasynth::Z3ExprRewritingAdapter::Z3ExprRewritingAdapter	(	z3::context &	c,
		const DistInput *	di,
		const char *	suffix
	)

~Z3ExprRewritingAdapter()

ilasynth::Z3ExprRewritingAdapter::~Z3ExprRewritingAdapter

(

)

Member Function Documentation

getBitvectorVarExpr()

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

protectedvirtual

Reimplemented from ilasynth::Z3ExprAdapter.

getBoolVarExpr()

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

protectedvirtual

Reimplemented from ilasynth::Z3ExprAdapter.

getIOCnst()

z3::expr ilasynth::Z3ExprRewritingAdapter::getIOCnst	(	const Node *	n,
		const py::object &	result
	)

getMemVarExpr()

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

protectedvirtual

Reimplemented from ilasynth::Z3ExprAdapter.

Member Data Documentation

distInp

const DistInput* ilasynth::Z3ExprRewritingAdapter::distInp

protected

---

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

• smt.hpp