Struct z3::ast::String

pub struct String<'ctx> { /* fields omitted */ }

Ast node representing a string value.

Implementations

impl<'ctx> String<'ctx>

pub fn new_const<S: Into<Symbol>>(ctx: &'ctx Context, name: S) -> String<'ctx>

Creates a new constant using the built-in string sort

pub fn fresh_const(ctx: &'ctx Context, prefix: &str) -> String<'ctx>

Creates a fresh constant using the built-in string sort

pub fn from_str(
    ctx: &'ctx Context,
    string: &str
) -> Result<String<'ctx>, NulError>

Creates a Z3 constant string from a &str

pub fn as_string(&self) -> Option<String>

Retrieves the underlying std::string::String

If this is not a constant z3::ast::String, return None.

Note that to_string() provided by std::string::ToString (which uses std::fmt::Display) returns an escaped string. In contrast, z3::ast::String::from_str(&ctx, s).unwrap().as_string() returns a String equal to the original value.

pub fn concat(context: &'ctx Context, values: &[&Self]) -> String<'ctx>

Appends the argument strings to Self

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

Checks whether Self contains a substring

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

Checks whether Self is a prefix of the argument

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

Checks whether Self is a sufix of the argument

Trait Implementations

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

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

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

fn get_z3_ast(&self) -> Z3_ast

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

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

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(context: &'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.

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

Get the Sort of the Ast

fn simplify(&self) -> Self where
    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)]) -> Self where
    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.

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

Return the nth child of this Ast.

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.

fn is_const(&self) -> bool

Return true if this is a Z3 constant.

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

Return the FuncDecl of the Ast.

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

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

impl<'ctx> Clone for String<'ctx>

fn clone(&self) -> Self

Returns a copy of the value.

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

Performs copy-assignment from source.

impl<'ctx> Debug for String<'ctx>

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<'ctx> Display for String<'ctx>

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<'ctx> Drop for String<'ctx>

fn drop(&mut self)

Executes the destructor for this type.

impl<'ctx> From<String<'ctx>> for Z3_ast

fn from(ast: String<'ctx>) -> Self

Performs the conversion.

impl<'ctx> From<String<'ctx>> for Dynamic<'ctx>

fn from(ast: String<'ctx>) -> Self

Performs the conversion.

impl<'ctx> Hash for String<'ctx>

fn hash<H: Hasher>(&self, state: &mut H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H) where
    H: Hasher, 

Feeds a slice of this type into the given Hasher.

impl<'ctx> PartialEq<String<'ctx>> for String<'ctx>

fn eq(&self, other: &String<'ctx>) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

This method tests for !=.

impl<'ctx> TryFrom<Dynamic<'ctx>> for String<'ctx>

type Error = String

The type returned in the event of a conversion error.

fn try_from(ast: Dynamic<'ctx>) -> Result<Self, String>

Performs the conversion.

impl<'ctx> Eq for String<'ctx>