jif.types
Class Solver

java.lang.Object
  extended by jif.types.Solver
Direct Known Subclasses:
SolverGLB

public abstract class Solver
extends java.lang.Object

A solver of Jif constraints. Finds solution to constraints essentially by propogating upper bounds backwards.


Field Summary
protected  VarMap dynBounds
           
protected static int STATUS_NO_SOLUTION
           
protected static int STATUS_NOT_SOLVED
           
protected static int STATUS_SOLVED
           
protected static int STATUS_SOLVING
           
static int stop_constraint
          Constraint number at which to stop the compiler, for debugging purposes.
protected  JifTypeSystem ts
           
 
Constructor Summary
  Solver(JifTypeSystem ts, java.lang.String solverName)
          Constructor
protected Solver(Solver js)
          Constructor
 
Method Summary
 void addConstraint(LabelConstraint c)
          Add the constraint c to the system
protected abstract  void addDependencies(Equation eqn)
          This abstract method must add the correct dependencies from Equation eqn to varaiables occuring in eqn, and dependencies in the other direction (that is, from variables occuring in eqn to eqn).
protected  void addDependency(Equation eqn, VarLabel var)
          This method records a dependency from Equation eqn to variable var.
protected  void addDependency(VarLabel var, Equation eqn)
          This method records a dependency from variable var to Equation eqn.
protected  void addEquationToQueue(Equation eqn)
           
protected  void addEquationToQueueHead(Equation eqn)
           
protected  void addTrace(VarLabel v, Equation eqn, Label lb)
          Record the fact that label variable v, in the constraint eqn had its bound set to the label lb.
 Label applyBoundsTo(Label L)
           
 VarMap bounds()
          Get the bounds for this Solver.
protected  void checkCandidateSolution()
          Check the candidate solution
protected  Graph createGraph()
          Creating the equation graph with edges based on information gathered during the addConstraint method.
protected  java.lang.String errorMsg(LabelConstraint c)
          Produce an error message for the constraint c, which cannot be satisfied.
protected  boolean errorShowConstraint()
           
protected  boolean errorShowDefns()
           
protected  boolean errorShowDetailMsg()
           
protected  boolean errorShowTechnicalMsg()
           
protected  java.lang.String errorStringConstraint(LabelConstraint c)
          Produce a string appropriate for an error message that displays the unsatisfiable constraint c.
protected  java.lang.String errorStringDefns(LabelConstraint c)
          Produce a string appropriate for an error message that displays the definitions needed by the unsatisfiable constraint c.
protected abstract  Equation findContradictiveEqn(LabelConstraint c)
           
protected  Equation findTrace(VarLabel var, Label threshold, boolean lowerThreshold)
           
protected abstract  Label getDefaultBound()
          This method must return a constant label, which is the default bound of variables.
protected  java.util.List getQueue()
           
protected  void inc_counter()
          Increase the count of the number of constraints added (not just to this system, but to all instances of the Solver).
static void report(int level, java.lang.String s)
          Convenience method to report messages for the appropriate topics
protected  void reportError(LabelConstraint c, java.util.Collection variables)
          Throws a SemanticException with the appropriate error message.
protected  void reportTraces(java.util.Collection variables)
          Report the traces for each variables in the collection Variables
 void setBound(VarLabel v, Label newBound, LabelConstraint responsible)
           
 void setBounds(VarMap bnds)
          Set the bounds for this Solver.
static boolean shouldReport(int obscurity)
          Convenience method to determine if messages of the given obscurity should be reported.
protected  VarMap solve_bounds()
          Solve the system of constraints, by finding upper bounds for the label variables.
protected abstract  void solve_eqn(Equation eqn)
          This method changes the bounds of variables in the Equation eqn, to make the equation satisfied.
 VarMap solve()
          Solve the system of constraints.
protected  Label triggerTransforms(Label label, LabelEnv env)
           
protected  void wakeUp(VarLabel v)
          Awakens all equations in the system that depend on the variable v, ensuring that they are in the queue of active equations.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

STATUS_NOT_SOLVED

protected static final int STATUS_NOT_SOLVED
See Also:
Constant Field Values

STATUS_SOLVING

protected static final int STATUS_SOLVING
See Also:
Constant Field Values

STATUS_SOLVED

protected static final int STATUS_SOLVED
See Also:
Constant Field Values

STATUS_NO_SOLUTION

protected static final int STATUS_NO_SOLUTION
See Also:
Constant Field Values

dynBounds

protected VarMap dynBounds

ts

protected JifTypeSystem ts

stop_constraint

public static int stop_constraint
Constraint number at which to stop the compiler, for debugging purposes. Set using a command line option, refer to ExtensionInfofor details

Constructor Detail

Solver

public Solver(JifTypeSystem ts,
              java.lang.String solverName)
Constructor


Solver

protected Solver(Solver js)
Constructor

Method Detail

report

public static final void report(int level,
                                java.lang.String s)
Convenience method to report messages for the appropriate topics


shouldReport

public static final boolean shouldReport(int obscurity)
Convenience method to determine if messages of the given obscurity should be reported.


applyBoundsTo

public Label applyBoundsTo(Label L)

triggerTransforms

protected Label triggerTransforms(Label label,
                                  LabelEnv env)

getQueue

protected java.util.List getQueue()

addEquationToQueue

protected void addEquationToQueue(Equation eqn)

addEquationToQueueHead

protected void addEquationToQueueHead(Equation eqn)

createGraph

protected final Graph createGraph()
Creating the equation graph with edges based on information gathered during the addConstraint method. TODO: XXX Maybe do most of this work while adding constraints?


bounds

public VarMap bounds()
Get the bounds for this Solver.


setBounds

public void setBounds(VarMap bnds)
Set the bounds for this Solver.


setBound

public void setBound(VarLabel v,
                     Label newBound,
                     LabelConstraint responsible)
              throws polyglot.types.SemanticException
Parameters:
v - the VarLabel to set the bound for
newBound - the new bound for v
responsible - the constraint that was responsible for modifying the bound.
Throws:
polyglot.types.SemanticException - if the new bound violates an equality constraint.

solve

public final VarMap solve()
                   throws polyglot.types.SemanticException
Solve the system of constraints. If the system has already been solved, then returned the cached solution.

Throws:
polyglot.types.SemanticException - if the Solver cannot find a solution to the system of contraints.

getDefaultBound

protected abstract Label getDefaultBound()
This method must return a constant label, which is the default bound of variables.


solve_bounds

protected VarMap solve_bounds()
                       throws polyglot.types.SemanticException
Solve the system of constraints, by finding upper bounds for the label variables.

Returns:
a solution to the system of constraints, in the form of a VarMap of the upper bounds of the label variables.
Throws:
polyglot.types.SemanticException - if the Solver cannot find a solution to the system of contraints.

solve_eqn

protected abstract void solve_eqn(Equation eqn)
                           throws polyglot.types.SemanticException
This method changes the bounds of variables in the Equation eqn, to make the equation satisfied. The method may postpone solving the equation by putting the equation back on the queue, using addEquationToQueue().

Throws:
polyglot.types.SemanticException

checkCandidateSolution

protected final void checkCandidateSolution()
                                     throws polyglot.types.SemanticException
Check the candidate solution

Throws:
polyglot.types.SemanticException

wakeUp

protected final void wakeUp(VarLabel v)
Awakens all equations in the system that depend on the variable v, ensuring that they are in the queue of active equations.


inc_counter

protected final void inc_counter()
Increase the count of the number of constraints added (not just to this system, but to all instances of the Solver). For debugging purposes, if the constraint counter is equal to the stop_constraint, then a RuntimeException is thrown.


addConstraint

public final void addConstraint(LabelConstraint c)
                         throws polyglot.types.SemanticException
Add the constraint c to the system

Throws:
polyglot.types.SemanticException

addDependencies

protected abstract void addDependencies(Equation eqn)
This abstract method must add the correct dependencies from Equation eqn to varaiables occuring in eqn, and dependencies in the other direction (that is, from variables occuring in eqn to eqn). There is a dependency from Equation eqn to variable var if the bound on var may be modified as a result of solving eqn. This dependency should be recorded by calling the method addDependency(eqn, var). There is a dependency from variable var to Equation eqn if modifying the bound on var may cause eqn to no longer be satisfied. This dependency should be recorded by calling the method addDependency(var, eqn).


addDependency

protected void addDependency(VarLabel var,
                             Equation eqn)
This method records a dependency from variable var to Equation eqn. This method should only be called by subclasses during the execution of the method addDependencies(). There is a dependency from variable var to Equation eqn if modifying the bound on var may cause eqn to no longer be satisfied.


addDependency

protected void addDependency(Equation eqn,
                             VarLabel var)
This method records a dependency from Equation eqn to variable var. This method should only be called by subclasses during the execution of the method addDependencies(). There is a dependency from Equation eqn to variable var if the bound on var may be modified as a result of solving eqn.


addTrace

protected final void addTrace(VarLabel v,
                              Equation eqn,
                              Label lb)
Record the fact that label variable v, in the constraint eqn had its bound set to the label lb.


findTrace

protected final Equation findTrace(VarLabel var,
                                   Label threshold,
                                   boolean lowerThreshold)
Returns:
an equation that contained label variable var, and that changed the bound of var to less than/greater than threshold. Null if no such equation exists. If lowerThreshold is true, then the equation returned is one that changed var to less than threshold; otherwise the equation returned is one that changed var to greater than the threshold

reportTraces

protected void reportTraces(java.util.Collection variables)
Report the traces for each variables in the collection Variables


errorShowConstraint

protected boolean errorShowConstraint()

errorShowTechnicalMsg

protected boolean errorShowTechnicalMsg()

errorShowDetailMsg

protected boolean errorShowDetailMsg()

errorShowDefns

protected boolean errorShowDefns()

errorMsg

protected final java.lang.String errorMsg(LabelConstraint c)
Produce an error message for the constraint c, which cannot be satisfied.


errorStringConstraint

protected java.lang.String errorStringConstraint(LabelConstraint c)
Produce a string appropriate for an error message that displays the unsatisfiable constraint c.


errorStringDefns

protected java.lang.String errorStringDefns(LabelConstraint c)
Produce a string appropriate for an error message that displays the definitions needed by the unsatisfiable constraint c.


reportError

protected void reportError(LabelConstraint c,
                           java.util.Collection variables)
                    throws polyglot.types.SemanticException
Throws a SemanticException with the appropriate error message.

Parameters:
c - The constraint that cannot be satisfied.
Throws:
polyglot.types.SemanticException - always.

findContradictiveEqn

protected abstract Equation findContradictiveEqn(LabelConstraint c)