z3 4.1.1 → 4.1.2
raw patch · 8 files changed
+551/−20 lines, 8 files
Files
- CHANGES.md +7/−0
- examples/Example/Monad/QuantifierElimination.hs +29/−0
- examples/Example/Monad/Quantifiers.hs +35/−0
- examples/Examples.hs +13/−5
- src/Z3/Base.hs +174/−12
- src/Z3/Base/C.hsc +139/−1
- src/Z3/Monad.hs +150/−0
- z3.cabal +4/−2
CHANGES.md view
@@ -1,6 +1,13 @@ # Release Notes +## 4.1.2++This minor release extends the supported quantifiers API, and adds+partial support for Z3's proof tactics.++* Improved support for theorem proving with quantifiers. (Jakub Daniel)+ ## 4.1.1 Another small release, made possible thanks to third-party contributions.
+ examples/Example/Monad/QuantifierElimination.hs view
@@ -0,0 +1,29 @@+module Example.Monad.QuantifierElimination+ ( run )+ where++import Control.Monad+import Control.Monad.Trans ( liftIO )++import Z3.Monad++run = evalZ3 $ do+ a <- mkFreshIntVar "a"+ b <- mkFreshIntVar "b"+ c <- mkFreshIntVar "c"++ a' <- toApp a+ b' <- toApp b+ c' <- toApp c++ f1 <- mkExistsConst [] [c'] =<< mkAnd =<< sequence [ mkDistinct [a, b, c], mkEq a =<< mkAdd [b, c] ]+ f2 <- mkForallConst [] [a', b'] f1++ forM_ [f1, f2] $ \f -> do+ g <- mkGoal True True False+ goalAssert g f+ qe <- mkTactic "qe" -- eliminate quantifiers+ aig <- mkTactic "aig" -- optionally also simplify+ t <- andThenTactic qe aig+ a <- applyTactic t g+ liftIO . putStrLn =<< astToString =<< mkAnd =<< getGoalFormulas =<< getApplyResultSubgoal a 0
+ examples/Example/Monad/Quantifiers.hs view
@@ -0,0 +1,35 @@+module Example.Monad.Quantifiers+ ( run )+ where++import Control.Monad+import Control.Monad.Trans ( liftIO )++import Z3.Monad++run = evalZ3 $ do+ a <- mkFreshIntVar "a"+ b <- mkFreshIntVar "b"+ c <- mkFreshIntVar "c"+ d <- mkFreshIntVar "d"++ a' <- toApp a+ b' <- toApp b+ c' <- toApp c+ d' <- toApp d++ fs <- sequence [ mkEq a =<< mkAdd [ b, c ]+ , mkExistsConst [] [a'] =<< mkEq a =<< mkAdd [ b, c ]+ , mkForallConst [] [a', d'] =<< mkExistsConst [] [ b', c' ] =<< join (liftM2 mkEq (mkAdd [ a, b ]) (mkMul [ c, d ]))+ , mkAdd [ a, b, c, d ] ]++ forM_ fs $ \a -> do+ k <- getAstKind a+ case k of+ Z3_QUANTIFIER_AST -> do+ t <- isQuantifierForall a+ vs <- getQuantifierBoundVars a+ b <- getQuantifierBody a+ f <- substituteVars a vs -- this step only replaces debruijn encoding of the bound variables+ liftIO . putStrLn . ((if t then "universal: " else "existential: ") ++) =<< astToString f+ _ -> liftIO . putStrLn =<< astToString a
examples/Examples.hs view
@@ -6,6 +6,8 @@ import qualified Example.Monad.DataTypes import qualified Example.Monad.FuncModel import qualified Example.Monad.MutuallyRecursive+import qualified Example.Monad.Quantifiers+import qualified Example.Monad.QuantifierElimination import qualified Example.Monad.ToSMTLib import qualified Example.Monad.Tuple import qualified Example.Monad.Interpolation@@ -22,20 +24,26 @@ , ("datatypes" , Example.Monad.DataTypes.run )- , ("funcmodel"+ , ("funcModel" , Example.Monad.FuncModel.run )- , ("mutuallyrecursive"+ , ("interpolation"+ , Example.Monad.Interpolation.run+ )+ , ("mutuallyRecursive" , Example.Monad.MutuallyRecursive.run )+ , ("quantifiers"+ , Example.Monad.Quantifiers.run+ )+ , ("quantifierElimination"+ , Example.Monad.QuantifierElimination.run+ ) , ("smtlib" , Example.Monad.ToSMTLib.run ) , ("tuple" , Example.Monad.Tuple.run- )- , ("interpolation"- , Example.Monad.Interpolation.run ) ]
src/Z3/Base.hs view
@@ -70,6 +70,9 @@ , Solver , SortKind(..) , ASTKind(..)+ , Tactic+ , ApplyResult+ , Goal -- ** Satisfiability result , Result(..) @@ -269,6 +272,8 @@ , getAppArg , getAppArgs , getSort+ , getArraySortDomain+ , getArraySortRange , getBoolValue , getAstKind , isApp@@ -276,12 +281,30 @@ , getNumeralString , simplify , simplifyEx+ , getIndexValue+ , isQuantifierForall+ , isQuantifierExists+ , getQuantifierWeight+ , getQuantifierNumPatterns+ , getQuantifierPatternAST+ , getQuantifierPatterns+ , getQuantifierNumNoPatterns+ , getQuantifierNoPatternAST+ , getQuantifierNoPatterns+ , getQuantifierNumBound+ , getQuantifierBoundName+ , getQuantifierBoundSort+ , getQuantifierBoundVars+ , getQuantifierBody -- ** Helpers , getBool , getInt , getReal , getBv + -- * Modifiers+ , substituteVars+ -- * Models , modelEval , evalArray@@ -309,6 +332,24 @@ , FuncModel (..) , evalFunc + -- * Tactics+ , mkTactic+ , andThenTactic+ , orElseTactic+ , skipTactic+ , tryForTactic+ , mkQuantifierEliminationTactic+ , mkAndInverterGraphTactic+ , applyTactic+ , getApplyResultNumSubgoals+ , getApplyResultSubgoal+ , getApplyResultSubgoals+ , mkGoal+ , goalAssert+ , getGoalSize+ , getGoalFormula+ , getGoalFormulas+ -- * String Conversion , ASTPrintMode(..) , setASTPrintMode@@ -445,6 +486,18 @@ newtype FuncEntry = FuncEntry { unFuncEntry :: ForeignPtr Z3_func_entry } deriving Eq +-- | A tactic+newtype Tactic = Tactic { unTactic :: ForeignPtr Z3_tactic }+ deriving Eq++-- | A goal (aka problem)+newtype Goal = Goal { unGoal :: ForeignPtr Z3_goal }+ deriving Eq++-- | A result of applying a tactic+newtype ApplyResult = ApplyResult { unApplyResult :: ForeignPtr Z3_apply_result }+ deriving Eq+ -- | A Z3 parameter set. -- -- Starting at Z3 4.0, parameter sets are used to configure many components@@ -1625,8 +1678,12 @@ -- TODO: Z3_get_array_sort_size --- TODO: Z3_get_array_sort_range+getArraySortDomain :: Context -> Sort -> IO Sort+getArraySortDomain = liftFun1 z3_get_array_sort_domain +getArraySortRange :: Context -> Sort -> IO Sort+getArraySortRange = liftFun1 z3_get_array_sort_range+ -- TODO: Z3_get_tuple_sort_mk_decl -- TODO: Z3_get_tuple_sort_num_fields@@ -1845,28 +1902,60 @@ -- TODO: Z3_get_pattern --- TODO: Z3_get_index_value+getIndexValue :: Context -> AST -> IO Int+getIndexValue = liftFun1 z3_get_index_value --- TODO: Z3_is_quantifier_forall+isQuantifierForall :: Context -> AST -> IO Bool+isQuantifierForall = liftFun1 z3_is_quantifier_forall --- TODO: Z3_get_quantifier_weight+isQuantifierExists :: Context -> AST -> IO Bool+isQuantifierExists ctx = fmap not . isQuantifierForall ctx --- TODO: Z3_get_quantifier_num_patterns+getQuantifierWeight :: Context -> AST -> IO Int+getQuantifierWeight = liftFun1 z3_get_quantifier_weight --- TODO: Z3_get_quantifier_pattern_ast+getQuantifierNumPatterns :: Context -> AST -> IO Int+getQuantifierNumPatterns = liftFun1 z3_get_quantifier_num_patterns --- TODO: Z3_get_quantifier_num_no_patterns+getQuantifierPatternAST :: Context -> AST -> Int -> IO AST+getQuantifierPatternAST = liftFun2 z3_get_quantifier_pattern_ast --- TODO: Z3_get_quantifier_no_pattern_ast+getQuantifierPatterns :: Context -> AST -> IO [AST]+getQuantifierPatterns ctx a = do+ n <- getQuantifierNumPatterns ctx a+ T.forM [0..n-1] (getQuantifierPatternAST ctx a) --- TODO: Z3_get_quantifier_num_bound+getQuantifierNumNoPatterns :: Context -> AST -> IO Int+getQuantifierNumNoPatterns = liftFun1 z3_get_quantifier_num_no_patterns --- TODO: Z3_get_quantifier_bound_name+getQuantifierNoPatternAST :: Context -> AST -> Int -> IO AST+getQuantifierNoPatternAST = liftFun2 z3_get_quantifier_no_pattern_ast --- TODO: Z3_get_quantifier_bound_sort+getQuantifierNoPatterns :: Context -> AST -> IO [AST]+getQuantifierNoPatterns ctx a = do+ n <- getQuantifierNumNoPatterns ctx a+ T.forM [0..n-1] (getQuantifierNoPatternAST ctx a) --- TODO: Z3_get_quantifier_body+getQuantifierNumBound :: Context -> AST -> IO Int+getQuantifierNumBound = liftFun1 z3_get_quantifier_num_bound +getQuantifierBoundName :: Context -> AST -> Int -> IO Symbol+getQuantifierBoundName = liftFun2 z3_get_quantifier_bound_name++getQuantifierBoundSort :: Context -> AST -> Int -> IO Sort+getQuantifierBoundSort = liftFun2 z3_get_quantifier_bound_sort++getQuantifierBoundVars :: Context -> AST -> IO [AST]+getQuantifierBoundVars ctx a = do+ n <- getQuantifierNumBound ctx a+ T.forM [0..n-1] $ \i -> do+ b <- getQuantifierBoundName ctx a i+ s <- getQuantifierBoundSort ctx a i+ mkVar ctx b s++getQuantifierBody :: Context -> AST -> IO AST+getQuantifierBody = liftFun1 z3_get_quantifier_body+ simplify :: Context -> AST -> IO AST simplify = liftFun1 z3_simplify @@ -1916,6 +2005,13 @@ -- TODO Modifiers +substituteVars :: Context -> AST -> [AST] -> IO AST+substituteVars ctx a vars =+ marshal z3_substitute_vars ctx $ \f ->+ h2c a $ \aPtr ->+ marshalArrayLen vars $ \varsNum varsArr ->+ f aPtr varsNum varsArr+ --------------------------------------------------------------------- -- Models @@ -2202,6 +2298,61 @@ f namePtr logicPtr statusPtr attrPtr assumpNum assumpArr formPtr ---------------------------------------------------------------------+-- Tactics++mkTactic :: Context -> String -> IO Tactic+mkTactic = liftFun1 z3_mk_tactic++andThenTactic :: Context -> Tactic -> Tactic -> IO Tactic+andThenTactic = liftFun2 z3_tactic_and_then++orElseTactic :: Context -> Tactic -> Tactic -> IO Tactic+orElseTactic = liftFun2 z3_tactic_or_else++skipTactic :: Context -> IO Tactic+skipTactic = liftFun0 z3_tactic_skip++tryForTactic :: Context -> Tactic -> Int -> IO Tactic+tryForTactic = liftFun2 z3_tactic_try_for++mkQuantifierEliminationTactic :: Context -> IO Tactic+mkQuantifierEliminationTactic ctx = mkTactic ctx "qe"++mkAndInverterGraphTactic :: Context -> IO Tactic+mkAndInverterGraphTactic ctx = mkTactic ctx "aig"++applyTactic :: Context -> Tactic -> Goal -> IO ApplyResult+applyTactic = liftFun2 z3_tactic_apply++getApplyResultNumSubgoals :: Context -> ApplyResult -> IO Int+getApplyResultNumSubgoals = liftFun1 z3_apply_result_get_num_subgoals++getApplyResultSubgoal :: Context -> ApplyResult -> Int -> IO Goal+getApplyResultSubgoal = liftFun2 z3_apply_result_get_subgoal++getApplyResultSubgoals :: Context -> ApplyResult -> IO [Goal]+getApplyResultSubgoals ctx a = do+ n <- getApplyResultNumSubgoals ctx a+ T.forM [0..n-1] (getApplyResultSubgoal ctx a)++mkGoal :: Context -> Bool -> Bool -> Bool -> IO Goal+mkGoal = liftFun3 z3_mk_goal++goalAssert :: Context -> Goal -> AST -> IO ()+goalAssert = liftFun2 z3_goal_assert++getGoalSize :: Context -> Goal -> IO Int+getGoalSize = liftFun1 z3_goal_size++getGoalFormula :: Context -> Goal -> Int -> IO AST+getGoalFormula = liftFun2 z3_goal_formula++getGoalFormulas :: Context -> Goal -> IO [AST]+getGoalFormulas ctx g = do+ n <- getGoalSize ctx g+ T.forM [0..n-1] (getGoalFormula ctx g)++--------------------------------------------------------------------- -- Parser interface -- TODO@@ -2856,6 +3007,17 @@ c2h = mkC2hRefCount Solver z3_solver_inc_ref z3_solver_dec_ref h2c slv = withForeignPtr (unSolver slv) +instance Marshal Tactic (Ptr Z3_tactic) where+ c2h = mkC2hRefCount Tactic z3_tactic_inc_ref z3_tactic_dec_ref+ h2c tac = withForeignPtr (unTactic tac)++instance Marshal ApplyResult (Ptr Z3_apply_result) where+ c2h = mkC2hRefCount ApplyResult z3_apply_result_inc_ref z3_apply_result_dec_ref+ h2c apl = withForeignPtr (unApplyResult apl)++instance Marshal Goal (Ptr Z3_goal) where+ c2h = mkC2hRefCount Goal z3_goal_inc_ref z3_goal_dec_ref+ h2c goa = withForeignPtr (unGoal goa) marshal :: Marshal rh rc => (Ptr Z3_context -> t) -> Context -> (t -> IO rc) -> IO rh
src/Z3/Base/C.hsc view
@@ -56,6 +56,12 @@ data Z3_model +data Z3_goal++data Z3_tactic++data Z3_apply_result+ data Z3_func_interp data Z3_func_entry@@ -858,6 +864,14 @@ foreign import ccall unsafe "Z3_get_sort" z3_get_sort :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_sort) +-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#ga6ffa46d55e4632d761db4dfae7441c09>+foreign import ccall unsafe "Z3_get_array_sort_domain"+ z3_get_array_sort_domain :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort)++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#gaa6f84f1b2b178f6fe5bc3b9a5762a73b>+foreign import ccall unsafe "Z3_get_array_sort_range"+ z3_get_array_sort_range :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort)+ -- | 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@@ -894,9 +908,54 @@ 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+-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#gac47b42af13aee024d34bb37ffaa0ad75>+foreign import ccall unsafe "Z3_is_quantifier_forall"+ z3_is_quantifier_forall :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_bool +-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#gaa5820368b5ae944bd17f10c2f8247c11>+foreign import ccall unsafe "Z3_get_quantifier_weight"+ z3_get_quantifier_weight :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#ga3e5cb3bd6e9b9de0d6e6a6e80eb36bba>+foreign import ccall unsafe "Z3_get_quantifier_num_patterns"+ z3_get_quantifier_num_patterns :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#gad48dd00ca5ebce768c66dca447f50037>+foreign import ccall unsafe "Z3_get_quantifier_pattern_ast"+ z3_get_quantifier_pattern_ast :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> IO (Ptr Z3_ast)++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#ga6b2c35b148f0bb05e9ebf8ab17c2b16e>+foreign import ccall unsafe "Z3_get_quantifier_num_no_patterns"+ z3_get_quantifier_num_no_patterns :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#ga7b68758cbe05352eca541e4028f9a8d8>+foreign import ccall unsafe "Z3_get_quantifier_no_pattern_ast"+ z3_get_quantifier_no_pattern_ast :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> IO (Ptr Z3_ast)++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#gac85bd38ea5c41ec9e0e956a8a1734a7d>+foreign import ccall unsafe "Z3_get_quantifier_num_bound"+ z3_get_quantifier_num_bound :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#ga3e6914c9186de8e588da66af78aa271f>+foreign import ccall unsafe "Z3_get_quantifier_bound_name"+ z3_get_quantifier_bound_name :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> IO (Ptr Z3_symbol)++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#gae9a7280ad96d05c8266aad869efb9b25>+foreign import ccall unsafe "Z3_get_quantifier_bound_sort"+ z3_get_quantifier_bound_sort :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> IO (Ptr Z3_sort)++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#ga94b1bdd4d3351afc860f6cbd2a2ada9f>+foreign import ccall unsafe "Z3_get_quantifier_body"+ z3_get_quantifier_body :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)+ ---------------------------------------------------------------------+-- * Modifiers++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#gad6e8afe205259b3d924f460d22665e90>+foreign import ccall unsafe "Z3_substitute_vars"+ z3_substitute_vars :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)++--------------------------------------------------------------------- -- * AST vectors -- | Reference: <http://z3prover.github.io/api/html/group__capi.html#ga99d6a99e914fcb11e5dcf9fcc3584425>@@ -1034,6 +1093,10 @@ -- TODO Constraints: Z3_check_assumptions -- TODO Constraints: Z3_get_implied_equalities +-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#gab3c5c7eadcfd209eec72ec0ac0ad2e96>+foreign import ccall unsafe "Z3_get_index_value"+ z3_get_index_value :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt+ -- | 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@@ -1125,6 +1188,81 @@ z3_write_interpolation_problem :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> Ptr CUInt -> Ptr CChar -> CUInt -> Ptr (Ptr Z3_ast) -> IO ()++---------------------------------------------------------------------+-- * Tactics++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#gaa4b9d53ba194d2d3a8bb2f55bec7e78e>+foreign import ccall unsafe "Z3_mk_tactic"+ z3_mk_tactic :: Ptr Z3_context -> Ptr CChar -> IO (Ptr Z3_tactic)++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#gaf53dac8f6c9b615cd21b9a2eeb006005>+foreign import ccall unsafe "Z3_tactic_and_then"+ z3_tactic_and_then :: Ptr Z3_context -> Ptr Z3_tactic -> Ptr Z3_tactic -> IO (Ptr Z3_tactic)++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#gad9964357958dd12ab20f0b315ddc219b>+foreign import ccall unsafe "Z3_tactic_or_else"+ z3_tactic_or_else :: Ptr Z3_context -> Ptr Z3_tactic -> Ptr Z3_tactic -> IO (Ptr Z3_tactic)++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#gab940c1401643ece97517ff27838313c4>+foreign import ccall unsafe "Z3_tactic_skip"+ z3_tactic_skip :: Ptr Z3_context -> IO (Ptr Z3_tactic)++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#gac0670bd04fa76af71b2abbc2f8b62889>+foreign import ccall unsafe "Z3_tactic_try_for"+ z3_tactic_try_for :: Ptr Z3_context -> Ptr Z3_tactic -> CUInt -> IO (Ptr Z3_tactic)++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#gabd0874d8777b3bc426782a87c04206b9>+foreign import ccall unsafe "Z3_tactic_inc_ref"+ z3_tactic_inc_ref :: Ptr Z3_context -> Ptr Z3_tactic -> IO ()++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#ga8feaef3d36dcb136fa7812a8c10cf178>+foreign import ccall unsafe "Z3_tactic_dec_ref"+ z3_tactic_dec_ref :: Ptr Z3_context -> Ptr Z3_tactic -> IO ()++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#gac9e9da38d6a9acff293bc22bf0cf1a20>+foreign import ccall unsafe "Z3_tactic_apply"+ z3_tactic_apply :: Ptr Z3_context -> Ptr Z3_tactic -> Ptr Z3_goal -> IO (Ptr Z3_apply_result)++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#ga1f182e7ef80015e8f2dcde219371aedc>+foreign import ccall unsafe "Z3_apply_result_inc_ref"+ z3_apply_result_inc_ref :: Ptr Z3_context -> Ptr Z3_apply_result -> IO ()++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#gac0fa60e39840a704f201ced90cde0ef9>+foreign import ccall unsafe "Z3_apply_result_dec_ref"+ z3_apply_result_dec_ref :: Ptr Z3_context -> Ptr Z3_apply_result -> IO ()++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#ga5ab8e77bdbfecc6f8845734cd7a729f7>+foreign import ccall unsafe "Z3_apply_result_get_num_subgoals"+ z3_apply_result_get_num_subgoals :: Ptr Z3_context -> Ptr Z3_apply_result -> IO CUInt++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#gac4f8342eed2de1c1caaa2fbf492439a9>+foreign import ccall unsafe "Z3_apply_result_get_subgoal"+ z3_apply_result_get_subgoal :: Ptr Z3_context -> Ptr Z3_apply_result -> CUInt -> IO (Ptr Z3_goal)++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#ga631394a36c83a1e0db7825fe92d8aebe>+foreign import ccall unsafe "Z3_mk_goal"+ z3_mk_goal :: Ptr Z3_context -> Z3_bool -> Z3_bool -> Z3_bool -> IO (Ptr Z3_goal)++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#ga63a581c33213fb14efe9e6175c74546b>+foreign import ccall unsafe "Z3_goal_inc_ref"+ z3_goal_inc_ref :: Ptr Z3_context -> Ptr Z3_goal -> IO ()++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#gad65f4f9f7035b6eef161ee93bb694e52>+foreign import ccall unsafe "Z3_goal_dec_ref"+ z3_goal_dec_ref :: Ptr Z3_context -> Ptr Z3_goal -> IO ()++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#ga3052a11993ce35250f108c365bc09ff7>+foreign import ccall unsafe "Z3_goal_assert"+ z3_goal_assert :: Ptr Z3_context -> Ptr Z3_goal -> Ptr Z3_ast -> IO ()++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#ga5badc99b0a1e154ef3cef17ff35fd021>+foreign import ccall unsafe "Z3_goal_size"+ z3_goal_size :: Ptr Z3_context -> Ptr Z3_goal -> IO CUInt++-- | Reference: <https://z3prover.github.io/api/html/group__capi.html#gaec43d4d20ed7e7bf4c7a57d37dc3bfc6>+foreign import ccall unsafe "Z3_goal_formula"+ z3_goal_formula :: Ptr Z3_context -> Ptr Z3_goal -> CUInt -> IO (Ptr Z3_ast) --------------------------------------------------------------------- -- * Solvers
src/Z3/Monad.hs view
@@ -231,6 +231,8 @@ , getAppArg , getAppArgs , getSort+ , getArraySortDomain+ , getArraySortRange , getBoolValue , getAstKind , isApp@@ -238,12 +240,30 @@ , getNumeralString , simplify , simplifyEx+ , getIndexValue+ , isQuantifierForall+ , isQuantifierExists+ , getQuantifierWeight+ , getQuantifierNumPatterns+ , getQuantifierPatternAST+ , getQuantifierPatterns+ , getQuantifierNumNoPatterns+ , getQuantifierNoPatternAST+ , getQuantifierNoPatterns+ , getQuantifierNumBound+ , getQuantifierBoundName+ , getQuantifierBoundSort+ , getQuantifierBoundVars+ , getQuantifierBody -- ** Helpers , getBool , getInt , getReal , getBv + -- * Modifiers+ , substituteVars+ -- * Models , modelEval , evalArray@@ -271,6 +291,24 @@ , FuncModel(..) , evalFunc + -- * Tactics+ , mkTactic+ , andThenTactic+ , orElseTactic+ , skipTactic+ , tryForTactic+ , mkQuantifierEliminationTactic+ , mkAndInverterGraphTactic+ , applyTactic+ , getApplyResultNumSubgoals+ , getApplyResultSubgoal+ , getApplyResultSubgoals+ , mkGoal+ , goalAssert+ , getGoalSize+ , getGoalFormula+ , getGoalFormulas+ -- * String Conversion , ASTPrintMode(..) , setASTPrintMode@@ -351,6 +389,9 @@ , Solver , SortKind(..) , ASTKind(..)+ , Tactic+ , ApplyResult+ , Goal ) import qualified Z3.Base as Base @@ -1469,6 +1510,12 @@ getSort :: MonadZ3 z3 => AST -> z3 Sort getSort = liftFun1 Base.getSort +getArraySortDomain :: MonadZ3 z3 => Sort -> z3 Sort+getArraySortDomain = liftFun1 Base.getArraySortDomain++getArraySortRange :: MonadZ3 z3 => Sort -> z3 Sort+getArraySortRange = liftFun1 Base.getArraySortRange+ -- | Returns @Just True@, @Just False@, or @Nothing@ for /undefined/. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga133aaa1ec31af9b570ed7627a3c8c5a4>@@ -1493,6 +1540,51 @@ getNumeralString :: MonadZ3 z3 => AST -> z3 String getNumeralString = liftFun1 Base.getNumeralString +getIndexValue :: MonadZ3 z3 => AST -> z3 Int+getIndexValue = liftFun1 Base.getIndexValue++isQuantifierForall :: MonadZ3 z3 => AST -> z3 Bool+isQuantifierForall = liftFun1 Base.isQuantifierForall++isQuantifierExists :: MonadZ3 z3 => AST -> z3 Bool+isQuantifierExists = liftFun1 Base.isQuantifierExists++getQuantifierWeight :: MonadZ3 z3 => AST -> z3 Int+getQuantifierWeight = liftFun1 Base.getQuantifierWeight++getQuantifierNumPatterns :: MonadZ3 z3 => AST -> z3 Int+getQuantifierNumPatterns = liftFun1 Base.getQuantifierNumPatterns++getQuantifierPatternAST :: MonadZ3 z3 => AST -> Int -> z3 AST+getQuantifierPatternAST = liftFun2 Base.getQuantifierPatternAST++getQuantifierPatterns :: MonadZ3 z3 => AST -> z3 [AST]+getQuantifierPatterns = liftFun1 Base.getQuantifierPatterns++getQuantifierNumNoPatterns :: MonadZ3 z3 => AST -> z3 Int+getQuantifierNumNoPatterns = liftFun1 Base.getQuantifierNumNoPatterns++getQuantifierNoPatternAST :: MonadZ3 z3 => AST -> Int -> z3 AST+getQuantifierNoPatternAST = liftFun2 Base.getQuantifierNoPatternAST++getQuantifierNoPatterns :: MonadZ3 z3 => AST -> z3 [AST]+getQuantifierNoPatterns = liftFun1 Base.getQuantifierNoPatterns++getQuantifierNumBound :: MonadZ3 z3 => AST -> z3 Int+getQuantifierNumBound = liftFun1 Base.getQuantifierNumBound++getQuantifierBoundName :: MonadZ3 z3 => AST -> Int -> z3 Symbol+getQuantifierBoundName = liftFun2 Base.getQuantifierBoundName++getQuantifierBoundSort :: MonadZ3 z3 => AST -> Int -> z3 Sort+getQuantifierBoundSort = liftFun2 Base.getQuantifierBoundSort++getQuantifierBoundVars :: MonadZ3 z3 => AST -> z3 [AST]+getQuantifierBoundVars = liftFun1 Base.getQuantifierBoundVars++getQuantifierBody :: MonadZ3 z3 => AST -> z3 AST+getQuantifierBody = liftFun1 Base.getQuantifierBody+ -- | Simplify the expression. -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gada433553406475e5dd6a494ea957844c>@@ -1528,7 +1620,14 @@ -> z3 Integer getBv = liftFun2 Base.getBv + ---------------------------------------------------------------------+-- Modifiers++substituteVars :: MonadZ3 z3 => AST -> [AST] -> z3 AST+substituteVars = liftFun2 Base.substituteVars++--------------------------------------------------------------------- -- Models -- | Evaluate an AST node in the given model.@@ -1683,6 +1782,57 @@ -- | Get function as a list of argument/value pairs. evalFunc :: MonadZ3 z3 => Model -> FuncDecl -> z3 (Maybe FuncModel) evalFunc = liftFun2 Base.evalFunc++---------------------------------------------------------------------+-- Tactics++mkTactic :: MonadZ3 z3 => String -> z3 Tactic+mkTactic = liftFun1 Base.mkTactic++andThenTactic :: MonadZ3 z3 => Tactic -> Tactic -> z3 Tactic+andThenTactic = liftFun2 Base.andThenTactic++orElseTactic :: MonadZ3 z3 => Tactic -> Tactic -> z3 Tactic+orElseTactic = liftFun2 Base.andThenTactic++skipTactic :: MonadZ3 z3 => z3 Tactic+skipTactic = liftScalar Base.skipTactic++tryForTactic :: MonadZ3 z3 => Tactic -> Int -> z3 Tactic+tryForTactic = liftFun2 Base.tryForTactic++mkQuantifierEliminationTactic :: MonadZ3 z3 => z3 Tactic+mkQuantifierEliminationTactic = liftScalar Base.mkQuantifierEliminationTactic++mkAndInverterGraphTactic :: MonadZ3 z3 => z3 Tactic+mkAndInverterGraphTactic = liftScalar Base.mkAndInverterGraphTactic++applyTactic :: MonadZ3 z3 => Tactic -> Goal -> z3 ApplyResult+applyTactic = liftFun2 Base.applyTactic++getApplyResultNumSubgoals :: MonadZ3 z3 => ApplyResult -> z3 Int+getApplyResultNumSubgoals = liftFun1 Base.getApplyResultNumSubgoals++getApplyResultSubgoal :: MonadZ3 z3 => ApplyResult -> Int -> z3 Goal+getApplyResultSubgoal = liftFun2 Base.getApplyResultSubgoal++getApplyResultSubgoals :: MonadZ3 z3 => ApplyResult -> z3 [Goal]+getApplyResultSubgoals = liftFun1 Base.getApplyResultSubgoals++mkGoal :: MonadZ3 z3 => Bool -> Bool -> Bool -> z3 Goal+mkGoal = liftFun3 Base.mkGoal++goalAssert :: MonadZ3 z3 => Goal -> AST -> z3 ()+goalAssert = liftFun2 Base.goalAssert++getGoalSize :: MonadZ3 z3 => Goal -> z3 Int+getGoalSize = liftFun1 Base.getGoalSize++getGoalFormula :: MonadZ3 z3 => Goal -> Int -> z3 AST+getGoalFormula = liftFun2 Base.getGoalFormula++getGoalFormulas :: MonadZ3 z3 => Goal -> z3 [AST]+getGoalFormulas = liftFun1 Base.getGoalFormulas --------------------------------------------------------------------- -- String Conversion
z3.cabal view
@@ -1,5 +1,5 @@ Name: z3-Version: 4.1.1+Version: 4.1.2 Synopsis: Bindings for the Z3 Theorem Prover Description: Bindings for the Z3 4./x/ Theorem Prover (<https://github.com/Z3Prover/z3>).@@ -102,10 +102,12 @@ Example.Monad.Queens4All Example.Monad.DataTypes Example.Monad.FuncModel+ Example.Monad.Interpolation Example.Monad.MutuallyRecursive+ Example.Monad.Quantifiers+ Example.Monad.QuantifierElimination Example.Monad.ToSMTLib Example.Monad.Tuple- Example.Monad.Interpolation Test-suite spec