| definition: |
funcs2SMT :: Options -> IORef VState -> [QName]
-> IO (Command, [TAFuncDecl], [(QName,Bool)])
funcs2SMT opts vstref qns = do
funs <- getAllFunctions vstref (nub qns)
unless (null funs) $ printWhenAll opts $ unlines $
"Operations to be axiomatized in SMT:" :
map (showCurryFuncDecl snd snd . unAnnFuncDecl) funs
let ndinfo = nondetOfFuncDecls funs
choicePlan = (TCons (pre "Choice") [],
pre "choose", pre "lchoice", pre "rchoice")
tfuns = map (addChoiceFuncDecl ndinfo choicePlan) funs
unless (null ndinfo) $ printWhenAll opts $
"Non-determinism status of these operations:\n" ++
unlines ((map showND) ndinfo)
unless (null tfuns) $ printWhenAll opts $ unlines $
"Transformed operations to be axiomatized in SMT:" :
map (showCurryFuncDecl snd snd . unAnnFuncDecl) tfuns
return (DefineSigsRec (map fun2SMT tfuns), tfuns, ndinfo)
where
showND ((_,n),nd) = n ++ ": " ++ if nd then "NONDET" else "DET"
|
| demand: |
no demanded arguments |
| deterministic: |
deterministic operation |
| documentation: |
Translates a list of operations specified by their qualified name (together with all operations on which these operation depend on) into an SMT string that axiomatizes their semantics. Non-deterministic operations are axiomatized by the "planned choice" translation (see module `FlatCurry.Typed.NonDet2Det`). In order to call them correctly, a list of qualified operation names together with their non-determinism status (`True` means non-deterministic) is also returned. |
| failfree: |
<FAILING> |
| indeterministic: |
referentially transparent operation |
| infix: |
no fixity defined |
| iotype: |
{(_,_,_) |-> _}
|
| name: |
funcs2SMT |
| precedence: |
no precedence defined |
| result-values: |
_ |
| signature: |
ToolOptions.Options -> Data.IORef.IORef VerifierState.VState -> [(String, String)] -> Prelude.IO (ESMT.Command, [FlatCurry.Annotated.Types.AFuncDecl FlatCurry.Types.TypeExpr], [((String, String), Prelude.Bool)]) |
| solution-complete: |
operation might suspend on free variables |
| terminating: |
possibly non-terminating |
| totally-defined: |
possibly non-reducible on same data term |