edu.mit.csail.sdg.alloy4
Class A4Reporter

java.lang.Object
  edu.mit.csail.sdg.alloy4.A4Reporter

public class A4Reporter
extends java.lang.Object

This class receives diagnostic, progress, and warning messages from Alloy4. (This default implementation ignores all calls; you should subclass it to do the appropriate screen output)

Field Summary

static A4Reporter

NOP This is a pre-constructed instance that simply ignores all calls.

Constructor Summary

A4Reporter()
Constructs a default A4Reporter object that does nothing.

A4Reporter(A4Reporter reporter)
Constructs an A4Reporter that forwards each method to the given A4Reporter.

Method Summary

void	bound(java.lang.String msg) This method is called by the BoundsComputer to report the bounds chosen for each sig and each field.
void	debug(java.lang.String msg) This method is called at various points to report the current progress; it is intended as a debugging aid for the developers; the messages are generally not useful for end users.
void	minimized(java.lang.Object command, int before, int after) If solver!=KK and solver!=CNF, this method is called by the translator after performing the unsat core minimization.
void	minimizing(java.lang.Object command, int before) If solver!=KK and solver!=CNF, this method is called by the translator before starting the unsat core minimization.
void	parse(java.lang.String msg) This method is called by the parser to report parser events.
void	resultCNF(java.lang.String filename) If solver==KK or solver==CNF, this method is called by the translator after it constructed the Kodkod or CNF file.
void	resultSAT(java.lang.Object command, long solvingTime, java.lang.Object solution) If solver!=KK and solver!=CNF, this method is called by the translator if the formula is satisfiable.
void	resultUNSAT(java.lang.Object command, long solvingTime, java.lang.Object solution) If solver!=KK and solver!=CNF, this method is called by the translator if the formula is unsatisfiable.
void	scope(java.lang.String msg) This method is called by the ScopeComputer to report the scope chosen for each sig.
void	solve(int primaryVars, int totalVars, int clauses) This method is called by the translator just after it generated the CNF.
void	translate(java.lang.String solver, int bitwidth, int maxseq, int skolemDepth, int symmetry) This method is called by the translator just before it begins generating CNF.
void	typecheck(java.lang.String msg) This method is called by the typechecker to report the type for each field/function/predicate/assertion, etc.
void	warning(ErrorWarning msg) This method is called by the typechecker to report a nonfatal type error.
void	write(java.lang.Object expr) This method is called by the A4SolutionWriter when it is writing a particular sig, field, or skolem.

Methods inherited from class java.lang.Object

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

Field Detail

NOP

public static final A4Reporter NOP

This is a pre-constructed instance that simply ignores all calls.

Constructor Detail

A4Reporter

public A4Reporter()

Constructs a default A4Reporter object that does nothing.

A4Reporter

public A4Reporter(A4Reporter reporter)

Constructs an A4Reporter that forwards each method to the given A4Reporter.

Method Detail

debug

public void debug(java.lang.String msg)

This method is called at various points to report the current progress; it is intended as a debugging aid for the developers; the messages are generally not useful for end users.

parse

public void parse(java.lang.String msg)

This method is called by the parser to report parser events.

typecheck

public void typecheck(java.lang.String msg)

This method is called by the typechecker to report the type for each field/function/predicate/assertion, etc.

warning

public void warning(ErrorWarning msg)

This method is called by the typechecker to report a nonfatal type error.

scope

public void scope(java.lang.String msg)

This method is called by the ScopeComputer to report the scope chosen for each sig.

bound

public void bound(java.lang.String msg)

This method is called by the BoundsComputer to report the bounds chosen for each sig and each field.

translate

public void translate(java.lang.String solver,
                      int bitwidth,
                      int maxseq,
                      int skolemDepth,
                      int symmetry)

This method is called by the translator just before it begins generating CNF.

Parameters:

solver - - the solver chosen by the user (eg. SAT4J, MiniSat...)

bitwidth - - the integer bitwidth chosen by the user

maxseq - - the scope on seq/Int chosen by the user

skolemDepth - - the skolem function depth chosen by the user (0, 1, 2...)

symmetry - - the amount of symmetry breaking chosen by the user (0...)

solve

public void solve(int primaryVars,
                  int totalVars,
                  int clauses)

This method is called by the translator just after it generated the CNF.

Parameters:

primaryVars - - the total number of primary variables

totalVars - - the total number of variables including the number of primary variables

clauses - - the total number of clauses

resultCNF

public void resultCNF(java.lang.String filename)

If solver==KK or solver==CNF, this method is called by the translator after it constructed the Kodkod or CNF file.

Parameters:

filename - - the Kodkod or CNF file generated by the translator

resultSAT

public void resultSAT(java.lang.Object command,
                      long solvingTime,
                      java.lang.Object solution)

If solver!=KK and solver!=CNF, this method is called by the translator if the formula is satisfiable.

Parameters:

command - - this is the original Command used to generate this solution

solvingTime - - this is the number of milliseconds the solver took to obtain this result

solution - - the satisfying A4Solution object

minimizing

public void minimizing(java.lang.Object command,
                       int before)

If solver!=KK and solver!=CNF, this method is called by the translator before starting the unsat core minimization.

Parameters:

command - - this is the original Command used to generate this solution

before - - the size of the unsat core before calling minimization

minimized

public void minimized(java.lang.Object command,
                      int before,
                      int after)

If solver!=KK and solver!=CNF, this method is called by the translator after performing the unsat core minimization.

Parameters:

command - - this is the original Command used to generate this solution

before - - the size of the unsat core before calling minimization

after - - the size of the unsat core after calling minimization

resultUNSAT

public void resultUNSAT(java.lang.Object command,
                        long solvingTime,
                        java.lang.Object solution)

If solver!=KK and solver!=CNF, this method is called by the translator if the formula is unsatisfiable.

Parameters:

command - - this is the original Command used to generate this solution

solvingTime - - this is the number of milliseconds the solver took to obtain this result

solution - - the unsatisfying A4Solution object

write

public void write(java.lang.Object expr)

This method is called by the A4SolutionWriter when it is writing a particular sig, field, or skolem.