Package org.variantsync.diffdetective.analysis.logic

Class Tseytin.Convert

java.lang.Object
org.variantsync.diffdetective.analysis.logic.Tseytin.Convert
Enclosing class:
Tseytin
private static class Tseytin.Convert extends Object
Helper class for Tseytin conversion that remembers generated formulas. This helper class basically models the conversion function equipped with some useful state. (Function programmers might see this as a function within a state monad.)

  • Field Summary

    Fields
    Modifier and Type
    Field
    Description
    private int
    currentIndex
     
    private final BiFunction<org.prop4j.Node,org.prop4j.Node,org.prop4j.Node>
    eq
     
    private final List<org.prop4j.Node>
    newSubFormulas
     

  • Constructor Summary

    Constructors
    Modifier
    Constructor
    Description
    private
    Convert(org.prop4j.Node formula, BiFunction<org.prop4j.Node,org.prop4j.Node,org.prop4j.Node> eq)
    Convertes the given formula with the given equivalence function.

  • Method Summary

    Modifier and Type
    Method
    Description
    private String
    getNextVariableName()
     
    private org.prop4j.Node
    tseytin(org.prop4j.Node formula)
    Performs tseyting conversion on the given formula.

    Methods inherited from class java.lang.Object

    clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

  • Field Details

    • newSubFormulas

      private final List<org.prop4j.Node> newSubFormulas

    • currentIndex

      private int currentIndex

    • eq

      private final BiFunction<org.prop4j.Node,org.prop4j.Node,org.prop4j.Node> eq

  • Constructor Details

    • Convert

      private Convert(org.prop4j.Node formula, BiFunction<org.prop4j.Node,org.prop4j.Node,org.prop4j.Node> eq)
      Convertes the given formula with the given equivalence function.
      Parameters:
      formula - Formula to tseytin convert.
      eq - Function that models the equivelency relationship between two given nodes. Typically, this function produces a propositional "iff" (<=>).

  • Method Details

    • tseytin

      private org.prop4j.Node tseytin(org.prop4j.Node formula)
      Performs tseyting conversion on the given formula.
      Parameters:
      formula - Formula to convert.
      Returns:
      The tseyting variable representing the input formula.

    • getNextVariableName

      private String getNextVariableName()