CurryInfo: verify-non-fail-2.0.0 / Verify.WithSMT.exp2SMTWithVars

definition: Info
 
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: Info
 no demanded arguments
deterministic: Info
 deterministic operation
documentation: Info
 
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: Info
 <FAILING>
indeterministic: Info
 referentially transparent operation
infix: Info
 no fixity defined
iotype: Info
 {(_,_,_) |-> _}
name: Info
 exp2SMTWithVars
precedence: Info
 no precedence defined
result-values: Info
 _
signature: Info
 Prelude.Int -> Prelude.Maybe Verify.ESMT.Term -> FlatCurry.Types.Expr
-> Prelude.Maybe (Verify.ESMT.Term, [(Prelude.Int, Verify.ESMT.Sort)])
solution-complete: Info
 operation might suspend on free variables
terminating: Info
 possibly non-terminating
totally-defined: Info
 possibly non-reducible on same data term