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 propogating 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 varaiables occuring in eqn, and dependencies in the other direction (that is, from variables occuring in eqn to eqn).
`protected boolean` | `allActivesAreMultiVarRHS()` return true if every active constraint has multi vars on the RHS.
`protected void` | `checkEquation(Equation 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` | `getDefaultBound()` The default bound of variables in this solver is bottom
`protected void` | `refineVariableEquation(VarLabel v, Equation eqn)` Raise the bound on the label variable v, which is a component of the RHS of the equation eqn.
`protected boolean` | `search(Equation eqn)` Search recursively for solution to system of constraints.
`protected void` | `solve_eqn(Equation eqn)` This method changes the bounds of variables in the RHS of Equation eqn, to make the equation satisfied.

Methods inherited from class jif.types.AbstractSolver
`addConstraint, addConstraintEquations, addDependency, addDependency, addEquationToQueue, addEquationToQueueHead, addTrace, applyBoundsTo, bounds, checkCandidateSolution, eqnEqnDependencies, eqnEqnReverseDependencies, errorMsg, errorShowConstraint, errorShowDefns, errorShowDetailMsg, errorShowTechnicalMsg, errorStringConstraint, errorStringDefns, findSCCs, findTrace, getQueue, inc_counter, isFixedValueVar, processConstraint, report, reportError, reportTraces, 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 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 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`

### getDefaultBound

    protected Label getDefaultBound()

  The default bound of variables in this solver is bottom

  Specified by:
    `getDefaultBound` in class `AbstractSolver`

### solve_eqn

    protected void solve_eqn(Equation 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`

### allActivesAreMultiVarRHS

    protected boolean allActivesAreMultiVarRHS()

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

### refineVariableEquation

    protected void refineVariableEquation(VarLabel v,
                                          Equation 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`

### 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(Equation 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

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