Handle quantifiedbool local functions better

Data/SBV/Core/Symbolic.hs

@@ -12,9 +12,11 @@
 {-# LANGUAGE BangPatterns               #-}
 {-# LANGUAGE CPP                        #-}
 {-# LANGUAGE DefaultSignatures          #-}
+{-# LANGUAGE DeriveAnyClass             #-}
 {-# LANGUAGE DeriveDataTypeable         #-}
 {-# LANGUAGE DeriveFunctor              #-}
 {-# LANGUAGE DeriveGeneric              #-}
+{-# LANGUAGE DerivingStrategies         #-}
 {-# LANGUAGE FlexibleInstances          #-}
 {-# LANGUAGE GADTs                      #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
@@ -235,7 +237,7 @@ data Op = Plus
         | ArrRead ArrayIndex
         | KindCast Kind Kind
         | Uninterpreted String
-        | QuantifiedBool String                 -- When we generate a forall/exists (nested etc.) boolean value
+        | QuantifiedBool [Op] String            -- When we generate a forall/exists (nested etc.) boolean value
         | SpecialRelOp Kind SpecialRelOp        -- Generate the equality to the internal operation
         | Label String                          -- Essentially no-op; useful for code generation to emit comments.
         | IEEEFP FPOp                           -- Floating-point ops, categorized separately
@@ -255,7 +257,7 @@ data Op = Plus
         | MaybeConstructor Kind Bool            -- Construct a maybe value; False: Nothing, True: Just
         | MaybeIs Kind Bool                     -- Maybe tester; False: nothing, True: just
         | MaybeAccess                           -- Maybe branch access; grab the contents of the just
-        deriving (Eq, Ord, G.Data)
+        deriving (Eq, Ord, Generic, G.Data, NFData)
 
 -- | Special relations supported by z3
 data SpecialRelOp = IsPartialOrder         String
@@ -293,7 +295,7 @@ data FPOp = FP_Cast        Kind Kind SV   -- From-Kind, To-Kind, RoundingMode. T
           | FP_IsNaN
           | FP_IsNegative
           | FP_IsPositive
-          deriving (Eq, Ord, G.Data)
+          deriving (Eq, Ord, G.Data, NFData, Generic)
 
 -- Note that the show instance maps to the SMTLib names. We need to make sure
 -- this mapping stays correct through SMTLib changes. The only exception
@@ -340,7 +342,7 @@ data NROp = NR_Sin
           | NR_Exp
           | NR_Log
           | NR_Pow
-          deriving (Eq, Ord, G.Data)
+          deriving (Eq, Ord, G.Data, NFData, Generic)
 
 -- | The show instance carefully arranges for these to be printed as it can be understood by dreal
 instance Show NROp where
@@ -365,15 +367,15 @@ data PBOp = PB_AtMost  Int        -- ^ At most k
           | PB_Le      [Int] Int  -- ^ At most k,  with coefficients given. Generalizes PB_AtMost
           | PB_Ge      [Int] Int  -- ^ At least k, with coefficients given. Generalizes PB_AtLeast
           | PB_Eq      [Int] Int  -- ^ Exactly k,  with coefficients given. Generalized PB_Exactly
-          deriving (Eq, Ord, Show, G.Data)
+          deriving (Eq, Ord, Show, G.Data, NFData, Generic)
 
 -- | Overflow operations
 data OvOp = PlusOv Bool           -- ^ Addition    overflow.    Bool is True if signed.
           | SubOv  Bool           -- ^ Subtraction overflow.    Bool is True if signed.
           | MulOv  Bool           -- ^ Multiplication overflow. Bool is True if signed.
           | DivOv                 -- ^ Division overflow.       Only signed, since unsigned division does not overflow.
           | NegOv                 -- ^ Unary negation overflow. Only signed, since unsigned negation does not overflow.
-          deriving (Eq, Ord, G.Data)
+          deriving (Eq, Ord, G.Data, NFData, Generic)
 
 -- | Show instance. It's important that these follow the SMTLib names.
 instance Show OvOp where
@@ -399,12 +401,12 @@ data StrOp = StrConcat       -- ^ Concatenation of one or more strings
            | StrToCode       -- ^ Equivalent to Haskell's ord
            | StrFromCode     -- ^ Equivalent to Haskell's chr
            | StrInRe RegExp  -- ^ Check if string is in the regular expression
-           deriving (Eq, Ord, G.Data)
+           deriving (Eq, Ord, G.Data, NFData, Generic)
 
 -- | Regular-expression operators. The only thing we can do is to compare for equality/disequality.
 data RegExOp = RegExEq  RegExp RegExp
              | RegExNEq RegExp RegExp
-             deriving (Eq, Ord, G.Data)
+             deriving (Eq, Ord, G.Data, NFData, Generic)
 
 -- | Regular expressions. Note that regular expressions themselves are
 -- concrete, but the 'Data.SBV.RegExp.match' function from the 'Data.SBV.RegExp.RegExpMatchable' class
@@ -428,7 +430,7 @@ data RegExp = Literal String       -- ^ Precisely match the given string
             | Power Int     RegExp -- ^ Exactly @n@ repetitions, i.e., nth power
             | Union [RegExp]       -- ^ Union of regular expressions
             | Inter RegExp RegExp  -- ^ Intersection of regular expressions
-            deriving (Eq, Ord, G.Data)
+            deriving (Eq, Ord, G.Data, Generic, NFData)
 
 -- | With overloaded strings, we can have direct literal regular expressions.
 instance IsString RegExp where
@@ -535,7 +537,7 @@ data SeqOp = SeqConcat            -- ^ See StrConcat
            | SeqFoldLeft  String  -- ^ Folding of sequences
            | SeqFoldLeftI String  -- ^ Folding of sequences with offset
            | SBVReverse Kind      -- ^ Reversal of sequences. NB. Also works for strings; hence the name.
-  deriving (Eq, Ord, G.Data)
+  deriving (Eq, Ord, G.Data, NFData, Generic)
 
 -- | Show instance for SeqOp. Again, mapping is important.
 instance Show SeqOp where
@@ -570,7 +572,7 @@ data SetOp = SetEqual
            | SetSubset
            | SetDifference
            | SetComplement
-        deriving (Eq, Ord, G.Data)
+        deriving (Eq, Ord, G.Data, NFData, Generic)
 
 -- The show instance for 'SetOp' is merely for debugging, we map them separately so
 -- the mapped strings are less important here.
@@ -605,7 +607,7 @@ instance Show Op where
 
   show (KindCast fr to)     = "cast_" ++ show fr ++ "_" ++ show to
   show (Uninterpreted i)    = "[uninterpreted] " ++ i
-  show (QuantifiedBool i)   = "[quantified boolean] " ++ i
+  show (QuantifiedBool _ i) = "[quantified boolean] " ++ i
 
   show (Label s)            = "[label] " ++ s
 
@@ -806,7 +808,7 @@ instance (MonadQuery m, Monoid w) => MonadQuery (LW.WriterT w m)
 -- | A query is a user-guided mechanism to directly communicate and extract
 -- results from the solver. A generalization of 'Data.SBV.Query'.
 newtype QueryT m a = QueryT { runQueryT :: ReaderT State m a }
-    deriving (Applicative, Functor, Monad, MonadIO, MonadTrans,
+    deriving newtype (Applicative, Functor, Monad, MonadIO, MonadTrans,
               MonadError e, MonadState s, MonadWriter w)
 
 instance Monad m => MonadQuery (QueryT m) where
@@ -1197,19 +1199,21 @@ lookupInput f sv ns
 data SMTDef = SMTDef String           -- ^ Defined functions -- name
                      Kind             -- ^ Final kind of the definition (resulting kind, not the params)
                      [String]         -- ^ other definitions it refers to
+                     [Op]             -- ^ ops used in it, in case we need to generate extra defs
                      (Maybe String)   -- ^ parameter string
                      (Int -> String)  -- ^ Body, in SMTLib syntax, given the tab amount
             | SMTLam Kind             -- ^ Final kind of the definition (resulting kind, not the params)
                      [String]         -- ^ Anonymous function -- other definitions it refers to
+                     [Op]             -- ^ ops used in it, in case we need to generate extra defs
                      (Maybe String)   -- ^ parameter string
                      (Int -> String)  -- ^ Body, in SMTLib syntax, given the tab amount
             deriving G.Data
 
 -- | For debug purposes
 instance Show SMTDef where
   show d = case d of
-             SMTDef nm fk frees p body -> shDef (Just nm) fk frees p body
-             SMTLam    fk frees p body -> shDef Nothing   fk frees p body
+             SMTDef nm fk frees _ p body -> shDef (Just nm) fk frees p body
+             SMTLam    fk frees _ p body -> shDef Nothing   fk frees p body
     where shDef mbNm fk frees p body = unlines [ "-- User defined function: " ++ fromMaybe "Anonymous" mbNm
                                                , "-- Final return type    : " ++ show fk
                                                , "-- Refers to            : " ++ intercalate ", " frees
@@ -1220,13 +1224,13 @@ instance Show SMTDef where
 
 -- The name of this definition
 smtDefGivenName :: SMTDef -> Maybe String
-smtDefGivenName (SMTDef n _ _ _ _) = Just n
-smtDefGivenName SMTLam{}           = Nothing
+smtDefGivenName (SMTDef n _ _ _ _ _) = Just n
+smtDefGivenName SMTLam{}             = Nothing
 
 -- | NFData instance for SMTDef
 instance NFData SMTDef where
-  rnf (SMTDef n fk frees params body) = rnf n `seq` rnf fk `seq` rnf frees `seq` rnf params `seq` rnf body
-  rnf (SMTLam   fk frees params body) =             rnf fk `seq` rnf frees `seq` rnf params `seq` rnf body
+  rnf (SMTDef n fk frees ops params body) = rnf n `seq` rnf fk `seq` rnf frees `seq` rnf ops `seq` rnf params `seq` rnf body
+  rnf (SMTLam   fk frees ops params body) =             rnf fk `seq` rnf frees `seq` rnf ops `seq` rnf params `seq` rnf body
 
 -- | The state of the symbolic interpreter
 data State  = State { sbvContext          :: SBVContext
@@ -1667,7 +1671,7 @@ instance (MonadSymbolic m, Monoid w) => MonadSymbolic (LW.WriterT w m)
 
 -- | A generalization of 'Data.SBV.Symbolic'.
 newtype SymbolicT m a = SymbolicT { runSymbolicT :: ReaderT State m a }
-                   deriving ( Applicative, Functor, Monad, MonadIO, MonadTrans
+                   deriving newtype ( Applicative, Functor, Monad, MonadIO, MonadTrans
                             , MonadError e, MonadState s, MonadWriter w
 #if MIN_VERSION_base(4,11,0)
                             , Fail.MonadFail
@@ -2154,7 +2158,7 @@ uncache = uncacheGen rSVCache
 data ArrayIndex = ArrayIndex { unArrayIndex   :: Int
                              , unArrayContext :: SBVContext
                              }
-               deriving (Eq, Ord, G.Data)
+               deriving (Eq, Ord, G.Data, NFData, Generic)
 
 -- | We simply show indexes as the underlying integer
 instance Show ArrayIndex where

Data/SBV/Lambda.hs

@@ -25,6 +25,7 @@ module Data.SBV.Lambda (
           , constraint,  constraintStr
         ) where
 
+
 import Control.Monad       (join)
 import Control.Monad.Trans (liftIO, MonadIO)
 
@@ -39,13 +40,13 @@ import qualified Data.SBV.Core.Symbolic as     S (mkNewState)
 import Data.IORef (readIORef, modifyIORef')
 import Data.List
 
-import qualified Data.Foldable      as F
-import qualified Data.Map.Strict    as M
+import qualified Data.Foldable as F
 
 import qualified Data.Generics.Uniplate.Data as G
 
 data Defn = Defn [String]                        -- The uninterpreted names referred to in the body
                  (Maybe [(Quantifier, String)])  -- Param declaration groups, if any
+                 [Op]                            -- All ops used in the definition
                  (Int -> String)                 -- Body, given the tab amount.
 
 -- | Maka a new substate from the incoming state, sharing parts as necessary
@@ -132,13 +133,13 @@ lambdaGen trans inState fk f = inSubState inState $ \st -> trans <$> convert st
 -- | Create an SMTLib lambda, in the given state.
 lambda :: (MonadIO m, Lambda (SymbolicT m) a) => State -> Kind -> a -> m SMTDef
 lambda inState fk = lambdaGen mkLam inState fk
-   where mkLam (Defn frees params body) = SMTLam fk frees (extractAllUniversals <$> params) body
+   where mkLam (Defn frees params ops body) = SMTLam fk frees ops (extractAllUniversals <$> params) body
 
 -- | Create an anonymous lambda, rendered as n SMTLib string
 lambdaStr :: (MonadIO m, Lambda (SymbolicT m) a) => State -> Kind -> a -> m String
 lambdaStr = lambdaGen mkLam
-   where mkLam (Defn _frees Nothing       body) = body 0
-         mkLam (Defn _frees (Just params) body) = "(lambda " ++ extractAllUniversals params ++ "\n" ++ body 2 ++ ")"
+   where mkLam (Defn _frees Nothing       _ops body) = body 0
+         mkLam (Defn _frees (Just params) _ops body) = "(lambda " ++ extractAllUniversals params ++ "\n" ++ body 2 ++ ")"
 
 -- | Generaic creator for named functions,
 namedLambdaGen :: (MonadIO m, Lambda (SymbolicT m) a) => (Defn -> b) -> State -> Kind -> a -> m b
@@ -147,26 +148,26 @@ namedLambdaGen trans inState fk f = inSubState inState $ \st -> trans <$> conver
 -- | Create a named SMTLib function, in the given state.
 namedLambda :: (MonadIO m, Lambda (SymbolicT m) a) => State -> String -> Kind -> a -> m SMTDef
 namedLambda inState nm fk = namedLambdaGen mkDef inState fk
-   where mkDef (Defn frees params body) = SMTDef nm fk frees (extractAllUniversals <$> params) body
+   where mkDef (Defn frees params ops body) = SMTDef nm fk frees ops (extractAllUniversals <$> params) body
 
 -- | Create a named SMTLib function, in the given state, string version
 namedLambdaStr :: (MonadIO m, Lambda (SymbolicT m) a) => State -> String -> SBVType -> a -> m String
 namedLambdaStr inState nm t = namedLambdaGen mkDef inState fk
-   where mkDef (Defn frees params body) = concat $ declUserFuns [(SMTDef nm fk frees (extractAllUniversals <$> params) body, t)]
+   where mkDef (Defn frees params ops body) = concat $ declUserFuns [(SMTDef nm fk frees ops (extractAllUniversals <$> params) body, t)]
          fk = case t of
                 SBVType [] -> error $ "namedLambdaStr: Invalid type for " ++ show nm ++ ", empty!"
                 SBVType xs -> last xs
 
 -- | Generic constraint generator.
-constraintGen :: (MonadIO m, Constraint (SymbolicT m) a) => ([String] -> (Int -> String) -> b) -> State -> a -> m b
+constraintGen :: (MonadIO m, Constraint (SymbolicT m) a) => ([String] -> [Op] -> (Int -> String) -> b) -> State -> a -> m b
 constraintGen trans inState@State{rProgInfo} f = do
    -- indicate we have quantifiers
    liftIO $ modifyIORef' rProgInfo (\u -> u{hasQuants = True})
 
-   let mkDef (Defn deps Nothing       body) = trans deps body
-       mkDef (Defn deps (Just params) body) = trans deps $ \i -> unwords (map mkGroup params) ++ "\n"
-                                                              ++ body (i + 2)
-                                                              ++ replicate (length params) ')'
+   let mkDef (Defn deps Nothing       ops body) = trans deps ops body
+       mkDef (Defn deps (Just params) ops body) = trans deps ops $ \i -> unwords (map mkGroup params) ++ "\n"
+                                                                      ++ body (i + 2)
+                                                                      ++ replicate (length params) ')'
        mkGroup (ALL, s) = "(forall " ++ s
        mkGroup (EX,  s) = "(exists " ++ s
 
@@ -180,14 +181,14 @@ instance Constraint Symbolic a => QuantifiedBool a where
 -- | Generate a constraint.
 constraint :: (MonadIO m, Constraint (SymbolicT m) a) => State -> a -> m SV
 constraint st = join . constraintGen mkSV st
-   where mkSV _deps d = liftIO $ newExpr st KBool (SBVApp (QuantifiedBool (d 0)) [])
+   where mkSV _deps ops d = liftIO $ newExpr st KBool (SBVApp (QuantifiedBool ops (d 0)) [])
 
 -- | Generate a constraint, string version
 constraintStr :: (MonadIO m, Constraint (SymbolicT m) a) => State -> a -> m String
 constraintStr = constraintGen toStr
-   where toStr deps body = intercalate "\n" [ "; user defined axiom: " ++ depInfo deps
-                                            , "(assert " ++ body 2 ++ ")"
-                                            ]
+   where toStr deps _ body = intercalate "\n" [ "; user defined axiom: " ++ depInfo deps
+                                              , "(assert " ++ body 2 ++ ")"
+                                              ]
 
          depInfo [] = ""
          depInfo ds = "[Refers to: " ++ intercalate ", " ds ++ "]"
@@ -263,6 +264,7 @@ toLambda curProgInfo cfg expectedKind result@Result{resAsgns = SBVPgm asgnsSeq}
          = res
          where res = Defn (nub [nm | Uninterpreted nm <- G.universeBi asgnsSeq])
                           mbParam
+                          (nub (sort (G.universeBi asgnsSeq)))
                           (intercalate "\n" . body)
 
                params = case is of
@@ -366,8 +368,7 @@ toLambda curProgInfo cfg expectedKind result@Result{resAsgns = SBVPgm asgnsSeq}
                                            ++ ")"
 
                mkAsgn (sv, e) = (sv, converter e)
-               converter = cvtExp curProgInfo solverCaps rm tableMap funcMap
+               converter = cvtExp curProgInfo solverCaps rm tableMap
                  where solverCaps = capabilities (solver cfg)
-                       funcMap    = M.empty
 
 {- HLint ignore module "Use second" -}

Data/SBV/Provers/Prover.hs

@@ -505,7 +505,7 @@ validate reducer isSAT cfg p res =
                                                 Nothing            -> Nothing
                                                 Just (SBVApp o as) -> case o of
                                                                         Uninterpreted v  -> Just $ "The value depends on the uninterpreted constant " ++ show v ++ "."
-                                                                        QuantifiedBool _ -> Just "The value depends on a quantified variable."
+                                                                        QuantifiedBool{} -> Just "The value depends on a quantified variable."
                                                                         IEEEFP FP_FMA    -> Just "Floating point FMA operation is not supported concretely."
                                                                         IEEEFP _         -> Just "Not all floating point operations are supported concretely."
                                                                         OverflowOp _     -> Just "Overflow-checking is not done concretely."