at.jku.fmv.qbf

Class QBF.ForAll

java.lang.Object

at.jku.fmv.qbf.QBF

at.jku.fmv.qbf.QBF.UnaryOperator

at.jku.fmv.qbf.QBF.Quantifier

at.jku.fmv.qbf.QBF.ForAll

Enclosing class:

QBF

public static final class QBF.ForAll
extends QBF.Quantifier

A universal quantifier.

Author:

phlo

Nested Class Summary

Nested classes/interfaces inherited from class at.jku.fmv.qbf.QBF

QBF.And, QBF.Exists, QBF.False, QBF.ForAll, QBF.MultiaryOperator, QBF.Not, QBF.Or, QBF.Quantifier, QBF.Terminal, QBF.Traverse, QBF.True, QBF.UnaryOperator, QBF.Variable

Field Summary

Fields inherited from class at.jku.fmv.qbf.QBF.Quantifier

variables

Fields inherited from class at.jku.fmv.qbf.QBF.UnaryOperator

subformula

Fields inherited from class at.jku.fmv.qbf.QBF

False, isAnd, isCNF, isConstant, isExists, isForAll, isLiteral, isNegation, isOr, isQuantifier, isVariable, True

Constructor Summary

Constructors

Constructor and Description
ForAll(QBF subformula, Set<String> variables)
ForAll(QBF subformula, String... variables)

Method Summary

Modifier and Type	Method and Description
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.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.

Methods inherited from class at.jku.fmv.qbf.QBF

accept, apply, cleanse, equals, getCriticalPaths, getQPaths, getSkeleton, hash, hashCode, isAnd, isCNF, isConstant, isExists, isForAll, isLiteral, isNegation, isOr, isQuantifier, isVariable, negate, prefixToString, quantifierToString, rename, stream, streamBoundVariables, streamFreeVariables, streamPrefix, streamQPaths, streamVariables, toNNF, toPCNF, toPNF, toString, unifyPrefix

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Constructor Detail

ForAll

public ForAll(QBF subformula,
              Set<String> variables)

ForAll

public ForAll(QBF subformula,
              String... variables)

Method Detail

accept

public 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)

Description copied from class: QBF

Applies a given Consumer to the underlying concrete type.

Specified by:

accept in class QBF

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

apply

public <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)

Description copied from class: QBF

Applies a given Function to the underlying concrete type.

Specified by:

apply in class QBF

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