Package com.tonic.analysis.source.recovery.rcs

Class BoolFormulaFactory

  • public final class BoolFormulaFactory
extends Object
    The reaching-condition boolean engine for one method's structuring pass.

    • Field Detail

      • truth

        public final BoolFormula truth
        The constant true formula.

      • falsity

        public final BoolFormula falsity
        The constant false formula.

    • Constructor Detail

      • BoolFormulaFactory

        public BoolFormulaFactory()
        Creates an engine with fresh BDD and NNF factories and an unconstrained domain.

    • Method Detail

      • atom

        public BoolFormula atom​(int var)
        Builds the positive-literal formula for one atom.
        Parameters:
        var - non-negative atom index
        Returns:
        the formula asserting that atom

      • and

        public BoolFormula and​(BoolFormula a,
                       BoolFormula b)
        Conjoins two formulas in both the BDD and NNF layers.
        Parameters:
        a - the left operand
        b - the right operand
        Returns:
        the conjunction, collapsed to a constant when the BDD proves it constant

      • or

        public BoolFormula or​(BoolFormula a,
                      BoolFormula b)
        Disjoins two formulas in both the BDD and NNF layers.
        Parameters:
        a - the left operand
        b - the right operand
        Returns:
        the disjunction, collapsed to a constant when the BDD proves it constant

      • not

        public BoolFormula not​(BoolFormula a)
        Negates a formula in both the BDD and NNF layers.
        Parameters:
        a - the operand
        Returns:
        the negation, collapsed to a constant when the BDD proves it constant

      • equivalent

        public boolean equivalent​(BoolFormula a,
                          BoolFormula b)
        Tests equality of the two canonical BDDs, ignoring the registered domains.
        Parameters:
        a - the left operand
        b - the right operand
        Returns:
        true if both denote the same boolean function

      • isTautology

        public boolean isTautology​(BoolFormula a)
        Tests whether a formula holds under every assignment, ignoring the registered domains.
        Parameters:
        a - the formula
        Returns:
        true if the formula is unconditionally true

      • isSatisfiable

        public boolean isSatisfiable​(BoolFormula a)
        Tests whether a formula holds under some assignment, ignoring the registered domains.
        Parameters:
        a - the formula
        Returns:
        true if the formula is not unconditionally false

      • implies

        public boolean implies​(BoolFormula a,
                       BoolFormula b)
        Tests entailment, ignoring the registered domains.
        Parameters:
        a - the antecedent
        b - the consequent
        Returns:
        true if every assignment satisfying a satisfies b

      • addMutualExclusion

        public void addMutualExclusion​(int[] atoms)
        Folds one switch selector's "at most one case holds" constraint into the domain.
        Parameters:
        atoms - the selector's case atom indices

      • equivalentGiven

        public boolean equivalentGiven​(BoolFormula a,
                               BoolFormula b)
        Tests equivalence restricted to the assignments the registered domains allow.
        Parameters:
        a - the left operand
        b - the right operand
        Returns:
        true if both agree on every domain-consistent assignment

      • satisfiableGiven

        public boolean satisfiableGiven​(BoolFormula a)
        Tests satisfiability restricted to the assignments the registered domains allow.
        Parameters:
        a - the formula
        Returns:
        true if some domain-consistent assignment satisfies it

      • overflowed

        public boolean overflowed()
        Reports whether the BDD node budget was exceeded, after which callers must emit from the NNF layer only.
        Returns:
        true once the budget was exceeded

      • evalSyntactic

        public boolean evalSyntactic​(BoolFormula f,
                             boolean[] assignment)
        Evaluates the syntactic NNF layer.
        Parameters:
        f - the formula
        assignment - truth values indexed by atom
        Returns:
        the value of the NNF under that assignment

      • evalCanonical

        public boolean evalCanonical​(BoolFormula f,
                             boolean[] assignment)
        Evaluates the canonical BDD layer by walking from its root to a terminal.
        Parameters:
        f - the formula
        assignment - truth values indexed by atom
        Returns:
        the value of the BDD under that assignment