Class Z3Prover

Class Z3Prover#

Class Documentation#

class Z3Prover#

Optional Z3-backed prover over the analyzer’s accepted premises.

Diagnostic and enumeration queries may propagate translation or solver errors. Their temporary assertions do not change the accepted premise environment.

Public Functions

bool IsEnabled() const#

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

Returns:

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

bool CanProve(const PrimExpr &expr)#

Attempt to prove that expr holds under the current premises.

Parameters:

expr – Boolean expression to prove.

Returns:

True only when proved; false for unsupported expressions, an unavailable backend, an inconclusive solver result, or a caught Z3 error. False is not a disproof.

ffi::String GetSMTLIB2(const ffi::Optional<PrimExpr> expr)#

Get the SMTLIB2 representation of the current context.

Parameters:

expr – Optional boolean expression whose negation is added as a proof query.

Returns:

The SMTLIB2 string, or a comment indicating that Z3 is disabled.

ffi::String GetStats()#

Get statistics about Z3 prover.

Returns:

The statistics string, or a comment indicating that Z3 is disabled.

void SetTimeoutMs(unsigned timeout_ms)#

Set timeout in milliseconds for Z3 prover.

Parameters:

timeout_ms – The timeout in milliseconds; zero disables the timeout. Ignored by the stub.

void SetRLimit(unsigned rlimit)#

Set resource limitation for Z3 prover.

Parameters:

rlimit – Z3 resource limit; zero disables it. Ignored by the stub.

ffi::String GetModel(const PrimExpr &expr)#

Get a counterexample model for a boolean expression.

Parameters:

expr – Boolean expression whose negation is checked under the current premises.

Returns:

A model satisfying the negation, or an empty string if no model is found (including an unknown result). The stub returns a comment indicating Z3 is disabled.

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.

Enumerates distinct values until the limit, unsatisfiability, or an inconclusive result. The count may be partial; it is not a proof of the domain cardinality.

Parameters:

  • var – The variable to count satisfying values for.

  • max_count – Maximum number of values to enumerate; nonpositive values enumerate none.

  • min_consecutive – Minimum size of each consecutive run in the enumerated values; nonpositive values disable this check. The check does not establish complete coverage.

Returns:

The enumerated count, -1 for an unsupported variable or disabled Z3, or -2 if a nonempty enumerated run is shorter than min_consecutive. Errors may propagate.