Module biodivine_sketchbook::algorithms::fo_logic::parser

Functions

• index_of_first 🔒
  Utility method to find the first occurrence of a specific token in the token tree.
• index_of_first_quantifier 🔒
  Utility method to find the first occurrence of a quantifier operator in the token tree.
• index_of_first_unary 🔒
  Utility method to find the first occurrence of an unary operator in the token tree.
• is_quantifier 🔒
  Predicate for whether given token represents a quantifier.
• is_unary 🔒
  Predicate for whether given token represents unary operator.
• parse_1_quantifiers 🔒
  Recursive parsing step 1: extract quantifier operators.
• parse_2_iff 🔒
  Recursive parsing step 2: extract <=> operators.
• parse_3_imp 🔒
  Recursive parsing step 3: extract => operators.
• parse_4_or 🔒
  Recursive parsing step 4: extract | operators.
• parse_5_xor 🔒
  Recursive parsing step 5: extract ^ operators.
• parse_6_and 🔒
  Recursive parsing step 6: extract & operators.
• parse_7_unary 🔒
  Recursive parsing step 7: extract unary operators (just a negation currently).
• parse_8_terms_and_parentheses 🔒
  Recursive parsing step 8: extract terms and recursively solve sub-formulae in parentheses and in functions.
• parse_and_minimize_fol_formula
  Parse an FOL formula string representation into an actual formula tree with renamed (minimized) set of variables.
• parse_fol_formula
  Parse an FOL formula string representation into an actual formula tree. Basically a wrapper for tokenize+parse (used often for testing/debug purposes).
• parse_fol_tokens
  Parse tokens of FOL formula into an abstract syntax tree using recursive steps.