z3 408.1 → 408.2
raw patch · 6 files changed
+1004/−15 lines, 6 files
Files
- CHANGES.md +12/−0
- src/Z3/Base.hs +363/−3
- src/Z3/Base/C.hsc +250/−0
- src/Z3/Monad.hs +365/−4
- test/Z3/Base/Spec.hs +4/−2
- z3.cabal +10/−6
CHANGES.md view
@@ -1,7 +1,19 @@ # Release Notes +## 408.2++Tested (sort of) with Z3 4.8.8.++* Added Optimization API. (David Cao)+* Added Sequences and regular expressions API. (Carlo Nucera)+* Added z3_solver_get_proof. ("0xd34df00d")+* Added MonadZ3 instance for ReaderT. ("0xd34df00d")+* Fixed two typos in docs. (Mauro Bringolf)+ ## 408.1++Tested (sort of) with Z3 4.8.4. * Added bindings to `substitute` and `isEqAST`. (Hengchu Zhang) * Added `MonadFail` instance for `Z3`, required by GHC >=8.6. (Conal Elliott)
src/Z3/Base.hs view
@@ -250,6 +250,43 @@ , mkBitvector , mkBvNum + -- * Sequences and regular expressions+ , mkSeqSort+ , isSeqSort+ , mkReSort+ , isReSort+ , mkStringSort+ , isStringSort+ , mkString+ , isString+ , getString+ , mkSeqEmpty+ , mkSeqUnit+ , mkSeqConcat+ , mkSeqPrefix+ , mkSeqSuffix+ , mkSeqContains+ , mkSeqExtract+ , mkSeqReplace+ , mkSeqAt+ , mkSeqLength+ , mkSeqIndex+ , mkStrToInt+ , mkIntToStr+ , mkSeqToRe+ , mkSeqInRe+ , mkRePlus+ , mkReStar+ , mkReOption+ , mkReUnion+ , mkReConcat+ , mkReRange+ , mkReLoop+ , mkReIntersect+ , mkReComplement+ , mkReEmpty+ , mkReFull+ -- * Quantifiers , mkPattern , mkBound@@ -396,6 +433,32 @@ , fixedpointGetAnswer , fixedpointGetAssertions + -- * Optimization+ , Optimize (..)+ , mkOptimize+ , optimizeAssert+ , optimizeAssertAndTrack+ , optimizeAssertSoft+ , optimizeMaximize+ , optimizeMinimize+ , optimizePush+ , optimizePop+ , optimizeCheck+ , optimizeGetReasonUnknown+ , optimizeGetModel+ , optimizeGetUnsatCore+ , optimizeSetParams+ , optimizeGetLower+ , optimizeGetUpper+ , optimizeGetUpperAsVector+ , optimizeGetLowerAsVector+ , optimizeToString+ , optimizeFromString+ , optimizeFromFile+ , optimizeGetHelp+ , optimizeGetAssertions+ , optimizeGetObjectives+ -- * Solvers , Logic(..) , mkSolver@@ -412,6 +475,7 @@ , solverCheck , solverCheckAssumptions , solverGetModel+ , solverGetProof , solverGetUnsatCore , solverGetReasonUnknown , solverToString@@ -1528,6 +1592,208 @@ mkBvNum ctx s n = mkIntegral ctx n =<< mkBvSort ctx s ---------------------------------------------------------------------+-- Sequences and regular expressions++-- | Create a sequence sort out of the sort for the elements.+mkSeqSort :: Context -> Sort -> IO Sort+mkSeqSort = liftFun1 z3_mk_seq_sort++-- | Check if s is a sequence sort.+isSeqSort :: Context -> Sort -> IO Bool+isSeqSort = liftFun1 z3_is_seq_sort++-- | Create a regular expression sort out of a sequence sort.+mkReSort :: Context -> Sort -> IO Sort+mkReSort = liftFun1 z3_mk_re_sort++-- | Check if s is a regular expression sort.+isReSort :: Context -> Sort -> IO Bool+isReSort = liftFun1 z3_is_re_sort++-- | Create a sort for 8 bit strings. This function creates a sort for ASCII+-- strings. Each character is 8 bits.+mkStringSort :: Context -> IO Sort+mkStringSort = liftFun0 z3_mk_string_sort++-- | Check if s is a string sort.+isStringSort :: Context -> Sort -> IO Bool+isStringSort = liftFun1 z3_is_string_sort++-- | Create a string constant out of the string that is passed in.+mkString :: Context -> String -> IO AST+mkString = liftFun1 z3_mk_string++-- | Determine if s is a string constant.+isString :: Context -> AST -> IO Bool+isString = liftFun1 z3_is_string++-- | Retrieve the string constant stored in s.+getString :: Context -> AST -> IO String+getString = liftFun1 z3_get_string++-- | Create an empty sequence of the sequence sort seq.+mkSeqEmpty :: Context -> Sort -> IO AST+mkSeqEmpty = liftFun1 z3_mk_seq_empty++-- | Create a unit sequence of a.+mkSeqUnit :: Context -> AST -> IO AST+mkSeqUnit = liftFun1 z3_mk_seq_unit++-- | Concatenate sequences.+mkSeqConcat :: (Integral int) => Context -> int -> [AST] -> IO AST+mkSeqConcat c i as+ | i < 0 = error "Z3.Base.mkSeqConcat: negative size"+ | i >= 0 && null as = error "Z3.Base.mkSeqConcet: empty list of expressions"+ | otherwise = marshal z3_mk_seq_concat c $ marshalArrayLen as++-- | Check if prefix is a prefix of s.+mkSeqPrefix :: Context+ -> AST -- ^ prefix+ -> AST -- ^ s+ -> IO AST+mkSeqPrefix = liftFun2 z3_mk_seq_prefix++-- | Check if suffix is a suffix of s.+mkSeqSuffix :: Context+ -> AST -- ^ suffix+ -> AST -- ^ s+ -> IO AST+mkSeqSuffix = liftFun2 z3_mk_seq_suffix++-- | Check if container contains containee.+mkSeqContains :: Context+ -> AST -- ^ container+ -> AST -- ^ containee+ -> IO AST+mkSeqContains = liftFun2 z3_mk_seq_contains++-- | Extract subsequence starting at offset of length.+mkSeqExtract :: Context+ -> AST -- ^ s+ -> AST -- ^ offset+ -> AST -- ^ length+ -> IO AST+mkSeqExtract = liftFun3 z3_mk_seq_extract++-- | Replace the first occurrence of src with dst in s.+mkSeqReplace :: Context+ -> AST -- ^ s+ -> AST -- ^ src+ -> AST -- ^ dst+ -> IO AST+mkSeqReplace = liftFun3 z3_mk_seq_replace++-- | Retrieve from s the unit sequence positioned at position index.+mkSeqAt :: Context+ -> AST -- ^ s+ -> AST -- ^ index+ -> IO AST+mkSeqAt = liftFun2 z3_mk_seq_at++-- | Return the length of the sequence s.+mkSeqLength :: Context+ -> AST -- ^ s+ -> IO AST+mkSeqLength = liftFun1 z3_mk_seq_length++-- | Return index of first occurrence of substr in s starting from offset+-- offset. If s does not contain substr, then the value is -1, if offset is the+-- length of s, then the value is -1 as well. The function is under-specified if+-- offset is negative or larger than the length of s.+mkSeqIndex :: Context+ -> AST -- ^ s+ -> AST -- ^ substr+ -> AST -- ^ offset+ -> IO AST+mkSeqIndex = liftFun3 z3_mk_seq_index++-- | Convert string to integer.+mkStrToInt :: Context -> AST -> IO AST+mkStrToInt = liftFun1 z3_mk_str_to_int++-- | Integer to string conversion.+mkIntToStr :: Context -> AST -> IO AST+mkIntToStr = liftFun1 z3_mk_int_to_str++-- | Create a regular expression that accepts the sequence.+mkSeqToRe :: Context -> AST -> IO AST+mkSeqToRe = liftFun1 z3_mk_seq_to_re++-- | Check if seq is in the language generated by the regular expression re.+mkSeqInRe :: Context+ -> AST -- ^ seq+ -> AST -- ^ re+ -> IO AST+mkSeqInRe = liftFun2 z3_mk_seq_in_re++-- | Create the regular language re+.+mkRePlus :: Context -> AST -> IO AST+mkRePlus = liftFun1 z3_mk_re_plus++-- | Create the regular language re*.+mkReStar :: Context -> AST -> IO AST+mkReStar = liftFun1 z3_mk_re_star++-- | Create the regular language [re].+mkReOption :: Context -> AST -> IO AST+mkReOption = liftFun1 z3_mk_re_option++-- | Create the union of the regular languages.+mkReUnion :: (Integral int) => Context -> int -> [AST] -> IO AST+mkReUnion c i as+ | i < 0 = error "Z3.Base.mkReUnion: negative size"+ | i >= 0 && null as = error "Z3.Base.mkReUnion: empty list of expressions"+ | otherwise = marshal z3_mk_re_union c $ marshalArrayLen as++-- | Create the concatenation of the regular languages.+mkReConcat :: (Integral int) => Context -> int -> [AST] -> IO AST+mkReConcat c i as+ | i < 0 = error "Z3.Base.mkReConcat: negative size"+ | i >= 0 && null as = error "Z3.Base.mkReConcat: empty list of expressions"+ | otherwise = marshal z3_mk_re_concat c $ marshalArrayLen as++-- | Create the range regular expression over two sequences of length 1.+mkReRange :: Context+ -> AST -- ^ lo+ -> AST -- ^ hi+ -> IO AST+mkReRange = liftFun2 z3_mk_re_range++-- | Create a regular expression loop. The supplied regular expression r is+-- repeated between lo and hi times. The lo should be below hi with one+-- exception: when supplying the value hi as 0, the meaning is to repeat the+-- argument r at least lo number of times, and with an unbounded upper bound.+mkReLoop :: (Integral int)+ => Context+ -> AST -- ^ r+ -> int -- ^ lo+ -> int -- ^ hi+ -> IO AST+mkReLoop c a i j+ | i < 0 = error "Z3.Base.mkReLoop: negative size"+ | i < 0 = error "Z3.Base.mkReLoop: empty list of expressions"+ | otherwise = liftFun3 z3_mk_re_loop c a i j++-- | Create the intersection of the regular languages.+mkReIntersect :: (Integral int) => Context -> int -> [AST] -> IO AST+mkReIntersect c i as+ | i < 0 = error "Z3.Base.mkReIntersect: negative size"+ | i >= 0 && null as = error "Z3.Base.mkReIntersect: empty list of expressions"+ | otherwise = marshal z3_mk_re_intersect c $ marshalArrayLen as++-- | Create the complement of the regular language.+mkReComplement :: Context -> AST -> IO AST+mkReComplement = liftFun1 z3_mk_re_complement++-- | Create an empty regular expression of sort re.+mkReEmpty :: Context -> Sort -> IO AST+mkReEmpty = liftFun1 z3_mk_re_empty++-- | Create an universal regular expression of sort re.+mkReFull :: Context -> Sort -> IO AST+mkReFull = liftFun1 z3_mk_re_full++ --------------------------------------------------------------------- -- Quantifiers -- | Create a pattern for quantifier instantiation.@@ -2584,6 +2850,94 @@ fixedpointGetAssertions :: Context -> Fixedpoint -> IO [AST] fixedpointGetAssertions = liftFun1 z3_fixedpoint_get_assertions +---------------------------------------------------------------------+-- Optimization facilities++newtype Optimize = Optimize { unOptimize :: ForeignPtr Z3_optimize }+ deriving Eq++instance Marshal Optimize (Ptr Z3_optimize) where+ c2h = mkC2hRefCount Optimize z3_optimize_inc_ref z3_optimize_dec_ref+ h2c fp = withForeignPtr (unOptimize fp)++mkOptimize :: Context -> IO Optimize+mkOptimize = liftFun0 z3_mk_optimize++optimizeAssert :: Context -> Optimize -> AST -> IO ()+optimizeAssert = liftFun2 z3_optimize_assert++optimizeAssertAndTrack :: Context -> Optimize -> AST -> AST -> IO ()+optimizeAssertAndTrack = liftFun3 z3_optimize_assert_and_track++optimizeAssertSoft :: Context -> Optimize -> AST -> String -> Symbol -> IO Int+optimizeAssertSoft ctx opt ast str sym =+ marshal z3_optimize_assert_soft ctx $ \f ->+ h2c opt $ \optPtr ->+ h2c ast $ \astPtr ->+ withCString str $ \strPtr ->+ h2c sym $ \symPtr ->+ f optPtr astPtr strPtr symPtr++optimizeMaximize :: Context -> Optimize -> AST -> IO Int+optimizeMaximize = liftFun2 z3_optimize_maximize++optimizeMinimize :: Context -> Optimize -> AST -> IO Int+optimizeMinimize = liftFun2 z3_optimize_minimize++optimizePush :: Context -> Optimize -> IO ()+optimizePush = liftFun1 z3_optimize_push++optimizePop :: Context -> Optimize -> IO ()+optimizePop = liftFun1 z3_optimize_pop++optimizeCheck :: Context -> Optimize -> [AST] -> IO Result+optimizeCheck ctx opt ss = marshal z3_optimize_check ctx $ \f ->+ h2c opt $ \optPtr ->+ marshalArrayLen ss $ \ssNum ssPtr ->+ f optPtr ssNum ssPtr++optimizeGetReasonUnknown :: Context -> Optimize -> IO String+optimizeGetReasonUnknown = liftFun1 z3_optimize_get_reason_unknown++optimizeGetModel :: Context -> Optimize -> IO Model+optimizeGetModel = liftFun1 z3_optimize_get_model++optimizeGetUnsatCore :: Context -> Optimize -> IO [AST]+optimizeGetUnsatCore = liftFun1 z3_optimize_get_unsat_core++optimizeSetParams :: Context -> Optimize -> Params -> IO ()+optimizeSetParams = liftFun2 z3_optimize_set_params++optimizeGetLower :: Context -> Optimize -> Int -> IO AST+optimizeGetLower = liftFun2 z3_optimize_get_lower++optimizeGetUpper :: Context -> Optimize -> Int -> IO AST+optimizeGetUpper = liftFun2 z3_optimize_get_upper++optimizeGetUpperAsVector :: Context -> Optimize -> Int -> IO [AST]+optimizeGetUpperAsVector = liftFun2 z3_optimize_get_upper_as_vector++optimizeGetLowerAsVector :: Context -> Optimize -> Int -> IO [AST]+optimizeGetLowerAsVector = liftFun2 z3_optimize_get_lower_as_vector++optimizeToString :: Context -> Optimize -> IO String+optimizeToString = liftFun1 z3_optimize_to_string++optimizeFromString :: Context -> Optimize -> String -> IO ()+optimizeFromString = liftFun2 z3_optimize_from_string++optimizeFromFile :: Context -> Optimize -> String -> IO ()+optimizeFromFile = liftFun2 z3_optimize_from_file+ +optimizeGetHelp :: Context -> Optimize -> IO String+optimizeGetHelp = liftFun1 z3_optimize_get_help++optimizeGetAssertions :: Context -> Optimize -> IO [AST]+optimizeGetAssertions = liftFun1 z3_optimize_get_assertions++optimizeGetObjectives :: Context -> Optimize -> IO [AST]+optimizeGetObjectives = liftFun1 z3_optimize_get_objectives+ -- AST vectors ? -- AST maps ?@@ -2785,6 +3139,14 @@ h2c solver $ \solverPtr -> f solverPtr +-- | Retrieve the proof for the last 'solverCheck' or 'solverCheckAssumptions'.+--+-- The error handler is invoked if a proof is not available because+-- the commands above were not invoked for the given solver,+-- or if the result was different from 'Unsat' (so 'Sat' does not have a proof).+solverGetProof :: Context -> Solver -> IO AST+solverGetProof = liftFun1 z3_solver_get_proof+ -- | Retrieve the unsat core for the last 'solverCheckAssumptions'; the unsat core is a subset of the assumptions solverGetUnsatCore :: Context -> Solver -> IO [AST] solverGetUnsatCore = liftFun1 z3_solver_get_unsat_core@@ -2902,9 +3264,7 @@ withContext ctx $ \ctxPtr -> do incRef ctxPtr xPtr contextIncRef ctx- let xFinalizer = do- decRef ctxPtr xPtr- contextDecRef ctxPtr (refCount ctx)+ let xFinalizer = do decRef ctxPtr xPtr; contextDecRef ctxPtr (refCount ctx) mk <$> newForeignPtr xPtr xFinalizer dummy_inc_ref :: Z3IncRefFun c
src/Z3/Base/C.hsc view
@@ -68,6 +68,8 @@ data Z3_fixedpoint +data Z3_optimize+ data Z3_solver data Z3_params@@ -759,6 +761,114 @@ z3_mk_unsigned_int64 :: Ptr Z3_context -> CULLong -> Ptr Z3_sort -> IO (Ptr Z3_ast) ---------------------------------------------------------------------+-- * Sequences and regular expressions++foreign import ccall unsafe "Z3_mk_seq_sort"+ z3_mk_seq_sort :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort)++foreign import ccall unsafe "Z3_is_seq_sort"+ z3_is_seq_sort :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_bool++foreign import ccall unsafe "Z3_mk_re_sort"+ z3_mk_re_sort :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_sort)++foreign import ccall unsafe "Z3_is_re_sort"+ z3_is_re_sort :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_bool++foreign import ccall unsafe "Z3_mk_string_sort"+ z3_mk_string_sort :: Ptr Z3_context -> IO (Ptr Z3_sort)++foreign import ccall unsafe "Z3_is_string_sort"+ z3_is_string_sort :: Ptr Z3_context -> Ptr Z3_sort -> IO Z3_bool++foreign import ccall unsafe "Z3_mk_string"+ z3_mk_string :: Ptr Z3_context -> Z3_string -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_is_string"+ z3_is_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_bool++foreign import ccall unsafe "Z3_get_string"+ z3_get_string :: Ptr Z3_context -> Ptr Z3_ast -> IO Z3_string++foreign import ccall unsafe "Z3_mk_seq_empty"+ z3_mk_seq_empty :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_seq_unit"+ z3_mk_seq_unit :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_seq_concat"+ z3_mk_seq_concat :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_seq_prefix"+ z3_mk_seq_prefix :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_seq_suffix"+ z3_mk_seq_suffix :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_seq_contains"+ z3_mk_seq_contains :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_seq_extract"+ z3_mk_seq_extract :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_seq_replace"+ z3_mk_seq_replace :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_seq_at"+ z3_mk_seq_at :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_seq_length"+ z3_mk_seq_length :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_seq_index"+ z3_mk_seq_index :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_str_to_int"+ z3_mk_str_to_int :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_int_to_str"+ z3_mk_int_to_str :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_seq_to_re"+ z3_mk_seq_to_re :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_seq_in_re"+ z3_mk_seq_in_re :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_re_plus"+ z3_mk_re_plus :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_re_star"+ z3_mk_re_star :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_re_option"+ z3_mk_re_option :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_re_union"+ z3_mk_re_union :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_re_concat"+ z3_mk_re_concat :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_re_range"+ z3_mk_re_range :: Ptr Z3_context -> Ptr Z3_ast -> Ptr Z3_ast -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_re_loop"+ z3_mk_re_loop :: Ptr Z3_context -> Ptr Z3_ast -> CUInt -> CUInt -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_re_intersect"+ z3_mk_re_intersect :: Ptr Z3_context -> CUInt -> Ptr (Ptr Z3_ast) -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_re_complement"+ z3_mk_re_complement :: Ptr Z3_context -> Ptr Z3_ast -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_re_empty"+ z3_mk_re_empty :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_mk_re_full"+ z3_mk_re_full :: Ptr Z3_context -> Ptr Z3_sort -> IO (Ptr Z3_ast)++--------------------------------------------------------------------- -- * Quantifiers -- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaf15c95b66dc3b0af735774ee401a6f85>@@ -1370,6 +1480,10 @@ foreign import ccall unsafe "Z3_solver_get_model" z3_solver_get_model :: Ptr Z3_context -> Ptr Z3_solver -> IO (Ptr Z3_model) +-- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gaba0fc4849eb0d1538d52aaa08f86a7c0>+foreign import ccall unsafe "Z3_solver_get_proof"+ z3_solver_get_proof :: Ptr Z3_context -> Ptr Z3_solver -> IO (Ptr Z3_ast)+ -- | Reference: <http://z3prover.github.io/api/html/group__capi.html#gabb4f8ed6a09873f5aeefe9cc01010864> foreign import ccall unsafe "Z3_solver_get_unsat_core" z3_solver_get_unsat_core :: Ptr Z3_context -> Ptr Z3_solver -> IO (Ptr Z3_ast_vector)@@ -1504,3 +1618,139 @@ -> CUInt -> Ptr (Ptr Z3_func_decl) -> IO Z3_lbool++---------------------------------------------------------------------+-- * Optimization facilities++foreign import ccall unsafe "Z3_mk_optimize"+ z3_mk_optimize :: Ptr Z3_context -> IO (Ptr Z3_optimize)++foreign import ccall unsafe "Z3_optimize_inc_ref"+ z3_optimize_inc_ref :: Ptr Z3_context -> Ptr Z3_optimize -> IO ()++foreign import ccall unsafe "Z3_optimize_dec_ref"+ z3_optimize_dec_ref :: Ptr Z3_context -> Ptr Z3_optimize -> IO ()++foreign import ccall unsafe "Z3_optimize_assert"+ z3_optimize_assert :: Ptr Z3_context -> Ptr Z3_optimize -> Ptr Z3_ast -> IO ()++foreign import ccall unsafe "Z3_optimize_assert_and_track"+ z3_optimize_assert_and_track :: Ptr Z3_context+ -> Ptr Z3_optimize+ -> Ptr Z3_ast+ -> Ptr Z3_ast+ -> IO ()++foreign import ccall unsafe "Z3_optimize_assert_soft"+ z3_optimize_assert_soft :: Ptr Z3_context+ -> Ptr Z3_optimize+ -> Ptr Z3_ast+ -> Z3_string+ -> Ptr Z3_symbol+ -> IO CUInt++foreign import ccall unsafe "Z3_optimize_maximize"+ z3_optimize_maximize :: Ptr Z3_context+ -> Ptr Z3_optimize+ -> Ptr Z3_ast+ -> IO CUInt++foreign import ccall unsafe "Z3_optimize_minimize"+ z3_optimize_minimize :: Ptr Z3_context+ -> Ptr Z3_optimize+ -> Ptr Z3_ast+ -> IO CUInt++foreign import ccall unsafe "Z3_optimize_push"+ z3_optimize_push :: Ptr Z3_context+ -> Ptr Z3_optimize+ -> IO ()++foreign import ccall unsafe "Z3_optimize_pop"+ z3_optimize_pop :: Ptr Z3_context+ -> Ptr Z3_optimize+ -> IO ()++foreign import ccall unsafe "Z3_optimize_check"+ z3_optimize_check :: Ptr Z3_context+ -> Ptr Z3_optimize+ -> CUInt+ -> Ptr (Ptr Z3_ast)+ -> IO Z3_lbool++foreign import ccall unsafe "Z3_optimize_get_reason_unknown"+ z3_optimize_get_reason_unknown :: Ptr Z3_context+ -> Ptr Z3_optimize+ -> IO Z3_string++foreign import ccall unsafe "Z3_optimize_get_model"+ z3_optimize_get_model :: Ptr Z3_context+ -> Ptr Z3_optimize+ -> IO (Ptr Z3_model)++foreign import ccall unsafe "Z3_optimize_get_unsat_core"+ z3_optimize_get_unsat_core :: Ptr Z3_context+ -> Ptr Z3_optimize+ -> IO (Ptr Z3_ast_vector)++foreign import ccall unsafe "Z3_optimize_set_params"+ z3_optimize_set_params :: Ptr Z3_context+ -> Ptr Z3_optimize+ -> Ptr Z3_params+ -> IO ()++foreign import ccall unsafe "Z3_optimize_get_lower"+ z3_optimize_get_lower :: Ptr Z3_context+ -> Ptr Z3_optimize+ -> CUInt+ -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_optimize_get_upper"+ z3_optimize_get_upper :: Ptr Z3_context+ -> Ptr Z3_optimize+ -> CUInt+ -> IO (Ptr Z3_ast)++foreign import ccall unsafe "Z3_optimize_get_lower_as_vector"+ z3_optimize_get_lower_as_vector :: Ptr Z3_context+ -> Ptr Z3_optimize+ -> CUInt+ -> IO (Ptr Z3_ast_vector)++foreign import ccall unsafe "Z3_optimize_get_upper_as_vector"+ z3_optimize_get_upper_as_vector :: Ptr Z3_context+ -> Ptr Z3_optimize+ -> CUInt+ -> IO (Ptr Z3_ast_vector)++foreign import ccall unsafe "Z3_optimize_to_string"+ z3_optimize_to_string :: Ptr Z3_context+ -> Ptr Z3_optimize+ -> IO Z3_string++foreign import ccall unsafe "Z3_optimize_from_string"+ z3_optimize_from_string :: Ptr Z3_context+ -> Ptr Z3_optimize+ -> Z3_string+ -> IO ()++foreign import ccall unsafe "Z3_optimize_from_file"+ z3_optimize_from_file :: Ptr Z3_context+ -> Ptr Z3_optimize+ -> Z3_string+ -> IO ()++foreign import ccall unsafe "Z3_optimize_get_help"+ z3_optimize_get_help :: Ptr Z3_context+ -> Ptr Z3_optimize+ -> IO Z3_string++foreign import ccall unsafe "Z3_optimize_get_assertions"+ z3_optimize_get_assertions :: Ptr Z3_context+ -> Ptr Z3_optimize+ -> IO (Ptr Z3_ast_vector)++foreign import ccall unsafe "Z3_optimize_get_objectives"+ z3_optimize_get_objectives :: Ptr Z3_context+ -> Ptr Z3_optimize+ -> IO (Ptr Z3_ast_vector)
src/Z3/Monad.hs view
@@ -207,6 +207,43 @@ , mkBitvector , mkBvNum + -- * Sequences and regular expressions+ , mkSeqSort+ , isSeqSort+ , mkReSort+ , isReSort+ , mkStringSort+ , isStringSort+ , mkString+ , isString+ , getString+ , mkSeqEmpty+ , mkSeqUnit+ , mkSeqConcat+ , mkSeqPrefix+ , mkSeqSuffix+ , mkSeqContains+ , mkSeqExtract+ , mkSeqReplace+ , mkSeqAt+ , mkSeqLength+ , mkSeqIndex+ , mkStrToInt+ , mkIntToStr+ , mkSeqToRe+ , mkSeqInRe+ , mkRePlus+ , mkReStar+ , mkReOption+ , mkReUnion+ , mkReConcat+ , mkReRange+ , mkReLoop+ , mkReIntersect+ , mkReComplement+ , mkReEmpty+ , mkReFull+ -- * Quantifiers , mkPattern , mkBound@@ -344,6 +381,7 @@ , getVersion -- * Fixedpoint+ , MonadFixedpoint(..) , Fixedpoint , fixedpointAddRule , fixedpointSetParams@@ -352,6 +390,32 @@ , fixedpointGetAnswer , fixedpointGetAssertions + -- * Optimization+ , MonadOptimize(..)+ , Optimize+ , optimizeAssert+ , optimizeAssertAndTrack+ , optimizeAssertSoft+ , optimizeMaximize+ , optimizeMinimize+ , optimizePush+ , optimizePop+ , optimizeCheck+ , optimizeGetReasonUnknown+ , optimizeGetModel+ , optimizeGetUnsatCore+ , optimizeSetParams+ , optimizeGetLower+ , optimizeGetUpper+ , optimizeGetUpperAsVector+ , optimizeGetLowerAsVector+ , optimizeToString+ , optimizeFromString+ , optimizeFromFile+ , optimizeGetHelp+ , optimizeGetAssertions+ , optimizeGetObjectives+ -- * Solvers , solverGetHelp , solverSetParams@@ -364,6 +428,7 @@ , solverCheck , solverCheckAssumptions , solverGetModel+ , solverGetProof , solverGetUnsatCore , solverGetReasonUnknown , solverToString@@ -403,6 +468,7 @@ , Params , Solver , Fixedpoint+ , Optimize , SortKind(..) , ASTKind(..) , Tactic@@ -415,7 +481,7 @@ import Data.Fixed ( Fixed, HasResolution ) import Control.Monad.Fail import Control.Monad.IO.Class ( MonadIO, liftIO )-import Control.Monad.Trans.Reader ( ReaderT, runReaderT, asks )+import Control.Monad.Trans.Reader ( ReaderT(..), runReaderT, asks ) import Control.Monad.Fix ( MonadFix ) import Data.Int ( Int64 ) import Data.List.NonEmpty (NonEmpty)@@ -430,6 +496,10 @@ getSolver :: m Base.Solver getContext :: m Base.Context +instance MonadZ3 m => MonadZ3 (ReaderT r m) where+ getSolver = ReaderT $ const getSolver+ getContext = ReaderT $ const getContext+ ------------------------------------------------- -- Lifting @@ -505,6 +575,27 @@ slv <- getFixedpoint liftIO $ f ctx slv a b +liftOptimize0 :: MonadOptimize z3 =>+ (Base.Context -> Base.Optimize -> IO b)+ -> z3 b+liftOptimize0 f_s =+ do ctx <- getContext+ liftIO . f_s ctx =<< getOptimize++liftOptimize1 :: MonadOptimize z3 =>+ (Base.Context -> Base.Optimize -> a -> IO b)+ -> a -> z3 b+liftOptimize1 f_s a =+ do ctx <- getContext+ liftIO . (\s -> f_s ctx s a) =<< getOptimize++liftOptimize2 :: MonadOptimize z3 => (Base.Context -> Base.Optimize -> a -> b -> IO c)+ -> a -> b -> z3 c+liftOptimize2 f a b = do+ ctx <- getContext+ slv <- getOptimize+ liftIO $ f ctx slv a b+ ------------------------------------------------- -- A simple Z3 monad. @@ -517,6 +608,7 @@ envSolver :: Base.Solver , envContext :: Base.Context , envFixedpoint :: Base.Fixedpoint+ , envOptimize :: Base.Optimize } instance MonadZ3 Z3 where@@ -526,6 +618,9 @@ instance MonadFixedpoint Z3 where getFixedpoint = Z3 $ asks envFixedpoint +instance MonadOptimize Z3 where+ getOptimize = Z3 $ asks envOptimize+ -- | Eval a Z3 script. evalZ3With :: Maybe Logic -> Opts -> Z3 a -> IO a evalZ3With mbLogic opts (Z3 s) = do@@ -544,7 +639,8 @@ ctx <- mkContext cfg solver <- maybe (Base.mkSolver ctx) (Base.mkSolverForLogic ctx) mbLogic fixedpoint <- Base.mkFixedpoint ctx- return $ Z3Env solver ctx fixedpoint+ optimize <- Base.mkOptimize ctx+ return $ Z3Env solver ctx fixedpoint optimize -- | Create a new Z3 environment. newEnv :: Maybe Logic -> Opts -> IO Z3Env@@ -667,11 +763,11 @@ -- constructor and projections. mkTupleSort = liftFun2 Base.mkTupleSort --- | Create a contructor+-- | Create a constructor -- -- Reference: <http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa779e39f7050b9d51857887954b5f9b0> mkConstructor :: MonadZ3 z3- => Symbol -- ^ Name of the sonstructor+ => Symbol -- ^ Name of the constructor -> Symbol -- ^ Name of recognizer function -> [(Symbol, Maybe Sort, Int)] -- ^ Name, sort option, and sortRefs -> z3 Constructor@@ -1469,6 +1565,191 @@ mkBvNum = liftFun2 Base.mkBvNum ---------------------------------------------------------------------+-- Sequences and regular expressions++-- | Create a sequence sort out of the sort for the elements.+mkSeqSort :: MonadZ3 z3 => Sort -> z3 Sort+mkSeqSort = liftFun1 Base.mkSeqSort++-- | Check if s is a sequence sort.+isSeqSort :: MonadZ3 z3 => Sort -> z3 Bool+isSeqSort = liftFun1 Base.isSeqSort++-- | Create a regular expression sort out of a sequence sort.+mkReSort :: MonadZ3 z3 => Sort -> z3 Sort+mkReSort = liftFun1 Base.mkReSort++-- | Check if s is a regular expression sort.+isReSort :: MonadZ3 z3 => Sort -> z3 Bool+isReSort = liftFun1 Base.isReSort++-- | Create a sort for 8 bit strings. This function creates a sort for ASCII+-- strings. Each character is 8 bits.+mkStringSort :: MonadZ3 z3 => z3 Sort+mkStringSort = liftScalar Base.mkStringSort++-- | Check if s is a string sort.+isStringSort :: MonadZ3 z3 => Sort -> z3 Bool+isStringSort = liftFun1 Base.isStringSort++-- | Create a string constant out of the string that is passed in.+mkString :: MonadZ3 z3 => String -> z3 AST+mkString = liftFun1 Base.mkString++-- | Determine if s is a string constant.+isString :: MonadZ3 z3 => AST -> z3 Bool+isString = liftFun1 Base.isString++-- | Retrieve the string constant stored in s.+getString :: MonadZ3 z3 => AST -> z3 String+getString = liftFun1 Base.getString++-- | Create an empty sequence of the sequence sort seq.+mkSeqEmpty :: MonadZ3 z3 => Sort -> z3 AST+mkSeqEmpty = liftFun1 Base.mkSeqEmpty++-- | Create a unit sequence of a.+mkSeqUnit :: MonadZ3 z3 => AST -> z3 AST+mkSeqUnit = liftFun1 Base.mkSeqUnit++-- | Concatenate sequences.+mkSeqConcat :: (Integral int, MonadZ3 z3) => int -> [AST] -> z3 AST+mkSeqConcat = liftFun2 Base.mkSeqConcat++-- | Check if prefix is a prefix of s.+mkSeqPrefix :: MonadZ3 z3+ => AST -- ^ prefix+ -> AST -- ^ s+ -> z3 AST+mkSeqPrefix = liftFun2 Base.mkSeqPrefix++-- | Check if suffix is a suffix of s.+mkSeqSuffix :: MonadZ3 z3+ => AST -- ^ suffix+ -> AST -- ^ s+ -> z3 AST+mkSeqSuffix = liftFun2 Base.mkSeqSuffix++-- | Check if container contains containee.+mkSeqContains :: MonadZ3 z3+ => AST -- ^ container+ -> AST -- ^ containee+ -> z3 AST+mkSeqContains = liftFun2 Base.mkSeqContains++-- | Extract subsequence starting at offset of length.+mkSeqExtract :: MonadZ3 z3+ => AST -- ^ s+ -> AST -- ^ offset+ -> AST -- ^ length+ -> z3 AST+mkSeqExtract = liftFun3 Base.mkSeqExtract++-- | Replace the first occurrence of src with dst in s.+mkSeqReplace :: MonadZ3 z3+ => AST -- ^ s+ -> AST -- ^ src+ -> AST -- ^ dst+ -> z3 AST+mkSeqReplace = liftFun3 Base.mkSeqReplace++-- | Retrieve from s the unit sequence positioned at position index.+mkSeqAt :: MonadZ3 z3+ => AST -- ^ s+ -> AST -- ^ index+ -> z3 AST+mkSeqAt = liftFun2 Base.mkSeqAt++-- | Return the length of the sequence s.+mkSeqLength :: MonadZ3 z3 => AST -> z3 AST+mkSeqLength = liftFun1 Base.mkSeqLength++-- | Return index of first occurrence of substr in s starting from offset+-- offset. If s does not contain substr, then the value is -1, if offset is the+-- length of s, then the value is -1 as well. The function is under-specified if+-- offset is negative or larger than the length of s.+mkSeqIndex :: MonadZ3 z3+ => AST -- ^ s+ -> AST -- ^ substr+ -> AST -- ^ offset+ -> z3 AST+mkSeqIndex = liftFun3 Base.mkSeqIndex++-- | Convert string to integer.+mkStrToInt :: MonadZ3 z3 => AST -> z3 AST+mkStrToInt = liftFun1 Base.mkStrToInt++-- | Integer to string conversion.+mkIntToStr :: MonadZ3 z3 => AST -> z3 AST+mkIntToStr = liftFun1 Base.mkIntToStr++-- | Create a regular expression that accepts the sequence.+mkSeqToRe :: MonadZ3 z3 => AST -> z3 AST+mkSeqToRe = liftFun1 Base.mkSeqToRe++-- | Check if seq is in the language generated by the regular expression re.+mkSeqInRe :: MonadZ3 z3+ => AST -- ^ seq+ -> AST -- ^ re+ -> z3 AST+mkSeqInRe = liftFun2 Base.mkSeqInRe++-- | Create the regular language re+.+mkRePlus :: MonadZ3 z3 => AST -> z3 AST+mkRePlus = liftFun1 Base.mkRePlus++-- | Create the regular language re*.+mkReStar :: MonadZ3 z3 => AST -> z3 AST+mkReStar = liftFun1 Base.mkReStar++-- | Create the regular language [re].+mkReOption :: MonadZ3 z3 => AST -> z3 AST+mkReOption = liftFun1 Base.mkReOption++-- | Create the union of the regular languages.+mkReUnion :: (Integral int, MonadZ3 z3) => int -> [AST] -> z3 AST+mkReUnion = liftFun2 Base.mkReUnion++-- | Create the concatenation of the regular languages.+mkReConcat :: (Integral int, MonadZ3 z3) => int -> [AST] -> z3 AST+mkReConcat = liftFun2 Base.mkReConcat++-- | Create the range regular expression over two sequences of length 1.+mkReRange :: MonadZ3 z3+ => AST -- ^ lo+ -> AST -- ^ hi+ -> z3 AST+mkReRange = liftFun2 Base.mkReRange++-- | Create a regular expression loop. The supplied regular expression r is+-- repeated between lo and hi times. The lo should be below hi with one+-- exception: when supplying the value hi as 0, the meaning is to repeat the+-- argument r at least lo number of times, and with an unbounded upper bound.+mkReLoop :: (Integral int, MonadZ3 z3)+ => AST -- ^ r+ -> int -- ^ lo+ -> int -- ^ hi+ -> z3 AST+mkReLoop = liftFun3 Base.mkReLoop++-- | Create the intersection of the regular languages.+mkReIntersect :: (Integral int, MonadZ3 z3) => int -> [AST] -> z3 AST+mkReIntersect = liftFun2 Base.mkReIntersect++-- | Create the complement of the regular language.+mkReComplement :: MonadZ3 z3 => AST -> z3 AST+mkReComplement = liftFun1 Base.mkReComplement++-- | Create an empty regular expression of sort re.+mkReEmpty :: MonadZ3 z3 => Sort -> z3 AST+mkReEmpty = liftFun1 Base.mkReEmpty++-- | Create an universal regular expression of sort re.+mkReFull :: MonadZ3 z3 => Sort -> z3 AST+mkReFull = liftFun1 Base.mkReFull+++--------------------------------------------------------------------- -- Quantifiers mkPattern :: MonadZ3 z3 => [AST] -> z3 Pattern@@ -2030,6 +2311,78 @@ fixedpointGetAssertions = liftFixedpoint0 Base.fixedpointGetAssertions ---------------------------------------------------------------------+-- Optimization++class MonadZ3 m => MonadOptimize m where+ getOptimize :: m Base.Optimize++optimizeAssert :: MonadOptimize z3 => AST -> z3 ()+optimizeAssert = liftOptimize1 Base.optimizeAssert++optimizeAssertAndTrack :: MonadOptimize z3 => AST -> AST -> z3 ()+optimizeAssertAndTrack = liftOptimize2 Base.optimizeAssertAndTrack++optimizeAssertSoft :: MonadOptimize z3 => AST -> String -> Symbol -> z3 ()+optimizeAssertSoft = undefined++optimizeMaximize :: MonadOptimize z3 => AST -> z3 Int+optimizeMaximize = liftOptimize1 Base.optimizeMaximize ++optimizeMinimize :: MonadOptimize z3 => AST -> z3 Int+optimizeMinimize = liftOptimize1 Base.optimizeMinimize ++optimizePush :: MonadOptimize z3 => z3 ()+optimizePush = liftOptimize0 Base.optimizePush++optimizePop :: MonadOptimize z3 => z3 ()+optimizePop = liftOptimize0 Base.optimizePop ++optimizeCheck :: MonadOptimize z3 => [AST] -> z3 Result+optimizeCheck = liftOptimize1 Base.optimizeCheck++optimizeGetReasonUnknown :: MonadOptimize z3 => z3 String+optimizeGetReasonUnknown = liftOptimize0 Base.optimizeGetReasonUnknown++optimizeGetModel :: MonadOptimize z3 => z3 Model+optimizeGetModel = liftOptimize0 Base.optimizeGetModel++optimizeGetUnsatCore :: MonadOptimize z3 => z3 [AST]+optimizeGetUnsatCore = liftOptimize0 Base.optimizeGetUnsatCore++optimizeSetParams :: MonadOptimize z3 => Params -> z3 ()+optimizeSetParams = liftOptimize1 Base.optimizeSetParams++optimizeGetLower :: MonadOptimize z3 => Int -> z3 AST+optimizeGetLower = liftOptimize1 Base.optimizeGetLower++optimizeGetUpper :: MonadOptimize z3 => Int -> z3 AST+optimizeGetUpper = liftOptimize1 Base.optimizeGetLower++optimizeGetUpperAsVector :: MonadOptimize z3 => Int -> z3 [AST]+optimizeGetUpperAsVector = liftOptimize1 Base.optimizeGetUpperAsVector++optimizeGetLowerAsVector :: MonadOptimize z3 => Int -> z3 [AST]+optimizeGetLowerAsVector = liftOptimize1 Base.optimizeGetLowerAsVector++optimizeToString :: MonadOptimize z3 => z3 String+optimizeToString = liftOptimize0 Base.optimizeToString++optimizeFromString :: MonadOptimize z3 => String -> z3 ()+optimizeFromString = liftOptimize1 Base.optimizeFromString++optimizeFromFile :: MonadOptimize z3 => String -> z3 ()+optimizeFromFile = liftOptimize1 Base.optimizeFromFile+ +optimizeGetHelp :: MonadOptimize z3 => z3 String+optimizeGetHelp = liftOptimize0 Base.optimizeGetHelp++optimizeGetAssertions :: MonadOptimize z3 => z3 [AST]+optimizeGetAssertions = liftOptimize0 Base.optimizeGetAssertions++optimizeGetObjectives :: MonadOptimize z3 => z3 [AST]+optimizeGetObjectives = liftOptimize0 Base.optimizeGetObjectives++--------------------------------------------------------------------- -- * Solvers -- mkSolver :: Context -> IO Solver@@ -2098,6 +2451,14 @@ -- or if the result was 'Unsat'. solverGetModel :: MonadZ3 z3 => z3 Model solverGetModel = liftSolver0 Base.solverGetModel+--+-- | Retrieve the proof for the last 'solverCheck' or 'solverCheckAssumptions'.+--+-- The error handler is invoked if a proof is not available because+-- the commands above were not invoked for the given solver,+-- or if the result was different from 'Unsat' (so 'Sat' does not have a proof).+solverGetProof :: MonadZ3 z3 => z3 AST+solverGetProof = liftSolver0 Base.solverGetProof -- | Retrieve the unsat core for the last 'solverCheckAssumptions'; the unsat core is a subset of the assumptions solverGetUnsatCore :: MonadZ3 z3 => z3 [AST]
test/Z3/Base/Spec.hs view
@@ -77,7 +77,9 @@ context "Bit-vectors" $ do specify "mkBvmul" $ \ctx ->- let bad = do+ let bad = do { x <- Z3.mkFreshIntVar ctx "x"; Z3.mkBvmul ctx x x- in bad `shouldThrow` anyZ3Error+ }+ in+ bad `shouldThrow` anyZ3Error
z3.cabal view
@@ -1,5 +1,5 @@ Name: z3-Version: 408.1+Version: 408.2 Synopsis: Bindings for the Z3 Theorem Prover Description: Bindings for the Z3 4./x/ Theorem Prover (<https://github.com/Z3Prover/z3>).@@ -30,10 +30,10 @@ Author: Iago Abal <mail@iagoabal.eu>, David Castro <david.castro.dcp@gmail.com> Maintainer: Iago Abal <mail@iagoabal.eu>-Copyright: 2012-2019, Iago Abal, David Castro+Copyright: 2012-2020, Iago Abal, David Castro Category: Math, SMT, Theorem Provers, Formal Methods, Bit vectors Build-type: Simple-Cabal-version: >= 1.8+Cabal-version: >= 1.10 Extra-source-files: README.md CHANGES.md HACKING.md @@ -64,11 +64,12 @@ Build-depends: semigroups >= 0.5 Build-tools: hsc2hs- Extensions: FlexibleInstances++ Default-language: Haskell2010+ Default-extensions: FlexibleInstances FlexibleContexts ForeignFunctionInterface MultiParamTypeClasses- Other-extensions: CPP DeriveDataTypeable EmptyDataDecls@@ -99,6 +100,8 @@ else Buildable: False + Default-language: Haskell2010+ Hs-source-dirs: examples Main-Is: Examples.hs @@ -119,7 +122,8 @@ Ghc-options: -Wall - Extensions: ScopedTypeVariables+ Default-language: Haskell2010+ Default-extensions: ScopedTypeVariables Hs-source-dirs: test