Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

deriving generic in base #53

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion CHANGES.md
Original file line number Diff line number Diff line change
@@ -1,11 +1,11 @@

# Release Notes

## 408.2

Tested (sort of) with Z3 4.8.8.

* Added Optimization API. (David Cao)
* Added Generic Instances on AST, FuncDecl, Z3Error, Z3ErrorCode. (Jeffrey Young)
* Added Sequences and regular expressions API. (Carlo Nucera)
* Added z3_solver_get_proof. ("0xd34df00d")
* Added MonadZ3 instance for ReaderT. ("0xd34df00d")
Expand Down
16 changes: 9 additions & 7 deletions src/Z3/Base.hs
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE NamedFieldPuns #-}
Expand Down Expand Up @@ -59,7 +60,7 @@ module Z3.Base (
Config
, Context
, Symbol
, AST
, AST(..)
, Sort
, TupleType(..)
, FuncDecl
Expand Down Expand Up @@ -550,6 +551,7 @@ import Foreign.C
, peekCString
, withCString )
import Foreign.Concurrent
import GHC.Generics ( Generic )

---------------------------------------------------------------------
-- * Types
Expand All @@ -576,7 +578,7 @@ newtype Symbol = Symbol { unSymbol :: Ptr Z3_symbol }
--
-- This is the data-structure used in Z3 to represent terms, formulas and types.
newtype AST = AST { unAST :: ForeignPtr Z3_ast }
deriving (Eq, Ord, Show, Typeable)
deriving (Eq, Ord, Show, Typeable, Generic)

-- | A kind of AST representing /types/.
newtype Sort = Sort { unSort :: ForeignPtr Z3_sort }
Expand All @@ -595,7 +597,7 @@ tupleProjs = map snd . namedTupleProjs

-- | A kind of AST representing function symbols.
newtype FuncDecl = FuncDecl { unFuncDecl :: ForeignPtr Z3_func_decl }
deriving (Eq, Ord, Show, Typeable)
deriving (Eq, Ord, Show, Typeable, Generic)

-- | A kind of AST representing constant and function declarations.
newtype App = App { unApp :: ForeignPtr Z3_app }
Expand Down Expand Up @@ -2122,7 +2124,7 @@ mkExistsConst = flip mkExistsWConst 0
getSymbolString :: Context -> Symbol -> IO String
getSymbolString = liftFun1 z3_get_symbol_string

-- | Return the sort name as a symbol.
-- | Return the sort name as a symbol.
getSortName :: Context -> Sort -> IO Symbol
getSortName = liftFun1 z3_get_sort_name

Expand Down Expand Up @@ -2930,7 +2932,7 @@ data Z3Error = Z3Error
{ errCode :: Z3ErrorCode
, errMsg :: String
}
deriving Typeable
deriving (Typeable, Generic)

instance Show Z3Error where
show (Z3Error _ s) = "Z3 error: " ++ s
Expand All @@ -2939,7 +2941,7 @@ instance Show Z3Error where
data Z3ErrorCode = SortError | IOB | InvalidArg | ParserError | NoParser
| InvalidPattern | MemoutFail | FileAccessError | InternalFatal
| InvalidUsage | DecRefError | Z3Exception
deriving (Show, Typeable)
deriving (Show, Typeable, Generic)

toZ3Error :: Z3_error_code -> Z3ErrorCode
toZ3Error e
Expand Down Expand Up @@ -3118,7 +3120,7 @@ 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

Expand Down
12 changes: 6 additions & 6 deletions src/Z3/Monad.hs
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ module Z3.Monad

-- * Types
, Symbol
, AST
, AST(..)
, Sort
, FuncDecl
, App
Expand Down Expand Up @@ -462,7 +462,7 @@ module Z3.Monad
import Z3.Opts
import Z3.Base
( Symbol
, AST
, AST(..)
, Sort
, TupleType
, FuncDecl
Expand Down Expand Up @@ -2381,16 +2381,16 @@ optimizeAssertSoft :: MonadOptimize z3 => AST -> String -> Symbol -> z3 ()
optimizeAssertSoft = undefined

optimizeMaximize :: MonadOptimize z3 => AST -> z3 Int
optimizeMaximize = liftOptimize1 Base.optimizeMaximize
optimizeMaximize = liftOptimize1 Base.optimizeMaximize

optimizeMinimize :: MonadOptimize z3 => AST -> z3 Int
optimizeMinimize = liftOptimize1 Base.optimizeMinimize
optimizeMinimize = liftOptimize1 Base.optimizeMinimize

optimizePush :: MonadOptimize z3 => z3 ()
optimizePush = liftOptimize0 Base.optimizePush

optimizePop :: MonadOptimize z3 => z3 ()
optimizePop = liftOptimize0 Base.optimizePop
optimizePop = liftOptimize0 Base.optimizePop

optimizeCheck :: MonadOptimize z3 => [AST] -> z3 Result
optimizeCheck = liftOptimize1 Base.optimizeCheck
Expand Down Expand Up @@ -2427,7 +2427,7 @@ optimizeFromString = liftOptimize1 Base.optimizeFromString

optimizeFromFile :: MonadOptimize z3 => String -> z3 ()
optimizeFromFile = liftOptimize1 Base.optimizeFromFile

optimizeGetHelp :: MonadOptimize z3 => z3 String
optimizeGetHelp = liftOptimize0 Base.optimizeGetHelp

Expand Down