CurryInfo: contract-prover-4.0.0 / ContractProver.checkImplicationWithSMT

 
checkImplicationWithSMT :: Options -> IORef VState -> String -> [(Int,TypeExpr)]
                        -> Term -> Term -> Term -> IO (Maybe String)
checkImplicationWithSMT opts vstref scripttitle vartypes
                        assertion impbindings imp = do
  let allsyms = catMaybes
                  (map (\n -> maybe Nothing Just (untransOpName n))
                       (map qidName
                         (allQIdsOfTerm (tConj [assertion, impbindings, imp]))))
  unless (null allsyms) $ printWhenIntermediate opts $
    "Translating operations into SMT: " ++ unwords (map showQName allsyms)
  (smtfuncs,fdecls,ndinfo) <- funcs2SMT opts vstref allsyms
  smttypes <- genSMTTypes vstref vartypes fdecls [assertion,impbindings,imp]
  let freshvar = maximum (map fst vartypes) + 1
      ([assertionC,impbindingsC,impC],newix) =
         nondetTransL ndinfo freshvar [assertion,impbindings,imp]
      smt = smttypes ++
            [ EmptyLine, smtfuncs, EmptyLine
            , Comment "Free variables:" ] ++
            map typedVar2SMT
                (vartypes ++ map toChoiceVar [freshvar .. newix-1]) ++
            [ EmptyLine
            , Comment "Boolean formula of assertion (known properties):"
            , sAssert assertionC, EmptyLine
            , Comment "Bindings of implication:"
            , sAssert impbindingsC, EmptyLine
            , Comment "Assert negated implication:"
            , sAssert (tNot impC), EmptyLine
            , Comment "check satisfiability:"
            , CheckSat
            , Comment "if unsat, we can omit this part of the contract check"
            ]
  smtstdtypes <- readInclude "Prelude.smt"
  smtchoice   <- if or (map snd ndinfo)
                   then readInclude "Prelude_Choice.smt"
                   else return ""
  let smtprelude = smtstdtypes ++ smtchoice
  callSMT opts $ "; " ++ scripttitle ++ "\n\n" ++ smtprelude ++ showSMT smt
 where
  readInclude f = getIncludePath f >>= readFile
  toChoiceVar i = (i, TCons (pre "Choice") [])

 no demanded arguments

 deterministic operation

 
Calls the SMT solver to check whether an assertion implies some
(pre/post) condition.
Returns `Nothing` if the proof was not successful, otherwise
the SMT script containing the proof (to obtain `unsat`) is returned.

 <FAILING>

 referentially transparent operation

 no fixity defined

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

 checkImplicationWithSMT

 no precedence defined

 _

 ToolOptions.Options -> Data.IORef.IORef VerifierState.VState -> String
-> [(Prelude.Int, FlatCurry.Types.TypeExpr)] -> ESMT.Term -> ESMT.Term
-> ESMT.Term -> Prelude.IO (Prelude.Maybe String)

 operation might suspend on free variables

 possibly non-terminating

 possibly non-reducible on same data term