Class FOFormulas

java.lang.Object
fr.inria.rules.integraal.model.formula.FOFormulas
public class FOFormulas extends Object
Utility class for standard operations on formulas
Author:
Florent Tornil, Guillaume Perution-Kihli

  • Method Details

    • createImageWith

      @Deprecated public static <Formula extends FOFormula> Formula createImageWith(Formula formula, Substitution s)
      Deprecated.
      Applies a substitution to a formula without evaluating nested functions.
      Type Parameters:
      Formula - the concrete formula type
      Parameters:
      formula - the formula to transform
      s - the substitution to apply
      Returns:
      the rewritten formula

    • createImageWith

      @Deprecated public static <Formula extends FOFormula> Formula createImageWith(Formula formula, Substitution s, boolean evaluateFunctions)
      Deprecated.
      Applies a substitution to a formula and optionally evaluates nested functions.
      Type Parameters:
      Formula - the concrete formula type
      Parameters:
      formula - the formula
      s - the substitution
      evaluateFunctions - whether nested evaluable functions should be evaluated
      Returns:
      a new FOFormula corresponding to the given FOFormula in which the given substitution have been applied

    • getTerms

      public static Collection<Term> getTerms(FOFormula formula)
      Collects all terms appearing in the supplied formula.
      Parameters:
      formula - the formula
      Returns:
      all the terms of the given formula

    • getJoinVariables

      public static Set<Variable> getJoinVariables(FOFormula formula)
      Computes the variables shared by at least two atoms of the formula.
      Parameters:
      formula - the atoms to compute join variables on, which may be compatible with flatten
      Returns:
      all the variables that are used in at least 2 atoms of the formula

    • getFirstLevelJoinVariables

      public static Set<Variable> getFirstLevelJoinVariables(FOFormula formula)
      Computes the variables shared by at least two direct children of the formula.
      Parameters:
      formula - the atoms to compute join variables - compute the join variables only on the first level, not recursively
      Returns:
      all the variables that are used in at least 2 direct subElements of the formula

    • getSharedVariables

      public static Stream<Variable> getSharedVariables(FOFormula formula, FOFormula... otherFormulas)
      Return the variables that appear both in formula and at least one formula of otherFormulas
      Parameters:
      formula - the reference formula
      otherFormulas - the formulas compared against formula
      Returns:
      a stream of variables

    • extractEvaluableFunctionsFromConjunctionFormula

      public static <F extends FOFormula> org.apache.commons.lang3.tuple.Pair<F, TermPartition> extractEvaluableFunctionsFromConjunctionFormula(F formula)
      Traverses the supplied first-order formula and rewrites every occurrence of an EvaluableFunction that appears inside an Atom.

      Algorithm overview:

      • The formula tree is visited depth-first.
      • Whenever an atom is met, each of its terms is inspected:
        • If a term is itself an evaluable function, the term is replaced by a fresh Variable.
        • An equation entry v = ef(...) is recorded in a TermPartition.
      • The traversal continues recursively through conjunctions, disjunctions and negations so that every nested atom is processed.

      The rewritten formula is structurally identical to the input (same connectives, predicates and arities) except that some terms have been replaced by fresh variables. Paired with the returned partition, it preserves exactly the original semantics.

      Type Parameters:
      F - the concrete subtype of FOFormula supplied by the caller
      Parameters:
      formula - the formula to transform (must not be null)
      Returns:
      a pair whose left component is the rewritten formula and whose right component is the aggregated TermPartition
      Throws:
      NullPointerException - if formula is null
      IllegalStateException - if an unsupported formula implementation is encountered

    • replaceEvaluableParts

      public static <F extends FOFormula> FOFormulas.EvaluableReplacementResult<F> replaceEvaluableParts(F formula)
      Replaces evaluable terms and computed atoms and returns the collected mappings.
      Type Parameters:
      F - the concrete formula type
      Parameters:
      formula - the formula to rewrite
      Returns:
      the rewritten formula together with the replacement maps

    • restoreEvaluableParts

      public static <F extends FOFormula> F restoreEvaluableParts(F formula, com.google.common.collect.BiMap<EvaluableFunction, LogicalFunctionalTerm> functionReplacement, com.google.common.collect.BiMap<Predicate, Invoker> atomReplacement)
      Restores evaluable terms and computed atoms from their placeholder representation.
      Type Parameters:
      F - the concrete formula type
      Parameters:
      formula - the rewritten formula to restore
      functionReplacement - the mapping from evaluable functions to placeholder logical terms
      atomReplacement - the mapping from computed predicates to their invokers
      Returns:
      the restored formula

    • replaceEvaluableParts

      public static <F extends FOFormula> F replaceEvaluableParts(F formula, com.google.common.collect.BiMap<EvaluableFunction, LogicalFunctionalTerm> funRepl, com.google.common.collect.BiMap<Predicate, Invoker> atomInv)
      Replaces evaluable terms and computed atoms in a formula with placeholder structures.
      Type Parameters:
      F - the concrete formula type
      Parameters:
      formula - the formula to rewrite
      funRepl - the mapping used for evaluable-function placeholders
      atomInv - the mapping used for computed-atom invokers
      Returns:
      the rewritten formula

    • replaceEvaluableParts

      public static Term replaceEvaluableParts(Term term, com.google.common.collect.BiMap<EvaluableFunction, LogicalFunctionalTerm> funRepl)
      Replaces evaluable parts inside a term with placeholder logical functional terms.
      Parameters:
      term - the term to rewrite
      funRepl - the mapping used for evaluable-function placeholders
      Returns:
      the rewritten term

    • restoreEvaluablePartsHelper

      public static Term restoreEvaluablePartsHelper(Term term, com.google.common.collect.BiMap<LogicalFunctionalTerm, EvaluableFunction> inverseFun)
      Restores evaluable parts inside a term from placeholder logical functional terms.
      Parameters:
      term - the term to restore
      inverseFun - the reverse mapping from placeholders to evaluable functions
      Returns:
      the restored term