{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-} {-| 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 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 . -} {-# 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 , repeat -- *** Bit-wise operations , xor , xnor , and , nand , or , nor , sll , srl , sra , rol , ror -- *** Arithmetic operations , add , inc , sub , dec , mul , udiv , sdiv , urem , srem , smod -- **** Overflow detection , uaddo , saddo , usubo , ssubo , umulo , smulo , sdivo -- *** Comparison operations , ult , slt , ulte , slte , ugt , sgt , ugte , sgte -- *** Array operations , read , write -- *** Function operations , apply -- ** Accessors , getSort , funGetDomainSort , funGetCodomainSort , funGetArity , getSymbol , setSymbol , getWidth , getIndexWidth , isConst , isVar , isArray , isArrayVar , isParam , isBoundParam , isUf , isFun -- ** Models , bvAssignment , unsignedBvAssignment , signedBvAssignment , boolAssignment -- ** Sorts , Sort , SortTy, sortTy , boolSort , bitvecSort , funSort , arraySort -- *** Accessors , isEqualSort , isArraySort , isBitvecSort , isFunSort , funSortCheck -- * Debug dumping , dump , dumpNode , dumpToString , dumpNodeToString , DumpFormat(..) ) where import Boolector.Foreign (Option(..), Status(..)) import qualified Boolector.Foreign as B import Data.Char (isDigit) import Data.Maybe (listToMaybe) 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.Applicative ((<$>)) import Control.Monad.State.Strict import Control.Exception hiding (assert) import Control.Concurrent import Prelude hiding (read, not, and, or, const, concat, repeat) 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 -> Word32 -> m () setOpt o w = liftBoolector2 B.setOpt o (fromIntegral w) -- | Get option. getOpt :: MonadBoolector m => Option -> m Word32 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 . _node -- | Add an assumption. assume :: MonadBoolector m => Node -> m () assume = liftBoolector1 B.assume . _node -- | Determine if assumption node is a failed assumption. failed :: MonadBoolector m => Node -> m Bool failed = liftBoolector1 B.failed . _node -- | 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 => Word32 -> m () push w = liftBoolector1 B.push (fromIntegral w) -- | Pop context levels. pop :: MonadBoolector m => Word32 -> 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 -- -- | Node data type wrapping the underlying Boolector node with a show string. data Node = Node { _node :: B.Node , _showNode :: String } deriving (Eq, Ord) instance Show Node where show = _showNode -- | 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 = mkNode "true" $ liftBoolector0 B.true -- | Create bit vector constant zero with bit width one. false :: MonadBoolector m => m Node false = mkNode "false" $ liftBoolector0 B.false -- | Create bit vector constant representing the bit vector @bits@. const :: MonadBoolector m => String -> m Node const str = mkNode ("0b" ++ str) $ liftBoolector1 B.const str -- | Create bit vector constant representing the decimal number @str@. constd :: MonadBoolector m => Sort -> String -> m Node constd srt str = mkNode str $ liftBoolector2 B.constd (_sort srt) str -- | Create bit vector constant representing the hexadecimal number @str@. consth :: MonadBoolector m => Sort -> String -> m Node consth srt str = mkNode ("0x" ++ str) $ liftBoolector2 B.consth (_sort srt) str -- | Create bit vector constant zero of sort @sort@. zero :: MonadBoolector m => Sort -> m Node zero = mkNode "zero" . liftBoolector1 B.zero . _sort -- | Create bit vector constant of sort @sort@, where each bit is set to one. ones :: MonadBoolector m => Sort -> m Node ones srt = mkNode onesStr $ liftBoolector1 B.one $ _sort srt where onesStr = "0b" ++ replicate nr '1' nr = case sortTy srt of BoolSort -> 1 BitVecSort wNr -> fromIntegral wNr _ -> error "invalid sort" -- | Create bit vector constant one of sort @sort@. one :: MonadBoolector m => Sort -> m Node one = mkNode "1" . liftBoolector1 B.one . _sort -- | 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 srt = constd srt (show i) -- | 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 srt = constd srt (show i) -- | Create a bit vector variable of sort @sort@. var :: MonadBoolector m => Sort -> String -> m Node var srt str = mkNamedNode "var" B.var srt str -- | Create the one's complement of bit vector @node@. not :: MonadBoolector m => Node -> m Node not n1 = mkNode ["not", show n1] $ liftBoolector1 B.not (_node n1) -- | Create the two's complement of bit vector @node@. neg :: MonadBoolector m => Node -> m Node neg n1 = mkNode ["neg", show n1] $ liftBoolector1 B.neg (_node n1) -- | Create *or* reduction of node @node@. -- -- All bits of node @node@ are combined by a Boolean *or*. redor :: MonadBoolector m => Node -> m Node redor n1 = mkNode ["redor", show n1] $ liftBoolector1 B.redor (_node n1) -- | Create *xor* reduction of node @node@. -- -- All bits of @node@ are combined by a Boolean *xor*. redxor :: MonadBoolector m => Node -> m Node redxor n1 = mkNode ["redxor", show n1] $ liftBoolector1 B.redxor (_node n1) -- | Create *and* reduction of node @node@. -- -- All bits of @node@ are combined by a Boolean *and*. redand :: MonadBoolector m => Node -> m Node redand n = mkNode ["redand", show n] $ liftBoolector1 B.redand (_node n) -- | Create a bit vector slice of @node@ from index @upper@ to index @lower@. slice :: MonadBoolector m => Node -- ^ Bit vector node. -> Word32 -- ^ Upper index which must be greater than or equal to zero, and less than the bit width of @node@. -> Word32 -- ^ Lower index which must be greater than or equal to zero, and less than or equal to @upper@. -> m Node slice n u l = mkNode ["slice", show n, show u, show l] $ liftBoolector3 B.slice (_node n) (fromIntegral u) (fromIntegral l) -- | Create unsigned extension. -- -- The bit vector @node@ is padded with @width@ * zeroes. uext :: MonadBoolector m => Node -> Word32 -> m Node uext n w = mkNode ["uext", show n, show w] $ liftBoolector2 B.uext (_node 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 -> Word32 -> m Node sext n w = mkNode ["sext", show n, show w] $ liftBoolector2 B.sext (_node n) (fromIntegral w) -- | Create the concatenation of two bit vectors. concat :: MonadBoolector m => Node -> Node -> m Node concat n1 n2 = mkNode ["concat", show n1, show n2] $ liftBoolector2 B.concat (_node n1) (_node n2) -- | Create @n@ concatenations of a given node @node@. repeat :: MonadBoolector m => Node -> Word32 -> m Node repeat n w = mkNode ["repeat", show n, show w] $ liftBoolector2 B.repeat (_node n) (fromIntegral w) -- | Create boolean implication. implies :: MonadBoolector m => Node -> Node -> m Node implies n1 n2 = mkNode ["implies", show n1, show n2] $ liftBoolector2 B.implies (_node n1) (_node n2) -- | Create Boolean equivalence. iff :: MonadBoolector m => Node -> Node -> m Node iff n1 n2 = mkNode ["iff", show n1, show n2] $ liftBoolector2 B.iff (_node n1) (_node n2) -- | 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 n1 n2 = mkNode ["eq", show n1, show n2] $ liftBoolector2 B.eq (_node n1) (_node n2) -- | 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 n1 n2 = mkNode ["ne", show n1, show n2] $ liftBoolector2 B.ne (_node n1) (_node n2) -- | 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 n1 n2 n3 = mkNode ["cond", show n1, show n2, show n3] $ liftBoolector3 B.cond (_node n1) (_node n2) (_node n3) -- -- Bit-wise operations. -- -- | Create a bit vector *xor*. xor :: MonadBoolector m => Node -> Node -> m Node xor n1 n2 = mkNode ["xor", show n1, show n2] $ liftBoolector2 B.xor (_node n1) (_node n2) -- | Create a bit vector *xnor*. xnor :: MonadBoolector m => Node -> Node -> m Node xnor n1 n2 = mkNode ["xnor", show n1, show n2] $ liftBoolector2 B.xnor (_node n1) (_node n2) -- | Create a bit vector *and*. and :: MonadBoolector m => Node -> Node -> m Node and n1 n2 = mkNode ["and", show n1, show n2] $ liftBoolector2 B.and (_node n1) (_node n2) -- | Create a bit vector *nand*. nand :: MonadBoolector m => Node -> Node -> m Node nand n1 n2 = mkNode ["nand", show n1, show n2] $ liftBoolector2 B.nand (_node n1) (_node n2) -- | Create a bit vector *or*. or :: MonadBoolector m => Node -> Node -> m Node or n1 n2 = mkNode ["or", show n1, show n2] $ liftBoolector2 B.or (_node n1) (_node n2) -- | Create a bit vector *nor*. nor :: MonadBoolector m => Node -> Node -> m Node nor n1 n2 = mkNode ["nor", show n1, show n2] $ liftBoolector2 B.nor (_node n1) (_node n2) -- | 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 n1 n2 = mkNode ["sll", show n1, show n2] $ liftBoolector2 B.sll (_node n1) (_node n2) -- | 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 n1 n2 = mkNode ["srl", show n1, show n2] $ liftBoolector2 B.srl (_node n1) (_node n2) -- | 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 n1 n2 = mkNode ["sra", show n1, show n2] $ liftBoolector2 B.sra (_node n1) (_node n2) -- | 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 n1 n2 = mkNode ["rol", show n1, show n2] $ liftBoolector2 B.rol (_node n1) (_node n2) -- | 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 n1 n2 = mkNode ["ror", show n1, show n2] $ liftBoolector2 B.ror (_node n1) (_node n2) -- -- Arithmetic operations. -- -- | Create bit vector addition. add :: MonadBoolector m => Node -> Node -> m Node add n1 n2 = mkNode ["add", show n1, show n2] $ liftBoolector2 B.add (_node n1) (_node n2) -- | Create bit vector expression that increments bit vector @node@ by one. inc :: Node -> Boolector Node inc n = mkNode ["inc", show n] $ liftBoolector1 B.inc (_node n) -- | Create a bit vector subtraction. sub :: MonadBoolector m => Node -> Node -> m Node sub n1 n2 = mkNode ["sub", show n1, show n2] $ liftBoolector2 B.sub (_node n1) (_node n2) -- | Create bit vector expression that decrements bit vector @node@ by one. dec :: MonadBoolector m => Node -> m Node dec n = mkNode ["dec", show n] $ liftBoolector1 B.dec (_node n) -- | Create a bitvector multiplication. mul :: MonadBoolector m => Node -> Node -> m Node mul n1 n2 = mkNode ["mul", show n1, show n2] $ liftBoolector2 B.mul (_node n1) (_node n2) -- | Create unsigned division. udiv :: MonadBoolector m => Node -> Node -> m Node udiv n1 n2 = mkNode ["udiv", show n1, show n2] $ liftBoolector2 B.udiv (_node n1) (_node n2) -- | Create signed division. sdiv :: MonadBoolector m => Node -> Node -> m Node sdiv n1 n2 = mkNode ["sdiv", show n1, show n2] $ liftBoolector2 B.sdiv (_node n1) (_node n2) -- | Create an unsigned remainder. urem :: MonadBoolector m => Node -> Node -> m Node urem n1 n2 = mkNode ["urem", show n1, show n2] $ liftBoolector2 B.urem (_node n1) (_node n2) -- | Create a signed remainder. srem :: MonadBoolector m => Node -> Node -> m Node srem n1 n2 = mkNode ["srem", show n1, show n2] $ liftBoolector2 B.srem (_node n1) (_node n2) -- | Create a, signed remainder where its sign matches the sign of the divisor. smod :: MonadBoolector m => Node -> Node -> m Node smod n1 n2 = mkNode ["smod", show n1, show n2] $ liftBoolector2 B.smod (_node n1) (_node n2) -- -- Overflow detection -- -- | Create an unsigned bit vector subtraction overflow detection. -- Returns bit vector with bit-width one, which indicates if the operation -- overflows. usubo :: MonadBoolector m => Node -> Node -> m Node usubo n1 n2 = mkNode ["usubo", show n1, show n2] $ liftBoolector2 B.usubo (_node n1) (_node n2) -- | Create a signed bit vector subtraction overflow detection. -- Returns bit vector with bit-width one, which indicates if the operation -- overflows. ssubo :: MonadBoolector m => Node -> Node -> m Node ssubo n1 n2 = mkNode ["ssubo", show n1, show n2] $ liftBoolector2 B.ssubo (_node n1) (_node n2) -- | Create an unsigned bit vector addition overflow detection. -- Returns bit vector with bit-width one, which indicates if the operation -- overflows. uaddo :: MonadBoolector m => Node -> Node -> m Node uaddo n1 n2 = mkNode ["uaddo", show n1, show n2] $ liftBoolector2 B.uaddo (_node n1) (_node n2) -- | Create a signed bit vector addition overflow detection. -- Returns bit vector with bit-width one, which indicates if the operation -- overflows. saddo :: MonadBoolector m => Node -> Node -> m Node saddo n1 n2 = mkNode ["saddo", show n1, show n2] $ liftBoolector2 B.saddo (_node n1) (_node n2) -- | Create an unsigned bit vector multiplication overflow detection. -- Returns bit vector with bit-width one, which indicates if the operation -- overflows. umulo :: MonadBoolector m => Node -> Node -> m Node umulo n1 n2 = mkNode ["umulo", show n1, show n2] $ liftBoolector2 B.umulo (_node n1) (_node n2) -- | Create signed multiplication overflow detection. -- Returns bit vector with bit-width one, which indicates if the operation -- overflows. smulo :: MonadBoolector m => Node -> Node -> m Node smulo n1 n2 = mkNode ["smulo", show n1, show n2] $ liftBoolector2 B.smulo (_node n1) (_node n2) -- | Create a signed bit vector division overflow detection. -- Returns bit vector with bit-width one, which indicates if the operation -- overflows. sdivo :: MonadBoolector m => Node -> Node -> m Node sdivo n1 n2 = mkNode ["sdivo", show n1, show n2] $ liftBoolector2 B.sdivo (_node n1) (_node n2) -- -- Comparison operations. -- -- | Create an unsigned less than. ult :: MonadBoolector m => Node -> Node -> m Node ult n1 n2 = mkNode ["ult", show n1, show n2] $ liftBoolector2 B.ult (_node n1) (_node n2) -- | Create a signed less than. slt :: MonadBoolector m => Node -> Node -> m Node slt n1 n2 = mkNode ["slt", show n1, show n2] $ liftBoolector2 B.slt (_node n1) (_node n2) -- | Create an unsigned less than or equal. ulte :: MonadBoolector m => Node -> Node -> m Node ulte n1 n2 = mkNode ["ulte", show n1, show n2] $ liftBoolector2 B.ulte (_node n1) (_node n2) -- | Create a signed less than or equal. slte :: MonadBoolector m => Node -> Node -> m Node slte n1 n2 = mkNode ["slte", show n1, show n2] $ liftBoolector2 B.slte (_node n1) (_node n2) -- | Create an unsigned greater than. ugt :: MonadBoolector m => Node -> Node -> m Node ugt n1 n2 = mkNode ["ugt", show n1, show n2] $ liftBoolector2 B.ugt (_node n1) (_node n2) -- | Create a signed greater than. sgt :: MonadBoolector m => Node -> Node -> m Node sgt n1 n2 = mkNode ["sgt", show n1, show n2] $ liftBoolector2 B.sgt (_node n1) (_node n2) -- | Create an unsigned greater than or equal. ugte :: MonadBoolector m => Node -> Node -> m Node ugte n1 n2 = mkNode ["ugte", show n1, show n2] $ liftBoolector2 B.ugte (_node n1) (_node n2) -- | Create a signed greater than or equal. sgte :: MonadBoolector m => Node -> Node -> m Node sgte n1 n2 = mkNode ["sgte", show n1, show n2] $ liftBoolector2 B.sgte (_node n1) (_node n2) -- -- 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 srt str = mkNamedNode "array" B.array srt str -- | 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 n1 n2 = mkNode ["read", show n1, show n2] $ liftBoolector2 B.read (_node n1) (_node n2) -- | 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 n1 n2 n3 = mkNode ["write", show n1, show n2, show n3] $ liftBoolector3 B.write (_node n1) (_node n2) (_node n3) -- -- Functions -- -- | Create an uninterpreted function with sort @sort@. -- -- The name must be unique. uf :: MonadBoolector m => Sort -> String -> m Node uf srt str = mkNamedNode "uf" B.uf srt str -- | 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 srt str = mkNode ["param", show srt, str] $ liftBoolector2 B.param (_sort srt) str -- | 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 n1 n2 = mkNode ["fun", show n1, show n2] $ liftBoolector2 B.fun (map _node n1) (_node n2) -- | 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 n1 n2 = mkNode ["apply", show n1, show n2] $ liftBoolector2 B.apply (map _node n1) (_node n2) -- -- Quantified terms -- -- | Create a universally quantified term. forall :: MonadBoolector m => [Node] -- ^ Quantified variables (create with 'param') -> Node -- ^ Term where variables may occur. (Cannot contain functions.) -> m Node forall n1 n2 = mkNode ["forall", show n1, show n2] $ liftBoolector2 B.forall (map _node n1) (_node n2) -- | Create an existentially quantifed term. exists :: MonadBoolector m => [Node] -- ^ Quantified variables (create with 'param') -> Node -- ^ Term where variables may occur. (Cannot contain functions.) -> m Node exists n1 n2 = mkNode ["exists", show n1, show n2] $ liftBoolector2 B.exists (map _node n1) (_node n2) -- -- Accessors -- -- | Get the sort of given @node@. The result does not have to be released. getSort :: MonadBoolector m => Node -> m Sort getSort n = liftBoolector1 B.getSort (_node n) >>= lookupSort -- | Get the domain sort of given function node @node@. -- -- The result does not have to be released. funGetDomainSort :: MonadBoolector m => Node -> m Sort funGetDomainSort n = liftBoolector1 B.funGetDomainSort (_node n) >>= lookupSort -- | Get the codomain sort of given function node @node@. -- -- The result does not have to be released. funGetCodomainSort :: MonadBoolector m => Node -> m Sort funGetCodomainSort n = liftBoolector1 B.funGetCodomainSort (_node n) >>= lookupSort -- | Get the arity of function node. funGetArity :: MonadBoolector m => Node -> m Word funGetArity n = fromIntegral `liftM` liftBoolector1 B.getFunArity (_node n) -- | Get the symbol of an expression. getSymbol :: MonadBoolector m => Node -> m (Maybe String) getSymbol = liftBoolector1 B.getSymbol . _node -- | Set the symbol of an expression. setSymbol :: MonadBoolector m => Node -> String -> m () setSymbol n str = liftBoolector2 B.setSymbol (_node n) str -- | 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 Word32 getWidth n = fromIntegral `liftM` liftBoolector1 B.getWidth (_node n) -- | Get the bit width of indices of @n_array@. getIndexWidth :: MonadBoolector m => Node -> m Word32 getIndexWidth n = fromIntegral `liftM` liftBoolector1 B.getIndexWidth (_node n) -- | Determine if given node is a constant node. isConst :: MonadBoolector m => Node -> m Bool isConst = liftBoolector1 B.isConst . _node -- | Determine if given node is a bit vector variable. isVar :: MonadBoolector m => Node -> m Bool isVar = liftBoolector1 B.isVar . _node -- | Determine if given node is an array node. isArray :: MonadBoolector m => Node -> m Bool isArray = liftBoolector1 B.isArray . _node -- | Determine if given node is an array node. isArrayVar :: MonadBoolector m => Node -> m Bool isArrayVar = liftBoolector1 B.isArrayVar . _node -- | Determine if given node is a parameter node. isParam :: MonadBoolector m => Node -> m Bool isParam = liftBoolector1 B.isParam . _node -- | Determine if given parameter node is bound by a function. isBoundParam :: MonadBoolector m => Node -> m Bool isBoundParam = liftBoolector1 B.isBoundParam . _node -- | Determine if given node is an uninterpreted function node. isUf :: MonadBoolector m => Node -> m Bool isUf = liftBoolector1 B.isUf . _node -- | Determine if given node is a function node. isFun :: MonadBoolector m => Node -> m Bool isFun = liftBoolector1 B.isFun . _node -- -- 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 . _node -- | 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 -- -- | Type of sorts, used to keep track of sorts without having to go back into C-land. data SortTy = BoolSort | BitVecSort Word | FunSort [SortTy] SortTy | ArraySort SortTy SortTy deriving (Eq, Ord, Show) -- | Sort wraps the udnerlying Boolector sort with a showable type. data Sort = Sort { sortTy :: SortTy -- ^ Get sort type , _sort :: B.Sort } deriving (Eq, Ord) instance Show Sort where show = show . sortTy -- | Create Boolean sort. boolSort :: Boolector Sort boolSort = do sc <- getSortCache case scBool sc of Just srt -> return srt _ -> do srt <- Sort BoolSort <$> 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 <- Sort (BitVecSort nr) <$> 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 <- Sort (FunSort (map sortTy args) (sortTy ret)) <$> liftBoolector2 B.funSort (map _sort args) (_sort 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 <- Sort (ArraySort (sortTy dom) (sortTy rng)) <$> liftBoolector2 B.arraySort (_sort dom) (_sort 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 n1 n2 = liftBoolector2 B.isEqualSort (_node n1) (_node n2) -- | Determine if @sort@ is an array sort. isArraySort :: Sort -> Bool isArraySort srt = case sortTy srt of ArraySort _ _ -> True _ -> False -- | Determine if @sort@ is a bit-vector sort. isBitvecSort :: Sort -> Bool isBitvecSort srt = case sortTy srt of BitVecSort _ -> True _ -> False -- | Determine if @sort@ is a function sort. isFunSort :: Sort -> Bool isFunSort srt = case sortTy srt of FunSort _ _ -> True _ -> False -- | 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 n1 n2 = liftBoolector2 B.funSortCheck (map _node n1) (_node n2) -- -- Dumping -- -- | Output dump format. data DumpFormat = DumpBtor | DumpSMT2 deriving (Eq, Show) -- | Recursively dump @node@ to file in BTOR or SMT-LIB v2 format. dumpNode :: MonadBoolector m => DumpFormat -> FilePath -> Node -> m () dumpNode fmt path node = do btor <- unBoolectorState `liftM` getBoolectorState liftIO $ B.withDumpFile path $ \file -> dumper btor file (_node node) where dumper = case fmt of DumpBtor -> B.dumpBtorNode _ -> B.dumpSmt2Node -- | Dump formula to file in BTOR or SMT-LIB v2 format. dump :: MonadBoolector m => DumpFormat -> FilePath -> m () dump fmt path = do btor <- unBoolectorState `liftM` getBoolectorState liftIO $ B.withDumpFile path (dumper btor) where dumper = case fmt of DumpBtor -> B.dumpBtor _ -> B.dumpSmt2 -- | Same as 'dumpNode', but returns string. -- TODO: this is super slow, we should request feature from boolector. dumpNodeToString :: MonadBoolector m => DumpFormat -> Node -> m String dumpNodeToString fmt node = do btor <- unBoolectorState `liftM` getBoolectorState liftIO $ B.withTempDumpFile (\file -> dumper btor file (_node node)) where dumper = case fmt of DumpBtor -> B.dumpBtorNode _ -> B.dumpSmt2Node -- | Same as 'dump', but returns string. -- TODO: this is super slow, we should request feature from boolector. dumpToString :: MonadBoolector m => DumpFormat -> m String dumpToString fmt = do btor <- unBoolectorState `liftM` getBoolectorState liftIO $ B.withTempDumpFile (dumper btor) where dumper = case fmt of DumpBtor -> B.dumpBtor _ -> B.dumpSmt2 -- -- 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 } } -- -- Internal helpers -- -- | Class used to create nodes from boolector nodes, given a stringification class Show s => MkNode s where mkNode :: MonadBoolector m => s -> m B.Node -> m Node instance MkNode String where mkNode str act = do node <- act return $ Node node str instance MkNode [String] where mkNode str act = do node <- act return $ Node node $ "(" ++ unwords str ++ ")" -- | Create a new named node given a constructor or return it from variable -- cache. The name must be unique. mkNamedNode :: MonadBoolector m => String -- ^ Kind of node -> (B.Btor -> B.Sort -> String -> IO B.Node) -- ^ Underlying constructor -> Sort -- ^ Sort of node -> String -- ^ Name of node -> m Node mkNamedNode kind ctor sort name = do vc <- getVarCache case Map.lookup (name, sort) vc of Just srt -> return srt _ -> do node <- mkNode [kind, name, "::", show sort] $ liftBoolector2 ctor (_sort sort) name setVarCache $ Map.insert (name, sort) node vc return node -- | Get the high level sort from cache that corresponds to boolector sort lookupSort :: MonadBoolector m => B.Sort -> m Sort lookupSort bSort = do sc <- getSortCache case () of _ | Just srt <- lookupBoolSort sc -> return srt _ | Just srt <- lookupBitVecSort sc -> return srt _ | Just srt <- lookupFunSort sc -> return srt _ | Just srt <- lookupArraySort sc -> return srt _ -> fail "BUG: should really have the sort in the cache" where lookupBoolSort sc = case scBool sc of Just srt | _sort srt == bSort -> Just srt _ -> Nothing lookupBitVecSort sc = listToMaybe $ IntMap.elems $ IntMap.filter (\s -> _sort s == bSort) $ scBitVec sc lookupFunSort sc = listToMaybe $ Map.elems $ Map.filter (\s -> _sort s == bSort) $ scFun sc lookupArraySort sc = listToMaybe $ Map.elems $ Map.filter (\s -> _sort s == bSort) $ scArray sc