module Data.Presburger.Omega.Expr
(
Exp, IntExp, BoolExp,
Var,
nthVariable, takeFreeVariables, takeFreeVariables',
varE, nthVarE, intE, boolE, trueE, falseE, negateE,
sumE, prodE, notE, conjE, disjE,
(|&&|),
sumOfProductsE,
(|+|), (|-|), (|*|), (*|),
isZeroE, isNonnegativeE,
(|==|), (|/=|), (|>|), (|>=|), (|<|), (|<=|),
forallE, existsE,
foldIntExp, foldBoolExp,
Expr, IntExpr, BoolExpr,
PredOp(..),
Quantifier(..),
wrapExpr, wrapSimplifiedExpr,
varExpr, sumOfProductsExpr, conjExpr, disjExpr, testExpr, existsExpr,
expEqual,
expToFormula,
rename,
adjustBindings,
variablesWithinRange,
)
where
import Control.Monad
import Data.IORef
import Data.List
import Data.Maybe
import qualified Data.IntMap as IntMap
import Data.IntMap(IntMap)
import qualified Data.Set as Set
import Data.Set(Set)
import Data.Unique
import Debug.Trace
import System.IO.Unsafe
import Data.Presburger.Omega.LowLevel
infixl 7 |*|
infixl 7 *|
infixl 6 |+|, |-|
infix 4 |>|, |>=|, |<|, |<=|, |==|, |/=|
infixr 3 |&&|
newtype Exp t = Exp (IORef (ExprBox t))
type IntExp = Exp Int
type BoolExp = Exp Bool
instance Show (Exp Int) where
showsPrec n e =
showsIntExprPrec emptyShowsEnv n (getSimplifiedExpr e)
instance Show (Exp Bool) where
showsPrec n e =
showsBoolExprPrec emptyShowsEnv n (getSimplifiedExpr e)
data ExprBox t =
ExprBox
{ isSimplified :: !Bool
, expression :: !(Expr t)
}
getExpr :: Exp t -> Expr t
getExpr (Exp ref) = expression $ unsafePerformIO $ readIORef ref
getSimplifiedExpr :: Exp t -> Expr t
getSimplifiedExpr (Exp ref) =
unsafePerformIO $ readIORef ref >>= simplifyAndUpdate
where
simplifyAndUpdate (ExprBox True e) = return e
simplifyAndUpdate (ExprBox False e) =
let e' = simplify e
newBox = ExprBox True e'
in do writeIORef ref $! newBox
return e'
wrapExpr :: Expr t -> Exp t
wrapExpr e = Exp $ unsafePerformIO $ newIORef (ExprBox False e)
wrapSimplifiedExpr :: Expr t -> Exp t
wrapSimplifiedExpr e = Exp $ unsafePerformIO $ newIORef (ExprBox True e)
data Var = Bound !Int
| Quantified !Unique
deriving(Eq, Ord)
nthVariable :: Int -> Var
nthVariable = Bound
newQuantified :: IO Var
newQuantified = do u <- newUnique
return (Quantified u)
freeVariables :: [Var]
freeVariables = map Bound [0..]
takeFreeVariables :: Int -> [Var]
takeFreeVariables n = take n freeVariables
takeFreeVariables' :: Int -> [IntExp]
takeFreeVariables' n = map varE $ take n freeVariables
varE :: Var -> IntExp
varE v = wrapExpr $ VarE v
nthVarE :: Int -> IntExp
nthVarE n = varE (nthVariable n)
intE :: Int -> IntExp
intE n = wrapExpr $ LitE n
boolE :: Bool -> BoolExp
boolE b = wrapExpr $ LitE b
trueE, falseE :: BoolExp
trueE = boolE True
falseE = boolE False
negateE :: IntExp -> IntExp
negateE e = wrapExpr $ CAUE Prod (1) [getExpr e]
sumE :: [IntExp] -> IntExp
sumE es = wrapExpr $ CAUE Sum 0 $ map getExpr es
prodE :: [IntExp] -> IntExp
prodE es = wrapExpr $ CAUE Prod 1 $ map getExpr es
notE :: BoolExp -> BoolExp
notE e = wrapExpr $ NotE $ getExpr e
conjE :: [BoolExp] -> BoolExp
conjE es = wrapExpr $ CAUE Conj True $ map getExpr es
disjE :: [BoolExp] -> BoolExp
disjE es = wrapExpr $ CAUE Disj False $ map getExpr es
(|&&|) :: BoolExp -> BoolExp -> BoolExp
e |&&| f = wrapExpr $ CAUE Conj True [getExpr e, getExpr f]
(|+|) :: IntExp -> IntExp -> IntExp
e |+| f = sumE [e, f]
(|-|) :: IntExp -> IntExp -> IntExp
e |-| f = sumE [e, negateE f]
(|*|) :: IntExp -> IntExp -> IntExp
e |*| f = prodE [e, f]
(*|) :: Int -> IntExp -> IntExp
n *| f = wrapExpr $ CAUE Prod n [getExpr f]
isZeroE :: IntExp -> BoolExp
isZeroE e = wrapExpr $ PredE IsZero $ getExpr e
isNonnegativeE :: IntExp -> BoolExp
isNonnegativeE e = wrapExpr $ PredE IsGEZ $ getExpr e
(|==|) :: IntExp -> IntExp -> BoolExp
e |==| f = isZeroE (e |-| f)
(|/=|) :: IntExp -> IntExp -> BoolExp
e |/=| f = disjE [e |>| f, e |<| f]
(|>|) :: IntExp -> IntExp -> BoolExp
e |>| f = isNonnegativeE (wrapExpr $ CAUE Sum (1) [getExpr e, getExpr $ negateE f])
(|<|) :: IntExp -> IntExp -> BoolExp
e |<| f = f |>| e
(|>=|) :: IntExp -> IntExp -> BoolExp
e |>=| f = isNonnegativeE (e |-| f)
(|<=|) :: IntExp -> IntExp -> BoolExp
e |<=| f = f |>=| e
forallE :: (Var -> BoolExp) -> BoolExp
forallE f = wrapExpr $ QuantE Forall $ getExpr $ withFreshVariable f
existsE :: (Var -> BoolExp) -> BoolExp
existsE f = wrapExpr $ QuantE Exists $ getExpr $ withFreshVariable f
foldIntExp :: forall a.
(Int -> [a] -> a)
-> (Int -> [a] -> a)
-> (Int -> a)
-> [a]
-> (IntExp -> a)
foldIntExp sumE prodE litE env expression =
foldIntExp' sumE prodE litE env (getSimplifiedExpr expression)
foldIntExp' :: forall a.
(Int -> [a] -> a)
-> (Int -> [a] -> a)
-> (Int -> a)
-> [a]
-> (Expr Int -> a)
foldIntExp' sumE prodE litE env expression = rec env expression
where
rec :: forall. [a] -> Expr Int -> a
rec env expression =
case expression
of CAUE Sum lit es -> sumE lit $ map (rec env) es
CAUE Prod lit es -> prodE lit $ map (rec env) es
LitE n -> litE n
VarE (Bound i) -> env `genericIndex` i
VarE _ -> error "Expr.fold: unexpected variable"
index (x:_) 0 = x
index (_:xs) n = index xs (n1)
index [] _ = error "Expr.fold: variable index out of range"
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)
foldBoolExp sumE prodE litE orE andE notE quantE predE trueE falseE
env expression = rec env (getSimplifiedExpr expression)
where
rec :: forall. [b] -> Expr Bool -> a
rec env expression =
case expression
of CAUE Disj True es -> trueE
CAUE Disj False es -> orE $ map (rec env) es
CAUE Conj True es -> andE $ map (rec env) es
CAUE Conj False es -> falseE
PredE pred e -> predE pred (integral env e)
NotE e -> notE (rec env e)
LitE True -> trueE
LitE False -> falseE
QuantE q e -> quantE q (quantifier env e)
quantifier env e value = rec (value:env) e
integral env e = foldIntExp' sumE prodE litE env e
withFreshVariable :: (Var -> Exp t) -> Exp t
withFreshVariable f = unsafePerformIO $ do
v <- newQuantified
return $ rename v (Bound 0) $ adjustBindings 0 1 $ f v
data Expr t where
CAUE :: !(CAUOp t)
-> !t
-> [Expr t]
-> Expr t
PredE :: !PredOp
-> Expr Int
-> Expr Bool
NotE :: Expr Bool -> Expr Bool
LitE :: !t -> Expr t
VarE :: !Var -> Expr Int
QuantE :: !Quantifier -> Expr Bool -> Expr Bool
type IntExpr = Expr Int
type BoolExpr = Expr Bool
data CAUOp t where
Sum :: CAUOp Int
Prod :: CAUOp Int
Conj :: CAUOp Bool
Disj :: CAUOp Bool
instance Eq (CAUOp t) where
Sum == Sum = True
Prod == Prod = True
Conj == Conj = True
Disj == Disj = True
_ == _ = False
instance Show (CAUOp t) where
show Sum = "Sum"
show Prod = "Prod"
show Conj = "Conj"
show Disj = "Disj"
data PredOp = IsZero | IsGEZ
deriving(Eq, Show)
data Quantifier = Forall | Exists
deriving(Eq, Show)
varExpr :: Var -> IntExpr
varExpr = VarE
sumOfProductsE :: Int
-> [(Int, [Var])]
-> IntExp
sumOfProductsE n prods = wrapSimplifiedExpr $ CAUE Sum n $ map prod prods
where
prod (n, vars) = CAUE Prod n $ map VarE vars
sumOfProductsExpr :: Int
-> [(Int, [Var])]
-> IntExpr
sumOfProductsExpr n prods = CAUE Sum n $ map prod prods
where
prod (n, vars) = CAUE Prod n $ map VarE vars
testExpr :: PredOp -> IntExpr -> BoolExpr
testExpr p e = PredE p e
conjExpr :: [BoolExpr] -> BoolExpr
conjExpr = CAUE Conj True
disjExpr :: [BoolExpr] -> BoolExpr
disjExpr = CAUE Disj False
existsExpr :: BoolExpr -> BoolExpr
existsExpr e = QuantE Exists e
isLitE :: Expr t -> Bool
isLitE (LitE _) = True
isLitE _ = False
data Term = Term !Int [IntExpr]
deconstructProduct :: IntExpr -> Term
deconstructProduct (CAUE Prod n xs) = Term n xs
deconstructProduct e = Term (unit Prod) [e]
rebuildProduct :: Term -> IntExpr
rebuildProduct (Term 1 [e]) = e
rebuildProduct (Term n es) = CAUE Prod n es
deconstructSum :: IntExpr -> Term
deconstructSum (CAUE Sum n xs) = Term n xs
deconstructSum e = Term (unit Sum) [e]
rebuildSum :: Term -> IntExpr
rebuildSum (Term 1 [e]) = e
rebuildSum (Term n es) = CAUE Sum n es
cauEq :: CAUOp t -> t -> t -> Bool
cauEq Sum = (==)
cauEq Prod = (==)
cauEq Conj = (==)
cauEq Disj = (==)
zero :: CAUOp t -> Maybe t
zero Sum = Nothing
zero Prod = Just 0
zero Conj = Just False
zero Disj = Just True
unit :: CAUOp t -> t
unit Sum = 0
unit Prod = 1
unit Conj = True
unit Disj = False
isZeroOf :: t -> CAUOp t -> Bool
l `isZeroOf` op = case zero op
of Nothing -> False
Just z -> cauEq op l z
isUnitOf :: t -> CAUOp t -> Bool
l `isUnitOf` op = cauEq op (unit op) l
evalCAUOp :: CAUOp t -> [t] -> t
evalCAUOp Sum = sum
evalCAUOp Prod = product
evalCAUOp Conj = and
evalCAUOp Disj = or
evalPred :: PredOp -> Int -> Bool
evalPred IsZero = (0 ==)
evalPred IsGEZ = (0 <=)
appPrec = 10
mulPrec = 7
addPrec = 6
cmpPrec = 4
andPrec = 3
lamPrec = 0
data ShowsEnv =
ShowsEnv
{
showNthVar :: ![Int -> ShowS]
, numBound :: !Int
, varNames :: [ShowS]
}
emptyShowsEnv =
ShowsEnv
{ showNthVar = []
, numBound = 0
, varNames = map showChar $
['x', 'y', 'z'] ++
['a' .. 'w'] ++
[error "out of variable names"]
}
bindVariable :: ShowsEnv -> (ShowS, ShowsEnv)
bindVariable env =
case varNames env
of nm : nms ->
let env' = ShowsEnv
{ showNthVar = showVar nm : showNthVar env
, numBound = 1 + numBound env
, varNames = nms
}
in (nm, env')
where
showVar nm n = showParen (n >= appPrec) $ showString "varE " . nm
bindVariables :: Int -> ShowsEnv -> ([ShowS], ShowsEnv)
bindVariables 0 env = ([], env)
bindVariables n env = let (v, env') = bindVariable env
(vs, env'') = bindVariables (n1) env
in (v:vs, env'')
showsVarPrec :: ShowsEnv -> Int -> Var -> ShowS
showsVarPrec env prec (Bound i) =
if i < numBound env
then (showNthVar env !! i) prec
else shift (numBound env)
where
shift n = showParen (prec >= appPrec) $
showString "nthVarE " . shows (in)
showsVarPrec _ _ (Quantified u) = showString "(Quantified _)"
showsInt :: Int -> ShowS
showsInt n | n >= 0 = showString "intE " . shows n
| otherwise = showString "intE " . showParen True (shows n)
showsIntExprPrec :: ShowsEnv -> Int -> IntExpr -> ShowS
showsIntExprPrec env n expression =
case expression
of CAUE Sum lit es -> showParen (n >= addPrec) $ showSum env lit es
CAUE Prod lit es -> showParen (n >= mulPrec) $ showProd env lit es
LitE l -> showParen (n >= appPrec) $
showsInt l
VarE v -> showsVarPrec env n v
showsBoolExprPrec :: ShowsEnv -> Int -> BoolExpr -> ShowS
showsBoolExprPrec env n expression =
case expression
of CAUE Conj lit es
| lit -> let texts = map (showsBoolExprPrec env 0) es
in showParen (n >= fromIntegral andPrec) $
texts `showSepBy` showString " |&&| "
| otherwise -> showString "falseE"
CAUE Disj lit es
| lit -> showString "trueE"
| otherwise -> let texts = map (showsBoolExprPrec env 0) es
in showParen (n >= appPrec) $
showString "disjE " . showsList texts
PredE IsGEZ e -> showGEZ env n e
PredE IsZero e -> showEQZ env n e
NotE e -> showString "notE " . showsBoolExprPrec env appPrec e
LitE True -> showString "trueE"
LitE False -> showString "falseE"
QuantE q e -> showParen (n >= appPrec) $
showQuantifier showsBoolExprPrec env q e
showGEZ :: ShowsEnv -> Int -> IntExpr -> ShowS
showGEZ env prec e =
showParen (prec >= cmpPrec) $
case e
of LitE n -> showGEZ' env n []
CAUE Sum lit es -> showGEZ' env lit es
_ -> showGEZ' env 0 [e]
showGEZ' env lit es =
case partitionSumBySign lit es
of (1, neg, pos) -> balanceInequality False 0 neg pos
(n, neg, pos) -> balanceInequality True n neg pos
where
balanceInequality True n neg [] =
showInequality le (negate n) [] neg
balanceInequality False n neg [] =
showInequality lt (negate n) [] neg
balanceInequality True n neg pos =
showInequality ge n neg pos
balanceInequality False n neg pos =
showInequality gt n neg pos
showInequality symbol lit neg pos =
let (pos', neg') =
if lit >= 0
then (CAUE Sum lit pos, CAUE Sum 0 neg)
else (CAUE Sum 0 pos, CAUE Sum (negate lit) neg)
in showsIntExprPrec env cmpPrec pos' .
symbol .
showsIntExprPrec env cmpPrec neg'
ge = showString " |>=| "
gt = showString " |>| "
le = showString " |<=| "
lt = showString " |<| "
showEQZ :: ShowsEnv -> Int -> IntExpr -> ShowS
showEQZ env prec (CAUE Sum lit [e]) =
showParen (prec >= cmpPrec) $
(showsIntExprPrec env cmpPrec e .
showString " |==| " .
showsIntExprPrec env cmpPrec (LitE lit)
)
showEQZ env prec e =
showParen (prec >= appPrec) $
showString "isZeroE " . showsIntExprPrec env appPrec e
partitionSumBySign n es =
case partition hasNegativeMultiplier es
of (neg, pos) -> let neg' = map negateMultiplier neg
in (n, neg', pos)
where
hasNegativeMultiplier :: IntExpr -> Bool
hasNegativeMultiplier (CAUE Prod n es) = n < 0
hasNegativeMultiplier (LitE n) = n < 0
hasNegativeMultiplier _ = False
negateMultiplier :: IntExpr -> IntExpr
negateMultiplier (CAUE Prod n es) = CAUE Prod (negate n) es
negateMultiplier (LitE n) = LitE (negate n)
negateMultiplier _ = error "partitionSumBySign: unexpected term"
showSum env lit es =
if lit == 0
then case es
of e : es' -> showsIntExprPrec env addPrec e . showSumTail es'
[] -> showsInt 0
else showsInt lit . showSumTail es
where
showSumTail es = foldr (.) id $ map showSumTailElement es
showSumTailElement e =
case deconstructProduct e
of Term 1 es -> add . showProd env 1 es
Term (1) es -> sub . showProd env 1 es
Term n es | n >= 0 -> add . showProd env n es
| otherwise -> sub . showProd env (negate n) es
add = showString " |+| "
sub = showString " |-| "
showProd env lit es =
let text = map (showsIntExprPrec env mulPrec) es
textLit = if lit == 1
then id
else showsPrec mulPrec lit . showString " *| "
in textLit . (text `showSepBy` showString " |*| ")
showsList :: [ShowS] -> ShowS
showsList ss =
showChar '[' . (ss `showSepBy` showString ", ") . showChar ']'
showSepBy :: [ShowS] -> ShowS -> ShowS
xs `showSepBy` sep = foldr (.) id (intersperse sep xs)
showQuantifier :: (ShowsEnv -> Int -> Expr t -> ShowS)
-> ShowsEnv -> Quantifier -> Expr t -> ShowS
showQuantifier showExpr env q e =
let quantifier = case q
of Forall -> showString "forallE $ \\"
Exists -> showString "existsE $ \\"
(varName, env') = bindVariable env
in quantifier . varName . showString " -> " . showExpr env' lamPrec e
showLambdaBound :: (ShowsEnv -> Int -> ShowS)
-> ShowsEnv -> Int -> ShowS
showLambdaBound showBody env prec =
let
(varName, env') = bindVariable env
in showParen (prec >= appPrec) $
showChar '\\' . varName . showString " -> " .
showBody env' lamPrec
showLambdaList :: Int
-> (ShowsEnv -> Int -> ShowS)
-> ShowsEnv -> Int -> ShowS
showLambdaList n_params showBody env prec =
let
(varNames, env') = bindVariables n_params env
in showParen (prec >= appPrec) $
showChar '\\' . showsList varNames . showString " -> " .
showBody env' lamPrec
expEqual :: Eq t => Expr t -> Expr t -> Bool
expEqual expr1 expr2 =
case (expr1, expr2)
of (CAUE op1 l1 es1, CAUE op2 l2 es2) ->
op1 == op2 && l1 == l2 && expListsEqual es1 es2
(PredE op1 e1, PredE op2 e2) ->
op1 == op2 && expEqual e1 e2
(NotE e1, NotE e2) -> expEqual e1 e2
(LitE l1, LitE l2) -> l1 == l2
(VarE v1, VarE v2) -> v1 == v2
(QuantE q1 e1, QuantE q2 e2) ->
q1 == q2 && expEqual e1 e2
(_, _) -> False
expListsEqual :: Eq t => [Expr t] -> [Expr t] -> Bool
expListsEqual (e:es1) es2 =
case findEqualExpr e es2
of Just (_, es2') -> expListsEqual es1 es2'
Nothing -> False
expListsEqual [] [] = True
expListsEqual [] _ = False
findEqualExpr :: Eq t => Expr t -> [Expr t] -> Maybe (Expr t, [Expr t])
findEqualExpr searchE es = go es id
where
go (e:es) h | expEqual searchE e = Just (e, h es)
| otherwise = go es (h . (e:))
go [] _ = Nothing
simplify :: Expr t -> Expr t
simplify e =
complexSimplifications $ basicSimplifications $ simplifyRec e
simplifyRec :: Expr t -> Expr t
simplifyRec expr =
case expr
of CAUE op lit es -> CAUE op lit $ map simplify es
PredE op e1 -> PredE op $ simplify e1
NotE e -> NotE $ simplify e
LitE _ -> expr
VarE v -> expr
QuantE q e -> QuantE q $ simplify e
basicSimplifications :: Expr t -> Expr t
basicSimplifications = zus . peval . flatten
complexSimplifications :: Expr t -> Expr t
complexSimplifications e =
case e
of CAUE Sum _ _ -> basicSimplifications $ collect e
CAUE Prod _ _ -> posToSop e
_ -> e
posToSop :: Expr Int -> Expr Int
posToSop expr@(CAUE Prod n es)
| all isSingletonTerm terms =
expr
| otherwise =
let
terms' = [LitE n] : map mkTermList terms
expr' = CAUE Sum 0 [CAUE Prod 1 t | t <- sequence terms']
in simplify expr'
where
terms = map deconstructSum es
mkTermList (Term n es) = LitE n : es
isSingletonTerm (Term 0 [_]) = True
isSingletonTerm (Term _ []) = True
isSingletonTerm (Term _ _ ) = False
posToSop expr = expr
flatten :: forall t. Expr t -> Expr t
flatten (CAUE op lit es) =
case flat lit id es of (lit', es') -> CAUE op lit' es'
where
flat lit hd (e:es) =
case e
of CAUE op2 lit2 es2
| op == op2 -> let lit' = evalCAUOp op [lit, lit2]
in flat lit' hd (es2 ++ es)
_ -> flat lit (hd . (e:)) es
flat lit hd [] = (lit, hd [])
flatten e = e
peval :: Expr t -> Expr t
peval exp@(CAUE op l es) =
case partition isLitE es
of ([], _) -> exp
(lits, notLits) -> let literals = l : map fromLitE lits
in CAUE op (evalCAUOp op literals) notLits
where
fromLitE (LitE l) = l
fromLitE _ = error "peval: unexpected expression"
peval exp@(PredE op e) =
case e
of LitE l -> LitE $ evalPred op l
_ -> exp
peval exp@(NotE e) =
case e
of LitE l -> LitE $ not l
_ -> exp
peval e = e
zus :: Expr t -> Expr t
zus exp@(CAUE op l es) =
case es
of [] -> LitE l
_ | l `isZeroOf` op -> LitE l
[e] | l `isUnitOf` op -> e
_ -> exp
zus e = e
collect :: Expr Int -> Expr Int
collect (CAUE Sum literal es) =
let es' = map simplify $
map rebuildProduct $
collectTerms $
map deconstructProduct es
in CAUE Sum literal es'
where
collectTerms :: [Term] -> [Term]
collectTerms (t:ts) =
case collectTerm t ts of (t', ts') -> t':collectTerms ts'
collectTerms [] = []
collectTerm :: Term -> [Term] -> (Term, [Term])
collectTerm (Term factor t) terms =
let (equalTerms, terms') = partition (sameTerms t) terms
factor' = factor + sum [n | Term n _ <- equalTerms]
in (Term factor' t, terms')
sameTerms t (Term _ t') = expListsEqual t t'
collect e = e
lookupVar :: Int -> [VarHandle] -> VarHandle
lookupVar n (v : vars) | n > 0 = lookupVar (n 1) vars
| n == 0 = v
| otherwise = error "lookupVar: negative index"
lookupVar _ [] = error "lookupVar: variable index out of range"
expToFormula :: [VarHandle]
-> BoolExp
-> Formula
expToFormula freeVars e = exprToFormula freeVars (getSimplifiedExpr e)
exprToFormula :: [VarHandle]
-> BoolExpr
-> Formula
exprToFormula freeVars expr =
case expr
of CAUE op lit es
| lit `isUnitOf` op ->
case op
of Conj -> conjunction $ map (exprToFormula freeVars) es
Disj -> disjunction $ map (exprToFormula freeVars) es
_ -> expToFormulaError "unhandled operator"
| otherwise ->
if lit then true else false
PredE op e ->
case sumToConstraint freeVars e
of (terms, constant) ->
case op
of IsZero -> equality terms constant
IsGEZ -> inequality terms constant
NotE e -> negation $ exprToFormula freeVars e
LitE True -> true
LitE False -> false
QuantE q e -> let body v = exprToFormula (v:freeVars) e
in case q
of Forall -> qForall body
Exists -> qExists body
sumToConstraint :: [VarHandle]
-> IntExpr
-> ([Coefficient], Int)
sumToConstraint freeVars expr =
case deconstructSum expr
of Term constant terms -> (map deconstructTerm terms, constant)
where
deconstructTerm :: IntExpr -> Coefficient
deconstructTerm expr =
case deconstructProduct expr
of Term n [VarE (Bound i)] -> Coefficient (lookupVar i freeVars) n
_ -> expToFormulaError "expression is non-affine"
expToFormulaError :: String -> a
expToFormulaError s = error $ "expToFormula: " ++ s
rename :: Var
-> Var
-> Exp t
-> Exp t
rename v1 v2 e = wrapExpr $ renameExpr v1 v2 $ getExpr e
renameExpr :: Var
-> Var
-> Expr t
-> Expr t
renameExpr !v1 v2 expr = rn expr
where
rn :: forall t. Expr t -> Expr t
rn (CAUE op lit es) = CAUE op lit $ map rn es
rn (PredE op e) = PredE op $ rn e
rn (NotE e) = NotE $ rn e
rn expr@(LitE _) = expr
rn expr@(VarE v) | v == v1 = VarE v2
| otherwise = expr
rn (QuantE q e) = QuantE q $ renameExpr (bump v1) (bump v2) e
bump (Bound n) = Bound (n+1)
bump v@(Quantified _) = v
adjustBindings :: Int
-> Int
-> Exp t
-> Exp t
adjustBindings firstBound shift e =
wrapExpr $ adjustBindingsExpr firstBound shift $ getExpr e
adjustBindingsExpr :: Int
-> Int
-> Expr t
-> Expr t
adjustBindingsExpr !firstBound !shift e = adj e
where
adj :: Expr t -> Expr t
adj (CAUE op lit es) = CAUE op lit (map adj es)
adj (PredE op e) = PredE op (adj e)
adj (NotE e) = NotE (adj e)
adj expr@(LitE _) = expr
adj expr@(VarE v) = case v
of Bound n
| n >= firstBound ->
VarE $ Bound (n + shift)
| otherwise ->
expr
Quantified _ -> expr
adj (QuantE q e) = QuantE q $
adjustBindingsExpr (firstBound + 1) shift e
variablesWithinRange :: Int -> Exp t -> Bool
variablesWithinRange n e = check n $ getExpr e
where
check :: Int -> Expr t -> Bool
check n e = check' e
where
check' :: Expr t -> Bool
check' (CAUE _ _ es) = all check' es
check' (PredE _ e) = check' e
check' (NotE e) = check' e
check' (LitE _) = True
check' (VarE (Bound i)) = i < n
check' (VarE (Quantified _)) = quantifiedVar
check' (QuantE _ e) = check (n+1) e
quantifiedVar :: Bool
quantifiedVar = error "variablesWithinRange: unexpected variable"