úÎ, )     (c) Levent ErkokBSD3erkokl@gmail.com experimentalSafe+The actual annotation.›Plugin options. Note that we allow picking multiple solvers, which will all be run in parallel. If you want to run all available solvers, use the option m. The default is to error-out on failure, using the default-SMT solver picked by SBV, which is currently Z3.Continue even if proof failsVSkip the proof. Can be handy for properties that we currently do not want to focus on.*Produce verbose output, good for debuggingCheck for safetyPerform quickCheck +Uninterpret this binding for proof purposes 9Use these names for the arguments; need not be exhaustive Use Z3  Use Yices  Use BoolectorUse CVC4 Use MathSATUse ABCUse all installed solvers-A property annotation, using default options.)Synonym for sbv really, just looks cooler   (c) Levent ErkokBSD3erkokl@gmail.com experimentalNone+The values kept track of by the interpreter'Configuration info as we run the pluginThe interpreter monadInterpreter environment8Given the user options, determine which solver(s) to useMCompute the span given a Tick. Returns the old-span if the tick span useless.Compute the span for a binding.&Show a GHC span in user-friendly form. !"#$%&'()*+,-./0123 !"#$%&'()*+,-./0123  !"#$%&'( )*+,-./0123(c) Levent ErkokBSD3erkokl@gmail.com experimentalNone4#Dispatch the analyzer over bindings5Prove an SBVTheorem6gSafely execute an action, catching the exceptions, printing and returning False if something goes wrong7Returns True if proof went thru8Uninterpret an expression9%Is this variable really a dictionary?:gConvert a Core type to an SBV kind, if known Otherwise, create an uninterpreted kind, and return that. 45678;9:<=4 45678;9:<=(c) Levent ErkokBSD3erkokl@gmail.com experimentalNone<>.Build the initial environment containing types?2Build the initial environment containing functions@(Special functions that have a fixed-typeA?Symbolic functions supported by the plugin; those from a class.B3Lift a unary SBV function to the plugin value spaceCPLift a unary SBV function that takes and integer value to the plugin value spaceD>Lift a two argument SBV function to our the plugin value space>?@ABCD>?@>?@ABCD(c) Levent ErkokBSD3erkokl@gmail.com experimentalNoneEntry point to the plugin(c) Levent ErkokBSD3erkokl@gmail.com experimentalNone  E      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJsbvPl_3kKoCv9PEdy2B3DM6VoeIpData.SBV.PluginData.SBV.Plugin.DataData.SBV.Plugin.CommonData.SBV.Plugin.AnalyzeData.SBV.Plugin.EnvData.SBV.Plugin.Plugin SBVAnnotationSBVoptions SBVOption IgnoreFailureSkipVerboseSafety QuickCheck UninterpretNamesZ3Yices BoolectorCVC4MathSATABC AnySolversbvtheorempluginValConfigEvalEnv pickSolverstickSpanbindSpanshowSpanBaseFuncdflagswordSizeisGHCioptsknownTCs knownFuns knownSpecials sbvAnnotationallBindscurLocflags machWordSizerUninterpreted rUsedNamesrUITypesbaseTCsenvMapspecMapcoreMap analyzeBindprovesafelyproveIt uninterpretisReallyADictionary getBaseType mkValidName$fOutputableVal$fOutputableKind buildTCEnv buildFunEnvbuildSpecialEnvsymFuncslift1lift1Intlift2