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

pub trait Ast<'ctx>: Sized + Debug + Into<Dynamic<'ctx>> {
    pub fn get_ctx(&self) -> &'ctx Context;

    pub fn get_z3_ast(&self) -> Z3_ast;

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

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

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

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

    pub fn simplify(&self) -> Self { ... }

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

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

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

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

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

Required methods

pub fn get_ctx(&self) -> &'ctx Context[src]

pub fn get_z3_ast(&self) -> Z3_ast[src]

pub fn new(ctx: &'ctx Context, ast: Z3_ast) -> Self[src]

Loading content...

Provided methods

pub fn _eq(&self, other: &Self) -> Bool<'ctx>[src]

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.

pub fn distinct(context: &'ctx Context, values: &[&Self]) -> Bool<'ctx>[src]

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.

pub fn get_sort(&self) -> Sort<'ctx>[src]

Get the Sort of the Ast

pub fn simplify(&self) -> Self[src]

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

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

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.

pub fn num_children(&self) -> usize[src]

Return the number of children of this AST node. Leaf nodes (eg Bool consts) will return 0.

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

Return the nth child of this AST node. Out-of-bound indices will return none.

pub fn children(&self) -> Vec<Dynamic<'ctx>>[src]

Return the children of this node as a Vec of Dynamic nodes.

Loading content...

Implementors

impl<'ctx> Ast<'ctx> for Array<'ctx>[src]

impl<'ctx> Ast<'ctx> for BV<'ctx>[src]

impl<'ctx> Ast<'ctx> for Bool<'ctx>[src]

impl<'ctx> Ast<'ctx> for Datatype<'ctx>[src]

impl<'ctx> Ast<'ctx> for Dynamic<'ctx>[src]

impl<'ctx> Ast<'ctx> for Int<'ctx>[src]

impl<'ctx> Ast<'ctx> for Real<'ctx>[src]

impl<'ctx> Ast<'ctx> for Set<'ctx>[src]

impl<'ctx> Ast<'ctx> for String<'ctx>[src]

Loading content...