A B C D E F G H I M P R S T U V

A

accept(FormulaVisitor) - Method in class edu.kit.iti.lfm.spotlight.Formula

Entry point for a FormulaVisitor.

accept(FormulaVisitor) - Method in class edu.kit.iti.lfm.spotlight.Formula.And

accept(FormulaVisitor) - Method in class edu.kit.iti.lfm.spotlight.Formula.Equiv

accept(FormulaVisitor) - Method in class edu.kit.iti.lfm.spotlight.Formula.Impl

accept(FormulaVisitor) - Method in class edu.kit.iti.lfm.spotlight.Formula.Literal

accept(FormulaVisitor) - Method in class edu.kit.iti.lfm.spotlight.Formula.Not

accept(FormulaVisitor) - Method in class edu.kit.iti.lfm.spotlight.Formula.Or

addClause(int...) - Method in class edu.kit.iti.lfm.spotlight.SATSolver

Add a single clause to the solver.

addClause(int[], int, int) - Method in class edu.kit.iti.lfm.spotlight.SATSolver

Add a single clause constructed from a part of an array to the solver.

addClause(Clause) - Method in class edu.kit.iti.lfm.spotlight.SATSolver

Add a single clause to the solver.

B

Board - Class in edu.kit.iti.lfm.spotlight

The board class is used to provide all necessary information on a Spotlight board which is a rectangular matrix of Field elements.

BoardComponent - Class in edu.kit.iti.lfm.spotlight

This class is used to display a Board on the screen.

BoardComponent(Board) - Constructor for class edu.kit.iti.lfm.spotlight.BoardComponent

Instantiates a new board component.

C

Clause - Class in edu.kit.iti.lfm.spotlight

The Class Clause represents DIMACS clauses.

Clause(int...) - Constructor for class edu.kit.iti.lfm.spotlight.Clause

Instantiates a new clause from a list of literals.

Clause(int[], int, int) - Constructor for class edu.kit.iti.lfm.spotlight.Clause

Instantiates a new clause from a segment of an integer array

colorFields(String) - Method in class edu.kit.iti.lfm.spotlight.Board

colorFields(int[]) - Method in class edu.kit.iti.lfm.spotlight.Board

concat(int) - Method in class edu.kit.iti.lfm.spotlight.Clause

Get a clause that represents this clause augmented by an additional literal.

concat(Clause) - Method in class edu.kit.iti.lfm.spotlight.Clause

Get a clause that represents this clause augmented by the literals of the argument.

containsCoordinates(int, int) - Method in class edu.kit.iti.lfm.spotlight.Board

Check whether the coordinates refer to a field on the board.

countColumns() - Method in class edu.kit.iti.lfm.spotlight.Board

Get the number of columns on the board, i.e., its width.

countRows() - Method in class edu.kit.iti.lfm.spotlight.Board

Get the number of rows on the board, i.e., its height.

countSubFormulas() - Method in class edu.kit.iti.lfm.spotlight.Formula

Get the number of direct subformulas for this formula.

D

depth - Static variable in class edu.kit.iti.lfm.spotlight.Formula

E

edu.kit.iti.lfm.spotlight - package edu.kit.iti.lfm.spotlight

equals(Object) - Method in class edu.kit.iti.lfm.spotlight.Formula

Indicate whether some other object is "equal to" this one.

F

FALSE - Static variable in class edu.kit.iti.lfm.spotlight.Formula

Field - Class in edu.kit.iti.lfm.spotlight

This class represents a single field on a Spotlight Board.

Field(int, int, int, Field.Direction, Field.FieldColor) - Constructor for class edu.kit.iti.lfm.spotlight.Field

Instantiates a new field.

Field.Direction - Enum in edu.kit.iti.lfm.spotlight

This enumeration lists the possible directions for arrows in fields of Boards.

Field.FieldColor - Enum in edu.kit.iti.lfm.spotlight

This declaration enumerates the colors that a field can take.

FIELD_SIZE - Static variable in class edu.kit.iti.lfm.spotlight.BoardComponent

The size of a single field on the board in pixels

Formula - Class in edu.kit.iti.lfm.spotlight

This class is the abstract base class to model propositional formulas of arbitrary structure.

Formula.And - Class in edu.kit.iti.lfm.spotlight

Propositional conjunction The conjunction takes two subformulas.

Formula.And(Formula, Formula) - Constructor for class edu.kit.iti.lfm.spotlight.Formula.And

Instantiate a new conjunction.

Formula.Equiv - Class in edu.kit.iti.lfm.spotlight

Propositional equivalence The equivalence takes two subformulas.

Formula.Equiv(Formula, Formula) - Constructor for class edu.kit.iti.lfm.spotlight.Formula.Equiv

Instantiate a new equivalence.

Formula.Impl - Class in edu.kit.iti.lfm.spotlight

Propositional implication The implication takes two subformulas.

Formula.Impl(Formula, Formula) - Constructor for class edu.kit.iti.lfm.spotlight.Formula.Impl

Instantiate a new implication.

Formula.Literal - Class in edu.kit.iti.lfm.spotlight

Prositional literal Literals are the basic blocks of formulas.

Formula.Literal(int) - Constructor for class edu.kit.iti.lfm.spotlight.Formula.Literal

Instantiate a new literal.

Formula.Not - Class in edu.kit.iti.lfm.spotlight

Propositional negation The negation takes one subformula.

Formula.Not(Formula) - Constructor for class edu.kit.iti.lfm.spotlight.Formula.Not

Instantiate a new negated formula.

Formula.Or - Class in edu.kit.iti.lfm.spotlight

Propositional disjunction The disjunction takes two subformulas.

Formula.Or(Formula, Formula) - Constructor for class edu.kit.iti.lfm.spotlight.Formula.Or

Instantiate a new disjunction.

FormulaVisitor - Interface in edu.kit.iti.lfm.spotlight

The interface FormulaVisitor models the visitor for Formulas according to the visitor pattern.

fromFile(File) - Static method in class edu.kit.iti.lfm.spotlight.Board

Extract a board from the contents of file.

fromStringDescription(String) - Static method in class edu.kit.iti.lfm.spotlight.Board

Extract a board from a string description.

G

getClauses() - Method in class edu.kit.iti.lfm.spotlight.SATSolver

Get the list of all clauses added to the solver.

getColor() - Method in class edu.kit.iti.lfm.spotlight.Field

Gets the color of this field.

getColoringString() - Method in class edu.kit.iti.lfm.spotlight.Board

Gets a string representation of the coloured board.

getColumn() - Method in class edu.kit.iti.lfm.spotlight.Field

Gets the column on the board.

getColumnOffset() - Method in enum edu.kit.iti.lfm.spotlight.Field.Direction

getColumnOffset() - Method in class edu.kit.iti.lfm.spotlight.Field

Gets the column component of the direction of the arrow as an offset.

getConstraint() - Method in class edu.kit.iti.lfm.spotlight.Field

Gets the constraint of this field.

getDirection() - Method in class edu.kit.iti.lfm.spotlight.Field

Gets the direction.

getField(int, int) - Method in class edu.kit.iti.lfm.spotlight.Board

Gets a field on the board

getMaximumVariable() - Method in class edu.kit.iti.lfm.spotlight.SATSolver

Get the highest variable index amongst all clauses in the solver.

getMaxVar() - Method in class edu.kit.iti.lfm.spotlight.Clause

Get the largest index of all literals in the clause.

getRegion(Board) - Method in class edu.kit.iti.lfm.spotlight.Field

Get the region of Fields this field points to.

getRegionForField(int, int) - Method in class edu.kit.iti.lfm.spotlight.Board

Get the region an arrow points to.

getRow() - Method in class edu.kit.iti.lfm.spotlight.Field

Gets the row of this field on the board.

getRowOffset() - Method in enum edu.kit.iti.lfm.spotlight.Field.Direction

getRowOffset() - Method in class edu.kit.iti.lfm.spotlight.Field

Gets the row component of the direction of the arrow as an offset.

getSequentialIndex(Field) - Method in class edu.kit.iti.lfm.spotlight.Board

The sequential index of a field in the board, e.g. for usage as propositional atom.

getSequentialIndex(Board) - Method in class edu.kit.iti.lfm.spotlight.Field

The sequential index of this field in the board given by the parameter, e.g. for usage as propositional atom.

getSubFormula(int) - Method in class edu.kit.iti.lfm.spotlight.Formula

Get a sub formula of this formula.

getValue() - Method in class edu.kit.iti.lfm.spotlight.Formula.Literal

getVar() - Method in class edu.kit.iti.lfm.spotlight.Formula.Literal

getVariable(int) - Method in class edu.kit.iti.lfm.spotlight.Clause

H

hashCode() - Method in class edu.kit.iti.lfm.spotlight.Formula

Return a hash code value for the object.

I

ISpotlightSolver - Interface in edu.kit.iti.lfm.spotlight

This interface ISpotlightSolver must be implemented for the assignment in "Formale Systeme 11/12".

iterator() - Method in class edu.kit.iti.lfm.spotlight.Board

Get an iterator going over all fields on the board.

M

main(String[]) - Static method in class edu.kit.iti.lfm.spotlight.BoardComponent

For testing purposes only

MINISAT_EXECUTABLE - Static variable in class edu.kit.iti.lfm.spotlight.SATSolver

If the MiniSat executable is not your search path for executables, you can specify its absolute location here.

MINISAT_KEEP - Static variable in class edu.kit.iti.lfm.spotlight.SATSolver

for debug: keep the input/output files from minisat.

P

paintComponent(Graphics) - Method in class edu.kit.iti.lfm.spotlight.BoardComponent

R

readFileAsString(File) - Static method in class edu.kit.iti.lfm.spotlight.Board

Read a file into a string.

S

SATSolver - Class in edu.kit.iti.lfm.spotlight

The class SATSolver provides an interface to a satisfiability solver.

SATSolver() - Constructor for class edu.kit.iti.lfm.spotlight.SATSolver

setColor(Field.FieldColor) - Method in class edu.kit.iti.lfm.spotlight.Field

Sets the color of this field.

solve(Board) - Method in interface edu.kit.iti.lfm.spotlight.ISpotlightSolver

Solve a Spotlight puzzle.

solve() - Method in class edu.kit.iti.lfm.spotlight.SATSolver

Invoke the SAT solver and return a satisfying variable assignment if one has been found.

SpotlightException - Exception in edu.kit.iti.lfm.spotlight

This exception class is used whenever a declared exception is thrown in the framework.

SpotlightException() - Constructor for exception edu.kit.iti.lfm.spotlight.SpotlightException

Constructs a new exception with null as its detail message.

SpotlightException(String) - Constructor for exception edu.kit.iti.lfm.spotlight.SpotlightException

Constructs a new exception with the specified detail message.

SpotlightException(Throwable) - Constructor for exception edu.kit.iti.lfm.spotlight.SpotlightException

Constructs a new exception with the specified cause and a detail message of (cause==null ?

SpotlightException(String, Throwable) - Constructor for exception edu.kit.iti.lfm.spotlight.SpotlightException

Constructs a new exception with the specified detail message and cause.

T

toArray() - Method in class edu.kit.iti.lfm.spotlight.Clause

Extract the integer values of this clause into an array.

toDescriptionString() - Method in class edu.kit.iti.lfm.spotlight.Board

Boards (i.e., signs and constraints, but not colors) can be written to a file.

toDIMACS() - Method in class edu.kit.iti.lfm.spotlight.Clause

Translate the clause to DIMACS text representation.

toString() - Method in class edu.kit.iti.lfm.spotlight.Board

toString() - Method in class edu.kit.iti.lfm.spotlight.Clause

A clause is textually represented as a list in curly braces.

toString() - Method in class edu.kit.iti.lfm.spotlight.Field

toString() - Method in class edu.kit.iti.lfm.spotlight.Formula.And

toString() - Method in class edu.kit.iti.lfm.spotlight.Formula.Equiv

toString() - Method in class edu.kit.iti.lfm.spotlight.Formula.Impl

toString() - Method in class edu.kit.iti.lfm.spotlight.Formula.Literal

toString() - Method in class edu.kit.iti.lfm.spotlight.Formula.Not

toString() - Method in class edu.kit.iti.lfm.spotlight.Formula.Or

toString() - Method in class edu.kit.iti.lfm.spotlight.Formula

Return a string representation of the object.

TRUE - Static variable in class edu.kit.iti.lfm.spotlight.Formula

U

USE_MINISAT - Static variable in class edu.kit.iti.lfm.spotlight.SATSolver

switch between sat4j and minisat.

V

valueOf(String) - Static method in enum edu.kit.iti.lfm.spotlight.Field.Direction

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

valueOf(String) - Static method in enum edu.kit.iti.lfm.spotlight.Field.FieldColor

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

values() - Static method in enum edu.kit.iti.lfm.spotlight.Field.Direction

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

values() - Static method in enum edu.kit.iti.lfm.spotlight.Field.FieldColor

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

visit(Formula.And) - Method in interface edu.kit.iti.lfm.spotlight.FormulaVisitor

visit(Formula.Or) - Method in interface edu.kit.iti.lfm.spotlight.FormulaVisitor

visit(Formula.Impl) - Method in interface edu.kit.iti.lfm.spotlight.FormulaVisitor

visit(Formula.Equiv) - Method in interface edu.kit.iti.lfm.spotlight.FormulaVisitor

visit(Formula.Not) - Method in interface edu.kit.iti.lfm.spotlight.FormulaVisitor

visit(Formula.Literal) - Method in interface edu.kit.iti.lfm.spotlight.FormulaVisitor

visualise() - Method in class edu.kit.iti.lfm.spotlight.Board

Open a new frame and visualize the current board in this frame.

A B C D E F G H I M P R S T U V