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

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