Struct biodivine_sketchbook::sketchbook::model::UninterpretedFn

source ·

pub struct UninterpretedFn {
    name: String,
    annotation: String,
    arguments: Vec<FnArgument>,
    tree: Option<FnTree>,
    expression: String,
}

Expand description

An uninterpreted function of a partially specified model.

Field arguments hold information regarding properties of the function with respect to each of its arguments (in order). It also tracks the arity.

You can leave the function completely unspecified, or you can add an “partial expression”. Field tree holds the parsed version of that formula, while expression tracks the original formula.

Fields§

§name: String§annotation: String§arguments: Vec<FnArgument>§tree: Option<FnTree>§expression: String

Implementations§

source §

impl UninterpretedFn

Creating new UninterpretedFn instances.

source

pub fn new_without_constraints( name: &str, arity: usize, ) -> Result<UninterpretedFn, String>

Create new UninterpretedFn object that has no constraints regarding monotonicity, essentiality, or its expression. Annotation is empty.

source

pub fn new( name: &str, annotation: &str, expression: &str, arguments: Vec<FnArgument>, model: &ModelState, own_id: &UninterpretedFnId, ) -> Result<UninterpretedFn, String>

Create new UninterpretedFn instance given all its raw components.

The model and function’s ID are used for validity check during argument parsing.

source

pub fn with_new_expression( original_fn: UninterpretedFn, new_expression: &str, context: &ModelState, own_id: &UninterpretedFnId, ) -> Result<UninterpretedFn, String>

Create uninterpreted function using another one as a template, but changing the expression. The provided original function object is consumed.

source

pub fn with_substituted_fn_symbol( original_fn: UninterpretedFn, old_id: &UninterpretedFnId, new_id: &UninterpretedFnId, context: &ModelState, ) -> UninterpretedFn

Create uninterpreted function from another one, substituting all occurrences of a given function symbol in the syntactic tree. The provided original function object is consumed.

source §

impl UninterpretedFn

Editing UninterpretedFn instances.

source

pub fn set_name(&mut self, new_name: &str) -> Result<(), String>

Rename this uninterpreted fn.

source

pub fn set_annotation(&mut self, annotation: &str)

Change annotation of this uninterpreted fn.

source

pub fn set_arity(&mut self, new_arity: usize) -> Result<(), String>

Change arity of this uninterpreted fn.

If arity is made larger, default arguments (without monotonicity/essentiality constraints) are added. If arity is made smaller, last arguments are dropped. These must not be used in function’s expression.

source

pub fn drop_last_argument(&mut self) -> Result<(), String>

Drop the last argument of the function, essentially decrementing the arity of this uninterpreted fn. The last argument must not be used in function’s expression.

source

pub fn add_argument( &mut self, monotonicity: Monotonicity, essentiality: Essentiality, )

Add an argument with specified monotonicity/essentiality. Argument is added at the end of the current argument list.

source

pub fn add_default_argument(&mut self)

Add default argument (with unknown monotonicity/essentiality) for this function. Argument is added at the end of the current argument list.

source

pub fn set_fn_expression( &mut self, new_expression: &str, model: &ModelState, own_id: &UninterpretedFnId, ) -> Result<(), String>

Set the function’s expression to a given string.

model is used to provide context regarding valid IDs.

We also need ID of this uninterpreted function to ensure that the expression is not defined recursively, i.e., to check that expression of function f does not contain f inside.

source