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 SolverGLB

    java.lang.Object
      jif.types.AbstractSolver
          jif.types.SolverGLB

All Implemented Interfaces:
  Solver

    public class SolverGLB

extends AbstractSolver

A solver of Jif constraints. Finds solution to constraints essentially by propagating lower bounds forwards.

Nested Class Summary

Nested classes/interfaces inherited from class jif.types.AbstractSolver
`AbstractSolver.EquationQueue, AbstractSolver.Frame`

Field Summary

Fields inherited from class jif.types.AbstractSolver
`bounds, compiler, constraint_counter, currentSCC, equations, fixedValueVars, Q, scc, solverCounter, staticFailedConstraints, status, STATUS_NO_SOLUTION, STATUS_NOT_SOLVED, STATUS_SOLVED, STATUS_SOLVING, THROW_STATIC_FAILED_CONSTRAINTS, topics, traces, ts, useSCC`

Constructor Summary
`` | `SolverGLB(JifTypeSystem ts, polyglot.frontend.Compiler compiler, java.lang.String solverName)` Constructor
`protected` | `SolverGLB(SolverGLB js)` Constructor

Method Summary
`protected void` | `addDependencies(Equation eqn)` This method adds 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 boolean` | `allActivesAreMultiVarRHS()` return true if every active constraint has multi vars on the RHS.
`protected void` | `checkEquation(LabelEquation eqn)` Check that the equation eqn is satisfied.
`protected void` | `checkEquation(PrincipalEquation eqn)` Check that the equation eqn is satisfied.
`protected Equation` | `findContradictiveEqn(LabelConstraint c)` Find a contradicting equation.
`protected ConfPolicy` | `findNeeded(ConfPolicy lhs, ConfPolicy rhs, LabelEnv env)`
`protected IntegPolicy` | `findNeeded(IntegPolicy lhs, IntegPolicy rhs, LabelEnv env)`
`protected Label` | `findNeeded(Label lhs, Label rhs, LabelEnv env)` Return the most permissive label L such that lhs <= rhs join L
`protected Label` | `getDefaultLabelBound()` The default bound of label variables in this solver is bottom
`protected Principal` | `getDefaultPrincipalBound()` The default bound of label variables in this solver is bottom
`protected void` | `refineVariableEquation(VarLabel v, LabelEquation eqn)` Raise the bound on the label variable v, which is a component of the RHS of the equation eqn.
`protected void` | `refineVariableEquation(VarPrincipal v, PrincipalEquation eqn)` Raise the bound on the label variable v, which is a component of the equation eqn.
`protected boolean` | `search(Equation eqn)` Search recursively for solution to system of constraints.
`protected void` | `solve_eqn(LabelEquation eqn)` This method changes the bounds of variables in the RHS of Equation eqn, to make the equation satisfied.
`protected void` | `solve_eqn(PrincipalEquation eqn)` This method changes the bounds of variables in the Equation eqn, to make the equation satisfied.

Methods inherited from class jif.types.AbstractSolver
`addConstraint, addConstraintEquations, addDependency, addDependency, addEquationToQueue, addEquationToQueueHead, addTrace, applyBoundsTo, bounds, checkCandidateSolution, checkEquationSatisfied, considerEquation, considerEquation, considerEquation, eqnEqnDependencies, eqnEqnReverseDependencies, errorMsg, errorShowConstraint, errorShowDefns, errorShowDetailMsg, errorShowTechnicalMsg, errorStringConstraint, errorStringDefns, findContradictiveEqn, findSCCs, findTrace, getQueue, inc_counter, isFixedValueVar, processConstraint, report, reportError, reportTraces, setBound, setBound, setBounds, setStatus, shouldReport, solve_bounds, solve, solverName, triggerTransforms, wakeUp`

Methods inherited from class java.lang.Object
`clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait`

Constructor Detail

### SolverGLB

    public SolverGLB(JifTypeSystem ts,
                     polyglot.frontend.Compiler compiler,
                     java.lang.String solverName)

  Constructor

### SolverGLB

    protected SolverGLB(SolverGLB js)

  Constructor

Method Detail

### addDependencies

    protected void addDependencies(Equation eqn)

  This method adds 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 all variables that occur on the RHS of eqn, as the bounds on these variables may be modified (upwards) as a result of solving eqn. There is a dependency from all variables on the LHS of eqn to eqn, because modifying (upwards) the bounds on these variables may cause eqn to no longer be satisfied.

  Specified by:
    `addDependencies` in class `AbstractSolver`

### getDefaultLabelBound

    protected Label getDefaultLabelBound()

  The default bound of label variables in this solver is bottom

  Specified by:
    `getDefaultLabelBound` in class `AbstractSolver`

### getDefaultPrincipalBound

    protected Principal getDefaultPrincipalBound()

  The default bound of label variables in this solver is bottom

  Specified by:
    `getDefaultPrincipalBound` in class `AbstractSolver`

### solve_eqn

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

  This method changes the bounds of variables in the RHS of Equation eqn, to make the equation satisfied. If the equation has no variables in the RHS, it just checks that the equation holds, and returns. Otherwise, if the RHS has exactly one variable, then it refines that variable (see here) and returns. If the RHS has more than one variable, then the method performs a search, attempting to refine each variable in turn, and then recursively attempting to solve the set of equations.

  Specified by:
    `solve_eqn` in class `AbstractSolver`
  Throws:
    `polyglot.types.SemanticException`

### solve_eqn

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

  Description copied from class: `AbstractSolver`
  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().

  Specified by:
    `solve_eqn` in class `AbstractSolver`
  Throws:
    `polyglot.types.SemanticException`

### allActivesAreMultiVarRHS

    protected boolean allActivesAreMultiVarRHS()

  return true if every active constraint has multi vars on the RHS.

### refineVariableEquation

    protected void refineVariableEquation(VarLabel v,
                                          LabelEquation eqn)
                                   throws polyglot.types.SemanticException

  Raise the bound on the label variable v, which is a component of the RHS of the equation eqn.

  Throws:
    `polyglot.types.SemanticException`

### refineVariableEquation

    protected void refineVariableEquation(VarPrincipal v,
                                          PrincipalEquation eqn)
                                   throws polyglot.types.SemanticException

  Raise the bound on the label variable v, which is a component of the equation eqn.

  Throws:
    `polyglot.types.SemanticException`

### findNeeded

    protected Label findNeeded(Label lhs,
                               Label rhs,
                               LabelEnv env)

  Return the most permissive label L such that lhs <= rhs join L

### findNeeded

    protected ConfPolicy findNeeded(ConfPolicy lhs,
                                    ConfPolicy rhs,
                                    LabelEnv env)

### findNeeded

    protected IntegPolicy findNeeded(IntegPolicy lhs,
                                     IntegPolicy rhs,
                                     LabelEnv env)

### search

    protected boolean search(Equation eqn)

  Search recursively for solution to system of constraints.

### checkEquation

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

  Check that the equation eqn is satisfied. The RHS of eqn cannot have any variables.

  Throws:
    `polyglot.types.SemanticException` - if eqn is not satisfied.
    `polyglot.util.InternalCompilerError` - if eqn contains variables

### checkEquation

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

  Check that the equation eqn is satisfied. The LHS of eqn cannot have any variables.

  Throws:
    `polyglot.types.SemanticException` - if eqn is not satisfied.
    `polyglot.util.InternalCompilerError` - if eqn contains variables

### findContradictiveEqn

    protected Equation findContradictiveEqn(LabelConstraint c)

  Find a contradicting equation.

  Specified by:
    `findContradictiveEqn` in class `AbstractSolver`

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