edu.mit.csail.sdg.alloy4
Class A4Reporter

java.lang.Object
  extended by 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.