Enum biodivine_lib_param_bn::FnUpdate

pub enum FnUpdate {
    Const(bool),
    Var(VariableId),
    Param(ParameterId, Vec<FnUpdate>),
    Not(Box<FnUpdate>),
    Binary(BinaryOp, Box<FnUpdate>, Box<FnUpdate>),
}

A Boolean update function formula which references Variables and Parameters of a BooleanNetwork.

An update function specifies the evolution rules for one specific Variable of a BooleanNetwork. The arguments used in the function must be the same as specified by the RegulatoryGraph of the network.

Variants

Const(bool)

A true/false constant.

Var(VariableId)

References a network variable.

Param(ParameterId, Vec<FnUpdate>)

References a network parameter (uninterpreted function).

The variable list are the arguments of the function invocation.

Not(Box<FnUpdate>)

Negation.

Binary(BinaryOp, Box<FnUpdate>, Box<FnUpdate>)

Binary boolean operation.

Implementations

impl FnUpdate

pub fn try_from_expression( expression: BooleanExpression, graph: &RegulatoryGraph ) -> Option<FnUpdate>

Convert a BooleanExpression to a FnUpdate, using RegulatoryGraph to resolve variable names.

impl FnUpdate

Constructor and destructor utility methods. These mainly avoid unnecessary boxing and exhaustive pattern matching when not necessary.

pub fn mk_true() -> FnUpdate

Create a true formula.

pub fn mk_false() -> FnUpdate

Create a false formula.

pub fn mk_var(id: VariableId) -> FnUpdate

Create an x formula where x is a Boolean variable.

pub fn mk_param(id: ParameterId, args: &[FnUpdate]) -> FnUpdate

Create a p(e_1, ..., e_k) formula where p is a parameter function and e_1 through e_k are general argument expressions.

pub fn mk_basic_param(id: ParameterId, args: &[VariableId]) -> FnUpdate

Same as Self::mk_param, but can take variable IDs as arguments directly.

pub fn mk_not(inner: FnUpdate) -> FnUpdate

Create a !phi formula, where phi is an inner FnUpdate.

pub fn mk_binary(op: BinaryOp, left: FnUpdate, right: FnUpdate) -> FnUpdate

Create a phi 'op' psi where phi and psi are arguments of op operator.

pub fn negation(self) -> FnUpdate

Negate this function.

pub fn and(self, other: FnUpdate) -> FnUpdate

Create a conjunction.

pub fn or(self, other: FnUpdate) -> FnUpdate

Create a disjunction.

pub fn xor(self, other: FnUpdate) -> FnUpdate

Create an exclusive or.

pub fn implies(self, other: FnUpdate) -> FnUpdate

Create an implication.

pub fn iff(self, other: FnUpdate) -> FnUpdate

Create an equivalence.

pub fn as_const(&self) -> Option<bool>

If Const, return the value, otherwise return None.

pub fn as_var(&self) -> Option<VariableId>

If Var, return the id, otherwise return None.

pub fn as_param(&self) -> Option<(ParameterId, &[FnUpdate])>

If Param, return the id and args, otherwise return None.

pub fn as_not(&self) -> Option<&FnUpdate>

If Not, return the inner function, otherwise return None.

pub fn as_binary(&self) -> Option<(&FnUpdate, BinaryOp, &FnUpdate)>

If Binary, return the operator and left/right formulas, otherwise return None.

pub fn mk_conjunction(items: &[FnUpdate]) -> FnUpdate

Build an expression which is equivalent to the conjunction of the given expressions.

pub fn mk_disjunction(items: &[FnUpdate]) -> FnUpdate

Build an expression which is equivalent to the disjunction of the given expressions.

impl FnUpdate

Other utility methods.

pub fn try_from_str( expression: &str, network: &BooleanNetwork ) -> Result<FnUpdate, String>

Try to parse an update function from a string expression using the provided network as context.

pub fn build_from_bdd(context: &SymbolicContext, bdd: &Bdd) -> FnUpdate

Build an update function from an instantiated Bdd.

The support set of the Bdd must be a subset of the state variables and zero-arity parameters.

Note that it should be possible to also build a variant of this function where this requirement is lifted, but it’s a bit more complicated and so far we are ok with only building fully instantiated update functions.

The function produces a DNF representation based on all satisfying clauses. This is far from minimal, but appears to be slightly more concise than the default translation in lib-bdd.

pub fn collect_arguments(&self) -> Vec<VariableId>

Return a sorted vector of all variables that are actually used as inputs in this function.

pub fn collect_parameters(&self) -> Vec<ParameterId>

Return a sorted vector of all parameters (i.e. uninterpreted functions) that are used in this update function.

pub fn to_string(&self, context: &BooleanNetwork) -> String

Convert this update function to a string, taking names from the provided BooleanNetwork.

pub fn evaluate(&self, values: &HashMap<VariableId, bool>) -> Option<bool>

If possible, evaluate this function using the given network variable valuation.

Note that this only works when the function output does not depend on parameters, and all necessary variable values are part of the valuation. Otherwise, the function returns None, as the value cannot be determined.

However, note that in some cases, even a partially specified function can be evaluated. For example, A & f(X, Y) is false whenever A = false, regardless of uninterpreted function f. In such cases, this method may still output the correct result.

In other words, the meaning of this method should be interpreted as “if it is possible to unambiguously evaluate this function using the provided valuation, do it; otherwise return None”.

pub fn walk_postorder<F>(&self, action: &mut F)

where F: FnMut(&FnUpdate),

Allows us to iterate through all nodes of the abstract syntax tree of this function in post-order.

Note that this is a preliminary version of the API. A more robust implementation should provide a standard iterator interface.

pub fn substitute_variable( &self, var: VariableId, expression: &FnUpdate ) -> FnUpdate

Create a copy of this FnUpdate with every occurrence of VariableId var substituted for FnUpdate expression.

pub fn rename_all( &self, variables: &HashMap<VariableId, VariableId>, parameters: &HashMap<ParameterId, ParameterId> ) -> FnUpdate

Rename all occurrences of the specified variables and parameters to new IDs.

pub fn contains_parameter(&self, parameter: ParameterId) -> bool

Returns true if this update function uses the given parameter.

pub fn contains_variable(&self, variable: VariableId) -> bool

Returns true if this update function uses the given variable.

pub fn to_and_or_normal_form(&self) -> FnUpdate

Perform a syntactic transformation of this update function which eliminates all binary operators except for & and |. Negation is also preserved.

Note that the result is neither a conjunction or disjunctive normal form, it just eliminates all operators other than conjunction and disjunction.

Furthermore, when the function contains parameters with expression arguments, the arguments are normalized as well.

pub fn distribute_negation(&self) -> FnUpdate

Perform a syntactic transformation which pushes every negation to literals (constants, variables, and parameter terms).

Note that constants will be automatically negated (true => false, false => true). Also, keep in mind that this will rewrite binary operators (and => or, iff => xor, etc.), so don’t expect the function to look the same afterwards.

Similar to Self::to_and_or_normal_form, when the function contains parameters with complex arguments, each argument is also normalized.

pub fn simplify_constants(&self) -> FnUpdate

Utility function that eliminates unnecessary constants from this update function using standard syntactic transformations.

Trait Implementations

impl Clone for FnUpdate

fn clone(&self) -> FnUpdate

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for FnUpdate

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

Formats the value using the given formatter.

impl Display for FnUpdate

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

Formats the value using the given formatter.

impl Hash for FnUpdate

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, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for FnUpdate

fn eq(&self, other: &FnUpdate) -> 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 !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for FnUpdate

impl StructuralPartialEq for FnUpdate