|
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.
|
|
failfree:
|
<FAILING>
|
|
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
|