Struct Analyzer

#[repr(C)]
pub struct Analyzer { /* private fields */ }

Implementations

impl Analyzer

pub fn new() -> Self

A fresh analyzer that knows no facts (sym.Analyzer).

pub fn set_z3_default_fallback(&self, enabled: bool) -> Result<()>

Set whether default-strength queries try Z3 after native analysis fails.

Enabled by default and preserved by deep_clone. Stronger queries and direct Z3 APIs are unaffected. This does not clear accepted premises or solver state.

pub fn deep_clone(&self) -> Result<Self>

A copy of the analyzer and the facts it knows (sym.AnalyzerClone).

pub fn sync_constraint_context(&self, context: &ObjectRef) -> Result<()>

Synchronize with a sym.ConstraintContext captured at its current position.

The context is an opaque FFI object until typed constraint bindings are available. Switching contexts removes facts that are no longer present. Mutating the context after this call takes effect only after another synchronization.

pub fn const_int_bound(&self, expr: impl IntoExpr) -> Result<ConstIntBound>

The constant bounds of expr (sym.AnalyzerConstIntBound).

pub fn const_int_bound_is_bound(&self, var: impl Into<Var>) -> Result<bool>

Whether var has constant bounds recorded (sym.AnalyzerConstIntBoundIsBound).

pub fn modular_set(&self, expr: impl IntoExpr) -> Result<ModularSet>

The modular set coeff * x + base of expr (sym.AnalyzerModularSet).

pub fn int_set( &self, expr: impl IntoExpr, dom_map: Option<&Map<Var, IntSet>>, ) -> Result<IntSet>

The integer set expr covers, with the variables of dom_map over their sets (sym.AnalyzerIntSet).

pub fn simplify(&self, expr: impl IntoExpr, steps: i32) -> Result<Expr>

Simplify expr, alternating the rewrite and canonical simplifiers steps times (sym.AnalyzerSimplify).

pub fn rewrite_simplify(&self, expr: impl IntoExpr) -> Result<Expr>

Simplify expr by rewrite rules (sym.AnalyzerRewriteSimplify).

pub fn canonical_simplify(&self, expr: impl IntoExpr) -> Result<Expr>

Simplify expr into canonical form (sym.AnalyzerCanonicalSimplify).

pub fn rewrite_simplify_stats(&self) -> Result<RewriteSimplifierStats>

The counters of the rewrite simplifier (sym.AnalyzerGetRewriteSimplifyStats).

pub fn reset_rewrite_simplify_stats(&self) -> Result<()>

Zero the counters of the rewrite simplifier (sym.AnalyzerResetRewriteSimplifyStats).

pub fn set_maximum_rewrite_steps(&self, maximum: i64) -> Result<()>

Cap the rewrites of one rewrite simplification; 0 is no cap (sym.AnalyzerSetMaximumRewriteSteps).

pub fn can_prove( &self, expr: impl IntoExpr, strength: ProofStrength, ) -> Result<bool>

Whether expr is provably true (sym.AnalyzerCanProve).

pub fn can_prove_equal( &self, lhs: impl IntoExpr, rhs: impl IntoExpr, ) -> Result<bool>

Whether lhs == rhs is provably true (sym.AnalyzerCanProveEqual).

pub fn try_compare( &self, lhs: impl IntoExpr, rhs: impl IntoExpr, ) -> Result<CompareResult>

The relation of lhs to rhs the known comparisons imply (sym.AnalyzerTryCompare).

pub fn is_z3_enabled(&self) -> Result<bool>

Whether the analyzer was built with the Z3 prover (sym.AnalyzerIsZ3Enabled).

pub fn smtlib2(&self, expr: Option<&Expr>) -> Result<String>

The facts the Z3 prover knows, and expr to prove if given, as an SMT-LIB2 script (sym.AnalyzerGetSMTLIB2).

pub fn set_z3_timeout_ms(&self, timeout_ms: u32) -> Result<()>

Bound each Z3 proof by timeout_ms milliseconds (sym.AnalyzerSetZ3TimeoutMs).

pub fn set_z3_rlimit(&self, rlimit: u32) -> Result<()>

Bound each Z3 proof by the resource limit rlimit (sym.AnalyzerSetZ3RLimit).

pub fn z3_stats(&self) -> Result<String>

The statistics of the Z3 prover (sym.AnalyzerGetZ3Stats).

Trait Implementations

impl AnyCompatible for Analyzer

unsafe fn is_undefined(field: *const Self) -> bool

Whether field, which holds a value of this type or all-zero bytes, holds all-zero bytes that are no value of this type, as a null object reference, a string of type index None or a zero device type: a field that a creator left undefined for reflection to set, as C++ UnsafeInit leaves a reference undefined (null). Unlike a C++ undefined reference, it is no value; a nullable reference is Option<T>, whose None is a defined value.

fn type_str() -> String

the type string of the type

unsafe fn copy_to_any_view(src: &Self, data: &mut TVMFFIAny)

the value to copy to TVMFFIAny

unsafe fn check_any_strict(data: &TVMFFIAny) -> bool

unsafe fn copy_from_any_view_after_check(data: &TVMFFIAny) -> Self

Copy value from TVMFFIAny after checking caller must ensure that the value is compatible with the type

unsafe fn move_to_any(src: Self, data: &mut TVMFFIAny)

consume the value to move to Any

unsafe fn move_from_any_after_check(data: &mut TVMFFIAny) -> Self

the value to move from TVMFFIAny NOTE: pay very careful attention to avoid memory leak!

unsafe fn try_cast_from_any_view(data: &TVMFFIAny) -> Result<Self, ()>

try to cast the value from AnyView

fn get_mismatch_type_info(data: &TVMFFIAny) -> String

Get the type key of a type when TryCastFromAnyView fails.

fn type_schema() -> String

The type schema of the type: the JSON object C++ TypeTraits<T>::TypeSchema writes, which the type schemas of functions and fields embed.

fn to_any(&self) -> Any

Borrow self into an owned Any, increfing object-backed values.

impl<'a> ArgIntoRef for &'a Analyzer

type Target = Analyzer

fn to_ref(&self) -> &Self::Target

impl ArgIntoRef for Analyzer

type Target = Analyzer

fn to_ref(&self) -> &Self::Target

impl Clone for Analyzer

fn clone(&self) -> Analyzer

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Deref for Analyzer

type Target = AnalyzerObj

The resulting type after dereferencing.

fn deref(&self) -> &AnalyzerObj

Dereferences the value.

impl From<&Analyzer> for Analyzer

fn from(value: &Analyzer) -> Self

Converts to this type from the input type.

impl<'a> IntoArgHolder for &'a Analyzer

type Target = &'a Analyzer

fn into_arg_holder(self) -> Self::Target

impl IntoArgHolder for Analyzer

type Target = Analyzer

fn into_arg_holder(self) -> Self::Target

impl ObjectRefCore for Analyzer

type ContainerType = <ObjectArc<AnalyzerObj> as Deref>::Target

fn data(this: &Self) -> &ObjectArc<Self::ContainerType>

fn into_data(this: Self) -> ObjectArc<Self::ContainerType>

unsafe fn from_data(data: ObjectArc<Self::ContainerType>) -> Self

Construct a reference view from an owning container handle.

fn same_as<Other>(&self, other: &Other) -> bool

where Other: ObjectRefCore,

Return whether two object references point to the same allocation.

fn downcast_ref<T>(&self) -> Option<&T>

where T: ObjectCore,

Borrow the underlying object as T when its runtime type is T or a subtype.

impl TryFrom<Any> for Analyzer

type Error = Error

The type returned in the event of a conversion error.

fn try_from(value: Any) -> Result<Self, Self::Error>

Performs the conversion.

impl<'a> TryFrom<AnyView<'a>> for Analyzer

type Error = Error

The type returned in the event of a conversion error.

fn try_from(value: AnyView<'a>) -> Result<Self, Self::Error>

Performs the conversion.