|
definition:
|
pred2SMT :: TAExpr -> TransStateM Term
pred2SMT exp = case simpExpr exp of
AVar _ i -> return (TSVar i)
ALit _ l -> return (lit2SMT l)
AComb _ ct (qf,ftype) args -> comb2bool qf ftype ct (length args) args
_ -> return (tComb (show exp) []) -- TODO!
where
comb2bool qf ftype ct ar args
| qf == pre "[]" && ar == 0
= return (sortedConst "nil" (polytype2sort (annExpr exp)))
| qf == pre "not" && ar == 1
= do barg <- pred2SMT (head args)
return (tNot barg)
| qf == pre "null" && ar == 1
= do let arg = head args
barg <- pred2SMT arg
vartype <- typeOfVar arg
return (tEqu barg (sortedConst "nil" (polytype2sort vartype)))
| qf == pre "apply"
= do -- cannot translate h.o. apply: replace it by new variable
fvar <- getFreshVar
addVarTypes [(fvar,annExpr exp)]
return (TSVar fvar)
| qf == pre "/="
= do be <- comb2bool (pre "==") ftype ct ar args
return (tNot be)
| otherwise
= do bargs <- mapM pred2SMT args
return (TComb (cons2SMT (ct /= ConsCall || not (null bargs))
False qf ftype)
bargs)
typeOfVar e = do
vartypes <- getVarTypes
case e of
AVar _ i -> maybe
(error $ "pred2SMT: variable " ++ show i ++ " not found")
return
(lookup i vartypes)
_ -> return $ annExpr e -- might not be correct due to applyFunc!
|
|
demand:
|
argument 1
|
|
deterministic:
|
deterministic operation
|
|
documentation:
|
-- Translates a Boolean FlatCurry expression into a Boolean formula.
-- Calls to user-defined functions are replaced by the first argument
-- (which might be true or false).
|
|
indeterministic:
|
referentially transparent operation
|
|
infix:
|
no fixity defined
|
|
name:
|
pred2SMT
|
|
precedence:
|
no precedence defined
|
|
result-values:
|
_
|
|
signature:
|
FlatCurry.Annotated.Types.AExpr FlatCurry.Types.TypeExpr
-> Control.Monad.Trans.State.StateT TransState Prelude.IO ESMT.Term
|
|
solution-complete:
|
operation might suspend on free variables
|
|
terminating:
|
possibly non-terminating
|
|
totally-defined:
|
possibly non-reducible on same data term
|