Module biodivine_sketchbook::algorithms::fo_logic::eval_wrappers

Functions

• eval_formula
  Evaluate given formula a given transition graph. The graph MUST support enough sets of symbolic variables to represent all occurring FO vars. Return the resulting set of colored vertices.
• eval_formula_dirty
  Evaluate given formula, but do not sanitize the result. The graph MUST support enough sets of symbolic variables to represent all occurring FO vars.
• eval_multiple_formulas
  Evaluate each of a list of FOL formulas on a given transition graph. Return the resulting sets of colored vertices (in the same order as input formulas). The graph MUST support enough sets of symbolic variables to represent all occurring FO vars.
• eval_multiple_formulas_dirty
  Evaluate each of a list of FOL formulas, but do not sanitize the results. The graph MUST support enough sets of symbolic variables to represent all occurring FO vars.
• eval_multiple_trees
  Evaluate each of a list of FOL formulas given by their syntax trees on a given transition graph. The graph MUST support enough sets of symbolic variables to represent all occurring FO vars. Return the list of resulting sets of colored vertices (in the same order as input formulas).
• eval_multiple_trees_dirty
  Evaluate each of a list of FOL formulas given by their syntax trees on a given transition graph.
• eval_tree
  Evaluate formula given by its syntactic tree. The graph MUST support enough sets of symbolic variables to represent all occurring FO vars. Return the resulting set of colored vertices.
• eval_tree_dirty
  Evaluate formula given by its syntactic tree, but do not sanitize the results. The graph MUST support enough sets of symbolic variables to represent all occurring FO vars.
• parse_and_validate 🔒
  Parse given FOL formulas list into syntactic trees and perform compatibility check with the provided graph (i.e., check if graph object supports all needed symbolic variables).