-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Integer sets and relations using Presburger arithmetic
--   
@package Omega
@version 1.0.2


-- | This module provides a low-level interface for creating, manipulating,
--   and querying Presburger arithmetic formulae. The real work is done by
--   the C++ Omega library
--   (<a>http://github.com/davewathaverford/the-omega-project</a>).
--   
--   The main data types are <a>OmegaSet</a> and <a>OmegaRel</a>, which use
--   a formula to define a set or relation, respectively, on integer-valued
--   points in Cartesian space. A typical use involves creating a
--   Presburger arithmetic <a>Formula</a>, using it to create a set or
--   relation, and then querying the set or relation.
module Data.Presburger.Omega.LowLevel

-- | Data types containing Presburger formulae.
class Presburger a

-- | A set of points in Z^n. This is a wrapper around the Omega library's
--   Relation type.
data OmegaSet

-- | Create an Omega set. The first parameter is the number of dimensions
--   the set inhabits. The second parameter builds a formula defining the
--   set's members. The set's members are those points for which the
--   formula evaluates to True.
newOmegaSet :: Int -> ([VarHandle] -> Formula) -> IO OmegaSet

-- | A relation from points in a <i>domain</i> Z^m to points in a
--   <i>range</i> Z^n. This is a wrapper around the Omega library's
--   Relation type.
--   
--   A relation can be considered as just a set of points in Z^(m+n).
--   However, many routines treat the domain and range differently.
data OmegaRel

-- | Create an Omega relation. The first two parameters are the number of
--   dimensions of the domain and range, respectively. The third parameter
--   builds a formula defining the relation. Two points are related iff the
--   formula evaluates to True on those points.
newOmegaRel :: Int -> Int -> ([VarHandle] -> [VarHandle] -> Formula) -> IO OmegaRel

-- | Inspect a set's low-level representation directly. This function takes
--   care of data structure traversal and relies on other routines to
--   interpret the data.
--   
--   All three accumulating functions take the set variables as their first
--   parameter, and any existentially quantified variables as their second
--   parameter. The set variables are returned along with a result value.
queryDNFSet :: ([VarHandle] -> [VarHandle] -> [Coefficient] -> Int -> a -> a) -> a -> ([VarHandle] -> [VarHandle] -> [Coefficient] -> Int -> b -> b) -> b -> ([VarHandle] -> [VarHandle] -> a -> b -> c -> c) -> c -> OmegaSet -> IO ([VarHandle], c)

-- | Inspect a relation's low-level representation directly. This function
--   takes care of data structure traversal and relies on other routines to
--   interpret the data.
--   
--   All three accumulating functions take the relation's input and output
--   variables as their first and second parameters, respectively, and any
--   existentially quantified variables as their second parameter. The
--   relation's input and output variables are returned along with a result
--   value.
queryDNFRelation :: ([VarHandle] -> [VarHandle] -> [VarHandle] -> [Coefficient] -> Int -> a -> a) -> a -> ([VarHandle] -> [VarHandle] -> [VarHandle] -> [Coefficient] -> Int -> b -> b) -> b -> ([VarHandle] -> [VarHandle] -> [VarHandle] -> a -> b -> c -> c) -> c -> OmegaRel -> IO ([VarHandle], [VarHandle], c)

-- | Determine a lower bound on whether the formula is satisfiable. The
--   lower bound is based on treating all UNKNOWN constraints as false.
lowerBoundSatisfiable :: Presburger a => a -> IO Bool

-- | Determine an upper bound on whether the formula is satisfiable. The
--   upper bound is based on treating all UNKNOWN constraints as true.
upperBoundSatisfiable :: Presburger a => a -> IO Bool

-- | Use simple, fast tests to decide whether the formula is a tautology.
obviousTautology :: Presburger a => a -> IO Bool

-- | True if the formula is a tautology.
definiteTautology :: Presburger a => a -> IO Bool

-- | True if the formula has no UNKNOWN constraints.
exact :: Presburger a => a -> IO Bool

-- | True if the formula has UNKNOWN constraints.
inexact :: Presburger a => a -> IO Bool

-- | True if the formula is UNKNOWN.
unknown :: Presburger a => a -> IO Bool

-- | Compute the upper bound of a set or relation by setting all UNKNOWN
--   constraints to true.
upperBound :: Presburger a => a -> IO a

-- | Compute the lower bound of a set or relation by setting all UNKNOWN
--   constraints to false.
lowerBound :: Presburger a => a -> IO a

-- | Test whether two sets or relations are equal. The sets or relations
--   must have the same arity.
--   
--   The answer is precise if both arguments are <a>exact</a>. If either
--   argument is inexact, this function returns <tt>False</tt>.
equal :: Presburger a => a -> a -> IO Bool

-- | Compute the union of two sets or relations. The sets or relations must
--   have the same arity.
union :: Presburger a => a -> a -> IO a

-- | Compute the intersection of two sets or relations. The sets or
--   relations must have the same arity.
intersection :: Presburger a => a -> a -> IO a

-- | Compute the composition of two sets or relations. The first relation's
--   domain must be the same dimension as the second's range.
composition :: OmegaRel -> OmegaRel -> IO OmegaRel

-- | Restrict the domain of a relation. If <tt>domain r</tt> is <tt>d</tt>,
--   then <tt>domain =&lt;&lt; restrictDomain r s</tt> is <tt>intersection
--   d s</tt>.
restrictDomain :: OmegaRel -> OmegaSet -> IO OmegaRel

-- | Restrict the range of a relation. If <tt>range r</tt> is <tt>d</tt>,
--   then <tt>range =&lt;&lt; restrictRange r s</tt> is <tt>intersection d
--   s</tt>.
restrictRange :: OmegaRel -> OmegaSet -> IO OmegaRel

-- | Compute the difference of two relations or sets. The members of
--   <tt>difference x y</tt> are the members of <tt>x</tt> that are not
--   members of <tt>y</tt>.
difference :: Presburger a => a -> a -> IO a

-- | Compute the cross product of two sets. The cross product relates every
--   element of <tt>s</tt> to every element of <tt>y</tt>.
crossProduct :: OmegaSet -> OmegaSet -> IO OmegaRel

-- | The <a>gist</a> routine takes a parameter specifying how much effort
--   to put into generating a good result. Higher effort takes more time.
--   It's unspecified what a given effort level does.
data Effort
Light :: Effort
Moderate :: Effort
Strenuous :: Effort

-- | Get the gist of a set or relation, given some background truth. The
--   gist operator uses heuristics to make a set or relation simpler, while
--   still retaining sufficient information to regenerate the original by
--   re-introducing the background truth. The sets or relations must have
--   the same arity.
--   
--   Given <tt>x</tt> computed by
--   
--   <pre>
--   x &lt;- intersection given =&lt;&lt; gist effort r given
--   </pre>
--   
--   we have <tt>x == r</tt>.
gist :: Presburger a => Effort -> a -> a -> IO a

-- | Get the transitive closure of a relation. In some cases, the
--   transitive closure cannot be computed exactly, in which case a lower
--   bound is returned.
transitiveClosure :: OmegaRel -> IO OmegaRel

-- | Get the domain of a relation.
domain :: OmegaRel -> IO OmegaSet

-- | Get the range of a relation.
range :: OmegaRel -> IO OmegaSet

-- | Get the inverse of a relation.
inverse :: OmegaRel -> IO OmegaRel

-- | Get the complement of a set or relation.
complement :: Presburger a => a -> IO a

-- | Get the deltas of a relation. The relation's input dimensionality must
--   be the same as its output dimensionality.
deltas :: OmegaRel -> IO OmegaSet

-- | Approximate a set or relation by allowing all existentially quantified
--   variables to take on rational values. This allows these variables to
--   be eliminated from the formula.
approximate :: Presburger a => a -> IO a

-- | A boolean-valued Presburger formula.
data Formula

-- | Truth.
true :: Formula

-- | Falsity.
false :: Formula

-- | Logical conjunction (and).
conjunction :: [Formula] -> Formula

-- | Logical disjunction (or).
disjunction :: [Formula] -> Formula

-- | Logical negation.
negation :: Formula -> Formula

-- | A variable in a formula.
data VarHandle

-- | Universal quantification. The <a>VarHandle</a> parameter is the
--   variable bound by the quantifier.
qForall :: (VarHandle -> Formula) -> Formula

-- | Existential quantification. The <a>VarHandle</a> parameter is the
--   variable bound by the quantifier.
qExists :: (VarHandle -> Formula) -> Formula

-- | An integer-valued term <tt>n*v</tt> in a formula.
data Coefficient
Coefficient :: {-# UNPACK #-} !VarHandle -> {-# UNPACK #-} !Int -> Coefficient
coeffVar :: Coefficient -> {-# UNPACK #-} !VarHandle
coeffValue :: Coefficient -> {-# UNPACK #-} !Int

-- | Construct an inequation of the form <tt>a*x + b*y + ... + d &gt;=
--   0</tt>.
inequality :: [Coefficient] -> Int -> Formula

-- | Construct an equation of the form <tt>a*x + b*y + ... + d = 0</tt>.
equality :: [Coefficient] -> Int -> Formula
instance Eq Effort
instance Show Effort
instance Enum Effort
instance Eq VarHandle
instance Storable Coefficient
instance Show Coefficient
instance Presburger OmegaRel
instance Show OmegaRel
instance Presburger OmegaSet
instance Show OmegaSet
instance Iterator C_GEQ_Iterator C_GEQ_Handle
instance Iterator C_EQ_Iterator C_EQ_Handle
instance Iterator (C_Tuple_Iterator (Ptr a)) (Ptr a)
instance Iterator C_DNF_Iterator C_Conjunct
instance Logical C_Quantifier
instance Logical C_And
instance Logical C_Form
instance Logical C_Relation
instance Constraint GEQ_Handle
instance Constraint EQ_Handle


-- | Expressions are the high-level interface for creating Presburger
--   formulae. As in Presburger arithmetic, expressions can represent
--   addition, subtraction, quantification, inequalities, and boolean
--   operators.
--   
--   Expressions allow formulas to be input in a freeform manner. When
--   converted to a formula with <a>expToFormula</a>, they will be
--   simplified to a form that the underlying library can use.
--   Multplication is unrestricted; however, if an expression involves the
--   product of two non-constant terms, it cannot be converted to a
--   formula.
--   
--   This module handles expressions and converts them to formulas. Sets
--   and relations are managed by the <a>Data.Presburger.Omega.Set</a> and
--   <a>Data.Presburger.Omega.Rel</a> modules.
module Data.Presburger.Omega.Expr

-- | Integer and boolean-valued expressions.
data Exp t
type IntExp = Exp Int
type BoolExp = Exp Bool

-- | Variables. Variables are represented internally by de Bruijn indices.
data Var

-- | Produce the Nth bound variable. Zero is the innermost variable index.
nthVariable :: Int -> Var

-- | Produce a set of variables to use as free variables in an expression.
--   This produces the list <tt>[nthVariable 0, nthVariable 1, ...]</tt>
takeFreeVariables :: Int -> [Var]

-- | Like <a>takeFreeVariables</a>, but produce the expression
--   corresponding to each variable.
takeFreeVariables' :: Int -> [IntExp]
varE :: Var -> IntExp
nthVarE :: Int -> IntExp
intE :: Int -> IntExp
boolE :: Bool -> BoolExp
trueE :: BoolExp
falseE :: BoolExp

-- | Multiplication by -1
negateE :: IntExp -> IntExp

-- | Summation
sumE :: [IntExp] -> IntExp

-- | Multiplication
prodE :: [IntExp] -> IntExp

-- | Logical negation
notE :: BoolExp -> BoolExp

-- | Conjunction
conjE :: [BoolExp] -> BoolExp

-- | Disjunction
disjE :: [BoolExp] -> BoolExp

-- | Conjunction
(|&&|) :: BoolExp -> BoolExp -> BoolExp

-- | Create a sum of products expression
sumOfProductsE :: Int -> [(Int, [Var])] -> IntExp

-- | Add
(|+|) :: IntExp -> IntExp -> IntExp

-- | Subtract
(|-|) :: IntExp -> IntExp -> IntExp

-- | Multiply
(|*|) :: IntExp -> IntExp -> IntExp

-- | Multiply by an integer
(*|) :: Int -> IntExp -> IntExp

-- | Test whether an integer expression is zero
isZeroE :: IntExp -> BoolExp

-- | Test whether an integer expression is nonnegative
isNonnegativeE :: IntExp -> BoolExp

-- | Equality test
(|==|) :: IntExp -> IntExp -> BoolExp

-- | Inequality test
(|/=|) :: IntExp -> IntExp -> BoolExp

-- | Greater than
(|>|) :: IntExp -> IntExp -> BoolExp

-- | Greater than or equal
(|>=|) :: IntExp -> IntExp -> BoolExp

-- | Less than
(|<|) :: IntExp -> IntExp -> BoolExp

-- | Less than or equal
(|<=|) :: IntExp -> IntExp -> BoolExp

-- | Build a universally quantified formula.
forallE :: (Var -> BoolExp) -> BoolExp

-- | Build an existentially quantified formula.
existsE :: (Var -> BoolExp) -> BoolExp

-- | Reduce an integer expression to a value. Values for free variables are
--   provided explicitly in an environment.
foldIntExp :: (Int -> [a] -> a) -> (Int -> [a] -> a) -> (Int -> a) -> [a] -> (IntExp -> a)

-- | Reduce a boolean expression to a value. Values for free variables are
--   provided explicitly in an environment.
foldBoolExp :: (Int -> [b] -> b) -> (Int -> [b] -> b) -> (Int -> b) -> ([a] -> a) -> ([a] -> a) -> (a -> a) -> (Quantifier -> (b -> a) -> a) -> (PredOp -> b -> a) -> a -> a -> [b] -> (BoolExp -> a)

-- | The internal representation of expressions.
data Expr t
type IntExpr = Expr Int
type BoolExpr = Expr Bool

-- | A predicate on an integer expresion.
data PredOp
IsZero :: PredOp
IsGEZ :: PredOp
data Quantifier
Forall :: Quantifier
Exists :: Quantifier

-- | Wrap an expression.
wrapExpr :: Expr t -> Exp t

-- | Wrap an expression that is known to be in simplified form.
wrapSimplifiedExpr :: Expr t -> Exp t
varExpr :: Var -> IntExpr
sumOfProductsExpr :: Int -> [(Int, [Var])] -> IntExpr
conjExpr :: [BoolExpr] -> BoolExpr
disjExpr :: [BoolExpr] -> BoolExpr
testExpr :: PredOp -> IntExpr -> BoolExpr
existsExpr :: BoolExpr -> BoolExpr

-- | Decide whether two expressions are syntactically equal, modulo
--   commutativity, associativity, and alpha-renaming.
expEqual :: Eq t => Expr t -> Expr t -> Bool

-- | Convert a boolean expression to a formula.
--   
--   The expression must be a Presburger formula. In particular, if an
--   expression involves the product of two non-constant terms, it cannot
--   be converted to a formula. The library internally simplifies
--   expressions to sum-of-products form, so complex expressions are valid
--   as long as each simplified product has at most one variable.
expToFormula :: [VarHandle] -> BoolExp -> Formula

-- | Substitute a single variable in an expression.
rename :: Var -> Var -> Exp t -> Exp t

-- | Adjust bound variable bindings by adding an offset to all bound
--   variable indices beyond a given level.
adjustBindings :: Int -> Int -> Exp t -> Exp t

-- | True if the expression has no more than the specified number of free
--   variables.
variablesWithinRange :: Int -> Exp t -> Bool
instance Eq Var
instance Ord Var
instance Eq PredOp
instance Show PredOp
instance Eq Quantifier
instance Show Quantifier
instance Show (CAUOp t)
instance Eq (CAUOp t)
instance Show (Exp Bool)
instance Show (Exp Int)


-- | Sets whose members are represented compactly using a Presburger
--   arithmetic formula. This is a high-level interface to <a>OmegaSet</a>.
--   
--   This module is intended to be imported qualified, e.g.
--   
--   <pre>
--   import qualified Data.Presburger.Omega.Set as WSet
--   </pre>
module Data.Presburger.Omega.Set

-- | Sets of points in Z^n defined by a formula.
data Set

-- | Create a set whose members are defined by a predicate.
--   
--   The expression should have one free variable for each dimension.
--   
--   For example, the set of all points on the plane is
--   
--   <pre>
--   set 2 (\[_, _] -&gt; trueE)
--   </pre>
--   
--   The set of all points (x, y, z) where x &gt; y + z is
--   
--   <pre>
--   set 3 (\[x,y,z] -&gt; x |&gt;| y |+| z)
--   </pre>
set :: Int -> ([Var] -> BoolExp) -> Set

-- | Convert an <a>OmegaSet</a> to a <a>Set</a>.
fromOmegaSet :: OmegaSet -> IO Set

-- | Convert a <a>Set</a> to an <a>OmegaSet</a>.
toOmegaSet :: Set -> OmegaSet

-- | Get the dimensionality of the space a set inhabits
dimension :: Set -> Int

-- | Get the predicate defining a set's members
predicate :: Set -> BoolExp
lowerBoundSatisfiable :: Set -> Bool
upperBoundSatisfiable :: Set -> Bool
obviousTautology :: Set -> Bool
definiteTautology :: Set -> Bool

-- | True if the set has no UNKNOWN constraints.
exact :: Set -> Bool

-- | True if the set has UNKNOWN constraints.
inexact :: Set -> Bool

-- | True if the set is completely UNKNOWN.
unknown :: Set -> Bool

-- | Test whether two sets are equal. The sets must have the same dimension
--   (<tt>dimension s1 == dimension s2</tt>), or an error will be raised.
--   
--   The answer is precise if both relations are <a>exact</a>. If either
--   relation is inexact, this function returns <tt>False</tt>.
equal :: Set -> Set -> Bool

-- | Compute the upper bound of a set by setting all UNKNOWN constraints to
--   true.
upperBound :: Set -> Set

-- | Compute the lower bound of a set by setting all UNKNOWN constraints to
--   false.
lowerBound :: Set -> Set

-- | Union of two sets. The sets must have the same dimension
--   (<tt>dimension s1 == dimension s2</tt>), or an error will be raised.
union :: Set -> Set -> Set

-- | Intersection of two sets. The sets must have the same dimension
--   (<tt>dimension s1 == dimension s2</tt>), or an error will be raised.
intersection :: Set -> Set -> Set

-- | Difference of two sets. The sets must have the same dimension
--   (<tt>dimension s1 == dimension s2</tt>), or an error will be raised.
difference :: Set -> Set -> Set

-- | The <a>gist</a> routine takes a parameter specifying how much effort
--   to put into generating a good result. Higher effort takes more time.
--   It's unspecified what a given effort level does.
data Effort
Light :: Effort
Moderate :: Effort
Strenuous :: Effort

-- | Get the gist of a set, given some background truth. The gist operator
--   uses heuristics to simplify the set while retaining sufficient
--   information to regenerate the original by re-introducing the
--   background truth. The sets must have the same dimension.
--   
--   The gist satisfies the property
--   
--   <pre>
--   x === gist effort x given `intersection` given
--   </pre>
gist :: Effort -> Set -> Set -> Set
complement :: Set -> Set
approximate :: Set -> Set
instance Show Set


-- | Relations whose members are represented compactly using a Presburger
--   arithmetic formula. This is a high-level interface to <a>OmegaRel</a>.
--   
--   This module is intended to be imported qualified, e.g.
--   
--   <pre>
--   import qualified Data.Presburger.Omega.Rel as WRel
--   </pre>
module Data.Presburger.Omega.Rel

-- | A relation from points in a <i>domain</i> Z^m to points in a
--   <i>range</i> Z^n.
--   
--   A relation can be considered just a set of points in Z^(m+n). However,
--   many functions that operate on relations treat the domain and range
--   differently.
data Rel

-- | Create a relation whose members are defined by a predicate.
--   
--   The expression should have <tt>m+n</tt> free variables, where
--   <tt>m</tt> and <tt>n</tt> are the first two parameters. The first
--   <tt>m</tt> variables refer to the domain, and the remaining variables
--   refer to the range.
rel :: Int -> Int -> BoolExp -> Rel

-- | Create a relation where each output is a function of the inputs.
--   
--   Each expression should have <tt>m</tt> free variables, where
--   <tt>m</tt> is the first parameter.
--   
--   For example, the relation <tt>{(x, y) -&gt; (y, x) | x &gt; 0
--   &amp;&amp; y &gt; 0}</tt> is
--   
--   <pre>
--   let [x, y] = takeFreeVariables' 2
--   in functionalRel 2 [y, x] (conjE [y |&gt;| intE 0, x |&gt;| intE 0])
--   </pre>
functionalRel :: Int -> [IntExp] -> BoolExp -> Rel

-- | Convert an <a>OmegaRel</a> to a <a>Rel</a>.
fromOmegaRel :: OmegaRel -> IO Rel

-- | Convert a <a>Rel</a> to an <a>OmegaRel</a>.
toOmegaRel :: Rel -> OmegaRel

-- | Get the dimensionality of a relation's domain
inputDimension :: Rel -> Int

-- | Get the dimensionality of a relation's range
outputDimension :: Rel -> Int

-- | Get the predicate defining a relation.
predicate :: Rel -> BoolExp
lowerBoundSatisfiable :: Rel -> Bool
upperBoundSatisfiable :: Rel -> Bool
obviousTautology :: Rel -> Bool
definiteTautology :: Rel -> Bool

-- | True if the relation has no UNKNOWN constraints.
exact :: Rel -> Bool

-- | True if the relation has UNKNOWN constraints.
inexact :: Rel -> Bool

-- | True if the relation is entirely UNKNOWN.
unknown :: Rel -> Bool

-- | Test whether two relations are equal. The relations must have the same
--   dimension (<tt>inputDimension r1 == inputDimension r2 &amp;&amp;
--   outputDimension r1 == outputDimension r2</tt>), or an error will be
--   raised.
--   
--   The answer is precise if both relations are <a>exact</a>. If either
--   relation is inexact, this function returns <tt>False</tt>.
equal :: Rel -> Rel -> Bool
upperBound :: Rel -> Rel
lowerBound :: Rel -> Rel

-- | Union of two relations. The relations must have the same dimension
--   (<tt>inputDimension r1 == inputDimension r2 &amp;&amp; outputDimension
--   r1 == outputDimension r2</tt>), or an error will be raised.
union :: Rel -> Rel -> Rel

-- | Intersection of two relations. The relations must have the same
--   dimension (<tt>inputDimension r1 == inputDimension r2 &amp;&amp;
--   outputDimension r1 == outputDimension r2</tt>), or an error will be
--   raised.
intersection :: Rel -> Rel -> Rel

-- | Composition of two relations. The second relation's output must be the
--   same size as the first's input (<tt>outputDimension r2 ==
--   inputDimension r1</tt>), or an error will be raised.
composition :: Rel -> Rel -> Rel

-- | Same as <a>composition</a>, with the arguments swapped.
join :: Rel -> Rel -> Rel

-- | Restrict the domain of a relation.
--   
--   <pre>
--   domain (restrictDomain r s) === intersection (domain r) s
--   </pre>
restrictDomain :: Rel -> Set -> Rel

-- | Restrict the range of a relation.
--   
--   <pre>
--   range (restrictRange r s) === intersection (range r) s
--   </pre>
restrictRange :: Rel -> Set -> Rel

-- | Difference of two relations. The relations must have the same
--   dimension (<tt>inputDimension r1 == inputDimension r2 &amp;&amp;
--   outputDimension r1 == outputDimension r2</tt>), or an error will be
--   raised.
difference :: Rel -> Rel -> Rel

-- | Cross product of two sets.
crossProduct :: Set -> Set -> Rel

-- | The <a>gist</a> routine takes a parameter specifying how much effort
--   to put into generating a good result. Higher effort takes more time.
--   It's unspecified what a given effort level does.
data Effort
Light :: Effort
Moderate :: Effort
Strenuous :: Effort

-- | Get the gist of a relation, given some background truth. The gist
--   operator uses heuristics to simplify the relation while retaining
--   sufficient information to regenerate the original by re-introducing
--   the background truth. The relations must have the same input
--   dimensions and the same output dimensions.
--   
--   The gist satisfies the property
--   
--   <pre>
--   x === gist effort x given `intersection` given
--   </pre>
gist :: Effort -> Rel -> Rel -> Rel

-- | Get the transitive closure of a relation. In some cases, the
--   transitive closure cannot be computed exactly, in which case a lower
--   bound is returned.
transitiveClosure :: Rel -> Rel
domain :: Rel -> Set
range :: Rel -> Set

-- | Invert a relation, swapping the domain and range.
inverse :: Rel -> Rel

-- | Get the complement of a relation.
complement :: Rel -> Rel
deltas :: Rel -> Set

-- | Approximate a relation by allowing all existentially quantified
--   variables to take on rational values. This allows these variables to
--   be eliminated from the formula.
approximate :: Rel -> Rel
instance Show Rel