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.
- data Exp t
- type IntExp = Exp Int
- type BoolExp = Exp Bool
- data Var
- nthVariable :: Int -> Var
- takeFreeVariables :: Int -> [Var]
- takeFreeVariables' :: Int -> [IntExp]
- varE :: Var -> IntExp
- nthVarE :: Int -> IntExp
- intE :: Int -> IntExp
- boolE :: Bool -> BoolExp
- trueE :: BoolExp
- falseE :: BoolExp
- negateE :: IntExp -> IntExp
- sumE :: [IntExp] -> IntExp
- prodE :: [IntExp] -> IntExp
- notE :: BoolExp -> BoolExp
- conjE :: [BoolExp] -> BoolExp
- disjE :: [BoolExp] -> BoolExp
- (|&&|) :: BoolExp -> BoolExp -> BoolExp
- sumOfProductsE :: Int -> [(Int, [Var])] -> IntExp
- (|+|) :: IntExp -> IntExp -> IntExp
- (|-|) :: IntExp -> IntExp -> IntExp
- (|*|) :: IntExp -> IntExp -> IntExp
- (*|) :: Int -> IntExp -> IntExp
- isZeroE :: IntExp -> BoolExp
- isNonnegativeE :: IntExp -> BoolExp
- (|==|) :: IntExp -> IntExp -> BoolExp
- (|/=|) :: IntExp -> IntExp -> BoolExp
- (|>|) :: IntExp -> IntExp -> BoolExp
- (|>=|) :: IntExp -> IntExp -> BoolExp
- (|<|) :: IntExp -> IntExp -> BoolExp
- (|<=|) :: IntExp -> IntExp -> BoolExp
- forallE :: (Var -> BoolExp) -> BoolExp
- existsE :: (Var -> BoolExp) -> BoolExp
- foldIntExp :: forall a. (Int -> [a] -> a) -> (Int -> [a] -> a) -> (Int -> a) -> [a] -> IntExp -> a
- foldBoolExp :: forall a b. (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
- data Expr t
- type IntExpr = Expr Int
- type BoolExpr = Expr Bool
- data PredOp
- data Quantifier
- wrapExpr :: Expr t -> Exp t
- 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
- expEqual :: Eq t => Expr t -> Expr t -> Bool
- expToFormula :: [VarHandle] -> BoolExp -> Formula
- rename :: Var -> Var -> Exp t -> Exp t
- adjustBindings :: Int -> Int -> Exp t -> Exp t
- variablesWithinRange :: Int -> Exp t -> Bool
Expressions
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.
Create a sum of products expression
isNonnegativeE :: IntExp -> BoolExpSource
Test whether an integer expression is nonnegative
Destruction
:: 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.
:: 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.
wrapSimplifiedExpr :: Expr t -> Exp tSource
Wrap an expression that is known to be in simplified form.
existsExpr :: BoolExpr -> BoolExprSource
Operations on expressions
expEqual :: Eq t => Expr t -> Expr t -> BoolSource
Decide whether two expressions are syntactically equal, modulo commutativity, associativity, and alpha-renaming.
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
:: Var | variable to replace |
-> Var | its replacement |
-> Exp t | expression to rename |
-> Exp t | renamed expression |
Substitute a single variable in an expression.
:: 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.