diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -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. diff --git a/examples/Example/Monad/QuantifierElimination.hs b/examples/Example/Monad/QuantifierElimination.hs new file mode 100644 --- /dev/null +++ b/examples/Example/Monad/QuantifierElimination.hs @@ -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 diff --git a/examples/Example/Monad/Quantifiers.hs b/examples/Example/Monad/Quantifiers.hs new file mode 100644 --- /dev/null +++ b/examples/Example/Monad/Quantifiers.hs @@ -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 diff --git a/examples/Examples.hs b/examples/Examples.hs --- a/examples/Examples.hs +++ b/examples/Examples.hs @@ -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 ) ] diff --git a/src/Z3/Base.hs b/src/Z3/Base.hs --- a/src/Z3/Base.hs +++ b/src/Z3/Base.hs @@ -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 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 @@ -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: +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: +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: 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: +foreign import ccall unsafe "Z3_is_quantifier_forall" + z3_is_quantifier_forall :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_bool +-- | Reference: +foreign import ccall unsafe "Z3_get_quantifier_weight" + z3_get_quantifier_weight :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt + +-- | Reference: +foreign import ccall unsafe "Z3_get_quantifier_num_patterns" + z3_get_quantifier_num_patterns :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt + +-- | Reference: +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: +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: +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: +foreign import ccall unsafe "Z3_get_quantifier_num_bound" + z3_get_quantifier_num_bound :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt + +-- | Reference: +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: +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: +foreign import ccall unsafe "Z3_get_quantifier_body" + z3_get_quantifier_body :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast) + --------------------------------------------------------------------- +-- * Modifiers + +-- | Reference: +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: @@ -1034,6 +1093,10 @@ -- TODO Constraints: Z3_check_assumptions -- TODO Constraints: Z3_get_implied_equalities +-- | Reference: +foreign import ccall unsafe "Z3_get_index_value" + z3_get_index_value :: Ptr Z3_context -> Ptr Z3_ast -> IO CUInt + -- | Reference: 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: +foreign import ccall unsafe "Z3_mk_tactic" + z3_mk_tactic :: Ptr Z3_context -> Ptr CChar -> IO (Ptr Z3_tactic) + +-- | Reference: +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: +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: +foreign import ccall unsafe "Z3_tactic_skip" + z3_tactic_skip :: Ptr Z3_context -> IO (Ptr Z3_tactic) + +-- | Reference: +foreign import ccall unsafe "Z3_tactic_try_for" + z3_tactic_try_for :: Ptr Z3_context -> Ptr Z3_tactic -> CUInt -> IO (Ptr Z3_tactic) + +-- | Reference: +foreign import ccall unsafe "Z3_tactic_inc_ref" + z3_tactic_inc_ref :: Ptr Z3_context -> Ptr Z3_tactic -> IO () + +-- | Reference: +foreign import ccall unsafe "Z3_tactic_dec_ref" + z3_tactic_dec_ref :: Ptr Z3_context -> Ptr Z3_tactic -> IO () + +-- | Reference: +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: +foreign import ccall unsafe "Z3_apply_result_inc_ref" + z3_apply_result_inc_ref :: Ptr Z3_context -> Ptr Z3_apply_result -> IO () + +-- | Reference: +foreign import ccall unsafe "Z3_apply_result_dec_ref" + z3_apply_result_dec_ref :: Ptr Z3_context -> Ptr Z3_apply_result -> IO () + +-- | Reference: +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: +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: +foreign import ccall unsafe "Z3_mk_goal" + z3_mk_goal :: Ptr Z3_context -> Z3_bool -> Z3_bool -> Z3_bool -> IO (Ptr Z3_goal) + +-- | Reference: +foreign import ccall unsafe "Z3_goal_inc_ref" + z3_goal_inc_ref :: Ptr Z3_context -> Ptr Z3_goal -> IO () + +-- | Reference: +foreign import ccall unsafe "Z3_goal_dec_ref" + z3_goal_dec_ref :: Ptr Z3_context -> Ptr Z3_goal -> IO () + +-- | Reference: +foreign import ccall unsafe "Z3_goal_assert" + z3_goal_assert :: Ptr Z3_context -> Ptr Z3_goal -> Ptr Z3_ast -> IO () + +-- | Reference: +foreign import ccall unsafe "Z3_goal_size" + z3_goal_size :: Ptr Z3_context -> Ptr Z3_goal -> IO CUInt + +-- | Reference: +foreign import ccall unsafe "Z3_goal_formula" + z3_goal_formula :: Ptr Z3_context -> Ptr Z3_goal -> CUInt -> IO (Ptr Z3_ast) --------------------------------------------------------------------- -- * Solvers diff --git a/src/Z3/Monad.hs b/src/Z3/Monad.hs --- a/src/Z3/Monad.hs +++ b/src/Z3/Monad.hs @@ -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: @@ -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: @@ -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 diff --git a/z3.cabal b/z3.cabal --- a/z3.cabal +++ b/z3.cabal @@ -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 (). @@ -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