smtlib2 0.1 → 0.2
raw patch · 8 files changed
+508/−436 lines, 8 filesdep ~atto-lisp
Dependency ranges changed: atto-lisp
Files
- Language/SMTLib2/Connection.hs +14/−19
- Language/SMTLib2/Internals.hs +104/−71
- Language/SMTLib2/Internals/Instances.hs +58/−39
- Language/SMTLib2/Internals/Interface.hs +68/−104
- Language/SMTLib2/Internals/Optimize.hs +37/−30
- Language/SMTLib2/Pipe.hs +224/−169
- Language/SMTLib2/Strategy.hs +0/−2
- smtlib2.cabal +3/−2
Language/SMTLib2/Connection.hs view
@@ -12,16 +12,13 @@ import Language.SMTLib2.Internals import Control.Concurrent.MVar-import Control.Monad.State (runStateT)-import Control.Monad.Reader (runReaderT) import Control.Monad.Trans (MonadIO,liftIO) import Control.Exception import Prelude (($),IO,return) -- | Represents a connection to an SMT solver. -- The SMT solver runs in a seperate thread and communication is handled via handles.-data SMTConnection b = SMTConnection { backend :: b- , status :: MVar SMTState+data SMTConnection b = SMTConnection { backend :: MVar b } -- | Create a new connection to a SMT solver by spawning a shell command.@@ -29,23 +26,21 @@ open :: (MonadIO m,SMTBackend b m) => b -- ^ The backend for the SMT solver. -> m (SMTConnection b) open solver = do- st <- liftIO $ newMVar emptySMTState- return (SMTConnection { backend = solver- , status = st- })+ st <- liftIO $ newMVar solver+ return (SMTConnection { backend = st }) -- | Closes an open SMT connection. Do not use the connection afterwards. close :: (MonadIO m,SMTBackend b m) => SMTConnection b -> m () close conn = do- st <- liftIO $ takeMVar (status conn)- smtHandle (backend conn) st SMTExit+ st <- liftIO $ takeMVar (backend conn)+ smtHandle st SMTExit return () -withConnection :: MonadIO m => SMTConnection b -> (b -> SMTState -> m (a,SMTState)) -> m a+withConnection :: MonadIO m => SMTConnection b -> (b -> m (a,b)) -> m a withConnection conn f = do- st <- liftIO $ takeMVar (status conn)- (res,nst) <- f (backend conn) st- liftIO $ putMVar (status conn) nst+ b <- liftIO $ takeMVar (backend conn)+ (res,nb) <- f b+ liftIO $ putMVar (backend conn) nb return res -- | Perform an action in the SMT solver associated with this connection and return the result.@@ -53,18 +48,18 @@ => SMTConnection b -- ^ The connection to the SMT solver to use -> SMT' m a -- ^ The action to perform -> m a-performSMT conn act = withConnection conn (\b st -> runStateT (runReaderT (runSMT act) (AnyBackend b)) st)+performSMT conn act = withConnection conn (runSMT act) performSMTExitCleanly :: SMTBackend b IO => SMTConnection b -> SMT' IO a -> IO a performSMTExitCleanly conn act = do- st <- takeMVar (status conn)+ b <- takeMVar (backend conn) catch (do- (res,nst) <- runStateT (runReaderT (runSMT act) (AnyBackend $ backend conn)) st- putMVar (status conn) nst+ (res,nb) <- runSMT act b+ putMVar (backend conn) nb return res) (\e -> do- smtHandle (backend conn) st SMTExit+ smtHandle b SMTExit throw (e :: SomeException))
Language/SMTLib2/Internals.hs view
@@ -4,8 +4,6 @@ import Language.SMTLib2.Internals.Operators import Language.SMTLib2.Strategy -import Control.Monad.Reader hiding (mapM,mapM_)-import Control.Monad.State hiding (mapM,mapM_) import Data.Typeable import Data.Map as Map hiding (assocs,foldl) import Data.Ratio@@ -27,7 +25,9 @@ -- Monad stuff import Control.Applicative (Applicative(..))-import Control.Monad.State.Lazy as Lazy (StateT)+import Control.Monad.Trans+import Control.Monad.Fix+import Control.Monad (ap,when) data SMTRequest response where SMTSetLogic :: String -> SMTRequest ()@@ -35,12 +35,13 @@ SMTSetOption :: SMTOption -> SMTRequest () SMTAssert :: SMTExpr Bool -> Maybe InterpolationGroup -> Maybe ClauseId -> SMTRequest () SMTCheckSat :: Maybe Tactic -> CheckSatLimits -> SMTRequest CheckSatResult+ SMTDeclaredDataTypes :: SMTRequest DataTypeInfo SMTDeclareDataTypes :: TypeCollection -> SMTRequest () SMTDeclareSort :: String -> Integer -> SMTRequest () SMTPush :: SMTRequest () SMTPop :: SMTRequest ()- SMTDefineFun :: SMTType res => FunInfo -> [FunInfo] -> SMTExpr res -> SMTRequest ()- SMTDeclareFun :: FunInfo -> SMTRequest ()+ SMTDefineFun :: (Args arg,SMTType res) => Maybe String -> Proxy arg -> ArgAnnotation arg -> SMTExpr res -> SMTRequest Integer+ SMTDeclareFun :: FunInfo -> SMTRequest Integer SMTGetValue :: SMTValue t => SMTExpr t -> SMTRequest t SMTGetModel :: SMTRequest SMTModel SMTGetProof :: SMTRequest (SMTExpr Bool)@@ -50,6 +51,9 @@ SMTComment :: String -> SMTRequest () SMTExit :: SMTRequest () SMTApply :: Tactic -> SMTRequest [SMTExpr Bool]+ SMTNameExpr :: String -> SMTExpr t -> SMTRequest Integer+ SMTNewInterpolationGroup :: SMTRequest InterpolationGroup+ SMTNewClauseId :: SMTRequest ClauseId deriving Typeable data SMTModel = SMTModel { modelFunctions :: Map Integer (Integer,[ProxyArg],SMTExpr Untyped)@@ -68,7 +72,9 @@ deriving (Show,Eq,Ord,Typeable) class Monad m => SMTBackend a m where- smtHandle :: Typeable response => a -> SMTState -> SMTRequest response -> m response+ smtHandle :: Typeable response => a -> SMTRequest response -> m (response,a)+ smtGetNames :: a -> m (Integer -> String)+ smtNextName :: a -> m (Maybe String -> String) -- | Haskell types which can be represented in SMT class (Ord t,Typeable t,@@ -92,7 +98,7 @@ type ArgumentSort = Fix ArgumentSort' data Unmangling a = PrimitiveUnmangling (Value -> SMTAnnotation a -> Maybe a)- | ComplexUnmangling (forall m. Monad m => (forall b. SMTValue b => SMTExpr b -> SMTAnnotation b -> m b) -> SMTExpr a -> SMTAnnotation a -> m (Maybe a))+ | ComplexUnmangling (forall m s. Monad m => (forall b. SMTValue b => s -> SMTExpr b -> SMTAnnotation b -> m (b,s)) -> s -> SMTExpr a -> SMTAnnotation a -> m (Maybe a,s)) data Mangling a = PrimitiveMangling (a -> SMTAnnotation a -> Value) | ComplexMangling (a -> SMTAnnotation a -> SMTExpr a)@@ -117,64 +123,49 @@ -- | An array which maps indices of type /i/ to elements of type /v/. data SMTArray (i :: *) (v :: *) = SMTArray deriving (Eq,Ord,Typeable) -data FunInfo = forall arg r. (Args arg,SMTType r) => FunInfo { funInfoId :: Integer- , funInfoProxy :: Proxy (arg,r)+data FunInfo = forall arg r. (Args arg,SMTType r) => FunInfo { funInfoProxy :: Proxy (arg,r) , funInfoArgAnn :: ArgAnnotation arg , funInfoResAnn :: SMTAnnotation r- , funInfoName :: Maybe (String,Integer)+ , funInfoName :: Maybe String } -data SMTState = SMTState { nextVar :: Integer- , nextInterpolationGroup :: Integer- , nextClauseId :: Integer- , allVars :: Map Integer FunInfo- , namedVars :: Map (String,Integer) Integer- , nameCount :: Map String Integer- , declaredDataTypes :: DataTypeInfo }- data AnyBackend m = forall b. SMTBackend b m => AnyBackend b -- | The SMT monad used for communating with the SMT solver-data SMT' m a = SMT { runSMT :: ReaderT (AnyBackend m) (Lazy.StateT SMTState m) a }+data SMT' m a = SMT { runSMT :: forall b. SMTBackend b m => b -> m (a,b) } type SMT = SMT' IO instance Functor m => Functor (SMT' m) where- fmap f = SMT . fmap f . runSMT+ fmap f (SMT g) = SMT $ \b -> fmap (\(r,b) -> (f r,b)) (g b) instance Monad m => Monad (SMT' m) where- return = SMT . return- m >>= f = SMT $ (runSMT m) >>= runSMT . f+ return x = SMT $ \b -> return (x,b)+ (SMT f) >>= g = SMT $ \b -> do+ (r,b1) <- f b+ case g r of+ SMT act -> act b1 instance MonadIO m => MonadIO (SMT' m) where- liftIO = SMT . liftIO+ liftIO act = SMT $ \b -> do+ res <- liftIO act+ return (res,b) instance MonadFix m => MonadFix (SMT' m) where- mfix f = SMT $ mfix (runSMT . f)+ mfix f = SMT $ \b -> mfix (\(~(res,_)) -> case f res of+ ~(SMT act) -> act b) instance (Monad m,Functor m) => Applicative (SMT' m) where pure = return (<*>) = ap ---askSMT :: Monad m => SMT' b m b---askSMT = SMT ask--smtBackend :: Monad m => (forall b. SMTBackend b m => b -> SMT' m a) -> SMT' m a-smtBackend f = SMT $ do- AnyBackend backend <- ask- runSMT $ f backend--getSMT :: Monad m => SMT' m SMTState-getSMT = SMT get--putSMT :: Monad m => SMTState -> SMT' m ()-putSMT = SMT . put--modifySMT :: Monad m => (SMTState -> SMTState) -> SMT' m ()-modifySMT f = SMT $ modify f+smtBackend :: Monad m => (forall b. SMTBackend b m => b -> m (res,b)) -> SMT' m res+smtBackend f = SMT f instance MonadTrans SMT' where- lift = SMT . lift . lift+ lift act = SMT $ \b -> do+ res <- act+ return (res,b) data Untyped = forall t. SMTType t => Untyped t deriving Typeable @@ -209,6 +200,7 @@ data SMTExpr t where Var :: SMTType t => Integer -> SMTAnnotation t -> SMTExpr t QVar :: SMTType t => Integer -> Integer -> SMTAnnotation t -> SMTExpr t+ FunArg :: SMTType t => Integer -> SMTAnnotation t -> SMTExpr t Const :: SMTValue t => t -> SMTAnnotation t -> SMTExpr t AsArray :: (Args arg,SMTType res) => SMTFunction arg res -> ArgAnnotation arg -> SMTExpr (SMTArray arg res)@@ -406,26 +398,16 @@ withSMTBackendExitCleanly backend act = bracket (return backend)- (\backend -> smtHandle backend emptySMTState SMTExit)- (\backend -> withSMTBackend' (AnyBackend backend) False act)--withSMTBackend :: SMTBackend b m => b -> SMT' m a -> m a-withSMTBackend backend act = withSMTBackend' (AnyBackend backend) True act+ (\backend -> smtHandle backend SMTExit)+ (\backend -> withSMTBackend' backend False act) -emptySMTState :: SMTState-emptySMTState = SMTState { nextVar = 0- , nextInterpolationGroup = 0- , nextClauseId = 0- , allVars = Map.empty- , namedVars = Map.empty- , nameCount = Map.empty- , declaredDataTypes = emptyDataTypeInfo- }+withSMTBackend :: SMTBackend a m => a -> SMT' m b -> m b+withSMTBackend b = withSMTBackend' b True -withSMTBackend' :: AnyBackend m -> Bool -> SMT' m a -> m a-withSMTBackend' backend@(AnyBackend b) mustExit f = do- (res,st) <- runStateT (runReaderT (runSMT f) backend) emptySMTState- when mustExit (smtHandle b st SMTExit)+withSMTBackend' :: SMTBackend a m => a -> Bool -> SMT' m b -> m b+withSMTBackend' backend mustExit f = do+ (res,nbackend) <- runSMT f backend+ when mustExit (smtHandle nbackend SMTExit >> return ()) return res funInfoSort :: FunInfo -> Sort@@ -438,7 +420,7 @@ , funInfoArgAnn = ann }) = getSorts (undefined::a) ann -newVariableId :: (Monad m) => Maybe String -> (Integer -> Maybe Integer -> (r,FunInfo)) -> SMT' m r+{-newVariableId :: (Monad m) => Maybe String -> (Integer -> Maybe Integer -> (r,FunInfo)) -> SMT' m r newVariableId name f = do st <- getSMT let idx = nextVar st@@ -501,7 +483,7 @@ nameVariable var name = do st <- getSMT let c = Map.findWithDefault 0 name (nameCount st)- putSMT $ st { nameCount = Map.insert name (c+1) (nameCount st) }+ putSMT $ st { nameCount = Map.insert name (c+1) (nameCount st) }-} argsSignature :: Args a => a -> ArgAnnotation a -> [Sort] argsSignature arg ann@@ -536,13 +518,14 @@ sortToArgumentSort (Fix s) = Fix (NormalSort (fmap sortToArgumentSort s)) declareType :: (Monad m,SMTType t) => t -> SMTAnnotation t -> SMT' m ()-declareType (_::t) ann = do- st <- getSMT- let (colls,ndts) = getNewTypeCollections (Proxy::Proxy t) ann- (declaredDataTypes st)- nst = st { declaredDataTypes = ndts }- putSMT nst- smtBackend $ \backend -> mapM_ (\coll -> lift $ smtHandle backend nst (SMTDeclareDataTypes coll)) colls+declareType (_::t) ann = smtBackend $ \b0 -> do+ (dts,b1) <- smtHandle b0 SMTDeclaredDataTypes+ let (colls,ndts) = getNewTypeCollections (Proxy::Proxy t) ann dts+ b2 <- foldlM (\backend coll -> do+ ((),nbackend) <- smtHandle backend (SMTDeclareDataTypes coll)+ return nbackend+ ) b1 colls+ return ((),b2) -- Data type info @@ -550,6 +533,7 @@ , datatypes :: Map String (DataType,TypeCollection) , constructors :: Map String (Constr,DataType,TypeCollection) , fields :: Map String (DataField,Constr,DataType,TypeCollection) }+ deriving Typeable data TypeCollection = TypeCollection { argCount :: Integer , dataTypes :: [DataType]@@ -622,6 +606,7 @@ , construct :: forall r. [Maybe ProxyArg] -> [AnyValue] -> (forall t. SMTType t => [ProxyArg] -> t -> SMTAnnotation t -> r) -> r+ , conUndefinedArgs :: forall r. [ProxyArg] -> (forall arg. Args arg => arg -> ArgAnnotation arg -> r) -> r , conTest :: forall t. SMTType t => [ProxyArg] -> t -> Bool } @@ -744,6 +729,44 @@ return (x:name,nc) unescapeName' "" = Just ("",0) +data SMTState = SMTState { nextVar :: Integer+ , nextInterpolationGroup :: Integer+ , nextClauseId :: Integer+ , allVars :: Map Integer (FunInfo,Integer)+ , namedVars :: Map (String,Integer) Integer+ , nameCount :: Map String Integer+ , declaredDataTypes :: DataTypeInfo }++emptySMTState :: SMTState+emptySMTState = SMTState { nextVar = 0+ , nextInterpolationGroup = 0+ , nextClauseId = 0+ , allVars = Map.empty+ , namedVars = Map.empty+ , nameCount = Map.empty+ , declaredDataTypes = emptyDataTypeInfo+ }++smtStateAddFun :: FunInfo -> SMTState -> (Integer,String,SMTState)+smtStateAddFun finfo st+ = (v,name',nst)+ where+ v = nextVar st+ nameBase = case funInfoName finfo of+ Nothing -> "var"+ Just n -> n+ nc = case Map.lookup nameBase (nameCount st) of+ Just n -> n+ Nothing -> 0+ name' = if nc==0+ then nameBase+ else nameBase++"_"++show nc+ nst = st { nextVar = v+1+ , allVars = Map.insert v (finfo,nc) (allVars st)+ , namedVars = Map.insert (nameBase,nc) v (namedVars st)+ , nameCount = Map.insert nameBase (nc+1) (nameCount st)+ }+ -- BitVectors #ifdef SMTLIB2_WITH_DATAKINDS@@ -999,7 +1022,11 @@ type BV64 = BitVector (BVTyped N64) instance Monad m => SMTBackend (AnyBackend m) m where- smtHandle (AnyBackend b) = smtHandle b+ smtHandle (AnyBackend b) req = do+ (res,nb) <- smtHandle b req+ return (res,AnyBackend nb)+ smtGetNames (AnyBackend b) = smtGetNames b+ smtNextName (AnyBackend b) = smtNextName b instance Show (SMTExpr t) where showsPrec = showExpr@@ -1017,6 +1044,10 @@ showsPrec 11 v . showChar ' ' . showsPrec 11 ann)+showExpr p (FunArg v ann) = showParen (p>10) (showString "FunArg " .+ showsPrec 11 v .+ showChar ' ' .+ showsPrec 11 ann) showExpr p (Const c ann) = showParen (p>10) (showString "Const " . showsPrec 11 c . showChar ' ' .@@ -1059,8 +1090,10 @@ showsPrec 11 obj . showChar ' ' . showsPrec 11 ann)-showExpr p (UntypedExpr e) = showExpr p e-showExpr p (UntypedExprValue e) = showExpr p e+showExpr p (UntypedExpr e) = showParen (p>10) (showString "UntypedExpr " .+ showExpr 11 e)+showExpr p (UntypedExprValue e) = showParen (p>10) (showString "UntypedExprValue " .+ showExpr 11 e) instance Show (SMTFunction arg res) where showsPrec _ SMTEq = showString "SMTEq"
Language/SMTLib2/Internals/Instances.hs view
@@ -59,6 +59,7 @@ extractAnnotation :: SMTExpr a -> SMTAnnotation a extractAnnotation (Var _ ann) = ann extractAnnotation (QVar _ _ ann) = ann+extractAnnotation (FunArg _ ann) = ann extractAnnotation (Const _ ann) = ann extractAnnotation (AsArray f arg) = (arg,inferResAnnotation f arg) extractAnnotation (Forall _ _ _) = ()@@ -127,6 +128,8 @@ = f (Var i ann::SMTExpr t) entype f (QVar lvl i (ProxyArg (_::t) ann)) = f (QVar lvl i ann::SMTExpr t)+entype f (FunArg i (ProxyArg (_::t) ann))+ = f (FunArg i ann::SMTExpr t) entype f (UntypedExpr x) = f x entype f (InternalObj obj (ProxyArg (_::t) ann)) = f (InternalObj obj ann :: SMTExpr t)@@ -137,6 +140,8 @@ = f (Var i ann::SMTExpr t) entypeValue f (QVar lvl i (ProxyArgValue (_::t) ann)) = f (QVar lvl i ann::SMTExpr t)+entypeValue f (FunArg i (ProxyArgValue (_::t) ann))+ = f (FunArg i ann::SMTExpr t) entypeValue f (Const (UntypedValue v) (ProxyArgValue (_::t) ann)) = case cast v of Just rv -> f (Const (rv::t) ann)@@ -196,12 +201,12 @@ instance SMTValue UntypedValue where unmangle = ComplexUnmangling $- \f val (ProxyArgValue _ ann)+ \f st val (ProxyArgValue _ ann) -> entypeValue (\(expr'::SMTExpr t) -> case cast ann of Just ann' -> do- res <- f expr' ann'- return $ Just $ UntypedValue res+ (res,nst) <- f st expr' ann'+ return (Just $ UntypedValue res,nst) ) val mangle = ComplexMangling (\(UntypedValue x) (ProxyArgValue (_::t) ann) -> case cast x of@@ -930,6 +935,7 @@ , construct = \[Just prx] [] f -> withProxyArg prx $ \(_::t) ann -> f [prx] (Nothing::Maybe t) ann+ , conUndefinedArgs = \_ f -> f () () , conTest = \args x -> case args of [s] -> withProxyArg s $ \(_::t) _ -> case cast x of@@ -946,6 +952,9 @@ [v] -> withAnyValue v $ \_ (rv::t) ann -> f [ProxyArg (undefined::t) ann] (Just rv) ann+ , conUndefinedArgs = \sorts f -> case sorts of+ [s] -> withProxyArg s $+ \(_::t) ann -> f (undefined::SMTExpr t) ann , conTest = \args x -> case args of [s] -> withProxyArg s $ \(_::t) _ -> case cast x of@@ -989,18 +998,18 @@ Nothing -> Nothing _ -> Nothing) ComplexUnmangling p- -> ComplexUnmangling $ \f (expr::SMTExpr (Maybe t)) ann -> do- isNothing <- f (App (SMTConTest- (Constructor [ProxyArg (undefined::t) (extractAnnotation expr)]- dtMaybe conNothing :: Constructor () (Maybe a))) expr- ) ()+ -> ComplexUnmangling $ \f st (expr::SMTExpr (Maybe t)) ann -> do+ (isNothing,st1) <- f st (App (SMTConTest+ (Constructor [ProxyArg (undefined::t) (extractAnnotation expr)]+ dtMaybe conNothing :: Constructor () (Maybe a))) expr+ ) () if isNothing- then return (Just Nothing)+ then return (Just Nothing,st1) else do- val <- p f (App (SMTFieldSel (Field [ProxyArg (undefined::t) (extractAnnotation expr)] dtMaybe conJust fieldFromJust)) expr) ann+ (val,st2) <- p f st1 (App (SMTFieldSel (Field [ProxyArg (undefined::t) (extractAnnotation expr)] dtMaybe conJust fieldFromJust)) expr) ann case val of- Nothing -> return Nothing- Just val' -> return (Just (Just val'))+ Nothing -> return (Nothing,st2)+ Just val' -> return (Just (Just val'),st2) mangle = case mangle of PrimitiveMangling p -> PrimitiveMangling $@@ -1047,6 +1056,7 @@ , construct = \[Just sort] args f -> withProxyArg sort $ \(_::t) ann -> f [sort] ([]::[t]) ann+ , conUndefinedArgs = \_ f -> f () () , conTest = \args x -> case args of [s] -> withProxyArg s $ \(_::t) _ -> case cast x of@@ -1058,18 +1068,21 @@ conInsert = Constr { conName = "insert" , conFields = [fieldHead ,fieldTail]- , construct = \sort args f- -> case args of- [h,t] -> withAnyValue h $- \_ (v::t) ann- -> case castAnyValue t of+ , construct = \sort args f+ -> case args of+ [h,t] -> withAnyValue h $+ \_ (v::t) ann+ -> case castAnyValue t of Just (vs,_) -> f [ProxyArg (undefined::t) ann] (v:vs) ann- , conTest = \args x -> case args of- [s] -> withProxyArg s $- \(_::t) _ -> case cast x of- Just ((_:_)::[t]) -> True- _ -> False- }+ , conUndefinedArgs = \sorts f -> case sorts of+ [s] -> withProxyArg s $+ \(_::t) ann -> f (undefined::(SMTExpr t,SMTExpr [t])) (ann,ann)+ , conTest = \args x -> case args of+ [s] -> withProxyArg s $+ \(_::t) _ -> case cast x of+ Just ((_:_)::[t]) -> True+ _ -> False+ } insert' :: SMTType a => SMTAnnotation a -> Constructor (SMTExpr a,SMTExpr [a]) [a] insert' ann = withUndef $@@ -1118,25 +1131,25 @@ t' <- pUnmangle p t ann return (h':t') cUnmangle :: Monad m- => ((forall b. SMTValue b => SMTExpr b -> SMTAnnotation b -> m b)- -> SMTExpr a -> SMTAnnotation a -> m (Maybe a))- -> (forall b. SMTValue b => SMTExpr b -> SMTAnnotation b -> m b)- -> SMTExpr [a] -> SMTAnnotation a -> m (Maybe [a])- cUnmangle c f (expr::SMTExpr [t]) ann = do- isNil <- f (App (SMTConTest- (Constructor [ProxyArg (undefined::t) ann] dtList conNil- ::Constructor () [t]))- expr) ()+ => ((forall b. SMTValue b => st -> SMTExpr b -> SMTAnnotation b -> m (b,st))+ -> st -> SMTExpr a -> SMTAnnotation a -> m (Maybe a,st))+ -> (forall b. SMTValue b => st -> SMTExpr b -> SMTAnnotation b -> m (b,st))+ -> st -> SMTExpr [a] -> SMTAnnotation a -> m (Maybe [a],st)+ cUnmangle c f st (expr::SMTExpr [t]) ann = do+ (isNil,st1) <- f st (App (SMTConTest+ (Constructor [ProxyArg (undefined::t) ann] dtList conNil+ ::Constructor () [t]))+ expr) () if isNil- then return (Just [])+ then return (Just [],st1) else do- h <- c f (App (SMTFieldSel (Field [ProxyArg (undefined::t) ann] dtList conInsert fieldHead))+ (h,st2) <- c f st1 (App (SMTFieldSel (Field [ProxyArg (undefined::t) ann] dtList conInsert fieldHead)) expr) ann- t <- cUnmangle c f (App (SMTFieldSel (Field [ProxyArg (undefined::t) ann] dtList conInsert fieldTail)) expr) ann- return $ do- h' <- h- t' <- t- return $ h':t'+ (t,st3) <- cUnmangle c f st2 (App (SMTFieldSel (Field [ProxyArg (undefined::t) ann] dtList conInsert fieldTail)) expr) ann+ return (do+ h' <- h+ t' <- t+ return $ h':t',st3) mangle = case mangle of PrimitiveMangling p -> PrimitiveMangling $ pMangle p@@ -1506,6 +1519,9 @@ r -> r compareExprs (QVar _ _ _) _ = LT compareExprs _ (QVar _ _ _) = GT+compareExprs (FunArg i _) (FunArg j _) = compare i j+compareExprs (FunArg _ _) _ = LT+compareExprs _ (FunArg _ _) = GT compareExprs (Const i _) (Const j _) = case cast j of Just j' -> compare i j' Nothing -> compare (typeOf i) (typeOf j)@@ -1571,6 +1587,9 @@ (QVar l1 v1 _,QVar l2 v2 _) -> if l1==l2 && v1==v2 then Just True else Nothing+ (FunArg v1 _,FunArg v2 _) -> if v1==v2+ then Just True+ else Nothing (Const v1 _,Const v2 _) -> Just $ v1 == v2 (AsArray f1 arg1,AsArray f2 arg2) -> case cast f2 of Nothing -> Nothing
Language/SMTLib2/Internals/Interface.hs view
@@ -12,7 +12,6 @@ import Data.Array import Data.Unit import Data.List (genericReplicate)-import Control.Monad.Trans (lift) import Data.Proxy -- | Check if the model is satisfiable (e.g. if there is a value for each variable so that every assertion holds)@@ -25,9 +24,7 @@ -- | Like 'checkSat', but gives you more options like choosing a tactic (Z3 only) or providing memory/time-limits checkSat' :: Monad m => Maybe Tactic -> CheckSatLimits -> SMT' m CheckSatResult-checkSat' tactic limits = smtBackend $ \backend -> do- st <- getSMT- lift $ smtHandle backend st (SMTCheckSat tactic limits)+checkSat' tactic limits = smtBackend $ \b -> smtHandle b (SMTCheckSat tactic limits) isSat :: CheckSatResult -> Bool isSat Sat = True@@ -36,21 +33,15 @@ -- | Apply the given tactic to the current assertions. (Works only with Z3) apply :: Monad m => Tactic -> SMT' m [SMTExpr Bool]-apply t = smtBackend $ \backend -> do- st <- getSMT- lift $ smtHandle backend st (SMTApply t)+apply t = smtBackend $ \backend -> smtHandle backend (SMTApply t) -- | Push a new context on the stack push :: Monad m => SMT' m ()-push = smtBackend $ \backend -> do- st <- getSMT- lift $ smtHandle backend st SMTPush+push = smtBackend $ \b -> smtHandle b SMTPush -- | Pop a new context from the stack pop :: Monad m => SMT' m ()-pop = smtBackend $ \backend -> do- st <- getSMT- lift $ smtHandle backend st SMTPop+pop = smtBackend $ \b -> smtHandle b SMTPop -- | Perform a stacked operation, meaning that every assertion and declaration made in it will be undone after the operation. stack :: Monad m => SMT' m a -> SMT' m a@@ -63,9 +54,7 @@ -- | Insert a comment into the SMTLib2 command stream. -- If you aren't looking at the command stream for debugging, this will do nothing. comment :: Monad m => String -> SMT' m ()-comment msg = smtBackend $ \backend -> do- st <- getSMT- lift $ smtHandle backend st (SMTComment msg)+comment msg = smtBackend $ \b -> smtHandle b (SMTComment msg) -- | Create a new named variable varNamed :: (SMTType t,Typeable t,Unit (SMTAnnotation t),Monad m) => String -> SMT' m (SMTExpr t)@@ -86,8 +75,8 @@ -- | Create a fresh untyped variable with a name untypedNamedVar :: Monad m => String -> Sort -> SMT' m (SMTExpr Untyped) untypedNamedVar name sort = do- st <- getSMT- withSort (declaredDataTypes st) sort $+ dts <- smtBackend $ \b -> smtHandle b SMTDeclaredDataTypes+ withSort dts sort $ \(_::t) ann -> do v <- varNamedAnn name ann return $ UntypedExpr (v::SMTExpr t)@@ -95,8 +84,8 @@ -- | Create a fresh untyped variable untypedVar :: Monad m => Sort -> SMT' m (SMTExpr Untyped) untypedVar sort = do- st <- getSMT- withSort (declaredDataTypes st) sort $+ dts <- smtBackend $ \b -> smtHandle b SMTDeclaredDataTypes+ withSort dts sort $ \(_::t) ann -> do v <- varAnn ann return $ UntypedExpr (v::SMTExpr t)@@ -113,15 +102,17 @@ argVarsAnnNamed' :: (Args a,Monad m) => Maybe String -> ArgAnnotation a -> SMT' m a argVarsAnnNamed' name ann = do (_,arg) <- foldExprs (\_ (_::SMTExpr t) ann' -> do- (res,info) <- newVariable name ann'- smtBackend $ \backend -> do- declareType (undefined::t) ann'- st <- getSMT- lift $ smtHandle backend st (SMTDeclareFun info)- case additionalConstraints (undefined::t) ann' of- Nothing -> return ()- Just constr -> mapM_ assert $ constr res- return ((),res)+ declareType (undefined::t) ann'+ let info = FunInfo { funInfoProxy = Proxy::Proxy ((),t)+ , funInfoArgAnn = ()+ , funInfoResAnn = ann'+ , funInfoName = name }+ res <- smtBackend $ \b -> smtHandle b (SMTDeclareFun info)+ let expr = Var res ann'+ case additionalConstraints (undefined::t) ann' of+ Nothing -> return ()+ Just constr -> mapM_ assert $ constr expr+ return ((),expr) ) () undefined ann return arg @@ -138,18 +129,14 @@ constantAnn x ann = Const x ann getValue :: (SMTValue t,Monad m) => SMTExpr t -> SMT' m t-getValue expr = smtBackend $ \backend -> do- st <- getSMT- lift $ smtHandle backend st (SMTGetValue expr)+getValue expr = smtBackend $ \b -> smtHandle b (SMTGetValue expr) getValues :: (LiftArgs arg,Monad m) => arg -> SMT' m (Unpacked arg) getValues args = unliftArgs args getValue -- | Extract all assigned values of the model getModel :: Monad m => SMT' m SMTModel-getModel = smtBackend $ \backend -> do- st <- getSMT- lift $ smtHandle backend st SMTGetModel+getModel = smtBackend $ \b -> smtHandle b SMTGetModel -- | Extract all values of an array by giving the range of indices. unmangleArray :: (Liftable i,LiftArgs i,Ix (Unpacked i),SMTValue v,@@ -176,12 +163,9 @@ defConstNamed name = defConstNamed' (Just name) defConstNamed' :: (SMTType r,Monad m) => Maybe String -> SMTExpr r -> SMT' m (SMTExpr r)-defConstNamed' name e = smtBackend $ \backend -> do- let ann = extractAnnotation e- (fun,info) <- newVariable name ann- st <- getSMT- lift $ smtHandle backend st (SMTDefineFun info [] e)- return fun+defConstNamed' name e = do+ i <- smtBackend $ \b -> smtHandle b (SMTDefineFun name (Proxy::Proxy ()) () e)+ return (Var i (extractAnnotation e)) -- | Define a new function with a body and custom type annotations for arguments and result. defFunAnnNamed :: (Args a,SMTType r,Monad m)@@ -189,16 +173,13 @@ defFunAnnNamed name = defFunAnnNamed' (Just name) defFunAnnNamed' :: (Args a,SMTType r,Monad m)- => Maybe String -> ArgAnnotation a -> (a -> SMTExpr r) -> SMT' m (SMTFunction a r)-defFunAnnNamed' name ann_arg f = smtBackend $ \backend -> do- (au,tps) <- createArgs' ann_arg- let body = f au- ann_res = extractAnnotation body- - (fun,info) <- newFunction name ann_arg ann_res- st <- getSMT- lift $ smtHandle backend st (SMTDefineFun info tps body)- return fun+ => Maybe String -> ArgAnnotation a -> (a -> SMTExpr r)+ -> SMT' m (SMTFunction a r)+defFunAnnNamed' name ann_arg (f::a -> SMTExpr r) = do+ let (_,rargs) = foldExprsId (\i _ ann -> (i+1,FunArg i ann)) 0 (undefined::a) ann_arg+ body = f rargs+ i <- smtBackend $ \b -> smtHandle b (SMTDefineFun name (Proxy::Proxy a) ann_arg body)+ return (SMTFun i (extractAnnotation body)) -- | Like `defFunAnnNamed`, but defaults the function name to "fun". defFunAnn :: (Args a,SMTType r,Monad m)@@ -230,49 +211,33 @@ -- | Asserts that a boolean expression is true assert :: Monad m => SMTExpr Bool -> SMT' m ()-assert expr = smtBackend $ \backend -> do- st <- getSMT- lift $ smtHandle backend st (SMTAssert expr Nothing Nothing)+assert expr = smtBackend $ \b -> smtHandle b (SMTAssert expr Nothing Nothing) -- | Create a new interpolation group interpolationGroup :: Monad m => SMT' m InterpolationGroup-interpolationGroup = do- st <- getSMT- let intgr = nextInterpolationGroup st- putSMT $ st { nextInterpolationGroup = succ intgr }- return (InterpolationGroup intgr)+interpolationGroup = smtBackend $ \b -> smtHandle b SMTNewInterpolationGroup -- | Assert a boolean expression and track it for an unsat core call later assertId :: Monad m => SMTExpr Bool -> SMT' m ClauseId-assertId expr = smtBackend $ \backend -> do- st <- getSMT- let cid = nextClauseId st- putSMT $ st { nextClauseId = succ cid }- lift $ smtHandle backend st (SMTAssert expr Nothing (Just $ ClauseId cid))- return (ClauseId cid)+assertId expr = smtBackend $ \b -> do+ (cid,b1) <- smtHandle b SMTNewClauseId+ ((),b2) <- smtHandle b1 (SMTAssert expr Nothing (Just cid))+ return (cid,b2) -- | Assert a boolean expression to be true and assign it to an interpolation group assertInterp :: Monad m => SMTExpr Bool -> InterpolationGroup -> SMT' m ()-assertInterp expr interp = smtBackend $ \backend -> do- st <- getSMT- lift $ smtHandle backend st (SMTAssert expr (Just interp) Nothing)+assertInterp expr interp = smtBackend $ \b -> smtHandle b (SMTAssert expr (Just interp) Nothing) getInterpolant :: Monad m => [InterpolationGroup] -> SMT' m (SMTExpr Bool)-getInterpolant grps = smtBackend $ \backend -> do- st <- getSMT- lift $ smtHandle backend st (SMTGetInterpolant grps)+getInterpolant grps = smtBackend $ \b -> smtHandle b (SMTGetInterpolant grps) -- | Set an option for the underlying SMT solver setOption :: Monad m => SMTOption -> SMT' m ()-setOption opt = smtBackend $ \backend -> do- st <- getSMT- lift $ smtHandle backend st (SMTSetOption opt)+setOption opt = smtBackend $ \b -> smtHandle b (SMTSetOption opt) -- | Get information about the underlying SMT solver getInfo :: (Monad m,Typeable i) => SMTInfo i -> SMT' m i-getInfo inf = smtBackend $ \backend -> do- st <- getSMT- lift $ smtHandle backend st (SMTGetInfo inf)+getInfo inf = smtBackend $ \b -> smtHandle b (SMTGetInfo inf) -- | Create a new uniterpreted function with annotations for -- the argument and the return type.@@ -285,18 +250,26 @@ funAnnNamed name = funAnnNamed' (Just name) funAnnNamed' :: (Liftable a, SMTType r,Monad m) => Maybe String -> ArgAnnotation a -> SMTAnnotation r -> SMT' m (SMTFunction a r)-funAnnNamed' name annArg annRet = smtBackend $ \backend -> do- (fun,info) <- newFunction name annArg annRet- st <- getSMT- lift $ smtHandle backend st (SMTDeclareFun info)- case additionalConstraints (undefined::t) annRet of- Nothing -> return ()- Just constr -> assert $ forAllAnn annArg- (\x -> case constr (fun `app` x) of- [] -> constant True- [x] -> x- xs -> and' `app` xs)- return fun+funAnnNamed' name annArg annRet+ = withUndef $ \(_::a) (_::r) -> do+ let finfo = FunInfo { funInfoProxy = Proxy::Proxy (a,r)+ , funInfoArgAnn = annArg+ , funInfoResAnn = annRet+ , funInfoName = name+ }+ i <- smtBackend $ \b -> smtHandle b (SMTDeclareFun finfo)+ let fun = SMTFun i annRet+ case additionalConstraints (undefined::t) annRet of+ Nothing -> return ()+ Just constr -> assert $ forAllAnn annArg+ (\x -> case constr (fun `app` x) of+ [] -> constant True+ [x] -> x+ xs -> and' `app` xs)+ return fun+ where+ withUndef :: (a -> r -> SMT' m (SMTFunction a r)) -> SMT' m (SMTFunction a r)+ withUndef f = f undefined undefined -- | funAnn with an annotation only for the return type. funAnnRet :: (Liftable a,SMTType r,Unit (ArgAnnotation a),Monad m)@@ -667,17 +640,14 @@ -- | Sets the logic used for the following program (Not needed for many solvers). setLogic :: Monad m => String -> SMT' m ()-setLogic name = smtBackend $ \backend -> do- st <- getSMT- lift $ smtHandle backend st (SMTSetLogic name)+setLogic name = smtBackend $ \b -> smtHandle b (SMTSetLogic name) -- | Given an arbitrary expression, this creates a named version of it and a name to reference it later on. named :: (SMTType a,SMTAnnotation a ~ (),Monad m) => String -> SMTExpr a -> SMT' m (SMTExpr a,SMTExpr a) named name expr = do- (var,info) <- newVariable (Just name) (extractAnnotation expr)- let Just (name,nc) = funInfoName info- return (Named expr name nc,var)+ i <- smtBackend $ \b -> smtHandle b (SMTNameExpr name expr)+ return (Named expr name i,Var i (extractAnnotation expr)) -- | Like `named`, but defaults the name to "named". named' :: (SMTType a,SMTAnnotation a ~ (),Monad m)@@ -686,23 +656,17 @@ -- | After an unsuccessful 'checkSat' this method extracts a proof from the SMT solver that the instance is unsatisfiable. getProof :: Monad m => SMT' m (SMTExpr Bool)-getProof = smtBackend $ \backend -> do- st <- getSMT- lift $ smtHandle backend st SMTGetProof+getProof = smtBackend $ \b -> smtHandle b SMTGetProof -- | Use the SMT solver to simplify a given expression. -- Currently only works with Z3. simplify :: (SMTType t,Monad m) => SMTExpr t -> SMT' m (SMTExpr t)-simplify expr = smtBackend $ \backend -> do- st <- getSMT- lift $ smtHandle backend st (SMTSimplify expr)+simplify expr = smtBackend $ \b -> smtHandle b (SMTSimplify expr) -- | After an unsuccessful 'checkSat', return a list of clauses which make the -- instance unsatisfiable. getUnsatCore :: Monad m => SMT' m [ClauseId]-getUnsatCore = smtBackend $ \backend -> do- st <- getSMT- lift $ smtHandle backend st SMTGetUnsatCore+getUnsatCore = smtBackend $ \b -> smtHandle b SMTGetUnsatCore optimizeExpr' :: SMTExpr a -> SMTExpr a optimizeExpr' e = case optimizeExpr e of
Language/SMTLib2/Internals/Optimize.hs view
@@ -14,42 +14,50 @@ data OptimizeBackend b = OptB b instance SMTBackend b m => SMTBackend (OptimizeBackend b) m where- smtHandle (OptB b) st (SMTAssert expr grp cid)+ smtHandle (OptB b) (SMTAssert expr grp cid) = let nexpr = case optimizeExpr expr of Just e -> e Nothing -> expr in case nexpr of- Const True _ -> return ()- _ -> smtHandle b st (SMTAssert nexpr grp cid)- smtHandle (OptB b) st (SMTDefineFun name args body)- = let nbody = case optimizeExpr body of- Just e -> e- Nothing -> body- in smtHandle b st (SMTDefineFun name args nbody)- smtHandle (OptB b) st (SMTGetValue expr)- = let nexpr = case optimizeExpr expr of- Just e -> e- Nothing -> expr- in smtHandle b st (SMTGetValue nexpr)- smtHandle (OptB b) st SMTGetProof = do- res <- smtHandle b st SMTGetProof- case optimizeExpr res of- Just e -> return e- Nothing -> return res- smtHandle (OptB b) st (SMTSimplify expr) = do+ Const True _ -> return ((),OptB b)+ _ -> do+ (res,nb) <- smtHandle b (SMTAssert nexpr grp cid)+ return (res,OptB nb)+ smtHandle (OptB b) (SMTDefineFun name prx ann body) = do+ let nbody = case optimizeExpr body of+ Just e -> e+ Nothing -> body+ (res,nb) <- smtHandle b (SMTDefineFun name prx ann nbody)+ return (res,OptB nb)+ smtHandle (OptB b) (SMTGetValue expr) = do let nexpr = case optimizeExpr expr of+ Just e -> e+ Nothing -> expr+ (res,nb) <- smtHandle b (SMTGetValue nexpr)+ return (res,OptB nb)+ smtHandle (OptB b) SMTGetProof = do+ (res,nb) <- smtHandle b SMTGetProof+ return (case optimizeExpr res of+ Just e -> e+ Nothing -> res,OptB nb)+ smtHandle (OptB b) (SMTSimplify expr) = do+ let nexpr = case optimizeExpr expr of Just e -> e Nothing -> expr- simp <- smtHandle b st (SMTSimplify nexpr)- case optimizeExpr simp of- Nothing -> return simp- Just simp' -> return simp'- smtHandle (OptB b) st (SMTGetInterpolant grps) = do- inter <- smtHandle b st (SMTGetInterpolant grps)- case optimizeExpr inter of- Nothing -> return inter- Just e -> return e- smtHandle (OptB b) st req = smtHandle b st req+ (simp,nb) <- smtHandle b (SMTSimplify nexpr)+ return (case optimizeExpr simp of+ Nothing -> simp+ Just simp' -> simp',OptB nb)+ smtHandle (OptB b) (SMTGetInterpolant grps) = do+ (inter,nb) <- smtHandle b (SMTGetInterpolant grps)+ return (case optimizeExpr inter of+ Nothing -> inter+ Just e -> e,OptB nb)+ smtHandle (OptB b) req = do+ (res,nb) <- smtHandle b req+ return (res,OptB nb)+ smtGetNames (OptB b) = smtGetNames b+ smtNextName (OptB b) = smtNextName b optimizeExpr :: SMTExpr t -> Maybe (SMTExpr t) optimizeExpr (App fun x) = let (opt,x') = foldExprsId (\opt expr ann -> case optimizeExpr expr of@@ -61,7 +69,6 @@ then Just $ App fun x' else Nothing Just res -> Just res- optimizeExpr _ = Nothing optimizeCall :: SMTFunction arg res -> arg -> Maybe (SMTExpr res)
Language/SMTLib2/Pipe.hs view
@@ -1,7 +1,7 @@ {-# LANGUAGE ViewPatterns #-} module Language.SMTLib2.Pipe (SMTPipe(),- FunctionParser(),+ FunctionParser(..), createSMTPipe, withPipe, exprToLisp,@@ -13,7 +13,9 @@ renderSMTRequest, renderSMTResponse, commonFunctions,- commonTheorems) where+ commonTheorems,+ simpleParser,+ FunctionParser'(..)) where import Language.SMTLib2.Internals as SMT import Language.SMTLib2.Internals.Instances@@ -33,7 +35,6 @@ import qualified Data.ByteString.Char8 as BS8 import Blaze.ByteString.Builder import Data.Typeable-import Data.Map (Map) import qualified Data.Map as Map import Data.Fix import Data.Proxy@@ -51,46 +52,64 @@ process. -} data SMTPipe = SMTPipe { channelIn :: Handle , channelOut :: Handle- , processHandle :: ProcessHandle }+ , processHandle :: ProcessHandle+ , smtState :: SMTState } renderExpr :: (SMTType t,Monad m) => SMTExpr t -> SMT' m String-renderExpr expr = do- st <- getSMT- return $ renderExpr' st expr- -renderExpr' :: SMTType t => SMTState -> SMTExpr t -> String-renderExpr' st expr- = let lexpr = exprToLisp expr (allVars st) (declaredDataTypes st)+renderExpr expr = smtBackend $ \b -> do+ getName <- smtGetNames b+ (dts,nb) <- smtHandle b SMTDeclaredDataTypes+ return (renderExpr' getName dts expr,nb)++renderExpr' :: SMTType t => (Integer -> String) -> DataTypeInfo -> SMTExpr t -> String+renderExpr' getName dts expr+ = let lexpr = exprToLisp expr getName dts in show lexpr instance MonadIO m => SMTBackend SMTPipe m where- smtHandle pipe st req@(SMTGetValue (expr::SMTExpr t))+ smtHandle pipe req@(SMTGetValue (expr::SMTExpr t)) = case unmangle :: Unmangling t of- PrimitiveUnmangling _ -> handleNormal pipe st req+ PrimitiveUnmangling _ -> handleNormal pipe req ComplexUnmangling f -> do- res <- f (\expr' ann -> smtHandle pipe st (SMTGetValue expr')) expr (extractAnnotation expr)+ (res,npipe) <- f (\pipe expr' ann -> smtHandle pipe (SMTGetValue expr')+ ) pipe expr (extractAnnotation expr) case res of- Just x -> return x+ Just x -> return (x,npipe) Nothing -> error $ "smtlib2: Error while unmangling expression "++show expr++" to type "++show (typeOf (undefined::t))- smtHandle pipe st req = handleNormal pipe st req+ smtHandle pipe req = handleNormal pipe req+ --smtGetState pipe = return $ smtState pipe+ smtGetNames pipe = return (\idx -> case Map.lookup idx (allVars (smtState pipe)) of+ Just (info,nc) -> case funInfoName info of+ Nothing -> escapeName (Right idx)+ Just name -> escapeName (Left (name,nc)))+ smtNextName pipe = return (\name -> case name of+ Nothing -> let nxt = nextVar (smtState pipe)+ in escapeName (Right nxt)+ Just name' -> case Map.lookup name' (nameCount (smtState pipe)) of+ Just nc -> escapeName (Left (name',nc))+ Nothing -> escapeName (Left (name',0))) -handleNormal :: (MonadIO m,Typeable a) => SMTPipe -> SMTState -> SMTRequest a -> m a-handleNormal pipe st req = do+handleNormal :: (MonadIO m,Typeable a) => SMTPipe -> SMTRequest a -> m (a,SMTPipe)+handleNormal pipe req = do case cast req of Just (_::SMTRequest ()) -> return () _ -> clearInput pipe- case renderSMTRequest st req of+ getName <- smtGetNames pipe+ nxtName <- smtNextName pipe+ case renderSMTRequest nxtName getName (declaredDataTypes $ smtState pipe) req of Left l -> putRequest pipe l+ Right "" -> return () Right msg -> liftIO $ IO.hPutStr (channelIn pipe) $ Prelude.unlines (fmap (';':) (Prelude.lines msg))- handleRequest pipe st req+ handleRequest pipe req -renderSMTRequest :: SMTState -> SMTRequest r -> Either L.Lisp String-renderSMTRequest st (SMTGetInfo SMTSolverName)+renderSMTRequest :: (Maybe String -> String) -> (Integer -> String) -> DataTypeInfo+ -> SMTRequest r -> Either L.Lisp String+renderSMTRequest _ _ _ (SMTGetInfo SMTSolverName) = Left $ L.List [L.Symbol "get-info",L.Symbol ":name"]-renderSMTRequest st (SMTGetInfo SMTSolverVersion)+renderSMTRequest _ _ _ (SMTGetInfo SMTSolverVersion) = Left $ L.List [L.Symbol "get-info",L.Symbol ":version"]-renderSMTRequest st (SMTAssert expr interp cid)- = let expr1 = exprToLisp expr (allVars st) (declaredDataTypes st)+renderSMTRequest _ getName dts (SMTAssert expr interp cid)+ = let expr1 = exprToLisp expr getName dts expr2 = case interp of Nothing -> expr1 Just (InterpolationGroup gr)@@ -106,7 +125,7 @@ ,L.Symbol ":named" ,L.Symbol (T.pack $ "_cid"++show cid)] in Left $ L.List [L.Symbol "assert",expr3]-renderSMTRequest st (SMTCheckSat tactic limits)+renderSMTRequest _ _ _ (SMTCheckSat tactic limits) = Left $ L.List (if extendedCheckSat then [L.Symbol "check-sat-using" ,case tactic of@@ -129,7 +148,8 @@ _ -> case limitMemory limits of Just _ -> True _ -> False-renderSMTRequest st (SMTDeclareDataTypes dts)+renderSMTRequest _ _ _ SMTDeclaredDataTypes = Right ""+renderSMTRequest _ _ _ (SMTDeclareDataTypes dts) = let param x = L.Symbol $ T.pack $ "arg"++show x in Left $ L.List [L.Symbol "declare-datatypes"@@ -147,109 +167,127 @@ | con <- dataTypeConstructors dt ] | dt <- dataTypes dts ] ]-renderSMTRequest st (SMTDeclareSort name arity)+renderSMTRequest _ _ _ (SMTDeclareSort name arity) = Left $ L.List [L.Symbol "declare-sort",L.Symbol $ T.pack name,L.toLisp arity]-renderSMTRequest st (SMTDeclareFun name)- = let tps = funInfoArgSorts name- rtp = funInfoSort name+renderSMTRequest nextName _ _ (SMTDeclareFun finfo)+ = let tps = funInfoArgSorts finfo+ rtp = funInfoSort finfo in Left $ L.List [L.Symbol "declare-fun"- ,L.Symbol $ T.pack $ getSMTName name+ ,L.Symbol $ T.pack (nextName (funInfoName finfo)) ,args (fmap sortToLisp tps) ,sortToLisp rtp ]-renderSMTRequest st (SMTDefineFun name arg definition)- = let ann = extractAnnotation definition- retSort = getSort (getUndef definition) ann+renderSMTRequest nextName getName dts (SMTDefineFun name (_::Proxy arg) argAnn (body::SMTExpr res))+ = let tpLst = zip [0..] (getTypes (undefined::arg) argAnn)+ annRes = extractAnnotation body+ name' = nextName name+ retSort = getSort (undefined::res) annRes in Left $ L.List [L.Symbol "define-fun"- ,L.Symbol $ T.pack $ getSMTName name- ,args [ L.List [ L.Symbol $ T.pack $ getSMTName n, sortToLisp $ funInfoSort n ]- | n <- arg ]+ ,L.Symbol $ T.pack name'+ ,args [ L.List [ L.Symbol $ T.pack $ "farg_"++show (j::Integer)+ , sortToLisp $ getSort u ann ]+ | (j,ProxyArg u ann) <- tpLst ] ,sortToLisp retSort- ,exprToLisp definition (allVars st) (declaredDataTypes st)]-renderSMTRequest st (SMTComment msg) = Right msg-renderSMTRequest st SMTExit = Left $ L.List [L.Symbol "exit"]-renderSMTRequest st (SMTGetInterpolant grps)+ ,exprToLisp body getName dts]+renderSMTRequest _ _ _ (SMTComment msg) = Right msg+renderSMTRequest _ _ _ SMTExit = Left $ L.List [L.Symbol "exit"]+renderSMTRequest _ _ _ (SMTGetInterpolant grps) = Left $ L.List [L.Symbol "get-interpolant" ,L.List [ L.Symbol $ T.pack ("i"++show g) | InterpolationGroup g <- grps ] ]-renderSMTRequest st (SMTSetOption opt)+renderSMTRequest _ _ _ (SMTSetOption opt) = Left $ L.List $ [L.Symbol "set-option"] ++(case opt of- PrintSuccess v -> [L.Symbol ":print-success"- ,L.Symbol $ if v then "true" else "false"]- ProduceModels v -> [L.Symbol ":produce-models"- ,L.Symbol $ if v then "true" else "false"]- SMT.ProduceProofs v -> [L.Symbol ":produce-proofs"- ,L.Symbol $ if v then "true" else "false"]- SMT.ProduceUnsatCores v -> [L.Symbol ":produce-unsat-cores"- ,L.Symbol $ if v then "true" else "false"]- ProduceInterpolants v -> [L.Symbol ":produce-interpolants"+ PrintSuccess v -> [L.Symbol ":print-success"+ ,L.Symbol $ if v then "true" else "false"]+ ProduceModels v -> [L.Symbol ":produce-models"+ ,L.Symbol $ if v then "true" else "false"]+ SMT.ProduceProofs v -> [L.Symbol ":produce-proofs"+ ,L.Symbol $ if v then "true" else "false"]+ SMT.ProduceUnsatCores v -> [L.Symbol ":produce-unsat-cores" ,L.Symbol $ if v then "true" else "false"]+ ProduceInterpolants v -> [L.Symbol ":produce-interpolants"+ ,L.Symbol $ if v then "true" else "false"] )-renderSMTRequest st (SMTSetLogic name)+renderSMTRequest _ _ _ (SMTSetLogic name) = Left $ L.List [L.Symbol "set-logic" ,L.Symbol $ T.pack name]-renderSMTRequest st SMTGetProof+renderSMTRequest _ _ _ SMTGetProof = Left $ L.List [L.Symbol "get-proof"]-renderSMTRequest st SMTGetUnsatCore+renderSMTRequest _ _ _ SMTGetUnsatCore = Left $ L.List [L.Symbol "get-unsat-core"]-renderSMTRequest st (SMTSimplify expr)- = let lexpr = exprToLisp expr (allVars st) (declaredDataTypes st)+renderSMTRequest _ getName dts (SMTSimplify expr)+ = let lexpr = exprToLisp expr getName dts in Left $ L.List [L.Symbol "simplify" ,lexpr]-renderSMTRequest st SMTPush = Left $ L.List [L.Symbol "push",L.toLisp (1::Integer)]-renderSMTRequest st SMTPop = Left $ L.List [L.Symbol "pop",L.toLisp (1::Integer)]-renderSMTRequest st (SMTGetValue expr)- = let lexpr = exprToLisp expr (allVars st) (declaredDataTypes st)+renderSMTRequest _ _ _ SMTPush = Left $ L.List [L.Symbol "push",L.toLisp (1::Integer)]+renderSMTRequest _ _ _ SMTPop = Left $ L.List [L.Symbol "pop",L.toLisp (1::Integer)]+renderSMTRequest _ getName dts (SMTGetValue expr)+ = let lexpr = exprToLisp expr getName dts in Left $ L.List [L.Symbol "get-value" ,L.List [lexpr]]-renderSMTRequest st SMTGetModel = Left $ L.List [L.Symbol "get-model"]-renderSMTRequest st (SMTApply tactic)+renderSMTRequest _ _ _ SMTGetModel = Left $ L.List [L.Symbol "get-model"]+renderSMTRequest _ _ _ (SMTApply tactic) = Left $ L.List [L.Symbol "apply" ,tacticToLisp tactic]+renderSMTRequest _ _ _ (SMTNameExpr _ _) = Right ""+renderSMTRequest _ _ _ SMTNewInterpolationGroup = Right ""+renderSMTRequest _ _ _ SMTNewClauseId = Right "" -handleRequest :: MonadIO m => SMTPipe -> SMTState -> SMTRequest response -> m response-handleRequest pipe _ (SMTGetInfo SMTSolverName) = do+handleRequest :: MonadIO m => SMTPipe -> SMTRequest response -> m (response,SMTPipe)+handleRequest pipe (SMTGetInfo SMTSolverName) = do res <- parseResponse pipe case res of- L.List [L.Symbol ":name",L.String name] -> return $ T.unpack name+ L.List [L.Symbol ":name",L.String name] -> return (T.unpack name,pipe) _ -> error "Invalid solver response to 'get-info' name query"-handleRequest pipe _ (SMTGetInfo SMTSolverVersion) = do+handleRequest pipe (SMTGetInfo SMTSolverVersion) = do res <- parseResponse pipe case res of- L.List [L.Symbol ":version",L.String name] -> return $ T.unpack name+ L.List [L.Symbol ":version",L.String name] -> return (T.unpack name,pipe) _ -> error "Invalid solver response to 'get-info' version query"-handleRequest pipe st (SMTAssert _ _ _) = return ()-handleRequest pipe _ (SMTCheckSat tactic limits) = do+handleRequest pipe (SMTAssert _ _ _) = return ((),pipe)+handleRequest pipe (SMTCheckSat tactic limits) = do res <- liftIO $ BS.hGetLine (channelOut pipe)- case res of- "sat" -> return Sat- "sat\r" -> return Sat- "unsat" -> return Unsat- "unsat\r" -> return Unsat- "unknown" -> return Unknown- "unknown\r" -> return Unknown- _ -> error $ "smtlib2: unknown check-sat response: "++show res-handleRequest pipe _ (SMTDeclareDataTypes dts) = return ()-handleRequest pipe _ (SMTDeclareSort name arity) = return ()-handleRequest pipe _ (SMTDeclareFun name) = return ()-handleRequest _ _ (SMTDefineFun name arg definition) = return ()-handleRequest _ _ (SMTComment msg) = return ()-handleRequest pipe _ SMTExit = do+ return (case res of+ "sat" -> Sat+ "sat\r" -> Sat+ "unsat" -> Unsat+ "unsat\r" -> Unsat+ "unknown" -> Unknown+ "unknown\r" -> Unknown+ _ -> error $ "smtlib2: unknown check-sat response: "++show res,pipe)+handleRequest pipe SMTDeclaredDataTypes = return (declaredDataTypes $ smtState pipe,pipe)+handleRequest pipe (SMTDeclareDataTypes dts) = do+ let ndts = addDataTypeStructure dts (declaredDataTypes $ smtState pipe)+ return ((),pipe { smtState = (smtState pipe) { declaredDataTypes = ndts } })+handleRequest pipe (SMTDeclareSort name arity) = return ((),pipe)+handleRequest pipe (SMTDeclareFun info)+ = let (v,name,nst) = smtStateAddFun info (smtState pipe)+ in return (v,pipe { smtState = nst })+handleRequest pipe (SMTDefineFun name (_::Proxy arg) argAnn (body::SMTExpr res)) = do+ let finfo = FunInfo { funInfoProxy = Proxy::Proxy (arg,res)+ , funInfoArgAnn = argAnn+ , funInfoResAnn = extractAnnotation body+ , funInfoName = name }+ (i,_,nst) = smtStateAddFun finfo (smtState pipe)+ return (i,pipe { smtState = nst })+handleRequest pipe (SMTComment msg) = return ((),pipe)+handleRequest pipe SMTExit = do liftIO $ hClose (channelIn pipe) liftIO $ hClose (channelOut pipe) liftIO $ terminateProcess (processHandle pipe) _ <- liftIO $ waitForProcess (processHandle pipe)- return ()-handleRequest pipe st (SMTGetInterpolant grps) = do+ return ((),pipe)+handleRequest pipe (SMTGetInterpolant grps) = do val <- parseResponse pipe case lispToExpr commonFunctions- (findName st) (declaredDataTypes st) gcast (Just $ Fix BoolSort) 0 val of- Just (Just x) -> return x+ (findName $ smtState pipe) (declaredDataTypes $ smtState pipe)+ gcast (Just $ Fix BoolSort) 0 val of+ Just (Just x) -> return (x,pipe) _ -> error $ "smtlib2: Failed to parse get-interpolant result: "++show val-handleRequest _ _ (SMTSetOption opt) = return ()-handleRequest _ _ (SMTSetLogic name) = return ()-handleRequest pipe st SMTGetProof = do+handleRequest pipe (SMTSetOption opt) = return ((),pipe)+handleRequest pipe (SMTSetLogic name) = return ((),pipe)+handleRequest pipe SMTGetProof = do res <- parseResponse pipe let proof = case res of L.List items -> case findProof items of@@ -257,36 +295,37 @@ Just p -> p _ -> res case lispToExpr (commonFunctions `mappend` commonTheorems)- (findName st)- (declaredDataTypes st) gcast (Just $ Fix BoolSort) 0 proof of- Just (Just x) -> return x+ (findName $ smtState pipe)+ (declaredDataTypes $ smtState pipe) gcast (Just $ Fix BoolSort) 0 proof of+ Just (Just x) -> return (x,pipe) _ -> error $ "smtlib2: Couldn't parse proof "++show res where findProof [] = Nothing findProof ((L.List [L.Symbol "proof",proof]):_) = Just proof findProof (x:xs) = findProof xs-handleRequest pipe _ SMTGetUnsatCore = do+handleRequest pipe SMTGetUnsatCore = do res <- parseResponse pipe case res of- L.List names -> return $- fmap (\name -> case name of- L.Symbol s -> case T.unpack s of- '_':'c':'i':'d':cid- | all isDigit cid -> ClauseId (read cid)- str -> error $ "Language.SMTLib2.getUnsatCore: Unknown clause id "++str- _ -> error $ "Language.SMTLib2.getUnsatCore: Unknown expression "- ++show name++" in core list."- ) names+ L.List names -> return+ (fmap (\name -> case name of+ L.Symbol s -> case T.unpack s of+ '_':'c':'i':'d':cid+ | all isDigit cid -> ClauseId (read cid)+ str -> error $ "Language.SMTLib2.getUnsatCore: Unknown clause id "++str+ _ -> error $ "Language.SMTLib2.getUnsatCore: Unknown expression "+ ++show name++" in core list."+ ) names,pipe) _ -> error $ "Language.SMTLib2.getUnsatCore: Unknown response "++show res++" to query."-handleRequest pipe st (SMTSimplify (expr::SMTExpr t)) = do+handleRequest pipe (SMTSimplify (expr::SMTExpr t)) = do val <- parseResponse pipe case lispToExpr commonFunctions- (findName st) (declaredDataTypes st) gcast (Just $ getSort (undefined::t) (extractAnnotation expr)) 0 val of- Just (Just x) -> return x+ (findName $ smtState pipe) (declaredDataTypes $ smtState pipe)+ gcast (Just $ getSort (undefined::t) (extractAnnotation expr)) 0 val of+ Just (Just x) -> return (x,pipe) _ -> error $ "smtlib2: Failed to parse simplify result: "++show val-handleRequest _ _ SMTPush = return ()-handleRequest _ _ SMTPop = return ()-handleRequest pipe st (SMTGetValue (expr::SMTExpr t)) = do+handleRequest pipe SMTPush = return ((),pipe)+handleRequest pipe SMTPop = return ((),pipe)+handleRequest pipe (SMTGetValue (expr::SMTExpr t)) = do let ann = extractAnnotation expr sort = getSort (undefined::t) ann PrimitiveUnmangling unm = unmangle :: Unmangling t@@ -294,16 +333,16 @@ case val of L.List [L.List [_,res]] -> let res' = removeLets res- in case lispToValue' (declaredDataTypes st) (Just sort) res' of+ in case lispToValue' (declaredDataTypes $ smtState pipe) (Just sort) res' of Just val' -> case unm val' ann of- Just val'' -> return val''+ Just val'' -> return (val'',pipe) Nothing -> error $ "smtlib2: Failed to unmangle value "++show val'++" to type "++show (typeOf (undefined::t)) Nothing -> error $ "smtlib2: Failed to parse value from "++show res _ -> error $ "smtlib2: Unexpected get-value response: "++show val-handleRequest pipe st SMTGetModel = do+handleRequest pipe SMTGetModel = do val <- parseResponse pipe case val of- L.List (L.Symbol "model":mdl) -> return $ foldl parseModel (SMTModel Map.empty) mdl+ L.List (L.Symbol "model":mdl) -> return (foldl parseModel (SMTModel Map.empty) mdl,pipe) _ -> error $ "smtlib2: Unexpected get-model response: "++show val where parseModel cur (L.List [L.Symbol "define-fun",@@ -313,7 +352,7 @@ fun]) = case mapM (\arg -> case arg of L.List [L.Symbol argName, argTp] -> case lispToSort argTp of- Just argTp' -> withSort (declaredDataTypes st) argTp' $+ Just argTp' -> withSort (declaredDataTypes $ smtState pipe ) argTp' $ \u ann -> Just (argName,ProxyArg u ann) _ -> Nothing _ -> Nothing@@ -324,13 +363,13 @@ funId = case unescapeName (T.unpack fname) of Nothing -> Nothing Just (Right idx) -> Just idx- Just (Left name) -> case Map.lookup name (namedVars st) of+ Just (Left name) -> case Map.lookup name (namedVars $ smtState pipe) of Just idx -> Just idx Nothing -> Nothing in case lispToExpr commonFunctions (\n -> do (i,tp) <- Map.lookup n argMp return $ QVar 0 i tp)- (declaredDataTypes st)+ (declaredDataTypes $ smtState pipe) UntypedExpr (Just rtp') 1@@ -343,45 +382,62 @@ Nothing -> error $ "smtlib2: Failed to parse return type: "++show rtp Nothing -> error $ "smtlib2: Failed to parse argument specification "++show args parseModel _ def = error $ "smtlib2: Failed to parse model entry: "++show def-handleRequest pipe st (SMTApply tactic) = do+handleRequest pipe (SMTApply tactic) = do val <- parseResponse pipe case val of L.List (L.Symbol "goals":goals)- -> return $- fmap (\goal -> case goal of- L.List ((L.Symbol "goal"):expr:_)- -> case lispToExpr (commonFunctions `mappend` commonTheorems)- (findName st)- (declaredDataTypes st) gcast (Just $ Fix BoolSort) 0 expr of- Just (Just x) -> x- _ -> error $ "smtlib2: Couldn't parse goal "++show expr- _ -> error $ "smtlib2: Couldn't parse goal description "++show val- ) goals+ -> return+ (fmap (\goal -> case goal of+ L.List ((L.Symbol "goal"):expr:_)+ -> case lispToExpr (commonFunctions `mappend` commonTheorems)+ (findName $ smtState pipe)+ (declaredDataTypes $ smtState pipe) gcast (Just $ Fix BoolSort) 0 expr of+ Just (Just x) -> x+ _ -> error $ "smtlib2: Couldn't parse goal "++show expr+ _ -> error $ "smtlib2: Couldn't parse goal description "++show val+ ) goals,pipe)+handleRequest pipe (SMTNameExpr name expr) = do+ return (nc,pipe { smtState = nst })+ where+ nc = case Map.lookup name (nameCount $ smtState pipe) of+ Just n -> n+ Nothing -> 0+ nst = (smtState pipe) { nameCount = Map.insert name (nc+1) (nameCount $ smtState pipe) }+handleRequest pipe SMTNewInterpolationGroup = do+ return (InterpolationGroup igrp,pipe { smtState = nst })+ where+ igrp = nextInterpolationGroup (smtState pipe)+ nst = (smtState pipe) { nextInterpolationGroup = igrp+1 }+handleRequest pipe SMTNewClauseId = do+ return (ClauseId icl,pipe { smtState = nst })+ where+ icl = nextClauseId (smtState pipe)+ nst = (smtState pipe) { nextClauseId = icl+1 } -renderSMTResponse :: SMTState -> SMTRequest response -> response -> Maybe String-renderSMTResponse _ (SMTGetInfo SMTSolverName) name+renderSMTResponse :: (Integer -> String) -> DataTypeInfo -> SMTRequest response -> response -> Maybe String+renderSMTResponse _ _ (SMTGetInfo SMTSolverName) name = Just $ show $ L.List [L.Symbol ":name",L.String $ T.pack name]-renderSMTResponse _ (SMTGetInfo SMTSolverVersion) vers+renderSMTResponse _ _ (SMTGetInfo SMTSolverVersion) vers = Just $ show $ L.List [L.Symbol ":version",L.String $ T.pack vers]-renderSMTResponse _ (SMTCheckSat _ _) res = case res of+renderSMTResponse _ _ (SMTCheckSat _ _) res = case res of Sat -> Just "sat" Unsat -> Just "unsat" Unknown -> Just "unknown"-renderSMTResponse st (SMTGetInterpolant grps) expr- = Just $ renderExpr' st expr-renderSMTResponse st SMTGetProof proof- = Just $ renderExpr' st proof-renderSMTResponse st (SMTSimplify _) expr- = Just $ renderExpr' st expr-renderSMTResponse _ (SMTGetValue _) v = Just $ show v-renderSMTResponse st (SMTApply _) goals+renderSMTResponse getName dts (SMTGetInterpolant grps) expr+ = Just $ renderExpr' getName dts expr+renderSMTResponse getName dts SMTGetProof proof+ = Just $ renderExpr' getName dts proof+renderSMTResponse getName dts (SMTSimplify _) expr+ = Just $ renderExpr' getName dts expr+renderSMTResponse _ _ (SMTGetValue _) v = Just $ show v+renderSMTResponse getName dts (SMTApply _) goals = Just $ show $ L.List $ [L.Symbol "goals"]++- [exprToLisp goal (allVars st) (declaredDataTypes st)+ [exprToLisp goal getName dts | goal <- goals ]-renderSMTResponse _ SMTGetUnsatCore core = Just (show core)-renderSMTResponse _ SMTGetModel mdl = Just (show mdl)-renderSMTResponse _ _ _ = Nothing+renderSMTResponse _ _ SMTGetUnsatCore core = Just (show core)+renderSMTResponse _ _ SMTGetModel mdl = Just (show mdl)+renderSMTResponse _ _ _ _ = Nothing -- | Spawn a new SMT solver process and create a pipe to communicate with it. createSMTPipe :: String -- ^ Path to the binary of the SMT solver@@ -403,7 +459,8 @@ (Just hin,Just hout,_,handle) <- createProcess cmd return $ SMTPipe { channelIn = hin , channelOut = hout- , processHandle = handle }+ , processHandle = handle+ , smtState = emptySMTState } sortToLisp :: Sort -> L.Lisp sortToLisp s = sortToLisp' sortToLisp (unFix s)@@ -452,10 +509,10 @@ return $ Fix $ NamedSort (T.unpack x) argSorts lispToSort _ = Nothing -getSMTName :: FunInfo -> String+{-getSMTName :: FunInfo -> String getSMTName info = escapeName (case funInfoName info of Nothing -> Right (funInfoId info)- Just name -> Left name)+ Just name -> Left name)-} findName :: SMTState -> T.Text -> Maybe (SMTExpr Untyped) findName st name = case unescapeName (T.unpack name) of@@ -464,18 +521,18 @@ Nothing -> Nothing Just (FunInfo { funInfoProxy = _::Proxy (a,t) , funInfoResAnn = ann- }) -> let expr :: SMTExpr t- expr = Var idx ann- in Just $ mkUntyped expr+ },nc) -> let expr :: SMTExpr t+ expr = Var idx ann+ in Just $ mkUntyped expr Just (Left name') -> case Map.lookup name' (namedVars st) of Nothing -> Nothing Just idx -> case Map.lookup idx (allVars st) of Nothing -> Nothing Just (FunInfo { funInfoProxy = _::Proxy (a,t) , funInfoResAnn = ann- }) -> let expr :: SMTExpr t- expr = Var idx ann- in Just $ mkUntyped expr+ },_) -> let expr :: SMTExpr t+ expr = Var idx ann+ in Just $ mkUntyped expr mkUntyped :: SMTType t => SMTExpr t -> SMTExpr Untyped mkUntyped e = case cast e of@@ -484,20 +541,18 @@ Just e' -> entypeValue UntypedExpr e' Nothing -> UntypedExpr e -exprToLisp :: SMTExpr t -> Map Integer FunInfo -> DataTypeInfo -> L.Lisp+exprToLisp :: SMTExpr t -> (Integer -> String) -> DataTypeInfo -> L.Lisp exprToLisp = exprToLispWith (\obj -> error $ "smtlib2: Can't translate internal object "++ show obj++" to s-expression.") -exprToLispWith :: (forall a. (Typeable a,Ord a,Show a) => a -> L.Lisp) -> SMTExpr t -> Map Integer FunInfo -> DataTypeInfo -> L.Lisp-exprToLispWith _ (Var idx _) mp _ = case Map.lookup idx mp of- Just info -> L.Symbol $ T.pack $- escapeName (case funInfoName info of- Nothing -> Right (funInfoId info)- Just name -> Left name)- Nothing -> L.Symbol $ T.pack $ escapeName (Right idx)+exprToLispWith :: (forall a. (Typeable a,Ord a,Show a) => a -> L.Lisp) -> SMTExpr t+ -> (Integer -> String)+ -> DataTypeInfo -> L.Lisp+exprToLispWith _ (Var idx _) mp _ = L.Symbol $ T.pack $ mp idx exprToLispWith _ (QVar lvl idx _) _ _ = L.Symbol $ T.pack $ "q_"++show lvl++"_"++show idx+exprToLispWith _ (FunArg i _) _ _ = L.Symbol $ T.pack $ "farg_"++show i exprToLispWith objs (Const x ann) mp dts = case mangle of PrimitiveMangling f -> valueToLisp dts $ f x ann ComplexMangling f -> exprToLispWith objs (f x ann) mp dts@@ -511,19 +566,19 @@ else f'] exprToLispWith objs (Forall lvl tps body) mp dts = L.List [L.Symbol "forall"- ,L.List [L.List [L.Symbol $ T.pack $ "q_"++show lvl++"_"++show i,sortToLisp sort]+ ,L.List [L.List [L.Symbol $ T.pack $ "q_"++show lvl++"_"++show (i::Integer),sortToLisp sort] | (i,tp) <- Prelude.zip [0..] tps , let sort = withProxyArg tp getSort ] ,exprToLispWith objs body mp dts] exprToLispWith objs (Exists lvl tps body) mp dts = L.List [L.Symbol "exists"- ,L.List [L.List [L.Symbol $ T.pack $ "q_"++show lvl++"_"++show i,sortToLisp sort]+ ,L.List [L.List [L.Symbol $ T.pack $ "q_"++show lvl++"_"++show (i::Integer),sortToLisp sort] | (i,tp) <- Prelude.zip [0..] tps , let sort = withProxyArg tp getSort ] ,exprToLispWith objs body mp dts] exprToLispWith objs (Let lvl args body) mp dts = L.List [L.Symbol "let"- ,L.List [L.List [L.Symbol $ T.pack $ "q_"++show lvl++"_"++show i,+ ,L.List [L.List [L.Symbol $ T.pack $ "q_"++show lvl++"_"++show (i::Integer), exprToLispWith objs def mp dts] | (i,def) <- Prelude.zip [0..] args ] ,exprToLispWith objs body mp dts]@@ -574,7 +629,7 @@ withUndef :: SMTFunction a b -> (a -> b -> r) -> r withUndef _ f = f undefined undefined -functionGetSymbol :: Map Integer FunInfo -> SMTFunction a b -> ArgAnnotation a -> L.Lisp+functionGetSymbol :: (Integer -> String) -> SMTFunction a b -> ArgAnnotation a -> L.Lisp functionGetSymbol _ SMTEq _ = L.Symbol "=" functionGetSymbol mp fun@(SMTMap f) ann = L.List [L.Symbol "_",@@ -595,8 +650,7 @@ L.List (fmap sortToLisp sigArg), sortToLisp sigRes] else sym' -functionGetSymbol mp (SMTFun name _) _ = case Map.lookup name mp of- Just info -> L.Symbol (T.pack $ getSMTName info)+functionGetSymbol mp (SMTFun i _) _ = L.Symbol (T.pack $ mp i) functionGetSymbol _ (SMTBuiltIn name _) _ = L.Symbol $ T.pack name functionGetSymbol _ (SMTOrd op) _ = L.Symbol $ case op of Ge -> ">="@@ -688,7 +742,7 @@ putRequest pipe expr = do clearInput pipe liftIO $ toByteStringIO (BS.hPutStr $ channelIn pipe) (mappend (L.fromLispExpr expr) flush)- liftIO $ BS.hPutStrLn (channelIn pipe) ""+ liftIO $ BS8.hPutStrLn (channelIn pipe) "" liftIO $ hFlush (channelIn pipe) parseResponse :: MonadIO m => SMTPipe -> m L.Lisp@@ -828,6 +882,7 @@ Just res -> Just res Nothing -> case sort of Just (Fix (NamedSort name argSorts)) -> lispToConstr dts (Just (name,argSorts)) l+ _ -> error $ "smtlib2: Cannot translate "++show l++" to value" lispToConstr :: DataTypeInfo -> Maybe (String,[Sort]) -> L.Lisp -> Maybe Value lispToConstr dts sort (L.List [L.Symbol "as",@@ -1589,7 +1644,7 @@ withPipe :: MonadIO m => String -> [String] -> SMT' m a -> m a withPipe prog args act = do pipe <- liftIO $ createSMTPipe prog args- withSMTBackend pipe act+ withSMTBackend' pipe True act tacticToLisp :: Tactic -> L.Lisp tacticToLisp Skip = L.Symbol "skip"
Language/SMTLib2/Strategy.hs view
@@ -2,8 +2,6 @@ import Language.SMTLib2.Internals.Operators -import Text.Show- data Tactic = Skip | AndThen [Tactic]
smtlib2.cabal view
@@ -1,5 +1,5 @@ Name: smtlib2-Version: 0.1+Version: 0.2 Author: Henning Günther <guenther@forsyte.at> Maintainer: guenther@forsyte.at Synopsis: A type-safe interface to communicate with an SMT solver.@@ -23,12 +23,13 @@ Library Build-Depends: base >= 4 && < 5,text,mtl,process,blaze-builder,bytestring,- attoparsec,atto-lisp >= 0.2,array,+ attoparsec,atto-lisp >= 0.2 && < 0.3,array, containers, transformers, data-fix, tagged Extensions: GADTs,RankNTypes,CPP,ScopedTypeVariables, MultiParamTypeClasses,FlexibleContexts,OverloadedStrings, DeriveFunctor,FlexibleInstances,DeriveTraversable,DeriveFoldable, DeriveDataTypeable+ GHC-Options: -fcontext-stack=100 if flag(WithConstraints) Build-Depends: constraints CPP-Options: -DSMTLIB2_WITH_CONSTRAINTS