QBF

java.lang.Object
- at.jku.fmv.qbf.QBF

Direct Known Subclasses:

QBF.MultiaryOperator, QBF.Terminal, QBF.UnaryOperator
```
public abstract class QBF
extends Object
```
A quantified boolean formula.
QBF is an immutable data structure, representing quantified boolean formula trees containing the following connectives:
- ¬ (negation)
- ∧ (conjunction)
- ∨ (disjunction)
- ∀ (universal quantification)
- ∃ (existential quantification)
Author:

phlo

Nested Class Summary

Nested Classes
Modifier and Type	Class and Description
`static class`	`QBF.And` A conjunction.
`static class`	`QBF.Exists` An existential quantifier.
`static class`	`QBF.False` The boolean constant `false`.
`static class`	`QBF.ForAll` A universal quantifier.
`static class`	`QBF.MultiaryOperator` Base class for multiary (n-ary) operators.
`static class`	`QBF.Not` A negation.
`static class`	`QBF.Or` A disjunction.
`static class`	`QBF.Quantifier` Base class for quantifier nodes.
`static class`	`QBF.Terminal` A terminal node in the QBF tree.
`static class`	`QBF.Traverse` Tree traversal order.
`static class`	`QBF.True` The boolean constant `true`.
`static class`	`QBF.UnaryOperator` Base class for unary operators.
`static class`	`QBF.Variable` A variable.

Field Summary

Fields
Modifier and Type	Field and Description
`static QBF`	`False` Singleton instance of the boolean constant `false`.
`static Predicate<QBF>`	`isAnd` Tests if the given instance is a `conjunction`.
`static Predicate<QBF>`	`isCNF` Tests if the given instance is in conjunctive normal form.
`static Predicate<QBF>`	`isConstant` Tests if the given instance is a boolean constant.
`static Predicate<QBF>`	`isExists` Tests if the given instance is a `existential quantifier`.
`static Predicate<QBF>`	`isForAll` Tests if the given instance is a `universal quantifier`.
`static Predicate<QBF>`	`isLiteral` Tests if the given instance is a literal.
`static Predicate<QBF>`	`isNegation` Tests if the given instance is a `negation`.
`static Predicate<QBF>`	`isOr` Tests if the given instance is a `disjunction`.
`static Predicate<QBF>`	`isQuantifier` Tests if the given instance is a quantifier.
`static Predicate<QBF>`	`isVariable` Tests if the given instance is a `variable`.
`static QBF`	`True` Singleton instance of the boolean constant `true`.

Method Summary

All Methods Static Methods Instance Methods Abstract Methods Concrete Methods Deprecated Methods
Modifier and Type	Method and Description
`void`	`accept(Consumer<QBF.ForAll> forall, Consumer<QBF.Exists> exists)` Applies a given `Consumer` to a quantifier.
`abstract void`	`accept(Consumer<QBF.True> t, Consumer<QBF.False> f, Consumer<QBF.Variable> var, Consumer<QBF.Not> not, Consumer<QBF.And> and, Consumer<QBF.Or> or, Consumer<QBF.ForAll> forall, Consumer<QBF.Exists> exists)` Applies a given `Consumer` to the underlying concrete type.
`<T> T`	`apply(Function<QBF.ForAll,T> forall, Function<QBF.Exists,T> exists)` Applies a given `Function` to a quantifier.
`abstract <T> T`	`apply(Function<QBF.True,T> t, Function<QBF.False,T> f, Function<QBF.Variable,T> var, Function<QBF.Not,T> not, Function<QBF.And,T> and, Function<QBF.Or,T> or, Function<QBF.ForAll,T> forall, Function<QBF.Exists,T> exists)` Applies a given `Function` to the underlying concrete type.
`QBF`	`cleanse()` Produces a cleansed formula.
`boolean`	`equals(Object o)`
`static List<QBF>`	`getCriticalPaths(List<QBF> qpaths)` Gets a list of critical q-paths.
`List<QBF>`	`getQPaths()` Gets a list of this formula's q-paths.
`QBF`	`getSkeleton()` Gets the propositional skeleton of this formula.
`protected int`	`hash()`
`int`	`hashCode()`
`boolean`	`isAnd()` Tests if this is a `conjunction`.
`boolean`	`isCNF()` Tests if this formula is in conjunctive normal form.
`boolean`	`isConstant()` Tests if this is a boolean constant.
`boolean`	`isExists()` Tests if this is a `existential quantifier`.
`boolean`	`isForAll()` Tests if this is a `universal quantifier`.
`boolean`	`isLiteral()` Tests if this is a literal.
`boolean`	`isNegation()` Tests if this is a `negation`.
`boolean`	`isOr()` Tests if this is a `disjunction`.
`boolean`	`isQuantifier()` Tests if this is a quantifier.
`boolean`	`isVariable()` Tests if this is a `variable`.
`QBF`	`negate()` Negates the current formula.
`String`	`prefixToString()` Gets a String representation of this formula's prefix.
`static String`	`quantifierToString(QBF.Quantifier q)` Gets a String representation of the given quantifier.
`QBF`	`rename(Map<String,String> variables)` Renames this formula's variables.
`Stream<QBF>`	`stream(QBF.Traverse traversal)` Streams the formula's nodes in a depth-first search manner.
`Stream<String>`	`streamBoundVariables()` Streams all bound variables in this formula.
`Stream<String>`	`streamFreeVariables()` Streams all free variables in this formula.
`Stream<QBF.Quantifier>`	`streamPrefix()` Streams this formula's prefix.
`Stream<QBF>`	`streamQPaths()` Streams this formula's q-paths.
`Stream<String>`	`streamVariables()` Streams all variables in this formula.
`QBF`	`toNNF()` Transforms this formula into negated normal form.
`QBF`	`toPCNF(PrenexingStrategy strategy, CNFEncoder encoder)` Transforms this formula into prenex conjunctive normal form.
`QBF`	`toPNF(PrenexingStrategy strategy)` Transforms this formula into prenex normal form.
`String`	`toString()`
`QBF`	`unifyPrefix()` Deprecated.

Methods inherited from class java.lang.Object
clone, finalize, getClass, notify, notifyAll, wait, wait, wait

- Field Detail
  - True
```
public static final QBF True
```
    Singleton instance of the boolean constant true.
  - False
```
public static final QBF False
```
    Singleton instance of the boolean constant false.
  - isConstant
```
public static final Predicate<QBF> isConstant
```
    Tests if the given instance is a boolean constant.
  - isQuantifier
```
public static final Predicate<QBF> isQuantifier
```
    Tests if the given instance is a quantifier.
  - isForAll
```
public static final Predicate<QBF> isForAll
```
    Tests if the given instance is a universal quantifier.
  - isExists
```
public static final Predicate<QBF> isExists
```
    Tests if the given instance is a existential quantifier.
  - isVariable
```
public static final Predicate<QBF> isVariable
```
    Tests if the given instance is a variable.
  - isLiteral
```
public static final Predicate<QBF> isLiteral
```
    Tests if the given instance is a literal.
  - isNegation
```
public static final Predicate<QBF> isNegation
```
    Tests if the given instance is a negation.
  - isAnd
```
public static final Predicate<QBF> isAnd
```
    Tests if the given instance is a conjunction.
  - isOr
```
public static final Predicate<QBF> isOr
```
    Tests if the given instance is a disjunction.
  - isCNF
```
public static final Predicate<QBF> isCNF
```
    Tests if the given instance is in conjunctive normal form.
- Method Detail
  - accept
```
public abstract void accept(Consumer<QBF.True> t,
                            Consumer<QBF.False> f,
                            Consumer<QBF.Variable> var,
                            Consumer<QBF.Not> not,
                            Consumer<QBF.And> and,
                            Consumer<QBF.Or> or,
                            Consumer<QBF.ForAll> forall,
                            Consumer<QBF.Exists> exists)
```
    Applies a given Consumer to the underlying concrete type.
    
    Parameters:
    
    t - Consumer accepting the boolean constant true
    
    f - Consumer accepting the boolean constant false
    
    var - Consumer accepting variables
    
    not - Consumer accepting negations
    
    and - Consumer accepting conjunctions
    
    or - Consumer accepting disjunctions
    
    forall - Consumer accepting universal quantifiers
    
    exists - Consumer accepting existential quantifiers
  - accept
```
public void accept(Consumer<QBF.ForAll> forall,
                   Consumer<QBF.Exists> exists)
```
    Applies a given Consumer to a quantifier.
    
    Parameters:
    
    forall - Consumer accepting universal quantifiers
    
    exists - Consumer accepting existential quantifiers
    
    Throws:
    
    IllegalArgumentException - if this is not a quantifier
  - apply
```
public abstract <T> T apply(Function<QBF.True,T> t,
                            Function<QBF.False,T> f,
                            Function<QBF.Variable,T> var,
                            Function<QBF.Not,T> not,
                            Function<QBF.And,T> and,
                            Function<QBF.Or,T> or,
                            Function<QBF.ForAll,T> forall,
                            Function<QBF.Exists,T> exists)
```
    Applies a given Function to the underlying concrete type.
    
    Type Parameters:
    
    T - return type
    
    Parameters:
    
    t - Function accepting the boolean constant true
    
    f - Function accepting the boolean constant false
    
    var - Function accepting variables
    
    not - Function accepting negations
    
    and - Function accepting conjunctions
    
    or - Function accepting disjunctions
    
    forall - Function accepting universal quantifiers
    
    exists - Function accepting existential quantifiers
    
    Returns:
    
    result of the Function application
  - apply
```
public <T> T apply(Function<QBF.ForAll,T> forall,
                   Function<QBF.Exists,T> exists)
```
    Applies a given Function to a quantifier.
    
    Type Parameters:
    
    T - return type
    
    Parameters:
    
    forall - Function accepting universal quantifiers
    
    exists - Function accepting existential quantifiers
    
    Returns:
    
    result of the Function application
    
    Throws:
    
    IllegalArgumentException - if this is not a quantifier
  - isConstant
```
public boolean isConstant()
```
    Tests if this is a boolean constant.
    
    Returns:
    
    true if this is either QBF.True or QBF.False
  - isQuantifier
```
public boolean isQuantifier()
```
    Tests if this is a quantifier.
    
    Returns:
    
    true if this is either QBF.ForAll or QBF.Exists
  - isForAll
```
public boolean isForAll()
```
    Tests if this is a universal quantifier.
    
    Returns:
    
    true if this is a universal quantifier
  - isExists
```
public boolean isExists()
```
    Tests if this is a existential quantifier.
    
    Returns:
    
    true if this is a existential quantifier
  - isVariable
```
public boolean isVariable()
```
    Tests if this is a variable.
    
    Returns:
    
    true if this is a variable
  - isLiteral
```
public boolean isLiteral()
```
    Tests if this is a literal.
    
    Returns:
    
    true if this is a literal.
  - isNegation
```
public boolean isNegation()
```
    Tests if this is a negation.
    
    Returns:
    
    true if this is a negation
  - isAnd
```
public boolean isAnd()
```
    Tests if this is a conjunction.
    
    Returns:
    
    true if this is a conjunction
  - isOr
```
public boolean isOr()
```
    Tests if this is a disjunction.
    
    Returns:
    
    true if this is a disjunction
  - isCNF
```
public boolean isCNF()
```
    Tests if this formula is in conjunctive normal form.
    
    Returns:
    
    true if this is in conjunctive normal form
  - hash
```
protected int hash()
```
  - hashCode
```
public int hashCode()
```
    Overrides:
    
    hashCode in class Object
  - equals
```
public boolean equals(Object o)
```
    Overrides:
    
    equals in class Object
  - stream
```
public Stream<QBF> stream(QBF.Traverse traversal)
```
    Streams the formula's nodes in a depth-first search manner.
    
    Parameters:
    
    traversal - pre- or post-order
    
    Returns:
    
    a sequential Stream over all nodes in this formula
  - streamVariables
```
public Stream<String> streamVariables()
```
    Streams all variables in this formula.
    
    Returns:
    
    a sequential Stream over all variables in this formula
  - streamFreeVariables
```
public Stream<String> streamFreeVariables()
```
    Streams all free variables in this formula.
    
    Returns:
    
    a sequential Stream over all free variables in this formula
  - streamBoundVariables
```
public Stream<String> streamBoundVariables()
```
    Streams all bound variables in this formula.
    
    Returns:
    
    a sequential Stream over all bound variables in this formula
  - streamPrefix
```
public Stream<QBF.Quantifier> streamPrefix()
```
    Streams this formula's prefix.
    
    Returns:
    
    a sequential Stream over this formula's prefix
  - streamQPaths
```
public Stream<QBF> streamQPaths()
```
    Streams this formula's q-paths.
    The set of q-paths of Φ, qpaths(Φ), is defined inductively as follows:
    1. If Φ is a variable, QBF.True or QBF.False, then qpaths(Φ) = {}.
    2. If Φ = ¬Φ1, then qpaths(Φ) = {Q̄1 p1 ... Q̄k pk | Q1 p1 ... Qk pk ∈ qpaths(Φ1)}.
    3. If Φ = Φ1 ◦ Φ 2 (◦ ∈ {∧, ∨}), then qpaths(Φ) = qpaths(Φ1) ∪ qpaths(Φ2).
    4. If Φ = Φ1 → Φ2, then qpaths(Φ) = qpaths(¬Φ1 ∨ Φ2).
    5. If Φ = Qp Φ1 (Q ∈ {∀, ∃}), then qpaths(Φ) = {Q ps | s ∈ qpaths(Φ1)}.
    Note: only the q-path's head node is returned, use streamPrefix() to get the full path.
    Returns:
    
    a sequential Stream over this formula's q-paths
  - getQPaths
```
public List<QBF> getQPaths()
```
    Gets a list of this formula's q-paths.
    The set of q-paths of Φ, qpaths(Φ), is defined inductively as follows:
    1. If Φ is a variable, QBF.True or QBF.False, then qpaths(Φ) = {}.
    2. If Φ = ¬Φ1, then qpaths(Φ) = {Q̄1 p1 ... Q̄k pk | Q1 p1 ... Qk pk ∈ qpaths(Φ1)}.
    3. If Φ = Φ1 ◦ Φ 2 (◦ ∈ {∧, ∨}), then qpaths(Φ) = qpaths(Φ1) ∪ qpaths(Φ2).
    4. If Φ = Φ1 → Φ2, then qpaths(Φ) = qpaths(¬Φ1 ∨ Φ2).
    5. If Φ = Qp Φ1 (Q ∈ {∀, ∃}), then qpaths(Φ) = {Q ps | s ∈ qpaths(Φ1)}.
    Note: only the q-path's head node is returned, use streamPrefix() to get the full path.
    Returns:
    
    a list of this formula's q-paths
  - getCriticalPaths
```
public static List<QBF> getCriticalPaths(List<QBF> qpaths)
```
    Gets a list of critical q-paths.
    A critical path is defined by having the largest number of quantifier alterations.
    
    Parameters:
    
    qpaths - a list of q-paths
    
    Returns:
    
    a list of critical paths
  - getSkeleton
```
public QBF getSkeleton()
```
    Gets the propositional skeleton of this formula.
    The propositional skeleton of a QBF Φ is given by deleting all quantifiers in Φ.
    
    Returns:
    
    the propositional skeleton
  - unifyPrefix
```
@Deprecated
public QBF unifyPrefix()
```
    Deprecated.
    
    Unifies all sequences of equal quantifiers in the formula's prefix. Example: ∀x: ∀y: ϕ → ∀x,y: ϕ
    
    Returns:
    
    this QBF with purely alternating prefix
  - negate
```
public QBF negate()
```
    Negates the current formula.
    
    Returns:
    
    this QBF's negation
  - rename
```
public QBF rename(Map<String,String> variables)
```
    Renames this formula's variables.
    
    Parameters:
    
    variables - a map of old to new variable names
    
    Returns:
    
    this QBF with renamed variables
  - cleanse
```
public QBF cleanse()
```
    Produces a cleansed formula.
    1. a variable is only quantified once
    2. a variable is either quantified or free
    3. quantifiers have all bound variables in their scope
    4. variables are renamed to integers in order of their occurrence, starting from 1:
      
      bound variables: [1, #bound]
      free variables: ]#bound, #variables]
    Returns:
    
    the cleansed QBF
  - toNNF
```
public QBF toNNF()
```
    Transforms this formula into negated normal form.
    
    Returns:
    
    this QBF in negated normal form
  - toPNF
```
public QBF toPNF(PrenexingStrategy strategy)
```
    Transforms this formula into prenex normal form.
    
    Parameters:
    
    strategy - prenexing strategy
    
    Returns:
    
    this QBF in prenex normal form
  - toPCNF
```
public QBF toPCNF(PrenexingStrategy strategy,
                  CNFEncoder encoder)
```
    Transforms this formula into prenex conjunctive normal form.
    
    Parameters:
    
    strategy - prenexing strategy
    
    encoder - CNF encoder
    
    Returns:
    
    this QBF in prenex conjunctive normal form
  - quantifierToString
```
public static String quantifierToString(QBF.Quantifier q)
```
    Gets a String representation of the given quantifier.
    
    Parameters:
    
    q - a quantifier
    
    Returns:
    
    the quantifier's String representation
  - prefixToString
```
public String prefixToString()
```
    Gets a String representation of this formula's prefix.
    
    Returns:
    
    this formulas prefix as String
  - toString
```
public String toString()
```
    Overrides:
    
    toString in class Object

Class QBF

Nested Class Summary

Field Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

True

False

isConstant

isQuantifier

isForAll

isExists

isVariable

isLiteral

isNegation

isAnd

isOr

isCNF

Method Detail

accept

accept

apply

apply

isConstant

isQuantifier

isForAll

isExists

isVariable

isLiteral

isNegation

isAnd

isOr

isCNF

hash

hashCode

equals

stream

streamVariables

streamFreeVariables

streamBoundVariables

streamPrefix

streamQPaths

getQPaths

getCriticalPaths

getSkeleton

unifyPrefix

negate

rename

cleanse

toNNF

toPNF

toPCNF

quantifierToString

prefixToString

toString