jpaul.Constraints
Class ConstraintSystem<V extends Var<Info>,Info>

java.lang.Object
  jpaul.Constraints.ConstraintSystem<V,Info>

public class ConstraintSystem<V extends Var<Info>,Info>
extends java.lang.Object

ConstraintSystem is an efficient solver for a system of constraints. Given a collection of constraints, this solver constructs an optimized form of them (mainly by unifying provably-equal variables) and computes a few internal data structures for the fixed-point solver. Later, we can solve the system a few times, obtaining different least fixed-point solutions if some of the constraints use external values that change. Hence, the name of this class: it is not just a solver, it is also an optimized, "ready-to-solve" constraint system.

A constraint system may contain variables that take values in different lattices: e.g., the values of some variables may be sets, while the values of others may be relations etc. All value lattices must be represented by subclasses of the type parameter Info, and all variables must be subclasses of the type parameter V (that is itself a subtype of Var<Info>). The relevant operations for each value lattice are represented as methods of the variables that take values in that lattice (see copy and join in the Var class). This solver performs the following optimizations:

• Unification of equal variables: The solver treats LtConstraints specially to detect strongly connected components of mutually smaller variables. Such variable can be unified into a single one. Next, for each variable vd such that the only constraint that modifies it has the form LtConstraint(vd,vd), we can unify vs and vd: in the least fixed-point solution, vd has the same value as vs.

• Iterating over strongly connected components: The fixed-point solver uses the in and out sets of each constraint to compute the dependencies between variables, compute the strongly connected components, and iterate over them, one by one, in topological order. This is much more efficient than chaotic iteration over all the constraints.

• Cheap constraints first: Inside each strongly connected component, the fixed-point solver does not execute an expensive constraint before iterating to saturation (i.e., no further progress possible) over the cheaper constraints. This is achieved by using a WorkPriorityQueue in the fixed-point solver.

Version:

$Id: ConstraintSystem.java,v 1.25 2006/03/14 02:29:28 salcianu Exp $

Author:

Alexandru Salcianu - salcianu@alum.mit.edu

See Also:

Var, Constraint

Field Summary

static boolean	CHECK_IN_OUT If on, the solver will check that each constraint reads/writes only variables declared in its in/out set.
static boolean	DEBUG Turns on several debugging messages and tests.

Constructor Summary

ConstraintSystem(java.util.Collection<Constraint<V,Info>> cs)
Creates a ConstraintSystem.

Method Summary

java.util.Map<V,V>	debugGetVarUnification() Returns a map from each original variable to the representative of its corresponding variable equivalence class.
void	debugPrintSolverStructs() Pretty-printer of solver internals using the standard output (System.out).
void	debugPrintSolverStructs(java.io.PrintStream ps) Pretty-printer of solver internals.
java.util.Collection<V>	debugUniqueVars() Returns the yet-ununified variables.
SolReader<V,Info>	solve() Solves this system of constraints.
java.util.Set<V>	vars() Returns the set of all variables from this constraint system.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

CHECK_IN_OUT

public static boolean CHECK_IN_OUT

If on, the solver will check that each constraint reads/writes only variables declared in its in/out set. Off by default. If the constraints are simple, these safety test may be very costly because they involve frequent collection membership tests.

DEBUG

public static boolean DEBUG

Turns on several debugging messages and tests. Off by default.

Constructor Detail

ConstraintSystem

public ConstraintSystem(java.util.Collection<Constraint<V,Info>> cs)

Creates a ConstraintSystem. Takes a collection of constraints, simplifies them by unifying variables known to be equal (e.g., because they are mutually smaller than one another), and makes the constraint system ready to be solved. Later, we can solve this system a few times, obtaining different solutions if some of the constraints use external values that change.

Method Detail

vars

public java.util.Set<V> vars()

Returns the set of all variables from this constraint system. The reason this method is public is that we want external entities to be able to estimate the effect of the various variable-unification optimizations by comparing the set of all variables with the set of variables that remain after unification (see debugUniqueVars()).

solve

public SolReader<V,Info> solve()

Solves this system of constraints. Returns the least solution of the constraints. Solving the same system twice may return different results, if the constraints use some external values that change in between the two calls to solve(); still, it is very important that these external values (if any) do NOT change during an execution of solve().

Note: this method is synchronized such that no two threads can execute it simultaneously: there are a few data structures that we create once and reuse in every call; also, there seems to be no reason why two threads would need to solve the same system twice.

debugPrintSolverStructs

public void debugPrintSolverStructs(java.io.PrintStream ps)

Pretty-printer of solver internals.

debugPrintSolverStructs

public void debugPrintSolverStructs()

Pretty-printer of solver internals using the standard output (System.out).

debugGetVarUnification

public java.util.Map<V,V> debugGetVarUnification()

Returns a map from each original variable to the representative of its corresponding variable equivalence class.

debugUniqueVars

public java.util.Collection<V> debugUniqueVars()

Returns the yet-ununified variables. These are the representatives of the equivalence classes of variables.