Docjar: A Java Source and Docuemnt Enginecom.*    java.*    javax.*    org.*    all    new    plug-in

Quick Search    Search Deep
Overview  Package   Class  Use  Deprecated  Index 
Home >> All >> mlsub >> typing >> [ lowlevel overview ]  PREV CLASS  NEXT CLASS
SUMMARY: JavaDoc of mlsub.typing.lowlevel.K0 JAVADOC | Sourc code of mlsub.typing.lowlevel.K0 SOURCE | Download mlsub.typing.lowlevel.K0 DOWNLOAD | NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD

mlsub.typing.lowlevel
Class K0  view K0 download K0.java

java.lang.Object
  extended bymlsub.typing.lowlevel.K0
public final class K0
extends java.lang.Object

A lowlevel constraint on integers.

Version:
$OrigRevision: 1.22 $, $OrigDate: 1999/10/28 10:56:58 $

Nested Class Summary
static class K0.AbstractsIterator
           
private  class K0.Backup
           
static class K0.Callbacks
           
static class K0.ImplementsIterator
           
static class K0.IndexIterator
           
static class K0.IndexSelector
           
static class K0.IneqIterator
           
private  class K0.Simplifier
           
 
Field Summary
private  BitVector _collapsed
           
private  BitVector _toCollapse
           
static int ALL
          Iterate thru the constraint
static int BACKTRACK_ONCE
           
static int BACKTRACK_UNLIMITED
           
private  int backtrackMode
          Marking / Backtracking
private  K0.Backup backup
           
private  BitMatrix C
          C maintains the constraint as it is entered
private  K0.Callbacks callbacks
           
private  BitMatrix Ct
          Transpose of C
static boolean debugK0
          Debugging
private  DomainVector domains
          Domains
private  BitVector garbage
           
private  boolean hasBeenInitialized
          Construction of the initial rigid context
private  int ID
           
private static int IDs
           
private  java.util.Vector interfaces
           
private  int m
          Number of rigid indexes.
private  int m0
          Number of rigid indexes in the initial rigid context (m0 <= m)
private  BitVector minimal
          Maintains the information "x is minimal" on [0, m0[
private  int n
          Total number of indexes.
(package private)  BitVector negTagged
           
private static int OVERLOADING_CONSTRUCTOR
          Overloading resolution
private static int OVERLOADING_INTERFACE
           
(package private)  BitVector posTagged
           
private  BitMatrix R
          Relation on the rigid indexes
private  BitMatrix Rt
          Transpose of R
static int SIMPLIFIED
          Iterate thru the constraint
private  int weakMarkedM
           
private  int weakMarkedSize
          Weak marking / Backtracking (only keeps track of the sizes) NB: calls to mark/backtrack and weakMark/weakBacktrack mustn't be interleaved
 
Constructor Summary
K0(int backtrackMode, K0.Callbacks callbacks)
           
K0(K0.Callbacks callbacks)
           
 
Method Summary
 void abstractsIter(K0.AbstractsIterator iterator)
           
 void backtrack()
           
 void clearTags()
           
(package private)  BitVector[] closeImplements(BitMatrix R, BitMatrix Rt)
          Saturate the "implements" constraint under the following axioms: x: I and I < J => x: J x ~ y and y: I => x: I Returns an array of BitVector rigidImplementors rigidImplementors[iid] is the set of x such that x :* iid
private  void closeInterfaceRelation()
          Saturate the subtyping between interfaces under : I < J and J < K => I < K
private  void collapseMinimal()
          Saturate the constraint C, Ct under the axiom: x <* y and Min(y) => y < x (hence x ~ y)
private  void collect()
           
private  int collect(int i, int j)
           
private  java.lang.String componentToString(BitVector component)
           
private  void computeApproxMinimals(int min, BitMatrix leq)
          Compute arrows for nodes in [min, n[
private  void computeArrows(BitMatrix leq)
           
private  void computeInitialArrows()
          Computes the arrows a ->_i b for a's that abstract some surinterface of i
private  void condense()
           
private  void condense(BitMatrix T)
          Condense the relation by merging equivalent indexes and collecting the garbage nodes.
 void createInitialContext()
          Initial rigidification
 void deleteAllSoft()
           
private  void domainMerge(int src, int dest)
           
private  void domainMove(int src, int dest)
           
 java.lang.String domainsToString()
           
 java.lang.String dumpInterfaces()
           
 java.lang.String dumpRigid()
           
 void enterConstraint(int x1, int v0, int x2)
           
 void enumerate(BitVector observers, LowlevelSolutionHandler handler)
           
 void enumerate(LowlevelSolutionHandler handler)
          Satisfiability
 void eq(int x1, int x2)
          Enter the constraint x1 = x2 Assume x1 and x2 are valid indexes
 int extend()
          Add a new variable to the constraint and returns its index
 int firstNonRigid()
          Returns an index that is guaranteed to be greater than any rigid index and less or equal to any non-rigid index.
(package private)  Interface getInterface(int iid)
           
 java.lang.String getName()
          Pretty printing
 boolean hasBeenInitialized()
           
 boolean hasNoSoft()
           
 void implementsIter(K0.ImplementsIterator iterator)
           
 void indexImplements(int x, int iid)
          Enter the constraint x: iid Assume x is a valid index and iid is a valid interface id
private  void indexImplements0(int x, int iid)
           
 void indexIter(K0.IndexIterator iterator)
           
private  void indexMerge(int src, int dest)
           
private  void indexMove(int src, int dest)
           
private  java.lang.String indexToString(int index)
           
 void ineqIter(K0.IneqIterator iterator)
           
private  java.lang.String ineqToString(int x, int y)
           
 void initialAbstracts(int x, int iid)
          Enter the initial assertion that x :: iid This means that no node strictly lesser than x may implement iid
(package private)  int initialContextSize()
           
 void initialImplements(int x, int iid)
          Enter the initial assertion that x : iid
 void initialLeq(int x, int y)
          Enter the initial assertion that x <= y
(package private)  java.lang.String interfaceToString(int iid)
           
 boolean isBeingSimplified(int i)
           
 boolean isLeq(int i1, int i2)
          Assume i1 and i2 are rigid
 boolean isMinimal(int x)
           
 boolean isRigid(int x)
          Returns true if x is the index of a rigid variable.
 boolean isValidIndex(int x)
           
 void leq(int x1, int x2)
          Enter the constraint x1 <= x2.
private  void leq0(int x1, int x2)
           
 void mark()
           
 void minimal(int x)
           
 boolean negTagged(int i)
           
 int newInterface()
          Add a new interface to the constraint and returns its ID
 int nInterfaces()
          Returns the number of interfaces.
 boolean posTagged(int i)
           
private  void prepareConstraint()
           
private  void rawSatisfy()
           
 void reduceDomain(int x, boolean unit, BitVector set)
           
private  LowlevelUnsatisfiable refine(LowlevelUnsatisfiable e)
          Better error messages
private  LowlevelIncompatibleClash refineIncompatible(BitMatrix C, BitMatrix R, int what)
           
 void releaseInitialContext()
           
 void rigidify()
          Rigidify the current constraint You must have called satisfy before
 void satisfy()
           
private  void saturateAbs(BitMatrix leq)
          Saturate the constraint under the Abs axiom.
private  void setApproxToMinAbove(int abs, Interface j, BitMatrix leq)
          Finds a minimum rigid node above 'abs' that implements 'j' and set it as the approximation of 'abs' for 'j'.
private  void setSize(int n)
           
 void simplify()
           
 void simplify(K0.IndexSelector selector)
           
 int size()
           
 void solveConstructorOverloading(int x, BitVector possibilities)
           
 void solveInterfaceOverloading(int x, BitVector possibilities)
           
private  void solveOverloading(int what, int x, BitVector possibilities)
          Assume this constraint has just been satisfied possibilities contains indexes of rigid variables (if what == OVERLOADING_CONSTRUCTOR) or interfaces (if what == OVERLOADING_INTERFACE).
 void startSimplify()
          Simplification
 void stopSimplify()
           
 void subInterface(int iid1, int iid2)
          Enter the assertion that interface iid1 is a subinterface of iid2 Assume if1 and if2 are >=0 and < nInterfaces()
 void tag(int i, int variance)
           
 java.lang.String toString()
          Convert this Object to a human-readable String.
 boolean wasEntered(int i1, int i2)
          Test if a constraint i1 <: i2 was explicitely entered.
 void weakBacktrack()
           
private  BitVector weakComponent(int x0)
           
 void weakMark()
           
(package private)  int weakMarkedSize()
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
 

Field Detail

debugK0

public static boolean debugK0
Debugging

IDs

private static int IDs

ID

private int ID

callbacks

private K0.Callbacks callbacks

R

private BitMatrix R
Relation on the rigid indexes

Rt

private BitMatrix Rt
Transpose of R

m

private int m
Number of rigid indexes. Below m, the relation is closed.

m0

private int m0
Number of rigid indexes in the initial rigid context (m0 <= m)

C

private BitMatrix C
C maintains the constraint as it is entered

Ct

private BitMatrix Ct
Transpose of C

n

private int n
Total number of indexes. Invariant: m <= n && n == C.size()

minimal

private BitVector minimal
Maintains the information "x is minimal" on [0, m0[

garbage

private BitVector garbage

interfaces

private java.util.Vector interfaces

hasBeenInitialized

private boolean hasBeenInitialized
Construction of the initial rigid context

domains

private DomainVector domains
Domains

_collapsed

private BitVector _collapsed

_toCollapse

private BitVector _toCollapse

backtrackMode

private int backtrackMode
Marking / Backtracking

BACKTRACK_UNLIMITED

public static final int BACKTRACK_UNLIMITED
See Also:
Constant Field Values

BACKTRACK_ONCE

public static final int BACKTRACK_ONCE
See Also:
Constant Field Values

backup

private K0.Backup backup

ALL

public static final int ALL
Iterate thru the constraint

See Also:
Constant Field Values

SIMPLIFIED

public static final int SIMPLIFIED
Iterate thru the constraint

See Also:
Constant Field Values

weakMarkedSize

private int weakMarkedSize
Weak marking / Backtracking (only keeps track of the sizes) NB: calls to mark/backtrack and weakMark/weakBacktrack mustn't be interleaved

weakMarkedM

private int weakMarkedM

negTagged

BitVector negTagged

posTagged

BitVector posTagged

OVERLOADING_CONSTRUCTOR

private static final int OVERLOADING_CONSTRUCTOR
Overloading resolution

See Also:
Constant Field Values

OVERLOADING_INTERFACE

private static final int OVERLOADING_INTERFACE
See Also:
Constant Field Values
Constructor Detail

K0

public K0(int backtrackMode,
          K0.Callbacks callbacks)

K0

public K0(K0.Callbacks callbacks)
Method Detail

initialContextSize

int initialContextSize()

firstNonRigid

public int firstNonRigid()
Returns an index that is guaranteed to be greater than any rigid index and less or equal to any non-rigid index.

isRigid

public boolean isRigid(int x)
Returns true if x is the index of a rigid variable. the index is assumed valid

hasNoSoft

public boolean hasNoSoft()

size

public int size()

isMinimal

public boolean isMinimal(int x)

minimal

public void minimal(int x)

isValidIndex

public boolean isValidIndex(int x)

getName

public java.lang.String getName()
Pretty printing

indexToString

private java.lang.String indexToString(int index)

interfaceToString

java.lang.String interfaceToString(int iid)

domainsToString

public java.lang.String domainsToString()

weakComponent

private BitVector weakComponent(int x0)

ineqToString

private java.lang.String ineqToString(int x,
                                      int y)

componentToString

private java.lang.String componentToString(BitVector component)

toString

public java.lang.String toString()
Description copied from class: java.lang.Object
Convert this Object to a human-readable String. There are no limits placed on how long this String should be or what it should contain. We suggest you make it as intuitive as possible to be able to place it into System.out.println() 55 and such.

It is typical, but not required, to ensure that this method never completes abruptly with a java.lang.RuntimeException.

This method will be called when performing string concatenation with this object. If the result is null, string concatenation will instead use "null".

The default implementation returns getClass().getName() + "@" + Integer.toHexString(hashCode()).

dumpInterfaces

public java.lang.String dumpInterfaces()

dumpRigid

public java.lang.String dumpRigid()

setSize

private void setSize(int n)

collect

private int collect(int i,
                    int j)

collect

private void collect()

indexMove

private void indexMove(int src,
                       int dest)

indexMerge

private void indexMerge(int src,
                        int dest)
                 throws Unsatisfiable

extend

public int extend()
Add a new variable to the constraint and returns its index

nInterfaces

public int nInterfaces()
Returns the number of interfaces. Interfaces are garanteed to be numbered from 0 to nInterfaces()-1

getInterface

Interface getInterface(int iid)

hasBeenInitialized

public boolean hasBeenInitialized()

newInterface

public int newInterface()
Add a new interface to the constraint and returns its ID

subInterface

public void subInterface(int iid1,
                         int iid2)
Enter the assertion that interface iid1 is a subinterface of iid2 Assume if1 and if2 are >=0 and < nInterfaces()

initialImplements

public void initialImplements(int x,
                              int iid)
Enter the initial assertion that x : iid

initialAbstracts

public void initialAbstracts(int x,
                             int iid)
Enter the initial assertion that x :: iid This means that no node strictly lesser than x may implement iid

initialLeq

public void initialLeq(int x,
                       int y)
Enter the initial assertion that x <= y

createInitialContext

public void createInitialContext()
                          throws LowlevelUnsatisfiable
Initial rigidification

releaseInitialContext

public void releaseInitialContext()

indexImplements

public void indexImplements(int x,
                            int iid)
                     throws Unsatisfiable
Enter the constraint x: iid Assume x is a valid index and iid is a valid interface id

indexImplements0

private void indexImplements0(int x,
                              int iid)
                       throws LowlevelUnsatisfiable

eq

public void eq(int x1,
               int x2)
        throws Unsatisfiable
Enter the constraint x1 = x2 Assume x1 and x2 are valid indexes

leq

public void leq(int x1,
                int x2)
         throws Unsatisfiable
Enter the constraint x1 <= x2. Assume x1 and x2 are valid indexes.

enterConstraint

public void enterConstraint(int x1,
                            int v0,
                            int x2)
                     throws Unsatisfiable

leq0

private void leq0(int x1,
                  int x2)
           throws LowlevelUnsatisfiable

refine

private LowlevelUnsatisfiable refine(LowlevelUnsatisfiable e)
Better error messages

refineIncompatible

private LowlevelIncompatibleClash refineIncompatible(BitMatrix C,
                                                     BitMatrix R,
                                                     int what)

domainMerge

private void domainMerge(int src,
                         int dest)
                  throws Unsatisfiable

domainMove

private void domainMove(int src,
                        int dest)

reduceDomain

public void reduceDomain(int x,
                         boolean unit,
                         BitVector set)
                  throws LowlevelUnsatisfiable

collapseMinimal

private void collapseMinimal()
                      throws Unsatisfiable
Saturate the constraint C, Ct under the axiom: x <* y and Min(y) => y < x (hence x ~ y)

computeInitialArrows

private void computeInitialArrows()
                           throws LowlevelUnsatisfiable
Computes the arrows a ->_i b for a's that abstract some surinterface of i

computeApproxMinimals

private void computeApproxMinimals(int min,
                                   BitMatrix leq)
                            throws LowlevelUnsatisfiable
Compute arrows for nodes in [min, n[

setApproxToMinAbove

private void setApproxToMinAbove(int abs,
                                 Interface j,
                                 BitMatrix leq)
                          throws LowlevelUnsatisfiable
Finds a minimum rigid node above 'abs' that implements 'j' and set it as the approximation of 'abs' for 'j'.

computeArrows

private void computeArrows(BitMatrix leq)
                    throws LowlevelUnsatisfiable

saturateAbs

private void saturateAbs(BitMatrix leq)
                  throws Unsatisfiable
Saturate the constraint under the Abs axiom.

condense

private void condense()
               throws Unsatisfiable

condense

private void condense(BitMatrix T)
               throws Unsatisfiable
Condense the relation by merging equivalent indexes and collecting the garbage nodes. T is a closure of C

prepareConstraint

private void prepareConstraint()
                        throws Unsatisfiable

enumerate

public void enumerate(LowlevelSolutionHandler handler)
               throws Unsatisfiable
Satisfiability

enumerate

public void enumerate(BitVector observers,
                      LowlevelSolutionHandler handler)

satisfy

public void satisfy()
             throws Unsatisfiable

rawSatisfy

private void rawSatisfy()
                 throws Unsatisfiable

closeInterfaceRelation

private void closeInterfaceRelation()
Saturate the subtyping between interfaces under : I < J and J < K => I < K

closeImplements

BitVector[] closeImplements(BitMatrix R,
                            BitMatrix Rt)
Saturate the "implements" constraint under the following axioms: x: I and I < J => x: J x ~ y and y: I => x: I Returns an array of BitVector rigidImplementors rigidImplementors[iid] is the set of x such that x :* iid

rigidify

public void rigidify()
Rigidify the current constraint You must have called satisfy before

mark

public void mark()

backtrack

public void backtrack()

ineqIter

public void ineqIter(K0.IneqIterator iterator)
              throws Unsatisfiable

indexIter

public void indexIter(K0.IndexIterator iterator)

implementsIter

public void implementsIter(K0.ImplementsIterator iterator)
                    throws Unsatisfiable

abstractsIter

public void abstractsIter(K0.AbstractsIterator iterator)
                   throws Unsatisfiable

weakMark

public void weakMark()

weakBacktrack

public void weakBacktrack()

weakMarkedSize

int weakMarkedSize()

startSimplify

public void startSimplify()
Simplification

stopSimplify

public void stopSimplify()

posTagged

public boolean posTagged(int i)

negTagged

public boolean negTagged(int i)

clearTags

public void clearTags()

tag

public void tag(int i,
                int variance)

simplify

public void simplify()

simplify

public void simplify(K0.IndexSelector selector)

isBeingSimplified

public boolean isBeingSimplified(int i)

deleteAllSoft

public void deleteAllSoft()

isLeq

public boolean isLeq(int i1,
                     int i2)
Assume i1 and i2 are rigid

wasEntered

public boolean wasEntered(int i1,
                          int i2)
Test if a constraint i1 <: i2 was explicitely entered.

solveOverloading

private void solveOverloading(int what,
                              int x,
                              BitVector possibilities)
Assume this constraint has just been satisfied possibilities contains indexes of rigid variables (if what == OVERLOADING_CONSTRUCTOR) or interfaces (if what == OVERLOADING_INTERFACE). For each index k in possibilities, try to enter constraint x <= k or x: k and delete k from possibilities if this makes the constraint unsatisfiable

solveConstructorOverloading

public void solveConstructorOverloading(int x,
                                        BitVector possibilities)

solveInterfaceOverloading

public void solveInterfaceOverloading(int x,
                                      BitVector possibilities)
Overview  Package   Class  Use  Deprecated  Index 
Home >> All >> mlsub >> typing >> [ lowlevel overview ]  PREV CLASS  NEXT CLASS
SUMMARY: JavaDoc of mlsub.typing.lowlevel.K0 JAVADOC | Sourc code of mlsub.typing.lowlevel.K0 SOURCE | Download mlsub.typing.lowlevel.K0 DOWNLOAD | NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD