jif.types
Class AbstractSolver

java.lang.Object
  jif.types.AbstractSolver

All Implemented Interfaces:

Solver

Direct Known Subclasses:

SolverGLB

public abstract class AbstractSolver
extends java.lang.Object
implements Solver

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

Nested Class Summary

protected static class	AbstractSolver.EquationQueue A queue for equations.
protected class	AbstractSolver.Frame

Field Summary

protected VarMap	bounds
protected polyglot.frontend.Compiler	compiler
protected static int	constraint_counter Counter of the number of constraints added to the system.
protected java.util.Set	currentSCC
protected java.util.Collection	equations
protected java.util.Set	fixedValueVars Set of Variables that had their initial value fixed when the constraint was added.
protected AbstractSolver.EquationQueue	Q
protected java.util.LinkedList	scc
protected static int	solverCounter Number of solvers instantiated, for debugging purposes
protected java.util.Set	staticFailedConstraints Constraints that were added to the solver, and failed statically.
protected int	status
protected static int	STATUS_NO_SOLUTION
protected static int	STATUS_NOT_SOLVED
protected static int	STATUS_SOLVED
protected static int	STATUS_SOLVING
protected static boolean	THROW_STATIC_FAILED_CONSTRAINTS
protected static java.util.Collection	topics
protected java.util.Map	traces
protected JifTypeSystem	ts
protected boolean	useSCC This boolean is used to turn on or off whether the strongly connected components optimization is used.

Constructor Summary

protected	AbstractSolver(AbstractSolver js) Constructor
protected	AbstractSolver(JifTypeSystem ts, polyglot.frontend.Compiler compiler, java.lang.String solverName) Constructor
protected	AbstractSolver(JifTypeSystem ts, polyglot.frontend.Compiler compiler, java.lang.String solverName, boolean useSCC) Constructor

Method Summary

void	addConstraint(Constraint c) Add the constraint c to the system
protected void	addConstraintEquations(Constraint c) Go through each equation in the constraint, add the equation if needed, and register dependencies for the equation.
protected abstract void	addDependencies(Equation eqn) This abstract method must add the correct dependencies from Equation eqn to variables occurring in eqn, and dependencies in the other direction (that is, from variables occurring in eqn to eqn).
protected void	addDependency(Equation eqn, Variable var) This method records a dependency from Equation eqn to variable var.
protected void	addDependency(Variable 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) Substitute variables in L with the solution for the variables.
VarMap	bounds() Get the bounds for this Solver.
protected void	checkCandidateSolution() Check the candidate solution
protected void	checkEquationSatisfied(LabelEquation eqn)
protected void	considerEquation(Equation eqn)
protected void	considerEquation(LabelEquation eqn)
protected void	considerEquation(PrincipalEquation eqn)
protected java.util.Set	eqnEqnDependencies(Equation eqn) Returns the equations that are dependent on the equation eqn by finding the variables that eqn may alter if it is solved (useing the map eqnVarDependencies), and then finds the equations that depend on those variables (using the map varEqnDependencies)
protected java.util.Set	eqnEqnReverseDependencies(Equation eqn) Returns the equations that are reverse dependent on the equation eqn by finding the variables that may invalidate eqn (using the map eqnVarReverseDependencies), and then finding the equations that may alter those variables (using the map varEqnReverseDependencies)
protected java.lang.String	errorMsg(Constraint 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(Constraint 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 Equation	findContradictiveEqn(Constraint c)
protected abstract Equation	findContradictiveEqn(LabelConstraint c)
protected java.util.LinkedList	findSCCs() Returns the linked list [by_scc, scc_head] where by_scc is an array in which SCCs occur in topologically order.
protected Equation	findTrace(VarLabel var, Label threshold, boolean lowerThreshold)
protected abstract Label	getDefaultLabelBound() This method must return a constant label, which is the default bound of label variables.
protected abstract Principal	getDefaultPrincipalBound() This method must return a constant principal, which is the default bound of principal 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).
protected boolean	isFixedValueVar(Variable v)
protected void	processConstraint(Constraint c) Perform any special processing for the label constraint
static void	report(int level, java.lang.String s) Convenience method to report messages for the appropriate topics
protected void	reportError(Constraint 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	setBound(VarPrincipal v, Principal newBound, PrincipalConstraint responsible)
void	setBounds(VarMap bnds) Set the bounds for this Solver.
protected void	setStatus(int status)
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(LabelEquation eqn) This method changes the bounds of variables in the Equation eqn, to make the equation satisfied.
protected abstract void	solve_eqn(PrincipalEquation eqn) This method changes the bounds of variables in the Equation eqn, to make the equation satisfied.
VarMap	solve() Solve the system of constraints.
java.lang.String	solverName()
protected Label	triggerTransforms(Label label, LabelEnv env)
protected void	wakeUp(Variable 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

Q

protected AbstractSolver.EquationQueue Q

scc

protected java.util.LinkedList scc

currentSCC

protected java.util.Set currentSCC

equations

protected java.util.Collection equations

fixedValueVars

protected java.util.Set fixedValueVars

Set of Variables that had their initial value fixed when the constraint was added.

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

status

protected int status

bounds

protected VarMap bounds

ts

protected JifTypeSystem ts

staticFailedConstraints

protected java.util.Set staticFailedConstraints

Constraints that were added to the solver, and failed statically. If the flag THROW_STATIC_FAILED_CONSTRAINTS is true, then the constraint will be thrown immediately, otherwise the constraint will be added to this set, and thrown when solve() is called.

THROW_STATIC_FAILED_CONSTRAINTS

protected static final boolean THROW_STATIC_FAILED_CONSTRAINTS

See Also:

Constant Field Values

compiler

protected final polyglot.frontend.Compiler compiler

traces

protected java.util.Map traces

topics

protected static java.util.Collection topics

useSCC

protected final boolean useSCC

This boolean is used to turn on or off whether the strongly connected components optimization is used. If true, the constraints are partitioned into strongly connected components, which are then sorted in topological order. If false, then constraints are solved in the order they are added to the solver

solverCounter

protected static int solverCounter

Number of solvers instantiated, for debugging purposes

constraint_counter

protected static int constraint_counter

Counter of the number of constraints added to the system. For debugging purposes.

Constructor Detail

AbstractSolver

protected AbstractSolver(JifTypeSystem ts,
                         polyglot.frontend.Compiler compiler,
                         java.lang.String solverName)

Constructor

AbstractSolver

protected AbstractSolver(JifTypeSystem ts,
                         polyglot.frontend.Compiler compiler,
                         java.lang.String solverName,
                         boolean useSCC)

Constructor

AbstractSolver

protected AbstractSolver(AbstractSolver 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)

Description copied from interface: Solver

Substitute variables in L with the solution for the variables. Should only be called after solve() has been called successfully.

Specified by:

applyBoundsTo in interface Solver

Returns:

L with variables replaced appropriately according to the solution.

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)

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.

setBound

public void setBound(VarPrincipal v,
                     Principal newBound,
                     PrincipalConstraint responsible)
              throws polyglot.types.SemanticException

Throws:

polyglot.types.SemanticException

solve

public VarMap solve()
             throws polyglot.types.SemanticException

Solve the system of constraints. If the system has already been solved, then returned the cached solution.

Specified by:

solve in interface Solver

Throws:

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

setStatus

protected void setStatus(int status)

getDefaultLabelBound

protected abstract Label getDefaultLabelBound()

This method must return a constant label, which is the default bound of label variables.

getDefaultPrincipalBound

protected abstract Principal getDefaultPrincipalBound()

This method must return a constant principal, which is the default bound of principal 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 constraints.

considerEquation

protected void considerEquation(Equation eqn)
                         throws polyglot.types.SemanticException

Throws:

polyglot.types.SemanticException

considerEquation

protected void considerEquation(LabelEquation eqn)
                         throws polyglot.types.SemanticException

Throws:

polyglot.types.SemanticException

solve_eqn

protected abstract void solve_eqn(LabelEquation 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

considerEquation

protected void considerEquation(PrincipalEquation eqn)
                         throws polyglot.types.SemanticException

Throws:

polyglot.types.SemanticException

solve_eqn

protected abstract void solve_eqn(PrincipalEquation 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

checkEquationSatisfied

protected void checkEquationSatisfied(LabelEquation eqn)
                               throws polyglot.types.SemanticException

Throws:

polyglot.types.SemanticException

wakeUp

protected final void wakeUp(Variable v)

Awakens all equations in the system that depend on the variable v, ensuring that they are in the queue of active equations.

solverName

public java.lang.String solverName()

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.

isFixedValueVar

protected boolean isFixedValueVar(Variable v)

addConstraint

public void addConstraint(Constraint c)
                   throws polyglot.types.SemanticException

Add the constraint c to the system

Specified by:

addConstraint in interface Solver

Throws:

polyglot.types.SemanticException

processConstraint

protected void processConstraint(Constraint c)
                          throws polyglot.types.SemanticException

Perform any special processing for the label constraint

Throws:

polyglot.types.SemanticException

addConstraintEquations

protected void addConstraintEquations(Constraint c)
                               throws polyglot.types.SemanticException

Go through each equation in the constraint, add the equation if needed, and register dependencies for the equation.

Parameters:

c -

Throws:

polyglot.types.SemanticException

addDependencies

protected abstract void addDependencies(Equation eqn)

This abstract method must add the correct dependencies from Equation eqn to variables occurring in eqn, and dependencies in the other direction (that is, from variables occurring 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(Variable 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,
                             Variable 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.

eqnEqnDependencies

protected java.util.Set eqnEqnDependencies(Equation eqn)

Returns the equations that are dependent on the equation eqn by finding the variables that eqn may alter if it is solved (useing the map eqnVarDependencies), and then finds the equations that depend on those variables (using the map varEqnDependencies)

eqnEqnReverseDependencies

protected java.util.Set eqnEqnReverseDependencies(Equation eqn)

Returns the equations that are reverse dependent on the equation eqn by finding the variables that may invalidate eqn (using the map eqnVarReverseDependencies), and then finding the equations that may alter those variables (using the map varEqnReverseDependencies)

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(Constraint c)

Produce an error message for the constraint c, which cannot be satisfied.

errorStringConstraint

protected java.lang.String errorStringConstraint(Constraint 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(Constraint 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 Equation findContradictiveEqn(Constraint c)

findContradictiveEqn

protected abstract Equation findContradictiveEqn(LabelConstraint c)

findSCCs

protected java.util.LinkedList findSCCs()

Returns the linked list [by_scc, scc_head] where by_scc is an array in which SCCs occur in topologically order. scc_head[n] where n is the first peer in an SCC is set to -1. scc_head[n] where n is the last peer in a (non-singleton) SCC is set to the index of the first peer. Otherwise it is -2. by_scc contains the peers grouped by SCC. scc_head marks where the SCCs are. The SCC begins with a -1 and ends with the index of the beginning of the SCC.