boolector (empty) → 0.0.0.1
raw patch · 9 files changed
+2153/−0 lines, 9 filesdep +basedep +boolectordep +containerssetup-changed
Dependencies added: base, boolector, containers, mtl
Files
- LICENSE +22/−0
- Setup.hs +2/−0
- boolector.cabal +72/−0
- src/Boolector.hs +1076/−0
- src/Boolector/Foreign.chs +762/−0
- test/API_Usage_Example.hs +42/−0
- test/Arith_Example.hs +90/−0
- test/Array_Example.hs +36/−0
- test/UF_Example.hs +51/−0
+ LICENSE view
@@ -0,0 +1,22 @@+Haskell binding for the Boolector SMT Solver++Copyright (c) 2018 Deian Stefan.+Copyright (c) 2014-2016 Johannes Waldmann and Armin Biere.++Permission is hereby granted, free of charge, to any person obtaining a copy of+this software and associated documentation files (the "Software"), to deal in+the Software without restriction, including without limitation the rights to+use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies+of the Software, and to permit persons to whom the Software is furnished to do+so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all+copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE+SOFTWARE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ boolector.cabal view
@@ -0,0 +1,72 @@+name: boolector+version: 0.0.0.1+synopsis: Haskell bindings for the Boolector SMT solver+description:++ This library provides a high-level, monadic DSL for writing symbolic+ computations atop the Boolector SMT solver (<https://github.com/Boolector/boolector>).+ .+ The API and its description is defined in the "Boolector" module.+ .+ Several examples can be found at: <https://github.com/PLSysSec/haskell-boolector/tree/master/test>++license: MIT+license-file: LICENSE+author: Dein Stefan, Johannes Waldmann, Armin Biere+maintainer: deian@cs.ucsd.edu+category: Math, SMT, Theorem Provers, Formal Methods, Bit vectors+build-type: Simple+cabal-version: >= 1.10++library+ hs-source-dirs: src+ default-language: Haskell2010+ exposed-modules:+ Boolector+ Boolector.Foreign+ build-depends:+ base >= 4.7 && < 5,+ containers,+ mtl++ ghc-options: -Wall -fno-warn-orphans+ build-tools: c2hs++ extra-libraries: boolector+ includes: boolector.h++Test-Suite API_Usage_Example+ default-language: Haskell2010+ Build-Depends: base >= 4.7 && < 5+ , boolector+ Type: exitcode-stdio-1.0+ main-is: API_Usage_Example.hs+ extra-libraries: boolector+ hs-source-dirs: test++Test-Suite Array_Example+ default-language: Haskell2010+ Build-Depends: base >= 4.7 && < 5+ , boolector+ Type: exitcode-stdio-1.0+ main-is: Array_Example.hs+ extra-libraries: boolector+ hs-source-dirs: test++Test-Suite UF_Example+ default-language: Haskell2010+ Build-Depends: base >= 4.7 && < 5+ , boolector+ Type: exitcode-stdio-1.0+ main-is: UF_Example.hs+ extra-libraries: boolector+ hs-source-dirs: test++Test-Suite Arith_Example+ default-language: Haskell2010+ Build-Depends: base >= 4.7 && < 5+ , boolector+ Type: exitcode-stdio-1.0+ main-is: Arith_Example.hs+ extra-libraries: boolector+ hs-source-dirs: test
+ src/Boolector.hs view
@@ -0,0 +1,1076 @@+{-|++This module exposes a DSL for writing symbolic computations atop the Boolector+SMT solver. The monadic interface manages the interface to Boolector, caches+already created sorts and variables, etc. A Boolector computation should not be+shared between threads.++Consider, the simple example from the Z3 tutorial+<https://rise4fun.com/z3/tutorialcontent/guide#h23> written in SMT LIB format:++@+ (declare-fun f (Int) Int)+ (declare-fun a () Int) ; a is a constant+ (declare-const b Int) ; syntax sugar for (declare-fun b () Int)+ (assert (> a 20))+ (assert (> b a))+ (assert (= (f 10) 1))+ (check-sat)+ (get-model)+@++With this library you can write the same program in Haskell:++@+main :: IO ()+main = do+ bs <- B.'newBoolectorState' Nothing+ B.'evalBoolector' bs $ do+ -- Create sorts:+ u32 <- B.'bitvecSort' 32+ fSort <- B.'funSort' [u32] u32++ -- Create variables f, a, and b:+ f <- B.'uf' fSort "f"+ a <- B.'var' u32 "a"+ b <- B.'var' u32 "b"++ -- Create several constants:+ c20 <- B.'unsignedInt' 20 u32+ c10 <- B.'unsignedInt' 10 u32+ c1 <- B.'one' u32++ -- Make assertions:+ B.'assert' =<< B.'ugt' a c20+ B.'assert' =<< B.'ugt' b a++ res <- B.'apply' [c10] f+ B.'assert' =<< B.'eq' res c1++ -- Check satisfiability:+ B.'Sat' <- B.'sat'++ -- Get model:+ ma <- B.'unsignedBvAssignment' a+ mb <- B.'unsignedBvAssignment' b++ -- Check model:+ assert (ma == 21) $ return ()+ assert (mb == 22) $ return ()+@++The API is inspired by the Z3 Haskell API <http://hackage.haskell.org/package/z3>.++-}++{-# language CPP #-}+{-# language GeneralizedNewtypeDeriving #-}+{-# language NoMonomorphismRestriction #-}+{-# language FlexibleContexts #-}++module Boolector ( -- * Boolector monadic computations+ Boolector+ , MonadBoolector(..)+ , evalBoolector+ , runBoolector+ -- ** Boolector state+ , BoolectorState+ , newBoolectorState+ -- ** Options and configurations+ , Option(..)+ , setOpt+ , getOpt+ , SatSolver(..)+ , setSatSolver+ -- * SAT/SMT queries+ , Node+ , sat+ , limitedSat+ , simplify+ , Status(..)+ -- ** Assert and assume+ , assert+ , assume+ , failed+ , fixateAssumptions+ , resetAssumptions+ , push+ , pop+ -- ** Variables and constants+ , var+ , const+ , constd+ , consth+ -- *** Booleans+ , bool+ , true+ , false+ -- *** Bit-vectors+ , zero+ , one+ , ones+ , unsignedInt+ , signedInt+ -- *** Arrays+ , array+ -- *** Functions+ , fun+ , uf+ -- **** Parameters+ , param+ -- *** Quantified terms+ , forall+ , exists+ -- ** Operations+ -- *** Implications and conditionals+ , implies+ , iff+ , cond+ -- *** Equality checking+ , eq+ , ne+ -- *** Bit flipping, extraction, extension, and reduction+ , not+ , neg+ , redor+ , redxor+ , redand+ , slice+ , uext+ , sext+ , concat+ -- *** Bit-wise operations+ , xor+ , xnor+ , and+ , nand+ , or+ , nor+ , sll+ , srl+ , sra+ , rol+ , ror+ -- *** Arithmetic operations+ , add+ , uaddo+ , saddo+ , inc+ , sub+ , usubo+ , ssubo+ , dec+ , mul+ , umulo+ , smulo+ , udiv+ , sdiv+ , sdivo+ , urem+ , srem+ , smod+ -- *** Comparison operations+ , ult+ , slt+ , ulte+ , slte+ , ugt+ , sgt+ , ugte+ , sgte+ -- *** Array operations+ , read+ , write+ -- *** Function operations+ , apply+ -- ** Accessors+ , getSort+ , funGetDomainSort+ , funGetCodomainSort+ , funGetArity+ , getSymbol+ , getWidth+ , getIndexWidth+ , isConst+ , isVar+ , isArray+ , isArrayVar+ , isParam+ , isBoundParam+ , isUf+ , isFun+ -- ** Models+ , bvAssignment+ , unsignedBvAssignment+ , signedBvAssignment+ , boolAssignment+ -- ** Sorts+ , Sort+ , boolSort+ , bitvecSort+ , funSort+ , arraySort+ -- *** Accessors+ , isEqualSort+ , isArraySort+ , isBitvecSort+ , isFunSort+ , funSortCheck+ -- * Debug dumping+ , dumpBtorNode+ , dumpSmt2Node+ , dumpBtor+ , dumpSmt2+ ) where++import Boolector.Foreign (Option(..), Status(..), Node, Sort)+import qualified Boolector.Foreign as B++import Data.Char (isDigit)+import Data.Map (Map)+import qualified Data.Map as Map+import Data.IntMap (IntMap)+import qualified Data.IntMap as IntMap+import Data.Word++import Control.Monad.State.Strict+import Control.Exception hiding (assert)+import Control.Concurrent++import Prelude hiding (read, not, and, or, const, concat)+import qualified Prelude as Prelude++--+-- Boolector monad+--++-- | Type class for Monads that wish to perform symbolic computations.+class MonadIO m => MonadBoolector m where+ -- | Get the Boolector state.+ getBoolectorState :: m BoolectorState+ -- | Put the Boolector state.+ putBoolectorState :: BoolectorState -> m ()++instance MonadBoolector Boolector where+ getBoolectorState = get+ putBoolectorState = put++-- | Solver state and cache+data BoolectorState = BoolectorState { unBoolectorState :: B.Btor+ , unBoolectorCache :: BoolectorCache }++-- | Bolector monad, keeping track of underlying solver state.+newtype Boolector a = Boolector { unBoolector :: StateT BoolectorState IO a }+ deriving (Functor, Applicative, Monad, MonadState BoolectorState, MonadIO)++-- | Evaluate a Boolector action with a given configurations.+evalBoolector :: BoolectorState -> Boolector a -> IO a+evalBoolector bState act = evalStateT (unBoolector act) bState++-- | Like 'evalBoolector', but take an explicit starting BoolectorState, and+-- return the final BoolectorState+runBoolector :: BoolectorState -> Boolector a -> IO (a, BoolectorState)+runBoolector bState act = runStateT (unBoolector act) bState++-- | Create new Boolector state with optional timeout. By default, we enable+-- support for model generation and incremental solving.+newBoolectorState :: Maybe Int -> IO BoolectorState+newBoolectorState Nothing = do+ b <- B.new+ B.setOpt b OPT_MODEL_GEN 2+ B.setOpt b OPT_AUTO_CLEANUP 1+ B.setOpt b OPT_INCREMENTAL 1+ return $ BoolectorState b emptyBoolectorCache+newBoolectorState (Just time) = do+ term <- newMVar 0+ btorState@(BoolectorState b _) <- newBoolectorState Nothing+ B.setTerm b $ \_ -> do+ readMVar term+ void $ forkIO $ do threadDelay $ time * 1000+ putMVar term 1 -- this will cause boolector eval to fail if not done+ return btorState++-- | Set option.+setOpt :: MonadBoolector m => Option -> Word -> m ()+setOpt o w = liftBoolector2 B.setOpt o (fromIntegral w)++-- | Get option.+getOpt :: MonadBoolector m => Option -> m Word+getOpt o = fromIntegral `liftM` liftBoolector1 B.getOpt o++-- | Which sat solver to use.+data SatSolver = Lingeling+ | PicoSAT+ | MiniSAT+ deriving Show++-- | Set the SAT solver to use. Returns 'True' if sucessfull.+setSatSolver :: MonadBoolector m => SatSolver -> m ()+setSatSolver solver = liftBoolector1 B.setSatSolver (show solver)++-- | Add a constraint.+assert :: MonadBoolector m => Node -> m ()+assert = liftBoolector1 B.assert++-- | Add an assumption.+assume :: MonadBoolector m => Node -> m ()+assume = liftBoolector1 B.assume++-- | Determine if assumption node is a failed assumption.+failed :: MonadBoolector m => Node -> m Bool+failed = liftBoolector1 B.failed++-- | Add all assumptions as assertions.+fixateAssumptions :: MonadBoolector m => m ()+fixateAssumptions = liftBoolector0 B.fixateAssumptions++-- | Resets all added assumptions.+resetAssumptions :: MonadBoolector m => m ()+resetAssumptions = liftBoolector0 B.resetAssumptions++-- | Solve an input formula.+sat :: MonadBoolector m => m Status+sat = liftBoolector0 B.sat++-- | Push new context levels.+push :: MonadBoolector m => Word -> m ()+push w = liftBoolector1 B.push (fromIntegral w)++-- | Pop context levels.+pop :: MonadBoolector m => Word -> m ()+pop w = liftBoolector1 B.pop (fromIntegral w)++-- | Solve an input formula and limit the search by the number of lemmas+-- generated and the number of conflicts encountered by the underlying+-- SAT solver.+limitedSat :: MonadBoolector m+ => Int -- ^ Limit for lemmas on demand (-1 unlimited).+ -> Int -- ^ Conflict limit for SAT solver (-1 unlimited).+ -> m Status+limitedSat = liftBoolector2 B.limitedSat++-- | Simplify current input formula.+simplify :: MonadBoolector m => m Status+simplify = liftBoolector0 B.sat++--+-- Expressions+--++-- | Like true and false+bool :: MonadBoolector m => Bool -> m Node+bool True = true+bool False = false++-- | Create constant true. This is represented by the bit vector constant one+-- with bit width one.+true :: MonadBoolector m => m Node+true = liftBoolector0 B.true++-- | Create bit vector constant zero with bit width one.+false :: MonadBoolector m => m Node+false = liftBoolector0 B.false++-- | Create bit vector constant representing the bit vector @bits@.+const :: MonadBoolector m => String -> m Node+const = liftBoolector1 B.const++-- | Create bit vector constant representing the decimal number @str@.+constd :: MonadBoolector m => Sort -> String -> m Node+constd = liftBoolector2 B.constd++-- | Create bit vector constant representing the hexadecimal number @str@.+consth :: MonadBoolector m => Sort -> String -> m Node+consth = liftBoolector2 B.consth++-- | Create bit vector constant zero of sort @sort@.+zero :: MonadBoolector m => Sort -> m Node+zero = liftBoolector1 B.zero++-- | Create bit vector constant of sort @sort@, where each bit is set to one.+ones :: MonadBoolector m => Sort -> m Node+ones = liftBoolector1 B.ones++-- | Create bit vector constant one of sort @sort@.+one :: MonadBoolector m => Sort -> m Node+one = liftBoolector1 B.one++-- | Create bit vector constant representing the unsigned integer @u@ of+-- sort @sort@.+--+-- The constant is obtained by either truncating bits or by unsigned extension+-- (padding with zeroes).+unsignedInt :: MonadBoolector m => Integer -> Sort -> m Node+unsignedInt i sort = liftBoolector2 B.unsignedInt (fromIntegral i) sort++-- | Create bit vector constant representing the signed integer @i@ of sort+-- @sort@.+--+-- The constant is obtained by either truncating bits or by+-- signed extension (padding with ones).+signedInt :: MonadBoolector m => Integer -> Sort -> m Node+signedInt i sort = liftBoolector2 B.int (fromIntegral i) sort++-- | Create a bit vector variable of sort @sort@.+var :: MonadBoolector m => Sort -> String -> m Node+var = createNamedNode B.var++-- | Create the one's complement of bit vector @node@.+not :: MonadBoolector m => Node -> m Node+not = liftBoolector1 B.not++-- | Create the two's complement of bit vector @node@.+neg :: MonadBoolector m => Node -> m Node+neg = liftBoolector1 B.neg++-- | Create *or* reduction of node @node@.+--+-- All bits of node @node@ are combined by a Boolean *or*.+redor :: MonadBoolector m => Node -> m Node+redor = liftBoolector1 B.redor++-- | Create *xor* reduction of node @node@.+--+-- All bits of @node@ are combined by a Boolean *xor*.+redxor :: MonadBoolector m => Node -> m Node+redxor = liftBoolector1 B.redxor++-- | Create *and* reduction of node @node@.+--+-- All bits of @node@ are combined by a Boolean *and*.+redand :: MonadBoolector m => Node -> m Node+redand = liftBoolector1 B.redand++-- | Create a bit vector slice of @node@ from index @upper@ to index @lower@.+slice :: MonadBoolector m+ => Node -- ^ Bit vector node.+ -> Word -- ^ Upper index which must be greater than or equal to zero, and less than the bit width of @node@.+ -> Word -- ^ Lower index which must be greater than or equal to zero, and less than or equal to @upper@.+ -> m Node+slice n u l = (liftBoolector3 B.slice) n (fromIntegral u) (fromIntegral l)++-- | Create unsigned extension.+--+-- The bit vector @node@ is padded with @width@ * zeroes.+uext :: MonadBoolector m => Node -> Word -> m Node+uext n w = (liftBoolector2 B.uext) n $ fromIntegral w++-- | Create signed extension.+--+-- The bit vector @node@ is padded with @width@ bits where the value+-- depends on the value of the most significant bit of node @n@.+sext :: MonadBoolector m => Node -> Word -> m Node+sext n w = liftBoolector2 B.sext n (fromIntegral w)++-- | Create the concatenation of two bit vectors.+concat :: MonadBoolector m => Node -> Node -> m Node+concat = liftBoolector2 B.concat++-- | Create boolean implication.+implies :: MonadBoolector m => Node -> Node -> m Node+implies = liftBoolector2 B.implies++-- | Create Boolean equivalence.+iff :: MonadBoolector m => Node -> Node -> m Node+iff = liftBoolector2 B.iff++-- | Create bit vector or array equality.+--+-- Both operands are either bit vectors with the same bit width or arrays+-- of the same type.+eq :: MonadBoolector m => Node -> Node -> m Node+eq = liftBoolector2 B.eq++-- | Create bit vector or array inequality.+--+-- Both operands are either bit vectors with the same bit width or arrays+-- of the same type.+ne :: MonadBoolector m => Node -> Node -> m Node+ne = liftBoolector2 B.ne++-- | Create an if-then-else.+--+-- If condition @n_cond@ is true, then @n_then@ is returned, else @n_else@+-- is returned.+-- Nodes @n_then@ and @n_else@ must be either both arrays or both bit vectors.+cond :: MonadBoolector m+ => Node -- ^ Condition+ -> Node -- ^ Then node+ -> Node -- ^ Else node+ -> m Node+cond = liftBoolector3 B.cond++--+-- Bit-wise operations.+--++-- | Create a bit vector *xor*.+xor :: MonadBoolector m => Node -> Node -> m Node+xor = liftBoolector2 B.xor++-- | Create a bit vector *xnor*.+xnor :: MonadBoolector m => Node -> Node -> m Node+xnor = liftBoolector2 B.xnor++-- | Create a bit vector *and*.+and :: MonadBoolector m => Node -> Node -> m Node+and = liftBoolector2 B.and++-- | Create a bit vector *nand*.+nand :: MonadBoolector m => Node -> Node -> m Node+nand = liftBoolector2 B.nand++-- | Create a bit vector *or*.+or :: MonadBoolector m => Node -> Node -> m Node+or = liftBoolector2 B.or++-- | Create a bit vector *nor*.+nor :: MonadBoolector m => Node -> Node -> m Node+nor = liftBoolector2 B.nor++-- | Create a logical shift left.+--+-- Given node @n1@, the value it represents is the number of zeroes shifted+-- into node @n0@ from the right.+sll :: MonadBoolector m+ => Node -- ^ First bit vector operand where the bit width is a power of two and greater than 1.+ -> Node -- ^ Second bit vector operand with bit width log2 of the bit width of @n0@.+ -> m Node+sll = liftBoolector2 B.sll++-- | Create a logical shift right.+--+-- Given node @n1@, the value it represents is the number of zeroes shifted+-- into node @n0@ from the left.+srl :: MonadBoolector m+ => Node -- ^ First bit vector operand where the bit width is a power of two and greater than 1.+ -> Node -- ^ Second bit vector operand with bit width log2 of the bit width of @n0@.+ -> m Node+srl = liftBoolector2 B.srl++-- | Create an arithmetic shift right.+--+-- Analogously to 'srl', but whether zeroes or ones are shifted in depends on+-- the most significant bit of @n0@.+sra :: MonadBoolector m+ => Node -- ^ First bit vector operand where the bit width is a power of two and greater than 1.+ -> Node -- ^ Second bit vector operand with bit width log2 of the bit width of @n0@.+ -> m Node+sra = liftBoolector2 B.sra++-- | Create a rotate left.+--+-- Given bit vector node @n1@, the value it represents is the number of bits+-- by which node @n0@ is rotated to the left.+rol :: MonadBoolector m+ => Node -- ^ First bit vector operand where the bit width is a power of two and greater than 1.+ -> Node -- ^ Second bit vector operand with bit width log2 of the bit width of @n0@.+ -> m Node+rol = liftBoolector2 B.rol++-- | Create a rotate right.+--+-- Given bit vector node @n1@, the value it represents is the number of bits by+-- which node @n0@ is rotated to the right.+ror :: MonadBoolector m+ => Node -- ^ First bit vector operand where the bit width is a power of two and greater than 1.+ -> Node -- ^ Second bit vector operand with bit width log2 of the bit width of @n0@.+ -> m Node+ror = liftBoolector2 B.ror++--+-- Arithmetic operations.+--++-- | Create bit vector addition.+add :: MonadBoolector m => Node -> Node -> m Node+add = liftBoolector2 B.add++-- | Create an unsigned bit vector addition overflow detection.+uaddo :: MonadBoolector m => Node -> Node -> m Node+uaddo = liftBoolector2 B.uaddo++-- | Create a signed bit vector addition overflow detection.+saddo :: MonadBoolector m => Node -> Node -> m Node+saddo = liftBoolector2 B.saddo++-- | Create bit vector expression that increments bit vector @node@ by one.+inc :: Node -> Boolector Node+inc = liftBoolector1 B.inc++-- | Create a bit vector subtraction.+sub :: MonadBoolector m => Node -> Node -> m Node+sub = liftBoolector2 B.sub++-- | Create an unsigned bit vector subtraction overflow detection.+usubo :: MonadBoolector m => Node -> Node -> m Node+usubo = liftBoolector2 B.usubo++-- | Create a signed bit vector subtraction overflow detection.+ssubo :: MonadBoolector m => Node -> Node -> m Node+ssubo = liftBoolector2 B.ssubo++-- | Create bit vector expression that decrements bit vector @node@ by one.+dec :: MonadBoolector m => Node -> m Node+dec = liftBoolector1 B.dec++-- | Create a bitvector multiplication.+mul :: MonadBoolector m => Node -> Node -> m Node+mul = liftBoolector2 B.mul++-- | Create an unsigned bit vector multiplication overflow detection.+umulo :: MonadBoolector m => Node -> Node -> m Node+umulo = liftBoolector2 B.umulo++-- | Create signed multiplication overflow detection.+smulo :: MonadBoolector m => Node -> Node -> m Node+smulo = liftBoolector2 B.smulo++-- | Create unsigned division.+udiv :: MonadBoolector m => Node -> Node -> m Node+udiv = liftBoolector2 B.udiv++-- | Create signed division.+sdiv :: MonadBoolector m => Node -> Node -> m Node+sdiv = liftBoolector2 B.sdiv++-- | Create a signed bit vector division overflow detection.+sdivo :: MonadBoolector m => Node -> Node -> m Node+sdivo = liftBoolector2 B.sdivo++-- | Create an unsigned remainder.+urem :: MonadBoolector m => Node -> Node -> m Node+urem = liftBoolector2 B.urem++-- | Create a signed remainder.+srem :: MonadBoolector m => Node -> Node -> m Node+srem = liftBoolector2 B.srem++-- | Create a, signed remainder where its sign matches the sign of the divisor.+smod :: MonadBoolector m => Node -> Node -> m Node+smod = liftBoolector2 B.smod++--+-- Comparison operations.+--++-- | Create an unsigned less than.+ult :: MonadBoolector m => Node -> Node -> m Node+ult = liftBoolector2 B.ult++-- | Create a signed less than.+slt :: MonadBoolector m => Node -> Node -> m Node+slt = liftBoolector2 B.slt++-- | Create an unsigned less than or equal.+ulte :: MonadBoolector m => Node -> Node -> m Node+ulte = liftBoolector2 B.ulte++-- | Create a signed less than or equal.+slte :: MonadBoolector m => Node -> Node -> m Node+slte = liftBoolector2 B.slte++-- | Create an unsigned greater than.+ugt :: MonadBoolector m => Node -> Node -> m Node+ugt = liftBoolector2 B.ugt++-- | Create a signed greater than.+sgt :: MonadBoolector m => Node -> Node -> m Node+sgt = liftBoolector2 B.sgt++-- | Create an unsigned greater than or equal.+ugte :: MonadBoolector m => Node -> Node -> m Node+ugte = liftBoolector2 B.ugte++-- | Create a signed greater than or equal.+sgte :: MonadBoolector m => Node -> Node -> m Node+sgte = liftBoolector2 B.sgte++--+-- Array operations+--++-- | Create a one-dimensional bit vector array with sort @sort@.+--+-- The name must be unique.+array :: MonadBoolector m => Sort -> String -> m Node+array = createNamedNode B.array++-- | Create a read on array @n_array@ at position @n_index@.+read :: MonadBoolector m+ => Node -- ^ Array operand.+ -> Node -- ^ Bit vector index. The bit width of @n_index@ must have the same bit width as the indices of @n_array@.+ -> m Node+read = liftBoolector2 B.read++-- | Create a write on array @n_array@ at position @n_index@ with value+-- @n_value@.+--+-- The array is updated at exactly one position, all other elements remain+-- unchanged. The bit width of @n_index@ must be the same as the bit width of+-- the indices of @n_array@. The bit width of @n_value@ must be the same as+-- the bit width of the elements of @n_array@.+write :: MonadBoolector m+ => Node -- ^ Array operand.+ -> Node -- ^ Bit vector index.+ -> Node -- ^ Bit vector value.+ -> m Node+write = liftBoolector3 B.write++--+-- Functions+--++-- | Create an uninterpreted function with sort @sort@.+--+-- The name must be unique.+uf :: MonadBoolector m => Sort -> String -> m Node+uf = createNamedNode B.uf++-- | Create function parameter of sort @sort@.+--+-- This kind of node is used to create parameterized expressions, which are+-- used to create functions. Once a parameter is bound to a function, it+-- cannot be re-used in other functions.+param :: MonadBoolector m => Sort -> String -> m Node+param = liftBoolector2 B.param++-- | Create a function with body @node@ parameterized over parameters+-- @param_nodes@.+--+-- This kind of node is similar to macros in the SMT-LIB standard 2.0.+-- Note that as soon as a parameter is bound to a function, it can not be+-- reused in other functions.+-- Call a function via 'apply'.+fun :: MonadBoolector m+ => [Node] -- ^ Parameters of function.+ -> Node -- ^ Function body parameterized over @param_nodes@.+ -> m Node+fun = liftBoolector2 B.fun++-- | Create a function application on function @n_fun@ with arguments+-- @arg_nodes@.+apply :: MonadBoolector m+ => [Node] -- ^ Arguments to be applied.+ -> Node -- ^ Number of arguments to be applied.+ -> m Node+apply = liftBoolector2 B.apply+++--+-- Quantified terms+--++-- | Create a universally quantified term.+forall :: MonadBoolector m+ => [Node] -- ^ Quantified variables+ -> Node -- ^ Term where variables may occur+ -> m Node+forall = liftBoolector2 B.forall++-- | Create an existentially quantifed term.+exists :: MonadBoolector m+ => [Node] -- ^ Quantified variables+ -> Node -- ^ Term where variables may occur+ -> m Node+exists = liftBoolector2 B.exists++--+-- Accessors+--++-- | Get the sort of given @node@. The result does not have to be released.+getSort :: MonadBoolector m => Node -> m Sort+getSort = liftBoolector1 B.getSort++-- | Get the domain sort of given function node @node@.+--+-- The result does not have to be released.+funGetDomainSort :: MonadBoolector m => Node -> m Sort+funGetDomainSort = liftBoolector1 B.funGetDomainSort++-- | Get the codomain sort of given function node @node@.+--+-- The result does not have to be released.+funGetCodomainSort :: MonadBoolector m => Node -> m Sort+funGetCodomainSort = liftBoolector1 B.funGetCodomainSort++-- | Get the arity of function node.+funGetArity :: MonadBoolector m => Node -> m Word+funGetArity n = fromIntegral `liftM` liftBoolector1 B.getFunArity n++-- | Get the symbol of an expression.+getSymbol :: MonadBoolector m => Node -> m String+getSymbol = liftBoolector1 B.getSymbol++-- | Get the bit width of an expression.+--+-- If the expression is an array, it returns the bit width of the array+-- elements.+-- If the expression is a function, it returns the bit width of the function's+-- return value.+getWidth :: MonadBoolector m => Node -> m Word+getWidth n = fromIntegral `liftM` liftBoolector1 B.getWidth n++-- | Get the bit width of indices of @n_array@.+getIndexWidth :: MonadBoolector m => Node -> m Word+getIndexWidth n = fromIntegral `liftM` liftBoolector1 B.getIndexWidth n++-- | Determine if given node is a constant node.+isConst :: MonadBoolector m => Node -> m Bool+isConst = liftBoolector1 B.isConst++-- | Determine if given node is a bit vector variable.+isVar :: MonadBoolector m => Node -> m Bool+isVar = liftBoolector1 B.isVar++-- | Determine if given node is an array node.+isArray :: MonadBoolector m => Node -> m Bool+isArray = liftBoolector1 B.isArray++-- | Determine if given node is an array node.+isArrayVar :: MonadBoolector m => Node -> m Bool+isArrayVar = liftBoolector1 B.isArrayVar++-- | Determine if given node is a parameter node.+isParam :: MonadBoolector m => Node -> m Bool+isParam = liftBoolector1 B.isParam++-- | Determine if given parameter node is bound by a function.+isBoundParam :: MonadBoolector m => Node -> m Bool+isBoundParam = liftBoolector1 B.isBoundParam++-- | Determine if given node is an uninterpreted function node.+isUf :: MonadBoolector m => Node -> m Bool+isUf = liftBoolector1 B.isUf++-- | Determine if given node is a function node.+isFun :: MonadBoolector m => Node -> m Bool+isFun = liftBoolector1 B.isFun+++--+-- Models.+--++-- | Generate an assignment string for bit vector expression if+-- boolector_sat has returned BOOLECTOR_SAT and model generation has been+-- enabled.+--+-- The expression can be an arbitrary bit vector expression which+-- occurs in an assertion or current assumption. The assignment string has to+-- be freed by 'freeBvAssignment'.+bvAssignment :: MonadBoolector m => Node -> m String+bvAssignment = liftBoolector1 B.bvAssignment++-- | Get unsigned integer value from model.+unsignedBvAssignment :: MonadBoolector m => Node -> m Integer+unsignedBvAssignment node = do+ str <- bvAssignment node+ when (Prelude.not $ all isDigit str) $ error $ "getModelVal: not numeric: " ++ str+ liftIO $ evaluate $ foldl (\ n c -> 2 * n + Prelude.read [c]) 0 str++-- | Get signed integer value from model.+signedBvAssignment :: MonadBoolector m => Node -> m Integer+signedBvAssignment node = do+ val <- unsignedBvAssignment node+ w <- getWidth node+ let max_signed_w = 2 ^ pred w+ return $ if val >= max_signed_w+ then val - (2*max_signed_w)+ else val++-- | Get Boolean value from model.+boolAssignment :: MonadBoolector m => Node -> m Bool+boolAssignment node = do+ str <- bvAssignment node+ liftIO $ evaluate $ case str of+ "0" -> False+ "1" -> True+ _ -> error $ "boolAssignment: not boolean: " ++ str++--+-- Sorts+--+++-- | Create Boolean sort.+boolSort :: Boolector Sort+boolSort = do+ sc <- getSortCache+ case scBool sc of+ Just srt -> return srt+ _ -> do srt <- liftBoolector0 B.boolSort+ setSortCache $ sc { scBool = Just srt }+ return srt++-- | Create bit vector sort of bit width @width@.+bitvecSort :: MonadBoolector m => Word -> m Sort+bitvecSort wnr = do+ sc <- getSortCache+ let bvMap = scBitVec sc+ case IntMap.lookup nr bvMap of+ Just srt -> return srt+ _ -> do srt <- liftBoolector1 B.bitvecSort nr+ setSortCache $ sc { scBitVec = IntMap.insert nr srt bvMap }+ return srt+ where nr = fromIntegral wnr++-- | Create function sort.+funSort :: MonadBoolector m => [Sort] -> Sort -> m Sort+funSort args ret = do+ sc <- getSortCache+ let funMap = scFun sc+ case Map.lookup (ret, args) funMap of+ Just srt -> return srt+ _ -> do srt <- liftBoolector2 B.funSort args ret+ setSortCache $ sc { scFun = Map.insert (ret, args) srt funMap }+ return srt++-- | Create array sort.+arraySort :: MonadBoolector m => Sort -> Sort -> m Sort+arraySort dom rng = do+ sc <- getSortCache+ let arrMap = scArray sc+ case Map.lookup (dom, rng) arrMap of+ Just srt -> return srt+ _ -> do srt <- liftBoolector2 B.arraySort dom rng+ setSortCache $ sc { scArray = Map.insert (dom, rng) srt arrMap }+ return srt++-- | Determine if @n0@ and @n1@ have the same sort or not.+isEqualSort :: MonadBoolector m => Node -> Node -> m Bool+isEqualSort = liftBoolector2 B.isEqualSort++-- | Determine if @sort@ is an array sort.+isArraySort :: MonadBoolector m => Sort -> m Bool+isArraySort = liftBoolector1 B.isArraySort++-- | Determine if @sort@ is a bit-vector sort.+isBitvecSort :: MonadBoolector m => Sort -> m Bool+isBitvecSort = liftBoolector1 B.isBitvecSort++-- | Determine if @sort@ is a function sort.+isFunSort :: MonadBoolector m => Sort -> m Bool+isFunSort = liftBoolector1 B.isFunSort++-- | Check if sorts of given arguments matches the function signature.+-- Returns 'Nothing' if all sorts are correct; otherwise it returns the+-- position of the incorrect argument.+funSortCheck :: MonadBoolector m => [Node] -> Node -> m (Maybe Int)+funSortCheck = liftBoolector2 B.funSortCheck+++--+-- Dumping+--++-- | Recursively dump @node@ to file in BTOR_ format.+dumpBtorNode :: MonadBoolector m => FilePath -> Node -> m ()+dumpBtorNode path node = do+ file <- liftIO $ B.fopen path "w"+ liftBoolector2 B.dumpBtorNode file node++-- | Recursively dump @node@ to file in SMT-LIB v2 format.+dumpSmt2Node :: MonadBoolector m => FilePath -> Node -> m ()+dumpSmt2Node path node = do+ file <- liftIO $ B.fopen path "w"+ liftBoolector2 B.dumpSmt2Node file node++-- | Dump formula to file in BTOR_ format.+dumpBtor :: MonadBoolector m => FilePath -> m ()+dumpBtor path = do+ file <- liftIO $ B.fopen path "w"+ liftBoolector1 B.dumpBtor file++-- | Dumps formula to file in SMT-LIB v2 format.+dumpSmt2 :: MonadBoolector m => FilePath -> m ()+dumpSmt2 path = do+ file <- liftIO $ B.fopen path "w"+ liftBoolector1 B.dumpSmt2 file++--+-- Helpers+--++liftBoolector0 :: MonadBoolector m => (B.Btor -> IO a) -> m a+liftBoolector0 f = do+ s <- getBoolectorState+ liftIO $ f (unBoolectorState s)++liftBoolector1 :: MonadBoolector m => (B.Btor -> a -> IO b) -> a -> m b+liftBoolector1 f x1 = do+ s <- getBoolectorState+ liftIO $ f (unBoolectorState s) x1++liftBoolector2 :: MonadBoolector m => (B.Btor -> a -> b -> IO c) -> a -> b -> m c+liftBoolector2 f x1 x2 = do+ s <- getBoolectorState+ liftIO $ f (unBoolectorState s) x1 x2++liftBoolector3 :: MonadBoolector m => (B.Btor -> a -> b -> c -> IO d) -> a -> b -> c -> m d+liftBoolector3 f x1 x2 x3 = do+ s <- getBoolectorState+ liftIO $ f (unBoolectorState s) x1 x2 x3++--+-- Solver cache+--++-- | Cache sorts and variables.+data BoolectorCache = BoolectorCache {+ sortCache :: SortCache+ , varCache :: VarCache+ }++-- | Empty boolector cache.+emptyBoolectorCache :: BoolectorCache+emptyBoolectorCache = BoolectorCache emptySortCache Map.empty++-- | Cache sorts.+data SortCache = SortCache {+ scBool :: Maybe Sort -- ^ Bool sort+ , scBitVec :: IntMap Sort -- ^ BitVector sorts+ , scFun :: Map (Sort, [Sort]) Sort -- ^ Function sorts+ , scArray :: Map (Sort, Sort) Sort -- ^ Array sorts+ }++-- | Empty sort cache.+emptySortCache :: SortCache+emptySortCache = SortCache Nothing IntMap.empty Map.empty Map.empty++-- | Get the sort cache from the underlying state.+getSortCache :: MonadBoolector m => m SortCache+getSortCache = (sortCache . unBoolectorCache) `liftM` getBoolectorState++-- | Set the sort cache into the underlying state.+setSortCache :: MonadBoolector m => SortCache -> m ()+setSortCache sc = do+ s0 <- getBoolectorState+ putBoolectorState $ s0 { unBoolectorCache = (unBoolectorCache s0) { sortCache = sc } }++-- | Variable and uninterpreted function cache.+type VarCache = Map (String, Sort) Node++-- | Get the variable cache from the underlying state.+getVarCache :: MonadBoolector m => m VarCache+getVarCache = (varCache . unBoolectorCache) `liftM` getBoolectorState++-- | Set the variable cache from into underlying state.+setVarCache :: MonadBoolector m => VarCache -> m ()+setVarCache vc = do+ s0 <- getBoolectorState+ putBoolectorState $ s0 { unBoolectorCache = (unBoolectorCache s0) { varCache = vc } }++-- | Create a new named node given a constructor or return it from variable+-- cache. The name must be unique.+createNamedNode :: MonadBoolector m+ => (B.Btor -> Sort -> String -> IO Node)+ -> Sort -> String -> m Node+createNamedNode ctor sort name = do+ vc <- getVarCache+ case Map.lookup (name, sort) vc of+ Just srt -> return srt+ _ -> do node <- liftBoolector2 ctor sort name+ setVarCache $ Map.insert (name, sort) node vc+ return node
+ src/Boolector/Foreign.chs view
@@ -0,0 +1,762 @@+{- |++ This module exports a subset of the low-level C Boolector API to Haskell+ code. In general, you don't want to use this module and should use the+ 'Boolector' module instead.++-}+{-# LANGUAGE StandaloneDeriving #-}+module Boolector.Foreign where++import Foreign+import Foreign.C++import Control.Monad++{#context lib = "boolector" prefix = "boolector_" #}++#include "boolector.h"+++--+-- Types+--++-- | Status.+{# enum define Status {+ BOOLECTOR_UNKNOWN as Unknown,+ BOOLECTOR_SAT as Sat,+ BOOLECTOR_UNSAT as Unsat+ } deriving (Eq, Ord, Show ) #}++-- | Boolector instances.+{#pointer *Btor as Btor foreign newtype #}+deriving instance Eq Btor+deriving instance Ord Btor++-- | AST node.+{#pointer *BoolectorNode as Node foreign newtype #}+deriving instance Eq Node+deriving instance Ord Node++-- | Sort.+{#pointer *BoolectorAnonymous as Sort foreign newtype #}+deriving instance Eq Sort+deriving instance Ord Sort++-- | Solver option.+-- See <https://github.com/Boolector/boolector/blob/47f94b39fb6e099195da043ddaf8d82e4b2aebc9/src/btortypes.h#L37>+{# enum define Option {+BTOR_OPT_MODEL_GEN as OPT_MODEL_GEN,+BTOR_OPT_INCREMENTAL as OPT_INCREMENTAL,+BTOR_OPT_INCREMENTAL_SMT1 as OPT_INCREMENTAL_SMT1,+BTOR_OPT_INPUT_FORMAT as OPT_INPUT_FORMAT,+BTOR_OPT_OUTPUT_NUMBER_FORMAT as OPT_OUTPUT_NUMBER_FORMAT,+BTOR_OPT_OUTPUT_FORMAT as OPT_OUTPUT_FORMAT,+BTOR_OPT_ENGINE as OPT_ENGINE,+BTOR_OPT_SAT_ENGINE as OPT_SAT_ENGINE,+BTOR_OPT_AUTO_CLEANUP as OPT_AUTO_CLEANUP,+BTOR_OPT_PRETTY_PRINT as OPT_PRETTY_PRINT,+BTOR_OPT_EXIT_CODES as OPT_EXIT_CODES,+BTOR_OPT_SEED as OPT_SEED,+BTOR_OPT_VERBOSITY as OPT_VERBOSITY,+BTOR_OPT_LOGLEVEL as OPT_LOGLEVEL,+BTOR_OPT_REWRITE_LEVEL as OPT_REWRITE_LEVEL,+BTOR_OPT_SKELETON_PREPROC as OPT_SKELETON_PREPROC,+BTOR_OPT_ACKERMANN as OPT_ACKERMANN,+BTOR_OPT_BETA_REDUCE_ALL as OPT_BETA_REDUCE_ALL,+BTOR_OPT_ELIMINATE_SLICES as OPT_ELIMINATE_SLICES,+BTOR_OPT_VAR_SUBST as OPT_VAR_SUBST,+BTOR_OPT_UCOPT as OPT_UCOPT,+BTOR_OPT_MERGE_LAMBDAS as OPT_MERGE_LAMBDAS,+BTOR_OPT_EXTRACT_LAMBDAS as OPT_EXTRACT_LAMBDAS,+BTOR_OPT_NORMALIZE as OPT_NORMALIZE,+BTOR_OPT_NORMALIZE_ADD as OPT_NORMALIZE_ADD,+BTOR_OPT_FUN_PREPROP as OPT_FUN_PREPROP,+BTOR_OPT_FUN_PRESLS as OPT_FUN_PRESLS,+BTOR_OPT_FUN_DUAL_PROP as OPT_FUN_DUAL_PROP,+BTOR_OPT_FUN_DUAL_PROP_QSORT as OPT_FUN_DUAL_PROP_QSORT,+BTOR_OPT_FUN_JUST as OPT_FUN_JUST,+BTOR_OPT_FUN_JUST_HEURISTIC as OPT_FUN_JUST_HEURISTIC,+BTOR_OPT_FUN_LAZY_SYNTHESIZE as OPT_FUN_LAZY_SYNTHESIZE,+BTOR_OPT_FUN_EAGER_LEMMAS as OPT_FUN_EAGER_LEMMAS,+BTOR_OPT_FUN_STORE_LAMBDAS as OPT_FUN_STORE_LAMBDAS,+BTOR_OPT_SLS_NFLIPS as OPT_SLS_NFLIPS,+BTOR_OPT_SLS_STRATEGY as OPT_SLS_STRATEGY,+BTOR_OPT_SLS_JUST as OPT_SLS_JUST,+BTOR_OPT_SLS_MOVE_GW as OPT_SLS_MOVE_GW,+BTOR_OPT_SLS_MOVE_RANGE as OPT_SLS_MOVE_RANGE,+BTOR_OPT_SLS_MOVE_SEGMENT as OPT_SLS_MOVE_SEGMENT,+BTOR_OPT_SLS_MOVE_RAND_WALK as OPT_SLS_MOVE_RAND_WALK,+BTOR_OPT_SLS_PROB_MOVE_RAND_WALK as OPT_SLS_PROB_MOVE_RAND_WALK,+BTOR_OPT_SLS_MOVE_RAND_ALL as OPT_SLS_MOVE_RAND_ALL,+BTOR_OPT_SLS_MOVE_RAND_RANGE as OPT_SLS_MOVE_RAND_RANGE,+BTOR_OPT_SLS_MOVE_PROP as OPT_SLS_MOVE_PROP,+BTOR_OPT_SLS_MOVE_PROP_N_PROP as OPT_SLS_MOVE_PROP_N_PROP,+BTOR_OPT_SLS_MOVE_PROP_N_SLS as OPT_SLS_MOVE_PROP_N_SLS,+BTOR_OPT_SLS_MOVE_PROP_FORCE_RW as OPT_SLS_MOVE_PROP_FORCE_RW,+BTOR_OPT_SLS_MOVE_INC_MOVE_TEST as OPT_SLS_MOVE_INC_MOVE_TEST,+BTOR_OPT_SLS_USE_RESTARTS as OPT_SLS_USE_RESTARTS,+BTOR_OPT_SLS_USE_BANDIT as OPT_SLS_USE_BANDIT,+BTOR_OPT_PROP_NPROPS as OPT_PROP_NPROPS,+BTOR_OPT_PROP_USE_RESTARTS as OPT_PROP_USE_RESTARTS,+BTOR_OPT_PROP_USE_BANDIT as OPT_PROP_USE_BANDIT,+BTOR_OPT_PROP_PATH_SEL as OPT_PROP_PATH_SEL,+BTOR_OPT_PROP_PROB_USE_INV_VALUE as OPT_PROP_PROB_USE_INV_VALUE,+BTOR_OPT_PROP_PROB_FLIP_COND as OPT_PROP_PROB_FLIP_COND,+BTOR_OPT_PROP_PROB_FLIP_COND_CONST as OPT_PROP_PROB_FLIP_COND_CONST,+BTOR_OPT_PROP_FLIP_COND_CONST_DELTA as OPT_PROP_FLIP_COND_CONST_DELTA,+BTOR_OPT_PROP_FLIP_COND_CONST_NPATHSEL as OPT_PROP_FLIP_COND_CONST_NPATHSEL,+BTOR_OPT_PROP_PROB_SLICE_KEEP_DC as OPT_PROP_PROB_SLICE_KEEP_DC,+BTOR_OPT_PROP_PROB_CONC_FLIP as OPT_PROP_PROB_CONC_FLIP,+BTOR_OPT_PROP_PROB_SLICE_FLIP as OPT_PROP_PROB_SLICE_FLIP,+BTOR_OPT_PROP_PROB_EQ_FLIP as OPT_PROP_PROB_EQ_FLIP,+BTOR_OPT_PROP_PROB_AND_FLIP as OPT_PROP_PROB_AND_FLIP,+BTOR_OPT_PROP_NO_MOVE_ON_CONFLICT as OPT_PROP_NO_MOVE_ON_CONFLICT,+BTOR_OPT_AIGPROP_USE_RESTARTS as OPT_AIGPROP_USE_RESTARTS,+BTOR_OPT_AIGPROP_USE_BANDIT as OPT_AIGPROP_USE_BANDIT,+BTOR_OPT_QUANT_SYNTH as OPT_QUANT_SYNTH,+BTOR_OPT_QUANT_DUAL_SOLVER as OPT_QUANT_DUAL_SOLVER,+BTOR_OPT_QUANT_SYNTH_LIMIT as OPT_QUANT_SYNTH_LIMIT,+BTOR_OPT_QUANT_SYNTH_ITE_COMPLETE as OPT_QUANT_SYNTH_ITE_COMPLETE,+BTOR_OPT_QUANT_FIXSYNTH as OPT_QUANT_FIXSYNTH,+BTOR_OPT_QUANT_SYNTH_QI as OPT_QUANT_SYNTH_QI,+BTOR_OPT_QUANT_DER as OPT_QUANT_DER,+BTOR_OPT_QUANT_CER as OPT_QUANT_CER,+BTOR_OPT_QUANT_MINISCOPE as OPT_QUANT_MINISCOPE,+BTOR_OPT_DEFAULT_TO_CADICAL as OPT_DEFAULT_TO_CADICAL,+BTOR_OPT_SORT_EXP as OPT_SORT_EXP,+BTOR_OPT_SORT_AIG as OPT_SORT_AIG,+BTOR_OPT_SORT_AIGVEC as OPT_SORT_AIGVEC,+BTOR_OPT_AUTO_CLEANUP_INTERNAL as OPT_AUTO_CLEANUP_INTERNAL,+BTOR_OPT_SIMPLIFY_CONSTRAINTS as OPT_SIMPLIFY_CONSTRAINTS,+BTOR_OPT_CHK_FAILED_ASSUMPTIONS as OPT_CHK_FAILED_ASSUMPTIONS,+BTOR_OPT_CHK_MODEL as OPT_CHK_MODEL,+BTOR_OPT_CHK_UNCONSTRAINED as OPT_CHK_UNCONSTRAINED,+BTOR_OPT_PARSE_INTERACTIVE as OPT_PARSE_INTERACTIVE,+BTOR_OPT_SAT_ENGINE_LGL_FORK as OPT_SAT_ENGINE_LGL_FORK,+BTOR_OPT_INCREMENTAL_RW as OPT_INCREMENTAL_RW,+BTOR_OPT_DECLSORT_BV_WIDTH as OPT_DECLSORT_BV_WIDTH,+BTOR_OPT_NUM_OPTS as OPT_NUM_OPTS+} deriving (Eq, Ord, Show ) #}+++--+-- Solver-level interface+--++-- | Create a new instance of Boolector.+new :: IO (Btor)+new = do+ ptrBtor <- new'_ + -- run delete on the btor at the end+ foreignPtrBtor <- newForeignPtr boolector_delete ptrBtor+ -- run release_all before delete+ addForeignPtrFinalizer boolector_release_all foreignPtrBtor + return $ Btor foreignPtrBtor++foreign import ccall "boolector_new"+ new'_ :: IO (Ptr Btor)++foreign import ccall "&boolector_delete"+ boolector_delete :: FinalizerPtr Btor++foreign import ccall "&boolector_release_all"+ boolector_release_all :: FinalizerPtr Btor++-- | Push new context levels.+{#fun push as ^ { `Btor', `CUInt' } -> `()' #}++-- | Pop context levels.+{#fun pop as ^ { `Btor', `CUInt' } -> `()' #}++-- | Set a termination callback.+setTerm :: Btor -> (Ptr () -> IO Int) -> IO ()+setTerm b callback = do+ cb <- makeWrapper callback+ withBtor b $ \ b' -> setTerm'_ b' cb nullPtr++foreign import ccall "wrapper"+ makeWrapper :: (Ptr () -> IO Int) -> IO (FunPtr (Ptr () -> IO Int))++foreign import ccall "boolector_set_term"+ setTerm'_ :: Ptr Btor -> (FunPtr (Ptr () -> IO Int)) -> Ptr () -> IO ()++--+-- Options+--++-- | Set the SAT solver to use.+--+-- Currently supported: @Lingeling@, @PicoSAT@, and @MiniSAT@.+-- Returns non-zero value if setting the SAT solver was successful.+{#fun set_sat_solver as ^ { `Btor', `String' } -> `()' #}++-- | Set option. See btortypes.h+{#fun set_opt as ^ { `Btor', `Option', `CUInt' } -> `()' #}++-- | Get the current value of an option.+{#fun get_opt as ^ { `Btor', `Option' } -> `CUInt' #}++-- | Check if Boolector has a given option.+{#fun has_opt as ^ { `Btor', `Option' } -> `Bool' #}++--+-- Solving+--++-- | Add a constraint.+{#fun assert as ^ { `Btor' , `Node' } -> `()' #}++-- | Add an assumption.+{#fun assume as ^ { `Btor' , `Node' } -> `()' #}++-- | Determine if assumption @node@ is a failed assumption.+--+-- Failed assumptions are those assumptions, that force an input formula+-- to become unsatisfiable.+{#fun failed as ^ { `Btor' , `Node' } -> `Bool' #}++-- | Add all assumptions as assertions.+{#fun fixate_assumptions as ^ { `Btor' } -> `()' #}++-- | Resets all added assumptions.+{#fun reset_assumptions as ^ { `Btor' } -> `()' #}++-- | Solve an input formula.+--+-- An input formula is defined by constraints added via 'assert'.+-- You can guide the search for a solution to an input formula by making+-- assumptions via 'assume'.+{#fun sat as ^ { `Btor' } -> `Status' #}++-- | Solve an input formula and limit the search by the number of lemmas+-- generated and the number of conflicts encountered by the underlying+-- SAT solver.+--+-- An input formula is defined by constraints added via 'assert'.+-- You can guide the search for a solution to an input formula by making+-- assumptions via 'assume'.+--+-- Returns 'Sat' if the input formula is satisfiable (under possibly given+-- assumptions), 'Usat' if the instance is unsatisfiable, and 'Unknown' if the+-- instance could not be solved within given limits.+{#fun limited_sat as ^ { `Btor' , `Int', `Int' } -> `Status' #}++-- | Simplify current input formula.+{#fun simplify as ^ { `Btor' } -> `Status' #}++--+-- Expressions+--++-- | Copy expression (increments reference counter).+{#fun copy as ^ { `Btor' , `Node' } -> `Node' #}++-- | Create bit vector constant representing the bit vector @bits@.+{#fun const as ^ { `Btor' , `String' } -> `Node' #}++-- | Create bit vector constant representing the decimal number @str@.+{#fun constd as ^ { `Btor' , `Sort', `String' } -> `Node' #}++-- | Create bit vector constant representing the hexadecimal number @str@.+{#fun consth as ^ { `Btor' , `Sort', `String' } -> `Node' #}++-- | Create constant true. This is represented by the bit vector constant one+-- with bit width one.+{#fun true as ^ { `Btor' } -> `Node' #}++-- | Create bit vector constant zero with bit width one.+{#fun false as ^ { `Btor' } -> `Node' #}++-- | Create bit vector constant zero of sort @sort@.+{#fun zero as ^ { `Btor', `Sort' } -> `Node' #}++-- | Create bit vector constant one of sort @sort@.+{#fun one as ^ { `Btor', `Sort' } -> `Node' #}++-- | Create bit vector constant of sort @sort@, where each bit is set to one.+{#fun ones as ^ { `Btor', `Sort' } -> `Node' #}++-- | Create bit vector constant representing the unsigned integer @u@ of+-- sort @sort@.+--+-- The constant is obtained by either truncating bits or by+-- unsigned extension (padding with zeroes).+{#fun unsigned_int as ^ { `Btor', `CUInt', `Sort' } -> `Node' #}++-- | Create bit vector constant representing the signed integer @i@ of sort+-- @sort@.+--+-- The constant is obtained by either truncating bits or by+-- signed extension (padding with ones).+{#fun int as ^ { `Btor', `CInt', `Sort' } -> `Node' #}++-- | Create a bit vector variable of sort @sort@.+--+-- The name must be unique.+{#fun var as ^ { `Btor' , `Sort', `String' } -> `Node' #}++-- | Create the one's complement of bit vector @node@.+{#fun not as ^ { `Btor' , `Node'} -> `Node' #}++-- | Create the two's complement of bit vector @node@.+{#fun neg as ^ { `Btor' , `Node'} -> `Node' #}++-- | Create *or* reduction of node @node@.+--+-- All bits of node @node@ are combined by a Boolean *or*.+{#fun redor as ^ { `Btor' , `Node'} -> `Node' #}++-- | Create *xor* reduction of node @node@.+--+-- All bits of @node@ are combined by a Boolean *xor*.+{#fun redxor as ^ { `Btor' , `Node'} -> `Node' #}++-- | Create *and* reduction of node @node@.+--+-- All bits of @node@ are combined by a Boolean *and*.+{#fun redand as ^ { `Btor' , `Node'} -> `Node' #}++-- | Create a bit vector slice of @node@ from index @upper@ to index @lower@.+{#fun slice as ^ { `Btor' , `Node', `CUInt', `CUInt'} -> `Node' #}++-- | Create unsigned extension.+--+-- The bit vector @node@ is padded with @width@ * zeroes.+{#fun uext as ^ { `Btor' , `Node', `CUInt'} -> `Node' #}++-- | Create signed extension.+--+-- The bit vector @node@ is padded with @width@ bits where the value+-- depends on the value of the most significant bit of node @n@.+{#fun sext as ^ { `Btor' , `Node', `CUInt'} -> `Node' #}++-- | Create the concatenation of two bit vectors.+{#fun concat as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create @n@ concatenations of a given node @node@.+{#fun repeat as ^ { `Btor' , `Node', `CUInt'} -> `Node' #}++--+-- Implications.+--++-- | Create boolean implication.+{#fun implies as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create Boolean equivalence.+{#fun iff as ^ { `Btor' , `Node', `Node'} -> `Node' #}++--+-- Equality.+--++-- | Create bit vector or array equality.+--+-- Both operands are either bit vectors with the same bit width or arrays+-- of the same type.+{#fun eq as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create bit vector or array inequality.+--+-- Both operands are either bit vectors with the same bit width or arrays+-- of the same type.+{#fun ne as ^ { `Btor' , `Node', `Node'} -> `Node' #}++--+-- Conditionals.+--++-- | Create an if-then-else.+--+-- If condition @n_cond@ is true, then @n_then@ is returned, else @n_else@+-- is returned.+-- Nodes @n_then@ and @n_else@ must be either both arrays or both bit vectors.+{#fun cond as ^ { `Btor' , `Node', `Node', `Node'} -> `Node' #}++--+-- Bit-wise operations.+--++-- | Create a bit vector *xor*.+{#fun xor as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create a bit vector *xnor*.+{#fun xnor as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create a bit vector *and*.+{#fun and as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create a bit vector *nand*.+{#fun nand as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create a bit vector *or*.+{#fun or as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create a bit vector *nor*.+{#fun nor as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create a logical shift left.+--+-- Given node @n1@, the value it represents is the number of zeroes shifted+-- into node @n0@ from the right.+{#fun sll as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create a logical shift right.+--+-- Given node @n1@, the value it represents is the number of zeroes shifted+-- into node @n0@ from the left.+{#fun srl as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create an arithmetic shift right.+--+-- Analogously to 'srl', but whether zeroes or ones are shifted in depends on+-- the most significant bit of @n0@.+{#fun sra as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create a rotate left.+--+-- Given bit vector node @n1@, the value it represents is the number of bits+-- by which node @n0@ is rotated to the left.+{#fun rol as ^ { `Btor' , `Node', `Node'} -> `Node' #}+-- | Create a rotate right.+--+-- Given bit vector node @n1@, the value it represents is the number of bits by+-- which node @n0@ is rotated to the right.+{#fun ror as ^ { `Btor' , `Node', `Node'} -> `Node' #}++--+-- Arithmetic operations.+--++-- | Create bit vector addition.+{#fun add as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create bit vector expression that increments bit vector @node@ by one.+{#fun inc as ^ { `Btor' , `Node' } -> `Node' #}++-- | Create an unsigned bit vector addition overflow detection.+{#fun uaddo as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create a signed bit vector addition overflow detection.+{#fun saddo as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create a bit vector subtraction.+{#fun sub as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create an unsigned bit vector subtraction overflow detection.+{#fun usubo as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create a signed bit vector subtraction overflow detection.+{#fun ssubo as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create bit vector expression that decrements bit vector @node@ by one.+{#fun dec as ^ { `Btor' , `Node' } -> `Node' #}++-- | Create a bitvector multiplication.+{#fun mul as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create an unsigned bit vector multiplication overflow detection.+{#fun umulo as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create signed multiplication overflow detection.+{#fun smulo as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create unsigned division.+{#fun udiv as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create signed division.+{#fun sdiv as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create a signed bit vector division overflow detection.+{#fun sdivo as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create an unsigned remainder.+{#fun urem as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create a signed remainder.+{#fun srem as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create a, signed remainder where its sign matches the sign of the divisor.+{#fun smod as ^ { `Btor' , `Node', `Node'} -> `Node' #}++--+-- Comparison operations.+--++-- | Create an unsigned less than.+{#fun ult as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create a signed less than.+{#fun slt as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create an unsigned less than or equal.+{#fun ulte as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create a signed less than or equal.+{#fun slte as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create an unsigned greater than.+{#fun ugt as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create a signed greater than.+{#fun sgt as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create an unsigned greater than or equal.+{#fun ugte as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create a signed greater than or equal.+{#fun sgte as ^ { `Btor' , `Node', `Node'} -> `Node' #}++--+-- Array operations+--++-- | Create a one-dimensional bit vector array with sort @sort@.+--+-- The name must be unique.+{#fun array as ^ { `Btor' , `Sort', `String' } -> `Node' #}++-- | Create a read on array @n_array@ at position @n_index@.+{#fun read as ^ { `Btor' , `Node', `Node'} -> `Node' #}++-- | Create a write on array @n_array@ at position @n_index@ with value+-- @n_value@.+--+-- The array is updated at exactly one position, all other elements remain+-- unchanged. The bit width of @n_index@ must be the same as the bit width of+-- the indices of @n_array@. The bit width of @n_value@ must be the same as+-- the bit width of the elements of @n_array@.+{#fun write as ^ { `Btor' , `Node', `Node', `Node'} -> `Node' #}++--+-- Functions+--++-- | Create an uninterpreted function with sort @sort@.+--+-- The name must be unique.+{#fun uf as ^ { `Btor' , `Sort', `String' } -> `Node' #}+++-- | Create function parameter of sort @sort@.+--+-- This kind of node is used to create parameterized expressions, which are+-- used to create functions. Once a parameter is bound to a function, it+-- cannot be re-used in other functions.+{#fun param as ^ { `Btor' , `Sort', `String'} -> `Node' #}++-- | Create a function with body @node@ parameterized over parameters+-- @param_nodes@.+--+-- This kind of node is similar to macros in the SMT-LIB standard 2.0.+-- Note that as soon as a parameter is bound to a function, it can not be+-- reused in other functions.+-- Call a function via 'apply'.+fun :: Btor -> [Node] -> Node -> IO Node+fun hbtor hargs hret = withBtor hbtor $ \cbotr ->+ withNodes hargs $ \cargs ->+ withArrayLen cargs $ \len cargsPtr ->+ withNode hret $ \cret -> do+ cptr <- fun'_ cbotr cargsPtr (fromIntegral len) cret+ Node `liftM` newForeignPtr_ cptr++foreign import ccall "boolector_fun"+ fun'_ :: Ptr Btor -> Ptr (Ptr Node) -> CUInt -> Ptr Node -> IO (Ptr Node)++-- | Create a function application on function @n_fun@ with arguments+-- @arg_nodes@.+apply :: Btor -> [Node] -> Node -> IO Node+apply hbtor hargs hfun = withBtor hbtor $ \cbotr ->+ withNodes hargs $ \cargs ->+ withArrayLen cargs $ \len cargsPtr ->+ withNode hfun $ \cfun -> do+ cptr <- apply'_ cbotr cargsPtr (fromIntegral len) cfun+ Node `liftM` newForeignPtr_ cptr++foreign import ccall "boolector_apply"+ apply'_ :: Ptr Btor -> Ptr (Ptr Node) -> CUInt -> Ptr Node -> IO (Ptr Node)++-- | Create a universally quantified term.+forall :: Btor -> [Node] -> Node -> IO Node+forall hbtor hparams hbody = withBtor hbtor $ \cbotr ->+ withNodes hparams $ \cparams ->+ withArrayLen cparams $ \len cparamsPtr ->+ withNode hbody $ \cbody -> do+ cptr <- forall'_ cbotr cparamsPtr (fromIntegral len) cbody+ Node `liftM` newForeignPtr_ cptr++foreign import ccall "boolector_forall"+ forall'_ :: Ptr Btor -> Ptr (Ptr Node) -> CUInt -> Ptr Node -> IO (Ptr Node)++-- | Create an existentially quantifed term.+exists :: Btor -> [Node] -> Node -> IO Node+exists hbtor hparams hbody = withBtor hbtor $ \cbotr ->+ withNodes hparams $ \cparams ->+ withArrayLen cparams $ \len cparamsPtr ->+ withNode hbody $ \cbody -> do+ cptr <- exists'_ cbotr cparamsPtr (fromIntegral len) cbody+ Node `liftM` newForeignPtr_ cptr++foreign import ccall "boolector_exists"+ exists'_ :: Ptr Btor -> Ptr (Ptr Node) -> CUInt -> Ptr Node -> IO (Ptr Node)++-- | Helper function for executing list of Nodes.+withNodes :: [Node] -> ([Ptr Node] -> IO a) -> IO a+withNodes [] f = f []+withNodes (hx:hxs) f = withNode hx $ \cx -> withNodes hxs $ \cxs -> f (cx:cxs)+++--+-- Accessors+--++-- | Get the sort of given node.+{#fun get_sort as ^ { `Btor' , `Node' } -> `Sort' #}++-- | Get the domain sort of given function node node.+{#fun fun_get_domain_sort as ^ { `Btor' , `Node' } -> `Sort' #}++-- | Get the codomain sort of given function node node.+{#fun fun_get_codomain_sort as ^ { `Btor' , `Node' } -> `Sort' #}++-- | Get the arity of function node.+{#fun get_fun_arity as ^ { `Btor' , `Node' } -> `CUInt' #}++-- | Get the symbol of an expression.+{#fun get_symbol as ^ { `Btor' , `Node' } -> `String' #}++-- | Set the symbol of an expression.+{#fun set_symbol as ^ { `Btor' , `Node', `String' } -> `()' #}++-- | Get the bit width of an expression.+--+-- If the expression is an array, it returns the bit width of the array+-- elements.+-- If the expression is a function, it returns the bit width of the function's+-- return value.+{#fun get_width as ^ { `Btor' , `Node' } -> `CUInt' #}++-- | Get the bit width of indices of @n_array@.+{#fun get_index_width as ^ { `Btor' , `Node' } -> `CUInt' #}++-- | Determine if given node is a constant node.+{#fun is_const as ^ { `Btor' , `Node' } -> `Bool' #}++-- | Determine if given node is a bit vector variable.+{#fun is_var as ^ { `Btor' , `Node' } -> `Bool' #}++-- | Determine if given node is an array node.+{#fun is_array as ^ { `Btor' , `Node' } -> `Bool' #}++-- | Determine if given node is an array node.+{#fun is_array_var as ^ { `Btor' , `Node' } -> `Bool' #}++-- | Determine if given node is a parameter node.+{#fun is_param as ^ { `Btor' , `Node' } -> `Bool' #}++-- | Determine if given parameter node is bound by a function.+{#fun is_bound_param as ^ { `Btor' , `Node' } -> `Bool' #}++-- | Determine if given node is an uninterpreted function node.+{#fun is_uf as ^ { `Btor' , `Node' } -> `Bool' #}++-- | Determine if given node is a function node.+{#fun is_fun as ^ { `Btor' , `Node' } -> `Bool' #}++-- | Check if sorts of given arguments matches the function signature.+-- Returns 'Nothing' if all sorts are correct; otherwise it returns the+-- position of the incorrect argument.+funSortCheck :: Btor -> [Node] -> Node -> IO (Maybe Int)+funSortCheck hbtor hparams hfun = withBtor hbtor $ \cbotr ->+ withNodes hparams $ \cparams ->+ withArrayLen cparams $ \len cparamsPtr ->+ withNode hfun $ \cfun -> do+ rt <- funSortCheck'_ cbotr cparamsPtr (fromIntegral len) cfun+ return $ if rt == -1+ then Nothing+ else Just $ fromIntegral rt++foreign import ccall "boolector_fun_sort_check"+ funSortCheck'_ :: Ptr Btor -> Ptr (Ptr Node) -> CUInt -> Ptr Node -> IO CInt++--+-- Models.+--++-- | Generate an assignment string for bit vector expression if+-- 'sat' has returned 'Sat' and model generation has been enabled.+--+-- The expression can be an arbitrary bit vector expression which+-- occurs in an assertion or current assumption. The assignment string has to+-- be freed by 'free_bv_assignment'.+{#fun bv_assignment as ^ { `Btor' , `Node' } -> `String' #}++-- | Free an assignment string for bit vectors. TODO: we should change+-- bv_assignment to return a ModelString and use free to actually free the+-- assignments. We're very leaky right now.+{#fun free_bv_assignment as ^ { `Btor' , `String' } -> `()' #}++--+-- Sorts.+--++-- | Create Boolean sort.+{#fun bool_sort as ^ { `Btor'} -> `Sort' #}++-- | Create bit vector sort of bit width @width@.+{#fun bitvec_sort as ^ { `Btor' , `CUInt' } -> `Sort' #}++-- | Create function sort.+funSort :: Btor -> [Sort] -> Sort -> IO Sort+funSort hbtor hargs hret = withBtor hbtor $ \cbotr ->+ withSorts hargs $ \cargs ->+ withArrayLen cargs $ \len cargsPtr ->+ withSort hret $ \cret -> do+ cptr <- funSort'_ cbotr cargsPtr (fromIntegral len) cret+ Sort `liftM` newForeignPtr_ cptr++foreign import ccall "boolector_fun_sort"+ funSort'_ :: Ptr Btor -> Ptr (Ptr Sort) -> CUInt -> Ptr Sort -> IO (Ptr Sort)++-- | Helper function for executing list of Sorts.+withSorts :: [Sort] -> ([Ptr Sort] -> IO a) -> IO a+withSorts [] f = f []+withSorts (hx:hxs) f = withSort hx $ \cx -> withSorts hxs $ \cxs -> f (cx:cxs)++-- | Create array sort.+{#fun array_sort as ^ { `Btor' , `Sort', `Sort' } -> `Sort' #}++-- | Determine if @n0@ and @n1@ have the same sort or not.+{#fun is_equal_sort as ^ { `Btor' , `Node', `Node' } -> `Bool' #}++-- | Determine if @sort@ is an array sort.+{#fun is_array_sort as ^ { `Btor' , `Sort' } -> `Bool' #}++-- | Determine if @sort@ is a bit-vector sort.+{#fun is_bitvec_sort as ^ { `Btor' , `Sort' } -> `Bool' #}++-- | Determine if @sort@ is a function sort.+{#fun is_fun_sort as ^ { `Btor' , `Sort' } -> `Bool' #}++--+-- Dumping+--++{#pointer *FILE as File foreign finalizer fclose newtype#}++-- | libc's fopen+{#fun fopen as ^ {`String', `String'} -> `File' #}++-- | Recursively dump @node@ to file in BTOR_ format.+{#fun dump_btor_node as ^ { `Btor' , `File', `Node' } -> `()' #}++-- | Dump formula to file in BTOR_ format.+{#fun dump_btor as ^ { `Btor' , `File' } -> `()' #}++-- | Recursively dump @node@ to file in SMT-LIB v2 format.+{#fun dump_smt2_node as ^ { `Btor' , `File', `Node' } -> `()' #}++-- | Dumps formula to file in SMT-LIB v2 format.+{#fun dump_smt2 as ^ { `Btor' , `File' } -> `()' #}
+ test/API_Usage_Example.hs view
@@ -0,0 +1,42 @@+import qualified Boolector as B++import Control.Monad.IO.Class+import Control.Exception (assert)+import Control.Concurrent++main :: IO ()+main = do+ -- Create new Boolector state with a 1000ms timeout+ bs <- B.newBoolectorState (Just 1000)+ B.evalBoolector bs $ do+ -- Create a 8-bit bit-vector+ u8 <- B.bitvecSort 8++ -- Create a constant value and two variables of sort u8+ c <- B.unsignedInt 35 u8+ x <- B.var u8 "x"+ y <- B.var u8 "y"++ -- Perofmr some operations on the values+ p <- B.mul x y+ o <- B.umulo x y+ no <- B.not o+ e <- B.eq c p++ -- Make some assertions+ B.assert =<< B.and no e+ one <- B.one u8+ B.assert =<< B.ugt x one+ B.assert =<< B.ugt y one++ -- Dump the corresponding SMT Lib 2 to a file+ B.dumpSmt2 "dump_example.smt2"++ -- Check satisfiability+ B.Sat <- B.sat++ -- Get model+ mx <- B.unsignedBvAssignment x+ my <- B.unsignedBvAssignment y+ assert (mx == 7) $ return ()+ assert (my == 5) $ return ()
+ test/Arith_Example.hs view
@@ -0,0 +1,90 @@+import qualified Boolector as B++import Control.Monad.IO.Class+import Control.Exception (assert)+++main :: IO ()+main = do+ bs <- B.newBoolectorState Nothing+ B.evalBoolector bs $ do+ -- Create sorts:+ i32 <- B.bitvecSort 32+ fSort <- B.funSort [i32] i32+ gSort <- B.funSort [i32, i32] i32++ -- Create variables x, y, z, f, g+ x <- B.var i32 "x"+ y <- B.var i32 "y"+ z <- B.var i32 "z"+ f <- B.uf fSort "f"+ g <- B.uf gSort "g"++ -- Create constant:+ two <- B.signedInt 2 i32+ + -- Create action to print model+ let printModel = do mx <- B.signedBvAssignment x+ my <- B.signedBvAssignment y+ mz <- B.signedBvAssignment z+ liftIO $ putStrLn $ show [mx, my, mz]+ + -- (assert (>= (* 2 x) (+ y z)))+ do tmp1 <- B.mul two x+ tmp2 <- B.add y z+ B.assert =<< B.sgte tmp1 tmp2++ -- (assert (< (f x) (g x x)))+ do tmp1 <- B.apply [x] f+ tmp2 <- B.apply [x, x] g+ B.assert =<< B.slt tmp1 tmp2++ -- (assert (> (f y) (g x x)))+ do tmp1 <- B.apply [y] f+ tmp2 <- B.apply [x, x] g+ B.assert =<< B.sgt tmp1 tmp2++ -- Check satisfiability:+ B.Sat <- B.sat++ -- Print model:+ printModel++ -- Push context+ B.push 1++ -- Add (false) assertion:+ B.assert =<< B.eq x y++ -- Check satisfiability:+ B.Unsat <- B.sat++ -- Pop context+ B.pop 1++ -- Can check sat again and pirnt model+ B.Sat <- B.sat+ printModel++++{- This example is from https://rise4fun.com/Z3/smtc_arith:++; This example illustrates basic arithmetic and uninterpreted functions+(declare-fun x () Int)+(declare-fun y () Int)+(declare-fun z () Int)+(assert (>= (* 2 x) (+ y z)))+(declare-fun f (Int) Int)+(declare-fun g (Int Int) Int)+(assert (< (f x) (g x x)))+(assert (> (f y) (g x x)))+(check-sat)+(get-model)+(push)+(assert (= x y))+(check-sat)+(pop)+(exit)++-}
+ test/Array_Example.hs view
@@ -0,0 +1,36 @@+import qualified Boolector as B++import Control.Monad.IO.Class+import Control.Exception (assert)++main :: IO ()+main = do+ bs <- B.newBoolectorState Nothing+ B.evalBoolector bs $ do+ u8 <- B.bitvecSort 8+ u32 <- B.bitvecSort 32++ arr8x32 <- B.arraySort u8 u32++ arr <- B.array arr8x32 "a"++ x <- B.var u8 "x"+ y <- B.unsignedInt 35 u32+ B.write arr x y++ z <- B.unsignedInt 23 u8+ B.assert =<< B.eq x z++ y' <- B.read arr x+ w <- B.var u8 "w"++ B.dumpSmt2 "dump_example.smt2"+ B.sat+ mx <- B.unsignedBvAssignment x+ my <- B.unsignedBvAssignment y+ my' <- B.unsignedBvAssignment y'+ mz <- B.unsignedBvAssignment z+ assert (mx == 23) $ return ()+ assert (my == 35) $ return ()+ assert (my' == 35) $ return ()+ assert (mz == 23) $ return ()
+ test/UF_Example.hs view
@@ -0,0 +1,51 @@+import qualified Boolector as B++import Control.Monad.IO.Class+import Control.Exception (assert)+++main :: IO ()+main = do+ bs <- B.newBoolectorState Nothing+ B.evalBoolector bs $ do+ -- Create sorts:+ u32 <- B.bitvecSort 32+ fSort <- B.funSort [u32] u32++ -- Create variables f, a, and b:+ f <- B.uf fSort "f"+ a <- B.var u32 "a"+ b <- B.var u32 "b"++ c20 <- B.unsignedInt 20 u32+ c10 <- B.unsignedInt 10 u32+ c1 <- B.one u32++ -- Make assertions:+ B.assert =<< B.ugt a c20+ B.assert =<< B.ugt b a++ res <- B.apply [c10] f+ B.assert =<< B.eq res c1++ -- Check satisfiability:+ B.Sat <- B.sat++ -- Get model:+ ma <- B.unsignedBvAssignment a+ mb <- B.unsignedBvAssignment b++ -- Check model:+ assert (ma == 21) $ return ()+ assert (mb == 22) $ return ()++{- This example is from https://rise4fun.com/z3/tutorialcontent/guide#h23+ (declare-fun f (Int) Int)+ (declare-fun a () Int) ; a is a constant+ (declare-const b Int) ; syntax sugar for (declare-fun b () Int)+ (assert (> a 20))+ (assert (> b a))+ (assert (= (f 10) 1))+ (check-sat)+ (get-model)+-}