diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -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. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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 diff --git a/examples/Example/Monad/DataTypes.hs b/examples/Example/Monad/DataTypes.hs new file mode 100644 --- /dev/null +++ b/examples/Example/Monad/DataTypes.hs @@ -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 diff --git a/examples/Example/Monad/FuncModel.hs b/examples/Example/Monad/FuncModel.hs new file mode 100644 --- /dev/null +++ b/examples/Example/Monad/FuncModel.hs @@ -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) + diff --git a/examples/Example/Monad/Interpolation.hs b/examples/Example/Monad/Interpolation.hs new file mode 100644 --- /dev/null +++ b/examples/Example/Monad/Interpolation.hs @@ -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" diff --git a/examples/Example/Monad/MutuallyRecursive.hs b/examples/Example/Monad/MutuallyRecursive.hs new file mode 100644 --- /dev/null +++ b/examples/Example/Monad/MutuallyRecursive.hs @@ -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 diff --git a/examples/Example/Monad/Queens4.hs b/examples/Example/Monad/Queens4.hs new file mode 100644 --- /dev/null +++ b/examples/Example/Monad/Queens4.hs @@ -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) diff --git a/examples/Example/Monad/Queens4All.hs b/examples/Example/Monad/Queens4All.hs new file mode 100644 --- /dev/null +++ b/examples/Example/Monad/Queens4All.hs @@ -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) diff --git a/examples/Example/Monad/ToSMTLib.hs b/examples/Example/Monad/ToSMTLib.hs new file mode 100644 --- /dev/null +++ b/examples/Example/Monad/ToSMTLib.hs @@ -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) diff --git a/examples/Example/Monad/Tuple.hs b/examples/Example/Monad/Tuple.hs new file mode 100644 --- /dev/null +++ b/examples/Example/Monad/Tuple.hs @@ -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" diff --git a/examples/Examples.hs b/examples/Examples.hs --- a/examples/Examples.hs +++ b/examples/Examples.hs @@ -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 ) ] diff --git a/src/Z3/Base.hs b/src/Z3/Base.hs --- a/src/Z3/Base.hs +++ b/src/Z3/Base.hs @@ -13,7 +13,7 @@ -- Low-level bindings to Z3 API. -- -- There is (mostly) a one-to-one correspondence with Z3 C API, thus see --- +-- -- 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 +-- See 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 )@ +-- /unsat/ -> @Just (Right )@ +-- /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 diff --git a/src/Z3/Base/C.hsc b/src/Z3/Base/C.hsc --- a/src/Z3/Base/C.hsc +++ b/src/Z3/Base/C.hsc @@ -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: +-- | Reference: 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: +-- | Reference: newtype Z3_bool = Z3_bool CInt deriving Eq --- | Reference: +-- | Reference: type Z3_error_handler = Ptr Z3_context -> Z3_error_code -> IO () z3_true, z3_false :: Z3_bool --- | Reference: +-- | Reference: z3_true = Z3_bool(#const Z3_TRUE) --- | Reference: +-- | Reference: z3_false = Z3_bool(#const Z3_FALSE) --- | Reference: +-- | Reference: type Z3_string = CString --- | Reference: +-- | Reference: 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: +-- | Reference: type Z3_error_code = CInt #{enum Z3_error_code, , z3_ok = Z3_OK @@ -118,7 +120,35 @@ , z3_exception = Z3_EXCEPTION } --- | Reference: +-- | Reference: +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: 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_config" z3_mk_config :: IO (Ptr Z3_config) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_del_config" z3_del_config :: Ptr Z3_config -> IO () --- | Reference: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_context_rc" z3_mk_context_rc :: Ptr Z3_config -> IO (Ptr Z3_context) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_del_context" z3_del_context :: Ptr Z3_context -> IO () --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_inc_ref" z3_inc_ref :: Ptr Z3_context -> Ptr Z3_ast -> IO () --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_inc_ref" z3_dec_ref :: Ptr Z3_context -> Ptr Z3_ast -> IO () --------------------------------------------------------------------- -- * Symbols --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_int_symbol" z3_mk_int_symbol :: Ptr Z3_context -> CInt -> IO (Ptr Z3_symbol) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_string_symbol" z3_mk_string_symbol :: Ptr Z3_context -> Z3_string -> IO (Ptr Z3_symbol) --------------------------------------------------------------------- -- * Sorts --- | Reference: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_uninterpreted_sort" z3_mk_uninterpreted_sort :: Ptr Z3_context -> Ptr Z3_symbol -> IO (Ptr Z3_sort) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bool_sort" z3_mk_bool_sort :: Ptr Z3_context -> IO (Ptr Z3_sort) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_int_sort" z3_mk_int_sort :: Ptr Z3_context -> IO (Ptr Z3_sort) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_real_sort" z3_mk_real_sort :: Ptr Z3_context -> IO (Ptr Z3_sort) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bv_sort" z3_mk_bv_sort :: Ptr Z3_context -> CUInt -> IO (Ptr Z3_sort) --- | Reference: +-- | Reference: 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: +-- | Reference: 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 +-- | Reference 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 +-- | Reference foreign import ccall unsafe "Z3_del_constructor" z3_del_constructor :: Ptr Z3_context -> Ptr Z3_constructor -> IO () - --- Reference: +-- | Reference: 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: + +-- | Reference +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 +foreign import ccall unsafe "Z3_del_constructor_list" + z3_del_constructor_list :: Ptr Z3_context + -> Ptr (Z3_constructor_list) + -> IO () + +-- | Reference: +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: 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: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_const" z3_mk_const :: Ptr Z3_context -> Ptr Z3_symbol -> Ptr Z3_sort -> IO (Ptr Z3_ast) --- Reference: +-- Reference: 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: +-- Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_true" z3_mk_true :: Ptr Z3_context -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_false" z3_mk_false :: Ptr Z3_context -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_eq" z3_mk_eq :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_distinct" z3_mk_distinct :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_not" z3_mk_not :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_iff" z3_mk_iff :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_implies" z3_mk_implies :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_xor" z3_mk_xor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_and" z3_mk_and :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_add" z3_mk_add :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_mul" z3_mk_mul :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_sub" z3_mk_sub :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_unary_minus" z3_mk_unary_minus :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_div" z3_mk_div :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_mod" z3_mk_mod :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_rem" z3_mk_rem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_lt" z3_mk_lt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_le" z3_mk_le :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_gt" z3_mk_gt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_ge" z3_mk_ge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_int2real" z3_mk_int2real :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_real2int" z3_mk_real2int :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvnot" z3_mk_bvnot :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvredand" z3_mk_bvredand :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvredor" z3_mk_bvredor :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvand" z3_mk_bvand :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvor" z3_mk_bvor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvxor" z3_mk_bvxor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvnand" z3_mk_bvnand :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvnor" z3_mk_bvnor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvxnor" z3_mk_bvxnor :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvadd" z3_mk_bvadd :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvsub" z3_mk_bvsub :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvmul" z3_mk_bvmul :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvudiv" z3_mk_bvudiv :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvsdiv" z3_mk_bvsdiv :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvurem" z3_mk_bvurem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvsrem" z3_mk_bvsrem :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvsmod" z3_mk_bvsmod :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvult" z3_mk_bvult :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvslt" z3_mk_bvslt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvule" z3_mk_bvule :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvsle" z3_mk_bvsle :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvuge" z3_mk_bvuge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvsge" z3_mk_bvsge :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvugt" z3_mk_bvugt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvsgt" z3_mk_bvsgt :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_concat" z3_mk_concat :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_extract" z3_mk_extract :: Ptr Z3_context -> CUInt -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_sign_ext" z3_mk_sign_ext :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_zero_ext" z3_mk_zero_ext :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_repeat" z3_mk_repeat :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvshl" z3_mk_bvshl :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvlshr" z3_mk_bvlshr :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bvashr" z3_mk_bvashr :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_rotate_left" z3_mk_rotate_left :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_rotate_right" z3_mk_rotate_right :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_int2bv" z3_mk_int2bv :: Ptr Z3_context -> CUInt -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bv2int" z3_mk_bv2int :: Ptr Z3_context -> Ptr Z3_ast -> Z3_bool -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_select" z3_mk_select :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_array_default" z3_mk_array_default :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) -------------------------------------------------------------------------------- -- * Sets --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_empty_set" z3_mk_empty_set :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_full_set" z3_mk_full_set :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_set_complement" z3_mk_set_complement :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_numeral" z3_mk_numeral :: Ptr Z3_context -> Z3_string -> Ptr Z3_sort -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_real" z3_mk_real :: Ptr Z3_context -> CInt -> CInt -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_int" z3_mk_int :: Ptr Z3_context -> CInt -> Ptr Z3_sort -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_unsigned_int" z3_mk_unsigned_int :: Ptr Z3_context -> CUInt -> Ptr Z3_sort -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_int64" z3_mk_int64 :: Ptr Z3_context -> CLLong -> Ptr Z3_sort -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_pattern" z3_mk_pattern :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_pattern) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_bound" z3_mk_bound :: Ptr Z3_context -> CUInt -> Ptr Z3_sort -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: 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: +-- | Referece: 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 +-- | Reference 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_exists_const" z3_mk_exists_const :: Ptr Z3_context -> CUInt @@ -743,115 +794,143 @@ --------------------------------------------------------------------- -- * Accessors --- | Reference: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_get_ast_kind" z3_get_ast_kind :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_ast_kind --- Reference: +-- | Reference: +foreign import ccall unsafe "Z3_is_app" + z3_is_app :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_bool + +-- Reference: foreign import ccall unsafe "Z3_get_app_num_args" z3_get_app_num_args :: Ptr Z3_context -> Ptr Z3_app -> IO CUInt --- Reference: +-- Reference: foreign import ccall unsafe "Z3_get_app_arg" z3_get_app_arg :: Ptr Z3_context -> Ptr Z3_app -> CUInt -> IO (Ptr Z3_ast) --- Reference: +-- Reference: foreign import ccall unsafe "Z3_get_app_decl" z3_get_app_decl :: Ptr Z3_context -> Ptr Z3_app -> IO (Ptr Z3_func_decl) --- Reference: +-- Reference: 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: +-- Reference: 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: +-- Reference: 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: +-- Reference: 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: +-- Reference: foreign import ccall unsafe "Z3_get_decl_name" z3_get_decl_name :: Ptr Z3_context -> Ptr Z3_func_decl -> IO (Ptr Z3_symbol) --- Reference: +-- Reference: foreign import ccall unsafe "Z3_get_symbol_string" z3_get_symbol_string :: Ptr Z3_context -> Ptr Z3_symbol -> IO Z3_string --- | Reference: +-- Reference: +foreign import ccall unsafe "Z3_get_sort_kind" + z3_get_sort_kind :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_sort_kind + +-- | Reference: foreign import ccall unsafe "Z3_get_bv_sort_size" z3_get_bv_sort_size :: Ptr Z3_context -> Ptr Z3_sort -> IO CUInt --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_app_to_ast" z3_app_to_ast :: Ptr Z3_context -> Ptr Z3_app -> IO (Ptr Z3_ast) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_get_sort" z3_get_sort :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_sort) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_get_bool_value" z3_get_bool_value :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_lbool --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_get_numeral_string" z3_get_numeral_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_string --- | Reference: +-- | Reference: +foreign import ccall unsafe "Z3_get_arity" + z3_get_arity :: Ptr Z3_context -> Ptr Z3_func_decl -> IO CUInt + +-- | Reference: +foreign import ccall unsafe "Z3_get_domain" + z3_get_domain :: Ptr Z3_context -> Ptr Z3_func_decl -> CUInt -> IO (Ptr Z3_sort) + +-- | Reference: +foreign import ccall unsafe "Z3_get_range" + z3_get_range :: Ptr Z3_context -> Ptr Z3_func_decl -> IO (Ptr Z3_sort) + +-- | Reference: foreign import ccall unsafe "Z3_to_app" z3_to_app :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_app) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_pattern_to_ast" z3_pattern_to_ast :: Ptr Z3_context -> Ptr Z3_pattern -> IO (Ptr Z3_ast) +-- | Reference: +foreign import ccall unsafe "Z3_simplify" + z3_simplify :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Reference: +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: +-- | Reference: foreign import ccall unsafe "Z3_ast_vector_size" z3_ast_vector_size :: Ptr Z3_context -> Ptr Z3_ast_vector -> IO CUInt --- | Reference: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_ast_vector_inc_ref" z3_ast_vector_inc_ref :: Ptr Z3_context -> Ptr Z3_ast_vector -> IO () --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_ast_vector_dec_ref" z3_ast_vector_dec_ref :: Ptr Z3_context -> Ptr Z3_ast_vector -> IO () --------------------------------------------------------------------- -- * Models --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_model_inc_ref" z3_model_inc_ref :: Ptr Z3_context -> Ptr Z3_model -> IO () --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_model_dec_ref" z3_model_dec_ref :: Ptr Z3_context -> Ptr Z3_model -> IO () --- | Reference: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_is_as_array" z3_is_as_array :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_bool --- | Reference: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_func_interp_inc_ref" z3_func_interp_inc_ref :: Ptr Z3_context -> Ptr Z3_func_interp -> IO () --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_func_interp_dec_ref" z3_func_interp_dec_ref :: Ptr Z3_context -> Ptr Z3_func_interp -> IO () --- | Reference: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_func_interp_get_arity" z3_func_interp_get_arity :: Ptr Z3_context -> Ptr Z3_func_interp -> IO CUInt --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_func_entry_inc_ref" z3_func_entry_inc_ref :: Ptr Z3_context -> Ptr Z3_func_entry -> IO () --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_func_entry_dec_ref" z3_func_entry_dec_ref :: Ptr Z3_context -> Ptr Z3_func_entry -> IO () --- | Reference: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_mk_params" z3_mk_params :: Ptr Z3_context -> IO (Ptr Z3_params) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_params_inc_ref" z3_params_inc_ref :: Ptr Z3_context -> Ptr Z3_params -> IO () --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_params_dec_ref" z3_params_dec_ref :: Ptr Z3_context -> Ptr Z3_params -> IO () --- | Reference: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_params_set_uint" z3_params_set_uint :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> CUInt -> IO () --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_params_set_double" z3_params_set_double :: Ptr Z3_context -> Ptr Z3_params -> Ptr Z3_symbol -> CDouble -> IO () --- | Reference: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_params_to_string" z3_params_to_string :: Ptr Z3_context -> Ptr Z3_params -> IO Z3_string --------------------------------------------------------------------- +-- * Interpolation + +-- | Reference: +foreign import ccall unsafe "Z3_mk_interpolant" + z3_mk_interpolant :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) + +-- | Reference: +foreign import ccall unsafe "Z3_mk_interpolation_context" + z3_mk_interpolation_context :: Ptr Z3_config -> IO (Ptr Z3_context) + +-- | Reference: +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: +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: +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: +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: +foreign import ccall unsafe "Z3_interpolation_profile" + z3_interpolation_profile :: Ptr Z3_context -> IO Z3_string + +-- | Reference: +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: +-- | Reference: foreign import ccall unsafe "Z3_mk_solver" z3_mk_solver :: Ptr Z3_context -> IO (Ptr Z3_solver) --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_mk_simple_solver" z3_mk_simple_solver :: Ptr Z3_context -> IO (Ptr Z3_solver) --- | Reference: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_solver_get_help" z3_solver_get_help :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_string --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_solver_set_params" z3_solver_set_params :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_params -> IO () --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_solver_inc_ref" z3_solver_inc_ref :: Ptr Z3_context -> Ptr Z3_solver -> IO () --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_solver_dec_ref" z3_solver_dec_ref :: Ptr Z3_context -> Ptr Z3_solver -> IO () --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_solver_push" z3_solver_push :: Ptr Z3_context -> Ptr Z3_solver -> IO () --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_solver_pop" z3_solver_pop :: Ptr Z3_context -> Ptr Z3_solver -> CUInt -> IO () --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_solver_get_num_scopes" z3_solver_get_num_scopes :: Ptr Z3_context -> Ptr Z3_solver -> IO CUInt --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_solver_reset" z3_solver_reset :: Ptr Z3_context -> Ptr Z3_solver -> IO () --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_solver_assert" z3_solver_assert :: Ptr Z3_context -> Ptr Z3_solver -> Ptr Z3_ast -> IO () --- | Reference: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_solver_check" z3_solver_check :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_lbool --- | Reference: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_solver_get_model" z3_solver_get_model :: Ptr Z3_context -> Ptr Z3_solver -> IO (Ptr Z3_model) --- | Reference: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_solver_get_reason_unknown" z3_solver_get_reason_unknown :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_string --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_solver_to_string" z3_solver_to_string :: Ptr Z3_context -> Ptr Z3_solver -> IO Z3_string --------------------------------------------------------------------- -- * String Conversion --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_set_ast_print_mode" z3_set_ast_print_mode :: Ptr Z3_context -> Z3_ast_print_mode -> IO () --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_ast_to_string" z3_ast_to_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_string --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_pattern_to_string" z3_pattern_to_string :: Ptr Z3_context -> Ptr Z3_pattern -> IO Z3_string --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_sort_to_string" z3_sort_to_string :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_string --- | Reference: +-- | Reference: 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: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_get_error_code" z3_get_error_code :: Ptr Z3_context -> IO Z3_error_code --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_set_error_handler" z3_set_error_handler :: Ptr Z3_context -> FunPtr Z3_error_handler -> IO () --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_set_error" z3_set_error :: Ptr Z3_context -> Z3_error_code -> IO () --- | Reference: +-- | Reference: foreign import ccall unsafe "Z3_get_error_msg" z3_get_error_msg :: Z3_error_code -> IO Z3_string --- | Reference: +-- | Reference: 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: +-- | Reference: foreign import ccall unsafe "Z3_get_version" z3_get_version :: Ptr CUInt -> Ptr CUInt -> Ptr CUInt -> Ptr CUInt -> IO () diff --git a/src/Z3/Monad.hs b/src/Z3/Monad.hs --- a/src/Z3/Monad.hs +++ b/src/Z3/Monad.hs @@ -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: @@ -1350,6 +1394,12 @@ getSymbolString :: MonadZ3 z3 => Symbol -> z3 String getSymbolString = liftFun1 Base.getSymbolString +-- | Return the sort kind. +-- +-- Reference: +getSortKind :: MonadZ3 z3 => Sort -> z3 SortKind +getSortKind = liftFun1 Base.getSortKind + -- | Return the size of the given bit-vector sort. -- -- Reference: @@ -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: 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: +simplify :: MonadZ3 z3 => AST -> z3 AST +simplify = liftFun1 Base.simplify + +-- | Simplify the expression using the given parameters. +-- +-- Reference: +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 diff --git a/z3.cabal b/z3.cabal --- a/z3.cabal +++ b/z3.cabal @@ -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 (). + Bindings for the Z3 4./x/ Theorem Prover (). . * "Z3.Base.C" provides the raw foreign imports from Z3's C API. . @@ -29,7 +29,7 @@ Author: Iago Abal , David Castro Maintainer: Iago Abal -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