A C E F G H I M N O P Q R S T U V W

A

accept(Consumer<QBF.True>, Consumer<QBF.False>, Consumer<QBF.Variable>, Consumer<QBF.Not>, Consumer<QBF.And>, Consumer<QBF.Or>, Consumer<QBF.ForAll>, Consumer<QBF.Exists>) - Method in class at.jku.fmv.qbf.QBF

Applies a given Consumer to the underlying concrete type.

accept(Consumer<QBF.ForAll>, Consumer<QBF.Exists>) - Method in class at.jku.fmv.qbf.QBF

Applies a given Consumer to a quantifier.

accept(Consumer<QBF.True>, Consumer<QBF.False>, Consumer<QBF.Variable>, Consumer<QBF.Not>, Consumer<QBF.And>, Consumer<QBF.Or>, Consumer<QBF.ForAll>, Consumer<QBF.Exists>) - Method in class at.jku.fmv.qbf.QBF.And

accept(Consumer<QBF.True>, Consumer<QBF.False>, Consumer<QBF.Variable>, Consumer<QBF.Not>, Consumer<QBF.And>, Consumer<QBF.Or>, Consumer<QBF.ForAll>, Consumer<QBF.Exists>) - Method in class at.jku.fmv.qbf.QBF.Exists

accept(Consumer<QBF.True>, Consumer<QBF.False>, Consumer<QBF.Variable>, Consumer<QBF.Not>, Consumer<QBF.And>, Consumer<QBF.Or>, Consumer<QBF.ForAll>, Consumer<QBF.Exists>) - Method in class at.jku.fmv.qbf.QBF.False

accept(Consumer<QBF.True>, Consumer<QBF.False>, Consumer<QBF.Variable>, Consumer<QBF.Not>, Consumer<QBF.And>, Consumer<QBF.Or>, Consumer<QBF.ForAll>, Consumer<QBF.Exists>) - Method in class at.jku.fmv.qbf.QBF.ForAll

accept(Consumer<QBF.True>, Consumer<QBF.False>, Consumer<QBF.Variable>, Consumer<QBF.Not>, Consumer<QBF.And>, Consumer<QBF.Or>, Consumer<QBF.ForAll>, Consumer<QBF.Exists>) - Method in class at.jku.fmv.qbf.QBF.Not

accept(Consumer<QBF.True>, Consumer<QBF.False>, Consumer<QBF.Variable>, Consumer<QBF.Not>, Consumer<QBF.And>, Consumer<QBF.Or>, Consumer<QBF.ForAll>, Consumer<QBF.Exists>) - Method in class at.jku.fmv.qbf.QBF.Or

accept(Consumer<QBF.True>, Consumer<QBF.False>, Consumer<QBF.Variable>, Consumer<QBF.Not>, Consumer<QBF.And>, Consumer<QBF.Or>, Consumer<QBF.ForAll>, Consumer<QBF.Exists>) - Method in class at.jku.fmv.qbf.QBF.True

accept(Consumer<QBF.True>, Consumer<QBF.False>, Consumer<QBF.Variable>, Consumer<QBF.Not>, Consumer<QBF.And>, Consumer<QBF.Or>, Consumer<QBF.ForAll>, Consumer<QBF.Exists>) - Method in class at.jku.fmv.qbf.QBF.Variable

And(List<QBF>) - Constructor for class at.jku.fmv.qbf.QBF.And

And(QBF...) - Constructor for class at.jku.fmv.qbf.QBF.And

apply(QBF) - Method in interface at.jku.fmv.qbf.pnf.PrenexingStrategy

Applies the prenexing strategy to the given formula.

apply(QBF) - Method in class at.jku.fmv.qbf.pnf.ShiftingStrategy

apply(Function<QBF.True, T>, Function<QBF.False, T>, Function<QBF.Variable, T>, Function<QBF.Not, T>, Function<QBF.And, T>, Function<QBF.Or, T>, Function<QBF.ForAll, T>, Function<QBF.Exists, T>) - Method in class at.jku.fmv.qbf.QBF.And

apply(Function<QBF.True, T>, Function<QBF.False, T>, Function<QBF.Variable, T>, Function<QBF.Not, T>, Function<QBF.And, T>, Function<QBF.Or, T>, Function<QBF.ForAll, T>, Function<QBF.Exists, T>) - Method in class at.jku.fmv.qbf.QBF

Applies a given Function to the underlying concrete type.

apply(Function<QBF.ForAll, T>, Function<QBF.Exists, T>) - Method in class at.jku.fmv.qbf.QBF

Applies a given Function to a quantifier.

apply(Function<QBF.True, T>, Function<QBF.False, T>, Function<QBF.Variable, T>, Function<QBF.Not, T>, Function<QBF.And, T>, Function<QBF.Or, T>, Function<QBF.ForAll, T>, Function<QBF.Exists, T>) - Method in class at.jku.fmv.qbf.QBF.Exists

apply(Function<QBF.True, T>, Function<QBF.False, T>, Function<QBF.Variable, T>, Function<QBF.Not, T>, Function<QBF.And, T>, Function<QBF.Or, T>, Function<QBF.ForAll, T>, Function<QBF.Exists, T>) - Method in class at.jku.fmv.qbf.QBF.False

apply(Function<QBF.True, T>, Function<QBF.False, T>, Function<QBF.Variable, T>, Function<QBF.Not, T>, Function<QBF.And, T>, Function<QBF.Or, T>, Function<QBF.ForAll, T>, Function<QBF.Exists, T>) - Method in class at.jku.fmv.qbf.QBF.ForAll

apply(Function<QBF.True, T>, Function<QBF.False, T>, Function<QBF.Variable, T>, Function<QBF.Not, T>, Function<QBF.And, T>, Function<QBF.Or, T>, Function<QBF.ForAll, T>, Function<QBF.Exists, T>) - Method in class at.jku.fmv.qbf.QBF.Not

apply(Function<QBF.True, T>, Function<QBF.False, T>, Function<QBF.Variable, T>, Function<QBF.Not, T>, Function<QBF.And, T>, Function<QBF.Or, T>, Function<QBF.ForAll, T>, Function<QBF.Exists, T>) - Method in class at.jku.fmv.qbf.QBF.Or

apply(Function<QBF.True, T>, Function<QBF.False, T>, Function<QBF.Variable, T>, Function<QBF.Not, T>, Function<QBF.And, T>, Function<QBF.Or, T>, Function<QBF.ForAll, T>, Function<QBF.Exists, T>) - Method in class at.jku.fmv.qbf.QBF.True

apply(Function<QBF.True, T>, Function<QBF.False, T>, Function<QBF.Variable, T>, Function<QBF.Not, T>, Function<QBF.And, T>, Function<QBF.Or, T>, Function<QBF.ForAll, T>, Function<QBF.Exists, T>) - Method in class at.jku.fmv.qbf.QBF.Variable

at.jku.fmv.qbf - package at.jku.fmv.qbf

at.jku.fmv.qbf.io - package at.jku.fmv.qbf.io

at.jku.fmv.qbf.io.util - package at.jku.fmv.qbf.io.util

at.jku.fmv.qbf.pcnf - package at.jku.fmv.qbf.pcnf

at.jku.fmv.qbf.pnf - package at.jku.fmv.qbf.pnf

C

cleanse() - Method in class at.jku.fmv.qbf.QBF

Produces a cleansed formula.

CNFEncoder - Interface in at.jku.fmv.qbf.pcnf

A conjunctive normal form encoder.

E

encode(QBF) - Method in interface at.jku.fmv.qbf.pcnf.CNFEncoder

Transforms the given formula from PNF into PCNF.

equals(Object) - Method in class at.jku.fmv.qbf.QBF

Exists(QBF, Set<String>) - Constructor for class at.jku.fmv.qbf.QBF.Exists

Exists(QBF, String...) - Constructor for class at.jku.fmv.qbf.QBF.Exists

ExistsDownForAllUp - Class in at.jku.fmv.qbf.pnf

∃↓∀↑ (prioritizing existential quantifiers)

ExistsDownForAllUp() - Constructor for class at.jku.fmv.qbf.pnf.ExistsDownForAllUp

ExistsUpForAllDown - Class in at.jku.fmv.qbf.pnf

∃↑∀↓ (prioritizing existential quantifiers)

ExistsUpForAllDown() - Constructor for class at.jku.fmv.qbf.pnf.ExistsUpForAllDown

F

False - Static variable in class at.jku.fmv.qbf.QBF

Singleton instance of the boolean constant false.

ForAll(QBF, Set<String>) - Constructor for class at.jku.fmv.qbf.QBF.ForAll

ForAll(QBF, String...) - Constructor for class at.jku.fmv.qbf.QBF.ForAll

ForAllDownExistsDown - Class in at.jku.fmv.qbf.pnf

∀↓∃↓

ForAllDownExistsDown() - Constructor for class at.jku.fmv.qbf.pnf.ForAllDownExistsDown

ForAllDownExistsUp - Class in at.jku.fmv.qbf.pnf

∀↓∃↑ (prioritizing universal quantifiers)

ForAllDownExistsUp() - Constructor for class at.jku.fmv.qbf.pnf.ForAllDownExistsUp

ForAllUpExistsDown - Class in at.jku.fmv.qbf.pnf

∀↑∃↓ (prioritizing universal quantifiers)

ForAllUpExistsDown() - Constructor for class at.jku.fmv.qbf.pnf.ForAllUpExistsDown

ForAllUpExistsUp - Class in at.jku.fmv.qbf.pnf

∀↑∃↑

ForAllUpExistsUp() - Constructor for class at.jku.fmv.qbf.pnf.ForAllUpExistsUp

G

getClauses(QBF) - Method in interface at.jku.fmv.qbf.pcnf.CNFEncoder

Gets a list of clauses for the given propositional skeleton.

getClauses(QBF) - Method in class at.jku.fmv.qbf.pcnf.PG86

getCriticalPaths(List<QBF>) - Static method in class at.jku.fmv.qbf.QBF

Gets a list of critical q-paths.

getQPaths() - Method in class at.jku.fmv.qbf.QBF

Gets a list of this formula's q-paths.

getSkeleton() - Method in class at.jku.fmv.qbf.QBF

Gets the propositional skeleton of this formula.

H

hash() - Method in class at.jku.fmv.qbf.QBF

hashCode() - Method in class at.jku.fmv.qbf.QBF

I

instanceOf(String, Class<? extends T>) - Static method in class main.qcir2pnf

isAnd - Static variable in class at.jku.fmv.qbf.QBF

Tests if the given instance is a conjunction.

isAnd() - Method in class at.jku.fmv.qbf.QBF

Tests if this is a conjunction.

isCNF - Static variable in class at.jku.fmv.qbf.QBF

Tests if the given instance is in conjunctive normal form.

isCNF() - Method in class at.jku.fmv.qbf.QBF

Tests if this formula is in conjunctive normal form.

isConstant - Static variable in class at.jku.fmv.qbf.QBF

Tests if the given instance is a boolean constant.

isConstant() - Method in class at.jku.fmv.qbf.QBF

Tests if this is a boolean constant.

isExists - Static variable in class at.jku.fmv.qbf.QBF

Tests if the given instance is a existential quantifier.

isExists() - Method in class at.jku.fmv.qbf.QBF

Tests if this is a existential quantifier.

isForAll - Static variable in class at.jku.fmv.qbf.QBF

Tests if the given instance is a universal quantifier.

isForAll() - Method in class at.jku.fmv.qbf.QBF

Tests if this is a universal quantifier.

isLiteral - Static variable in class at.jku.fmv.qbf.QBF

Tests if the given instance is a literal.

isLiteral() - Method in class at.jku.fmv.qbf.QBF

Tests if this is a literal.

isNegation - Static variable in class at.jku.fmv.qbf.QBF

Tests if the given instance is a negation.

isNegation() - Method in class at.jku.fmv.qbf.QBF

Tests if this is a negation.

isOr - Static variable in class at.jku.fmv.qbf.QBF

Tests if the given instance is a disjunction.

isOr() - Method in class at.jku.fmv.qbf.QBF

Tests if this is a disjunction.

isQuantifier - Static variable in class at.jku.fmv.qbf.QBF

Tests if the given instance is a quantifier.

isQuantifier() - Method in class at.jku.fmv.qbf.QBF

Tests if this is a quantifier.

isVariable - Static variable in class at.jku.fmv.qbf.QBF

Tests if the given instance is a variable.

isVariable() - Method in class at.jku.fmv.qbf.QBF

Tests if this is a variable.

M

main - package main

main(String[]) - Static method in class main.qcir2pnf

N

name - Variable in class at.jku.fmv.qbf.QBF.Variable

negate() - Method in class at.jku.fmv.qbf.QBF

Negates the current formula.

Not(QBF) - Constructor for class at.jku.fmv.qbf.QBF.Not

O

Or(List<QBF>) - Constructor for class at.jku.fmv.qbf.QBF.Or

Or(QBF...) - Constructor for class at.jku.fmv.qbf.QBF.Or

P

ParserException - Exception in at.jku.fmv.qbf.io.util

ParserException(Throwable) - Constructor for exception at.jku.fmv.qbf.io.util.ParserException

ParserException(Path, String) - Constructor for exception at.jku.fmv.qbf.io.util.ParserException

ParserException(Path, String, int) - Constructor for exception at.jku.fmv.qbf.io.util.ParserException

ParserException(Path, int, Throwable) - Constructor for exception at.jku.fmv.qbf.io.util.ParserException

ParserException(Path, String, Throwable) - Constructor for exception at.jku.fmv.qbf.io.util.ParserException

ParserException(Path, String, int, Throwable) - Constructor for exception at.jku.fmv.qbf.io.util.ParserException

PG86 - Class in at.jku.fmv.qbf.pcnf

An optimized variant of Tseitin transformation [PG86].

PG86() - Constructor for class at.jku.fmv.qbf.pcnf.PG86

prefixToString() - Method in class at.jku.fmv.qbf.QBF

Gets a String representation of this formula's prefix.

PrenexingStrategy - Interface in at.jku.fmv.qbf.pnf

A prenexing strategy.

Q

QBF - Class in at.jku.fmv.qbf

A quantified boolean formula.

QBF.And - Class in at.jku.fmv.qbf

A conjunction.

QBF.Exists - Class in at.jku.fmv.qbf

An existential quantifier.

QBF.False - Class in at.jku.fmv.qbf

The boolean constant false.

QBF.ForAll - Class in at.jku.fmv.qbf

A universal quantifier.

QBF.MultiaryOperator - Class in at.jku.fmv.qbf

Base class for multiary (n-ary) operators.

QBF.Not - Class in at.jku.fmv.qbf

A negation.

QBF.Or - Class in at.jku.fmv.qbf

A disjunction.

QBF.Quantifier - Class in at.jku.fmv.qbf

Base class for quantifier nodes.

QBF.Terminal - Class in at.jku.fmv.qbf

A terminal node in the QBF tree.

QBF.Traverse - Enum in at.jku.fmv.qbf

Tree traversal order.

QBF.True - Class in at.jku.fmv.qbf

The boolean constant true.

QBF.UnaryOperator - Class in at.jku.fmv.qbf

Base class for unary operators.

QBF.Variable - Class in at.jku.fmv.qbf

A variable.

QCIR - Class in at.jku.fmv.qbf.io

A class for reading and writing QCIR-G14 files.

qcir2pnf - Class in main

qcir2pnf() - Constructor for class main.qcir2pnf

QDIMACS - Class in at.jku.fmv.qbf.io

A class for reading and writing QDIMACS files.

quantifierToString(QBF.Quantifier) - Static method in class at.jku.fmv.qbf.QBF

Gets a String representation of the given quantifier.

R

read(Path) - Static method in class at.jku.fmv.qbf.io.QCIR

Reads a given QCIR file.

read(Path) - Static method in class at.jku.fmv.qbf.io.QDIMACS

Reads a given QDIMACS file.

rename(Map<String, String>) - Method in class at.jku.fmv.qbf.QBF

Renames this formula's variables.

S

ShiftingStrategy - Class in at.jku.fmv.qbf.pnf

Abstract class for strategies based on quantifier shifting.

ShiftingStrategy() - Constructor for class at.jku.fmv.qbf.pnf.ShiftingStrategy

SimpleUpDownStrategy - Class in at.jku.fmv.qbf.pnf

Abstract class for strategies based on simple variable reordering.

SimpleUpDownStrategy() - Constructor for class at.jku.fmv.qbf.pnf.SimpleUpDownStrategy

stream(String) - Method in class at.jku.fmv.qbf.io.util.StringTokenizer

stream(QBF.Traverse) - Method in class at.jku.fmv.qbf.QBF

Streams the formula's nodes in a depth-first search manner.

streamBoundVariables() - Method in class at.jku.fmv.qbf.QBF

Streams all bound variables in this formula.

streamFreeVariables() - Method in class at.jku.fmv.qbf.QBF

Streams all free variables in this formula.

streamPrefix() - Method in class at.jku.fmv.qbf.QBF

Streams this formula's prefix.

streamQPaths() - Method in class at.jku.fmv.qbf.QBF

Streams this formula's q-paths.

streamVariables() - Method in class at.jku.fmv.qbf.QBF

Streams all variables in this formula.

StringTokenizer - Class in at.jku.fmv.qbf.io.util

StringTokenizer(char) - Constructor for class at.jku.fmv.qbf.io.util.StringTokenizer

subformula - Variable in class at.jku.fmv.qbf.QBF.UnaryOperator

subformulas - Variable in class at.jku.fmv.qbf.QBF.MultiaryOperator

T

Terminal() - Constructor for class at.jku.fmv.qbf.QBF.Terminal

tokenize(String) - Method in class at.jku.fmv.qbf.io.util.StringTokenizer

toNNF() - Method in class at.jku.fmv.qbf.QBF

Transforms this formula into negated normal form.

toPCNF(PrenexingStrategy, CNFEncoder) - Method in class at.jku.fmv.qbf.QBF

Transforms this formula into prenex conjunctive normal form.

toPNF(PrenexingStrategy) - Method in class at.jku.fmv.qbf.QBF

Transforms this formula into prenex normal form.

toString() - Method in class at.jku.fmv.qbf.QBF

True - Static variable in class at.jku.fmv.qbf.QBF

Singleton instance of the boolean constant true.

U

unifyPrefix() - Method in class at.jku.fmv.qbf.QBF

Deprecated.

V

valueOf(String) - Static method in enum at.jku.fmv.qbf.QBF.Traverse

Returns the enum constant of this type with the specified name.

values() - Static method in enum at.jku.fmv.qbf.QBF.Traverse

Returns an array containing the constants of this enum type, in the order they are declared.

Variable(String) - Constructor for class at.jku.fmv.qbf.QBF.Variable

variables - Variable in class at.jku.fmv.qbf.QBF.Quantifier

W

write(QBF, Path, boolean) - Static method in class at.jku.fmv.qbf.io.QCIR

Writes the given QBF to a QCIR file.

write(QBF, Path) - Static method in class at.jku.fmv.qbf.io.QDIMACS

Writes the given QBF to a QDIMACS file.

writeParallel(QBF, Path, boolean) - Static method in class at.jku.fmv.qbf.io.QCIR

A C E F G H I M N O P Q R S T U V W