|
definition:
|
exp2SMTWithVars :: Int -> Maybe Term -> Expr -> Maybe (Term, [(Int,Sort)])
exp2SMTWithVars maxusedvar lhs exp =
maybe Nothing
(\t -> Just $ elimFailed maxusedvar t)
(exp2SMT lhs (replaceHigherOrderInExp exp))
|
|
demand:
|
no demanded arguments
|
|
deterministic:
|
deterministic operation
|
|
documentation:
|
-- Translates a (Boolean) FlatCurry expression into an SMT expression.
-- If the second argument is an SMT expression, an equation between
-- this expression and the translated result expression is generated.
-- This is useful to axiomatize non-deterministic operations.
-- If successful, the translated SMT expression together with new variables
-- (which are replacements for higher-order applications) are returned.
-- The first argument is the maximum index of already used variables.
|
|
indeterministic:
|
referentially transparent operation
|
|
infix:
|
no fixity defined
|
|
iotype:
|
{(_,_,_) |-> _}
|
|
name:
|
exp2SMTWithVars
|
|
precedence:
|
no precedence defined
|
|
result-values:
|
_
|
|
signature:
|
Prelude.Int -> Prelude.Maybe Verify.ESMT.Term -> FlatCurry.Types.Expr
-> Prelude.Maybe (Verify.ESMT.Term, [(Prelude.Int, Verify.ESMT.Sort)])
|
|
solution-complete:
|
operation might suspend on free variables
|
|
terminating:
|
possibly non-terminating
|
|
totally-defined:
|
possibly non-reducible on same data term
|