Omega-0.2.2: Operations on Presburger arithmetic formulae

Data.Presburger.Omega.Expr

Contents

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

data Var Source

Variables. Variables are represented internally by de Bruijn indices.

Instances

Construction

nthVariable :: Int -> VarSource

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

takeFreeVariables :: Int -> [Var]Source

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

takeFreeVariables' :: Int -> [IntExp]Source

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

negateE :: IntExp -> IntExpSource

Multiplication by -1

sumE :: [IntExp] -> IntExpSource

Summation

prodE :: [IntExp] -> IntExpSource

Multiplication

notE :: BoolExp -> BoolExpSource

Logical negation

conjE :: [BoolExp] -> BoolExpSource

Conjunction

disjE :: [BoolExp] -> BoolExpSource

Disjunction

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

Conjunction

sumOfProductsESource

Arguments

:: Int

constant part of sum

-> [(Int, [Var])]

product terms

-> IntExp 

Create a sum of products expression

(|-|) :: IntExp -> IntExp -> IntExpSource

Subtract

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

Multiply

(*|) :: Int -> IntExp -> IntExpSource

Multiply by an integer

isZeroE :: IntExp -> BoolExpSource

Test whether an integer expression is zero

isNonnegativeE :: IntExp -> BoolExpSource

Test whether an integer expression is nonnegative

(|==|) :: IntExp -> IntExp -> BoolExpSource

Equality test

(|/=|) :: IntExp -> IntExp -> BoolExpSource

Inequality test

(|>|) :: IntExp -> IntExp -> BoolExpSource

Greater than

(|>=|) :: IntExp -> IntExp -> BoolExpSource

Greater than or equal

(|<|) :: IntExp -> IntExp -> BoolExpSource

Less than

(|<=|) :: IntExp -> IntExp -> BoolExpSource

Less than or equal

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

Build a universally quantified formula.

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

Build an existentially quantified formula.

Destruction

foldIntExpSource

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.

foldBoolExpSource

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

data Quantifier Source

Constructors

Forall 
Exists 

wrapExpr :: Expr t -> Exp tSource

Wrap an expression.

wrapSimplifiedExpr :: Expr t -> Exp tSource

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

sumOfProductsExprSource

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.

expToFormulaSource

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

renameSource

Arguments

:: Var

variable to replace

-> Var

its replacement

-> Exp t

expression to rename

-> Exp t

renamed expression

Substitute a single variable in an expression.

adjustBindingsSource

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.

variablesWithinRange :: Int -> Exp t -> BoolSource

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