CurryInfo: contract-prover-4.0.0 / Curry2SMT.funcs2SMT

 
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"

 no demanded arguments

 deterministic operation

 
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.

 <FAILING>

 referentially transparent operation

 no fixity defined

 {(_,_,_) |-> _}

 funcs2SMT

 no precedence defined

 _

 ToolOptions.Options -> Data.IORef.IORef VerifierState.VState
-> [(String, String)]
-> Prelude.IO (ESMT.Command, [FlatCurry.Annotated.Types.AFuncDecl FlatCurry.Types.TypeExpr], [((String, String), Prelude.Bool)])

 operation might suspend on free variables

 possibly non-terminating

 possibly non-reducible on same data term