compiler/edu.cornell.cs.apl.viaduct.algebra.solver/ConstraintSystem

ConstraintSystem

class ConstraintSystem<A : HeytingAlgebra<A>, T : Throwable>(top: A)

Given a set of constraints of the form t1 ≤ t2, finds the unique maximum solution if it exists.

A solution to a set of constraints is an assignment of values to all variables in the system. A maximum solution assigns the greatest possible value to each variable, where greatest is with respect to PartialOrder.lessThanOrEqualTo.

Parameters

domain of values

type of exceptions thrown when there are unsatisfiable constraints

top

greatest element of A

Constructors

ConstraintSystem

fun <A : HeytingAlgebra<A>> ConstraintSystem(top: A)

Functions

addLessThanOrEqualToConstraint

fun addLessThanOrEqualToConstraint(lhs: AtomicTerm<A>, rhs: RightHandTerm<A>, failWith: (A, A) -> T)

fun addLessThanOrEqualToConstraint(lhs: LeftHandTerm<A>, rhs: AtomicTerm<A>, failWith: (A, A) -> T)

Add the constraint lhs <= rhs to the system.

addNewVariable

fun addNewVariable(label: Any): VariableTerm<A>

Creates a fresh variable and add it to the system.

exportDotGraph

fun exportDotGraph(writer: Writer?)

Output the constraint system as a DOT graph.

solve

fun solve(): ConstraintSolution<A>

Returns the greatest solution to the set of constraints in the system.