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

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

    fn get_z3_ast(&self) -> Z3_ast;

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

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

    fn distinct(&self, other: &[&Self]) -> Bool<'ctx> { ... }

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

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

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

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

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

Loading content...

Provided methods

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

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 distinct(&self, other: &[&Self]) -> Bool<'ctx>

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) -> Self

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)]) -> Self

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.

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]

Loading content...