pub struct Regexp<'ctx> { /* private fields */ }
Expand description
Ast
node representing a regular expression.
use z3::ast;
use z3::{Config, Context, Solver, SatResult};
let cfg = Config::new();
let ctx = &Context::new(&cfg);
let solver = Solver::new(&ctx);
let s = ast::String::new_const(ctx, "s");
// the regexp representing foo[a-c]*
let a = ast::Regexp::concat(ctx, &[
&ast::Regexp::literal(ctx, "foo"),
&ast::Regexp::range(ctx, &'a', &'c').star()
]);
// the regexp representing [a-z]+
let b = ast::Regexp::range(ctx, &'a', &'z').plus();
// intersection of a and b is non-empty
let intersect = ast::Regexp::intersect(ctx, &[&a, &b]);
solver.assert(&s.regex_matches(&intersect));
assert!(solver.check() == SatResult::Sat);
Implementations§
source§impl<'ctx> Regexp<'ctx>
impl<'ctx> Regexp<'ctx>
sourcepub fn literal(ctx: &'ctx Context, s: &str) -> Self
pub fn literal(ctx: &'ctx Context, s: &str) -> Self
Creates a regular expression that recognizes the string given as parameter
sourcepub fn range(ctx: &'ctx Context, lo: &char, hi: &char) -> Self
pub fn range(ctx: &'ctx Context, lo: &char, hi: &char) -> Self
Creates a regular expression that recognizes a character in the specificed range (e.g.
[a-z]
)
sourcepub fn loop(&self, lo: u32, hi: u32) -> Self
pub fn loop(&self, lo: u32, hi: u32) -> Self
Creates a regular expression that recognizes this regular expression lo
to hi
times (e.g. a{2,3}
)
sourcepub fn full(ctx: &'ctx Context) -> Self
pub fn full(ctx: &'ctx Context) -> Self
Creates a regular expression that recognizes all sequences
sourcepub fn empty(ctx: &'ctx Context) -> Self
pub fn empty(ctx: &'ctx Context) -> Self
Creates a regular expression that doesn’t recognize any sequences
sourcepub fn plus(&self) -> Self
pub fn plus(&self) -> Self
Creates a regular expression that recognizes this regular expression one or more times (e.g. a+
)
sourcepub fn star(&self) -> Self
pub fn star(&self) -> Self
Creates a regular expression that recognizes this regular expression any number of times
(Kleene star, e.g. a*
)
sourcepub fn complement(&self) -> Self
pub fn complement(&self) -> Self
Creates a regular expression that recognizes any sequence that this regular expression doesn’t
Trait Implementations§
source§impl<'ctx> Ast<'ctx> for Regexp<'ctx>
impl<'ctx> Ast<'ctx> for Regexp<'ctx>
fn get_ctx(&self) -> &'ctx Context
fn get_z3_ast(&self) -> Z3_ast
source§fn _safe_eq(&self, other: &Self) -> Result<Bool<'ctx>, SortDiffers<'ctx>>where
Self: Sized,
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.source§fn simplify(&self) -> Selfwhere
Self: Sized,
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.source§fn substitute<T: Ast<'ctx>>(&self, substitutions: &[(&T, &T)]) -> Selfwhere
Self: Sized,
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
.source§fn num_children(&self) -> usize
fn num_children(&self) -> usize
Return the number of children of this
Ast
. Read morefn safe_decl(&self) -> Result<FuncDecl<'ctx>, IsNotApp>
fn translate<'src_ctx>(&'src_ctx self, dest: &'ctx Context) -> Selfwhere Self: Sized,
source§impl<'ctx> PartialEq<Regexp<'ctx>> for Regexp<'ctx>
impl<'ctx> PartialEq<Regexp<'ctx>> for Regexp<'ctx>
impl<'ctx> Eq for Regexp<'ctx>
Auto Trait Implementations§
impl<'ctx> RefUnwindSafe for Regexp<'ctx>
impl<'ctx> !Send for Regexp<'ctx>
impl<'ctx> !Sync for Regexp<'ctx>
impl<'ctx> Unpin for Regexp<'ctx>
impl<'ctx> UnwindSafe for Regexp<'ctx>
Blanket Implementations§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more