tvm::arith::Z3Prover Class Reference

#include <analyzer.h>

Collaboration diagram for tvm::arith::Z3Prover:

Public Member Functions
void	Bind (const Var &var, const Range &new_range, bool allow_override=false)
	Update binding of var to a new expression.
void	Bind (const Var &var, const PrimExpr &expr, bool allow_override=false)
	Update binding of var to a new expression.
bool	IsEnabled () const
	Whether the Z3 backend is compiled into this build (USE_Z3=ON).
bool	CanProve (const PrimExpr &expr)
	Whether can we prove expr is always true.
std::function< void()>	EnterConstraint (const PrimExpr &constraint, bool is_assume=false)
	Update the internal state to enter constraint.
ffi::String	GetSMTLIB2 (const ffi::Optional< PrimExpr > expr)
	Get the SMTLIB2 representation of the current context.
ffi::String	GetStats ()
	Get statistics about Z3 prover.
void	SetTimeoutMs (unsigned timeout_ms)
	Set timeout in milliseconds for Z3 prover.
void	SetRLimit (unsigned rlimit)
	Set resource limitation for Z3 prover.
ffi::String	GetModel (const PrimExpr &expr)
	Get the Z3 model for the given expression if satisfiable.
int64_t	CountSatisfyingValues (const Var &var, int64_t max_count=2048, int64_t min_consecutive=1)
	Count the number of integer values that satisfy the current constraints.

Friends
class	AnalyzerObj
class	Analyzer

Member Function Documentation

Bind() [1/2]

void tvm::arith::Z3Prover::Bind	(	const Var &	var,
		const PrimExpr &	expr,
		bool	allow_override = false
	)

Update binding of var to a new expression.

Parameters

var	The variable of interest.
expr	The bound expression.
allow_override	whether we allow override of existing information.

Bind() [2/2]

void tvm::arith::Z3Prover::Bind	(	const Var &	var,
		const Range &	new_range,
		bool	allow_override = false
	)

Update binding of var to a new expression.

Parameters

var	The variable of interest.
new_range	The range of allowed values for this var.
allow_override	whether we allow override of existing information.

CanProve()

bool tvm::arith::Z3Prover::CanProve

(

const PrimExpr &

expr

)

Whether can we prove expr is always true.

Parameters

expr	The expression.

Returns

Whether we can prove it.

CountSatisfyingValues()

int64_t tvm::arith::Z3Prover::CountSatisfyingValues	(	const Var &	var,
		int64_t	max_count = 2048,
		int64_t	min_consecutive = 1
	)

Count the number of integer values that satisfy the current constraints.

This method uses Z3's model enumeration to count how many distinct values of the given variable satisfy all current constraints.

Parameters

var	The variable to count satisfying values for.
max_count	Maximum number of solutions to enumerate.
min_consecutive	Minimum consecutive count requirement.

Returns

The number of distinct values that satisfy the constraints, or a negative error code.

EnterConstraint()

std::function< void()> tvm::arith::Z3Prover::EnterConstraint	(	const PrimExpr &	constraint,
		bool	is_assume = false
	)

Update the internal state to enter constraint.

Parameters

constraint	A constraint expression.
is_assume	Whether the constraint comes from an assumption.

Returns

an exit function that must be called to cleanup the constraint can be nullptr.

GetModel()

ffi::String tvm::arith::Z3Prover::GetModel

(

const PrimExpr &

expr

)

Get the Z3 model for the given expression if satisfiable.

Parameters

expr	The expression to get the model for.

Returns

The model as a string.

GetSMTLIB2()

ffi::String tvm::arith::Z3Prover::GetSMTLIB2

(

const ffi::Optional< PrimExpr >

expr

)

Get the SMTLIB2 representation of the current context.

Parameters

expr	The optional expression to check.

Returns

The SMTLIB2 string.

GetStats()

ffi::String tvm::arith::Z3Prover::GetStats

(

)

Get statistics about Z3 prover.

Returns

The statistics string.

IsEnabled()

bool tvm::arith::Z3Prover::IsEnabled

(

)

const

Whether the Z3 backend is compiled into this build (USE_Z3=ON).

Returns

true if the real Z3 prover is available, false for the stub.

SetRLimit()

void tvm::arith::Z3Prover::SetRLimit

(

unsigned

rlimit

)

Set resource limitation for Z3 prover.

Parameters

rlimit

the resource limitation.

SetTimeoutMs()

void tvm::arith::Z3Prover::SetTimeoutMs

(

unsigned

timeout_ms

)

Set timeout in milliseconds for Z3 prover.

Parameters

timeout_ms

The timeout in milliseconds.

Friends And Related Symbol Documentation

Analyzer

friend class Analyzer

friend

AnalyzerObj

friend class AnalyzerObj

friend

---

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

• include/tvm/arith/analyzer.h