Class AnalyzerObj#
Defined in File analyzer.h
Inheritance Relationships#
Base Type#
public ffi::Object
Class Documentation#
-
class AnalyzerObj : public ffi::Object#
Coordinated symbolic analyses over an explicitly synchronized premise environment.
Queries may update caches, solver state, and statistics, but do not append persistent premises. Proof methods are conservative: false means not proved. Sub-analyzers borrow their owner and must not outlive it. This mutable object must not be queried or synchronized concurrently from multiple threads.
Public Functions
-
AnalyzerObj()#
Construct an analyzer with no accepted premises and default query settings.
-
void SetZ3DefaultFallback(bool enabled)#
Set whether DEFAULT-strength queries try Z3 after native analysis fails.
Enabled by default. This setting is local to the analyzer and preserved by Clone. Stronger proof queries and direct Z3 APIs are unaffected. Disabling the fallback does not clear accepted premises or existing solver state.
- Parameters:
enabled – Whether to allow the DEFAULT-strength Z3 fallback.
-
void SyncConstraintContext(const ConstraintContext &context)#
Synchronize all derived facts to the supplied premise environment.
Unchanged positions need no replay; recognized additive prefixes update incrementally, and other transitions clear and replay all backends. Query settings and cumulative rewrite counters survive synchronization.
The context must bind each Var identity at most once across value and range bindings. Unsupported or effectful premises may be ignored conservatively. Captured constraint and expression nodes must not be mutated through aliases. Appending to the caller’s context after this call takes effect only after a later synchronization. Synchronization during a query or another synchronization is rejected. If ingestion throws, discard this analyzer: partially applied backend state is not rolled back.
-
ConstraintContext GetConstraintContext() const#
Snapshot the accepted premise environment.
- Returns:
A context that can be extended independently. Constraint and expression nodes are shared and must not be mutated through aliases. Appending to this context does not update the analyzer until SyncConstraintContext is called.
-
bool CanProveGreaterEqual(const PrimExpr &expr, int64_t lower_bound)#
Attempt to prove expr >= lower_bound.
Bounds help distinguish truncating and floor division/remainder semantics.
Note
Analyzer will call into sub-analyzers to get the result.
- Parameters:
expr – The expression.
lower_bound – The lower bound.
- Returns:
True if proved; false if unknown or false.
-
bool CanProveLess(const PrimExpr &expr, int64_t upper_bound)#
Attempt to prove expr < upper_bound.
Bounds help distinguish truncating and floor division/remainder semantics.
Note
Analyzer will call into sub-analyzers to get the result.
- Parameters:
expr – The expression.
upper_bound – The upper bound.
- Returns:
True if proved; false if unknown or false.
-
bool CanProveEqual(const PrimExpr &lhs, const PrimExpr &rhs)#
Attempt to prove lhs == rhs.
Note
Analyzer will call into sub-analyzers to get the result.
- Parameters:
lhs – The input lhs.
rhs – The input rhs.
- Returns:
True if equality is proved; false does not establish inequality.
-
bool CanProveLessEqualThanSymbolicShapeValue(const PrimExpr &lhs, const PrimExpr &shape)#
Attempt to prove lhs <= a possibly symbolic shape.
By calling this function, the caller gives an extra hint that shape > 0, because it appeared in buffer shape.
This is useful to prove condition such as 32 <= 32 * n where the 32 * n is known to be a shape. Use this routine to reduce the symbolic comparisons in buffer compaction.
The underlying analyzer will use the kSymbolicBound proof.
- Parameters:
lhs – The input lhs.
shape – The symbolic shape.
- Returns:
True if proved using the caller’s positive-shape guarantee; false otherwise.
-
bool CanProve(const PrimExpr &cond, ProofStrength strength = ProofStrength::kDefault)#
Attempt to prove a condition under the current premises.
Note
Analyzer will call into sub-analyzers to get the result. Do not use strength beyond default in sub-analyzers and only use it in top-level predicate analysis. When built with Z3, all strengths try it after native analysis fails. SetZ3DefaultFallback(false) disables this fallback only for DEFAULT-strength queries. Z3’s existing resource limit and timeout apply; unknown means cannot prove.
- Parameters:
cond – The expression to be proved.
strength – Proof effort; kSymbolicBound additionally enables symbolic bound analysis.
- Returns:
True if proved; false includes unsupported or inconclusive queries.
-
PrimExpr Simplify(const PrimExpr &expr, int steps = 2)#
Simplify expr.
Note
Analyzer will call into sub-analyzers to get the result.
- Parameters:
expr – The expression to be simplified.
steps – Number of alternating rewrite/canonical passes after an initial canonical pass. The default of two runs canonical, rewrite, then canonical. Nonpositive values run only the initial canonical pass. Processing may stop early at a constant expression.
- Returns:
An equivalent expression under the current premises.
-
Analyzer Clone() const#
Copy accepted facts and query settings into an independent analyzer.
Backend state is independent: subsequent synchronization, simplification, and query settings on either analyzer do not affect the other. Premise and expression nodes are shared and must not be mutated through aliases. Query scratch, solver instances, and accumulated statistics are not copied. Copying an Analyzer handle alone instead shares the same mutable state.
- Returns:
A new analyzer with independent backend state and the same accepted premises.
Public Members
-
ConstIntBoundAnalyzer const_int_bound#
sub-analyzer: const integer bound
-
ModularSetAnalyzer modular_set#
sub-analyzer: modular set
-
RewriteSimplifier rewrite_simplify#
sub-analyzer rewrite simplify
-
CanonicalSimplifier canonical_simplify#
sub-analyzer canonical simplify
-
IntSetAnalyzer int_set#
sub-analyzer: int set
-
AnalyzerObj()#