Function biodivine_sketchbook::algorithms::fo_logic::utils::validate_and_rename_recursive

source · 
fn validate_and_rename_recursive(
    orig_tree: FolTreeNode,
    var_base_name: &str,
    renaming_map: HashMap<String, String>,
    index: u32,
) -> Result<FolTreeNode, String>
Expand description

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.

The format of variable names is given by how [SymbolicContext::with_extra_state_variables] creates new extra variables. Basically, we choose a name of one BN variable (var_core_name), and it is used as a base for extra variables {var_base_name}_extra_{index}.