sbv-0.9.5: Symbolic Bit Vectors: Prove bit-precise program properties using SMT solvers.

Index

 # Data.SBV &&& Data.SBV .&. Data.SBV ./= Data.SBV .< Data.SBV .<= Data.SBV .== Data.SBV .> Data.SBV .>= Data.SBV .|. Data.SBV <*> Data.SBV.Examples.Polynomials.Polynomials <+> Data.SBV <=> Data.SBV === Data.SBV ==> Data.SBV A Data.SBV.Examples.Uninterpreted.AUF Actions Data.SBV.Examples.Puzzles.U2Bridge Adam Data.SBV.Examples.Puzzles.U2Bridge adam Data.SBV.Examples.Puzzles.U2Bridge adc Data.SBV.Examples.BitPrecise.Legato Address Data.SBV.Examples.BitPrecise.Legato allDifferent Data.SBV allEqual Data.SBV allPuzzles Data.SBV.Examples.Puzzles.Sudoku allSat Data.SBV AllSatResult 1 (Type/Class) Data.SBV 2 (Data Constructor) Data.SBV allSatWith Data.SBV assert Data.SBV.Internals Assertion Data.SBV.Internals bAll Data.SBV bAnd Data.SBV bAny Data.SBV bcc Data.SBV.Examples.BitPrecise.Legato bin Data.SBV binS Data.SBV Bit Data.SBV.Examples.BitPrecise.Legato bit Data.SBV Bits Data.SBV bitSize Data.SBV bitValue Data.SBV blastBE Data.SBV blastLE Data.SBV bne Data.SBV.Examples.BitPrecise.Legato bnot Data.SBV Board 1 (Type/Class) Data.SBV.Examples.Puzzles.MagicSquare 2 (Type/Class) Data.SBV.Examples.Puzzles.Sudoku Bono Data.SBV.Examples.Puzzles.U2Bridge bono Data.SBV.Examples.Puzzles.U2Bridge Boolean Data.SBV bOr Data.SBV bumpTime1 Data.SBV.Examples.Puzzles.U2Bridge bumpTime2 Data.SBV.Examples.Puzzles.U2Bridge BVDivisible Data.SBV bvQuotRem Data.SBV check 1 (Function) Data.SBV.Examples.Puzzles.MagicSquare 2 (Function) Data.SBV.Examples.Puzzles.Sudoku chunk Data.SBV.Examples.Puzzles.MagicSquare clc Data.SBV.Examples.BitPrecise.Legato clearBit Data.SBV complement Data.SBV complementBit Data.SBV conditionalSetClearCorrect Data.SBV.Examples.BitPrecise.BitTricks correctnessTheorem Data.SBV.Examples.BitPrecise.Legato Count Data.SBV.Examples.Puzzles.DogCatMouse crossTime Data.SBV.Examples.Puzzles.U2Bridge cvtModel Data.SBV defaultSMTCfg Data.SBV dex Data.SBV.Examples.BitPrecise.Legato diag Data.SBV.Examples.Puzzles.MagicSquare displayModels Data.SBV dispSolution Data.SBV.Examples.Puzzles.Sudoku Edge Data.SBV.Examples.Puzzles.U2Bridge edge Data.SBV.Examples.Puzzles.U2Bridge Elem Data.SBV.Examples.Puzzles.MagicSquare end Data.SBV.Examples.BitPrecise.Legato engine Data.SBV EqSymbolic Data.SBV Equality Data.SBV executable Data.SBV extend Data.SBV Extract Data.SBV.Examples.BitPrecise.Legato f Data.SBV.Examples.Uninterpreted.AUF false Data.SBV fastMaxCorrect Data.SBV.Examples.BitPrecise.BitTricks fastMinCorrect Data.SBV.Examples.BitPrecise.BitTricks Flag Data.SBV.Examples.BitPrecise.Legato FlagC Data.SBV.Examples.BitPrecise.Legato Flags Data.SBV.Examples.BitPrecise.Legato flags Data.SBV.Examples.BitPrecise.Legato FlagZ Data.SBV.Examples.BitPrecise.Legato flash Data.SBV.Examples.Puzzles.U2Bridge forAll Data.SBV forAll_ Data.SBV free Data.SBV free_ Data.SBV FromBits Data.SBV fromBitsBE Data.SBV fromBitsLE Data.SBV fromBool Data.SBV fromCW Data.SBV generateGoldCheck Data.SBV.Internals getFlag Data.SBV.Examples.BitPrecise.Legato getModel Data.SBV getReg Data.SBV.Examples.BitPrecise.Legato GF28 Data.SBV.Examples.Polynomials.Polynomials here Data.SBV.Examples.Puzzles.U2Bridge hex Data.SBV hexS Data.SBV initMachine Data.SBV.Examples.BitPrecise.Legato InitVals Data.SBV.Examples.BitPrecise.Legato Instruction Data.SBV.Examples.BitPrecise.Legato Int Data.SBV Int16 Data.SBV Int32 Data.SBV Int64 Data.SBV Int8 Data.SBV ioShowsAs Data.SBV.Internals isConcrete Data.SBV isMagic Data.SBV.Examples.Puzzles.MagicSquare isSatisfiable Data.SBV isSatisfiableWithin Data.SBV isSigned Data.SBV isSymbolic Data.SBV isTheorem Data.SBV isTheoremWithin Data.SBV isU2Member Data.SBV.Examples.Puzzles.U2Bridge isValid 1 (Function) Data.SBV.Examples.Puzzles.NQueens 2 (Function) Data.SBV.Examples.Puzzles.U2Bridge ite Data.SBV lAdam Data.SBV.Examples.Puzzles.U2Bridge Larry Data.SBV.Examples.Puzzles.U2Bridge larry Data.SBV.Examples.Puzzles.U2Bridge lBono Data.SBV.Examples.Puzzles.U2Bridge lda Data.SBV.Examples.BitPrecise.Legato ldx Data.SBV.Examples.BitPrecise.Legato lEdge Data.SBV.Examples.Puzzles.U2Bridge legato Data.SBV.Examples.BitPrecise.Legato legatoIsCorrect Data.SBV.Examples.BitPrecise.Legato literal Data.SBV lLarry Data.SBV.Examples.Puzzles.U2Bridge Location Data.SBV.Examples.Puzzles.U2Bridge lsb Data.SBV magic Data.SBV.Examples.Puzzles.MagicSquare Memory Data.SBV.Examples.BitPrecise.Legato memory Data.SBV.Examples.BitPrecise.Legato Mergeable Data.SBV mergeArrays Data.SBV mkTestSuite Data.SBV.Internals Model Data.SBV.Examples.BitPrecise.Legato Mostek 1 (Type/Class) Data.SBV.Examples.BitPrecise.Legato 2 (Data Constructor) Data.SBV.Examples.BitPrecise.Legato Move Data.SBV.Examples.Puzzles.U2Bridge move1 Data.SBV.Examples.Puzzles.U2Bridge move2 Data.SBV.Examples.Puzzles.U2Bridge msb Data.SBV multAssoc Data.SBV.Examples.Polynomials.Polynomials multComm Data.SBV.Examples.Polynomials.Polynomials multUnit Data.SBV.Examples.Polynomials.Polynomials name Data.SBV newArray Data.SBV newArray_ Data.SBV nQueens Data.SBV.Examples.Puzzles.NQueens numberOfModels Data.SBV oneIf Data.SBV oppositeSignsCorrect Data.SBV.Examples.BitPrecise.BitTricks options Data.SBV OrdSymbolic Data.SBV output Data.SBV pAdd Data.SBV parseCWs Data.SBV pDiv Data.SBV pDivMod Data.SBV peek 1 (Function) Data.SBV.Examples.BitPrecise.Legato 2 (Function) Data.SBV.Examples.Puzzles.U2Bridge pMod Data.SBV pMult Data.SBV poke Data.SBV.Examples.BitPrecise.Legato polyDivMod Data.SBV.Examples.Polynomials.Polynomials Polynomial Data.SBV polynomial Data.SBV powerOfTwoCorrect Data.SBV.Examples.BitPrecise.BitTricks Predicate Data.SBV PrettyNum Data.SBV printBase Data.SBV Program Data.SBV.Examples.BitPrecise.Legato ProofError Data.SBV Provable Data.SBV prove Data.SBV proveThm Data.SBV.Examples.Uninterpreted.AUF proveWith Data.SBV Puzzle Data.SBV.Examples.Puzzles.Sudoku puzzle Data.SBV.Examples.Puzzles.DogCatMouse puzzle0 Data.SBV.Examples.Puzzles.Sudoku puzzle1 Data.SBV.Examples.Puzzles.Sudoku puzzle2 Data.SBV.Examples.Puzzles.Sudoku puzzle3 Data.SBV.Examples.Puzzles.Sudoku puzzle4 Data.SBV.Examples.Puzzles.Sudoku puzzle5 Data.SBV.Examples.Puzzles.Sudoku puzzle6 Data.SBV.Examples.Puzzles.Sudoku queries Data.SBV.Examples.BitPrecise.BitTricks readArray Data.SBV readBin Data.SBV RegA Data.SBV.Examples.BitPrecise.Legato Register Data.SBV.Examples.BitPrecise.Legato Registers Data.SBV.Examples.BitPrecise.Legato registers Data.SBV.Examples.BitPrecise.Legato RegX Data.SBV.Examples.BitPrecise.Legato resetArray Data.SBV Result Data.SBV.Internals rorM Data.SBV.Examples.BitPrecise.Legato rorR Data.SBV.Examples.BitPrecise.Legato rotate Data.SBV rotateL Data.SBV rotateR Data.SBV Row 1 (Type/Class) Data.SBV.Examples.Puzzles.MagicSquare 2 (Type/Class) Data.SBV.Examples.Puzzles.Sudoku run Data.SBV.Examples.Puzzles.U2Bridge runLegato Data.SBV.Examples.BitPrecise.Legato runSymbolic Data.SBV.Internals SArray Data.SBV sat Data.SBV Satisfiable Data.SBV SatModel Data.SBV SatResult 1 (Type/Class) Data.SBV 2 (Data Constructor) Data.SBV satWith Data.SBV SBool Data.SBV SBV 1 (Type/Class) Data.SBV.Internals 2 (Data Constructor) Data.SBV.Internals SBVTestSuite 1 (Type/Class) Data.SBV.Internals 2 (Data Constructor) Data.SBV.Internals select Data.SBV setBit Data.SBV setBitTo Data.SBV setFlag Data.SBV.Examples.BitPrecise.Legato setReg Data.SBV.Examples.BitPrecise.Legato SFunArray Data.SBV shift Data.SBV shiftL Data.SBV shiftR Data.SBV showPoly Data.SBV showsAs Data.SBV.Internals SInt16 Data.SBV SInt32 Data.SBV SInt64 Data.SBV SInt8 Data.SBV smax Data.SBV smin Data.SBV SMTConfig 1 (Type/Class) Data.SBV 2 (Data Constructor) Data.SBV SMTResult Data.SBV SMTSolver 1 (Type/Class) Data.SBV 2 (Data Constructor) Data.SBV Solution Data.SBV.Examples.Puzzles.NQueens solve 1 (Function) Data.SBV.Examples.Puzzles.DogCatMouse 2 (Function) Data.SBV.Examples.Puzzles.Sudoku solveAll Data.SBV.Examples.Puzzles.Sudoku solveN Data.SBV.Examples.Puzzles.U2Bridge solver Data.SBV solveU2 Data.SBV.Examples.Puzzles.U2Bridge split Data.SBV Splittable Data.SBV start Data.SBV.Examples.Puzzles.U2Bridge Status 1 (Type/Class) Data.SBV.Examples.Puzzles.U2Bridge 2 (Data Constructor) Data.SBV.Examples.Puzzles.U2Bridge SU2Member Data.SBV.Examples.Puzzles.U2Bridge SWord16 Data.SBV SWord32 Data.SBV SWord64 Data.SBV SWord8 Data.SBV SymArray Data.SBV Symbolic Data.SBV symbolicMerge Data.SBV SymWord Data.SBV Test Data.SBV.Internals test Data.SBV.Internals testBit Data.SBV TestCase Data.SBV.Internals testGF28 Data.SBV.Examples.Polynomials.Polynomials TestLabel Data.SBV.Internals TestList Data.SBV.Internals there Data.SBV.Examples.Puzzles.U2Bridge thm Data.SBV.Examples.Uninterpreted.AUF ThmResult 1 (Type/Class) Data.SBV 2 (Data Constructor) Data.SBV Time Data.SBV.Examples.Puzzles.U2Bridge time Data.SBV.Examples.Puzzles.U2Bridge TimeOut Data.SBV timeout Data.SBV timing Data.SBV timingSMTCfg Data.SBV true Data.SBV U2Member Data.SBV.Examples.Puzzles.U2Bridge uninterpret Data.SBV Uninterpreted Data.SBV Unknown Data.SBV unliteral Data.SBV Unsatisfiable Data.SBV valid Data.SBV.Examples.Puzzles.Sudoku Value Data.SBV.Examples.BitPrecise.Legato verbose Data.SBV verboseSMTCfg Data.SBV verboseTimingSMTCfg Data.SBV whenS Data.SBV.Examples.Puzzles.U2Bridge whereIs Data.SBV.Examples.Puzzles.U2Bridge Word Data.SBV Word16 Data.SBV Word32 Data.SBV Word64 Data.SBV Word8 Data.SBV writeArray Data.SBV xferFlash Data.SBV.Examples.Puzzles.U2Bridge xferPerson Data.SBV.Examples.Puzzles.U2Bridge xor Data.SBV yices Data.SBV ||| Data.SBV ~& Data.SBV ~: Data.SBV.Internals ~| Data.SBV