Overview | Package | Class | Tree | Deprecated | Index | Help
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

## 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.

Overview | Package | Class | Tree | Deprecated | Index | Help
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD