summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDeianStefan <>2018-06-19 04:46:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2018-06-19 04:46:00 (GMT)
commit8f3319cf747a8c006388ff53afc431cca048a8cc (patch)
tree48990a08d8bf606ec906661f6dc79aac43614547
version 0.0.0.10.0.0.1
-rw-r--r--LICENSE22
-rw-r--r--Setup.hs2
-rw-r--r--boolector.cabal72
-rw-r--r--src/Boolector.hs1076
-rw-r--r--src/Boolector/Foreign.chs762
-rw-r--r--test/API_Usage_Example.hs42
-rw-r--r--test/Arith_Example.hs90
-rw-r--r--test/Array_Example.hs36
-rw-r--r--test/UF_Example.hs51
9 files changed, 2153 insertions, 0 deletions
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..db6b8d0
--- /dev/null
+++ b/LICENSE
@@ -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.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
index 0000000..9a994af
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/boolector.cabal b/boolector.cabal
new file mode 100644
index 0000000..b800536
--- /dev/null
+++ b/boolector.cabal
@@ -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
diff --git a/src/Boolector.hs b/src/Boolector.hs
new file mode 100644
index 0000000..af35306
--- /dev/null
+++ b/src/Boolector.hs
@@ -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
diff --git a/src/Boolector/Foreign.chs b/src/Boolector/Foreign.chs
new file mode 100644
index 0000000..1c702a9
--- /dev/null
+++ b/src/Boolector/Foreign.chs
@@ -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' } -> `()' #}
diff --git a/test/API_Usage_Example.hs b/test/API_Usage_Example.hs
new file mode 100644
index 0000000..bffd007
--- /dev/null
+++ b/test/API_Usage_Example.hs
@@ -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 ()
diff --git a/test/Arith_Example.hs b/test/Arith_Example.hs
new file mode 100644
index 0000000..4fff224
--- /dev/null
+++ b/test/Arith_Example.hs
@@ -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)
+
+-}
diff --git a/test/Array_Example.hs b/test/Array_Example.hs
new file mode 100644
index 0000000..ab84699
--- /dev/null
+++ b/test/Array_Example.hs
@@ -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 ()
diff --git a/test/UF_Example.hs b/test/UF_Example.hs
new file mode 100644
index 0000000..fc9fabf
--- /dev/null
+++ b/test/UF_Example.hs
@@ -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)
+-}