jif.types
Class SolverGLB

java.lang.Object
  jif.types.Solver
      jif.types.SolverGLB

public class SolverGLB
extends Solver

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

Field Summary

Fields inherited from class jif.types.Solver

dynBounds, STATUS_NO_SOLUTION, STATUS_NOT_SOLVED, STATUS_SOLVED, STATUS_SOLVING, stop_constraint, ts

Constructor Summary

	SolverGLB(JifTypeSystem ts, 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 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.Solver

addConstraint, addDependency, addDependency, addEquationToQueue, addEquationToQueueHead, addTrace, applyBoundsTo, bounds, checkCandidateSolution, createGraph, errorMsg, errorShowConstraint, errorShowDefns, errorShowDetailMsg, errorShowTechnicalMsg, errorStringConstraint, errorStringDefns, findTrace, getQueue, inc_counter, report, reportError, reportTraces, setBound, setBounds, shouldReport, solve_bounds, solve, 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,
                 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 Solver

getDefaultBound

protected Label getDefaultBound()

The default bound of variables in this solver is bottom

Specified by:

getDefaultBound in class Solver

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 Solver

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)

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 Solver