Module biodivine_sketchbook::algorithms::fo_logic::utils

Functions

• check_fn_symbol_support
  Check that symbolic context supports given function symbol (parameter) of given arity.
• check_fol_var_support
  Check that extended symbolic graph’s BDD supports given extra variable.
• check_update_fn_support
  Check that BN has given variable, and that it has given number of regulators.
• collect_unique_fn_symbols
  Compute the set of all unique function symbols (with arities) in the formula tree.
• collect_unique_fn_symbols_recursive 🔒
• collect_unique_fol_vars
  Compute the set of all uniquely named FOL variables in the formula tree.
• collect_unique_fol_vars_recursive 🔒
• get_implicit_function_name
  Compute a valid name for an “anonymous update function” of the corresponding variable.
• get_var_base_and_offset
  For a given FOL variable name, get a base variable of the BN and offset that was used to add it to the symbolic context.
• get_var_from_implicit
  If the provided function symbol corresponds to (implicit) update function for some variable, get the variable’s name. Return Err if the symbol is not in format “f_VAR”.
• is_update_fn_symbol
  Check if a given function symbol name corresponds to an (implicit) update function.
• validate_and_rename_recursive 🔒
  Checks that all FOL variables in the formula’s syntactic tree are quantified (exactly once), and renames these variables to a pseudo-canonical form that will be used in BDDs. It renames as many variables as possible to identical names, without affecting the semantics.
• validate_and_rename_vars
  Checks that all FOL variables in the formula’s syntactic tree are quantified (exactly once), and renames these variables to a pseudo-canonical form that will be used in BDDs. It renames as many variables as possible to identical names, without affecting the semantics.