Trait z3::ast::Ast

pub trait Ast<'ctx>: Debug {
    // Required methods
    fn get_ctx(&self) -> &'ctx Context;
    fn get_z3_ast(&self) -> Z3_ast;
    unsafe fn wrap(ctx: &'ctx Context, ast: Z3_ast) -> Self
       where Self: Sized;

    // Provided methods
    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(ctx: &'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 { ... }
}

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

Required Methods

fn get_ctx(&self) -> &'ctx Context

fn get_z3_ast(&self) -> Z3_ast

unsafe fn wrap(ctx: &'ctx Context, ast: Z3_ast) -> Selfwhere Self: Sized,

Wrap a raw Z3_ast.

Safety

The ast must be a valid pointer to a Z3_ast.

Provided Methods

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

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.

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

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

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

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.

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

Get the Sort of the Ast.

fn simplify(&self) -> Selfwhere Self: Sized,

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

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

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.

fn num_children(&self) -> usize

Return the number of children of this Ast.

Leaf nodes (eg Bool consts) will return 0.

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

Return the nth child of this Ast.

Out-of-bound indices will return None.

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

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

fn kind(&self) -> AstKind

Return the AstKind for this Ast.

fn is_app(&self) -> bool

Return true if this is a Z3 function application.

Note that constants are function applications with 0 arguments.

fn is_const(&self) -> bool

Return true if this is a Z3 constant.

Note that constants are function applications with 0 arguments.

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

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.

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

fn translate<'src_ctx>(&'src_ctx self, dest: &'ctx Context) -> Selfwhere Self: Sized,

Implementors

impl<'ctx> Ast<'ctx> for Array<'ctx>

impl<'ctx> Ast<'ctx> for BV<'ctx>

impl<'ctx> Ast<'ctx> for Bool<'ctx>

impl<'ctx> Ast<'ctx> for Datatype<'ctx>

impl<'ctx> Ast<'ctx> for Dynamic<'ctx>

impl<'ctx> Ast<'ctx> for Float<'ctx>

impl<'ctx> Ast<'ctx> for Int<'ctx>

impl<'ctx> Ast<'ctx> for Real<'ctx>

impl<'ctx> Ast<'ctx> for Regexp<'ctx>

impl<'ctx> Ast<'ctx> for Set<'ctx>

impl<'ctx> Ast<'ctx> for String<'ctx>