Omega-1.0: Operations on Presburger arithmetic formulae

Safe Haskell Safe-Infered

Data.Presburger.Omega.Expr

Description

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 `expToFormula`, 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 Data.Presburger.Omega.Set and Data.Presburger.Omega.Rel modules.

Synopsis

# Expressions

data Exp t Source

Integer and boolean-valued expressions.

Instances

 Show (Exp Bool) Show (Exp Int)

data Var Source

Variables. Variables are represented internally by de Bruijn indices.

Instances

 Eq Var Ord Var

## Construction

Produce the Nth bound variable. Zero is the innermost variable index.

Produce a set of variables to use as free variables in an expression. This produces the list `[nthVariable 0, nthVariable 1, ...]`

Like `takeFreeVariables`, but produce the expression corresponding to each variable.

Multiplication by -1

sumE :: [IntExp] -> IntExpSource

Summation

prodE :: [IntExp] -> IntExpSource

Multiplication

Logical negation

conjE :: [BoolExp] -> BoolExpSource

Conjunction

disjE :: [BoolExp] -> BoolExpSource

Disjunction

Conjunction

Arguments

 :: Int constant part of sum -> [(Int, [Var])] product terms -> IntExp

Create a sum of products expression

Add

Subtract

Multiply

Multiply by an integer

Test whether an integer expression is zero

Test whether an integer expression is nonnegative

Equality test

Inequality test

Greater than

Greater than or equal

Less than

Less than or equal

forallE :: (Var -> BoolExp) -> BoolExpSource

Build a universally quantified formula.

existsE :: (Var -> BoolExp) -> BoolExpSource

Build an existentially quantified formula.

## Destruction

Arguments

 :: forall a . => (Int -> [a] -> a) summation -> (Int -> [a] -> a) multiplication -> (Int -> a) integer literal -> [a] environment -> IntExp -> a

Reduce an integer expression to a value. Values for free variables are provided explicitly in an environment.

Arguments

 :: forall a b . => (Int -> [b] -> b) summation -> (Int -> [b] -> b) multiplication -> (Int -> b) integer literal -> ([a] -> a) disjunction -> ([a] -> a) conjunction -> (a -> a) negation -> (Quantifier -> (b -> a) -> a) quantification -> (PredOp -> b -> a) an integer predicate -> a true -> a false -> [b] environment -> BoolExp -> a

Reduce a boolean expression to a value. Values for free variables are provided explicitly in an environment.

## Internal data structures

These are exported to allow other modules to build the low-level representation of expressions, and avoid the cost of simplifying expressions. Normally, the `Exp` functions are sufficient.

data Expr t Source

The internal representation of expressions.

data PredOp Source

A predicate on an integer expresion.

Constructors

 IsZero IsGEZ

Instances

 Eq PredOp Show PredOp

data Quantifier Source

Constructors

 Forall Exists

Instances

 Eq Quantifier Show Quantifier

wrapExpr :: Expr t -> Exp tSource

Wrap an expression.

Wrap an expression that is known to be in simplified form.

Arguments

 :: Int constant part of sum -> [(Int, [Var])] product terms -> IntExpr

## Operations on expressions

expEqual :: Eq t => Expr t -> Expr t -> BoolSource

Decide whether two expressions are syntactically equal, modulo commutativity, associativity, and alpha-renaming.

Arguments

 :: [VarHandle] Free variables -> BoolExp Expression to convert -> Formula

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.

## Manipulating variables

Arguments

 :: Var variable to replace -> Var its replacement -> Exp t expression to rename -> Exp t renamed expression

Substitute a single variable in an expression.

Arguments

 :: Int first variable to change -> Int Amount to shift by -> Exp t Input expression -> Exp t Adjusted expression

Adjust bound variable bindings by adding an offset to all bound variable indices beyond a given level.

True if the expression has no more than the specified number of free variables.