diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -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) diff --git a/src/Z3/Base.hs b/src/Z3/Base.hs --- a/src/Z3/Base.hs +++ b/src/Z3/Base.hs @@ -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 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 @@ -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: @@ -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: +foreign import ccall unsafe "Z3_solver_get_proof" + z3_solver_get_proof :: Ptr Z3_context -> Ptr Z3_solver -> IO (Ptr Z3_ast) + -- | 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) @@ -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) diff --git a/src/Z3/Monad.hs b/src/Z3/Monad.hs --- a/src/Z3/Monad.hs +++ b/src/Z3/Monad.hs @@ -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: 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] diff --git a/test/Z3/Base/Spec.hs b/test/Z3/Base/Spec.hs --- a/test/Z3/Base/Spec.hs +++ b/test/Z3/Base/Spec.hs @@ -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 diff --git a/z3.cabal b/z3.cabal --- a/z3.cabal +++ b/z3.cabal @@ -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 (). @@ -30,10 +30,10 @@ Author: Iago Abal , David Castro Maintainer: Iago Abal -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