Struct StringSolver 

pub struct StringSolver { /* private fields */ }

String theory solver

Implementations

impl StringSolver

pub fn new() -> Self

Create a new string solver

pub fn add_equality(&mut self, lhs: StringExpr, rhs: StringExpr, origin: TermId)

Add a string equality

pub fn add_disequality( &mut self, lhs: StringExpr, rhs: StringExpr, origin: TermId, )

Add a string disequality

pub fn add_length_eq(&mut self, var: u32, len: i64, origin: TermId)

Add a length constraint

pub fn add_regex_membership( &mut self, var: u32, regex: Arc<Regex>, positive: bool, origin: TermId, )

Add regex membership constraint

pub fn add_prefix(&mut self, prefix: StringExpr, s: StringExpr, origin: TermId)

Add prefix constraint: str.prefixof(prefix, s)

pub fn add_suffix(&mut self, suffix: StringExpr, s: StringExpr, origin: TermId)

Add suffix constraint: str.suffixof(suffix, s)

pub fn add_contains( &mut self, s: StringExpr, substr: StringExpr, origin: TermId, )

Add contains constraint: str.contains(s, substr)

pub fn add_str_to_int(&mut self, str_var: u32, int_value: i64, origin: TermId)

Add string-to-int constraint: int = str.to_int(s) Returns the integer value that string s represents Returns -1 if s is not a valid numeral

pub fn add_int_to_str(&mut self, str_var: u32, int_value: i64, origin: TermId)

Add int-to-string constraint: s = str.from_int(int) Converts integer to its decimal string representation

Trait Implementations

impl Debug for StringSolver

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

Formats the value using the given formatter.

impl Default for StringSolver

fn default() -> Self

Returns the “default value” for a type.

impl Theory for StringSolver

fn id(&self) -> TheoryId

Get the theory identifier

fn name(&self) -> &str

Get the name of this theory

fn can_handle(&self, _term: TermId) -> bool

Check if this theory can handle a term

fn assert_true(&mut self, term: TermId) -> Result<TheoryResult>

Assert a term as true

fn assert_false(&mut self, term: TermId) -> Result<TheoryResult>

Assert a term as false

fn check(&mut self) -> Result<TheoryResult>

Check consistency of current assertions

fn push(&mut self)

Push a context level

fn pop(&mut self)

Pop a context level

fn reset(&mut self)

Reset the theory solver

fn get_model(&self) -> Vec<(TermId, TermId)>

Get the current model (if satisfiable)