Merge pull request #19 from bruderj15/quantifiers

Quantifiers

README.md

@@ -65,10 +65,11 @@ May print: `(Sat,Just (V3 (-2.0) (-1.0) 0.0,V3 (-2.0) (-1.0) 0.0))`
 - [x] Solvers via external process: CVC5, Z3, Yices2-SMT & MathSAT
 - [x] Add your own solvers via the [Solver type](https://github.com/bruderj15/Hasmtlib/blob/master/src/Language/Hasmtlib/Type/Solver.hs)
 - [x] Incremental solving
+- [x] Quantifiers `for_all` and `exists`
 
 ### Coming
 - [ ] Observable sharing
-- [ ] Quantifiers `for_all` and `exists`
+- [ ] (Maybe) signed BitVec with corresponding encoding on the type-level (unsigned, ones-complement, twos-complement)
 
 ## Examples
 There are some examples in [here](https://github.com/bruderj15/Hasmtlib/tree/master/src/Language/Hasmtlib/Example).

hasmtlib.cabal

@@ -38,10 +38,12 @@ library
                      , Language.Hasmtlib.Solver.Yices
                      , Language.Hasmtlib.Solver.Z3
                      , Language.Hasmtlib.Type.Expr
+                     , Language.Hasmtlib.Type.MonadSMT
                      , Language.Hasmtlib.Type.SMT
                      , Language.Hasmtlib.Type.Pipe
                      , Language.Hasmtlib.Type.Solution
                      , Language.Hasmtlib.Type.Solver
+                     , Language.Hasmtlib.Type.Option
 
   other-modules:       Language.Hasmtlib.Internal.Expr
                      , Language.Hasmtlib.Internal.Expr.Num

src/Language/Hasmtlib.hs

@@ -1,9 +1,11 @@
 module Language.Hasmtlib
   (
-    module Language.Hasmtlib.Type.SMT
+    module Language.Hasmtlib.Type.MonadSMT
+  , module Language.Hasmtlib.Type.SMT
   , module Language.Hasmtlib.Type.Pipe
   , module Language.Hasmtlib.Type.Expr
   , module Language.Hasmtlib.Type.Solver
+  , module Language.Hasmtlib.Type.Option
   , module Language.Hasmtlib.Type.Solution
   , module Language.Hasmtlib.Integraled
   , module Language.Hasmtlib.Iteable
@@ -19,10 +21,12 @@ module Language.Hasmtlib
   )
   where
 
+import Language.Hasmtlib.Type.MonadSMT
 import Language.Hasmtlib.Type.SMT
 import Language.Hasmtlib.Type.Pipe
 import Language.Hasmtlib.Type.Expr
 import Language.Hasmtlib.Type.Solver
+import Language.Hasmtlib.Type.Option
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Integraled
 import Language.Hasmtlib.Iteable

src/Language/Hasmtlib/Codec.hs

@@ -113,6 +113,8 @@ instance KnownSMTRepr t => Codec (Expr t) where
   decode sol (BvuLTHE x y)      = liftA2 (<=) (decode sol x) (decode sol y)
   decode sol (BvuGTHE x y)      = liftA2 (>=) (decode sol x) (decode sol y)
   decode sol (BvuGT x y)        = liftA2 (>) (decode sol x) (decode sol y)
+  decode _ (ForAll _ _)       = Nothing
+  decode _ (Exists _ _)       = Nothing
   encode = Constant . putValue
 
 instance Codec () where

src/Language/Hasmtlib/Example/Quantifier.hs

@@ -0,0 +1,22 @@
+module Language.Hasmtlib.Example.Quantifier where
+
+import Prelude hiding (mod, (&&), (||))
+import Language.Hasmtlib
+
+main :: IO ()
+main = do
+  res <- solveWith cvc5Debug $ do
+    setLogic "BV"
+
+    z <- var @(BvType 8)
+
+    assert $ z === 0
+
+    assert $
+      for_all $ \x ->
+          exists $ \y ->
+            x - y === z
+
+    return ()
+
+  print res

src/Language/Hasmtlib/Internal/Expr.hs

@@ -13,7 +13,7 @@ import Data.Proxy
 import Data.Coerce
 import Data.ByteString.Builder
 import Control.Lens
-import GHC.TypeNats
+import GHC.TypeLits
 
 -- | Types of variables in SMTLib - used as promoted Type
 data SMTType = IntType | RealType | BoolType | BvType Nat
@@ -150,7 +150,8 @@ data Expr (t :: SMTType) where
   BvuGTHE  :: KnownNat n => Expr (BvType n) -> Expr (BvType n) -> Expr BoolType
   BvuGT    :: KnownNat n => Expr (BvType n) -> Expr (BvType n) -> Expr BoolType
 
-deriving instance Show (Expr t)
+  ForAll   :: KnownSMTRepr t => Maybe (SMTVar t) -> (Expr t -> Expr BoolType) -> Expr BoolType
+  Exists   :: KnownSMTRepr t => Maybe (SMTVar t) -> (Expr t -> Expr BoolType) -> Expr BoolType
 
 instance Boolean (Expr BoolType) where
   bool = Constant . BoolValue
@@ -260,3 +261,16 @@ instance KnownSMTRepr t => RenderSMTLib2 (Expr t) where
   renderSMTLib2 (BvuLTHE x y)      = renderBinary "bvule"  (renderSMTLib2 x) (renderSMTLib2 y)
   renderSMTLib2 (BvuGTHE x y)      = renderBinary "bvuge"  (renderSMTLib2 x) (renderSMTLib2 y)
   renderSMTLib2 (BvuGT x y)        = renderBinary "bvugt"  (renderSMTLib2 x) (renderSMTLib2 y)
+
+  renderSMTLib2 (ForAll mQvar f) = renderQuantifier "forall" mQvar f
+  renderSMTLib2 (Exists mQvar f) = renderQuantifier "exists" mQvar f
+
+renderQuantifier :: forall t. KnownSMTRepr t => Builder -> Maybe (SMTVar t) -> (Expr t -> Expr BoolType) -> Builder
+renderQuantifier qname (Just qvar) f =
+  renderBinary
+    qname
+    ("(" <> renderUnary (renderSMTLib2 qvar) (singRepr @t) <> ")")
+    expr
+  where
+    expr = renderSMTLib2 $ f $ Var qvar
+renderQuantifier _ Nothing _ = mempty

src/Language/Hasmtlib/Type/Expr.hs

@@ -1,13 +1,45 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
 module Language.Hasmtlib.Type.Expr
  ( SMTType(..)
  , SMTVar(..)
  , ValueType
  , Value(..), extractValue, putValue
  , Repr(..), KnownSMTRepr(..), SomeKnownSMTRepr(..)
  , Expr
+ , for_all , exists
  , module Language.Hasmtlib.Internal.Expr.Num
  )
 where
 
 import Language.Hasmtlib.Internal.Expr
 import Language.Hasmtlib.Internal.Expr.Num
+
+-- | A universal quantification for any specific type
+--   If the type cannot be inferred, apply a type-annotation.
+--   Nested quantifiers are also supported.
+-- 
+--   Usage:
+--   assert $
+--      for_all @IntType $ \x ->
+--         x + 0 === x && 0 + x === 0 
+--    
+--   The lambdas 'x' is all-quantified here.
+--   It will only be scoped for the lambdas body.
+for_all :: forall t. KnownSMTRepr t => (Expr t -> Expr BoolType) -> Expr BoolType
+for_all = ForAll Nothing
+
+-- | An existential quantification for any specific type
+--   If the type cannot be inferred, apply a type-annotation.
+--   Nested quantifiers are also supported.
+-- 
+--   Usage:
+--   assert $
+--      for_all @(BvType 8) $ \x ->
+--          exists $ \y ->
+--            x - y === 0 
+--    
+--   The lambdas 'y' is existentially quantified here.
+--   It will only be scoped for the lambdas body.
+exists :: forall t. KnownSMTRepr t => (Expr t -> Expr BoolType) -> Expr BoolType
+exists = Exists Nothing

src/Language/Hasmtlib/Type/MonadSMT.hs

@@ -0,0 +1,82 @@
+module Language.Hasmtlib.Type.MonadSMT where
+
+import Language.Hasmtlib.Internal.Expr
+import Language.Hasmtlib.Type.Option
+import Data.Proxy
+import Control.Monad
+import Control.Monad.State
+
+class MonadState s m => MonadSMT s m where
+  -- | Construct a variable.
+  --   Usage:
+  --      x :: SMTVar RealType <- smtvar' (Proxy @RealType)
+  smtvar'    :: forall t. KnownSMTRepr t => Proxy t -> m (SMTVar t)
+
+  -- | Construct a variable as expression.
+  --   Usage:
+  --      x :: Expr RealType <- var' (Proxy @RealType)
+  var'       :: forall t. KnownSMTRepr t => Proxy t -> m (Expr t)
+
+  -- | Assert a boolean expression.
+  --   Usage
+  --      x :: Expr IntType <- var @IntType
+  --      assert $ x + 5 === 42
+  assert    :: Expr BoolType -> m ()
+
+  -- | Set an SMT-Solver-Option.
+  setOption :: SMTOption -> m ()
+
+  -- | Set the logic for the SMT-Solver to use.
+  --   Usage:
+  --      setLogic "QF_LRA"
+  setLogic  :: String -> m ()
+
+-- | Wrapper for @var'@ which hides the Proxy
+var :: forall t s m. (KnownSMTRepr t, MonadSMT s m) => m (Expr t)
+var = var' (Proxy @t)
+{-# INLINE var #-}
+
+-- | Wrapper for @smtvar'@ which hides the Proxy
+smtvar :: forall t s m. (KnownSMTRepr t, MonadSMT s m) => m (SMTVar t)
+smtvar = smtvar' (Proxy @t)
+{-# INLINE smtvar #-}
+
+-- | Create a constant.
+--   Usage
+--      >>> constant True
+--          Constant (BoolValue True)
+--
+--      >>> let x :: Integer = 10 ; constant x
+--          Constant (IntValue 10)
+--
+--      >>> constant @IntType 5
+--          Constant (IntValue 5)
+--
+--      >>> constant @(BvType 8) 5
+--          Constant (BvValue 0000101)
+constant :: KnownSMTRepr t => ValueType t -> Expr t
+constant = Constant . putValue
+{-# INLINE constant #-}
+
+--   We need this separate so we get a pure API for quantifiers
+--   Ideally we would do that when rendering the expression
+--   However renderSMTLib2 is pure but we need a new quantified var which is stateful
+-- | Assign quantified variables to all quantified subexpressions of an expression
+--   This shall only be used internally.
+--   Usually before rendering an assert.
+quantify :: MonadSMT s m => Expr t -> m (Expr t)
+quantify (Not x)      = fmap   Not  (quantify x)
+quantify (And x y)    = liftM2 And  (quantify x) (quantify y)
+quantify (Or x y)     = liftM2 Or   (quantify x) (quantify y)
+quantify (Impl x y)   = liftM2 Impl (quantify x) (quantify y)
+quantify (Xor x y)    = liftM2 Xor  (quantify x) (quantify y)
+quantify (Ite p t f)  = liftM3 Ite  (quantify p) (quantify t) (quantify f)
+quantify (ForAll _ f) = do
+  qVar <- smtvar
+  qBody <- quantify $ f $ Var qVar
+  return $ ForAll (Just qVar) (const qBody)
+quantify (Exists _ f) = do
+  qVar <- smtvar
+  qBody <- quantify $ f $ Var qVar
+  return $ Exists (Just qVar) (const qBody)
+quantify expr = return expr

src/Language/Hasmtlib/Type/Option.hs

@@ -0,0 +1,16 @@
+module Language.Hasmtlib.Type.Option where
+
+import Language.Hasmtlib.Internal.Render
+import Data.Data (Data)
+import Data.ByteString.Builder
+
+data SMTOption =
+    PrintSuccess  Bool              -- | Print \"success\" after each operation
+  | ProduceModels Bool              -- | Produce a satisfying assignment after each successful checkSat
+  | Incremental   Bool              -- | Incremental solving
+  deriving (Show, Eq, Ord, Data)
+
+instance RenderSMTLib2 SMTOption where
+  renderSMTLib2 (PrintSuccess  b) = renderBinary "set-option" (":print-success"  :: Builder) b
+  renderSMTLib2 (ProduceModels b) = renderBinary "set-option" (":produce-models" :: Builder) b
+  renderSMTLib2 (Incremental   b) = renderBinary "set-option" (":incremental"    :: Builder) b

src/Language/Hasmtlib/Type/Pipe.hs

@@ -3,23 +3,24 @@
 
 module Language.Hasmtlib.Type.Pipe
  ( Pipe, withSolver
- , MonadSMT(..)
  , push, pop
  , solve, checkSat, getModel, getValue
  )
  where
 
 import Language.Hasmtlib.Type.SMT
+import Language.Hasmtlib.Type.MonadSMT
 import Language.Hasmtlib.Internal.Expr
 import Language.Hasmtlib.Internal.Render
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Codec
 import Language.Hasmtlib.Internal.Parser hiding (var, constant)
 import qualified SMTLIB.Backends as B
+import Data.List (isPrefixOf)
 import Data.IntMap (singleton)
 import Data.Coerce
 import Data.ByteString.Builder
-import Data.ByteString.Lazy hiding (filter, singleton)
+import Data.ByteString.Lazy hiding (filter, singleton, isPrefixOf)
 import Data.Attoparsec.ByteString hiding (Result)
 import Control.Monad
 import Control.Monad.State
@@ -28,31 +29,41 @@ import Control.Lens hiding (List)
 -- | Pipe to the solver.
 -- | If @B.Solver@ is @B.Queuing@ then all commands but those that expect an answer are sent to the queue.
 data Pipe = Pipe
-  { _lastPipeVarId :: {-# UNPACK #-} !Int
-  , _pipe          :: !B.Solver
+  { _lastPipeVarId :: {-# UNPACK #-} !Int              -- | Last Id assigned to a new var
+  , _mPipeLogic    :: Maybe String                     -- | Logic for the SMT-Solver
+  , _pipe          :: !B.Solver                        -- | Active pipe to the backend
   }
 
 $(makeLenses ''Pipe)
 
 withSolver :: B.Solver -> Pipe
-withSolver = Pipe 0
+withSolver = Pipe 0 Nothing
 
 instance (MonadState Pipe m, MonadIO m) => MonadSMT Pipe m where
-  var' _ = do
+  smtvar' _ = fmap coerce $ lastPipeVarId <+= 1
+  {-# INLINE smtvar' #-}
+
+  var' p = do
     smt <- get
-    newVar <- fmap coerce $ lastPipeVarId <+= 1 
+    newVar <- smtvar' p
     liftIO $ B.command_ (smt^.pipe) $ renderDeclareVar newVar
     return $ Var newVar
+  {-# INLINEABLE var' #-}
 
   assert expr = do
     smt <- get
-    liftIO $ B.command_ (smt^.pipe) $ renderAssert expr
+    qExpr <- case smt^.mPipeLogic of
+      Nothing    -> return expr
+      Just logic -> if "QF" `isPrefixOf` logic then return expr else quantify expr
+    liftIO $ B.command_ (smt^.pipe) $ renderAssert qExpr
+  {-# INLINEABLE assert #-}
 
   setOption opt = do
     smt <- get
     liftIO $ B.command_ (smt^.pipe) $ renderSMTLib2 opt
 
   setLogic l = do
+    mPipeLogic ?= l
     smt <- get
     liftIO $ B.command_ (smt^.pipe) $ renderSetLogic (stringUtf8 l)