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, failedEquations, fixedValueVars, fullTrace, 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

    Constructors
    Modifier | Constructor and Description
    --- | ---
    `` | `SolverGLB(JifTypeSystem ts, polyglot.frontend.Compiler compiler, java.lang.String solverName)` Constructor
    `protected` | `SolverGLB(SolverGLB js)` Constructor

  - ### Method Summary

    All Methods Instance Methods Concrete Methods
    Modifier and Type | Method and Description
    --- | ---
    `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, boolean trace)` 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, findContradictiveEqn, findSCCs, findTrace, genFlowMessage, getQueue, inc_counter, isFixedValueVar, processConstraint, report, reportError, reportTrace, 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,
                                                boolean trace)
                                         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)

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

    - #### 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)
                            throws polyglot.types.SemanticException

      Search recursively for solution to system of constraints.
      Throws:
        `polyglot.types.SemanticException`

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