z3 4.1.0 → 4.1.1
raw patch · 15 files changed
+1353/−264 lines, 15 filesdep ~z3
Dependency ranges changed: z3
Files
- CHANGES.md +11/−0
- README.md +1/−2
- examples/Example/Monad/DataTypes.hs +91/−0
- examples/Example/Monad/FuncModel.hs +89/−0
- examples/Example/Monad/Interpolation.hs +35/−0
- examples/Example/Monad/MutuallyRecursive.hs +85/−0
- examples/Example/Monad/Queens4.hs +53/−0
- examples/Example/Monad/Queens4All.hs +77/−0
- examples/Example/Monad/ToSMTLib.hs +51/−0
- examples/Example/Monad/Tuple.hs +30/−0
- examples/Examples.hs +8/−0
- src/Z3/Base.hs +331/−38
- src/Z3/Base/C.hsc +341/−216
- src/Z3/Monad.hs +137/−4
- z3.cabal +13/−4
CHANGES.md view
@@ -1,6 +1,17 @@ # Release Notes +## 4.1.1++Another small release, made possible thanks to third-party contributions.++* Added bindings for getting the accessors of datatype constructors. (William Hallahan)+* Added bindings for declaring mutually recursive datatypes. (William Hallahan)+* Added partial support for the _Interpolation_ API. (Jakub Daniel)+* Added bindings for deconstructing function applications. (Jakub Daniel)+* Added bindings for ```simplify``` and ```simplifyEx```. (Gleb Popov)+* Some code cleanup. (Jakub Daniel and Iago Abal)+ ## 4.1.0 Small maintenance release that however introduces one API breaking change.
README.md view
@@ -72,9 +72,8 @@ In order to run this SMT script: main :: IO ()- main = evalZ3With Nothing opts script >>= \mbSol ->+ main = evalZ3 script >>= \mbSol -> case mbSol of Nothing -> error "No solution found." Just sol -> putStr "Solution: " >> print sol- where opts = opt "MODEL" True +? opt "MODEL_COMPLETION" True
+ examples/Example/Monad/DataTypes.hs view
@@ -0,0 +1,91 @@+{-# LANGUAGE ScopedTypeVariables #-}++module Example.Monad.DataTypes where++import Z3.Monad+import Control.Monad.Trans (liftIO)++run :: IO ()+run = evalZ3 datatypeScript++mkCellDatatype :: Z3 Sort+mkCellDatatype = do+ -- Create a cell data type of the form:+ -- data Cell = Nil | Cons {car :: Cell, cdr :: Cell}++ -- Nil constructor+ nil <- mkStringSymbol "Nil"+ isNil <- mkStringSymbol "is_Nil"+ nilConst <- mkConstructor nil isNil []++ -- Cons constructor+ car <- mkStringSymbol "car"+ cdr <- mkStringSymbol "cdr"+ cons <- mkStringSymbol "Cons"+ isCons <- mkStringSymbol "is_Cons"+ -- In the following, car and cdr are the field names. The second argument,+ -- their sort, is Nothing, since this is a recursive sort. The third argument is+ -- 0, since the type is not mutually recursive.+ consConst <- mkConstructor cons isCons [(car,Nothing,0),(cdr,Nothing,0)]++ -- Cell datatype+ cell <- mkStringSymbol "Cell"+ mkDatatype cell [nilConst, consConst]++datatypeScript :: Z3 ()+datatypeScript = do+ cell <- mkCellDatatype+ liftIO $ putStrLn "Cell constructors are:"+ [nilConst, consConst] <- getDatatypeSortConstructors cell+ mapM_ (\c -> getDeclName c >>= getSymbolString >>= liftIO . putStrLn) [nilConst, consConst]++ nil <- mkApp nilConst []+ -- t1 = Cons (Nil,Nil)+ t1 <- mkApp consConst [nil, nil]++ liftIO $ putStrLn "prove (nil != cons (nil,nil)) //Expect Unsat"+ p <- (mkEq nil t1 >>= mkNot)+ push+ mkNot p >>= assert+ check >>= liftIO . print+ pop 1++ liftIO $ putStrLn "prove (cons (x,u) = cons(y,v) => x = y && u = v) //Expect Unsat"+ [u,v,x,y] <- mapM (flip mkFreshConst cell) ["u","v","x","y"]+ t1 <- mkApp consConst [x,u]+ t2 <- mkApp consConst [y,v]+ p1 <- mkEq t1 t2+ p2 <- mkEq x y+ p3 <- mkEq u v+ p4 <- mkAnd [p2, p3]+ p5 <- mkImplies p1 p4+ push+ mkNot p5 >>= assert+ check >>= liftIO . print+ pop 1++ liftIO $ putStrLn "we expect a = cons(x, cons(y, nil)), x = y != Nil"++ [isNil, isCons] <- getDatatypeSortRecognizers cell+ [[], [car, cdr]] <- getDatatypeSortConstructorAccessors cell++ a <- mkFreshConst "a" cell+ b <- mkApp cdr [a]+ c <- mkApp cdr [b]++ carA <- mkApp car [a]+ carB <- mkApp car [b]++ push+ mkApp isCons [a] >>= assert+ mkApp isCons [b] >>= assert+ mkApp isNil [c] >>= assert++ mkApp isCons [carA] >>= assert+ mkEq carA carB >>= assert++ (ch, m) <- getModel++ case m of Just m' -> showModel m' >>= liftIO . putStrLn+ otherwise -> liftIO . print $ ch+ pop 1
+ examples/Example/Monad/FuncModel.hs view
@@ -0,0 +1,89 @@+-- | Extracting function and array interpretations.+module Example.Monad.FuncModel+ ( run )+ where++import Z3.Monad++run :: IO ()+run =+ do evalZ3 arrayScript >>= print+ evalZ3 funcScript >>= print++type RetType = ([([Integer], Integer)], Integer)++toIntsPair :: ([AST], AST) -> Z3 ([Integer], Integer)+toIntsPair (is, i) =+ do is' <- mapM getInt is+ i' <- getInt i+ return (is', i')++toRetType :: FuncModel -> Z3 RetType+toRetType (FuncModel fs elsePart) =+ do fs' <- mapM toIntsPair fs+ elsePart' <- getInt elsePart+ return (fs', elsePart')++-- * Arrays++-- FIXME: This script crashes when calling 'convertArr', which mysteriously now+-- returns 'Nothing'. It seems that 'isAsArray' is returning 'False' for 'a1'.+arrayScript :: Z3 (RetType, RetType)+arrayScript =+ do intSort <- mkIntSort+ arrSort <- mkArraySort intSort intSort++ a1Sym <- mkStringSymbol "a1"+ a2Sym <- mkStringSymbol "a2"++ a1 <- mkConst a1Sym arrSort+ a2 <- mkConst a2Sym arrSort+++ i1 <- mkIntNum (5 :: Int)+ i2 <- mkIntNum (10 :: Int)+ a1Val1 <- mkSelect a1 i1+ mkGt a1Val1 i2 >>= assert++ i3 <- mkIntNum (42 :: Int)+ i4 <- mkIntNum (81 :: Int)+ a3 <- mkStore a1 i3 i4+ mkEq a2 a3 >>= assert++ let+ convertArr :: Model -> AST -> Z3 RetType+ convertArr model arr =+ do Just f <- evalArray model arr+ toRetType f++ (_res, modelMb) <- getModel+ case modelMb of+ Just model ->+ do a1' <- convertArr model a1+ a2' <- convertArr model a2+ return (a1', a2')+ Nothing -> error "Couldn't construct model"++-- * Functions++funcScript :: Z3 RetType+funcScript = do+ -- f :: (Integer,Integer) -> Integer+ intSort <- mkIntSort+ fDecl <- mkFreshFuncDecl "f" [intSort, intSort] intSort++ -- f(5,10) > 42+ i5 <- mkIntNum (5 :: Integer)+ i10 <- mkIntNum (10 :: Integer)+ i42 <- mkIntNum (42 :: Integer)+ r <- mkApp fDecl [i5, i10]+ assert =<< mkGt r i42++ -- check satisfiability and obtain model+ (res, mbModel) <- getModel+ case mbModel of+ Just model -> do+ Just f <- evalFunc model fDecl+ toRetType f+ Nothing -> error ("Couldn't construct model: " ++ show res)+
+ examples/Example/Monad/Interpolation.hs view
@@ -0,0 +1,35 @@+-- | Compute interpolant for an unsatisfiable conjunction of formulas+module Example.Monad.Interpolation+ ( run )+ where++import Control.Monad+import Control.Monad.Trans ( liftIO )++import Z3.Monad++run :: IO ()+run = do+ env <- newItpEnv Nothing stdOpts+ evalZ3WithEnv z3 env++z3 = do+ a <- mkFreshBoolVar "a"+ b <- mkFreshBoolVar "b"++ na <- mkNot a+ nb <- mkNot b++ f1 <- mkIff a b+ f2 <- mkIff a nb++ g1 <- mkInterpolant f1+ g2 <- mkInterpolant f2+ g3 <- mkInterpolant =<< mkTrue++ params <- mkParams+ res <- flip computeInterpolant params =<< mkAnd [g1, g2, g3]++ case res of+ Just (Right itps) -> mapM_ (liftIO . putStrLn <=< astToString) itps+ otherwise -> error "could not compute interpolants"
+ examples/Example/Monad/MutuallyRecursive.hs view
@@ -0,0 +1,85 @@+{-# LANGUAGE ScopedTypeVariables #-}++module Example.Monad.MutuallyRecursive where++import Z3.Monad+import Control.Monad.Trans (liftIO)++run :: IO ()+run = evalZ3 datatypeScript++mkForestTreeDatatypes :: Z3 [Sort]+mkForestTreeDatatypes = do+ -- Creates forest and tree data types of the form:+ -- data Forest = NilF | ConsF {carF :: Tree, cdrF :: Forest}+ -- data Tree = NilT | ConsT {carT :: Forest, cdrT :: Forest}++ -- Nil constructors+ nilF <- mkStringSymbol "NilF"+ isNilF <- mkStringSymbol "is_NilF"+ nilFConst <- mkConstructor nilF isNilF []++ nilT <- mkStringSymbol "NilT"+ isNilT <- mkStringSymbol "is_NilT"+ nilTConst <- mkConstructor nilT isNilT []++ -- Cons constructors+ carF <- mkStringSymbol "carF"+ cdrF <- mkStringSymbol "cdrF"+ consF <- mkStringSymbol "ConsF"+ isConsF <- mkStringSymbol "is_ConsF"++ carT <- mkStringSymbol "carT"+ cdrT <- mkStringSymbol "cdrT"+ consT <- mkStringSymbol "ConsT"+ isConsT <- mkStringSymbol "is_ConsT"++ -- In the following, carT, cdrT, carF, and carT are the field names. The second argument,+ -- their sort, is Nothing, since this is a recursive sort. When we put these in one list+ -- (below) the third argument determines which type they refer to.+ consFConst <- mkConstructor consF isConsF [(carF,Nothing,1),(cdrF,Nothing,0)]+ consTConst <- mkConstructor consT isConsT [(carT,Nothing,0),(cdrT,Nothing,0)]+++ -- datatypes (might not need sort list...)+ forest <- mkStringSymbol "Forest"+ tree <- mkStringSymbol "Tree"++ let forestList = [nilFConst, consFConst]+ let treeList = [nilTConst, consTConst]++ mkDatatypes [forest, tree] [forestList, treeList]++datatypeScript :: Z3 ()+datatypeScript = do+ [forest, tree] <- mkForestTreeDatatypes++ [nilF, consF] <- getDatatypeSortConstructors forest+ [nilT, consT] <- getDatatypeSortConstructors tree++ nilF' <- mkApp nilF []++ t1 <- mkApp consT [nilF', nilF']+ f1 <- mkApp consF [t1, nilF']++ liftIO $ putStrLn "prove (NilF != ConsF(ConsT(NilT, NilT), NilF)) //Expect Unsat"+ p <- (mkEq nilF' f1 >>= mkNot)+ push+ mkNot p >>= assert+ check >>= liftIO . print+ pop 1++ liftIO $ putStrLn "prove (consF (x,u) = consF(y,v) => x = y && u = v) //Expect Unsat"+ [x,y] <- mapM (flip mkFreshConst tree) ["x","y"]+ [u,v] <- mapM (flip mkFreshConst forest) ["u","v"]+ f1 <- mkApp consF [x, u]+ f2 <- mkApp consF [y, v]+ p1 <- mkEq f1 f2+ p2 <- mkEq x y+ p3 <- mkEq u v+ p4 <- mkAnd [p2, p3]+ p5 <- mkImplies p1 p4+ push+ mkNot p5 >>= assert+ check >>= liftIO . print+ pop 1
+ examples/Example/Monad/Queens4.hs view
@@ -0,0 +1,53 @@+-- | The 4-queens puzzle.+module Example.Monad.Queens4+ ( run )+ where++import Control.Applicative+import Control.Monad ( join )+import Data.Maybe+import qualified Data.Traversable as T++import Z3.Monad++run :: IO ()+run = evalZ3 script >>= \mbSol ->+ case mbSol of+ Nothing -> error "No solution found."+ Just sol -> putStr "Solution: " >> print sol++script :: Z3 (Maybe [Integer])+script = do+ q1 <- mkFreshIntVar "q1"+ q2 <- mkFreshIntVar "q2"+ q3 <- mkFreshIntVar "q3"+ q4 <- mkFreshIntVar "q4"+ _1 <- mkInteger 1+ _4 <- mkInteger 4+ -- the ith-queen is in the ith-row.+ -- qi is the column of the ith-queen+ assert =<< mkAnd =<< T.sequence+ [ mkLe _1 q1, mkLe q1 _4 -- 1 <= q1 <= 4+ , mkLe _1 q2, mkLe q2 _4+ , mkLe _1 q3, mkLe q3 _4+ , mkLe _1 q4, mkLe q4 _4+ ]+ -- different columns+ assert =<< mkDistinct [q1,q2,q3,q4]+ -- avoid diagonal attacks+ assert =<< mkNot =<< mkOr =<< T.sequence+ [ diagonal 1 q1 q2 -- diagonal line of attack between q1 and q2+ , diagonal 2 q1 q3+ , diagonal 3 q1 q4+ , diagonal 1 q2 q3+ , diagonal 2 q2 q4+ , diagonal 1 q3 q4+ ]+ -- check and get solution+ fmap snd $ withModel $ \m ->+ catMaybes <$> mapM (evalInt m) [q1,q2,q3,q4]+ where mkAbs x = do+ _0 <- mkInteger 0+ join $ mkIte <$> mkLe _0 x <*> pure x <*> mkUnaryMinus x+ diagonal d c c' =+ join $ mkEq <$> (mkAbs =<< mkSub [c',c]) <*> (mkInteger d)
+ examples/Example/Monad/Queens4All.hs view
@@ -0,0 +1,77 @@+-- | All the solutions of the 4-queens puzzle.+module Example.Monad.Queens4All+ ( run )+ where++import Control.Applicative+import Control.Monad ( join )+import Data.Maybe+import qualified Data.Traversable as T++import Z3.Monad++run :: IO ()+run = do+ sols <- evalZ3 script+ putStrLn "Solutions: "+ mapM_ print sols+++type Solution = [Integer]++getSolutions :: AST -> AST -> AST -> AST -> Z3 [Solution]+getSolutions q1 q2 q3 q4 = go []+ where go acc = do+ mb_sol <- getSolution+ case mb_sol of+ Nothing -> return acc+ Just sol -> do restrictSolution sol+ go (sol:acc)+ restrictSolution :: Solution -> Z3 ()+ restrictSolution [c1,c2,c3,c4] =+ assert =<< mkNot =<< mkOr =<< T.sequence+ [ mkEq q1 =<< mkIntNum c1+ , mkEq q2 =<< mkIntNum c2+ , mkEq q3 =<< mkIntNum c3+ , mkEq q4 =<< mkIntNum c4+ ]+ restrictSolution _____________ = error "invalid argument"+ getSolution :: Z3 (Maybe Solution)+ getSolution = fmap snd $ withModel $ \m ->+ catMaybes <$> mapM (evalInt m) [q1,q2,q3,q4]++script :: Z3 [Solution]+script = do+ q1 <- mkFreshIntVar "q1"+ q2 <- mkFreshIntVar "q2"+ q3 <- mkFreshIntVar "q3"+ q4 <- mkFreshIntVar "q4"+ _1 <- mkIntNum (1::Integer)+ _4 <- mkIntNum (4::Integer)+ -- the ith-queen is in the ith-row.+ -- qi is the column of the ith-queen+ assert =<< mkAnd =<< T.sequence+ [ mkLe _1 q1, mkLe q1 _4 -- 1 <= q1 <= 4+ , mkLe _1 q2, mkLe q2 _4+ , mkLe _1 q3, mkLe q3 _4+ , mkLe _1 q4, mkLe q4 _4+ ]+ -- different columns+ assert =<< mkDistinct [q1,q2,q3,q4]+ -- avoid diagonal attacks+ assert =<< mkNot =<< mkOr =<< T.sequence+ [ diagonal 1 q1 q2 -- diagonal line of attack between q1 and q2+ , diagonal 2 q1 q3+ , diagonal 3 q1 q4+ , diagonal 1 q2 q3+ , diagonal 2 q2 q4+ , diagonal 1 q3 q4+ ]+ getSolutions q1 q2 q3 q4+ where mkAbs :: AST -> Z3 AST+ mkAbs x = do+ _0 <- mkIntNum (0::Integer)+ join $ mkIte <$> mkLe _0 x <*> pure x <*> mkUnaryMinus x+ diagonal :: Integer -> AST -> AST -> Z3 AST+ diagonal d c c' =+ join $ mkEq <$> (mkAbs =<< mkSub [c',c]) <*> (mkIntNum d)
+ examples/Example/Monad/ToSMTLib.hs view
@@ -0,0 +1,51 @@+-- | Generate SMTLib.+module Example.Monad.ToSMTLib+ ( run )+ where++import Control.Applicative+import Control.Monad ( join )+import Control.Monad.Trans+import Data.Maybe+import qualified Data.Traversable as T++import Z3.Monad++run :: IO ()+run = evalZ3 script >>= putStrLn++script :: Z3 String+script = do+ intSort <- mkIntSort+ q1 <- flip mkConst intSort =<< mkStringSymbol "q1"+ q2 <- flip mkConst intSort =<< mkStringSymbol "q2"+ q3 <- flip mkConst intSort =<< mkStringSymbol "q3"+ q4 <- flip mkConst intSort =<< mkStringSymbol "q4"+ _1 <- mkIntNum (1::Integer)+ _4 <- mkIntNum (4::Integer)+ -- the ith-queen is in the ith-row.+ -- qi is the column of the ith-queen+ as1 <- mkAnd =<< T.sequence [mkLe _1 q1, mkLe q1 _4]+ as2 <- mkAnd =<< T.sequence [mkLe _1 q2, mkLe q2 _4]+ as3 <- mkAnd =<< T.sequence [mkLe _1 q3, mkLe q3 _4]+ as4 <- mkAnd =<< T.sequence [mkLe _1 q4, mkLe q4 _4]+ -- different columns+ as5 <- mkDistinct [q1,q2,q3,q4]+ -- avoid diagonal attacks+ as6 <- mkNot =<< diagonal 1 q1 q2+ as7 <- mkNot =<< diagonal 2 q1 q3+ as8 <- mkNot =<< diagonal 3 q1 q4+ as9 <- mkNot =<< diagonal 1 q2 q3+ as10 <- mkNot =<< diagonal 2 q2 q4+ as11 <- mkNot =<< diagonal 1 q3 q4+ -- SMTLib script+ _true <- mkTrue+ benchmarkToSMTLibString "queens" "QF_LIA" "unknown" ""+ [as1,as2,as3,as4,as5,as6,as7,as8,as9,as10,as11]+ _true+ where mkAbs :: AST -> Z3 AST+ mkAbs x = do+ _0 <- mkIntNum (0::Integer)+ join $ mkIte <$> mkLe _0 x <*> pure x <*> mkUnaryMinus x+ diagonal d c c' =+ join $ mkEq <$> (mkAbs =<< mkSub [c',c]) <*> (mkIntNum d)
+ examples/Example/Monad/Tuple.hs view
@@ -0,0 +1,30 @@+-- | Create and use tuples.+module Example.Monad.Tuple+ ( run )+ where++import Z3.Monad++run :: IO ()+run = evalZ3 script >>= putStrLn++script :: Z3 String+script = do+ -- newtype Tup = Tup { arg1 :: Int, arg2 :: Int }+ intSort <- mkIntSort+ tupSym <- mkStringSymbol "Tup"+ arg1Sym <- mkStringSymbol "arg1"+ arg2Sym <- mkStringSymbol "arg2"+ (tupSort, _constr, [_proj1, proj2]) <-+ mkTupleSort tupSym [(arg1Sym, intSort), (arg2Sym, intSort)]+ -- t :: Tup+ tSym <- mkStringSymbol "t"+ t <- mkConst tSym tupSort+ -- arg2 t > 5+ p2 <- mkApp proj2 [t]+ assert =<< mkGt p2 =<< mkIntNum (5 :: Integer)+ -- get interpretation for t+ (_res, mbModel) <- getModel+ case mbModel of+ Just model -> showModel model+ Nothing -> return "Couldn't construct model"
examples/Examples.hs view
@@ -5,8 +5,10 @@ import qualified Example.Monad.Queens4All import qualified Example.Monad.DataTypes import qualified Example.Monad.FuncModel+import qualified Example.Monad.MutuallyRecursive import qualified Example.Monad.ToSMTLib import qualified Example.Monad.Tuple+import qualified Example.Monad.Interpolation import System.Environment @@ -23,11 +25,17 @@ , ("funcmodel" , Example.Monad.FuncModel.run )+ , ("mutuallyrecursive"+ , Example.Monad.MutuallyRecursive.run+ ) , ("smtlib" , Example.Monad.ToSMTLib.run ) , ("tuple" , Example.Monad.Tuple.run+ )+ , ("interpolation"+ , Example.Monad.Interpolation.run ) ]
src/Z3/Base.hs view
@@ -13,7 +13,7 @@ -- Low-level bindings to Z3 API. -- -- There is (mostly) a one-to-one correspondence with Z3 C API, thus see--- <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html>+-- <http://z3prover.github.io/api/html/group__capi.html> -- for further details. {- HACKING@@ -68,6 +68,7 @@ , FuncEntry , Params , Solver+ , SortKind(..) , ASTKind(..) -- ** Satisfiability result , Result(..)@@ -105,6 +106,7 @@ , mkTupleSort , mkConstructor , mkDatatype+ , mkDatatypes , mkSetSort -- * Constants and Applications@@ -252,15 +254,28 @@ -- * Accessors , getSymbolString+ , getSortKind , getBvSortSize , getDatatypeSortConstructors , getDatatypeSortRecognizers+ , getDatatypeSortConstructorAccessors , getDeclName+ , getArity+ , getDomain+ , getRange+ , appToAst+ , getAppDecl+ , getAppNumArgs+ , getAppArg+ , getAppArgs , getSort , getBoolValue , getAstKind+ , isApp , toApp , getNumeralString+ , simplify+ , simplifyEx -- ** Helpers , getBool , getInt@@ -311,6 +326,17 @@ , Version(..) , getVersion + -- * Interpolation+ , InterpolationProblem(..)+ , mkInterpolant+ , mkInterpolationContext+ , getInterpolant+ , computeInterpolant+ , readInterpolationProblem+ , checkInterpolant+ , interpolationProfile+ , writeInterpolationProblem+ -- * Solvers , Logic(..) , mkSolver@@ -338,7 +364,7 @@ import Control.Applicative ( (<$>), (<*>), (<*), pure ) import Control.Exception ( Exception, bracket, throw )-import Control.Monad ( join, when )+import Control.Monad ( join, when, (>=>) ) import Data.Fixed ( Fixed, HasResolution ) import Data.Int import Data.IORef ( IORef, newIORef, atomicModifyIORef' )@@ -403,6 +429,10 @@ newtype Constructor = Constructor { unConstructor :: ForeignPtr Z3_constructor } deriving (Eq, Ord, Show) +-- | A list of type contructors for (recursive) datatypes.+newtype ConstructorList = ConstructorList { unConstructorList :: ForeignPtr Z3_constructor_list }+ deriving (Eq, Ord, Show)+ -- | A model for the constraints asserted into the logical context. newtype Model = Model { unModel :: ForeignPtr Z3_model } deriving Eq@@ -438,6 +468,22 @@ | Undef deriving (Eq, Ord, Read, Show) +-- | Different kinds of Z3 types.+data SortKind+ = Z3_UNINTERPRETED_SORT+ | Z3_BOOL_SORT+ | Z3_INT_SORT+ | Z3_REAL_SORT+ | Z3_BV_SORT+ | Z3_ARRAY_SORT+ | Z3_DATATYPE_SORT+ | Z3_RELATION_SORT+ | Z3_FINITE_DOMAIN_SORT+ | Z3_FLOATING_POINT_SORT+ | Z3_ROUNDING_MODE_SORT+ | Z3_UNKNOWN_SORT+ deriving (Eq, Show)+ -- | Different kinds of Z3 AST nodes. data ASTKind = Z3_NUMERAL_AST@@ -447,6 +493,7 @@ | Z3_SORT_AST | Z3_FUNC_DECL_AST | Z3_UNKNOWN_AST+ deriving (Eq, Show) --------------------------------------------------------------------- -- * Configuration@@ -490,17 +537,20 @@ --------------------------------------------------------------------- -- Create context +mkContextWith :: (Ptr Z3_config -> IO (Ptr Z3_context)) -> Config -> IO Context+mkContextWith mkCtx cfg = do+ ctxPtr <- mkCtx (unConfig cfg)+ z3_set_error_handler ctxPtr nullFunPtr+ count <- newIORef 1+ Context <$> newForeignPtr ctxPtr (contextDecRef ctxPtr count)+ <*> pure count+ -- | Create a context using the given configuration. -- -- /Z3_del_context/ is called by Haskell's garbage collector before -- freeing the 'Context' object. mkContext :: Config -> IO Context-mkContext cfg = do- ctxPtr <- z3_mk_context_rc (unConfig cfg)- z3_set_error_handler ctxPtr nullFunPtr- count <- newIORef 1- Context <$> newForeignPtr ctxPtr (contextDecRef ctxPtr count)- <*> pure count+mkContext = mkContextWith z3_mk_context_rc -- TODO: Z3_update_param_value -- TODO: Z3_interrupt@@ -693,13 +743,38 @@ mkDatatype c sym consList = marshalArrayLen consList $ \ n consPtrs -> do toHsCheckError c $ \cPtr -> z3_mk_datatype cPtr (unSymbol sym) n consPtrs +-- | Create list of constructors+mkConstructorList :: Context -- ^ Context+ -> [Constructor] -- ^ List of Constructors+ -> IO ConstructorList+mkConstructorList c consList = marshalArrayLen consList $ \ n consPtrs -> do+ toHsCheckError c $ \cPtr -> z3_mk_constructor_list cPtr n consPtrs++-- | Create mutually recursive datatypes, such as a tree and forest.+--+-- Returns the datatype sorts+mkDatatypes :: Context+ -> [Symbol]+ -> [[Constructor]]+ -> IO ([Sort])+mkDatatypes c syms consLists =+ if length consLists == n then do+ consLists' <- mapM (mkConstructorList c) consLists++ withContextError c $ \cPtr ->+ marshalArrayLen syms $ \ symLen symsPtr ->+ marshalArray consLists' $ \ consPtr ->+ allocaArray n $ \ sortsPtr -> do+ z3_mk_datatypes cPtr symLen symsPtr sortsPtr consPtr+ peekArrayToHs c n sortsPtr+ else+ error "Z3.Base.mkDatatypes: lists of different length"+ where n = length syms+ -- | Create an set type with a given domain type mkSetSort :: Context -> Sort -> IO Sort mkSetSort = liftFun1 z3_mk_set_sort ---- TODO: from Z3_mk_constructor_list on- --------------------------------------------------------------------- -- * Constants and Applications @@ -858,11 +933,13 @@ -- | Create an AST node representing args[0] and ... and args[num_args-1]. mkAnd :: Context -> [AST] -> IO AST-mkAnd = liftAstN "Z3.Base.mkAnd: empty list of expressions" z3_mk_and+mkAnd ctx [] = mkTrue ctx+mkAnd ctx as = marshal z3_mk_and ctx $ marshalArrayLen as -- | Create an AST node representing args[0] or ... or args[num_args-1]. mkOr :: Context -> [AST] -> IO AST-mkOr = liftAstN "Z3.Base.mkOr: empty list of expressions" z3_mk_or+mkOr ctx [] = mkFalse ctx+mkOr ctx os = marshal z3_mk_or ctx $ marshalArrayLen os ------------------------------------------------- -- ** Helpers@@ -1391,7 +1468,7 @@ -- -- Bound variables are indexed by de-Bruijn indices. ----- See <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1d4da8849fca699b345322f8ee1fa31e>+-- See <http://z3prover.github.io/api/html/group__capi.html#ga1d4da8849fca699b345322f8ee1fa31e> mkBound :: Context -> Int -- ^ de-Bruijn index. -> Sort@@ -1520,7 +1597,25 @@ -- TODO: Z3_is_eq_sort --- TODO: Z3_get_sort_kind+-- | Return the sort kind of the given sort.+getSortKind :: Context -> Sort -> IO SortKind+getSortKind ctx sort = toSortKind <$> liftFun1 z3_get_sort_kind ctx sort+ where toSortKind :: Z3_sort_kind -> SortKind+ toSortKind k+ | k == z3_uninterpreted_sort = Z3_UNINTERPRETED_SORT+ | k == z3_bool_sort = Z3_BOOL_SORT+ | k == z3_int_sort = Z3_INT_SORT+ | k == z3_real_sort = Z3_REAL_SORT+ | k == z3_bv_sort = Z3_BV_SORT+ | k == z3_array_sort = Z3_ARRAY_SORT+ | k == z3_datatype_sort = Z3_DATATYPE_SORT+ | k == z3_relation_sort = Z3_RELATION_SORT+ | k == z3_finite_domain_sort = Z3_FINITE_DOMAIN_SORT+ | k == z3_floating_point_sort = Z3_FLOATING_POINT_SORT+ | k == z3_rounding_mode_sort = Z3_ROUNDING_MODE_SORT+ | k == z3_unknown_sort = Z3_UNKNOWN_SORT+ | otherwise =+ error "Z3.Base.getSortKind: unknown `Z3_sort_kind'" -- | Return the size of the given bit-vector sort. getBvSortSize :: Context -> Sort -> IO Int@@ -1538,7 +1633,6 @@ -- TODO: Z3_get_tuple_sort_field_decl --- TODO: Needs proper review -- | Get list of constructors for datatype. getDatatypeSortConstructors :: Context -> Sort -- ^ Datatype sort.@@ -1546,13 +1640,12 @@ getDatatypeSortConstructors c dtSort = withContextError c $ \cPtr -> h2c dtSort $ \dtSortPtr -> do- numCons <- checkError cPtr $ z3_get_datatype_sort_num_constructors cPtr dtSortPtr- T.mapM (getConstructor dtSortPtr) [0..(numCons-1)]+ numCons <- checkError cPtr $ z3_get_datatype_sort_num_constructors cPtr dtSortPtr+ T.mapM (getConstructor dtSortPtr) [0..(numCons-1)] where- getConstructor dtSortPtr idx = do+ getConstructor dtSortPtr idx = toHsCheckError c $ \cPtr -> z3_get_datatype_sort_constructor cPtr dtSortPtr idx --- TODO: Needs proper review -- | Get list of recognizers for datatype. getDatatypeSortRecognizers :: Context -> Sort -- ^ Datatype sort.@@ -1560,15 +1653,35 @@ getDatatypeSortRecognizers c dtSort = withContextError c $ \cPtr -> h2c dtSort $ \dtSortPtr -> do- numCons <- checkError cPtr $ z3_get_datatype_sort_num_constructors cPtr dtSortPtr- T.mapM (getConstructor dtSortPtr) [0..(numCons-1)]+ numCons <- checkError cPtr $ z3_get_datatype_sort_num_constructors cPtr dtSortPtr+ T.mapM (getRecognizer dtSortPtr) [0..(numCons-1)] where- -- TODO: Maybe this should be renamed to getRecognizer :-)- getConstructor dtSortPtr idx = do+ getRecognizer dtSortPtr idx = toHsCheckError c $ \cPtr -> z3_get_datatype_sort_recognizer cPtr dtSortPtr idx --- TODO: Z3_get_datatype_sort_constructor_accessor+-- | Get list of accessors for the datatype constructor.+getDatatypeSortConstructorAccessors :: Context+ -> Sort -- ^ Datatype sort.+ -> IO [[FuncDecl]] -- ^ Constructor accessors.+getDatatypeSortConstructorAccessors c dtSort =+ withContextError c $ \cPtr ->+ h2c dtSort $ \dtSortPtr -> do+ numCons <- checkError cPtr $ z3_get_datatype_sort_num_constructors cPtr dtSortPtr+ T.mapM (getAccessors dtSortPtr) [0..(numCons-1)]+ where+ getConstructor dtSortPtr idx_c =+ withContext c $ \cPtr -> z3_get_datatype_sort_constructor cPtr dtSortPtr idx_c + getAccessors dtSortPtr idx_c = do+ consPtr <- getConstructor dtSortPtr idx_c+ numAs <- toHsCheckError c $ \cPtr -> z3_get_arity cPtr consPtr+ if numAs > 0 -- NB: (0::CUInt) - 1 == 0+ then T.mapM (\idx_a -> getAccessors' dtSortPtr idx_c idx_a) [0..(numAs - 1)]+ else return []++ getAccessors' dtSortPtr idx_c idx_a =+ toHsCheckError c $ \cPtr -> z3_get_datatype_sort_constructor_accessor cPtr dtSortPtr idx_c idx_a+ -- TODO: Z3_get_relation_arity -- TODO: Z3_get_relation_column@@ -1588,8 +1701,21 @@ -- TODO: Z3_get_domain_size --- TODO: Z3_get_range+-- | Returns the number of parameters of the given declaration+getArity :: Context -> FuncDecl -> IO Int+getArity = liftFun1 z3_get_arity +-- | Returns the sort of the i-th parameter of the given function declaration+getDomain :: Context+ -> FuncDecl -- ^ A function declaration+ -> Int -- ^ i+ -> IO Sort+getDomain = liftFun2 z3_get_domain++-- | Returns the range of the given declaration.+getRange :: Context -> FuncDecl -> IO Sort+getRange = liftFun1 z3_get_range+ -- TODO: Z3_get_decl_num_parameters -- TODO: Z3_get_decl_parameter_kind@@ -1608,14 +1734,28 @@ -- TODO: Z3_get_decl_rational_parameter --- TODO: Z3_app_to_ast+-- | Convert an app into AST. This is just type casting.+appToAst :: Context -> App -> IO AST+appToAst = liftFun1 z3_app_to_ast --- TODO: Z3_get_app_decl+-- | Return the declaration of a constant or function application.+getAppDecl :: Context -> App -> IO FuncDecl+getAppDecl = liftFun1 z3_get_app_decl --- TODO: Z3_get_app_num_args+-- | Return the number of argument of an application. If t is an constant, then the number of arguments is 0.+getAppNumArgs :: Context -> App -> IO Int+getAppNumArgs = liftFun1 z3_get_app_num_args --- TODO: Z3_get_app_arg+-- | Return the i-th argument of the given application.+getAppArg :: Context -> App -> Int -> IO AST+getAppArg = liftFun2 z3_get_app_arg +-- | Return a list of all the arguments of the given application.+getAppArgs :: Context -> App -> IO [AST]+getAppArgs ctx a = do+ n <- getAppNumArgs ctx a+ T.forM [0..n-1] (getAppArg ctx a)+ -- TODO: Z3_is_eq_ast -- TODO: Z3_get_ast_id@@ -1657,7 +1797,9 @@ | otherwise = error "Z3.Base.getAstKind: unknown `Z3_ast_kind'" --- TODO: Z3_is_app+-- | Return True if an ast is APP_AST, False otherwise.+isApp :: Context -> AST -> IO Bool+isApp = liftFun1 z3_is_app -- TODO: Z3_is_numeral_ast @@ -1725,9 +1867,11 @@ -- TODO: Z3_get_quantifier_body --- TODO: Z3_simplify+simplify :: Context -> AST -> IO AST+simplify = liftFun1 z3_simplify --- TODO: Z3_simplify_ex+simplifyEx :: Context -> AST -> Params -> IO AST+simplifyEx = liftFun2 z3_simplify_ex -- TODO: Z3_simplify_get_help @@ -2076,7 +2220,7 @@ deriving Typeable instance Show Z3Error where- show (Z3Error _ s) = s+ show (Z3Error _ s) = "Z3 error: " ++ s -- | Z3 error codes. data Z3ErrorCode = SortError | IOB | InvalidArg | ParserError | NoParser@@ -2168,6 +2312,131 @@ -- TODO ---------------------------------------------------------------------+-- Interpolation++-- | Interpolation problem formulation.+data InterpolationProblem =+ InterpolationProblem {+ getConstraints :: [AST]+ , getParents :: Maybe [Int]+ , getTheoryTerms :: [AST]+ }++-- | Generate a Z3 context suitable for generation of interpolants.+mkInterpolationContext :: Config -> IO Context+mkInterpolationContext = mkContextWith z3_mk_interpolation_context++-- | Create an AST node marking a formula position for interpolation.+mkInterpolant :: Context+ -> AST -- ^ boolean expression+ -> IO AST+mkInterpolant = liftFun1 z3_mk_interpolant++-- | Extracts interpolants from a proof of unsatisfiability.+--+-- Interpolants are computed in pre-order for occurrences of 'mkInterpolant'+-- within the second argument, which needs to be in form of a conjunction.+getInterpolant :: Context+ -> AST -- ^ proof of /false/+ -> AST -- ^ interpolation pattern (cf. 'mkInterpolant')+ -> Params+ -> IO [AST]+getInterpolant = liftFun3 z3_get_interpolant++-- | Checks satisfiability of input conjunction.+--+-- Returns either a model witnessing satisfiability, or a (sequence) interpolants+-- between individual subformulae of the conjunction wrapped in 'mkInterpolant'.+--+-- Result:+-- /sat/ -> @Just (Left <model>)@+-- /unsat/ -> @Just (Right <interp>)@+-- /unknown/ -> @Nothing@+computeInterpolant :: Context -> AST -> Params+ -> IO (Maybe (Either Model [AST]))+computeInterpolant c p ps =+ alloca $ \interp ->+ alloca $ \model ->+ h2c p $ \pat -> do+ h2c ps $ \params -> do+ res <- toHsCheckError c $ \ctx ->+ z3_compute_interpolant ctx pat params interp model+ case res of+ Sat -> Just . Left <$> peekToHs c model+ Unsat -> Just . Right <$> peekToHs c interp+ Undef -> return Nothing++-- | Read an interpolation problem from file.+readInterpolationProblem :: Context -> FilePath+ -> IO (Either String InterpolationProblem)+readInterpolationProblem c file =+ withCString file $ \fileName ->+ alloca $ \num ->+ alloca $ \cnsts ->+ alloca $ \parents ->+ alloca $ \errorMsg ->+ alloca $ \numTheory ->+ alloca $ \theory -> do+ suc <- toHsCheckError c $ \ctx ->+ z3_read_interpolation_problem ctx num cnsts parents fileName errorMsg+ numTheory theory+ if suc+ then do+ n <- peekToHs c num+ constraints' <- peekArrayToHs c n cnsts+ parents' <- peekPtrArrayToHs c n `T.traverse` ptrToMaybe parents+ nt <- peekToHs c numTheory+ theory' <- peekArrayToHs c nt theory+ return $ Right $ InterpolationProblem+ { getConstraints = constraints'+ , getParents = parents'+ , getTheoryTerms = theory' }+ else do+ Left <$> peekToHs c errorMsg++-- | Check the correctness of an interpolant.+--+-- The Z3 context must have no constraints asserted when this call is made.+-- That means that after interpolating, you must first fully pop the Z3 context+-- before calling this.+checkInterpolant :: Context -> InterpolationProblem -> [AST] -> IO (Result,Maybe String)+checkInterpolant c prob is =+ marshalArrayLen cs $ \num cnsts ->+ marshalMaybeArray ps $ \parents ->+ marshalArray is $ \interps ->+ alloca $ \errorMsgPtr ->+ marshalArrayLen t $ \numTheory theory -> do+ res <- toHsCheckError c $ \ctx ->+ z3_check_interpolant ctx num cnsts parents interps errorMsgPtr numTheory theory+ errorMsg <- peekToMaybeHs c errorMsgPtr+ return (res,errorMsg)+ where cs = getConstraints prob+ ps = getParents prob+ t = getTheoryTerms prob++-- | Return a string summarizing cumulative time used for interpolation.+--+-- This string is purely for entertainment purposes and has no semantics.+interpolationProfile :: Context -> IO String+interpolationProfile = liftFun0 z3_interpolation_profile++-- | Write an interpolation problem to file suitable for reading with 'readInterpolationProblem'.+--+-- The output file is a sequence of SMT-LIB2 format commands, suitable for reading+-- with command-line Z3 or other interpolating solvers.+writeInterpolationProblem :: Context -> FilePath -> InterpolationProblem -> IO ()+writeInterpolationProblem c file prob =+ marshalArrayLen cs $ \num cnsts ->+ marshalMaybeArray ps $ \parents ->+ withCString file $ \filename ->+ marshalArrayLen t $ \numTheory theory ->+ toHsCheckError c $ \ctx ->+ z3_write_interpolation_problem ctx num cnsts parents filename numTheory theory+ where cs = getConstraints prob+ ps = getParents prob+ t = getTheoryTerms prob++--------------------------------------------------------------------- -- Solvers -- | Solvers available in Z3.@@ -2407,6 +2676,10 @@ marshalArrayLen hs f = hs2cs hs $ \cs -> withArrayLen cs $ \n -> f (fromIntegral n) +marshalMaybeArray :: (Marshal h c, Storable c) => Maybe [h] -> (Ptr c -> IO a) -> IO a+marshalMaybeArray Nothing f = f nullPtr+marshalMaybeArray (Just hs) f = marshalArray hs f+ liftAstN :: String -> (Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)) -> Context -> [AST] -> IO AST@@ -2418,16 +2691,32 @@ c2h :: Context -> c -> IO h h2c :: h -> (c -> IO r) -> IO r -toHsCheckError :: Marshal h c => Context -> (Ptr Z3_context -> IO c) -> IO h-toHsCheckError c f = withContext c $ \cPtr ->- c2h c =<< checkError cPtr (f cPtr)- hs2cs :: Marshal h c => [h] -> ([c] -> IO r) -> IO r hs2cs [] f = f [] hs2cs (h:hs) f = h2c h $ \c -> hs2cs hs $ \cs -> f (c:cs) +cs2hs :: Marshal h c => Context -> [c] -> IO [h]+cs2hs ctx = mapM (c2h ctx)++peekToHs :: (Marshal h c, Storable c) => Context -> Ptr c -> IO h+peekToHs c ptr = c2h c =<< peek ptr++peekToMaybeHs :: (Marshal h (Ptr c), Storable c) => Context -> Ptr (Ptr c) -> IO (Maybe h)+peekToMaybeHs c = peek >=> (c2h c `T.traverse`) . ptrToMaybe++peekArrayToHs :: (Marshal h c, Storable c) => Context -> Int -> Ptr c -> IO [h]+peekArrayToHs c n dPtr =+ cs2hs c =<< peekArray n dPtr++peekPtrArrayToHs :: (Marshal h c, Storable c) => Context -> Int -> Ptr (Ptr c) -> IO [h]+peekPtrArrayToHs c n = peekArray n >=> mapM (peekToHs c)++toHsCheckError :: Marshal h c => Context -> (Ptr Z3_context -> IO c) -> IO h+toHsCheckError c f = withContext c $ \cPtr ->+ c2h c =<< checkError cPtr (f cPtr)+ type Z3SetRefCount c = Ptr Z3_context -> Ptr c -> IO () type Z3IncRefFun c = Z3SetRefCount c type Z3DecRefFun c = Z3SetRefCount c@@ -2558,6 +2847,10 @@ instance Marshal Constructor (Ptr Z3_constructor) where c2h = mkC2hRefCount Constructor dummy_inc_ref z3_del_constructor h2c cns = withForeignPtr (unConstructor cns)++instance Marshal ConstructorList (Ptr Z3_constructor_list) where+ c2h = mkC2hRefCount ConstructorList dummy_inc_ref z3_del_constructor_list+ h2c cl = withForeignPtr (unConstructorList cl) instance Marshal Solver (Ptr Z3_solver) where c2h = mkC2hRefCount Solver z3_solver_inc_ref z3_solver_dec_ref
src/Z3/Base/C.hsc view
@@ -52,6 +52,8 @@ data Z3_constructor +data Z3_constructor_list+ data Z3_model data Z3_func_interp@@ -64,7 +66,7 @@ data Z3_ast_vector --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6c2de6ea89b244e37c3ffb17a9ea2a89>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga6c2de6ea89b244e37c3ffb17a9ea2a89> newtype Z3_lbool = Z3_lbool CInt deriving Eq @@ -73,23 +75,23 @@ z3_l_false = Z3_lbool (#const Z3_L_FALSE) z3_l_undef = Z3_lbool (#const Z3_L_UNDEF) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3a65ded0ada3ee285865759a21140eeb>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga3a65ded0ada3ee285865759a21140eeb> newtype Z3_bool = Z3_bool CInt deriving Eq --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga311274c8a65a5d25cf715ebdf0c68747>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga311274c8a65a5d25cf715ebdf0c68747> type Z3_error_handler = Ptr Z3_context -> Z3_error_code -> IO () z3_true, z3_false :: Z3_bool--- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad86c8730a2e4e61bac585b240a6288d4>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gad86c8730a2e4e61bac585b240a6288d4> z3_true = Z3_bool(#const Z3_TRUE)--- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1d9cee57472b2c7623642f123b8f1781>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga1d9cee57472b2c7623642f123b8f1781> z3_false = Z3_bool(#const Z3_FALSE) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga49f047b93b0282e686956678da5b86b1>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga49f047b93b0282e686956678da5b86b1> type Z3_string = CString --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0112dc1e8e08a19bf7a4299bb09a9727>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga0112dc1e8e08a19bf7a4299bb09a9727> type Z3_ast_print_mode = CInt z3_print_smtlib_full :: Z3_ast_print_mode z3_print_smtlib_full = #const Z3_PRINT_SMTLIB_FULL@@ -100,7 +102,7 @@ z3_print_smtlib2_compliant :: Z3_ast_print_mode z3_print_smtlib2_compliant = #const Z3_PRINT_SMTLIB2_COMPLIANT --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa9f9e7b1b5b81381fab96debbaaa638f>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaa9f9e7b1b5b81381fab96debbaaa638f> type Z3_error_code = CInt #{enum Z3_error_code, , z3_ok = Z3_OK@@ -118,7 +120,35 @@ , z3_exception = Z3_EXCEPTION } --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga015148ad21a032e79a496629651dedb8>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga4cd6ad05aba48f4b679f0c13310ed2a4>+type Z3_sort_kind = CInt+z3_uninterpreted_sort :: Z3_sort_kind+z3_uninterpreted_sort = #const Z3_UNINTERPRETED_SORT+z3_bool_sort :: Z3_sort_kind+z3_bool_sort = #const Z3_BOOL_SORT+z3_int_sort :: Z3_sort_kind+z3_int_sort = #const Z3_INT_SORT+z3_real_sort :: Z3_sort_kind+z3_real_sort = #const Z3_REAL_SORT+z3_bv_sort :: Z3_sort_kind+z3_bv_sort = #const Z3_BV_SORT+z3_array_sort :: Z3_sort_kind+z3_array_sort = #const Z3_ARRAY_SORT+z3_datatype_sort :: Z3_sort_kind+z3_datatype_sort = #const Z3_DATATYPE_SORT+z3_relation_sort :: Z3_sort_kind+z3_relation_sort = #const Z3_RELATION_SORT+z3_finite_domain_sort :: Z3_sort_kind+z3_finite_domain_sort = #const Z3_FINITE_DOMAIN_SORT+z3_floating_point_sort :: Z3_sort_kind+z3_floating_point_sort = #const Z3_FLOATING_POINT_SORT+z3_rounding_mode_sort :: Z3_sort_kind+z3_rounding_mode_sort = #const Z3_ROUNDING_MODE_SORT+z3_unknown_sort :: Z3_sort_kind+z3_unknown_sort = #const Z3_UNKNOWN_SORT+++-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga015148ad21a032e79a496629651dedb8> type Z3_ast_kind = CInt z3_numeral_ast :: Z3_ast_kind z3_numeral_ast = #const Z3_NUMERAL_AST@@ -139,15 +169,15 @@ --------------------------------------------------------------------- -- * Create configuration --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7d6c40d9b79fe8a8851cc8540970787f>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga7d6c40d9b79fe8a8851cc8540970787f> foreign import ccall unsafe "Z3_mk_config" z3_mk_config :: IO (Ptr Z3_config) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5e620acf5d55d0271097c9bb97219774>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga5e620acf5d55d0271097c9bb97219774> foreign import ccall unsafe "Z3_del_config" z3_del_config :: Ptr Z3_config -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga001ade87a1671fe77d7e53ed0f4f1ec3>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga001ade87a1671fe77d7e53ed0f4f1ec3> foreign import ccall unsafe "Z3_set_param_value" z3_set_param_value :: Ptr Z3_config -> Z3_string -> Z3_string -> IO () @@ -155,67 +185,67 @@ --------------------------------------------------------------------- -- * Create context --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga98acd59d946eceb4f261bc50489216ee>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga98acd59d946eceb4f261bc50489216ee> foreign import ccall unsafe "Z3_mk_context_rc" z3_mk_context_rc :: Ptr Z3_config -> IO (Ptr Z3_context) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga556eae80ed43ab13e1e7dc3b38c35200>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga556eae80ed43ab13e1e7dc3b38c35200> foreign import ccall unsafe "Z3_del_context" z3_del_context :: Ptr Z3_context -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4a11514494fbf3467b89f0a80ac81e7a>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga4a11514494fbf3467b89f0a80ac81e7a> foreign import ccall unsafe "Z3_inc_ref" z3_inc_ref :: Ptr Z3_context -> Ptr Z3_ast -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9cd52225142c085630495044acc68bd2>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga9cd52225142c085630495044acc68bd2> foreign import ccall unsafe "Z3_inc_ref" z3_dec_ref :: Ptr Z3_context -> Ptr Z3_ast -> IO () --------------------------------------------------------------------- -- * Symbols --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3df806baf6124df3e63a58cf23e12411>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga3df806baf6124df3e63a58cf23e12411> foreign import ccall unsafe "Z3_mk_int_symbol" z3_mk_int_symbol :: Ptr Z3_context -> CInt -> IO (Ptr Z3_symbol) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafebb0d3c212927cf7834c3a20a84ecae>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gafebb0d3c212927cf7834c3a20a84ecae> foreign import ccall unsafe "Z3_mk_string_symbol" z3_mk_string_symbol :: Ptr Z3_context -> Z3_string -> IO (Ptr Z3_symbol) --------------------------------------------------------------------- -- * Sorts --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga57c27f2c4e9eccf17072a84c6cecb1db>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga57c27f2c4e9eccf17072a84c6cecb1db> foreign import ccall unsafe "Z3_sort_to_ast" z3_sort_to_ast :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast) -- TODO Sorts: Z3_is_eq_sort --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga736e88741af1c178cbebf94c49aa42de>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga736e88741af1c178cbebf94c49aa42de> foreign import ccall unsafe "Z3_mk_uninterpreted_sort" z3_mk_uninterpreted_sort :: Ptr Z3_context -> Ptr Z3_symbol -> IO (Ptr Z3_sort) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacdc73510b69a010b71793d429015f342>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gacdc73510b69a010b71793d429015f342> foreign import ccall unsafe "Z3_mk_bool_sort" z3_mk_bool_sort :: Ptr Z3_context -> IO (Ptr Z3_sort) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6cd426ab5748653b77d389fd3eac1015>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga6cd426ab5748653b77d389fd3eac1015> foreign import ccall unsafe "Z3_mk_int_sort" z3_mk_int_sort :: Ptr Z3_context -> IO (Ptr Z3_sort) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga40ef93b9738485caed6dc84631c3c1a0>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga40ef93b9738485caed6dc84631c3c1a0> foreign import ccall unsafe "Z3_mk_real_sort" z3_mk_real_sort :: Ptr Z3_context -> IO (Ptr Z3_sort) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeed000a1bbb84b6ca6fdaac6cf0c1688>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaeed000a1bbb84b6ca6fdaac6cf0c1688> foreign import ccall unsafe "Z3_mk_bv_sort" z3_mk_bv_sort :: Ptr Z3_context -> CUInt -> IO (Ptr Z3_sort) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafe617994cce1b516f46128e448c84445>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gafe617994cce1b516f46128e448c84445> foreign import ccall unsafe "Z3_mk_array_sort" z3_mk_array_sort :: Ptr Z3_context -> Ptr Z3_sort -> Ptr Z3_sort -> IO (Ptr Z3_sort) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7156b9c0a76a28fae46c81f8e3cdf0f1>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga7156b9c0a76a28fae46c81f8e3cdf0f1> foreign import ccall unsafe "Z3_mk_tuple_sort" z3_mk_tuple_sort :: Ptr Z3_context -> Ptr Z3_symbol@@ -226,7 +256,7 @@ -> Ptr (Ptr Z3_func_decl) -> IO (Ptr Z3_sort) --- Reference <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa779e39f7050b9d51857887954b5f9b0>+-- | Reference <http://z3prover.github.io/api/html/group__capi.html#gaa779e39f7050b9d51857887954b5f9b0> foreign import ccall unsafe "Z3_mk_constructor" z3_mk_constructor :: Ptr Z3_context -> Ptr Z3_symbol@@ -237,20 +267,41 @@ -> Ptr CUInt -> IO (Ptr Z3_constructor) --- Reference <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga63816efdbce93734c72f395b6a6a9e35>+-- | Reference <http://z3prover.github.io/api/html/group__capi.html#ga63816efdbce93734c72f395b6a6a9e35> foreign import ccall unsafe "Z3_del_constructor" z3_del_constructor :: Ptr Z3_context -> Ptr Z3_constructor -> IO () ---- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab6809d53327d807da9158abdf75df387>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gab6809d53327d807da9158abdf75df387> foreign import ccall unsafe "Z3_mk_datatype" z3_mk_datatype :: Ptr Z3_context -> Ptr Z3_symbol -> CUInt -> Ptr (Ptr Z3_constructor) -> IO (Ptr Z3_sort)- --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6865879523e7e882d7e50a2d8445ac8b>++-- | Reference <http://z3prover.github.io/api/html/group__capi.html#gac9305d5d4eb1ce68d17300f5af19fafd>+foreign import ccall unsafe "Z3_mk_constructor_list"+ z3_mk_constructor_list :: Ptr Z3_context+ -> CUInt+ -> Ptr (Ptr Z3_constructor)+ -> IO (Ptr Z3_constructor_list)++-- | Reference <http://z3prover.github.io/api/html/group__capi.html#gaa7a2e823e23fdfba407ea5088c8d1709>+foreign import ccall unsafe "Z3_del_constructor_list"+ z3_del_constructor_list :: Ptr Z3_context+ -> Ptr (Z3_constructor_list)+ -> IO ()++-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gac9305d5d4eb1ce68d17300f5af19fafd>+foreign import ccall unsafe "Z3_mk_datatypes"+ z3_mk_datatypes :: Ptr Z3_context+ -> CUInt+ -> Ptr (Ptr Z3_symbol)+ -> Ptr (Ptr Z3_sort)+ -> Ptr (Ptr Z3_constructor_list)+ -> IO ()++-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga6865879523e7e882d7e50a2d8445ac8b> foreign import ccall unsafe "Z3_mk_set_sort" z3_mk_set_sort :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort) @@ -259,7 +310,7 @@ --------------------------------------------------------------------- -- * Constants and Applications --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa5c5e2602a44d5f1373f077434859ca2>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaa5c5e2602a44d5f1373f077434859ca2> foreign import ccall unsafe "Z3_mk_func_decl" z3_mk_func_decl :: Ptr Z3_context -> Ptr Z3_symbol@@ -268,7 +319,7 @@ -> Ptr Z3_sort -> IO (Ptr Z3_func_decl) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga33a202d86bf628bfab9b6f437536cebe>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga33a202d86bf628bfab9b6f437536cebe> foreign import ccall unsafe "Z3_mk_app" z3_mk_app :: Ptr Z3_context -> Ptr Z3_func_decl@@ -276,15 +327,15 @@ -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga093c9703393f33ae282ec5e8729354ef>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga093c9703393f33ae282ec5e8729354ef> foreign import ccall unsafe "Z3_mk_const" z3_mk_const :: Ptr Z3_context -> Ptr Z3_symbol -> Ptr Z3_sort -> IO (Ptr Z3_ast) --- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga99cbd3e87cdd759a3d0ea43b4884ed32>+-- Reference: <http://z3prover.github.io/api/html/group__capi.html#ga99cbd3e87cdd759a3d0ea43b4884ed32> foreign import ccall unsafe "Z3_mk_fresh_const" z3_mk_fresh_const :: Ptr Z3_context -> Z3_string -> Ptr Z3_sort -> IO (Ptr Z3_ast) --- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1f60c7eb41c5603e55a188a14dc929ec>+-- Reference: <http://z3prover.github.io/api/html/group__capi.html#ga1f60c7eb41c5603e55a188a14dc929ec> foreign import ccall unsafe "Z3_mk_fresh_func_decl" z3_mk_fresh_func_decl :: Ptr z3_context -> Z3_string@@ -296,409 +347,409 @@ --------------------------------------------------------------------- -- * Propositional Logic and Equality --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae898e7380409bbc57b56cc5205ef1db7>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gae898e7380409bbc57b56cc5205ef1db7> foreign import ccall unsafe "Z3_mk_true" z3_mk_true :: Ptr Z3_context -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5952ac17671117a02001fed6575c778d>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga5952ac17671117a02001fed6575c778d> foreign import ccall unsafe "Z3_mk_false" z3_mk_false :: Ptr Z3_context -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95a19ce675b70e22bb0401f7137af37c>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga95a19ce675b70e22bb0401f7137af37c> foreign import ccall unsafe "Z3_mk_eq" z3_mk_eq :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa076d3a668e0ec97d61744403153ecf7>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaa076d3a668e0ec97d61744403153ecf7> foreign import ccall unsafe "Z3_mk_distinct" z3_mk_distinct :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3329538091996eb7b3dc677760a61072>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga3329538091996eb7b3dc677760a61072> foreign import ccall unsafe "Z3_mk_not" z3_mk_not :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94417eed5c36e1ad48bcfc8ad6e83547>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga94417eed5c36e1ad48bcfc8ad6e83547> foreign import ccall unsafe "Z3_mk_ite" z3_mk_ite :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga930a8e844d345fbebc498ac43a696042>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga930a8e844d345fbebc498ac43a696042> foreign import ccall unsafe "Z3_mk_iff" z3_mk_iff :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac829c0e25bbbd30343bf073f7b524517>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gac829c0e25bbbd30343bf073f7b524517> foreign import ccall unsafe "Z3_mk_implies" z3_mk_implies :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacc6d1b848032dec0c4617b594d4229ec>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gacc6d1b848032dec0c4617b594d4229ec> foreign import ccall unsafe "Z3_mk_xor" z3_mk_xor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacde98ce4a8ed1dde50b9669db4838c61>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gacde98ce4a8ed1dde50b9669db4838c61> foreign import ccall unsafe "Z3_mk_and" z3_mk_and :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga00866d16331d505620a6c515302021f9>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga00866d16331d505620a6c515302021f9> foreign import ccall unsafe "Z3_mk_or" z3_mk_or :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --------------------------------------------------------------------- -- * Arithmetic: Integers and Reals --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e4ac0a4e53eee0b4b0ef159ed7d0cd5>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga4e4ac0a4e53eee0b4b0ef159ed7d0cd5> foreign import ccall unsafe "Z3_mk_add" z3_mk_add :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab9affbf8401a18eea474b59ad4adc890>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gab9affbf8401a18eea474b59ad4adc890> foreign import ccall unsafe "Z3_mk_mul" z3_mk_mul :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4f5fea9b683f9e674fd8f14d676cc9a9>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga4f5fea9b683f9e674fd8f14d676cc9a9> foreign import ccall unsafe "Z3_mk_sub" z3_mk_sub :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gadcd2929ad732937e25f34277ce4988ea>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gadcd2929ad732937e25f34277ce4988ea> foreign import ccall unsafe "Z3_mk_unary_minus" z3_mk_unary_minus :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1ac60ee8307af8d0b900375914194ff3>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga1ac60ee8307af8d0b900375914194ff3> foreign import ccall unsafe "Z3_mk_div" z3_mk_div :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8e350ac77e6b8fe805f57efe196e7713>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga8e350ac77e6b8fe805f57efe196e7713> foreign import ccall unsafe "Z3_mk_mod" z3_mk_mod :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2fcdb17f9039bbdaddf8a30d037bd9ff>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga2fcdb17f9039bbdaddf8a30d037bd9ff> foreign import ccall unsafe "Z3_mk_rem" z3_mk_rem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga58a3dc67c5de52cf599c346803ba1534>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga58a3dc67c5de52cf599c346803ba1534> foreign import ccall unsafe "Z3_mk_lt" z3_mk_lt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa9a33d11096841f4e8c407f1578bc0bf>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaa9a33d11096841f4e8c407f1578bc0bf> foreign import ccall unsafe "Z3_mk_le" z3_mk_le :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46167b86067586bb742c0557d7babfd3>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga46167b86067586bb742c0557d7babfd3> foreign import ccall unsafe "Z3_mk_gt" z3_mk_gt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad9245cbadb80b192323d01a8360fb942>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gad9245cbadb80b192323d01a8360fb942> foreign import ccall unsafe "Z3_mk_ge" z3_mk_ge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7130641e614c7ebafd28ae16a7681a21>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga7130641e614c7ebafd28ae16a7681a21> foreign import ccall unsafe "Z3_mk_int2real" z3_mk_int2real :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga759b6563ba1204aae55289009a3fdc6d>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga759b6563ba1204aae55289009a3fdc6d> foreign import ccall unsafe "Z3_mk_real2int" z3_mk_real2int :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaac2ad0fb04e4900fdb4add438d137ad3>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaac2ad0fb04e4900fdb4add438d137ad3> foreign import ccall unsafe "Z3_mk_is_int" z3_mk_is_int :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --------------------------------------------------------------------- -- * Bit-vectors --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga36cf75c92c54c1ca633a230344f23080>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga36cf75c92c54c1ca633a230344f23080> foreign import ccall unsafe "Z3_mk_bvnot" z3_mk_bvnot :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaccc04f2b58903279b1b3be589b00a7d8>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaccc04f2b58903279b1b3be589b00a7d8> foreign import ccall unsafe "Z3_mk_bvredand" z3_mk_bvredand :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafd18e127c0586abf47ad9cd96895f7d2>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gafd18e127c0586abf47ad9cd96895f7d2> foreign import ccall unsafe "Z3_mk_bvredor" z3_mk_bvredor :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab96e0ea55334cbcd5a0e79323b57615d>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gab96e0ea55334cbcd5a0e79323b57615d> foreign import ccall unsafe "Z3_mk_bvand" z3_mk_bvand :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga77a6ae233fb3371d187c6d559b2843f5>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga77a6ae233fb3371d187c6d559b2843f5> foreign import ccall unsafe "Z3_mk_bvor" z3_mk_bvor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0a3821ea00b1c762205f73e4bc29e7d8>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga0a3821ea00b1c762205f73e4bc29e7d8> foreign import ccall unsafe "Z3_mk_bvxor" z3_mk_bvxor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga96dc37d36efd658fff5b2b4df49b0e61>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga96dc37d36efd658fff5b2b4df49b0e61> foreign import ccall unsafe "Z3_mk_bvnand" z3_mk_bvnand :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabf15059e9e8a2eafe4929fdfd259aadb>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gabf15059e9e8a2eafe4929fdfd259aadb> foreign import ccall unsafe "Z3_mk_bvnor" z3_mk_bvnor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga784f5ca36a4b03b93c67242cc94b21d6>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga784f5ca36a4b03b93c67242cc94b21d6> foreign import ccall unsafe "Z3_mk_bvxnor" z3_mk_bvxnor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0c78be00c03eda4ed6a983224ed5c7b7+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga0c78be00c03eda4ed6a983224ed5c7b7 foreign import ccall unsafe "Z3_mk_bvneg" z3_mk_bvneg :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga819814e33573f3f9948b32fdc5311158>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga819814e33573f3f9948b32fdc5311158> foreign import ccall unsafe "Z3_mk_bvadd" z3_mk_bvadd :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga688c9aa1347888c7a51be4e46c19178e>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga688c9aa1347888c7a51be4e46c19178e> foreign import ccall unsafe "Z3_mk_bvsub" z3_mk_bvsub :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6abd3dde2a1ceff1704cf7221a72258c>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga6abd3dde2a1ceff1704cf7221a72258c> foreign import ccall unsafe "Z3_mk_bvmul" z3_mk_bvmul :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga56ce0cd61666c6f8cf5777286f590544>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga56ce0cd61666c6f8cf5777286f590544> foreign import ccall unsafe "Z3_mk_bvudiv" z3_mk_bvudiv :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad240fedb2fda1c1005b8e9d3c7f3d5a0>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gad240fedb2fda1c1005b8e9d3c7f3d5a0> foreign import ccall unsafe "Z3_mk_bvsdiv" z3_mk_bvsdiv :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5df4298ec835e43ddc9e3e0bae690c8d>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga5df4298ec835e43ddc9e3e0bae690c8d> foreign import ccall unsafe "Z3_mk_bvurem" z3_mk_bvurem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46c18a3042fca174fe659d3185693db1>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga46c18a3042fca174fe659d3185693db1> foreign import ccall unsafe "Z3_mk_bvsrem" z3_mk_bvsrem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95dac8e6eecb50f63cb82038560e0879>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga95dac8e6eecb50f63cb82038560e0879> foreign import ccall unsafe "Z3_mk_bvsmod" z3_mk_bvsmod :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5774b22e93abcaf9b594672af6c7c3c4>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga5774b22e93abcaf9b594672af6c7c3c4> foreign import ccall unsafe "Z3_mk_bvult" z3_mk_bvult :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8ce08af4ed1fbdf08d4d6e63d171663a>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga8ce08af4ed1fbdf08d4d6e63d171663a> foreign import ccall unsafe "Z3_mk_bvslt" z3_mk_bvslt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab738b89de0410e70c089d3ac9e696e87>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gab738b89de0410e70c089d3ac9e696e87> foreign import ccall unsafe "Z3_mk_bvule" z3_mk_bvule :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab7c026feb93e7d2eab180e96f1e6255d>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gab7c026feb93e7d2eab180e96f1e6255d> foreign import ccall unsafe "Z3_mk_bvsle" z3_mk_bvsle :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gade58fbfcf61b67bf8c4a441490d3c4df>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gade58fbfcf61b67bf8c4a441490d3c4df> foreign import ccall unsafe "Z3_mk_bvuge" z3_mk_bvuge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeec3414c0e8a90a6aa5a23af36bf6dc5>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaeec3414c0e8a90a6aa5a23af36bf6dc5> foreign import ccall unsafe "Z3_mk_bvsge" z3_mk_bvsge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga063ab9f16246c99e5c1c893613927ee3>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga063ab9f16246c99e5c1c893613927ee3> foreign import ccall unsafe "Z3_mk_bvugt" z3_mk_bvugt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e93a985aa2a7812c7c11a2c65d7c5f0>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga4e93a985aa2a7812c7c11a2c65d7c5f0> foreign import ccall unsafe "Z3_mk_bvsgt" z3_mk_bvsgt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae774128fa5e9ff7458a36bd10e6ca0fa>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gae774128fa5e9ff7458a36bd10e6ca0fa> foreign import ccall unsafe "Z3_mk_concat" z3_mk_concat :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga32d2fe7563f3e6b114c1b97b205d4317>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga32d2fe7563f3e6b114c1b97b205d4317> foreign import ccall unsafe "Z3_mk_extract" z3_mk_extract :: Ptr Z3_context -> CUInt -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad29099270b36d0680bb54b560353c10e>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gad29099270b36d0680bb54b560353c10e> foreign import ccall unsafe "Z3_mk_sign_ext" z3_mk_sign_ext :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac9322fae11365a78640baf9078c428b3>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gac9322fae11365a78640baf9078c428b3> foreign import ccall unsafe "Z3_mk_zero_ext" z3_mk_zero_ext :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga03e81721502ea225c264d1f556c9119d>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga03e81721502ea225c264d1f556c9119d> foreign import ccall unsafe "Z3_mk_repeat" z3_mk_repeat :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8d5e776c786c1172fa0d7dfede454e1>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gac8d5e776c786c1172fa0d7dfede454e1> foreign import ccall unsafe "Z3_mk_bvshl" z3_mk_bvshl :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac59645a6edadad79a201f417e4e0c512>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gac59645a6edadad79a201f417e4e0c512> foreign import ccall unsafe "Z3_mk_bvlshr" z3_mk_bvlshr :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga674b580ad605ba1c2c9f9d3748be87c4>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga674b580ad605ba1c2c9f9d3748be87c4> foreign import ccall unsafe "Z3_mk_bvashr" z3_mk_bvashr :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4932b7d08fea079dd903cd857a52dcda>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga4932b7d08fea079dd903cd857a52dcda> foreign import ccall unsafe "Z3_mk_rotate_left" z3_mk_rotate_left :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3b94e1bf87ecd1a1858af8ebc1da4a1c>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga3b94e1bf87ecd1a1858af8ebc1da4a1c> foreign import ccall unsafe "Z3_mk_rotate_right" z3_mk_rotate_right :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf46f1cb80e5a56044591a76e7c89e5e7>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaf46f1cb80e5a56044591a76e7c89e5e7> foreign import ccall unsafe "Z3_mk_ext_rotate_left" z3_mk_ext_rotate_left :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabb227526c592b523879083f12aab281f>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gabb227526c592b523879083f12aab281f> foreign import ccall unsafe "Z3_mk_ext_rotate_right" z3_mk_ext_rotate_right :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga35f89eb05df43fbd9cce7200cc1f30b5>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga35f89eb05df43fbd9cce7200cc1f30b5> foreign import ccall unsafe "Z3_mk_int2bv" z3_mk_int2bv :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac87b227dc3821d57258d7f53a28323d4>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gac87b227dc3821d57258d7f53a28323d4> foreign import ccall unsafe "Z3_mk_bv2int" z3_mk_bv2int :: Ptr Z3_context -> Ptr Z3_ast -> Z3_bool -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga88f6b5ec876f05e0d7ba51e96c4b077f>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga88f6b5ec876f05e0d7ba51e96c4b077f> foreign import ccall unsafe "Z3_mk_bvadd_no_overflow" z3_mk_bvadd_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Z3_bool -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1e2b1927cf4e50000c1600d47a152947>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga1e2b1927cf4e50000c1600d47a152947> foreign import ccall unsafe "Z3_mk_bvadd_no_underflow" z3_mk_bvadd_no_underflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga785f8127b87e0b42130e6d8f52167d7c>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga785f8127b87e0b42130e6d8f52167d7c> foreign import ccall unsafe "Z3_mk_bvsub_no_overflow" z3_mk_bvsub_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6480850f9fa01e14aea936c88ff184c4>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga6480850f9fa01e14aea936c88ff184c4> foreign import ccall unsafe "Z3_mk_bvsub_no_underflow" z3_mk_bvsub_no_underflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa17e7b2c33dfe2abbd74d390927ae83e>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaa17e7b2c33dfe2abbd74d390927ae83e> foreign import ccall unsafe "Z3_mk_bvsdiv_no_overflow" z3_mk_bvsdiv_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae9c5d72605ddcd0e76657341eaccb6c7>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gae9c5d72605ddcd0e76657341eaccb6c7> foreign import ccall unsafe "Z3_mk_bvneg_no_overflow" z3_mk_bvneg_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga86f4415719d295a2f6845c70b3aaa1df>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga86f4415719d295a2f6845c70b3aaa1df> foreign import ccall unsafe "Z3_mk_bvmul_no_overflow" z3_mk_bvmul_no_overflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Z3_bool -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga501ccc01d737aad3ede5699741717fda>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga501ccc01d737aad3ede5699741717fda> foreign import ccall unsafe "Z3_mk_bvmul_no_underflow" z3_mk_bvmul_no_underflow :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) -------------------------------------------------------------------------------- -- * Arrays --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga38f423f3683379e7f597a7fe59eccb67>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga38f423f3683379e7f597a7fe59eccb67> foreign import ccall unsafe "Z3_mk_select" z3_mk_select :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae305a4f54b4a64f7e5973ae6ccb13593>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gae305a4f54b4a64f7e5973ae6ccb13593> foreign import ccall unsafe "Z3_mk_store" z3_mk_store :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga84ea6f0c32b99c70033feaa8f00e8f2d>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga84ea6f0c32b99c70033feaa8f00e8f2d> foreign import ccall unsafe "Z3_mk_const_array" z3_mk_const_array :: Ptr Z3_context -> Ptr Z3_sort -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9150242d9430a8c3d55d2ca3b9a4362d>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga9150242d9430a8c3d55d2ca3b9a4362d> foreign import ccall unsafe "Z3_mk_map" z3_mk_map :: Ptr Z3_context -> Ptr Z3_func_decl -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga78e89cca82f0ab4d5f4e662e5e5fba7d>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga78e89cca82f0ab4d5f4e662e5e5fba7d> foreign import ccall unsafe "Z3_mk_array_default" z3_mk_array_default :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) -------------------------------------------------------------------------------- -- * Sets --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga358b6b80509a567148f1c0ca9252118c>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga358b6b80509a567148f1c0ca9252118c> foreign import ccall unsafe "Z3_mk_empty_set" z3_mk_empty_set :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5e92662c657374f7332aa32ce4503dd2>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga5e92662c657374f7332aa32ce4503dd2> foreign import ccall unsafe "Z3_mk_full_set" z3_mk_full_set :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga856c3d0e28ce720f53912c2bbdd76175>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga856c3d0e28ce720f53912c2bbdd76175> foreign import ccall unsafe "Z3_mk_set_add" z3_mk_set_add :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga80e883f39dd3b88f9d0745c8a5b91d1d>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga80e883f39dd3b88f9d0745c8a5b91d1d> foreign import ccall unsafe "Z3_mk_set_del" z3_mk_set_del :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4050162a13d539b8913200963bb4743c>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga4050162a13d539b8913200963bb4743c> foreign import ccall unsafe "Z3_mk_set_union" z3_mk_set_union :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8a8abff0ebe6aeeaa6c919eaa013049d>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga8a8abff0ebe6aeeaa6c919eaa013049d> foreign import ccall unsafe "Z3_mk_set_intersect" z3_mk_set_intersect :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabb49c62f70b8198362e1a29ba6d8bde1>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gabb49c62f70b8198362e1a29ba6d8bde1> foreign import ccall unsafe "Z3_mk_set_difference" z3_mk_set_difference :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5c57143c9229cdf730c5103ff696590f>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga5c57143c9229cdf730c5103ff696590f> foreign import ccall unsafe "Z3_mk_set_complement" z3_mk_set_complement :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac6e516f3dce0bdd41095c6d6daf56063>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gac6e516f3dce0bdd41095c6d6daf56063> foreign import ccall unsafe "Z3_mk_set_member" z3_mk_set_member :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga139c5803af0e86464adc7cedc53e7f3a>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga139c5803af0e86464adc7cedc53e7f3a> foreign import ccall unsafe "Z3_mk_set_subset" z3_mk_set_subset :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --------------------------------------------------------------------- -- * Numerals --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8aca397e32ca33618d8024bff32948c>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gac8aca397e32ca33618d8024bff32948c> foreign import ccall unsafe "Z3_mk_numeral" z3_mk_numeral :: Ptr Z3_context -> Z3_string -> Ptr Z3_sort -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabe0bbc1e01a084a75506a62e5e6900b3>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gabe0bbc1e01a084a75506a62e5e6900b3> foreign import ccall unsafe "Z3_mk_real" z3_mk_real :: Ptr Z3_context -> CInt -> CInt -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8779204998136569c3e166c34cfd3e2c>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga8779204998136569c3e166c34cfd3e2c> foreign import ccall unsafe "Z3_mk_int" z3_mk_int :: Ptr Z3_context -> CInt -> Ptr Z3_sort -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7201b6231b61421c005457206760a121>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga7201b6231b61421c005457206760a121> foreign import ccall unsafe "Z3_mk_unsigned_int" z3_mk_unsigned_int :: Ptr Z3_context -> CUInt -> Ptr Z3_sort -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga42cc319787d485d9cb665d80e02d206f>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga42cc319787d485d9cb665d80e02d206f> foreign import ccall unsafe "Z3_mk_int64" z3_mk_int64 :: Ptr Z3_context -> CLLong -> Ptr Z3_sort -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga88a165138162a8bac401672f0a1b7891>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga88a165138162a8bac401672f0a1b7891> foreign import ccall unsafe "Z3_mk_unsigned_int64" z3_mk_unsigned_int64 :: Ptr Z3_context -> CULLong -> Ptr Z3_sort -> IO (Ptr Z3_ast) --------------------------------------------------------------------- -- * Quantifiers --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf15c95b66dc3b0af735774ee401a6f85>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaf15c95b66dc3b0af735774ee401a6f85> foreign import ccall unsafe "Z3_mk_pattern" z3_mk_pattern :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_pattern) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1d4da8849fca699b345322f8ee1fa31e>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga1d4da8849fca699b345322f8ee1fa31e> foreign import ccall unsafe "Z3_mk_bound" z3_mk_bound :: Ptr Z3_context -> CUInt -> Ptr Z3_sort -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7e975b7d7ac96de1db73d8f71166c663>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga7e975b7d7ac96de1db73d8f71166c663> foreign import ccall unsafe "Z3_mk_forall" z3_mk_forall :: Ptr Z3_context -> CUInt -> CUInt -> Ptr (Ptr Z3_pattern)@@ -706,7 +757,7 @@ -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Referece: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4ffce34ff9117e6243283f11d87c1407>+-- | Referece: <http://z3prover.github.io/api/html/group__capi.html#ga4ffce34ff9117e6243283f11d87c1407> foreign import ccall unsafe "Z3_mk_exists" z3_mk_exists :: Ptr Z3_context -> CUInt -> CUInt -> Ptr (Ptr Z3_pattern)@@ -716,7 +767,7 @@ -- TODO: Z3_mk_quantifier, Z3_mk_quantifier_ex --- | Reference <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabdb40b3ac220bce5a3801e6d29fb3bb6>+-- | Reference <http://z3prover.github.io/api/html/group__capi.html#gabdb40b3ac220bce5a3801e6d29fb3bb6> foreign import ccall unsafe "Z3_mk_forall_const" z3_mk_forall_const :: Ptr Z3_context -> CUInt@@ -727,7 +778,7 @@ -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2011bea0f4445d58ec4d7cefe4499ceb>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga2011bea0f4445d58ec4d7cefe4499ceb> foreign import ccall unsafe "Z3_mk_exists_const" z3_mk_exists_const :: Ptr Z3_context -> CUInt@@ -743,115 +794,143 @@ --------------------------------------------------------------------- -- * Accessors --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gadc82da786f3b558de8ded05bf6478902>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gadc82da786f3b558de8ded05bf6478902> foreign import ccall unsafe "Z3_func_decl_to_ast" z3_func_decl_to_ast :: Ptr Z3_context -> Ptr Z3_func_decl -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4c43608feea4cae363ef9c520c239a5c>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga4c43608feea4cae363ef9c520c239a5c> foreign import ccall unsafe "Z3_get_ast_kind" z3_get_ast_kind :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_ast_kind --- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae8ad520b79b46c323863bacffa0e12c0>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga87a4f9add28db792a24476a1082b4fe4>+foreign import ccall unsafe "Z3_is_app"+ z3_is_app :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_bool++-- Reference: <http://z3prover.github.io/api/html/group__capi.html#gae8ad520b79b46c323863bacffa0e12c0> foreign import ccall unsafe "Z3_get_app_num_args" z3_get_app_num_args :: Ptr Z3_context -> Ptr Z3_app -> IO CUInt --- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga49a576b11f9f6ca4a94670e538a84c6b>+-- Reference: <http://z3prover.github.io/api/html/group__capi.html#ga49a576b11f9f6ca4a94670e538a84c6b> foreign import ccall unsafe "Z3_get_app_arg" z3_get_app_arg :: Ptr Z3_context -> Ptr Z3_app -> CUInt -> IO (Ptr Z3_ast) --- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4ffab51c30484a32edc65194573cfd28>+-- Reference: <http://z3prover.github.io/api/html/group__capi.html#ga4ffab51c30484a32edc65194573cfd28> foreign import ccall unsafe "Z3_get_app_decl" z3_get_app_decl :: Ptr Z3_context -> Ptr Z3_app -> IO (Ptr Z3_func_decl) --- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae9ab82612fd84f5ce7991ade7d7ad920>+-- Reference: <http://z3prover.github.io/api/html/group__capi.html#gae9ab82612fd84f5ce7991ade7d7ad920> foreign import ccall unsafe "Z3_get_datatype_sort_num_constructors" z3_get_datatype_sort_num_constructors :: Ptr Z3_context -> Ptr Z3_sort -> IO CUInt --- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa5630cbd0f28d2bda21dc5376fe86a9b>+-- Reference: <http://z3prover.github.io/api/html/group__capi.html#gaa5630cbd0f28d2bda21dc5376fe86a9b> foreign import ccall unsafe "Z3_get_datatype_sort_constructor" z3_get_datatype_sort_constructor :: Ptr Z3_context -> Ptr Z3_sort -> CUInt -> IO (Ptr Z3_func_decl) --- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacf79f46d05b3ed69684d47eaf242319c>+-- Reference: <http://z3prover.github.io/api/html/group__capi.html#gacf79f46d05b3ed69684d47eaf242319c> foreign import ccall unsafe "Z3_get_datatype_sort_recognizer" z3_get_datatype_sort_recognizer :: Ptr Z3_context -> Ptr Z3_sort -> CUInt -> IO (Ptr Z3_func_decl) --- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab0ade72138d0479409f47cef21972eb2>+-- Reference: <http://z3prover.github.io/api/html/group__capi.html#gab0ade72138d0479409f47cef21972eb2> foreign import ccall unsafe "Z3_get_datatype_sort_constructor_accessor" z3_get_datatype_sort_constructor_accessor :: Ptr Z3_context -> Ptr Z3_sort -> CUInt -> CUInt -> IO (Ptr Z3_func_decl) --- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga741b1bf11cb92aa2ec9ef2fef73ff129>+-- Reference: <http://z3prover.github.io/api/html/group__capi.html#ga741b1bf11cb92aa2ec9ef2fef73ff129> foreign import ccall unsafe "Z3_get_decl_name" z3_get_decl_name :: Ptr Z3_context -> Ptr Z3_func_decl -> IO (Ptr Z3_symbol) --- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf1683d9464f377e5089ce6ebf2a9bd31>+-- Reference: <http://z3prover.github.io/api/html/group__capi.html#gaf1683d9464f377e5089ce6ebf2a9bd31> foreign import ccall unsafe "Z3_get_symbol_string" z3_get_symbol_string :: Ptr Z3_context -> Ptr Z3_symbol -> IO Z3_string --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8fc3550edace7bc046e16d1f96ddb419>+-- Reference: <http://z3prover.github.io/api/html/group__capi.html#gacd85d48842c7bfaa696596d16875681a>+foreign import ccall unsafe "Z3_get_sort_kind"+ z3_get_sort_kind :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_sort_kind++-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga8fc3550edace7bc046e16d1f96ddb419> foreign import ccall unsafe "Z3_get_bv_sort_size" z3_get_bv_sort_size :: Ptr Z3_context -> Ptr Z3_sort -> IO CUInt --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae259256eb0f2c10e48fc6227760b7fda>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gae259256eb0f2c10e48fc6227760b7fda> foreign import ccall unsafe "Z3_app_to_ast" z3_app_to_ast :: Ptr Z3_context -> Ptr Z3_app -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0a4dac7e9397ff067136354cd33cb933>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga0a4dac7e9397ff067136354cd33cb933> foreign import ccall unsafe "Z3_get_sort" z3_get_sort :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_sort) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga133aaa1ec31af9b570ed7627a3c8c5a4>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga133aaa1ec31af9b570ed7627a3c8c5a4> foreign import ccall unsafe "Z3_get_bool_value" z3_get_bool_value :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_lbool --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94617ef18fa7157e1a3f85db625d2f4b>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga94617ef18fa7157e1a3f85db625d2f4b> foreign import ccall unsafe "Z3_get_numeral_string" z3_get_numeral_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_string --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf9345fd0822d7e9928dd4ab14a09765b>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga203f32e3b904955f703f61f91a8626a4>+foreign import ccall unsafe "Z3_get_arity"+ z3_get_arity :: Ptr Z3_context -> Ptr Z3_func_decl -> IO CUInt++-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gad025402a9cac1a8d8facddba3f8cbddc>+foreign import ccall unsafe "Z3_get_domain"+ z3_get_domain :: Ptr Z3_context -> Ptr Z3_func_decl -> CUInt -> IO (Ptr Z3_sort)++-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga913ecf28cd4bddc8255f77f80b6aafe9>+foreign import ccall unsafe "Z3_get_range"+ z3_get_range :: Ptr Z3_context -> Ptr Z3_func_decl -> IO (Ptr Z3_sort)++-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaf9345fd0822d7e9928dd4ab14a09765b> foreign import ccall unsafe "Z3_to_app" z3_to_app :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_app) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafe4334258b639fa1f8754375b9b56fd7>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gafe4334258b639fa1f8754375b9b56fd7> foreign import ccall unsafe "Z3_pattern_to_ast" z3_pattern_to_ast :: Ptr Z3_context -> Ptr Z3_pattern -> IO (Ptr Z3_ast) +-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gada433553406475e5dd6a494ea957844c>+foreign import ccall unsafe "Z3_simplify"+ z3_simplify :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)++-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga34329d4c83ca8c98e18b2884b679008c>+foreign import ccall unsafe "Z3_simplify_ex"+ z3_simplify_ex :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_params -> IO (Ptr Z3_ast)+ -- TODO Modifiers --------------------------------------------------------------------- -- * AST vectors --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga99d6a99e914fcb11e5dcf9fcc3584425>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga99d6a99e914fcb11e5dcf9fcc3584425> foreign import ccall unsafe "Z3_ast_vector_size" z3_ast_vector_size :: Ptr Z3_context -> Ptr Z3_ast_vector -> IO CUInt --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3a90216036017ce16db63fb3aa5f6047>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga3a90216036017ce16db63fb3aa5f6047> foreign import ccall unsafe "Z3_ast_vector_get" z3_ast_vector_get :: Ptr Z3_context -> Ptr Z3_ast_vector -> CUInt -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaea0024e05e6f82434ff31e6ec6fab432>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaea0024e05e6f82434ff31e6ec6fab432> foreign import ccall unsafe "Z3_ast_vector_inc_ref" z3_ast_vector_inc_ref :: Ptr Z3_context -> Ptr Z3_ast_vector -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab0e22d719f55f93fb8788fa4534cc342>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gab0e22d719f55f93fb8788fa4534cc342> foreign import ccall unsafe "Z3_ast_vector_dec_ref" z3_ast_vector_dec_ref :: Ptr Z3_context -> Ptr Z3_ast_vector -> IO () --------------------------------------------------------------------- -- * Models --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac06a904e7ac6209d8019c606412d3cec>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gac06a904e7ac6209d8019c606412d3cec> foreign import ccall unsafe "Z3_model_inc_ref" z3_model_inc_ref :: Ptr Z3_context -> Ptr Z3_model -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacc2df0767d4a94d7216d3db49c41547f>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gacc2df0767d4a94d7216d3db49c41547f> foreign import ccall unsafe "Z3_model_dec_ref" z3_model_dec_ref :: Ptr Z3_context -> Ptr Z3_model -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga86670c291a16640b932e7892176a9d1b>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga86670c291a16640b932e7892176a9d1b> foreign import ccall unsafe "Z3_model_eval" z3_model_eval :: Ptr Z3_context -> Ptr Z3_model@@ -860,87 +939,87 @@ -> Ptr (Ptr Z3_ast) -> IO Z3_bool --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4674da67d226bfb16861829b9f129cfa>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga4674da67d226bfb16861829b9f129cfa> foreign import ccall unsafe "Z3_is_as_array" z3_is_as_array :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_bool --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7d9262dc6e79f2aeb23fd4a383589dda>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga7d9262dc6e79f2aeb23fd4a383589dda> foreign import ccall unsafe "Z3_get_as_array_func_decl" z3_get_as_array_func_decl :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_func_decl) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafb9cc5eca9564d8a849c154c5a4a8633>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gafb9cc5eca9564d8a849c154c5a4a8633> foreign import ccall unsafe "Z3_model_get_func_interp" z3_model_get_func_interp :: Ptr Z3_context -> Ptr Z3_model -> Ptr Z3_func_decl -> IO (Ptr Z3_func_interp) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga80218e1d50bdc4dac5ba18bd13a8ddfb>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga80218e1d50bdc4dac5ba18bd13a8ddfb> foreign import ccall unsafe "Z3_func_interp_inc_ref" z3_func_interp_inc_ref :: Ptr Z3_context -> Ptr Z3_func_interp -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabe3aefc84db4fc3ce5349e958f1ec34b>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gabe3aefc84db4fc3ce5349e958f1ec34b> foreign import ccall unsafe "Z3_func_interp_dec_ref" z3_func_interp_dec_ref :: Ptr Z3_context -> Ptr Z3_func_interp -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2bab9ae1444940e7593729beec279844>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga2bab9ae1444940e7593729beec279844> foreign import ccall unsafe "Z3_func_interp_get_num_entries" z3_func_interp_get_num_entries :: Ptr Z3_context -> Ptr Z3_func_interp -> IO CUInt --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf157e1e1cd8c0cfe6a21be6370f659da>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaf157e1e1cd8c0cfe6a21be6370f659da> foreign import ccall unsafe "Z3_func_interp_get_entry" z3_func_interp_get_entry :: Ptr Z3_context -> Ptr Z3_func_interp -> CUInt -> IO (Ptr Z3_func_entry) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46de7559826ba71b8488d727cba1fb64>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga46de7559826ba71b8488d727cba1fb64> foreign import ccall unsafe "Z3_func_interp_get_else" z3_func_interp_get_else :: Ptr Z3_context -> Ptr Z3_func_interp -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaca22cbdb6f7787aaae5d814f2ab383d8>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaca22cbdb6f7787aaae5d814f2ab383d8> foreign import ccall unsafe "Z3_func_interp_get_arity" z3_func_interp_get_arity :: Ptr Z3_context -> Ptr Z3_func_interp -> IO CUInt --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga82cd36e7b02c432436950d5c2301245e>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga82cd36e7b02c432436950d5c2301245e> foreign import ccall unsafe "Z3_func_entry_inc_ref" z3_func_entry_inc_ref :: Ptr Z3_context -> Ptr Z3_func_entry -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9a9a2a75d7fc3d842839662e53365903>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga9a9a2a75d7fc3d842839662e53365903> foreign import ccall unsafe "Z3_func_entry_dec_ref" z3_func_entry_dec_ref :: Ptr Z3_context -> Ptr Z3_func_entry -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9fd65e2ab039aa8e40608c2ecf7084da>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga9fd65e2ab039aa8e40608c2ecf7084da> foreign import ccall unsafe "Z3_func_entry_get_value" z3_func_entry_get_value :: Ptr Z3_context -> Ptr Z3_func_entry -> IO (Ptr Z3_ast) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga51aed8c5bc4b1f53f0c371312de3ce1a>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga51aed8c5bc4b1f53f0c371312de3ce1a> foreign import ccall unsafe "Z3_func_entry_get_num_args" z3_func_entry_get_num_args :: Ptr Z3_context -> Ptr Z3_func_entry -> IO CUInt --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6fe03fe3c824fceb52766a4d8c2cbeab>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga6fe03fe3c824fceb52766a4d8c2cbeab> foreign import ccall unsafe "Z3_func_entry_get_arg" z3_func_entry_get_arg :: Ptr Z3_context -> Ptr Z3_func_entry@@ -955,7 +1034,7 @@ -- TODO Constraints: Z3_check_assumptions -- TODO Constraints: Z3_get_implied_equalities --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf36d49862a8c0d20dd5e6508eef5f8af>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaf36d49862a8c0d20dd5e6508eef5f8af> foreign import ccall unsafe "Z3_model_to_string" z3_model_to_string :: Ptr Z3_context -> Ptr Z3_model -> IO Z3_string @@ -965,148 +1044,194 @@ --------------------------------------------------------------------- -- * Parameters --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac7f883536538ab0ad234fde58988e673>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gac7f883536538ab0ad234fde58988e673> foreign import ccall unsafe "Z3_mk_params" z3_mk_params :: Ptr Z3_context -> IO (Ptr Z3_params) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3a91c9f749b89e1dcf1493177d395d0c>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga3a91c9f749b89e1dcf1493177d395d0c> foreign import ccall unsafe "Z3_params_inc_ref" z3_params_inc_ref :: Ptr Z3_context -> Ptr Z3_params -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae4df28ba713b81ee99abd929e32484ea>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gae4df28ba713b81ee99abd929e32484ea> foreign import ccall unsafe "Z3_params_dec_ref" z3_params_dec_ref :: Ptr Z3_context -> Ptr Z3_params -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga39e3df967eaad45b343256d56c54e91c>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga39e3df967eaad45b343256d56c54e91c> foreign import ccall unsafe "Z3_params_set_bool" z3_params_set_bool :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> Z3_bool -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4974397cb652c7f7f479012eb465e250>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga4974397cb652c7f7f479012eb465e250> foreign import ccall unsafe "Z3_params_set_uint" z3_params_set_uint :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> CUInt -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga11498ce4b25d294f5f89ab7ac1b74c62>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga11498ce4b25d294f5f89ab7ac1b74c62> foreign import ccall unsafe "Z3_params_set_double" z3_params_set_double :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> CDouble -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac2e899a4906b6133a23fdb60ef992ec9>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gac2e899a4906b6133a23fdb60ef992ec9> foreign import ccall unsafe "Z3_params_set_symbol" z3_params_set_symbol :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> Ptr Z3_symbol -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga624e692e180a8b2f617156b1e1ae9722>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga624e692e180a8b2f617156b1e1ae9722> foreign import ccall unsafe "Z3_params_to_string" z3_params_to_string :: Ptr Z3_context -> Ptr Z3_params -> IO Z3_string ---------------------------------------------------------------------+-- * Interpolation++-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga0d5e342cd83ed43185bcfdc583513959>+foreign import ccall unsafe "Z3_mk_interpolant"+ z3_mk_interpolant :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)++-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga1fd3d3fe7bc4426c4787c3cc8cf92864>+foreign import ccall unsafe "Z3_mk_interpolation_context"+ z3_mk_interpolation_context :: Ptr Z3_config -> IO (Ptr Z3_context)++-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gad4417737993c62d39a6624118427f506>+foreign import ccall unsafe "Z3_get_interpolant"+ z3_get_interpolant :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast+ -> Ptr Z3_params -> IO (Ptr Z3_ast_vector)++-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaf62f6b456349886273e15d3cfe8656fe>+foreign import ccall unsafe "Z3_compute_interpolant"+ z3_compute_interpolant :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_params+ -> Ptr (Ptr Z3_ast_vector) -> Ptr (Ptr Z3_model)+ -> IO Z3_lbool++-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga2bf6a92d53d65fc32163792bedd5d31f>+foreign import ccall unsafe "Z3_read_interpolation_problem"+ z3_read_interpolation_problem :: Ptr Z3_context -> Ptr CUInt -> Ptr (Ptr Z3_ast)+ -> Ptr (Ptr CUInt) -> Ptr CChar -> Ptr Z3_string+ -- TODO: report "inexact" result type+ -> Ptr CUInt -> Ptr (Ptr Z3_ast) -> IO Z3_bool++-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gadf50d7093abe5a892593baef552bbf89>+foreign import ccall unsafe "Z3_check_interpolant"+ z3_check_interpolant :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> Ptr CUInt+ -> Ptr (Ptr Z3_ast) -> Ptr Z3_string -> CUInt+ -- TODO: report "inexact" result type+ -> Ptr (Ptr Z3_ast) -> IO Z3_lbool++-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gad45c5746cd1eefe4f2fc6df956c9cd8e>+foreign import ccall unsafe "Z3_interpolation_profile"+ z3_interpolation_profile :: Ptr Z3_context -> IO Z3_string++-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga2a8ee59130e23e10568a1f70e387c608>+foreign import ccall unsafe "Z3_write_interpolation_problem"+ z3_write_interpolation_problem :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast)+ -> Ptr CUInt -> Ptr CChar -> CUInt+ -> Ptr (Ptr Z3_ast) -> IO ()++--------------------------------------------------------------------- -- * Solvers --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5735499ef0b46846c5d45982eaa0e74c>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga5735499ef0b46846c5d45982eaa0e74c> foreign import ccall unsafe "Z3_mk_solver" z3_mk_solver :: Ptr Z3_context -> IO (Ptr Z3_solver) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5735499ef0b46846c5d45982eaa0e74c>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga5735499ef0b46846c5d45982eaa0e74c> foreign import ccall unsafe "Z3_mk_simple_solver" z3_mk_simple_solver :: Ptr Z3_context -> IO (Ptr Z3_solver) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga54244cfc9d9cd2ca8f08c3909d700628>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga54244cfc9d9cd2ca8f08c3909d700628> foreign import ccall unsafe "Z3_mk_solver_for_logic" z3_mk_solver_for_logic :: Ptr Z3_context -> Ptr Z3_symbol -> IO (Ptr Z3_solver) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga047bb9dff9d57c7d3a71b7af4555956b>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga047bb9dff9d57c7d3a71b7af4555956b> foreign import ccall unsafe "Z3_solver_get_help" z3_solver_get_help :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_string --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga887441b3468a1bc605bbf564ddebf2ae>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga887441b3468a1bc605bbf564ddebf2ae> foreign import ccall unsafe "Z3_solver_set_params" z3_solver_set_params :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_params -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga388e25a8b477abbd49f08c6c29dfa12d>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga388e25a8b477abbd49f08c6c29dfa12d> foreign import ccall unsafe "Z3_solver_inc_ref" z3_solver_inc_ref :: Ptr Z3_context -> Ptr Z3_solver -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2362dcef4e9b8ede41298a50428902ff>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga2362dcef4e9b8ede41298a50428902ff> foreign import ccall unsafe "Z3_solver_dec_ref" z3_solver_dec_ref :: Ptr Z3_context -> Ptr Z3_solver -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae41bebe15b1b1105f9abb8690188d1e2>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gae41bebe15b1b1105f9abb8690188d1e2> foreign import ccall unsafe "Z3_solver_push" z3_solver_push :: Ptr Z3_context -> Ptr Z3_solver -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga40aa98e15aceffa5be3afad2e065478a>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga40aa98e15aceffa5be3afad2e065478a> foreign import ccall unsafe "Z3_solver_pop" z3_solver_pop :: Ptr Z3_context -> Ptr Z3_solver -> CUInt -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafd4b4a6465601835341b477b75725b28>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gafd4b4a6465601835341b477b75725b28> foreign import ccall unsafe "Z3_solver_get_num_scopes" z3_solver_get_num_scopes :: Ptr Z3_context -> Ptr Z3_solver -> IO CUInt --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4a4a215b9130d7980e3c393fe857335f>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga4a4a215b9130d7980e3c393fe857335f> foreign import ccall unsafe "Z3_solver_reset" z3_solver_reset :: Ptr Z3_context -> Ptr Z3_solver -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga72afadf5e8b216f2c6ae675e872b8be4>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga72afadf5e8b216f2c6ae675e872b8be4> foreign import ccall unsafe "Z3_solver_assert" z3_solver_assert :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_ast -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf46fb6f3aa3ef451d6be01a737697810>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaf46fb6f3aa3ef451d6be01a737697810> foreign import ccall unsafe "Z3_solver_assert_and_track" z3_solver_assert_and_track :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_ast -> Ptr Z3_ast -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga000e369de7b71caa4ee701089709c526>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga000e369de7b71caa4ee701089709c526> foreign import ccall unsafe "Z3_solver_check" z3_solver_check :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_lbool --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga45b40829aaa382bbf427a744911452f9>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga45b40829aaa382bbf427a744911452f9> foreign import ccall unsafe "Z3_solver_check_assumptions" z3_solver_check_assumptions :: Ptr Z3_context -> Ptr Z3_solver -> CUInt -> Ptr (Ptr Z3_ast) -> IO Z3_lbool --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf14a54d904a7e45eecc00c5fb8a9d5c9>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaf14a54d904a7e45eecc00c5fb8a9d5c9> foreign import ccall unsafe "Z3_solver_get_model" z3_solver_get_model :: Ptr Z3_context -> Ptr Z3_solver -> IO (Ptr Z3_model) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabb4f8ed6a09873f5aeefe9cc01010864>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gabb4f8ed6a09873f5aeefe9cc01010864> foreign import ccall unsafe "Z3_solver_get_unsat_core" z3_solver_get_unsat_core :: Ptr Z3_context -> Ptr Z3_solver -> IO (Ptr Z3_ast_vector) --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaed5d19000004b43dd75e487682e91b55>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaed5d19000004b43dd75e487682e91b55> foreign import ccall unsafe "Z3_solver_get_reason_unknown" z3_solver_get_reason_unknown :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_string --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf52e41db4b12a84188b80255454d3abb>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaf52e41db4b12a84188b80255454d3abb> foreign import ccall unsafe "Z3_solver_to_string" z3_solver_to_string :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_string --------------------------------------------------------------------- -- * String Conversion --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga20d66dac19b6d6a06537843d0e25f761>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga20d66dac19b6d6a06537843d0e25f761> foreign import ccall unsafe "Z3_set_ast_print_mode" z3_set_ast_print_mode :: Ptr Z3_context -> Z3_ast_print_mode -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab1aa4b78298fe00b3167bf7bfd88aea3>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gab1aa4b78298fe00b3167bf7bfd88aea3> foreign import ccall unsafe "Z3_ast_to_string" z3_ast_to_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_string --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga51b048ddbbcd88708e7aa4fe1c2462d6>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga51b048ddbbcd88708e7aa4fe1c2462d6> foreign import ccall unsafe "Z3_pattern_to_string" z3_pattern_to_string :: Ptr Z3_context -> Ptr Z3_pattern -> IO Z3_string --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf90c72f63eab298e1dd750f6a26fb945>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaf90c72f63eab298e1dd750f6a26fb945> foreign import ccall unsafe "Z3_sort_to_string" z3_sort_to_string :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_string --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga15243dcad77f5571e28e8aa1da465675>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga15243dcad77f5571e28e8aa1da465675> foreign import ccall unsafe "Z3_func_decl_to_string" z3_func_decl_to_string :: Ptr Z3_context -> Ptr Z3_func_decl -> IO Z3_string --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf93844a5964ad8dee609fac3470d86e4>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaf93844a5964ad8dee609fac3470d86e4> foreign import ccall unsafe "Z3_benchmark_to_smtlib_string" z3_benchmark_to_smtlib_string :: Ptr Z3_context -> Z3_string -- ^ name@@ -1121,29 +1246,29 @@ --------------------------------------------------------------------- -- * Error Handling --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8ac771e68b28d2c86f40aa84889b3807>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga8ac771e68b28d2c86f40aa84889b3807> foreign import ccall unsafe "Z3_get_error_code" z3_get_error_code :: Ptr Z3_context -> IO Z3_error_code --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gadaa12e9990f37b0c1e2bf1dd502dbf39>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gadaa12e9990f37b0c1e2bf1dd502dbf39> foreign import ccall unsafe "Z3_set_error_handler" z3_set_error_handler :: Ptr Z3_context -> FunPtr Z3_error_handler -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga41cf70319c4802ab7301dd168d6f5e45>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga41cf70319c4802ab7301dd168d6f5e45> foreign import ccall unsafe "Z3_set_error" z3_set_error :: Ptr Z3_context -> Z3_error_code -> IO () --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf06357c49299efb8a0bdaeb3bc96c6d6>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaf06357c49299efb8a0bdaeb3bc96c6d6> foreign import ccall unsafe "Z3_get_error_msg" z3_get_error_msg :: Z3_error_code -> IO Z3_string --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae0aba52b5738b2ea78e0d6ad67ef1f92>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gae0aba52b5738b2ea78e0d6ad67ef1f92> foreign import ccall unsafe "Z3_get_error_msg_ex" z3_get_error_msg_ex :: Ptr Z3_context -> Z3_error_code -> IO Z3_string --------------------------------------------------------------------- -- * Miscellaneous --- | Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga45fcd18a00379b13a536c5b6117190ae>+-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga45fcd18a00379b13a536c5b6117190ae> foreign import ccall unsafe "Z3_get_version" z3_get_version :: Ptr CUInt -> Ptr CUInt -> Ptr CUInt -> Ptr CUInt -> IO ()
src/Z3/Monad.hs view
@@ -24,6 +24,7 @@ -- ** Z3 enviroments , Z3Env , newEnv+ , newItpEnv , evalZ3WithEnv -- * Types@@ -40,6 +41,7 @@ , FuncEntry , Params , Solver+ , SortKind(..) , ASTKind(..) -- ** Satisfiability result , Result(..)@@ -66,6 +68,7 @@ , mkTupleSort , mkConstructor , mkDatatype+ , mkDatatypes , mkSetSort -- * Constants and Applications@@ -213,15 +216,28 @@ -- * Accessors , getSymbolString+ , getSortKind , getBvSortSize , getDatatypeSortConstructors , getDatatypeSortRecognizers+ , getDatatypeSortConstructorAccessors , getDeclName+ , getArity+ , getDomain+ , getRange+ , appToAst+ , getAppDecl+ , getAppNumArgs+ , getAppArg+ , getAppArgs , getSort , getBoolValue , getAstKind+ , isApp , toApp , getNumeralString+ , simplify+ , simplifyEx -- ** Helpers , getBool , getInt@@ -272,6 +288,17 @@ , Version(..) , getVersion + -- * Interpolation+ , Base.InterpolationProblem(..)+ , mkInterpolant+ , Base.mkInterpolationContext+ , getInterpolant+ , computeInterpolant+ , readInterpolationProblem+ , checkInterpolant+ , interpolationProfile+ , writeInterpolationProblem+ -- * Solvers , solverGetHelp , solverSetParams@@ -322,6 +349,7 @@ , Version(..) , Params , Solver+ , SortKind(..) , ASTKind(..) ) import qualified Z3.Base as Base@@ -418,15 +446,22 @@ evalZ3 :: Z3 a -> IO a evalZ3 = evalZ3With Nothing stdOpts --- | Create a new Z3 environment.-newEnv :: Maybe Logic -> Opts -> IO Z3Env-newEnv mbLogic opts =++newEnvWith :: (Base.Config -> IO Base.Context) -> Maybe Logic -> Opts -> IO Z3Env+newEnvWith mkContext mbLogic opts = Base.withConfig $ \cfg -> do setOpts cfg opts- ctx <- Base.mkContext cfg+ ctx <- mkContext cfg solver <- maybe (Base.mkSolver ctx) (Base.mkSolverForLogic ctx) mbLogic return $ Z3Env solver ctx +-- | Create a new Z3 environment.+newEnv :: Maybe Logic -> Opts -> IO Z3Env+newEnv = newEnvWith Base.mkContext++newItpEnv :: Maybe Logic -> Opts -> IO Z3Env+newItpEnv = newEnvWith Base.mkInterpolationContext+ -- | Eval a Z3 script with a given environment. -- -- Environments may facilitate running many queries under the same@@ -560,6 +595,15 @@ -> z3 Sort mkDatatype = liftFun2 Base.mkDatatype +-- | Create mutually recursive datatypes, such as a tree and forest.+--+-- Returns the datatype sorts+mkDatatypes :: MonadZ3 z3+ => [Symbol]+ -> [[Constructor]]+ -> z3 [Sort]+mkDatatypes = liftFun2 Base.mkDatatypes+ -- | Create a set type -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6865879523e7e882d7e50a2d8445ac8b>@@ -1350,6 +1394,12 @@ getSymbolString :: MonadZ3 z3 => Symbol -> z3 String getSymbolString = liftFun1 Base.getSymbolString +-- | Return the sort kind.+--+-- Reference: <http://z3prover.github.io/api/html/group__capi.html#gacd85d48842c7bfaa696596d16875681a>+getSortKind :: MonadZ3 z3 => Sort -> z3 SortKind+getSortKind = liftFun1 Base.getSortKind+ -- | Return the size of the given bit-vector sort. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8fc3550edace7bc046e16d1f96ddb419>@@ -1368,12 +1418,53 @@ -> z3 [FuncDecl] -- ^ Constructor recognizers. getDatatypeSortRecognizers = liftFun1 Base.getDatatypeSortRecognizers +-- | Get list of accessors for datatype.+getDatatypeSortConstructorAccessors :: MonadZ3 z3+ => Sort -- ^ Datatype sort.+ -> z3 [[FuncDecl]] -- ^ Constructor recognizers.+getDatatypeSortConstructorAccessors = liftFun1 Base.getDatatypeSortConstructorAccessors+ -- | Return the constant declaration name as a symbol. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga741b1bf11cb92aa2ec9ef2fef73ff129> getDeclName :: MonadZ3 z3 => FuncDecl -> z3 Symbol getDeclName = liftFun1 Base.getDeclName +-- | Returns the number of parameters of the given declaration+getArity :: MonadZ3 z3 => FuncDecl -> z3 Int+getArity = liftFun1 Base.getArity++-- | Returns the sort of the i-th parameter of the given function declaration+getDomain :: MonadZ3 z3+ => FuncDecl -- ^ A function declaration+ -> Int -- ^ i+ -> z3 Sort+getDomain = liftFun2 Base.getDomain++-- | Returns the range of the given declaration.+getRange :: MonadZ3 z3 => FuncDecl -> z3 Sort+getRange = liftFun1 Base.getRange++-- | Convert an app into AST. This is just type casting.+appToAst :: MonadZ3 z3 => App -> z3 AST+appToAst = liftFun1 Base.appToAst++-- | Return the declaration of a constant or function application.+getAppDecl :: MonadZ3 z3 => App -> z3 FuncDecl+getAppDecl = liftFun1 Base.getAppDecl++-- | Return the number of argument of an application. If t is an constant, then the number of arguments is 0.+getAppNumArgs :: MonadZ3 z3 => App -> z3 Int+getAppNumArgs = liftFun1 Base.getAppNumArgs++-- | Return the i-th argument of the given application.+getAppArg :: MonadZ3 z3 => App -> Int -> z3 AST+getAppArg = liftFun2 Base.getAppArg++-- | Return a list of all the arguments of the given application.+getAppArgs :: MonadZ3 z3 => App -> z3 [AST]+getAppArgs = liftFun1 Base.getAppArgs+ -- | Return the sort of an AST node. getSort :: MonadZ3 z3 => AST -> z3 Sort getSort = liftFun1 Base.getSort@@ -1390,6 +1481,10 @@ getAstKind :: MonadZ3 z3 => AST -> z3 ASTKind getAstKind = liftFun1 Base.getAstKind +-- | Return True if an ast is APP_AST, False otherwise.+isApp :: MonadZ3 z3 => AST -> z3 Bool+isApp = liftFun1 Base.isApp+ -- | Cast AST into an App. toApp :: MonadZ3 z3 => AST -> z3 App toApp = liftFun1 Base.toApp@@ -1398,6 +1493,18 @@ getNumeralString :: MonadZ3 z3 => AST -> z3 String getNumeralString = liftFun1 Base.getNumeralString +-- | Simplify the expression.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gada433553406475e5dd6a494ea957844c>+simplify :: MonadZ3 z3 => AST -> z3 AST+simplify = liftFun1 Base.simplify++-- | Simplify the expression using the given parameters.+--+-- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga34329d4c83ca8c98e18b2884b679008c>+simplifyEx :: MonadZ3 z3 => AST -> Params -> z3 AST+simplifyEx = liftFun2 Base.simplifyEx+ ------------------------------------------------- -- ** Helpers @@ -1619,6 +1726,32 @@ -- | Return Z3 version number information. getVersion :: MonadZ3 z3 => z3 Version getVersion = liftIO Base.getVersion+++---------------------------------------------------------------------+-- * Interpolation++mkInterpolant :: MonadZ3 z3 => AST -> z3 AST+mkInterpolant = liftFun1 Base.mkInterpolant++getInterpolant :: MonadZ3 z3 => AST -> AST -> Params -> z3 [AST]+getInterpolant = liftFun3 Base.getInterpolant++computeInterpolant :: MonadZ3 z3 => AST -> Params+ -> z3 (Maybe (Either Model [AST]))+computeInterpolant = liftFun2 Base.computeInterpolant++readInterpolationProblem :: MonadZ3 z3 => FilePath -> z3 (Either String Base.InterpolationProblem)+readInterpolationProblem = liftFun1 Base.readInterpolationProblem++checkInterpolant :: MonadZ3 z3 => Base.InterpolationProblem -> [AST] -> z3 (Result, Maybe String)+checkInterpolant = liftFun2 Base.checkInterpolant++interpolationProfile :: MonadZ3 z3 => z3 String+interpolationProfile = liftScalar Base.interpolationProfile++writeInterpolationProblem :: MonadZ3 z3 => FilePath -> Base.InterpolationProblem -> z3 ()+writeInterpolationProblem = liftFun2 Base.writeInterpolationProblem --------------------------------------------------------------------- -- * Solvers
z3.cabal view
@@ -1,8 +1,8 @@ Name: z3-Version: 4.1.0+Version: 4.1.1 Synopsis: Bindings for the Z3 Theorem Prover Description:- Bindings for the (now open source!) Z3 4./x/ Theorem Prover (<https://github.com/Z3Prover/z3>).+ Bindings for the Z3 4./x/ Theorem Prover (<https://github.com/Z3Prover/z3>). . * "Z3.Base.C" provides the raw foreign imports from Z3's C API. .@@ -29,7 +29,7 @@ Author: Iago Abal <mail@iagoabal.eu>, David Castro <david.castro.dcp@gmail.com> Maintainer: Iago Abal <mail@iagoabal.eu>-Copyright: 2012-2015, Iago Abal, David Castro+Copyright: 2012-2017, Iago Abal, David Castro Category: Math, SMT, Theorem Provers, Formal Methods, Bit vectors Build-type: Simple Cabal-version: >= 1.8@@ -98,6 +98,15 @@ Hs-source-dirs: examples Main-Is: Examples.hs + Other-Modules: Example.Monad.Queens4+ Example.Monad.Queens4All+ Example.Monad.DataTypes+ Example.Monad.FuncModel+ Example.Monad.MutuallyRecursive+ Example.Monad.ToSMTLib+ Example.Monad.Tuple+ Example.Monad.Interpolation+ Test-suite spec Type: exitcode-stdio-1.0@@ -113,6 +122,6 @@ Other-modules: Z3.Base.Spec Build-depends: base >= 4.5,- z3 == 4.*,+ z3, hspec >= 2.1, QuickCheck >= 2.5.1