forge.util
Class SystemOutReporter

java.lang.Object
  forge.solve.ForgeReporter
      forge.util.SystemOutReporter

public final class SystemOutReporter
extends ForgeReporter

A reporter that prints out basic information to the standard out noting which phase of the translation it is in.

Author:

Greg Dennis (gdennis@mit.edu)

Field Summary

static ForgeReporter

REPORTER

Method Summary

void	buildingAnalysis() Reports that Forge is building an analysis from a given specification and bounds.
void	detectedSymmetries(java.util.Set<?> parts) Reports the symmetries detected by Kodkod as a set of (kodkod.util.ints.IntSet) objects.
void	detectingSymmetries(java.lang.Object bounds) Reports that Kodkod is detecting symmetries in the given bounds (kodkod.instance.Bounds).
void	flattening(java.lang.Object circuit) Reports that Kodkod flattering of the given boolean circuit (kodkod.engine.bool.BooleanFormula) is in progress.
void	generatingSBP() Reports that Kodkod SBP is in progress.
void	optimizingBoundsAndFormula() Reports that Kodkod is optimizing the bounds and formula.
void	skolemizing(java.lang.Object decl, java.lang.Object skolem, java.util.List<?> context) Reports that Kodkod is skolemizing the declaration (kodkod.ast.Decl) using the given skolem relation (kodkod.ast.Relation).
void	solvingAnalysis() Reports that Forge is about to invoke Kodkod to solve the analysis.
void	solvingCNF(int primaryVars, int vars, int clauses) Reports that Kodkod generated a CNF consisting of the given number of variables and clauses, is being analyzed by a SAT solver.
void	transformingProcedure() Reports that Forge is transforming the procedure.
void	translatingToBoolean(java.lang.Object formula, java.lang.Object bounds) Reports that Kodkod is translating the given formula (kodkod.ast.Formula) and bounds (kodkod.instance.Bounds) to a boolean circuit.
void	translatingToCNF(java.lang.Object circuit) Reports that Kodkod is translating the given boolean circuit (kodkod.engine.bool.BooleanFormula) to CNF.
void	translatingToKodkod() Reports that Forge is translating the procedure to Kodkod.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

REPORTER

public static final ForgeReporter REPORTER

Method Detail

flattening

public void flattening(java.lang.Object circuit)

Description copied from class: ForgeReporter

Reports that Kodkod flattering of the given boolean circuit (kodkod.engine.bool.BooleanFormula) is in progress.

Overrides:

flattening in class ForgeReporter

solvingAnalysis

public void solvingAnalysis()

Description copied from class: ForgeReporter

Reports that Forge is about to invoke Kodkod to solve the analysis.

Overrides:

solvingAnalysis in class ForgeReporter

transformingProcedure

public void transformingProcedure()

Description copied from class: ForgeReporter

Reports that Forge is transforming the procedure.

Overrides:

transformingProcedure in class ForgeReporter

generatingSBP

public void generatingSBP()

Description copied from class: ForgeReporter

Reports that Kodkod SBP is in progress.

Overrides:

generatingSBP in class ForgeReporter

optimizingBoundsAndFormula

public void optimizingBoundsAndFormula()

Description copied from class: ForgeReporter

Reports that Kodkod is optimizing the bounds and formula.

Overrides:

optimizingBoundsAndFormula in class ForgeReporter

detectedSymmetries

public void detectedSymmetries(java.util.Set<?> parts)

Description copied from class: ForgeReporter

Reports the symmetries detected by Kodkod as a set of (kodkod.util.ints.IntSet) objects.

Overrides:

detectedSymmetries in class ForgeReporter

detectingSymmetries

public void detectingSymmetries(java.lang.Object bounds)

Description copied from class: ForgeReporter

Reports that Kodkod is detecting symmetries in the given bounds (kodkod.instance.Bounds).

Overrides:

detectingSymmetries in class ForgeReporter

buildingAnalysis

public void buildingAnalysis()

Description copied from class: ForgeReporter

Reports that Forge is building an analysis from a given specification and bounds.

Overrides:

buildingAnalysis in class ForgeReporter

translatingToBoolean

public void translatingToBoolean(java.lang.Object formula,
                                 java.lang.Object bounds)

Description copied from class: ForgeReporter

Reports that Kodkod is translating the given formula (kodkod.ast.Formula) and bounds (kodkod.instance.Bounds) to a boolean circuit.

Overrides:

translatingToBoolean in class ForgeReporter

translatingToKodkod

public void translatingToKodkod()

Description copied from class: ForgeReporter

Reports that Forge is translating the procedure to Kodkod.

Overrides:

translatingToKodkod in class ForgeReporter

translatingToCNF

public void translatingToCNF(java.lang.Object circuit)

Description copied from class: ForgeReporter

Reports that Kodkod is translating the given boolean circuit (kodkod.engine.bool.BooleanFormula) to CNF.

Overrides:

translatingToCNF in class ForgeReporter

solvingCNF

public void solvingCNF(int primaryVars,
                       int vars,
                       int clauses)

Description copied from class: ForgeReporter

Reports that Kodkod generated a CNF consisting of the given number of variables and clauses, is being analyzed by a SAT solver.

Overrides:

solvingCNF in class ForgeReporter

skolemizing

public void skolemizing(java.lang.Object decl,
                        java.lang.Object skolem,
                        java.util.List<?> context)

Description copied from class: ForgeReporter

Reports that Kodkod is skolemizing the declaration (kodkod.ast.Decl) using the given skolem relation (kodkod.ast.Relation). The context list (java.util.List) contains non-skolemizable quantified declarations on which the given decl depends, in the order of declaration, the most recent being the last in the list.

Overrides:

skolemizing in class ForgeReporter