Trait z3::ast::Ast[−][src]

pub trait Ast<'ctx>: Debug {

Show 18 methods    fn get_ctx(&self) -> &'ctx Context;

    fn get_z3_ast(&self) -> Z3_ast;

    fn new(ctx: &'ctx Context, ast: Z3_ast) -> Self
    where
        Self: Sized;

    fn _eq(&self, other: &Self) -> Bool<'ctx>
    where
        Self: Sized,
    { ... }

    fn _safe_eq(&self, other: &Self) -> Result<Bool<'ctx>, SortDiffers<'ctx>>
    where
        Self: Sized,
    { ... }

    fn distinct(context: &'ctx Context, values: &[&Self]) -> Bool<'ctx>
    where
        Self: Sized,
    { ... }

    fn get_sort(&self) -> Sort<'ctx> { ... }

    fn simplify(&self) -> Self
    where
        Self: Sized,
    { ... }

    fn substitute<T: Ast<'ctx>>(&self, substitutions: &[(&T, &T)]) -> Self
    where
        Self: Sized,
    { ... }

    fn num_children(&self) -> usize { ... }

    fn nth_child(&self, idx: usize) -> Option<Dynamic<'ctx>> { ... }

    fn children(&self) -> Vec<Dynamic<'ctx>> { ... }

    fn kind(&self) -> AstKind { ... }

    fn is_app(&self) -> bool { ... }

    fn is_const(&self) -> bool { ... }

    fn decl(&self) -> FuncDecl<'ctx> { ... }

    fn safe_decl(&self) -> Result<FuncDecl<'ctx>, IsNotApp> { ... }

    fn translate<'src_ctx>(&'src_ctx self, dest: &'ctx Context) -> Self
    where
        Self: Sized,
    { ... }

}
Expand description

Abstract syntax tree (AST) nodes represent terms, constants, or expressions. The Ast trait contains methods common to all AST subtypes.

Required methods

Provided methods

Compare this Ast with another Ast, and get a Bool representing the result.

This operation works with all possible Asts (int, real, BV, etc), but the two Asts being compared must be the same type.

Compare this Ast with another Ast, and get a Result. Errors if the sort does not match for the two values.

Compare this Ast with a list of other Asts, and get a Bool which is true only if all arguments (including Self) are pairwise distinct.

This operation works with all possible Asts (int, real, BV, etc), but the Asts being compared must all be the same type.

Get the Sort of the Ast

Simplify the Ast. Returns a new Ast which is equivalent, but simplified using algebraic simplification rules, such as constant propagation.

Performs substitution on the Ast. The slice substitutions contains a list of pairs with a “from” Ast that will be substituted by a “to” Ast.

Return the number of children of this Ast.

Leaf nodes (eg Bool consts) will return 0.

Return the nth child of this Ast.

Out-of-bound indices will return None.

Return the children of this node as a Vec<Dynamic>.

Return the AstKind for this Ast.

Return true if this is a Z3 function application.

Note that constants are function applications with 0 arguments.

Return true if this is a Z3 constant.

Note that constants are function applications with 0 arguments.

Return the FuncDecl of the Ast.

This will panic if the Ast is not an app, i.e. if AstKind is not App or Numeral.

Implementors