at.jku.fmv.qbf

Class QBF.Exists

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.Exists

Enclosing class:

QBF

public static final class QBF.Exists
extends QBF.Quantifier

An existential 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
Exists(QBF subformula, Set<String> variables)
Exists(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

Exists

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

Exists

public Exists(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