ptolemy.graph
Class InequalitySolver

java.lang.Object
  extended by ptolemy.graph.InequalitySolver

public class InequalitySolver
extends java.lang.Object

An algorithm to solve a set of inequality constraints. This algorithm is based on J. Rehof and T. Mogensen, "Tractable Constraints in Finite Semilattices," Third International Static Analysis Symposium, pp. 285-301, Vol 1145 of Lecture Notes in Computer Science, Springer, Sept., 1996.

The algorithm in Rehof works for definite inequalities. This class does not enforce this requirement. However, if the inequalities are not definite, this solver may not be able to find the solution even when the set of inequalities is satisfiable. See the above paper for details.

This solver supports finding both the least and greatest solutions (if they exist). It assumes that the CPO passed to the constructor is a lattice, but it does not verify it. If the algorithm finds that the LUB or GLB of some elements does not exist, an Exception is thrown.

Since:
Ptolemy II 0.2
Version:
$Id: InequalitySolver.java 57040 2010-01-27 20:52:32Z cxh $
Author:
Yuhong Xiong
Accepted Rating:
Red (cxh)
Proposed Rating:
Green (cxh)

Nested Class Summary
private static class InequalitySolver.Info
           
 
Field Summary
private  java.util.Hashtable _Clist
           
private  CPO _cpo
           
private  java.util.ArrayList _Ilist
           
 
Constructor Summary
InequalitySolver(CPO cpo)
          Construct an inequality solver.
 
Method Summary
private  void _addToClist(InequalityTerm[] variables, java.lang.Integer indexWrap)
           
private  java.util.Iterator _filterVariables(java.lang.Object value)
           
private  boolean _solve(boolean least)
           
 void addInequalities(java.util.Iterator inequalities)
          Add a group of inequalities to the set of constraints.
 void addInequality(Inequality ineq)
          Add an Inequality to the set of constraints.
 java.util.Iterator bottomVariables()
          Return an Iterator of the variables whose current values are the bottom of the underlying CPO.
 java.lang.String description()
          Return a description of this solver as a String.
 boolean solveGreatest()
          Solve the set of inequalities for the greatest solution.
 boolean solveLeast()
          Solve the set of inequalities for the least solution.
 java.util.Iterator topVariables()
          Return an Iterator of the variables whose current values are the top of the underlying CPO.
 java.util.Iterator unsatisfiedInequalities()
          Return an Iterator of Inequalities that are not satisfied with the current value of variables.
 java.util.Iterator variables()
          Return an Iterator of all the variables in the inequality constraints.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

_cpo

private CPO _cpo

_Ilist

private java.util.ArrayList _Ilist

_Clist

private java.util.Hashtable _Clist
Constructor Detail

InequalitySolver

public InequalitySolver(CPO cpo)
Construct an inequality solver.

Parameters:
cpo - The CPO over which the inequalities are defined.
Method Detail

addInequalities

public void addInequalities(java.util.Iterator inequalities)
Add a group of inequalities to the set of constraints.

Parameters:
inequalities - An Iterator for instances of Inequality.

addInequality

public void addInequality(Inequality ineq)
Add an Inequality to the set of constraints.

Parameters:
ineq - An Inequality.

bottomVariables

public java.util.Iterator bottomVariables()
                                   throws IllegalActionException
Return an Iterator of the variables whose current values are the bottom of the underlying CPO. If none of the variables have its current value set to the bottom, an empty Iterator is returned.

Returns:
An Iterator of InequalityTerms
Throws:
InvalidStateException - If the underlying CPO does not have a bottom element.
IllegalActionException - If testing any one of the variables throws an exception.

description

public java.lang.String description()
Return a description of this solver as a String.

Returns:
A description of this solver.

solveGreatest

public boolean solveGreatest()
                      throws IllegalActionException
Solve the set of inequalities for the greatest solution. If the set of inequalities is definite (when solving for the greatest solution, definite means that the lesser terms of all the inequalities are either constants or single variables), this method can always determine satisfiability. In this case, if the set of inequalities is satisfiable, this method returns true, and the variables are set to the greatest solution. If the set of inequalities is not satisfiable, this method returns false.

If the set of inequalities is not definite, this method cannot always determine satisfiability. In this case, if the set of inequalities is satisfiable, this method may or may not return true. If this method returns true, the variables are set to the greatest solution. If the set of inequalities is not satisfiable, this method returns false.

In any case, if this method returns false, the variables are set to the greatest solution for the subset of inequalities whose lesser terms are a single variable. See the paper referred in the class document for details.

Returns:
True if a solution for the inequalities is found, false otherwise.
Throws:
IllegalActionException - If testing any one of the inequalities throws an exception.

solveLeast

public boolean solveLeast()
                   throws IllegalActionException
Solve the set of inequalities for the least solution. If the set of inequalities is definite (when solving for the least solution, definite means that the greater terms of all the inequalities are either constants or single variables), this method can always determine satisfiability. In this case, if the set of inequalities is satisfiable, this method returns true, and the variables are set to the least solution. If the set of inequalities is not satisfiable, this method returns false.

If the set of inequalities is not definite, this method cannot always determine satisfiability. In this case, if the set of inequalities is satisfiable, this method may or may not return true. If this method returns true, the variables are set to the least solution. If the set of inequalities is not satisfiable, this method returns false.

In any case, if this method returns false, the variables are set to the least solution for the subset of inequalities whose greater terms are a single variable. See the paper referred to in the class document for details.

Returns:
True if a solution for the inequalities is found, false otherwise.
Throws:
IllegalActionException - If testing any one of the inequalities throws an exception.

topVariables

public java.util.Iterator topVariables()
                                throws IllegalActionException
Return an Iterator of the variables whose current values are the top of the underlying CPO. If none of the variables have the current value set to the top, an empty Iterator is returned.

Returns:
An Iterator of InequalityTerms
Throws:
InvalidStateException - If the underlying CPO does not have a top element.
IllegalActionException - If testing any one of the variables throws an exception.

unsatisfiedInequalities

public java.util.Iterator unsatisfiedInequalities()
                                           throws IllegalActionException
Return an Iterator of Inequalities that are not satisfied with the current value of variables. If all the inequalities are satisfied, an empty Iterator is returned.

Returns:
An Iterator of Inequalities
Throws:
IllegalActionException - If testing any one of the inequalities throws an exception.

variables

public java.util.Iterator variables()
Return an Iterator of all the variables in the inequality constraints.

Returns:
An Iterator of InequalityTerms
Throws:
IllegalActionException - If testing any one of the variables throws an exception.

_addToClist

private void _addToClist(InequalityTerm[] variables,
                         java.lang.Integer indexWrap)

_filterVariables

private java.util.Iterator _filterVariables(java.lang.Object value)
                                     throws IllegalActionException
Throws:
IllegalActionException

_solve

private boolean _solve(boolean least)
                throws IllegalActionException
Throws:
IllegalActionException