-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Core.Symbolic
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Symbolic values
-----------------------------------------------------------------------------

{-# LANGUAGE CPP                        #-}
{-# LANGUAGE DefaultSignatures          #-}
{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE DeriveFunctor              #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE FunctionalDependencies     #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NamedFieldPuns             #-}
{-# LANGUAGE PatternGuards              #-}
{-# LANGUAGE Rank2Types                 #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE TupleSections              #-}
{-# LANGUAGE TypeOperators              #-}
{-# LANGUAGE UndecidableInstances       #-} -- for undetermined s in MonadState

{-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}

module Data.SBV.Core.Symbolic
  ( NodeId(..)
  , SV(..), swKind, trueSV, falseSV
  , Op(..), PBOp(..), OvOp(..), FPOp(..), StrOp(..), SeqOp(..), SetOp(..), RegExp(..)
  , Quantifier(..), needsExistentials
  , RoundingMode(..)
  , SBVType(..), svUninterpreted, newUninterpreted, addAxiom
  , SVal(..)
  , svMkSymVar, sWordN, sWordN_, sIntN, sIntN_
  , ArrayContext(..), ArrayInfo
  , svToSV, svToSymSV, forceSVArg
  , SBVExpr(..), newExpr, isCodeGenMode, isSafetyCheckingIStage, isRunIStage, isSetupIStage
  , Cached, cache, uncache, modifyState, modifyIncState
  , ArrayIndex(..), FArrayIndex(..), uncacheAI, uncacheFAI
  , NamedSymVar
  , getSValPathCondition, extendSValPathCondition
  , getTableIndex
  , SBVPgm(..), MonadSymbolic(..), SymbolicT, Symbolic, runSymbolic, State(..), withNewIncState, IncState(..), incrementInternalCounter
  , inSMTMode, SBVRunMode(..), IStage(..), Result(..)
  , registerKind, registerLabel, recordObservable
  , addAssertion, addNewSMTOption, imposeConstraint, internalConstraint, internalVariable
  , SMTLibPgm(..), SMTLibVersion(..), smtLibVersionExtension
  , SolverCapabilities(..)
  , extractSymbolicSimulationState
  , OptimizeStyle(..), Objective(..), Penalty(..), objectiveName, addSValOptGoal
  , MonadQuery(..), QueryT(..), Query, Queriable(..), Fresh(..), QueryState(..), QueryContext(..)
  , SMTScript(..), Solver(..), SMTSolver(..), SMTResult(..), SMTModel(..), SMTConfig(..), SMTEngine
  , validationRequested, outputSVal
  ) where

import Control.Arrow               (first, second, (***))
import Control.DeepSeq             (NFData(..))
import Control.Monad               (when)
import Control.Monad.Except        (MonadError, ExceptT)
import Control.Monad.Reader        (MonadReader(..), ReaderT, runReaderT,
                                    mapReaderT)
import Control.Monad.State.Lazy    (MonadState)
import Control.Monad.Trans         (MonadIO(liftIO), MonadTrans(lift))
import Control.Monad.Trans.Maybe   (MaybeT)
import Control.Monad.Writer.Strict (MonadWriter)
import Data.Char                   (isAlpha, isAlphaNum, toLower)
import Data.IORef                  (IORef, newIORef, readIORef)
import Data.List                   (intercalate, sortBy)
import Data.Maybe                  (isJust, fromJust, fromMaybe)
import Data.String                 (IsString(fromString))

import Data.Time (getCurrentTime, UTCTime)

import GHC.Stack

import qualified Control.Monad.State.Lazy    as LS
import qualified Control.Monad.State.Strict  as SS
import qualified Control.Monad.Writer.Lazy   as LW
import qualified Control.Monad.Writer.Strict as SW
import qualified Data.IORef                  as R    (modifyIORef')
import qualified Data.Generics               as G    (Data(..))
import qualified Data.IntMap.Strict          as IMap (IntMap, empty, toAscList, lookup, insertWith)
import qualified Data.Map.Strict             as Map  (Map, empty, toList, lookup, insert, size)
import qualified Data.Set                    as Set  (Set, empty, toList, insert, member)
import qualified Data.Foldable               as F    (toList)
import qualified Data.Sequence               as S    (Seq, empty, (|>))

import System.Mem.StableName

import Data.SBV.Core.Kind
import Data.SBV.Core.Concrete
import Data.SBV.SMT.SMTLibNames
import Data.SBV.Utils.TDiff (Timing)
import Data.SBV.Utils.Lib   (stringToQFS)

import Data.SBV.Control.Types

#if MIN_VERSION_base(4,11,0)
import Control.Monad.Fail as Fail
#endif

-- | A symbolic node id
newtype NodeId = NodeId Int deriving (NodeId -> NodeId -> Bool
(NodeId -> NodeId -> Bool)
-> (NodeId -> NodeId -> Bool) -> Eq NodeId
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NodeId -> NodeId -> Bool
$c/= :: NodeId -> NodeId -> Bool
== :: NodeId -> NodeId -> Bool
$c== :: NodeId -> NodeId -> Bool
Eq, Eq NodeId
Eq NodeId =>
(NodeId -> NodeId -> Ordering)
-> (NodeId -> NodeId -> Bool)
-> (NodeId -> NodeId -> Bool)
-> (NodeId -> NodeId -> Bool)
-> (NodeId -> NodeId -> Bool)
-> (NodeId -> NodeId -> NodeId)
-> (NodeId -> NodeId -> NodeId)
-> Ord NodeId
NodeId -> NodeId -> Bool
NodeId -> NodeId -> Ordering
NodeId -> NodeId -> NodeId
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: NodeId -> NodeId -> NodeId
$cmin :: NodeId -> NodeId -> NodeId
max :: NodeId -> NodeId -> NodeId
$cmax :: NodeId -> NodeId -> NodeId
>= :: NodeId -> NodeId -> Bool
$c>= :: NodeId -> NodeId -> Bool
> :: NodeId -> NodeId -> Bool
$c> :: NodeId -> NodeId -> Bool
<= :: NodeId -> NodeId -> Bool
$c<= :: NodeId -> NodeId -> Bool
< :: NodeId -> NodeId -> Bool
$c< :: NodeId -> NodeId -> Bool
compare :: NodeId -> NodeId -> Ordering
$ccompare :: NodeId -> NodeId -> Ordering
$cp1Ord :: Eq NodeId
Ord)

-- | A symbolic word, tracking it's signedness and size.
data SV = SV !Kind !NodeId

-- | For equality, we merely use the node-id
instance Eq SV where
  SV _ n1 :: NodeId
n1 == :: SV -> SV -> Bool
== SV _ n2 :: NodeId
n2 = NodeId
n1 NodeId -> NodeId -> Bool
forall a. Eq a => a -> a -> Bool
== NodeId
n2

-- | Again, simply use the node-id for ordering
instance Ord SV where
  SV _ n1 :: NodeId
n1 compare :: SV -> SV -> Ordering
`compare` SV _ n2 :: NodeId
n2 = NodeId
n1 NodeId -> NodeId -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` NodeId
n2

instance HasKind SV where
  kindOf :: SV -> Kind
kindOf (SV k :: Kind
k _) = Kind
k

instance Show SV where
  show :: SV -> String
show (SV _ (NodeId n :: Int
n)) = case Int
n of
                             -2 -> "false"
                             -1 -> "true"
                             _  -> 's' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
n

-- | Kind of a symbolic word.
swKind :: SV -> Kind
swKind :: SV -> Kind
swKind (SV k :: Kind
k _) = Kind
k

-- | Forcing an argument; this is a necessary evil to make sure all the arguments
-- to an uninterpreted function are evaluated before called; the semantics of uinterpreted
-- functions is necessarily strict; deviating from Haskell's
forceSVArg :: SV -> IO ()
forceSVArg :: SV -> IO ()
forceSVArg (SV k :: Kind
k n :: NodeId
n) = Kind
k Kind -> IO () -> IO ()
forall a b. a -> b -> b
`seq` NodeId
n NodeId -> IO () -> IO ()
forall a b. a -> b -> b
`seq` () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | Constant False as an 'SV'. Note that this value always occupies slot -2.
falseSV :: SV
falseSV :: SV
falseSV = Kind -> NodeId -> SV
SV Kind
KBool (NodeId -> SV) -> NodeId -> SV
forall a b. (a -> b) -> a -> b
$ Int -> NodeId
NodeId (-2)

-- | Constant True as an 'SV'. Note that this value always occupies slot -1.
trueSV :: SV
trueSV :: SV
trueSV  = Kind -> NodeId -> SV
SV Kind
KBool (NodeId -> SV) -> NodeId -> SV
forall a b. (a -> b) -> a -> b
$ Int -> NodeId
NodeId (-1)

-- | Symbolic operations
data Op = Plus
        | Times
        | Minus
        | UNeg
        | Abs
        | Quot
        | Rem
        | Equal
        | NotEqual
        | LessThan
        | GreaterThan
        | LessEq
        | GreaterEq
        | Ite
        | And
        | Or
        | XOr
        | Not
        | Shl
        | Shr
        | Rol Int
        | Ror Int
        | Extract Int Int                       -- Extract i j: extract bits i to j. Least significant bit is 0 (big-endian)
        | Join                                  -- Concat two words to form a bigger one, in the order given
        | LkUp (Int, Kind, Kind, Int) !SV !SV   -- (table-index, arg-type, res-type, length of the table) index out-of-bounds-value
        | ArrEq   ArrayIndex ArrayIndex         -- Array equality
        | ArrRead ArrayIndex
        | KindCast Kind Kind
        | Uninterpreted String
        | Label String                          -- Essentially no-op; useful for code generation to emit comments.
        | IEEEFP FPOp                           -- Floating-point ops, categorized separately
        | PseudoBoolean PBOp                    -- Pseudo-boolean ops, categorized separately
        | OverflowOp    OvOp                    -- Overflow-ops, categorized separately
        | StrOp StrOp                           -- String ops, categorized separately
        | SeqOp SeqOp                           -- Sequence ops, categorized separately
        | SetOp SetOp                           -- Set operations, categorized separately
        | TupleConstructor Int                  -- Construct an n-tuple
        | TupleAccess Int Int                   -- Access element i of an n-tuple; second argument is n
        | EitherConstructor Kind Kind Bool      -- Construct a sum; False: left, True: right
        | EitherIs Kind Kind Bool               -- Either branch tester; False: left, True: right
        | EitherAccess Bool                     -- Either branch access; False: left, True: right
        | 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 (Op -> Op -> Bool
(Op -> Op -> Bool) -> (Op -> Op -> Bool) -> Eq Op
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Op -> Op -> Bool
$c/= :: Op -> Op -> Bool
== :: Op -> Op -> Bool
$c== :: Op -> Op -> Bool
Eq, Eq Op
Eq Op =>
(Op -> Op -> Ordering)
-> (Op -> Op -> Bool)
-> (Op -> Op -> Bool)
-> (Op -> Op -> Bool)
-> (Op -> Op -> Bool)
-> (Op -> Op -> Op)
-> (Op -> Op -> Op)
-> Ord Op
Op -> Op -> Bool
Op -> Op -> Ordering
Op -> Op -> Op
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Op -> Op -> Op
$cmin :: Op -> Op -> Op
max :: Op -> Op -> Op
$cmax :: Op -> Op -> Op
>= :: Op -> Op -> Bool
$c>= :: Op -> Op -> Bool
> :: Op -> Op -> Bool
$c> :: Op -> Op -> Bool
<= :: Op -> Op -> Bool
$c<= :: Op -> Op -> Bool
< :: Op -> Op -> Bool
$c< :: Op -> Op -> Bool
compare :: Op -> Op -> Ordering
$ccompare :: Op -> Op -> Ordering
$cp1Ord :: Eq Op
Ord)

-- | Floating point operations
data FPOp = FP_Cast        Kind Kind SV   -- From-Kind, To-Kind, RoundingMode. This is "value" conversion
          | FP_Reinterpret Kind Kind      -- From-Kind, To-Kind. This is bit-reinterpretation using IEEE-754 interchange format
          | FP_Abs
          | FP_Neg
          | FP_Add
          | FP_Sub
          | FP_Mul
          | FP_Div
          | FP_FMA
          | FP_Sqrt
          | FP_Rem
          | FP_RoundToIntegral
          | FP_Min
          | FP_Max
          | FP_ObjEqual
          | FP_IsNormal
          | FP_IsSubnormal
          | FP_IsZero
          | FP_IsInfinite
          | FP_IsNaN
          | FP_IsNegative
          | FP_IsPositive
          deriving (FPOp -> FPOp -> Bool
(FPOp -> FPOp -> Bool) -> (FPOp -> FPOp -> Bool) -> Eq FPOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FPOp -> FPOp -> Bool
$c/= :: FPOp -> FPOp -> Bool
== :: FPOp -> FPOp -> Bool
$c== :: FPOp -> FPOp -> Bool
Eq, Eq FPOp
Eq FPOp =>
(FPOp -> FPOp -> Ordering)
-> (FPOp -> FPOp -> Bool)
-> (FPOp -> FPOp -> Bool)
-> (FPOp -> FPOp -> Bool)
-> (FPOp -> FPOp -> Bool)
-> (FPOp -> FPOp -> FPOp)
-> (FPOp -> FPOp -> FPOp)
-> Ord FPOp
FPOp -> FPOp -> Bool
FPOp -> FPOp -> Ordering
FPOp -> FPOp -> FPOp
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: FPOp -> FPOp -> FPOp
$cmin :: FPOp -> FPOp -> FPOp
max :: FPOp -> FPOp -> FPOp
$cmax :: FPOp -> FPOp -> FPOp
>= :: FPOp -> FPOp -> Bool
$c>= :: FPOp -> FPOp -> Bool
> :: FPOp -> FPOp -> Bool
$c> :: FPOp -> FPOp -> Bool
<= :: FPOp -> FPOp -> Bool
$c<= :: FPOp -> FPOp -> Bool
< :: FPOp -> FPOp -> Bool
$c< :: FPOp -> FPOp -> Bool
compare :: FPOp -> FPOp -> Ordering
$ccompare :: FPOp -> FPOp -> Ordering
$cp1Ord :: Eq FPOp
Ord)

-- 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
-- is FP_Cast; where we handle different source/origins explicitly later on.
instance Show FPOp where
   show :: FPOp -> String
show (FP_Cast f :: Kind
f t :: Kind
t r :: SV
r)      = "(FP_Cast: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ " -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ ", using RM [" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ "])"
   show (FP_Reinterpret f :: Kind
f t :: Kind
t) = case (Kind
f, Kind
t) of
                                  (KBounded False 32, KFloat)  -> "(_ to_fp 8 24)"
                                  (KBounded False 64, KDouble) -> "(_ to_fp 11 53)"
                                  _                            -> ShowS
forall a. HasCallStack => String -> a
error ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ "SBV.FP_Reinterpret: Unexpected conversion: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ " to " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
t
   show FP_Abs               = "fp.abs"
   show FP_Neg               = "fp.neg"
   show FP_Add               = "fp.add"
   show FP_Sub               = "fp.sub"
   show FP_Mul               = "fp.mul"
   show FP_Div               = "fp.div"
   show FP_FMA               = "fp.fma"
   show FP_Sqrt              = "fp.sqrt"
   show FP_Rem               = "fp.rem"
   show FP_RoundToIntegral   = "fp.roundToIntegral"
   show FP_Min               = "fp.min"
   show FP_Max               = "fp.max"
   show FP_ObjEqual          = "="
   show FP_IsNormal          = "fp.isNormal"
   show FP_IsSubnormal       = "fp.isSubnormal"
   show FP_IsZero            = "fp.isZero"
   show FP_IsInfinite        = "fp.isInfinite"
   show FP_IsNaN             = "fp.isNaN"
   show FP_IsNegative        = "fp.isNegative"
   show FP_IsPositive        = "fp.isPositive"

-- | Pseudo-boolean operations
data PBOp = PB_AtMost  Int        -- ^ At most k
          | PB_AtLeast Int        -- ^ At least k
          | PB_Exactly Int        -- ^ Exactly 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 (PBOp -> PBOp -> Bool
(PBOp -> PBOp -> Bool) -> (PBOp -> PBOp -> Bool) -> Eq PBOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PBOp -> PBOp -> Bool
$c/= :: PBOp -> PBOp -> Bool
== :: PBOp -> PBOp -> Bool
$c== :: PBOp -> PBOp -> Bool
Eq, Eq PBOp
Eq PBOp =>
(PBOp -> PBOp -> Ordering)
-> (PBOp -> PBOp -> Bool)
-> (PBOp -> PBOp -> Bool)
-> (PBOp -> PBOp -> Bool)
-> (PBOp -> PBOp -> Bool)
-> (PBOp -> PBOp -> PBOp)
-> (PBOp -> PBOp -> PBOp)
-> Ord PBOp
PBOp -> PBOp -> Bool
PBOp -> PBOp -> Ordering
PBOp -> PBOp -> PBOp
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: PBOp -> PBOp -> PBOp
$cmin :: PBOp -> PBOp -> PBOp
max :: PBOp -> PBOp -> PBOp
$cmax :: PBOp -> PBOp -> PBOp
>= :: PBOp -> PBOp -> Bool
$c>= :: PBOp -> PBOp -> Bool
> :: PBOp -> PBOp -> Bool
$c> :: PBOp -> PBOp -> Bool
<= :: PBOp -> PBOp -> Bool
$c<= :: PBOp -> PBOp -> Bool
< :: PBOp -> PBOp -> Bool
$c< :: PBOp -> PBOp -> Bool
compare :: PBOp -> PBOp -> Ordering
$ccompare :: PBOp -> PBOp -> Ordering
$cp1Ord :: Eq PBOp
Ord, Int -> PBOp -> ShowS
[PBOp] -> ShowS
PBOp -> String
(Int -> PBOp -> ShowS)
-> (PBOp -> String) -> ([PBOp] -> ShowS) -> Show PBOp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PBOp] -> ShowS
$cshowList :: [PBOp] -> ShowS
show :: PBOp -> String
$cshow :: PBOp -> String
showsPrec :: Int -> PBOp -> ShowS
$cshowsPrec :: Int -> PBOp -> ShowS
Show)

-- | Overflow operations
data OvOp = Overflow_SMul_OVFL   -- ^ Signed multiplication overflow
          | Overflow_SMul_UDFL   -- ^ Signed multiplication underflow
          | Overflow_UMul_OVFL   -- ^ Unsigned multiplication overflow
          deriving (OvOp -> OvOp -> Bool
(OvOp -> OvOp -> Bool) -> (OvOp -> OvOp -> Bool) -> Eq OvOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OvOp -> OvOp -> Bool
$c/= :: OvOp -> OvOp -> Bool
== :: OvOp -> OvOp -> Bool
$c== :: OvOp -> OvOp -> Bool
Eq, Eq OvOp
Eq OvOp =>
(OvOp -> OvOp -> Ordering)
-> (OvOp -> OvOp -> Bool)
-> (OvOp -> OvOp -> Bool)
-> (OvOp -> OvOp -> Bool)
-> (OvOp -> OvOp -> Bool)
-> (OvOp -> OvOp -> OvOp)
-> (OvOp -> OvOp -> OvOp)
-> Ord OvOp
OvOp -> OvOp -> Bool
OvOp -> OvOp -> Ordering
OvOp -> OvOp -> OvOp
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: OvOp -> OvOp -> OvOp
$cmin :: OvOp -> OvOp -> OvOp
max :: OvOp -> OvOp -> OvOp
$cmax :: OvOp -> OvOp -> OvOp
>= :: OvOp -> OvOp -> Bool
$c>= :: OvOp -> OvOp -> Bool
> :: OvOp -> OvOp -> Bool
$c> :: OvOp -> OvOp -> Bool
<= :: OvOp -> OvOp -> Bool
$c<= :: OvOp -> OvOp -> Bool
< :: OvOp -> OvOp -> Bool
$c< :: OvOp -> OvOp -> Bool
compare :: OvOp -> OvOp -> Ordering
$ccompare :: OvOp -> OvOp -> Ordering
$cp1Ord :: Eq OvOp
Ord)

-- | Show instance. It's important that these follow the internal z3 names
instance Show OvOp where
  show :: OvOp -> String
show Overflow_SMul_OVFL = "bvsmul_noovfl"
  show Overflow_SMul_UDFL = "bvsmul_noudfl"
  show Overflow_UMul_OVFL = "bvumul_noovfl"

-- | String operations. Note that we do not define @StrAt@ as it translates to 'StrSubstr' trivially.
data StrOp = StrConcat       -- ^ Concatenation of one or more strings
           | StrLen          -- ^ String length
           | StrUnit         -- ^ Unit string
           | StrNth          -- ^ Nth element
           | StrSubstr       -- ^ Retrieves substring of @s@ at @offset@
           | StrIndexOf      -- ^ Retrieves first position of @sub@ in @s@, @-1@ if there are no occurrences
           | StrContains     -- ^ Does @s@ contain the substring @sub@?
           | StrPrefixOf     -- ^ Is @pre@ a prefix of @s@?
           | StrSuffixOf     -- ^ Is @suf@ a suffix of @s@?
           | StrReplace      -- ^ Replace the first occurrence of @src@ by @dst@ in @s@
           | StrStrToNat     -- ^ Retrieve integer encoded by string @s@ (ground rewriting only)
           | StrNatToStr     -- ^ Retrieve string encoded by integer @i@ (ground rewriting only)
           | StrInRe RegExp  -- ^ Check if string is in the regular expression
           deriving (StrOp -> StrOp -> Bool
(StrOp -> StrOp -> Bool) -> (StrOp -> StrOp -> Bool) -> Eq StrOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: StrOp -> StrOp -> Bool
$c/= :: StrOp -> StrOp -> Bool
== :: StrOp -> StrOp -> Bool
$c== :: StrOp -> StrOp -> Bool
Eq, Eq StrOp
Eq StrOp =>
(StrOp -> StrOp -> Ordering)
-> (StrOp -> StrOp -> Bool)
-> (StrOp -> StrOp -> Bool)
-> (StrOp -> StrOp -> Bool)
-> (StrOp -> StrOp -> Bool)
-> (StrOp -> StrOp -> StrOp)
-> (StrOp -> StrOp -> StrOp)
-> Ord StrOp
StrOp -> StrOp -> Bool
StrOp -> StrOp -> Ordering
StrOp -> StrOp -> StrOp
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: StrOp -> StrOp -> StrOp
$cmin :: StrOp -> StrOp -> StrOp
max :: StrOp -> StrOp -> StrOp
$cmax :: StrOp -> StrOp -> StrOp
>= :: StrOp -> StrOp -> Bool
$c>= :: StrOp -> StrOp -> Bool
> :: StrOp -> StrOp -> Bool
$c> :: StrOp -> StrOp -> Bool
<= :: StrOp -> StrOp -> Bool
$c<= :: StrOp -> StrOp -> Bool
< :: StrOp -> StrOp -> Bool
$c< :: StrOp -> StrOp -> Bool
compare :: StrOp -> StrOp -> Ordering
$ccompare :: StrOp -> StrOp -> Ordering
$cp1Ord :: Eq StrOp
Ord)

-- | Regular expressions. Note that regular expressions themselves are
-- concrete, but the 'Data.SBV.RegExp.match' function from the 'Data.SBV.RegExp.RegExpMatchable' class
-- can check membership against a symbolic string/character. Also, we
-- are preferring a datatype approach here, as opposed to coming up with
-- some string-representation; there are way too many alternatives
-- already so inventing one isn't a priority. Please get in touch if you
-- would like a parser for this type as it might be easier to use.
data RegExp = Literal String       -- ^ Precisely match the given string
            | All                  -- ^ Accept every string
            | None                 -- ^ Accept no strings
            | Range Char Char      -- ^ Accept range of characters
            | Conc  [RegExp]       -- ^ Concatenation
            | KStar RegExp         -- ^ Kleene Star: Zero or more
            | KPlus RegExp         -- ^ Kleene Plus: One or more
            | Opt   RegExp         -- ^ Zero or one
            | Loop  Int Int RegExp -- ^ From @n@ repetitions to @m@ repetitions
            | Union [RegExp]       -- ^ Union of regular expressions
            | Inter RegExp RegExp  -- ^ Intersection of regular expressions
            deriving (RegExp -> RegExp -> Bool
(RegExp -> RegExp -> Bool)
-> (RegExp -> RegExp -> Bool) -> Eq RegExp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RegExp -> RegExp -> Bool
$c/= :: RegExp -> RegExp -> Bool
== :: RegExp -> RegExp -> Bool
$c== :: RegExp -> RegExp -> Bool
Eq, Eq RegExp
Eq RegExp =>
(RegExp -> RegExp -> Ordering)
-> (RegExp -> RegExp -> Bool)
-> (RegExp -> RegExp -> Bool)
-> (RegExp -> RegExp -> Bool)
-> (RegExp -> RegExp -> Bool)
-> (RegExp -> RegExp -> RegExp)
-> (RegExp -> RegExp -> RegExp)
-> Ord RegExp
RegExp -> RegExp -> Bool
RegExp -> RegExp -> Ordering
RegExp -> RegExp -> RegExp
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: RegExp -> RegExp -> RegExp
$cmin :: RegExp -> RegExp -> RegExp
max :: RegExp -> RegExp -> RegExp
$cmax :: RegExp -> RegExp -> RegExp
>= :: RegExp -> RegExp -> Bool
$c>= :: RegExp -> RegExp -> Bool
> :: RegExp -> RegExp -> Bool
$c> :: RegExp -> RegExp -> Bool
<= :: RegExp -> RegExp -> Bool
$c<= :: RegExp -> RegExp -> Bool
< :: RegExp -> RegExp -> Bool
$c< :: RegExp -> RegExp -> Bool
compare :: RegExp -> RegExp -> Ordering
$ccompare :: RegExp -> RegExp -> Ordering
$cp1Ord :: Eq RegExp
Ord)

-- | With overloaded strings, we can have direct literal regular expressions.
instance IsString RegExp where
  fromString :: String -> RegExp
fromString = String -> RegExp
Literal

-- | Regular expressions as a 'Num' instance. Note that
-- only `+` (union) and `*` (concatenation) make sense.
instance Num RegExp where
  -- flatten the concats to make them simpler
  Conc xs :: [RegExp]
xs * :: RegExp -> RegExp -> RegExp
* y :: RegExp
y = [RegExp] -> RegExp
Conc ([RegExp]
xs [RegExp] -> [RegExp] -> [RegExp]
forall a. [a] -> [a] -> [a]
++ [RegExp
y])
  x :: RegExp
x * Conc ys :: [RegExp]
ys = [RegExp] -> RegExp
Conc (RegExp
x  RegExp -> [RegExp] -> [RegExp]
forall a. a -> [a] -> [a]
:  [RegExp]
ys)
  x :: RegExp
x * y :: RegExp
y       = [RegExp] -> RegExp
Conc [RegExp
x, RegExp
y]

  -- flatten the unions to make them simpler
  Union xs :: [RegExp]
xs + :: RegExp -> RegExp -> RegExp
+ y :: RegExp
y = [RegExp] -> RegExp
Union ([RegExp]
xs [RegExp] -> [RegExp] -> [RegExp]
forall a. [a] -> [a] -> [a]
++ [RegExp
y])
  x :: RegExp
x + Union ys :: [RegExp]
ys = [RegExp] -> RegExp
Union (RegExp
x  RegExp -> [RegExp] -> [RegExp]
forall a. a -> [a] -> [a]
: [RegExp]
ys)
  x :: RegExp
x + y :: RegExp
y        = [RegExp] -> RegExp
Union [RegExp
x, RegExp
y]

  abs :: RegExp -> RegExp
abs         = String -> RegExp -> RegExp
forall a. HasCallStack => String -> a
error "Num.RegExp: no abs method"
  signum :: RegExp -> RegExp
signum      = String -> RegExp -> RegExp
forall a. HasCallStack => String -> a
error "Num.RegExp: no signum method"

  fromInteger :: Integer -> RegExp
fromInteger x :: Integer
x
    | Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 0    = RegExp
None
    | Integer
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== 1    = String -> RegExp
Literal ""   -- Unit for concatenation is the empty string
    | Bool
True      = String -> RegExp
forall a. HasCallStack => String -> a
error (String -> RegExp) -> String -> RegExp
forall a b. (a -> b) -> a -> b
$ "Num.RegExp: Only 0 and 1 makes sense as a reg-exp, no meaning for: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
x

  negate :: RegExp -> RegExp
negate      = String -> RegExp -> RegExp
forall a. HasCallStack => String -> a
error "Num.RegExp: no negate method"

-- | Show instance for `RegExp`. The mapping is done so the outcome matches the
-- SMTLib string reg-exp operations
instance Show RegExp where
  show :: RegExp -> String
show (Literal s :: String
s)       = "(str.to.re \"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
stringToQFS String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\")"
  show All               = "re.allchar"
  show None              = "re.nostr"
  show (Range ch1 :: Char
ch1 ch2 :: Char
ch2)   = "(re.range \"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
stringToQFS [Char
ch1] String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\" \"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
stringToQFS [Char
ch2] String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\")"
  show (Conc [])         = Integer -> String
forall a. Show a => a -> String
show (1 :: Integer)
  show (Conc [x :: RegExp
x])        = RegExp -> String
forall a. Show a => a -> String
show RegExp
x
  show (Conc xs :: [RegExp]
xs)         = "(re.++ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((RegExp -> String) -> [RegExp] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map RegExp -> String
forall a. Show a => a -> String
show [RegExp]
xs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
  show (KStar r :: RegExp
r)         = "(re.* " String -> ShowS
forall a. [a] -> [a] -> [a]
++ RegExp -> String
forall a. Show a => a -> String
show RegExp
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
  show (KPlus r :: RegExp
r)         = "(re.+ " String -> ShowS
forall a. [a] -> [a] -> [a]
++ RegExp -> String
forall a. Show a => a -> String
show RegExp
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
  show (Opt   r :: RegExp
r)         = "(re.opt " String -> ShowS
forall a. [a] -> [a] -> [a]
++ RegExp -> String
forall a. Show a => a -> String
show RegExp
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
  show (Loop  lo :: Int
lo hi :: Int
hi r :: RegExp
r)
     | Int
lo Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= 0, Int
hi Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
lo = "((_ re.loop " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
lo String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
hi String -> ShowS
forall a. [a] -> [a] -> [a]
++ ") " String -> ShowS
forall a. [a] -> [a] -> [a]
++ RegExp -> String
forall a. Show a => a -> String
show RegExp
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
     | Bool
True              = ShowS
forall a. HasCallStack => String -> a
error ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ "Invalid regular-expression Loop with arguments: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall a. Show a => a -> String
show (Int
lo, Int
hi)
  show (Inter r1 :: RegExp
r1 r2 :: RegExp
r2)     = "(re.inter " String -> ShowS
forall a. [a] -> [a] -> [a]
++ RegExp -> String
forall a. Show a => a -> String
show RegExp
r1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ RegExp -> String
forall a. Show a => a -> String
show RegExp
r2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
  show (Union [])        = "re.nostr"
  show (Union [x :: RegExp
x])       = RegExp -> String
forall a. Show a => a -> String
show RegExp
x
  show (Union xs :: [RegExp]
xs)        = "(re.union " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((RegExp -> String) -> [RegExp] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map RegExp -> String
forall a. Show a => a -> String
show [RegExp]
xs) String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"

-- | Show instance for @StrOp@. Note that the mapping here is
-- important to match the SMTLib equivalents, see here: <http://rise4fun.com/z3/tutorialcontent/sequences>
instance Show StrOp where
  show :: StrOp -> String
show StrConcat   = "str.++"
  show StrLen      = "str.len"
  show StrUnit     = "seq.unit"      -- NB. The "seq" prefix is intentional; works uniformly.
  show StrNth      = "seq.nth"       -- NB. The "seq" prefix is intentional; works uniformly.
  show StrSubstr   = "str.substr"
  show StrIndexOf  = "str.indexof"
  show StrContains = "str.contains"
  show StrPrefixOf = "str.prefixof"
  show StrSuffixOf = "str.suffixof"
  show StrReplace  = "str.replace"
  show StrStrToNat = "str.to.int"    -- NB. SMTLib uses "int" here though only nats are supported
  show StrNatToStr = "int.to.str"    -- NB. SMTLib uses "int" here though only nats are supported
  -- Note the breakage here with respect to argument order. We fix this explicitly later.
  show (StrInRe s :: RegExp
s) = "str.in.re " String -> ShowS
forall a. [a] -> [a] -> [a]
++ RegExp -> String
forall a. Show a => a -> String
show RegExp
s

-- | Sequence operations.
data SeqOp = SeqConcat    -- ^ See StrConcat
           | SeqLen       -- ^ See StrLen
           | SeqUnit      -- ^ See StrUnit
           | SeqNth       -- ^ See StrNth
           | SeqSubseq    -- ^ See StrSubseq
           | SeqIndexOf   -- ^ See StrIndexOf
           | SeqContains  -- ^ See StrContains
           | SeqPrefixOf  -- ^ See StrPrefixOf
           | SeqSuffixOf  -- ^ See StrSuffixOf
           | SeqReplace   -- ^ See StrReplace
  deriving (SeqOp -> SeqOp -> Bool
(SeqOp -> SeqOp -> Bool) -> (SeqOp -> SeqOp -> Bool) -> Eq SeqOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SeqOp -> SeqOp -> Bool
$c/= :: SeqOp -> SeqOp -> Bool
== :: SeqOp -> SeqOp -> Bool
$c== :: SeqOp -> SeqOp -> Bool
Eq, Eq SeqOp
Eq SeqOp =>
(SeqOp -> SeqOp -> Ordering)
-> (SeqOp -> SeqOp -> Bool)
-> (SeqOp -> SeqOp -> Bool)
-> (SeqOp -> SeqOp -> Bool)
-> (SeqOp -> SeqOp -> Bool)
-> (SeqOp -> SeqOp -> SeqOp)
-> (SeqOp -> SeqOp -> SeqOp)
-> Ord SeqOp
SeqOp -> SeqOp -> Bool
SeqOp -> SeqOp -> Ordering
SeqOp -> SeqOp -> SeqOp
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SeqOp -> SeqOp -> SeqOp
$cmin :: SeqOp -> SeqOp -> SeqOp
max :: SeqOp -> SeqOp -> SeqOp
$cmax :: SeqOp -> SeqOp -> SeqOp
>= :: SeqOp -> SeqOp -> Bool
$c>= :: SeqOp -> SeqOp -> Bool
> :: SeqOp -> SeqOp -> Bool
$c> :: SeqOp -> SeqOp -> Bool
<= :: SeqOp -> SeqOp -> Bool
$c<= :: SeqOp -> SeqOp -> Bool
< :: SeqOp -> SeqOp -> Bool
$c< :: SeqOp -> SeqOp -> Bool
compare :: SeqOp -> SeqOp -> Ordering
$ccompare :: SeqOp -> SeqOp -> Ordering
$cp1Ord :: Eq SeqOp
Ord)

-- | Show instance for SeqOp. Again, mapping is important.
instance Show SeqOp where
  show :: SeqOp -> String
show SeqConcat   = "seq.++"
  show SeqLen      = "seq.len"
  show SeqUnit     = "seq.unit"
  show SeqNth      = "seq.nth"
  show SeqSubseq   = "seq.extract"
  show SeqIndexOf  = "seq.indexof"
  show SeqContains = "seq.contains"
  show SeqPrefixOf = "seq.prefixof"
  show SeqSuffixOf = "seq.suffixof"
  show SeqReplace  = "seq.replace"

-- | Set operations.
data SetOp = SetEqual
           | SetMember
           | SetInsert
           | SetDelete
           | SetIntersect
           | SetUnion
           | SetSubset
           | SetDifference
           | SetComplement
           | SetHasSize
        deriving (SetOp -> SetOp -> Bool
(SetOp -> SetOp -> Bool) -> (SetOp -> SetOp -> Bool) -> Eq SetOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SetOp -> SetOp -> Bool
$c/= :: SetOp -> SetOp -> Bool
== :: SetOp -> SetOp -> Bool
$c== :: SetOp -> SetOp -> Bool
Eq, Eq SetOp
Eq SetOp =>
(SetOp -> SetOp -> Ordering)
-> (SetOp -> SetOp -> Bool)
-> (SetOp -> SetOp -> Bool)
-> (SetOp -> SetOp -> Bool)
-> (SetOp -> SetOp -> Bool)
-> (SetOp -> SetOp -> SetOp)
-> (SetOp -> SetOp -> SetOp)
-> Ord SetOp
SetOp -> SetOp -> Bool
SetOp -> SetOp -> Ordering
SetOp -> SetOp -> SetOp
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SetOp -> SetOp -> SetOp
$cmin :: SetOp -> SetOp -> SetOp
max :: SetOp -> SetOp -> SetOp
$cmax :: SetOp -> SetOp -> SetOp
>= :: SetOp -> SetOp -> Bool
$c>= :: SetOp -> SetOp -> Bool
> :: SetOp -> SetOp -> Bool
$c> :: SetOp -> SetOp -> Bool
<= :: SetOp -> SetOp -> Bool
$c<= :: SetOp -> SetOp -> Bool
< :: SetOp -> SetOp -> Bool
$c< :: SetOp -> SetOp -> Bool
compare :: SetOp -> SetOp -> Ordering
$ccompare :: SetOp -> SetOp -> Ordering
$cp1Ord :: Eq SetOp
Ord)

-- The show instance for 'SetOp' is merely for debugging, we map them separately so
-- the mapped strings are less important here.
instance Show SetOp where
  show :: SetOp -> String
show SetEqual      = "=="
  show SetMember     = "Set.member"
  show SetInsert     = "Set.insert"
  show SetDelete     = "Set.delete"
  show SetIntersect  = "Set.intersect"
  show SetUnion      = "Set.union"
  show SetSubset     = "Set.subset"
  show SetDifference = "Set.difference"
  show SetComplement = "Set.complement"
  show SetHasSize    = "Set.setHasSize"

-- Show instance for 'Op'. Note that this is largely for debugging purposes, not used
-- for being read by any tool.
instance Show Op where
  show :: Op -> String
show Shl    = "<<"
  show Shr    = ">>"

  show (Rol i :: Int
i) = "<<<" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
  show (Ror i :: Int
i) = ">>>" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i

  show (Extract i :: Int
i j :: Int
j) = "choose [" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ ":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
j String -> ShowS
forall a. [a] -> [a] -> [a]
++ "]"

  show (LkUp (ti :: Int
ti, at :: Kind
at, rt :: Kind
rt, l :: Int
l) i :: SV
i e :: SV
e)
        = "lookup(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
tinfo String -> ShowS
forall a. [a] -> [a] -> [a]
++ ", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ ", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
        where tinfo :: String
tinfo = "table" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
ti String -> ShowS
forall a. [a] -> [a] -> [a]
++ "(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
at String -> ShowS
forall a. [a] -> [a] -> [a]
++ " -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
rt String -> ShowS
forall a. [a] -> [a] -> [a]
++ ", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"

  show (ArrEq i :: ArrayIndex
i j :: ArrayIndex
j)          = "array_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ArrayIndex -> String
forall a. Show a => a -> String
show ArrayIndex
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ " == array_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ArrayIndex -> String
forall a. Show a => a -> String
show ArrayIndex
j
  show (ArrRead i :: ArrayIndex
i)          = "select array_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ArrayIndex -> String
forall a. Show a => a -> String
show ArrayIndex
i

  show (KindCast fr :: Kind
fr to :: Kind
to)     = "cast_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
fr String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
to
  show (Uninterpreted i :: String
i)    = "[uninterpreted] " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
i

  show (Label s :: String
s)            = "[label] " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s

  show (IEEEFP w :: FPOp
w)           = FPOp -> String
forall a. Show a => a -> String
show FPOp
w

  show (PseudoBoolean p :: PBOp
p)    = PBOp -> String
forall a. Show a => a -> String
show PBOp
p

  show (OverflowOp o :: OvOp
o)       = OvOp -> String
forall a. Show a => a -> String
show OvOp
o

  show (StrOp s :: StrOp
s)            = StrOp -> String
forall a. Show a => a -> String
show StrOp
s
  show (SeqOp s :: SeqOp
s)            = SeqOp -> String
forall a. Show a => a -> String
show SeqOp
s
  show (SetOp s :: SetOp
s)            = SetOp -> String
forall a. Show a => a -> String
show SetOp
s

  show (TupleConstructor   0) = "mkSBVTuple0"
  show (TupleConstructor   n :: Int
n) = "mkSBVTuple" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
  show (TupleAccess      i :: Int
i n :: Int
n) = "proj_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_SBVTuple" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n

  show (EitherConstructor k1 :: Kind
k1 k2 :: Kind
k2  False) = "(_ left_SBVEither "  String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show (Kind -> Kind -> Kind
KEither Kind
k1 Kind
k2) String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
  show (EitherConstructor k1 :: Kind
k1 k2 :: Kind
k2  True ) = "(_ right_SBVEither " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show (Kind -> Kind -> Kind
KEither Kind
k1 Kind
k2) String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
  show (EitherIs          k1 :: Kind
k1 k2 :: Kind
k2  False) = "(_ is (left_SBVEither ("  String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ ") " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show (Kind -> Kind -> Kind
KEither Kind
k1 Kind
k2) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "))"
  show (EitherIs          k1 :: Kind
k1 k2 :: Kind
k2  True ) = "(_ is (right_SBVEither (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ ") " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show (Kind -> Kind -> Kind
KEither Kind
k1 Kind
k2) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "))"
  show (EitherAccess             False) = "get_left_SBVEither"
  show (EitherAccess             True ) = "get_right_SBVEither"

  show (MaybeConstructor k :: Kind
k False) = "(_ nothing_SBVMaybe " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show (Kind -> Kind
KMaybe Kind
k) String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
  show (MaybeConstructor k :: Kind
k True)  = "(_ just_SBVMaybe "    String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show (Kind -> Kind
KMaybe Kind
k) String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
  show (MaybeIs          k :: Kind
k False) = "(_ is (nothing_SBVMaybe () "              String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show (Kind -> Kind
KMaybe Kind
k) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "))"
  show (MaybeIs          k :: Kind
k True ) = "(_ is (just_SBVMaybe (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ ") " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show (Kind -> Kind
KMaybe Kind
k) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "))"
  show MaybeAccess               = "get_just_SBVMaybe"

  show op :: Op
op
    | Just s :: String
s <- Op
op Op -> [(Op, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(Op, String)]
syms = String
s
    | Bool
True                       = ShowS
forall a. HasCallStack => String -> a
error "impossible happened; can't find op!"
    where syms :: [(Op, String)]
syms = [ (Op
Plus, "+"), (Op
Times, "*"), (Op
Minus, "-"), (Op
UNeg, "-"), (Op
Abs, "abs")
                 , (Op
Quot, "quot")
                 , (Op
Rem,  "rem")
                 , (Op
Equal, "=="), (Op
NotEqual, "/=")
                 , (Op
LessThan, "<"), (Op
GreaterThan, ">"), (Op
LessEq, "<="), (Op
GreaterEq, ">=")
                 , (Op
Ite, "if_then_else")
                 , (Op
And, "&"), (Op
Or, "|"), (Op
XOr, "^"), (Op
Not, "~")
                 , (Op
Join, "#")
                 ]

-- | Quantifiers: forall or exists. Note that we allow
-- arbitrary nestings.
data Quantifier = ALL | EX deriving Quantifier -> Quantifier -> Bool
(Quantifier -> Quantifier -> Bool)
-> (Quantifier -> Quantifier -> Bool) -> Eq Quantifier
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Quantifier -> Quantifier -> Bool
$c/= :: Quantifier -> Quantifier -> Bool
== :: Quantifier -> Quantifier -> Bool
$c== :: Quantifier -> Quantifier -> Bool
Eq

-- | Show instance for 'Quantifier'
instance Show Quantifier where
  show :: Quantifier -> String
show ALL = "Forall"
  show EX  = "Exists"

-- | Are there any existential quantifiers?
needsExistentials :: [Quantifier] -> Bool
needsExistentials :: [Quantifier] -> Bool
needsExistentials = (Quantifier
EX Quantifier -> [Quantifier] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`)

-- | A simple type for SBV computations, used mainly for uninterpreted constants.
-- We keep track of the signedness/size of the arguments. A non-function will
-- have just one entry in the list.
newtype SBVType = SBVType [Kind]
             deriving (SBVType -> SBVType -> Bool
(SBVType -> SBVType -> Bool)
-> (SBVType -> SBVType -> Bool) -> Eq SBVType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SBVType -> SBVType -> Bool
$c/= :: SBVType -> SBVType -> Bool
== :: SBVType -> SBVType -> Bool
$c== :: SBVType -> SBVType -> Bool
Eq, Eq SBVType
Eq SBVType =>
(SBVType -> SBVType -> Ordering)
-> (SBVType -> SBVType -> Bool)
-> (SBVType -> SBVType -> Bool)
-> (SBVType -> SBVType -> Bool)
-> (SBVType -> SBVType -> Bool)
-> (SBVType -> SBVType -> SBVType)
-> (SBVType -> SBVType -> SBVType)
-> Ord SBVType
SBVType -> SBVType -> Bool
SBVType -> SBVType -> Ordering
SBVType -> SBVType -> SBVType
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SBVType -> SBVType -> SBVType
$cmin :: SBVType -> SBVType -> SBVType
max :: SBVType -> SBVType -> SBVType
$cmax :: SBVType -> SBVType -> SBVType
>= :: SBVType -> SBVType -> Bool
$c>= :: SBVType -> SBVType -> Bool
> :: SBVType -> SBVType -> Bool
$c> :: SBVType -> SBVType -> Bool
<= :: SBVType -> SBVType -> Bool
$c<= :: SBVType -> SBVType -> Bool
< :: SBVType -> SBVType -> Bool
$c< :: SBVType -> SBVType -> Bool
compare :: SBVType -> SBVType -> Ordering
$ccompare :: SBVType -> SBVType -> Ordering
$cp1Ord :: Eq SBVType
Ord)

instance Show SBVType where
  show :: SBVType -> String
show (SBVType []) = ShowS
forall a. HasCallStack => String -> a
error "SBV: internal error, empty SBVType"
  show (SBVType xs :: [Kind]
xs) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate " -> " ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Kind -> String) -> [Kind] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Kind -> String
forall a. Show a => a -> String
show [Kind]
xs

-- | A symbolic expression
data SBVExpr = SBVApp !Op ![SV]
             deriving (SBVExpr -> SBVExpr -> Bool
(SBVExpr -> SBVExpr -> Bool)
-> (SBVExpr -> SBVExpr -> Bool) -> Eq SBVExpr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SBVExpr -> SBVExpr -> Bool
$c/= :: SBVExpr -> SBVExpr -> Bool
== :: SBVExpr -> SBVExpr -> Bool
$c== :: SBVExpr -> SBVExpr -> Bool
Eq, Eq SBVExpr
Eq SBVExpr =>
(SBVExpr -> SBVExpr -> Ordering)
-> (SBVExpr -> SBVExpr -> Bool)
-> (SBVExpr -> SBVExpr -> Bool)
-> (SBVExpr -> SBVExpr -> Bool)
-> (SBVExpr -> SBVExpr -> Bool)
-> (SBVExpr -> SBVExpr -> SBVExpr)
-> (SBVExpr -> SBVExpr -> SBVExpr)
-> Ord SBVExpr
SBVExpr -> SBVExpr -> Bool
SBVExpr -> SBVExpr -> Ordering
SBVExpr -> SBVExpr -> SBVExpr
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: SBVExpr -> SBVExpr -> SBVExpr
$cmin :: SBVExpr -> SBVExpr -> SBVExpr
max :: SBVExpr -> SBVExpr -> SBVExpr
$cmax :: SBVExpr -> SBVExpr -> SBVExpr
>= :: SBVExpr -> SBVExpr -> Bool
$c>= :: SBVExpr -> SBVExpr -> Bool
> :: SBVExpr -> SBVExpr -> Bool
$c> :: SBVExpr -> SBVExpr -> Bool
<= :: SBVExpr -> SBVExpr -> Bool
$c<= :: SBVExpr -> SBVExpr -> Bool
< :: SBVExpr -> SBVExpr -> Bool
$c< :: SBVExpr -> SBVExpr -> Bool
compare :: SBVExpr -> SBVExpr -> Ordering
$ccompare :: SBVExpr -> SBVExpr -> Ordering
$cp1Ord :: Eq SBVExpr
Ord)

-- | To improve hash-consing, take advantage of commutative operators by
-- reordering their arguments.
reorder :: SBVExpr -> SBVExpr
reorder :: SBVExpr -> SBVExpr
reorder s :: SBVExpr
s = case SBVExpr
s of
              SBVApp op :: Op
op [a :: SV
a, b :: SV
b] | Op -> Bool
isCommutative Op
op Bool -> Bool -> Bool
&& SV
a SV -> SV -> Bool
forall a. Ord a => a -> a -> Bool
> SV
b -> Op -> [SV] -> SBVExpr
SBVApp Op
op [SV
b, SV
a]
              _ -> SBVExpr
s
  where isCommutative :: Op -> Bool
        isCommutative :: Op -> Bool
isCommutative o :: Op
o = Op
o Op -> [Op] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Op
Plus, Op
Times, Op
Equal, Op
NotEqual, Op
And, Op
Or, Op
XOr]

-- Show instance for 'SBVExpr'. Again, only for debugging purposes.
instance Show SBVExpr where
  show :: SBVExpr -> String
show (SBVApp Ite [t :: SV
t, a :: SV
a, b :: SV
b])             = [String] -> String
unwords ["if", SV -> String
forall a. Show a => a -> String
show SV
t, "then", SV -> String
forall a. Show a => a -> String
show SV
a, "else", SV -> String
forall a. Show a => a -> String
show SV
b]
  show (SBVApp Shl     [a :: SV
a, i :: SV
i])            = [String] -> String
unwords [SV -> String
forall a. Show a => a -> String
show SV
a, "<<", SV -> String
forall a. Show a => a -> String
show SV
i]
  show (SBVApp Shr     [a :: SV
a, i :: SV
i])            = [String] -> String
unwords [SV -> String
forall a. Show a => a -> String
show SV
a, ">>", SV -> String
forall a. Show a => a -> String
show SV
i]
  show (SBVApp (Rol i :: Int
i) [a :: SV
a])               = [String] -> String
unwords [SV -> String
forall a. Show a => a -> String
show SV
a, "<<<", Int -> String
forall a. Show a => a -> String
show Int
i]
  show (SBVApp (Ror i :: Int
i) [a :: SV
a])               = [String] -> String
unwords [SV -> String
forall a. Show a => a -> String
show SV
a, ">>>", Int -> String
forall a. Show a => a -> String
show Int
i]
  show (SBVApp (PseudoBoolean pb :: PBOp
pb) args :: [SV]
args)   = [String] -> String
unwords (PBOp -> String
forall a. Show a => a -> String
show PBOp
pb String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
forall a. Show a => a -> String
show [SV]
args)
  show (SBVApp (OverflowOp op :: OvOp
op)    args :: [SV]
args)   = [String] -> String
unwords (OvOp -> String
forall a. Show a => a -> String
show OvOp
op String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
forall a. Show a => a -> String
show [SV]
args)
  show (SBVApp op :: Op
op                 [a :: SV
a, b :: SV
b]) = [String] -> String
unwords [SV -> String
forall a. Show a => a -> String
show SV
a, Op -> String
forall a. Show a => a -> String
show Op
op, SV -> String
forall a. Show a => a -> String
show SV
b]
  show (SBVApp op :: Op
op                 args :: [SV]
args)   = [String] -> String
unwords (Op -> String
forall a. Show a => a -> String
show Op
op String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
forall a. Show a => a -> String
show [SV]
args)

-- | A program is a sequence of assignments
newtype SBVPgm = SBVPgm {SBVPgm -> Seq (SV, SBVExpr)
pgmAssignments :: S.Seq (SV, SBVExpr)}

-- | 'NamedSymVar' pairs symbolic values and user given/automatically generated names
type NamedSymVar = (SV, String)

-- | Style of optimization. Note that in the pareto case the user is allowed
-- to specify a max number of fronts to query the solver for, since there might
-- potentially be an infinite number of them and there is no way to know exactly
-- how many ahead of time. If 'Nothing' is given, SBV will possibly loop forever
-- if the number is really infinite.
data OptimizeStyle = Lexicographic      -- ^ Objectives are optimized in the order given, earlier objectives have higher priority.
                   | Independent        -- ^ Each objective is optimized independently.
                   | Pareto (Maybe Int) -- ^ Objectives are optimized according to pareto front: That is, no objective can be made better without making some other worse.
                   deriving (OptimizeStyle -> OptimizeStyle -> Bool
(OptimizeStyle -> OptimizeStyle -> Bool)
-> (OptimizeStyle -> OptimizeStyle -> Bool) -> Eq OptimizeStyle
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OptimizeStyle -> OptimizeStyle -> Bool
$c/= :: OptimizeStyle -> OptimizeStyle -> Bool
== :: OptimizeStyle -> OptimizeStyle -> Bool
$c== :: OptimizeStyle -> OptimizeStyle -> Bool
Eq, Int -> OptimizeStyle -> ShowS
[OptimizeStyle] -> ShowS
OptimizeStyle -> String
(Int -> OptimizeStyle -> ShowS)
-> (OptimizeStyle -> String)
-> ([OptimizeStyle] -> ShowS)
-> Show OptimizeStyle
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [OptimizeStyle] -> ShowS
$cshowList :: [OptimizeStyle] -> ShowS
show :: OptimizeStyle -> String
$cshow :: OptimizeStyle -> String
showsPrec :: Int -> OptimizeStyle -> ShowS
$cshowsPrec :: Int -> OptimizeStyle -> ShowS
Show)

-- | Penalty for a soft-assertion. The default penalty is @1@, with all soft-assertions belonging
-- to the same objective goal. A positive weight and an optional group can be provided by using
-- the 'Penalty' constructor.
data Penalty = DefaultPenalty                  -- ^ Default: Penalty of @1@ and no group attached
             | Penalty Rational (Maybe String) -- ^ Penalty with a weight and an optional group
             deriving Int -> Penalty -> ShowS
[Penalty] -> ShowS
Penalty -> String
(Int -> Penalty -> ShowS)
-> (Penalty -> String) -> ([Penalty] -> ShowS) -> Show Penalty
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Penalty] -> ShowS
$cshowList :: [Penalty] -> ShowS
show :: Penalty -> String
$cshow :: Penalty -> String
showsPrec :: Int -> Penalty -> ShowS
$cshowsPrec :: Int -> Penalty -> ShowS
Show

-- | Objective of optimization. We can minimize, maximize, or give a soft assertion with a penalty
-- for not satisfying it.
data Objective a = Minimize          String a         -- ^ Minimize this metric
                 | Maximize          String a         -- ^ Maximize this metric
                 | AssertWithPenalty String a Penalty -- ^ A soft assertion, with an associated penalty
                 deriving (Int -> Objective a -> ShowS
[Objective a] -> ShowS
Objective a -> String
(Int -> Objective a -> ShowS)
-> (Objective a -> String)
-> ([Objective a] -> ShowS)
-> Show (Objective a)
forall a. Show a => Int -> Objective a -> ShowS
forall a. Show a => [Objective a] -> ShowS
forall a. Show a => Objective a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Objective a] -> ShowS
$cshowList :: forall a. Show a => [Objective a] -> ShowS
show :: Objective a -> String
$cshow :: forall a. Show a => Objective a -> String
showsPrec :: Int -> Objective a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Objective a -> ShowS
Show, a -> Objective b -> Objective a
(a -> b) -> Objective a -> Objective b
(forall a b. (a -> b) -> Objective a -> Objective b)
-> (forall a b. a -> Objective b -> Objective a)
-> Functor Objective
forall a b. a -> Objective b -> Objective a
forall a b. (a -> b) -> Objective a -> Objective b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Objective b -> Objective a
$c<$ :: forall a b. a -> Objective b -> Objective a
fmap :: (a -> b) -> Objective a -> Objective b
$cfmap :: forall a b. (a -> b) -> Objective a -> Objective b
Functor)

-- | The name of the objective
objectiveName :: Objective a -> String
objectiveName :: Objective a -> String
objectiveName (Minimize          s :: String
s _)   = String
s
objectiveName (Maximize          s :: String
s _)   = String
s
objectiveName (AssertWithPenalty s :: String
s _ _) = String
s

-- | The state we keep track of as we interact with the solver
data QueryState = QueryState { QueryState -> Maybe Int -> String -> IO String
queryAsk                 :: Maybe Int -> String -> IO String
                             , QueryState -> Maybe Int -> String -> IO ()
querySend                :: Maybe Int -> String -> IO ()
                             , QueryState -> Maybe Int -> IO String
queryRetrieveResponse    :: Maybe Int -> IO String
                             , QueryState -> SMTConfig
queryConfig              :: SMTConfig
                             , QueryState -> IO ()
queryTerminate           :: IO ()
                             , QueryState -> Maybe Int
queryTimeOutValue        :: Maybe Int
                             , QueryState -> Int
queryAssertionStackDepth :: Int
                             , QueryState -> Maybe (Int, Int)
queryTblArrPreserveIndex :: Maybe (Int, Int)
                             }

-- | Computations which support query operations.
class Monad m => MonadQuery m where
  queryState :: m State

  default queryState :: (MonadTrans t, MonadQuery m', m ~ t m') => m State
  queryState = m' State -> t m' State
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m' State
forall (m :: * -> *). MonadQuery m => m State
queryState

instance MonadQuery m             => MonadQuery (ExceptT e m)
instance MonadQuery m             => MonadQuery (MaybeT m)
instance MonadQuery m             => MonadQuery (ReaderT r m)
instance MonadQuery m             => MonadQuery (SS.StateT s m)
instance MonadQuery m             => MonadQuery (LS.StateT s m)
instance (MonadQuery m, Monoid w) => MonadQuery (SW.WriterT w m)
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 { QueryT m a -> ReaderT State m a
runQueryT :: ReaderT State m a }
    deriving (Functor (QueryT m)
a -> QueryT m a
Functor (QueryT m) =>
(forall a. a -> QueryT m a)
-> (forall a b. QueryT m (a -> b) -> QueryT m a -> QueryT m b)
-> (forall a b c.
    (a -> b -> c) -> QueryT m a -> QueryT m b -> QueryT m c)
-> (forall a b. QueryT m a -> QueryT m b -> QueryT m b)
-> (forall a b. QueryT m a -> QueryT m b -> QueryT m a)
-> Applicative (QueryT m)
QueryT m a -> QueryT m b -> QueryT m b
QueryT m a -> QueryT m b -> QueryT m a
QueryT m (a -> b) -> QueryT m a -> QueryT m b
(a -> b -> c) -> QueryT m a -> QueryT m b -> QueryT m c
forall a. a -> QueryT m a
forall a b. QueryT m a -> QueryT m b -> QueryT m a
forall a b. QueryT m a -> QueryT m b -> QueryT m b
forall a b. QueryT m (a -> b) -> QueryT m a -> QueryT m b
forall a b c.
(a -> b -> c) -> QueryT m a -> QueryT m b -> QueryT m c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
forall (m :: * -> *). Applicative m => Functor (QueryT m)
forall (m :: * -> *) a. Applicative m => a -> QueryT m a
forall (m :: * -> *) a b.
Applicative m =>
QueryT m a -> QueryT m b -> QueryT m a
forall (m :: * -> *) a b.
Applicative m =>
QueryT m a -> QueryT m b -> QueryT m b
forall (m :: * -> *) a b.
Applicative m =>
QueryT m (a -> b) -> QueryT m a -> QueryT m b
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c) -> QueryT m a -> QueryT m b -> QueryT m c
<* :: QueryT m a -> QueryT m b -> QueryT m a
$c<* :: forall (m :: * -> *) a b.
Applicative m =>
QueryT m a -> QueryT m b -> QueryT m a
*> :: QueryT m a -> QueryT m b -> QueryT m b
$c*> :: forall (m :: * -> *) a b.
Applicative m =>
QueryT m a -> QueryT m b -> QueryT m b
liftA2 :: (a -> b -> c) -> QueryT m a -> QueryT m b -> QueryT m c
$cliftA2 :: forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c) -> QueryT m a -> QueryT m b -> QueryT m c
<*> :: QueryT m (a -> b) -> QueryT m a -> QueryT m b
$c<*> :: forall (m :: * -> *) a b.
Applicative m =>
QueryT m (a -> b) -> QueryT m a -> QueryT m b
pure :: a -> QueryT m a
$cpure :: forall (m :: * -> *) a. Applicative m => a -> QueryT m a
$cp1Applicative :: forall (m :: * -> *). Applicative m => Functor (QueryT m)
Applicative, a -> QueryT m b -> QueryT m a
(a -> b) -> QueryT m a -> QueryT m b
(forall a b. (a -> b) -> QueryT m a -> QueryT m b)
-> (forall a b. a -> QueryT m b -> QueryT m a)
-> Functor (QueryT m)
forall a b. a -> QueryT m b -> QueryT m a
forall a b. (a -> b) -> QueryT m a -> QueryT m b
forall (m :: * -> *) a b.
Functor m =>
a -> QueryT m b -> QueryT m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> QueryT m a -> QueryT m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> QueryT m b -> QueryT m a
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> QueryT m b -> QueryT m a
fmap :: (a -> b) -> QueryT m a -> QueryT m b
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> QueryT m a -> QueryT m b
Functor, Applicative (QueryT m)
a -> QueryT m a
Applicative (QueryT m) =>
(forall a b. QueryT m a -> (a -> QueryT m b) -> QueryT m b)
-> (forall a b. QueryT m a -> QueryT m b -> QueryT m b)
-> (forall a. a -> QueryT m a)
-> Monad (QueryT m)
QueryT m a -> (a -> QueryT m b) -> QueryT m b
QueryT m a -> QueryT m b -> QueryT m b
forall a. a -> QueryT m a
forall a b. QueryT m a -> QueryT m b -> QueryT m b
forall a b. QueryT m a -> (a -> QueryT m b) -> QueryT m b
forall (m :: * -> *). Monad m => Applicative (QueryT m)
forall (m :: * -> *) a. Monad m => a -> QueryT m a
forall (m :: * -> *) a b.
Monad m =>
QueryT m a -> QueryT m b -> QueryT m b
forall (m :: * -> *) a b.
Monad m =>
QueryT m a -> (a -> QueryT m b) -> QueryT m b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> QueryT m a
$creturn :: forall (m :: * -> *) a. Monad m => a -> QueryT m a
>> :: QueryT m a -> QueryT m b -> QueryT m b
$c>> :: forall (m :: * -> *) a b.
Monad m =>
QueryT m a -> QueryT m b -> QueryT m b
>>= :: QueryT m a -> (a -> QueryT m b) -> QueryT m b
$c>>= :: forall (m :: * -> *) a b.
Monad m =>
QueryT m a -> (a -> QueryT m b) -> QueryT m b
$cp1Monad :: forall (m :: * -> *). Monad m => Applicative (QueryT m)
Monad, Monad (QueryT m)
Monad (QueryT m) =>
(forall a. IO a -> QueryT m a) -> MonadIO (QueryT m)
IO a -> QueryT m a
forall a. IO a -> QueryT m a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> MonadIO m
forall (m :: * -> *). MonadIO m => Monad (QueryT m)
forall (m :: * -> *) a. MonadIO m => IO a -> QueryT m a
liftIO :: IO a -> QueryT m a
$cliftIO :: forall (m :: * -> *) a. MonadIO m => IO a -> QueryT m a
$cp1MonadIO :: forall (m :: * -> *). MonadIO m => Monad (QueryT m)
MonadIO, m a -> QueryT m a
(forall (m :: * -> *) a. Monad m => m a -> QueryT m a)
-> MonadTrans QueryT
forall (m :: * -> *) a. Monad m => m a -> QueryT m a
forall (t :: (* -> *) -> * -> *).
(forall (m :: * -> *) a. Monad m => m a -> t m a) -> MonadTrans t
lift :: m a -> QueryT m a
$clift :: forall (m :: * -> *) a. Monad m => m a -> QueryT m a
MonadTrans,
              MonadError e, MonadState s, MonadWriter w)

instance Monad m => MonadQuery (QueryT m) where
  queryState :: QueryT m State
queryState = ReaderT State m State -> QueryT m State
forall (m :: * -> *) a. ReaderT State m a -> QueryT m a
QueryT ReaderT State m State
forall r (m :: * -> *). MonadReader r m => m r
ask

mapQueryT :: (ReaderT State m a -> ReaderT State n b) -> QueryT m a -> QueryT n b
mapQueryT :: (ReaderT State m a -> ReaderT State n b)
-> QueryT m a -> QueryT n b
mapQueryT f :: ReaderT State m a -> ReaderT State n b
f = ReaderT State n b -> QueryT n b
forall (m :: * -> *) a. ReaderT State m a -> QueryT m a
QueryT (ReaderT State n b -> QueryT n b)
-> (QueryT m a -> ReaderT State n b) -> QueryT m a -> QueryT n b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReaderT State m a -> ReaderT State n b
f (ReaderT State m a -> ReaderT State n b)
-> (QueryT m a -> ReaderT State m a)
-> QueryT m a
-> ReaderT State n b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QueryT m a -> ReaderT State m a
forall (m :: * -> *) a. QueryT m a -> ReaderT State m a
runQueryT
{-# INLINE mapQueryT #-}

-- | Create a fresh variable of some type in the underlying query monad transformer.
-- For further control on how these variables are projected and embedded, see the
-- 'Queriable' class.
class Fresh m a where
  fresh :: QueryT m a

-- | An queriable value. This is a generalization of the 'Fresh' class, in case one needs
-- to be more specific about how projections/embeddings are done.
class Queriable m a b | a -> b where
  -- | ^ Create a new symbolic value of type @a@
  create  :: QueryT m a
  -- | ^ Extract the current value in a SAT context
  project :: a -> QueryT m b
  -- | ^ Create a literal value. Morally, 'embed' and 'project' are inverses of each other
  -- via the 'QueryT' monad transformer.
  embed   :: b -> QueryT m a

-- Have to define this one by hand, because we use ReaderT in the implementation
instance MonadReader r m => MonadReader r (QueryT m) where
  ask :: QueryT m r
ask = m r -> QueryT m r
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m r
forall r (m :: * -> *). MonadReader r m => m r
ask
  local :: (r -> r) -> QueryT m a -> QueryT m a
local f :: r -> r
f = (ReaderT State m a -> ReaderT State m a)
-> QueryT m a -> QueryT m a
forall (m :: * -> *) a (n :: * -> *) b.
(ReaderT State m a -> ReaderT State n b)
-> QueryT m a -> QueryT n b
mapQueryT ((ReaderT State m a -> ReaderT State m a)
 -> QueryT m a -> QueryT m a)
-> (ReaderT State m a -> ReaderT State m a)
-> QueryT m a
-> QueryT m a
forall a b. (a -> b) -> a -> b
$ (m a -> m a) -> ReaderT State m a -> ReaderT State m a
forall (m :: * -> *) a (n :: * -> *) b r.
(m a -> n b) -> ReaderT r m a -> ReaderT r n b
mapReaderT ((m a -> m a) -> ReaderT State m a -> ReaderT State m a)
-> (m a -> m a) -> ReaderT State m a -> ReaderT State m a
forall a b. (a -> b) -> a -> b
$ (r -> r) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local r -> r
f

-- | A query is a user-guided mechanism to directly communicate and extract
-- results from the solver.
type Query = QueryT IO

instance MonadSymbolic Query where
   symbolicEnv :: Query State
symbolicEnv = Query State
forall (m :: * -> *). MonadQuery m => m State
queryState

instance NFData OptimizeStyle where
   rnf :: OptimizeStyle -> ()
rnf x :: OptimizeStyle
x = OptimizeStyle
x OptimizeStyle -> () -> ()
forall a b. a -> b -> b
`seq` ()

instance NFData Penalty where
   rnf :: Penalty -> ()
rnf DefaultPenalty  = ()
   rnf (Penalty p :: Rational
p mbs :: Maybe String
mbs) = Rational -> ()
forall a. NFData a => a -> ()
rnf Rational
p () -> () -> ()
forall a b. a -> b -> b
`seq` Maybe String -> ()
forall a. NFData a => a -> ()
rnf Maybe String
mbs

instance NFData a => NFData (Objective a) where
   rnf :: Objective a -> ()
rnf (Minimize          s :: String
s a :: a
a)   = String -> ()
forall a. NFData a => a -> ()
rnf String
s () -> () -> ()
forall a b. a -> b -> b
`seq` a -> ()
forall a. NFData a => a -> ()
rnf a
a
   rnf (Maximize          s :: String
s a :: a
a)   = String -> ()
forall a. NFData a => a -> ()
rnf String
s () -> () -> ()
forall a b. a -> b -> b
`seq` a -> ()
forall a. NFData a => a -> ()
rnf a
a
   rnf (AssertWithPenalty s :: String
s a :: a
a p :: Penalty
p) = String -> ()
forall a. NFData a => a -> ()
rnf String
s () -> () -> ()
forall a b. a -> b -> b
`seq` a -> ()
forall a. NFData a => a -> ()
rnf a
a () -> () -> ()
forall a b. a -> b -> b
`seq` Penalty -> ()
forall a. NFData a => a -> ()
rnf Penalty
p

-- | Result of running a symbolic computation
data Result = Result { Result -> Set Kind
reskinds       :: Set.Set Kind                                 -- ^ kinds used in the program
                     , Result -> [(String, CV)]
resTraces      :: [(String, CV)]                               -- ^ quick-check counter-example information (if any)
                     , Result -> [(String, CV -> Bool, SV)]
resObservables :: [(String, CV -> Bool, SV)]                   -- ^ observable expressions (part of the model)
                     , Result -> [(String, [String])]
resUISegs      :: [(String, [String])]                         -- ^ uninterpeted code segments
                     , Result -> ([(Quantifier, NamedSymVar)], [NamedSymVar])
resInputs      :: ([(Quantifier, NamedSymVar)], [NamedSymVar]) -- ^ inputs (possibly existential) + tracker vars
                     , Result -> [(SV, CV)]
resConsts      :: [(SV, CV)]                                   -- ^ constants
                     , Result -> [((Int, Kind, Kind), [SV])]
resTables      :: [((Int, Kind, Kind), [SV])]                  -- ^ tables (automatically constructed) (tableno, index-type, result-type) elts
                     , Result -> [(Int, ArrayInfo)]
resArrays      :: [(Int, ArrayInfo)]                           -- ^ arrays (user specified)
                     , Result -> [(String, SBVType)]
resUIConsts    :: [(String, SBVType)]                          -- ^ uninterpreted constants
                     , Result -> [(String, [String])]
resAxioms      :: [(String, [String])]                         -- ^ axioms
                     , Result -> SBVPgm
resAsgns       :: SBVPgm                                       -- ^ assignments
                     , Result -> Seq (Bool, [(String, String)], SV)
resConstraints :: S.Seq (Bool, [(String, String)], SV)         -- ^ additional constraints (boolean)
                     , Result -> [(String, Maybe CallStack, SV)]
resAssertions  :: [(String, Maybe CallStack, SV)]              -- ^ assertions
                     , Result -> [SV]
resOutputs     :: [SV]                                         -- ^ outputs
                     }

-- Show instance for 'Result'. Only for debugging purposes.
instance Show Result where
  -- If there's nothing interesting going on, just print the constant. Note that the
  -- definiton of interesting here is rather subjective; but essentially if we reduced
  -- the result to a single constant already, without any reference to anything.
  show :: Result -> String
show Result{resConsts :: Result -> [(SV, CV)]
resConsts=[(SV, CV)]
cs, resOutputs :: Result -> [SV]
resOutputs=[r :: SV
r]}
    | Just c :: CV
c <- SV
r SV -> [(SV, CV)] -> Maybe CV
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(SV, CV)]
cs
    = CV -> String
forall a. Show a => a -> String
show CV
c
  show (Result kinds :: Set Kind
kinds _ _ cgs :: [(String, [String])]
cgs is :: ([(Quantifier, NamedSymVar)], [NamedSymVar])
is cs :: [(SV, CV)]
cs ts :: [((Int, Kind, Kind), [SV])]
ts as :: [(Int, ArrayInfo)]
as uis :: [(String, SBVType)]
uis axs :: [(String, [String])]
axs xs :: SBVPgm
xs cstrs :: Seq (Bool, [(String, String)], SV)
cstrs asserts :: [(String, Maybe CallStack, SV)]
asserts os :: [SV]
os) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
                   (if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
usorts then [] else "SORTS" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ("  " String -> ShowS
forall a. [a] -> [a] -> [a]
++) [String]
usorts)
                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["INPUTS"]
                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((Quantifier, NamedSymVar) -> String)
-> [(Quantifier, NamedSymVar)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Quantifier, NamedSymVar) -> String
shn (([(Quantifier, NamedSymVar)], [NamedSymVar])
-> [(Quantifier, NamedSymVar)]
forall a b. (a, b) -> a
fst ([(Quantifier, NamedSymVar)], [NamedSymVar])
is)
                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (if [NamedSymVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (([(Quantifier, NamedSymVar)], [NamedSymVar]) -> [NamedSymVar]
forall a b. (a, b) -> b
snd ([(Quantifier, NamedSymVar)], [NamedSymVar])
is) then [] else "TRACKER VARS" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (NamedSymVar -> String) -> [NamedSymVar] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((Quantifier, NamedSymVar) -> String
shn ((Quantifier, NamedSymVar) -> String)
-> (NamedSymVar -> (Quantifier, NamedSymVar))
-> NamedSymVar
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Quantifier
EX,)) (([(Quantifier, NamedSymVar)], [NamedSymVar]) -> [NamedSymVar]
forall a b. (a, b) -> b
snd ([(Quantifier, NamedSymVar)], [NamedSymVar])
is))
                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["CONSTANTS"]
                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((SV, CV) -> [String]) -> [(SV, CV)] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SV, CV) -> [String]
forall a. Show a => (SV, a) -> [String]
shc [(SV, CV)]
cs
                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["TABLES"]
                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (((Int, Kind, Kind), [SV]) -> String)
-> [((Int, Kind, Kind), [SV])] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((Int, Kind, Kind), [SV]) -> String
forall a a a a.
(Show a, Show a, Show a, Show a) =>
((a, a, a), a) -> String
sht [((Int, Kind, Kind), [SV])]
ts
                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["ARRAYS"]
                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((Int, ArrayInfo) -> String) -> [(Int, ArrayInfo)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Int, ArrayInfo) -> String
forall a a a a.
(Show a, Show a, Show a, Show a) =>
(a, (String, (a, a), a)) -> String
sha [(Int, ArrayInfo)]
as
                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["UNINTERPRETED CONSTANTS"]
                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((String, SBVType) -> String) -> [(String, SBVType)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, SBVType) -> String
forall a. Show a => (String, a) -> String
shui [(String, SBVType)]
uis
                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["USER GIVEN CODE SEGMENTS"]
                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((String, [String]) -> [String])
-> [(String, [String])] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (String, [String]) -> [String]
shcg [(String, [String])]
cgs
                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["AXIOMS"]
                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((String, [String]) -> String) -> [(String, [String])] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, [String]) -> String
shax [(String, [String])]
axs
                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["DEFINE"]
                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((SV, SBVExpr) -> String) -> [(SV, SBVExpr)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\(s :: SV
s, e :: SBVExpr
e) -> "  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SV -> String
shs SV
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ " = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SBVExpr -> String
forall a. Show a => a -> String
show SBVExpr
e) (Seq (SV, SBVExpr) -> [(SV, SBVExpr)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList (SBVPgm -> Seq (SV, SBVExpr)
pgmAssignments SBVPgm
xs))
                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["CONSTRAINTS"]
                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((Bool, [(String, String)], SV) -> String)
-> [(Bool, [(String, String)], SV)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (("  " String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS
-> ((Bool, [(String, String)], SV) -> String)
-> (Bool, [(String, String)], SV)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool, [(String, String)], SV) -> String
forall a. Show a => (Bool, [(String, String)], a) -> String
shCstr) (Seq (Bool, [(String, String)], SV)
-> [(Bool, [(String, String)], SV)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (Bool, [(String, String)], SV)
cstrs)
                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["ASSERTIONS"]
                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((String, Maybe CallStack, SV) -> String)
-> [(String, Maybe CallStack, SV)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (("  "String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS
-> ((String, Maybe CallStack, SV) -> String)
-> (String, Maybe CallStack, SV)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, Maybe CallStack, SV) -> String
forall a. Show a => (String, Maybe CallStack, a) -> String
shAssert) [(String, Maybe CallStack, SV)]
asserts
                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["OUTPUTS"]
                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [SV] -> [String]
forall a. Show a => [a] -> [String]
sh2 [SV]
os
    where sh2 :: Show a => [a] -> [String]
          sh2 :: [a] -> [String]
sh2 = (a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (("  "String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> (a -> String) -> a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> String
forall a. Show a => a -> String
show)

          usorts :: [String]
usorts = [String -> Either String [String] -> String
forall a. String -> Either a [String] -> String
sh String
s Either String [String]
t | KUninterpreted s :: String
s t :: Either String [String]
t <- Set Kind -> [Kind]
forall a. Set a -> [a]
Set.toList Set Kind
kinds]
                   where sh :: String -> Either a [String] -> String
sh s :: String
s (Left   _) = String
s
                         sh s :: String
s (Right es :: [String]
es) = String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ " (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " [String]
es String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"

          shs :: SV -> String
shs sv :: SV
sv = SV -> String
forall a. Show a => a -> String
show SV
sv String -> ShowS
forall a. [a] -> [a] -> [a]
++ " :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show (SV -> Kind
swKind SV
sv)

          sht :: ((a, a, a), a) -> String
sht ((i :: a
i, at :: a
at, rt :: a
rt), es :: a
es)  = "  Table " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ " : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
at String -> ShowS
forall a. [a] -> [a] -> [a]
++ "->" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
rt String -> ShowS
forall a. [a] -> [a] -> [a]
++ " = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
es

          shc :: (SV, a) -> [String]
shc (sv :: SV
sv, cv :: a
cv)
            | SV
sv SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
falseSV Bool -> Bool -> Bool
|| SV
sv SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
trueSV
            = []
            | Bool
True
            = ["  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
sv String -> ShowS
forall a. [a] -> [a] -> [a]
++ " = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
cv]

          shcg :: (String, [String]) -> [String]
shcg (s :: String
s, ss :: [String]
ss) = ("Variable: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ("  " String -> ShowS
forall a. [a] -> [a] -> [a]
++) [String]
ss

          shn :: (Quantifier, NamedSymVar) -> String
shn (q :: Quantifier
q, (sv :: SV
sv, nm :: String
nm)) = "  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
ni String -> ShowS
forall a. [a] -> [a] -> [a]
++ " :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show (SV -> Kind
swKind SV
sv) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
ex String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
alias
            where ni :: String
ni = SV -> String
forall a. Show a => a -> String
show SV
sv
                  ex :: String
ex | Quantifier
q Quantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
== Quantifier
ALL = ""
                     | Bool
True     = ", existential"
                  alias :: String
alias | String
ni String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
nm = ""
                        | Bool
True     = ", aliasing " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
nm

          sha :: (a, (String, (a, a), a)) -> String
sha (i :: a
i, (nm :: String
nm, (ai :: a
ai, bi :: a
bi), ctx :: a
ctx)) = "  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
ni String -> ShowS
forall a. [a] -> [a] -> [a]
++ " :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
ai String -> ShowS
forall a. [a] -> [a] -> [a]
++ " -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
bi String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
alias
                                       String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n     Context: "     String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
ctx
            where ni :: String
ni = "array_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i
                  alias :: String
alias | String
ni String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
nm = ""
                        | Bool
True     = ", aliasing " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
nm

          shui :: (String, a) -> String
shui (nm :: String
nm, t :: a
t) = "  [uninterpreted] " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ " :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
t

          shax :: (String, [String]) -> String
shax (nm :: String
nm, ss :: [String]
ss) = "  -- user defined axiom: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n  " [String]
ss

          shCstr :: (Bool, [(String, String)], a) -> String
shCstr (isSoft :: Bool
isSoft, [], c :: a
c)               = Bool -> String
soft Bool
isSoft String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
c
          shCstr (isSoft :: Bool
isSoft, [(":named", nm :: String
nm)], c :: a
c) = Bool -> String
soft Bool
isSoft String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ ": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
c
          shCstr (isSoft :: Bool
isSoft, attrs :: [(String, String)]
attrs, c :: a
c)            = Bool -> String
soft Bool
isSoft String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ " (attributes: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(String, String)] -> String
forall a. Show a => a -> String
show [(String, String)]
attrs String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"

          soft :: Bool -> String
soft True  = "[SOFT] "
          soft False = ""

          shAssert :: (String, Maybe CallStack, a) -> String
shAssert (nm :: String
nm, stk :: Maybe CallStack
stk, p :: a
p) = "  -- assertion: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> (CallStack -> String) -> Maybe CallStack -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "[No location]"
#if MIN_VERSION_base(4,9,0)
                CallStack -> String
prettyCallStack
#else
                showCallStack
#endif
                Maybe CallStack
stk String -> ShowS
forall a. [a] -> [a] -> [a]
++ ": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
p

-- | The context of a symbolic array as created
data ArrayContext = ArrayFree (Maybe SV)                   -- ^ A new array, the contents are initialized with the given value, if any
                  | ArrayMutate ArrayIndex SV SV           -- ^ An array created by mutating another array at a given cell
                  | ArrayMerge  SV ArrayIndex ArrayIndex   -- ^ An array created by symbolically merging two other arrays

instance Show ArrayContext where
  show :: ArrayContext -> String
show (ArrayFree Nothing)   = " initialized with random elements"
  show (ArrayFree (Just sv :: SV
sv)) = " initialized with " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
sv
  show (ArrayMutate i :: ArrayIndex
i a :: SV
a b :: SV
b)   = " cloned from array_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ ArrayIndex -> String
forall a. Show a => a -> String
show ArrayIndex
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ " with " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
a String -> ShowS
forall a. [a] -> [a] -> [a]
++ " :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show (SV -> Kind
swKind SV
a) String -> ShowS
forall a. [a] -> [a] -> [a]
++ " |-> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ " :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show (SV -> Kind
swKind SV
b)
  show (ArrayMerge  s :: SV
s i :: ArrayIndex
i j :: ArrayIndex
j)   = " merged arrays " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ArrayIndex -> String
forall a. Show a => a -> String
show ArrayIndex
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ " and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ArrayIndex -> String
forall a. Show a => a -> String
show ArrayIndex
j String -> ShowS
forall a. [a] -> [a] -> [a]
++ " on condition " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
s

-- | Expression map, used for hash-consing
type ExprMap = Map.Map SBVExpr SV

-- | Constants are stored in a map, for hash-consing.
type CnstMap = Map.Map CV SV

-- | Kinds used in the program; used for determining the final SMT-Lib logic to pick
type KindSet = Set.Set Kind

-- | Tables generated during a symbolic run
type TableMap = Map.Map (Kind, Kind, [SV]) Int

-- | Representation for symbolic arrays
type ArrayInfo = (String, (Kind, Kind), ArrayContext)

-- | SMT Arrays generated during a symbolic run
type ArrayMap  = IMap.IntMap ArrayInfo

-- | Functional Arrays generated during a symbolic run
type FArrayMap  = IMap.IntMap (SVal -> SVal, IORef (IMap.IntMap SV))

-- | Uninterpreted-constants generated during a symbolic run
type UIMap     = Map.Map String SBVType

-- | Code-segments for Uninterpreted-constants, as given by the user
type CgMap     = Map.Map String [String]

-- | Cached values, implementing sharing
type Cache a   = IMap.IntMap [(StableName (State -> IO a), a)]

-- | Stage of an interactive run
data IStage = ISetup        -- Before we initiate contact.
            | ISafe         -- In the context of a safe/safeWith call
            | IRun          -- After the contact is started

-- | Are we cecking safety
isSafetyCheckingIStage :: IStage -> Bool
isSafetyCheckingIStage :: IStage -> Bool
isSafetyCheckingIStage s :: IStage
s = case IStage
s of
                             ISetup -> Bool
False
                             ISafe  -> Bool
True
                             IRun   -> Bool
False

-- | Are we in setup?
isSetupIStage :: IStage -> Bool
isSetupIStage :: IStage -> Bool
isSetupIStage s :: IStage
s = case IStage
s of
                   ISetup -> Bool
True
                   ISafe  -> Bool
False
                   IRun   -> Bool
True

-- | Are we in a run?
isRunIStage :: IStage -> Bool
isRunIStage :: IStage -> Bool
isRunIStage s :: IStage
s = case IStage
s of
                  ISetup -> Bool
False
                  ISafe  -> Bool
False
                  IRun   -> Bool
True

-- | Different means of running a symbolic piece of code
data SBVRunMode = SMTMode QueryContext IStage Bool SMTConfig                        -- ^ In regular mode, with a stage. Bool is True if this is SAT.
                | CodeGen                                                           -- ^ Code generation mode.
                | Concrete (Maybe (Bool, [((Quantifier, NamedSymVar), Maybe CV)]))  -- ^ Concrete simulation mode, with given environment if any. If Nothing: Random.

-- Show instance for SBVRunMode; debugging purposes only
instance Show SBVRunMode where
   show :: SBVRunMode -> String
show (SMTMode qc :: QueryContext
qc ISetup True  _)  = "Satisfiability setup (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ QueryContext -> String
forall a. Show a => a -> String
show QueryContext
qc String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
   show (SMTMode qc :: QueryContext
qc ISafe  True  _)  = "Safety setup (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ QueryContext -> String
forall a. Show a => a -> String
show QueryContext
qc String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
   show (SMTMode qc :: QueryContext
qc IRun   True  _)  = "Satisfiability (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ QueryContext -> String
forall a. Show a => a -> String
show QueryContext
qc String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
   show (SMTMode qc :: QueryContext
qc ISetup False _)  = "Proof setup (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ QueryContext -> String
forall a. Show a => a -> String
show QueryContext
qc String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
   show (SMTMode qc :: QueryContext
qc ISafe  False _)  = ShowS
forall a. HasCallStack => String -> a
error ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ "ISafe-False is not an expected/supported combination for SBVRunMode! (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ QueryContext -> String
forall a. Show a => a -> String
show QueryContext
qc String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
   show (SMTMode qc :: QueryContext
qc IRun   False _)  = "Proof (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ QueryContext -> String
forall a. Show a => a -> String
show QueryContext
qc String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"
   show CodeGen                      = "Code generation"
   show (Concrete Nothing)           = "Concrete evaluation with random values"
   show (Concrete (Just (True, _)))  = "Concrete evaluation during model validation for sat"
   show (Concrete (Just (False, _))) = "Concrete evaluation during model validation for prove"

-- | Is this a CodeGen run? (i.e., generating code)
isCodeGenMode :: State -> IO Bool
isCodeGenMode :: State -> IO Bool
isCodeGenMode State{IORef SBVRunMode
runMode :: State -> IORef SBVRunMode
runMode :: IORef SBVRunMode
runMode} = do SBVRunMode
rm <- IORef SBVRunMode -> IO SBVRunMode
forall a. IORef a -> IO a
readIORef IORef SBVRunMode
runMode
                                  Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ case SBVRunMode
rm of
                                             Concrete{} -> Bool
False
                                             SMTMode{}  -> Bool
False
                                             CodeGen    -> Bool
True

-- | The state in query mode, i.e., additional context
data IncState = IncState { IncState -> IORef [NamedSymVar]
rNewInps        :: IORef [NamedSymVar]   -- always existential!
                         , IncState -> IORef (Set Kind)
rNewKinds       :: IORef KindSet
                         , IncState -> IORef CnstMap
rNewConsts      :: IORef CnstMap
                         , IncState -> IORef ArrayMap
rNewArrs        :: IORef ArrayMap
                         , IncState -> IORef TableMap
rNewTbls        :: IORef TableMap
                         , IncState -> IORef UIMap
rNewUIs         :: IORef UIMap
                         , IncState -> IORef SBVPgm
rNewAsgns       :: IORef SBVPgm
                         , IncState -> IORef (Seq (Bool, [(String, String)], SV))
rNewConstraints :: IORef (S.Seq (Bool, [(String, String)], SV))
                         }

-- | Get a new IncState
newIncState :: IO IncState
newIncState :: IO IncState
newIncState = do
        IORef [NamedSymVar]
is    <- [NamedSymVar] -> IO (IORef [NamedSymVar])
forall a. a -> IO (IORef a)
newIORef []
        IORef (Set Kind)
ks    <- Set Kind -> IO (IORef (Set Kind))
forall a. a -> IO (IORef a)
newIORef Set Kind
forall a. Set a
Set.empty
        IORef CnstMap
nc    <- CnstMap -> IO (IORef CnstMap)
forall a. a -> IO (IORef a)
newIORef CnstMap
forall k a. Map k a
Map.empty
        IORef ArrayMap
am    <- ArrayMap -> IO (IORef ArrayMap)
forall a. a -> IO (IORef a)
newIORef ArrayMap
forall a. IntMap a
IMap.empty
        IORef TableMap
tm    <- TableMap -> IO (IORef TableMap)
forall a. a -> IO (IORef a)
newIORef TableMap
forall k a. Map k a
Map.empty
        IORef UIMap
ui    <- UIMap -> IO (IORef UIMap)
forall a. a -> IO (IORef a)
newIORef UIMap
forall k a. Map k a
Map.empty
        IORef SBVPgm
pgm   <- SBVPgm -> IO (IORef SBVPgm)
forall a. a -> IO (IORef a)
newIORef (Seq (SV, SBVExpr) -> SBVPgm
SBVPgm Seq (SV, SBVExpr)
forall a. Seq a
S.empty)
        IORef (Seq (Bool, [(String, String)], SV))
cstrs <- Seq (Bool, [(String, String)], SV)
-> IO (IORef (Seq (Bool, [(String, String)], SV)))
forall a. a -> IO (IORef a)
newIORef Seq (Bool, [(String, String)], SV)
forall a. Seq a
S.empty
        IncState -> IO IncState
forall (m :: * -> *) a. Monad m => a -> m a
return IncState :: IORef [NamedSymVar]
-> IORef (Set Kind)
-> IORef CnstMap
-> IORef ArrayMap
-> IORef TableMap
-> IORef UIMap
-> IORef SBVPgm
-> IORef (Seq (Bool, [(String, String)], SV))
-> IncState
IncState { rNewInps :: IORef [NamedSymVar]
rNewInps        = IORef [NamedSymVar]
is
                        , rNewKinds :: IORef (Set Kind)
rNewKinds       = IORef (Set Kind)
ks
                        , rNewConsts :: IORef CnstMap
rNewConsts      = IORef CnstMap
nc
                        , rNewArrs :: IORef ArrayMap
rNewArrs        = IORef ArrayMap
am
                        , rNewTbls :: IORef TableMap
rNewTbls        = IORef TableMap
tm
                        , rNewUIs :: IORef UIMap
rNewUIs         = IORef UIMap
ui
                        , rNewAsgns :: IORef SBVPgm
rNewAsgns       = IORef SBVPgm
pgm
                        , rNewConstraints :: IORef (Seq (Bool, [(String, String)], SV))
rNewConstraints = IORef (Seq (Bool, [(String, String)], SV))
cstrs
                        }

-- | Get a new IncState
withNewIncState :: State -> (State -> IO a) -> IO (IncState, a)
withNewIncState :: State -> (State -> IO a) -> IO (IncState, a)
withNewIncState st :: State
st cont :: State -> IO a
cont = do
        IncState
is <- IO IncState
newIncState
        IORef IncState -> (IncState -> IncState) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
R.modifyIORef' (State -> IORef IncState
rIncState State
st) (IncState -> IncState -> IncState
forall a b. a -> b -> a
const IncState
is)
        a
r  <- State -> IO a
cont State
st
        IncState
finalIncState <- IORef IncState -> IO IncState
forall a. IORef a -> IO a
readIORef (State -> IORef IncState
rIncState State
st)
        (IncState, a) -> IO (IncState, a)
forall (m :: * -> *) a. Monad m => a -> m a
return (IncState
finalIncState, a
r)

-- | The state of the symbolic interpreter
data State  = State { State -> SVal
pathCond     :: SVal                             -- ^ kind KBool
                    , State -> UTCTime
startTime    :: UTCTime
                    , State -> IORef SBVRunMode
runMode      :: IORef SBVRunMode
                    , State -> IORef IncState
rIncState    :: IORef IncState
                    , State -> IORef [(String, CV)]
rCInfo       :: IORef [(String, CV)]
                    , State -> IORef [(String, CV -> Bool, SV)]
rObservables :: IORef [(String, CV -> Bool, SV)]
                    , State -> IORef Int
rctr         :: IORef Int
                    , State -> IORef (Set Kind)
rUsedKinds   :: IORef KindSet
                    , State -> IORef (Set String)
rUsedLbls    :: IORef (Set.Set String)
                    , State
-> IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
rinps        :: IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set.Set String) -- First : User defined, with proper quantifiers
                                                                                                           -- Second: Internally declared, always existential
                                                                                                           -- Third : Entire set of names, for faster lookup
                    , State -> IORef (Seq (Bool, [(String, String)], SV))
rConstraints :: IORef (S.Seq (Bool, [(String, String)], SV))
                    , State -> IORef [SV]
routs        :: IORef [SV]
                    , State -> IORef TableMap
rtblMap      :: IORef TableMap
                    , State -> IORef SBVPgm
spgm         :: IORef SBVPgm
                    , State -> IORef CnstMap
rconstMap    :: IORef CnstMap
                    , State -> IORef ExprMap
rexprMap     :: IORef ExprMap
                    , State -> IORef ArrayMap
rArrayMap    :: IORef ArrayMap
                    , State -> IORef FArrayMap
rFArrayMap   :: IORef FArrayMap
                    , State -> IORef UIMap
rUIMap       :: IORef UIMap
                    , State -> IORef CgMap
rCgMap       :: IORef CgMap
                    , State -> IORef [(String, [String])]
raxioms      :: IORef [(String, [String])]
                    , State -> IORef [SMTOption]
rSMTOptions  :: IORef [SMTOption]
                    , State -> IORef [Objective (SV, SV)]
rOptGoals    :: IORef [Objective (SV, SV)]
                    , State -> IORef [(String, Maybe CallStack, SV)]
rAsserts     :: IORef [(String, Maybe CallStack, SV)]
                    , State -> IORef (Cache SV)
rSVCache     :: IORef (Cache SV)
                    , State -> IORef (Cache ArrayIndex)
rAICache     :: IORef (Cache ArrayIndex)
                    , State -> IORef (Cache FArrayIndex)
rFAICache    :: IORef (Cache FArrayIndex)
                    , State -> IORef (Maybe QueryState)
rQueryState  :: IORef (Maybe QueryState)
                    }

-- NFData is a bit of a lie, but it's sufficient, most of the content is iorefs that we don't want to touch
instance NFData State where
   rnf :: State -> ()
rnf State{} = ()

-- | Get the current path condition
getSValPathCondition :: State -> SVal
getSValPathCondition :: State -> SVal
getSValPathCondition = State -> SVal
pathCond

-- | Extend the path condition with the given test value.
extendSValPathCondition :: State -> (SVal -> SVal) -> State
extendSValPathCondition :: State -> (SVal -> SVal) -> State
extendSValPathCondition st :: State
st f :: SVal -> SVal
f = State
st{pathCond :: SVal
pathCond = SVal -> SVal
f (State -> SVal
pathCond State
st)}

-- | Are we running in proof mode?
inSMTMode :: State -> IO Bool
inSMTMode :: State -> IO Bool
inSMTMode State{IORef SBVRunMode
runMode :: IORef SBVRunMode
runMode :: State -> IORef SBVRunMode
runMode} = do SBVRunMode
rm <- IORef SBVRunMode -> IO SBVRunMode
forall a. IORef a -> IO a
readIORef IORef SBVRunMode
runMode
                              Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> IO Bool) -> Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ case SBVRunMode
rm of
                                         CodeGen    -> Bool
False
                                         Concrete{} -> Bool
False
                                         SMTMode{}  -> Bool
True

-- | The "Symbolic" value. Either a constant (@Left@) or a symbolic
-- value (@Right Cached@). Note that caching is essential for making
-- sure sharing is preserved.
data SVal = SVal !Kind !(Either CV (Cached SV))

instance HasKind SVal where
  kindOf :: SVal -> Kind
kindOf (SVal k :: Kind
k _) = Kind
k

-- Show instance for 'SVal'. Not particularly "desirable", but will do if needed
-- NB. We do not show the type info on constant KBool values, since there's no
-- implicit "fromBoolean" applied to Booleans in Haskell; and thus a statement
-- of the form "True :: SBool" is just meaningless. (There should be a fromBoolean!)
instance Show SVal where
  show :: SVal -> String
show (SVal KBool (Left c :: CV
c))  = Bool -> CV -> String
showCV Bool
False CV
c
  show (SVal k :: Kind
k     (Left c :: CV
c))  = Bool -> CV -> String
showCV Bool
False CV
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ " :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k
  show (SVal k :: Kind
k     (Right _)) =         "<symbolic> :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k

-- We really don't want an 'Eq' instance for 'SBV' or 'SVal'. As it really makes no sense.
-- But since we do want the 'Bits' instance, we're forced to define equality. See
-- <http://github.com/LeventErkok/sbv/issues/301>. We simply error out.
-- | This instance is only defined so that we can define an instance for
-- 'Data.Bits.Bits'. '==' and '/=' simply throw an error.
instance Eq SVal where
  a :: SVal
a == :: SVal -> SVal -> Bool
== b :: SVal
b = String -> String -> (String, String) -> Bool
forall a. String -> String -> (String, String) -> a
noEquals "==" ".==" (SVal -> String
forall a. Show a => a -> String
show SVal
a, SVal -> String
forall a. Show a => a -> String
show SVal
b)
  a :: SVal
a /= :: SVal -> SVal -> Bool
/= b :: SVal
b = String -> String -> (String, String) -> Bool
forall a. String -> String -> (String, String) -> a
noEquals "/=" "./=" (SVal -> String
forall a. Show a => a -> String
show SVal
a, SVal -> String
forall a. Show a => a -> String
show SVal
b)

-- Bail out nicely.
noEquals :: String -> String -> (String, String) -> a
noEquals :: String -> String -> (String, String) -> a
noEquals o :: String
o n :: String
n (l :: String
l, r :: String
r) = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ ""
                                      , "*** Data.SBV: Comparing symbolic values using Haskell's Eq class!"
                                      , "***"
                                      , "*** Received:    " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ "  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
o String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
r
                                      , "*** Instead use: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ " "  String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
r
                                      , "***"
                                      , "*** The Eq instance for symbolic values are necessiated only because"
                                      , "*** of the Bits class requirement. You must use symbolic equality"
                                      , "*** operators instead. (And complain to Haskell folks that they"
                                      , "*** remove the 'Eq' superclass from 'Bits'!.)"
                                      ]

-- | Things we do not support in interactive mode, at least for now!
noInteractive :: [String] -> a
noInteractive :: [String] -> a
noInteractive ss :: [String]
ss = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$  ""
                                   String -> [String] -> [String]
forall a. a -> [a] -> [a]
:  "*** Data.SBV: Unsupported interactive/query mode feature."
                                   String -> [String] -> [String]
forall a. a -> [a] -> [a]
:  ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ("***  " String -> ShowS
forall a. [a] -> [a] -> [a]
++) [String]
ss
                                   [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["*** Data.SBV: Please report this as a feature request!"]

-- | Modification of the state, but carefully handling the interactive tasks.
-- Note that the state is always updated regardless of the mode, but we get
-- to also perform extra operation in interactive mode. (Typically error out, but also simply
-- ignore if it has no impact.)
modifyState :: State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState :: State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState st :: State
st@State{IORef SBVRunMode
runMode :: IORef SBVRunMode
runMode :: State -> IORef SBVRunMode
runMode} field :: State -> IORef a
field update :: a -> a
update interactiveUpdate :: IO ()
interactiveUpdate = do
        IORef a -> (a -> a) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
R.modifyIORef' (State -> IORef a
field State
st) a -> a
update
        SBVRunMode
rm <- IORef SBVRunMode -> IO SBVRunMode
forall a. IORef a -> IO a
readIORef IORef SBVRunMode
runMode
        case SBVRunMode
rm of
          SMTMode _ IRun _ _ -> IO ()
interactiveUpdate
          _                  -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | Modify the incremental state
modifyIncState  :: State -> (IncState -> IORef a) -> (a -> a) -> IO ()
modifyIncState :: State -> (IncState -> IORef a) -> (a -> a) -> IO ()
modifyIncState State{IORef IncState
rIncState :: IORef IncState
rIncState :: State -> IORef IncState
rIncState} field :: IncState -> IORef a
field update :: a -> a
update = do
        IncState
incState <- IORef IncState -> IO IncState
forall a. IORef a -> IO a
readIORef IORef IncState
rIncState
        IORef a -> (a -> a) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
R.modifyIORef' (IncState -> IORef a
field IncState
incState) a -> a
update

-- | Add an observable
recordObservable :: State -> String -> (CV -> Bool) -> SV -> IO ()
recordObservable :: State -> String -> (CV -> Bool) -> SV -> IO ()
recordObservable st :: State
st nm :: String
nm chk :: CV -> Bool
chk sv :: SV
sv = State
-> (State -> IORef [(String, CV -> Bool, SV)])
-> ([(String, CV -> Bool, SV)] -> [(String, CV -> Bool, SV)])
-> IO ()
-> IO ()
forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State -> IORef [(String, CV -> Bool, SV)]
rObservables ((String
nm, CV -> Bool
chk, SV
sv)(String, CV -> Bool, SV)
-> [(String, CV -> Bool, SV)] -> [(String, CV -> Bool, SV)]
forall a. a -> [a] -> [a]
:) (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())

-- | Increment the variable counter
incrementInternalCounter :: State -> IO Int
incrementInternalCounter :: State -> IO Int
incrementInternalCounter st :: State
st = do Int
ctr <- IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef (State -> IORef Int
rctr State
st)
                                 State -> (State -> IORef Int) -> (Int -> Int) -> IO () -> IO ()
forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State -> IORef Int
rctr (Int -> Int -> Int
forall a. Num a => a -> a -> a
+1) (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
                                 Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
ctr

-- | Uninterpreted constants and functions. An uninterpreted constant is
-- a value that is indexed by its name. The only property the prover assumes
-- about these values are that they are equivalent to themselves; i.e., (for
-- functions) they return the same results when applied to same arguments.
-- We support uninterpreted-functions as a general means of black-box'ing
-- operations that are /irrelevant/ for the purposes of the proof; i.e., when
-- the proofs can be performed without any knowledge about the function itself.
svUninterpreted :: Kind -> String -> Maybe [String] -> [SVal] -> SVal
svUninterpreted :: Kind -> String -> Maybe [String] -> [SVal] -> SVal
svUninterpreted k :: Kind
k nm :: String
nm code :: Maybe [String]
code args :: [SVal]
args = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
result
  where result :: State -> IO SV
result st :: State
st = do let ty :: SBVType
ty = [Kind] -> SBVType
SBVType ((SVal -> Kind) -> [SVal] -> [Kind]
forall a b. (a -> b) -> [a] -> [b]
map SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf [SVal]
args [Kind] -> [Kind] -> [Kind]
forall a. [a] -> [a] -> [a]
++ [Kind
k])
                       State -> String -> SBVType -> Maybe [String] -> IO ()
newUninterpreted State
st String
nm SBVType
ty Maybe [String]
code
                       [SV]
sws <- (SVal -> IO SV) -> [SVal] -> IO [SV]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (State -> SVal -> IO SV
svToSV State
st) [SVal]
args
                       (SV -> IO ()) -> [SV] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ SV -> IO ()
forceSVArg [SV]
sws
                       State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (SBVExpr -> IO SV) -> SBVExpr -> IO SV
forall a b. (a -> b) -> a -> b
$ Op -> [SV] -> SBVExpr
SBVApp (String -> Op
Uninterpreted String
nm) [SV]
sws

-- | Create a new uninterpreted symbol, possibly with user given code
newUninterpreted :: State -> String -> SBVType -> Maybe [String] -> IO ()
newUninterpreted :: State -> String -> SBVType -> Maybe [String] -> IO ()
newUninterpreted st :: State
st nm :: String
nm t :: SBVType
t mbCode :: Maybe [String]
mbCode
  | String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
nm Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
enclosed Bool -> Bool -> Bool
&& (Bool -> Bool
not (Char -> Bool
isAlpha (String -> Char
forall a. [a] -> a
head String
nm)) Bool -> Bool -> Bool
|| Bool -> Bool
not ((Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
validChar (ShowS
forall a. [a] -> [a]
tail String
nm)))
  = String -> IO ()
forall a. HasCallStack => String -> a
error (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Bad uninterpreted constant name: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ ". Must be a valid identifier."
  | Bool
True = do UIMap
uiMap <- IORef UIMap -> IO UIMap
forall a. IORef a -> IO a
readIORef (State -> IORef UIMap
rUIMap State
st)
              case String
nm String -> UIMap -> Maybe SBVType
forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` UIMap
uiMap of
                Just t' :: SBVType
t' -> SBVType -> IO () -> IO ()
forall r. SBVType -> r -> r
checkType SBVType
t' (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
                Nothing -> do State
-> (State -> IORef UIMap) -> (UIMap -> UIMap) -> IO () -> IO ()
forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State -> IORef UIMap
rUIMap (String -> SBVType -> UIMap -> UIMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
nm SBVType
t)
                                        (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ State -> (IncState -> IORef UIMap) -> (UIMap -> UIMap) -> IO ()
forall a. State -> (IncState -> IORef a) -> (a -> a) -> IO ()
modifyIncState State
st IncState -> IORef UIMap
rNewUIs (\newUIs :: UIMap
newUIs -> case String
nm String -> UIMap -> Maybe SBVType
forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` UIMap
newUIs of
                                                                                  Just t' :: SBVType
t' -> SBVType -> UIMap -> UIMap
forall r. SBVType -> r -> r
checkType SBVType
t' UIMap
newUIs
                                                                                  Nothing -> String -> SBVType -> UIMap -> UIMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
nm SBVType
t UIMap
newUIs)

                              -- No need to record the code in interactive mode: CodeGen doesn't use interactive
                              Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe [String] -> Bool
forall a. Maybe a -> Bool
isJust Maybe [String]
mbCode) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ State
-> (State -> IORef CgMap) -> (CgMap -> CgMap) -> IO () -> IO ()
forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State -> IORef CgMap
rCgMap (String -> [String] -> CgMap -> CgMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
nm (Maybe [String] -> [String]
forall a. HasCallStack => Maybe a -> a
fromJust Maybe [String]
mbCode)) (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
  where checkType :: SBVType -> r -> r
        checkType :: SBVType -> r -> r
checkType t' :: SBVType
t' cont :: r
cont
          | SBVType
t SBVType -> SBVType -> Bool
forall a. Eq a => a -> a -> Bool
/= SBVType
t' = String -> r
forall a. HasCallStack => String -> a
error (String -> r) -> String -> r
forall a b. (a -> b) -> a -> b
$  "Uninterpreted constant " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ " used at incompatible types\n"
                            String -> ShowS
forall a. [a] -> [a] -> [a]
++ "      Current type      : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SBVType -> String
forall a. Show a => a -> String
show SBVType
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n"
                            String -> ShowS
forall a. [a] -> [a] -> [a]
++ "      Previously used at: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SBVType -> String
forall a. Show a => a -> String
show SBVType
t'
          | Bool
True    = r
cont

        validChar :: Char -> Bool
validChar x :: Char
x = Char -> Bool
isAlphaNum Char
x Bool -> Bool -> Bool
|| Char
x Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` "_"
        enclosed :: Bool
enclosed    = String -> Char
forall a. [a] -> a
head String
nm Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '|' Bool -> Bool -> Bool
&& String -> Char
forall a. [a] -> a
last String
nm Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '|' Bool -> Bool -> Bool
&& String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
nm Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 2 Bool -> Bool -> Bool
&& Bool -> Bool
not ((Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` "|\\") (ShowS
forall a. [a] -> [a]
tail (ShowS
forall a. [a] -> [a]
init String
nm)))

-- | Add a new sAssert based constraint
addAssertion :: State -> Maybe CallStack -> String -> SV -> IO ()
addAssertion :: State -> Maybe CallStack -> String -> SV -> IO ()
addAssertion st :: State
st cs :: Maybe CallStack
cs msg :: String
msg cond :: SV
cond = State
-> (State -> IORef [(String, Maybe CallStack, SV)])
-> ([(String, Maybe CallStack, SV)]
    -> [(String, Maybe CallStack, SV)])
-> IO ()
-> IO ()
forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State -> IORef [(String, Maybe CallStack, SV)]
rAsserts ((String
msg, Maybe CallStack
cs, SV
cond)(String, Maybe CallStack, SV)
-> [(String, Maybe CallStack, SV)]
-> [(String, Maybe CallStack, SV)]
forall a. a -> [a] -> [a]
:)
                                        (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> IO ()
forall a. [String] -> a
noInteractive [ "Named assertions (sAssert):"
                                                        , "  Tag: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
msg
                                                        , "  Loc: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> (CallStack -> String) -> Maybe CallStack -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "Unknown" CallStack -> String
forall a. Show a => a -> String
show Maybe CallStack
cs
                                                        ]

-- | Create an internal variable, which acts as an input but isn't visible to the user.
-- Such variables are existentially quantified in a SAT context, and universally quantified
-- in a proof context.
internalVariable :: State -> Kind -> IO SV
internalVariable :: State -> Kind -> IO SV
internalVariable st :: State
st k :: Kind
k = do (sv :: SV
sv, nm :: String
nm) <- State -> Kind -> IO NamedSymVar
newSV State
st Kind
k
                           SBVRunMode
rm <- IORef SBVRunMode -> IO SBVRunMode
forall a. IORef a -> IO a
readIORef (State -> IORef SBVRunMode
runMode State
st)
                           let q :: Quantifier
q = case SBVRunMode
rm of
                                     SMTMode  _ _ True  _ -> Quantifier
EX
                                     SMTMode  _ _ False _ -> Quantifier
ALL
                                     CodeGen              -> Quantifier
ALL
                                     Concrete{}           -> Quantifier
ALL
                               n :: String
n = "__internal_sbv_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm
                               v :: NamedSymVar
v = (SV
sv, String
n)
                           State
-> (State
    -> IORef
         (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String))
-> ((([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    -> (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String))
-> IO ()
-> IO ()
forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State
-> IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
rinps (([(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)])
-> ([(Quantifier, NamedSymVar)], [NamedSymVar])
-> ([(Quantifier, NamedSymVar)], [NamedSymVar])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((Quantifier
q, NamedSymVar
v) (Quantifier, NamedSymVar)
-> [(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)]
forall a. a -> [a] -> [a]
:) (([(Quantifier, NamedSymVar)], [NamedSymVar])
 -> ([(Quantifier, NamedSymVar)], [NamedSymVar]))
-> (Set String -> Set String)
-> (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
-> (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert String
n)
                                     (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ State
-> (IncState -> IORef [NamedSymVar])
-> ([NamedSymVar] -> [NamedSymVar])
-> IO ()
forall a. State -> (IncState -> IORef a) -> (a -> a) -> IO ()
modifyIncState State
st IncState -> IORef [NamedSymVar]
rNewInps (\newInps :: [NamedSymVar]
newInps -> case Quantifier
q of
                                                                                 EX -> NamedSymVar
v NamedSymVar -> [NamedSymVar] -> [NamedSymVar]
forall a. a -> [a] -> [a]
: [NamedSymVar]
newInps
                                                                                 -- I don't think the following can actually happen
                                                                                 -- but just be safe:
                                                                                 ALL  -> [String] -> [NamedSymVar]
forall a. [String] -> a
noInteractive [ "Internal universally quantified variable creation:"
                                                                                                       , "  Named: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm
                                                                                                       ])
                           SV -> IO SV
forall (m :: * -> *) a. Monad m => a -> m a
return SV
sv
{-# INLINE internalVariable #-}

-- | Create a new SV
newSV :: State -> Kind -> IO (SV, String)
newSV :: State -> Kind -> IO NamedSymVar
newSV st :: State
st k :: Kind
k = do Int
ctr <- State -> IO Int
incrementInternalCounter State
st
                let sv :: SV
sv = Kind -> NodeId -> SV
SV Kind
k (Int -> NodeId
NodeId Int
ctr)
                State -> Kind -> IO ()
registerKind State
st Kind
k
                NamedSymVar -> IO NamedSymVar
forall (m :: * -> *) a. Monad m => a -> m a
return (SV
sv, 's' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
ctr)
{-# INLINE newSV #-}

-- | Register a new kind with the system, used for uninterpreted sorts.
-- NB: Is it safe to have new kinds in query mode? It could be that
-- the new kind might introduce a constraint that effects the logic. For
-- instance, if we're seeing 'Double' for the first time and using a BV
-- logic, then things would fall apart. But this should be rare, and hopefully
-- the success-response checking mechanism will catch the rare cases where this
-- is an issue. In either case, the user can always arrange for the right
-- logic by calling 'Data.SBV.setLogic' appropriately, so it seems safe to just
-- allow for this.
registerKind :: State -> Kind -> IO ()
registerKind :: State -> Kind -> IO ()
registerKind st :: State
st k :: Kind
k
  | KUninterpreted sortName :: String
sortName _ <- Kind
k, (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
sortName String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
smtLibReservedNames
  = String -> IO ()
forall a. HasCallStack => String -> a
error (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "SBV: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
sortName String -> ShowS
forall a. [a] -> [a] -> [a]
++ " is a reserved sort; please use a different name."
  | Bool
True
  = do -- Adding a kind to the incState is tricky; we only need to add it
       --     *    If it's an uninterpreted sort that's not already in the general state
       --     * OR If it's a tuple-sort whose cardinality isn't already in the general state
       --     * OR If it's a list that's not already in the general state (so we can send the flatten commands)

       Set Kind
existingKinds <- IORef (Set Kind) -> IO (Set Kind)
forall a. IORef a -> IO a
readIORef (State -> IORef (Set Kind)
rUsedKinds State
st)

       State
-> (State -> IORef (Set Kind))
-> (Set Kind -> Set Kind)
-> IO ()
-> IO ()
forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State -> IORef (Set Kind)
rUsedKinds (Kind -> Set Kind -> Set Kind
forall a. Ord a => a -> Set a -> Set a
Set.insert Kind
k) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do

                          -- Why do we discriminate here? Because the incremental context is sensitive to the
                          -- order: In particular, if an uninterpreted kind is already in there, we don't
                          -- want to re-add because double-declaration would be wrong. See 'cvtInc' for details.
                          let needsAdding :: Bool
needsAdding = case Kind
k of
                                              KUninterpreted{} -> Kind
k Kind -> Set Kind -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Set Kind
existingKinds
                                              KList{}          -> Kind
k Kind -> Set Kind -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Set Kind
existingKinds
                                              KTuple nks :: [Kind]
nks       -> [Kind] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
nks Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [[Kind] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
oks | KTuple oks :: [Kind]
oks <- Set Kind -> [Kind]
forall a. Set a -> [a]
Set.toList Set Kind
existingKinds]
                                              KMaybe{}         -> Kind
k Kind -> Set Kind -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Set Kind
existingKinds
                                              KEither{}        -> Kind
k Kind -> Set Kind -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Set Kind
existingKinds
                                              _                -> Bool
False

                          Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
needsAdding (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ State
-> (IncState -> IORef (Set Kind))
-> (Set Kind -> Set Kind)
-> IO ()
forall a. State -> (IncState -> IORef a) -> (a -> a) -> IO ()
modifyIncState State
st IncState -> IORef (Set Kind)
rNewKinds (Kind -> Set Kind -> Set Kind
forall a. Ord a => a -> Set a -> Set a
Set.insert Kind
k)

       -- Don't forget to register subkinds!
       case Kind
k of
         KBool          {}    -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
         KBounded       {}    -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
         KUnbounded     {}    -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
         KReal          {}    -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
         KUninterpreted {}    -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
         KFloat         {}    -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
         KDouble        {}    -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
         KChar          {}    -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
         KString        {}    -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
         KList          ek :: Kind
ek    -> State -> Kind -> IO ()
registerKind State
st Kind
ek
         KSet           ek :: Kind
ek    -> State -> Kind -> IO ()
registerKind State
st Kind
ek
         KTuple         eks :: [Kind]
eks   -> (Kind -> IO ()) -> [Kind] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (State -> Kind -> IO ()
registerKind State
st) [Kind]
eks
         KMaybe         ke :: Kind
ke    -> State -> Kind -> IO ()
registerKind State
st Kind
ke
         KEither        k1 :: Kind
k1 k2 :: Kind
k2 -> (Kind -> IO ()) -> [Kind] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (State -> Kind -> IO ()
registerKind State
st) [Kind
k1, Kind
k2]

-- | Register a new label with the system, making sure they are unique and have no '|'s in them
registerLabel :: String -> State -> String -> IO ()
registerLabel :: String -> State -> String -> IO ()
registerLabel whence :: String
whence st :: State
st nm :: String
nm
  | (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
nm String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
smtLibReservedNames
  = String -> IO ()
err "is a reserved string; please use a different name."
  | '|' Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
nm
  = String -> IO ()
err "contains the character `|', which is not allowed!"
  | '\\' Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
nm
  = String -> IO ()
err "contains the character `\\', which is not allowed!"
  | Bool
True
  = do Set String
old <- IORef (Set String) -> IO (Set String)
forall a. IORef a -> IO a
readIORef (IORef (Set String) -> IO (Set String))
-> IORef (Set String) -> IO (Set String)
forall a b. (a -> b) -> a -> b
$ State -> IORef (Set String)
rUsedLbls State
st
       if String
nm String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set String
old
          then String -> IO ()
err "is used multiple times. Please do not use duplicate names!"
          else State
-> (State -> IORef (Set String))
-> (Set String -> Set String)
-> IO ()
-> IO ()
forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State -> IORef (Set String)
rUsedLbls (String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert String
nm) (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())

  where err :: String -> IO ()
err w :: String
w = String -> IO ()
forall a. HasCallStack => String -> a
error (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "SBV (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
whence String -> ShowS
forall a. [a] -> [a] -> [a]
++ "): " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ " " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
w

-- | Create a new constant; hash-cons as necessary
newConst :: State -> CV -> IO SV
newConst :: State -> CV -> IO SV
newConst st :: State
st c :: CV
c = do
  CnstMap
constMap <- IORef CnstMap -> IO CnstMap
forall a. IORef a -> IO a
readIORef (State -> IORef CnstMap
rconstMap State
st)
  case CV
c CV -> CnstMap -> Maybe SV
forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` CnstMap
constMap of
    -- NB. Unlike in 'newExpr', we don't have to make sure the returned sv
    -- has the kind we asked for, because the constMap stores the full CV
    -- which already has a kind field in it.
    Just sv :: SV
sv -> SV -> IO SV
forall (m :: * -> *) a. Monad m => a -> m a
return SV
sv
    Nothing -> do (sv :: SV
sv, _) <- State -> Kind -> IO NamedSymVar
newSV State
st (CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
c)
                  let ins :: CnstMap -> CnstMap
ins = CV -> SV -> CnstMap -> CnstMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert CV
c SV
sv
                  State
-> (State -> IORef CnstMap)
-> (CnstMap -> CnstMap)
-> IO ()
-> IO ()
forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State -> IORef CnstMap
rconstMap CnstMap -> CnstMap
ins (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ State
-> (IncState -> IORef CnstMap) -> (CnstMap -> CnstMap) -> IO ()
forall a. State -> (IncState -> IORef a) -> (a -> a) -> IO ()
modifyIncState State
st IncState -> IORef CnstMap
rNewConsts CnstMap -> CnstMap
ins
                  SV -> IO SV
forall (m :: * -> *) a. Monad m => a -> m a
return SV
sv
{-# INLINE newConst #-}

-- | Create a new table; hash-cons as necessary
getTableIndex :: State -> Kind -> Kind -> [SV] -> IO Int
getTableIndex :: State -> Kind -> Kind -> [SV] -> IO Int
getTableIndex st :: State
st at :: Kind
at rt :: Kind
rt elts :: [SV]
elts = do
  let key :: (Kind, Kind, [SV])
key = (Kind
at, Kind
rt, [SV]
elts)
  TableMap
tblMap <- IORef TableMap -> IO TableMap
forall a. IORef a -> IO a
readIORef (State -> IORef TableMap
rtblMap State
st)
  case (Kind, Kind, [SV])
key (Kind, Kind, [SV]) -> TableMap -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` TableMap
tblMap of
    Just i :: Int
i -> Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
i
    _      -> do let i :: Int
i   = TableMap -> Int
forall k a. Map k a -> Int
Map.size TableMap
tblMap
                     upd :: TableMap -> TableMap
upd = (Kind, Kind, [SV]) -> Int -> TableMap -> TableMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Kind, Kind, [SV])
key Int
i
                 State
-> (State -> IORef TableMap)
-> (TableMap -> TableMap)
-> IO ()
-> IO ()
forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State -> IORef TableMap
rtblMap TableMap -> TableMap
upd (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ State
-> (IncState -> IORef TableMap) -> (TableMap -> TableMap) -> IO ()
forall a. State -> (IncState -> IORef a) -> (a -> a) -> IO ()
modifyIncState State
st IncState -> IORef TableMap
rNewTbls TableMap -> TableMap
upd
                 Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
i

-- | Create a new expression; hash-cons as necessary
newExpr :: State -> Kind -> SBVExpr -> IO SV
newExpr :: State -> Kind -> SBVExpr -> IO SV
newExpr st :: State
st k :: Kind
k app :: SBVExpr
app = do
   let e :: SBVExpr
e = SBVExpr -> SBVExpr
reorder SBVExpr
app
   ExprMap
exprMap <- IORef ExprMap -> IO ExprMap
forall a. IORef a -> IO a
readIORef (State -> IORef ExprMap
rexprMap State
st)
   case SBVExpr
e SBVExpr -> ExprMap -> Maybe SV
forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` ExprMap
exprMap of
     -- NB. Check to make sure that the kind of the hash-consed value
     -- is the same kind as we're requesting. This might look unnecessary,
     -- at first, but `svSign` and `svUnsign` rely on this as we can
     -- get the same expression but at a different type. See
     -- <http://github.com/GaloisInc/cryptol/issues/566> as an example.
     Just sv :: SV
sv | SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
sv Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k -> SV -> IO SV
forall (m :: * -> *) a. Monad m => a -> m a
return SV
sv
     _                        -> do (sv :: SV
sv, _) <- State -> Kind -> IO NamedSymVar
newSV State
st Kind
k
                                    let append :: SBVPgm -> SBVPgm
append (SBVPgm xs :: Seq (SV, SBVExpr)
xs) = Seq (SV, SBVExpr) -> SBVPgm
SBVPgm (Seq (SV, SBVExpr)
xs Seq (SV, SBVExpr) -> (SV, SBVExpr) -> Seq (SV, SBVExpr)
forall a. Seq a -> a -> Seq a
S.|> (SV
sv, SBVExpr
e))
                                    State
-> (State -> IORef SBVPgm) -> (SBVPgm -> SBVPgm) -> IO () -> IO ()
forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State -> IORef SBVPgm
spgm SBVPgm -> SBVPgm
append (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ State -> (IncState -> IORef SBVPgm) -> (SBVPgm -> SBVPgm) -> IO ()
forall a. State -> (IncState -> IORef a) -> (a -> a) -> IO ()
modifyIncState State
st IncState -> IORef SBVPgm
rNewAsgns SBVPgm -> SBVPgm
append
                                    State
-> (State -> IORef ExprMap)
-> (ExprMap -> ExprMap)
-> IO ()
-> IO ()
forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State -> IORef ExprMap
rexprMap (SBVExpr -> SV -> ExprMap -> ExprMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SBVExpr
e SV
sv) (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
                                    SV -> IO SV
forall (m :: * -> *) a. Monad m => a -> m a
return SV
sv
{-# INLINE newExpr #-}

-- | Convert a symbolic value to an internal SV
svToSV :: State -> SVal -> IO SV
svToSV :: State -> SVal -> IO SV
svToSV st :: State
st (SVal _ (Left c :: CV
c))  = State -> CV -> IO SV
newConst State
st CV
c
svToSV st :: State
st (SVal _ (Right f :: Cached SV
f)) = Cached SV -> State -> IO SV
uncache Cached SV
f State
st

-- | Generalization of 'Data.SBV.svToSymSV'
svToSymSV :: MonadSymbolic m => SVal -> m SV
svToSymSV :: SVal -> m SV
svToSymSV sbv :: SVal
sbv = do State
st <- m State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv
                   IO SV -> m SV
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SV -> m SV) -> IO SV -> m SV
forall a b. (a -> b) -> a -> b
$ State -> SVal -> IO SV
svToSV State
st SVal
sbv

-------------------------------------------------------------------------
-- * Symbolic Computations
-------------------------------------------------------------------------
-- | A Symbolic computation. Represented by a reader monad carrying the
-- state of the computation, layered on top of IO for creating unique
-- references to hold onto intermediate results.

-- | Computations which support symbolic operations
class MonadIO m => MonadSymbolic m where
  symbolicEnv :: m State

  default symbolicEnv :: (MonadTrans t, MonadSymbolic m', m ~ t m') => m State
  symbolicEnv = m' State -> t m' State
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m' State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv

instance MonadSymbolic m             => MonadSymbolic (ExceptT e m)
instance MonadSymbolic m             => MonadSymbolic (MaybeT m)
instance MonadSymbolic m             => MonadSymbolic (ReaderT r m)
instance MonadSymbolic m             => MonadSymbolic (SS.StateT s m)
instance MonadSymbolic m             => MonadSymbolic (LS.StateT s m)
instance (MonadSymbolic m, Monoid w) => MonadSymbolic (SW.WriterT w m)
instance (MonadSymbolic m, Monoid w) => MonadSymbolic (LW.WriterT w m)

-- | A generalization of 'Data.SBV.Symbolic'.
newtype SymbolicT m a = SymbolicT { SymbolicT m a -> ReaderT State m a
runSymbolicT :: ReaderT State m a }
                   deriving ( Functor (SymbolicT m)
a -> SymbolicT m a
Functor (SymbolicT m) =>
(forall a. a -> SymbolicT m a)
-> (forall a b.
    SymbolicT m (a -> b) -> SymbolicT m a -> SymbolicT m b)
-> (forall a b c.
    (a -> b -> c) -> SymbolicT m a -> SymbolicT m b -> SymbolicT m c)
-> (forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b)
-> (forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m a)
-> Applicative (SymbolicT m)
SymbolicT m a -> SymbolicT m b -> SymbolicT m b
SymbolicT m a -> SymbolicT m b -> SymbolicT m a
SymbolicT m (a -> b) -> SymbolicT m a -> SymbolicT m b
(a -> b -> c) -> SymbolicT m a -> SymbolicT m b -> SymbolicT m c
forall a. a -> SymbolicT m a
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m a
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
forall a b. SymbolicT m (a -> b) -> SymbolicT m a -> SymbolicT m b
forall a b c.
(a -> b -> c) -> SymbolicT m a -> SymbolicT m b -> SymbolicT m c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
forall (m :: * -> *). Applicative m => Functor (SymbolicT m)
forall (m :: * -> *) a. Applicative m => a -> SymbolicT m a
forall (m :: * -> *) a b.
Applicative m =>
SymbolicT m a -> SymbolicT m b -> SymbolicT m a
forall (m :: * -> *) a b.
Applicative m =>
SymbolicT m a -> SymbolicT m b -> SymbolicT m b
forall (m :: * -> *) a b.
Applicative m =>
SymbolicT m (a -> b) -> SymbolicT m a -> SymbolicT m b
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c) -> SymbolicT m a -> SymbolicT m b -> SymbolicT m c
<* :: SymbolicT m a -> SymbolicT m b -> SymbolicT m a
$c<* :: forall (m :: * -> *) a b.
Applicative m =>
SymbolicT m a -> SymbolicT m b -> SymbolicT m a
*> :: SymbolicT m a -> SymbolicT m b -> SymbolicT m b
$c*> :: forall (m :: * -> *) a b.
Applicative m =>
SymbolicT m a -> SymbolicT m b -> SymbolicT m b
liftA2 :: (a -> b -> c) -> SymbolicT m a -> SymbolicT m b -> SymbolicT m c
$cliftA2 :: forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c) -> SymbolicT m a -> SymbolicT m b -> SymbolicT m c
<*> :: SymbolicT m (a -> b) -> SymbolicT m a -> SymbolicT m b
$c<*> :: forall (m :: * -> *) a b.
Applicative m =>
SymbolicT m (a -> b) -> SymbolicT m a -> SymbolicT m b
pure :: a -> SymbolicT m a
$cpure :: forall (m :: * -> *) a. Applicative m => a -> SymbolicT m a
$cp1Applicative :: forall (m :: * -> *). Applicative m => Functor (SymbolicT m)
Applicative, a -> SymbolicT m b -> SymbolicT m a
(a -> b) -> SymbolicT m a -> SymbolicT m b
(forall a b. (a -> b) -> SymbolicT m a -> SymbolicT m b)
-> (forall a b. a -> SymbolicT m b -> SymbolicT m a)
-> Functor (SymbolicT m)
forall a b. a -> SymbolicT m b -> SymbolicT m a
forall a b. (a -> b) -> SymbolicT m a -> SymbolicT m b
forall (m :: * -> *) a b.
Functor m =>
a -> SymbolicT m b -> SymbolicT m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> SymbolicT m a -> SymbolicT m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> SymbolicT m b -> SymbolicT m a
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> SymbolicT m b -> SymbolicT m a
fmap :: (a -> b) -> SymbolicT m a -> SymbolicT m b
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> SymbolicT m a -> SymbolicT m b
Functor, Applicative (SymbolicT m)
a -> SymbolicT m a
Applicative (SymbolicT m) =>
(forall a b.
 SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b)
-> (forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b)
-> (forall a. a -> SymbolicT m a)
-> Monad (SymbolicT m)
SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
SymbolicT m a -> SymbolicT m b -> SymbolicT m b
forall a. a -> SymbolicT m a
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *). Monad m => Applicative (SymbolicT m)
forall (m :: * -> *) a. Monad m => a -> SymbolicT m a
forall (m :: * -> *) a b.
Monad m =>
SymbolicT m a -> SymbolicT m b -> SymbolicT m b
forall (m :: * -> *) a b.
Monad m =>
SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> SymbolicT m a
$creturn :: forall (m :: * -> *) a. Monad m => a -> SymbolicT m a
>> :: SymbolicT m a -> SymbolicT m b -> SymbolicT m b
$c>> :: forall (m :: * -> *) a b.
Monad m =>
SymbolicT m a -> SymbolicT m b -> SymbolicT m b
>>= :: SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
$c>>= :: forall (m :: * -> *) a b.
Monad m =>
SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
$cp1Monad :: forall (m :: * -> *). Monad m => Applicative (SymbolicT m)
Monad, Monad (SymbolicT m)
Monad (SymbolicT m) =>
(forall a. IO a -> SymbolicT m a) -> MonadIO (SymbolicT m)
IO a -> SymbolicT m a
forall a. IO a -> SymbolicT m a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> MonadIO m
forall (m :: * -> *). MonadIO m => Monad (SymbolicT m)
forall (m :: * -> *) a. MonadIO m => IO a -> SymbolicT m a
liftIO :: IO a -> SymbolicT m a
$cliftIO :: forall (m :: * -> *) a. MonadIO m => IO a -> SymbolicT m a
$cp1MonadIO :: forall (m :: * -> *). MonadIO m => Monad (SymbolicT m)
MonadIO, m a -> SymbolicT m a
(forall (m :: * -> *) a. Monad m => m a -> SymbolicT m a)
-> MonadTrans SymbolicT
forall (m :: * -> *) a. Monad m => m a -> SymbolicT m a
forall (t :: (* -> *) -> * -> *).
(forall (m :: * -> *) a. Monad m => m a -> t m a) -> MonadTrans t
lift :: m a -> SymbolicT m a
$clift :: forall (m :: * -> *) a. Monad m => m a -> SymbolicT m a
MonadTrans
                            , MonadError e, MonadState s, MonadWriter w
#if MIN_VERSION_base(4,11,0)
                            , Monad (SymbolicT m)
Monad (SymbolicT m) =>
(forall a. String -> SymbolicT m a) -> MonadFail (SymbolicT m)
String -> SymbolicT m a
forall a. String -> SymbolicT m a
forall (m :: * -> *).
Monad m =>
(forall a. String -> m a) -> MonadFail m
forall (m :: * -> *). MonadFail m => Monad (SymbolicT m)
forall (m :: * -> *) a. MonadFail m => String -> SymbolicT m a
fail :: String -> SymbolicT m a
$cfail :: forall (m :: * -> *) a. MonadFail m => String -> SymbolicT m a
$cp1MonadFail :: forall (m :: * -> *). MonadFail m => Monad (SymbolicT m)
Fail.MonadFail
#endif
                            )

-- | `MonadSymbolic` instance for `SymbolicT m`
instance MonadIO m => MonadSymbolic (SymbolicT m) where
  symbolicEnv :: SymbolicT m State
symbolicEnv = ReaderT State m State -> SymbolicT m State
forall (m :: * -> *) a. ReaderT State m a -> SymbolicT m a
SymbolicT ReaderT State m State
forall r (m :: * -> *). MonadReader r m => m r
ask

-- | Map a computation over the symbolic transformer.
mapSymbolicT :: (ReaderT State m a -> ReaderT State n b) -> SymbolicT m a -> SymbolicT n b
mapSymbolicT :: (ReaderT State m a -> ReaderT State n b)
-> SymbolicT m a -> SymbolicT n b
mapSymbolicT f :: ReaderT State m a -> ReaderT State n b
f = ReaderT State n b -> SymbolicT n b
forall (m :: * -> *) a. ReaderT State m a -> SymbolicT m a
SymbolicT (ReaderT State n b -> SymbolicT n b)
-> (SymbolicT m a -> ReaderT State n b)
-> SymbolicT m a
-> SymbolicT n b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReaderT State m a -> ReaderT State n b
f (ReaderT State m a -> ReaderT State n b)
-> (SymbolicT m a -> ReaderT State m a)
-> SymbolicT m a
-> ReaderT State n b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbolicT m a -> ReaderT State m a
forall (m :: * -> *) a. SymbolicT m a -> ReaderT State m a
runSymbolicT
{-# INLINE mapSymbolicT #-}

-- Have to define this one by hand, because we use ReaderT in the implementation
instance MonadReader r m => MonadReader r (SymbolicT m) where
  ask :: SymbolicT m r
ask = m r -> SymbolicT m r
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m r
forall r (m :: * -> *). MonadReader r m => m r
ask
  local :: (r -> r) -> SymbolicT m a -> SymbolicT m a
local f :: r -> r
f = (ReaderT State m a -> ReaderT State m a)
-> SymbolicT m a -> SymbolicT m a
forall (m :: * -> *) a (n :: * -> *) b.
(ReaderT State m a -> ReaderT State n b)
-> SymbolicT m a -> SymbolicT n b
mapSymbolicT ((ReaderT State m a -> ReaderT State m a)
 -> SymbolicT m a -> SymbolicT m a)
-> (ReaderT State m a -> ReaderT State m a)
-> SymbolicT m a
-> SymbolicT m a
forall a b. (a -> b) -> a -> b
$ (m a -> m a) -> ReaderT State m a -> ReaderT State m a
forall (m :: * -> *) a (n :: * -> *) b r.
(m a -> n b) -> ReaderT r m a -> ReaderT r n b
mapReaderT ((m a -> m a) -> ReaderT State m a -> ReaderT State m a)
-> (m a -> m a) -> ReaderT State m a -> ReaderT State m a
forall a b. (a -> b) -> a -> b
$ (r -> r) -> m a -> m a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local r -> r
f

-- | `Symbolic` is specialization of `SymbolicT` to the `IO` monad. Unless you are using
-- transformers explicitly, this is the type you should prefer.
type Symbolic = SymbolicT IO

-- | Create a symbolic value, based on the quantifier we have. If an
-- explicit quantifier is given, we just use that. If not, then we
-- pick the quantifier appropriately based on the run-mode.
-- @randomCV@ is used for generating random values for this variable
-- when used for @quickCheck@ or 'Data.SBV.Tools.GenTest.genTest' purposes.
svMkSymVar :: Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
svMkSymVar :: Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
svMkSymVar = Bool
-> Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
svMkSymVarGen Bool
False

-- | Create an existentially quantified tracker variable
svMkTrackerVar :: Kind -> String -> State -> IO SVal
svMkTrackerVar :: Kind -> String -> State -> IO SVal
svMkTrackerVar k :: Kind
k nm :: String
nm = Bool
-> Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
svMkSymVarGen Bool
True (Quantifier -> Maybe Quantifier
forall a. a -> Maybe a
Just Quantifier
EX) Kind
k (String -> Maybe String
forall a. a -> Maybe a
Just String
nm)

-- | Generalization of 'Data.SBV.sWordN'
sWordN :: MonadSymbolic m => Int -> String -> m SVal
sWordN :: Int -> String -> m SVal
sWordN w :: Int
w nm :: String
nm = m State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv m State -> (State -> m SVal) -> m SVal
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO SVal -> m SVal
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SVal -> m SVal) -> (State -> IO SVal) -> State -> m SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
svMkSymVar Maybe Quantifier
forall a. Maybe a
Nothing (Bool -> Int -> Kind
KBounded Bool
False Int
w) (String -> Maybe String
forall a. a -> Maybe a
Just String
nm)

-- | Generalization of 'Data.SBV.sWordN_'
sWordN_ :: MonadSymbolic m => Int -> m SVal
sWordN_ :: Int -> m SVal
sWordN_ w :: Int
w = m State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv m State -> (State -> m SVal) -> m SVal
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO SVal -> m SVal
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SVal -> m SVal) -> (State -> IO SVal) -> State -> m SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
svMkSymVar Maybe Quantifier
forall a. Maybe a
Nothing (Bool -> Int -> Kind
KBounded Bool
False Int
w) Maybe String
forall a. Maybe a
Nothing

-- | Generalization of 'Data.SBV.sIntN'
sIntN :: MonadSymbolic m => Int -> String -> m SVal
sIntN :: Int -> String -> m SVal
sIntN w :: Int
w nm :: String
nm = m State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv m State -> (State -> m SVal) -> m SVal
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO SVal -> m SVal
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SVal -> m SVal) -> (State -> IO SVal) -> State -> m SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
svMkSymVar Maybe Quantifier
forall a. Maybe a
Nothing (Bool -> Int -> Kind
KBounded Bool
True Int
w) (String -> Maybe String
forall a. a -> Maybe a
Just String
nm)

-- | Generalization of 'Data.SBV.sIntN_'
sIntN_ :: MonadSymbolic m => Int -> m SVal
sIntN_ :: Int -> m SVal
sIntN_ w :: Int
w = m State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv m State -> (State -> m SVal) -> m SVal
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO SVal -> m SVal
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SVal -> m SVal) -> (State -> IO SVal) -> State -> m SVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
svMkSymVar Maybe Quantifier
forall a. Maybe a
Nothing (Bool -> Int -> Kind
KBounded Bool
True Int
w) Maybe String
forall a. Maybe a
Nothing

-- | Create a symbolic value, based on the quantifier we have. If an
-- explicit quantifier is given, we just use that. If not, then we
-- pick the quantifier appropriately based on the run-mode.
-- @randomCV@ is used for generating random values for this variable
-- when used for @quickCheck@ or 'Data.SBV.Tools.GenTest.genTest' purposes.
svMkSymVarGen :: Bool -> Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
svMkSymVarGen :: Bool
-> Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
svMkSymVarGen isTracker :: Bool
isTracker mbQ :: Maybe Quantifier
mbQ k :: Kind
k mbNm :: Maybe String
mbNm st :: State
st = do
        SBVRunMode
rm <- IORef SBVRunMode -> IO SBVRunMode
forall a. IORef a -> IO a
readIORef (State -> IORef SBVRunMode
runMode State
st)

        let varInfo :: String
varInfo = case Maybe String
mbNm of
                        Nothing -> ", of type " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k
                        Just nm :: String
nm -> ", while defining " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ " :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k

            disallow :: String -> IO SVal
disallow what :: String
what  = String -> IO SVal
forall a. HasCallStack => String -> a
error (String -> IO SVal) -> String -> IO SVal
forall a b. (a -> b) -> a -> b
$ "Data.SBV: Unsupported: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
what String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
varInfo String -> ShowS
forall a. [a] -> [a] -> [a]
++ " in mode: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SBVRunMode -> String
forall a. Show a => a -> String
show SBVRunMode
rm

            noUI :: IO SVal -> IO SVal
noUI cont :: IO SVal
cont
              | Kind -> Bool
forall a. HasKind a => a -> Bool
isUninterpreted Kind
k  = String -> IO SVal
disallow "Uninterpreted sorts"
              | Bool
True               = IO SVal
cont

            mkS :: Quantifier -> IO SVal
mkS q :: Quantifier
q = do (sv :: SV
sv, internalName :: String
internalName) <- State -> Kind -> IO NamedSymVar
newSV State
st Kind
k
                       let nm :: String
nm = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
internalName Maybe String
mbNm
                       State -> Bool -> String -> Kind -> Quantifier -> SV -> IO SVal
introduceUserName State
st Bool
isTracker String
nm Kind
k Quantifier
q SV
sv

            mkC :: CV -> IO SVal
mkC cv :: CV
cv = do State -> Kind -> IO ()
registerKind State
st Kind
k
                        State
-> (State -> IORef [(String, CV)])
-> ([(String, CV)] -> [(String, CV)])
-> IO ()
-> IO ()
forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State -> IORef [(String, CV)]
rCInfo ((String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe "_" Maybe String
mbNm, CV
cv)(String, CV) -> [(String, CV)] -> [(String, CV)]
forall a. a -> [a] -> [a]
:) (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
                        SVal -> IO SVal
forall (m :: * -> *) a. Monad m => a -> m a
return (SVal -> IO SVal) -> SVal -> IO SVal
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left CV
cv)

        case (Maybe Quantifier
mbQ, SBVRunMode
rm) of
          (Just q :: Quantifier
q,  SMTMode{}          ) -> Quantifier -> IO SVal
mkS Quantifier
q
          (Nothing, SMTMode _ _ isSAT :: Bool
isSAT _) -> Quantifier -> IO SVal
mkS (if Bool
isSAT then Quantifier
EX else Quantifier
ALL)

          (Just EX, CodeGen{})           -> String -> IO SVal
disallow "Existentially quantified variables"
          (_      , CodeGen)             -> IO SVal -> IO SVal
noUI (IO SVal -> IO SVal) -> IO SVal -> IO SVal
forall a b. (a -> b) -> a -> b
$ Quantifier -> IO SVal
mkS Quantifier
ALL  -- code generation, pick universal

          (Just EX, Concrete Nothing)    -> String -> IO SVal
disallow "Existentially quantified variables"
          (_      , Concrete Nothing)    -> IO SVal -> IO SVal
noUI (Kind -> IO CV
randomCV Kind
k IO CV -> (CV -> IO SVal) -> IO SVal
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= CV -> IO SVal
mkC)

          -- Model validation:
          (_      , Concrete (Just (_isSat :: Bool
_isSat, env :: [((Quantifier, NamedSymVar), Maybe CV)]
env))) ->
                        let bad :: String -> String -> a
bad why :: String
why conc :: String
conc = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ ""
                                                           , "*** Data.SBV: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
why
                                                           , "***"
                                                           , "***   To turn validation off, use `cfg{validateModel = False}`"
                                                           , "***"
                                                           , "*** " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
conc
                                                           ]

                            cant :: String
cant   = "Validation engine is not capable of handling this case. Failed to validate."
                            report :: String
report = "Please report this as a bug in SBV!"

                        in if Kind -> Bool
forall a. HasKind a => a -> Bool
isUninterpreted Kind
k
                           then String -> String -> IO SVal
forall a. String -> String -> a
bad ("Cannot validate models in the presence of uninterpeted kinds, saw: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k) String
cant
                           else do (sv :: SV
sv, internalName :: String
internalName) <- State -> Kind -> IO NamedSymVar
newSV State
st Kind
k

                                   let nm :: String
nm = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
internalName Maybe String
mbNm
                                       nsv :: NamedSymVar
nsv = (SV
sv, String
nm)

                                       cv :: CV
cv = case [(Quantifier
q, Maybe CV
v) | ((q :: Quantifier
q, nsv' :: NamedSymVar
nsv'), v :: Maybe CV
v) <- [((Quantifier, NamedSymVar), Maybe CV)]
env, NamedSymVar
nsv NamedSymVar -> NamedSymVar -> Bool
forall a. Eq a => a -> a -> Bool
== NamedSymVar
nsv'] of
                                              []              -> if Bool
isTracker
                                                                 then  -- The sole purpose of a tracker variable is to send the optimization
                                                                       -- directive to the solver, so we can name "expressions" that are minimized
                                                                       -- or maximized. There will be no constraints on these when we are doing
                                                                       -- the validation; in fact they will not even be used anywhere during a
                                                                       -- validation run. So, simply push a zero value that inhabits all metrics.
                                                                       Kind -> Integer -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k (0::Integer)
                                                                 else String -> String -> CV
forall a. String -> String -> a
bad ("Cannot locate variable: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (NamedSymVar, Kind) -> String
forall a. Show a => a -> String
show (NamedSymVar
nsv, Kind
k)) String
report
                                              [(ALL, _)]      -> -- We can stop here, as we can't really validate in the presence of a universal quantifier:
                                                                 -- we'd have to validate for each possible value. But that's more or less useless. Instead,
                                                                 -- just issue a warning and use 0 for this value.
                                                                 Kind -> Integer -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k (0::Integer)
                                              [(EX, Nothing)] -> String -> String -> CV
forall a. String -> String -> a
bad ("Cannot locate model value of variable: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show (NamedSymVar -> String
forall a b. (a, b) -> b
snd NamedSymVar
nsv)) String
report
                                              [(EX, Just c :: CV
c)]  -> CV
c
                                              r :: [(Quantifier, Maybe CV)]
r               -> String -> String -> CV
forall a. String -> String -> a
bad (   "Found multiple matching values for variable: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NamedSymVar -> String
forall a. Show a => a -> String
show NamedSymVar
nsv
                                                                      String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n*** " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(Quantifier, Maybe CV)] -> String
forall a. Show a => a -> String
show [(Quantifier, Maybe CV)]
r) String
report

                                   CV -> IO SVal
mkC CV
cv

-- | Introduce a new user name. We simply append a suffix if we have seen this variable before.
introduceUserName :: State -> Bool -> String -> Kind -> Quantifier -> SV -> IO SVal
introduceUserName :: State -> Bool -> String -> Kind -> Quantifier -> SV -> IO SVal
introduceUserName st :: State
st isTracker :: Bool
isTracker nmOrig :: String
nmOrig k :: Kind
k q :: Quantifier
q sv :: SV
sv = do
        (_, old :: Set String
old) <- IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
-> IO (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
forall a. IORef a -> IO a
readIORef (State
-> IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
rinps State
st)

        let nm :: String
nm  = String -> Set String -> String
mkUnique String
nmOrig Set String
old

        if Bool
isTracker Bool -> Bool -> Bool
&& Quantifier
q Quantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
== Quantifier
ALL
           then String -> IO SVal
forall a. HasCallStack => String -> a
error (String -> IO SVal) -> String -> IO SVal
forall a b. (a -> b) -> a -> b
$ "SBV: Impossible happened! A universally quantified tracker variable is being introduced: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
nm
           else do let newInp :: [NamedSymVar] -> [NamedSymVar]
newInp olds :: [NamedSymVar]
olds = case Quantifier
q of
                                      EX  -> (SV
sv, String
nm) NamedSymVar -> [NamedSymVar] -> [NamedSymVar]
forall a. a -> [a] -> [a]
: [NamedSymVar]
olds
                                      ALL -> [String] -> [NamedSymVar]
forall a. [String] -> a
noInteractive [ "Adding a new universally quantified variable: "
                                                           , "  Name      : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
nm
                                                           , "  Kind      : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k
                                                           , "  Quantifier: Universal"
                                                           , "  Node      : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
sv
                                                           , "Only existential variables are supported in query mode."
                                                           ]
                   if Bool
isTracker
                      then State
-> (State
    -> IORef
         (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String))
-> ((([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    -> (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String))
-> IO ()
-> IO ()
forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State
-> IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
rinps (([NamedSymVar] -> [NamedSymVar])
-> ([(Quantifier, NamedSymVar)], [NamedSymVar])
-> ([(Quantifier, NamedSymVar)], [NamedSymVar])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second ((:) (SV
sv, String
nm)) (([(Quantifier, NamedSymVar)], [NamedSymVar])
 -> ([(Quantifier, NamedSymVar)], [NamedSymVar]))
-> (Set String -> Set String)
-> (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
-> (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert String
nm)
                                     (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> IO ()
forall a. [String] -> a
noInteractive ["Adding a new tracker variable in interactive mode: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
nm]
                      else State
-> (State
    -> IORef
         (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String))
-> ((([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    -> (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String))
-> IO ()
-> IO ()
forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State
-> IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
rinps (([(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)])
-> ([(Quantifier, NamedSymVar)], [NamedSymVar])
-> ([(Quantifier, NamedSymVar)], [NamedSymVar])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first ((:) (Quantifier
q, (SV
sv, String
nm))) (([(Quantifier, NamedSymVar)], [NamedSymVar])
 -> ([(Quantifier, NamedSymVar)], [NamedSymVar]))
-> (Set String -> Set String)
-> (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
-> (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert String
nm)
                                     (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ State
-> (IncState -> IORef [NamedSymVar])
-> ([NamedSymVar] -> [NamedSymVar])
-> IO ()
forall a. State -> (IncState -> IORef a) -> (a -> a) -> IO ()
modifyIncState State
st IncState -> IORef [NamedSymVar]
rNewInps [NamedSymVar] -> [NamedSymVar]
newInp
                   SVal -> IO SVal
forall (m :: * -> *) a. Monad m => a -> m a
return (SVal -> IO SVal) -> SVal -> IO SVal
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache (IO SV -> State -> IO SV
forall a b. a -> b -> a
const (SV -> IO SV
forall (m :: * -> *) a. Monad m => a -> m a
return SV
sv))

   where -- The following can be rather slow if we keep reusing the same prefix, but I doubt it'll be a problem in practice
         -- Also, the following will fail if we span the range of integers without finding a match, but your computer would
         -- die way ahead of that happening if that's the case!
         mkUnique :: String -> Set String -> String
mkUnique prefix :: String
prefix names :: Set String
names = [String] -> String
forall a. [a] -> a
head ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set String
names) (String
prefix String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String
prefix String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i | Int
i <- [(0::Int)..]])

-- | Generalization of 'Data.SBV.addAxiom'
addAxiom :: MonadSymbolic m => String -> [String] -> m ()
addAxiom :: String -> [String] -> m ()
addAxiom nm :: String
nm ax :: [String]
ax = do
        State
st <- m State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv
        IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ State
-> (State -> IORef [(String, [String])])
-> ([(String, [String])] -> [(String, [String])])
-> IO ()
-> IO ()
forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State -> IORef [(String, [String])]
raxioms ((String
nm, [String]
ax) (String, [String]) -> [(String, [String])] -> [(String, [String])]
forall a. a -> [a] -> [a]
:)
                           (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> IO ()
forall a. [String] -> a
noInteractive [ "Adding a new axiom:"
                                           , "  Named: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
nm
                                           , "  Axiom: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines [String]
ax
                                           ]

-- | Generalization of 'Data.SBV.runSymbolic'
runSymbolic :: MonadIO m => SBVRunMode -> SymbolicT m a -> m (a, Result)
runSymbolic :: SBVRunMode -> SymbolicT m a -> m (a, Result)
runSymbolic currentRunMode :: SBVRunMode
currentRunMode (SymbolicT c :: ReaderT State m a
c) = do
   State
st <- IO State -> m State
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO State -> m State) -> IO State -> m State
forall a b. (a -> b) -> a -> b
$ do
     UTCTime
currTime  <- IO UTCTime
getCurrentTime
     IORef SBVRunMode
rm        <- SBVRunMode -> IO (IORef SBVRunMode)
forall a. a -> IO (IORef a)
newIORef SBVRunMode
currentRunMode
     IORef Int
ctr       <- Int -> IO (IORef Int)
forall a. a -> IO (IORef a)
newIORef (-2) -- start from -2; False and True will always occupy the first two elements
     IORef [(String, CV)]
cInfo     <- [(String, CV)] -> IO (IORef [(String, CV)])
forall a. a -> IO (IORef a)
newIORef []
     IORef [(String, CV -> Bool, SV)]
observes  <- [(String, CV -> Bool, SV)] -> IO (IORef [(String, CV -> Bool, SV)])
forall a. a -> IO (IORef a)
newIORef []
     IORef SBVPgm
pgm       <- SBVPgm -> IO (IORef SBVPgm)
forall a. a -> IO (IORef a)
newIORef (Seq (SV, SBVExpr) -> SBVPgm
SBVPgm Seq (SV, SBVExpr)
forall a. Seq a
S.empty)
     IORef ExprMap
emap      <- ExprMap -> IO (IORef ExprMap)
forall a. a -> IO (IORef a)
newIORef ExprMap
forall k a. Map k a
Map.empty
     IORef CnstMap
cmap      <- CnstMap -> IO (IORef CnstMap)
forall a. a -> IO (IORef a)
newIORef CnstMap
forall k a. Map k a
Map.empty
     IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
inps      <- (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
-> IO
     (IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String))
forall a. a -> IO (IORef a)
newIORef (([], []), Set String
forall a. Set a
Set.empty)
     IORef [SV]
outs      <- [SV] -> IO (IORef [SV])
forall a. a -> IO (IORef a)
newIORef []
     IORef TableMap
tables    <- TableMap -> IO (IORef TableMap)
forall a. a -> IO (IORef a)
newIORef TableMap
forall k a. Map k a
Map.empty
     IORef ArrayMap
arrays    <- ArrayMap -> IO (IORef ArrayMap)
forall a. a -> IO (IORef a)
newIORef ArrayMap
forall a. IntMap a
IMap.empty
     IORef FArrayMap
fArrays   <- FArrayMap -> IO (IORef FArrayMap)
forall a. a -> IO (IORef a)
newIORef FArrayMap
forall a. IntMap a
IMap.empty
     IORef UIMap
uis       <- UIMap -> IO (IORef UIMap)
forall a. a -> IO (IORef a)
newIORef UIMap
forall k a. Map k a
Map.empty
     IORef CgMap
cgs       <- CgMap -> IO (IORef CgMap)
forall a. a -> IO (IORef a)
newIORef CgMap
forall k a. Map k a
Map.empty
     IORef [(String, [String])]
axioms    <- [(String, [String])] -> IO (IORef [(String, [String])])
forall a. a -> IO (IORef a)
newIORef []
     IORef (Cache SV)
swCache   <- Cache SV -> IO (IORef (Cache SV))
forall a. a -> IO (IORef a)
newIORef Cache SV
forall a. IntMap a
IMap.empty
     IORef (Cache ArrayIndex)
aiCache   <- Cache ArrayIndex -> IO (IORef (Cache ArrayIndex))
forall a. a -> IO (IORef a)
newIORef Cache ArrayIndex
forall a. IntMap a
IMap.empty
     IORef (Cache FArrayIndex)
faiCache  <- Cache FArrayIndex -> IO (IORef (Cache FArrayIndex))
forall a. a -> IO (IORef a)
newIORef Cache FArrayIndex
forall a. IntMap a
IMap.empty
     IORef (Set Kind)
usedKinds <- Set Kind -> IO (IORef (Set Kind))
forall a. a -> IO (IORef a)
newIORef Set Kind
forall a. Set a
Set.empty
     IORef (Set String)
usedLbls  <- Set String -> IO (IORef (Set String))
forall a. a -> IO (IORef a)
newIORef Set String
forall a. Set a
Set.empty
     IORef (Seq (Bool, [(String, String)], SV))
cstrs     <- Seq (Bool, [(String, String)], SV)
-> IO (IORef (Seq (Bool, [(String, String)], SV)))
forall a. a -> IO (IORef a)
newIORef Seq (Bool, [(String, String)], SV)
forall a. Seq a
S.empty
     IORef [SMTOption]
smtOpts   <- [SMTOption] -> IO (IORef [SMTOption])
forall a. a -> IO (IORef a)
newIORef []
     IORef [Objective (SV, SV)]
optGoals  <- [Objective (SV, SV)] -> IO (IORef [Objective (SV, SV)])
forall a. a -> IO (IORef a)
newIORef []
     IORef [(String, Maybe CallStack, SV)]
asserts   <- [(String, Maybe CallStack, SV)]
-> IO (IORef [(String, Maybe CallStack, SV)])
forall a. a -> IO (IORef a)
newIORef []
     IORef IncState
istate    <- IncState -> IO (IORef IncState)
forall a. a -> IO (IORef a)
newIORef (IncState -> IO (IORef IncState))
-> IO IncState -> IO (IORef IncState)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO IncState
newIncState
     IORef (Maybe QueryState)
qstate    <- Maybe QueryState -> IO (IORef (Maybe QueryState))
forall a. a -> IO (IORef a)
newIORef Maybe QueryState
forall a. Maybe a
Nothing
     State -> IO State
forall (f :: * -> *) a. Applicative f => a -> f a
pure (State -> IO State) -> State -> IO State
forall a b. (a -> b) -> a -> b
$ State :: SVal
-> UTCTime
-> IORef SBVRunMode
-> IORef IncState
-> IORef [(String, CV)]
-> IORef [(String, CV -> Bool, SV)]
-> IORef Int
-> IORef (Set Kind)
-> IORef (Set String)
-> IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
-> IORef (Seq (Bool, [(String, String)], SV))
-> IORef [SV]
-> IORef TableMap
-> IORef SBVPgm
-> IORef CnstMap
-> IORef ExprMap
-> IORef ArrayMap
-> IORef FArrayMap
-> IORef UIMap
-> IORef CgMap
-> IORef [(String, [String])]
-> IORef [SMTOption]
-> IORef [Objective (SV, SV)]
-> IORef [(String, Maybe CallStack, SV)]
-> IORef (Cache SV)
-> IORef (Cache ArrayIndex)
-> IORef (Cache FArrayIndex)
-> IORef (Maybe QueryState)
-> State
State { runMode :: IORef SBVRunMode
runMode      = IORef SBVRunMode
rm
                  , startTime :: UTCTime
startTime    = UTCTime
currTime
                  , pathCond :: SVal
pathCond     = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KBool (CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left CV
trueCV)
                  , rIncState :: IORef IncState
rIncState    = IORef IncState
istate
                  , rCInfo :: IORef [(String, CV)]
rCInfo       = IORef [(String, CV)]
cInfo
                  , rObservables :: IORef [(String, CV -> Bool, SV)]
rObservables = IORef [(String, CV -> Bool, SV)]
observes
                  , rctr :: IORef Int
rctr         = IORef Int
ctr
                  , rUsedKinds :: IORef (Set Kind)
rUsedKinds   = IORef (Set Kind)
usedKinds
                  , rUsedLbls :: IORef (Set String)
rUsedLbls    = IORef (Set String)
usedLbls
                  , rinps :: IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
rinps        = IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
inps
                  , routs :: IORef [SV]
routs        = IORef [SV]
outs
                  , rtblMap :: IORef TableMap
rtblMap      = IORef TableMap
tables
                  , spgm :: IORef SBVPgm
spgm         = IORef SBVPgm
pgm
                  , rconstMap :: IORef CnstMap
rconstMap    = IORef CnstMap
cmap
                  , rArrayMap :: IORef ArrayMap
rArrayMap    = IORef ArrayMap
arrays
                  , rFArrayMap :: IORef FArrayMap
rFArrayMap   = IORef FArrayMap
fArrays
                  , rexprMap :: IORef ExprMap
rexprMap     = IORef ExprMap
emap
                  , rUIMap :: IORef UIMap
rUIMap       = IORef UIMap
uis
                  , rCgMap :: IORef CgMap
rCgMap       = IORef CgMap
cgs
                  , raxioms :: IORef [(String, [String])]
raxioms      = IORef [(String, [String])]
axioms
                  , rSVCache :: IORef (Cache SV)
rSVCache     = IORef (Cache SV)
swCache
                  , rAICache :: IORef (Cache ArrayIndex)
rAICache     = IORef (Cache ArrayIndex)
aiCache
                  , rFAICache :: IORef (Cache FArrayIndex)
rFAICache    = IORef (Cache FArrayIndex)
faiCache
                  , rConstraints :: IORef (Seq (Bool, [(String, String)], SV))
rConstraints = IORef (Seq (Bool, [(String, String)], SV))
cstrs
                  , rSMTOptions :: IORef [SMTOption]
rSMTOptions  = IORef [SMTOption]
smtOpts
                  , rOptGoals :: IORef [Objective (SV, SV)]
rOptGoals    = IORef [Objective (SV, SV)]
optGoals
                  , rAsserts :: IORef [(String, Maybe CallStack, SV)]
rAsserts     = IORef [(String, Maybe CallStack, SV)]
asserts
                  , rQueryState :: IORef (Maybe QueryState)
rQueryState   = IORef (Maybe QueryState)
qstate
                  }
   SV
_ <- IO SV -> m SV
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SV -> m SV) -> IO SV -> m SV
forall a b. (a -> b) -> a -> b
$ State -> CV -> IO SV
newConst State
st CV
falseCV -- s(-2) == falseSV
   SV
_ <- IO SV -> m SV
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SV -> m SV) -> IO SV -> m SV
forall a b. (a -> b) -> a -> b
$ State -> CV -> IO SV
newConst State
st CV
trueCV  -- s(-1) == trueSV
   a
r <- ReaderT State m a -> State -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT State m a
c State
st
   Result
res <- IO Result -> m Result
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Result -> m Result) -> IO Result -> m Result
forall a b. (a -> b) -> a -> b
$ State -> IO Result
extractSymbolicSimulationState State
st

   -- Clean-up after ourselves
   Maybe QueryState
qs <- IO (Maybe QueryState) -> m (Maybe QueryState)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Maybe QueryState) -> m (Maybe QueryState))
-> IO (Maybe QueryState) -> m (Maybe QueryState)
forall a b. (a -> b) -> a -> b
$ IORef (Maybe QueryState) -> IO (Maybe QueryState)
forall a. IORef a -> IO a
readIORef (IORef (Maybe QueryState) -> IO (Maybe QueryState))
-> IORef (Maybe QueryState) -> IO (Maybe QueryState)
forall a b. (a -> b) -> a -> b
$ State -> IORef (Maybe QueryState)
rQueryState State
st
   case Maybe QueryState
qs of
     Nothing                         -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
     Just QueryState{IO ()
queryTerminate :: IO ()
queryTerminate :: QueryState -> IO ()
queryTerminate} -> IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO ()
queryTerminate

   (a, Result) -> m (a, Result)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
r, Result
res)

-- | Grab the program from a running symbolic simulation state.
extractSymbolicSimulationState :: State -> IO Result
extractSymbolicSimulationState :: State -> IO Result
extractSymbolicSimulationState st :: State
st@State{ spgm :: State -> IORef SBVPgm
spgm=IORef SBVPgm
pgm, rinps :: State
-> IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
rinps=IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
inps, routs :: State -> IORef [SV]
routs=IORef [SV]
outs, rtblMap :: State -> IORef TableMap
rtblMap=IORef TableMap
tables, rArrayMap :: State -> IORef ArrayMap
rArrayMap=IORef ArrayMap
arrays, rUIMap :: State -> IORef UIMap
rUIMap=IORef UIMap
uis, raxioms :: State -> IORef [(String, [String])]
raxioms=IORef [(String, [String])]
axioms
                                       , rAsserts :: State -> IORef [(String, Maybe CallStack, SV)]
rAsserts=IORef [(String, Maybe CallStack, SV)]
asserts, rUsedKinds :: State -> IORef (Set Kind)
rUsedKinds=IORef (Set Kind)
usedKinds, rCgMap :: State -> IORef CgMap
rCgMap=IORef CgMap
cgs, rCInfo :: State -> IORef [(String, CV)]
rCInfo=IORef [(String, CV)]
cInfo, rConstraints :: State -> IORef (Seq (Bool, [(String, String)], SV))
rConstraints=IORef (Seq (Bool, [(String, String)], SV))
cstrs
                                       , rObservables :: State -> IORef [(String, CV -> Bool, SV)]
rObservables=IORef [(String, CV -> Bool, SV)]
observes
                                       } = do
   SBVPgm rpgm :: Seq (SV, SBVExpr)
rpgm  <- IORef SBVPgm -> IO SBVPgm
forall a. IORef a -> IO a
readIORef IORef SBVPgm
pgm
   ([(Quantifier, NamedSymVar)], [NamedSymVar])
inpsO <- ([(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)]
forall a. [a] -> [a]
reverse ([(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)])
-> ([NamedSymVar] -> [NamedSymVar])
-> ([(Quantifier, NamedSymVar)], [NamedSymVar])
-> ([(Quantifier, NamedSymVar)], [NamedSymVar])
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** [NamedSymVar] -> [NamedSymVar]
forall a. [a] -> [a]
reverse) (([(Quantifier, NamedSymVar)], [NamedSymVar])
 -> ([(Quantifier, NamedSymVar)], [NamedSymVar]))
-> ((([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
    -> ([(Quantifier, NamedSymVar)], [NamedSymVar]))
-> (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
-> ([(Quantifier, NamedSymVar)], [NamedSymVar])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
-> ([(Quantifier, NamedSymVar)], [NamedSymVar])
forall a b. (a, b) -> a
fst ((([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
 -> ([(Quantifier, NamedSymVar)], [NamedSymVar]))
-> IO (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
-> IO ([(Quantifier, NamedSymVar)], [NamedSymVar])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
-> IO (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
forall a. IORef a -> IO a
readIORef IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
inps
   [SV]
outsO <- [SV] -> [SV]
forall a. [a] -> [a]
reverse ([SV] -> [SV]) -> IO [SV] -> IO [SV]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef [SV] -> IO [SV]
forall a. IORef a -> IO a
readIORef IORef [SV]
outs

   let swap :: (b, a) -> (a, b)
swap  (a :: b
a, b :: a
b)              = (a
b, b
a)
       cmp :: (a, b) -> (a, b) -> Ordering
cmp   (a :: a
a, _) (b :: a
b, _)       = a
a a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` a
b
       arrange :: (a, (b, c, b)) -> ((a, b, c), b)
arrange (i :: a
i, (at :: b
at, rt :: c
rt, es :: b
es)) = ((a
i, b
at, c
rt), b
es)

   [(SV, CV)]
cnsts <- ((SV, CV) -> (SV, CV) -> Ordering) -> [(SV, CV)] -> [(SV, CV)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (SV, CV) -> (SV, CV) -> Ordering
forall a b b. Ord a => (a, b) -> (a, b) -> Ordering
cmp ([(SV, CV)] -> [(SV, CV)])
-> (CnstMap -> [(SV, CV)]) -> CnstMap -> [(SV, CV)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((CV, SV) -> (SV, CV)) -> [(CV, SV)] -> [(SV, CV)]
forall a b. (a -> b) -> [a] -> [b]
map (CV, SV) -> (SV, CV)
forall b a. (b, a) -> (a, b)
swap ([(CV, SV)] -> [(SV, CV)])
-> (CnstMap -> [(CV, SV)]) -> CnstMap -> [(SV, CV)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CnstMap -> [(CV, SV)]
forall k a. Map k a -> [(k, a)]
Map.toList (CnstMap -> [(SV, CV)]) -> IO CnstMap -> IO [(SV, CV)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef CnstMap -> IO CnstMap
forall a. IORef a -> IO a
readIORef (State -> IORef CnstMap
rconstMap State
st)
   [((Int, Kind, Kind), [SV])]
tbls  <- ((Int, (Kind, Kind, [SV])) -> ((Int, Kind, Kind), [SV]))
-> [(Int, (Kind, Kind, [SV]))] -> [((Int, Kind, Kind), [SV])]
forall a b. (a -> b) -> [a] -> [b]
map (Int, (Kind, Kind, [SV])) -> ((Int, Kind, Kind), [SV])
forall a b c b. (a, (b, c, b)) -> ((a, b, c), b)
arrange ([(Int, (Kind, Kind, [SV]))] -> [((Int, Kind, Kind), [SV])])
-> (TableMap -> [(Int, (Kind, Kind, [SV]))])
-> TableMap
-> [((Int, Kind, Kind), [SV])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, (Kind, Kind, [SV]))
 -> (Int, (Kind, Kind, [SV])) -> Ordering)
-> [(Int, (Kind, Kind, [SV]))] -> [(Int, (Kind, Kind, [SV]))]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Int, (Kind, Kind, [SV])) -> (Int, (Kind, Kind, [SV])) -> Ordering
forall a b b. Ord a => (a, b) -> (a, b) -> Ordering
cmp ([(Int, (Kind, Kind, [SV]))] -> [(Int, (Kind, Kind, [SV]))])
-> (TableMap -> [(Int, (Kind, Kind, [SV]))])
-> TableMap
-> [(Int, (Kind, Kind, [SV]))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((Kind, Kind, [SV]), Int) -> (Int, (Kind, Kind, [SV])))
-> [((Kind, Kind, [SV]), Int)] -> [(Int, (Kind, Kind, [SV]))]
forall a b. (a -> b) -> [a] -> [b]
map ((Kind, Kind, [SV]), Int) -> (Int, (Kind, Kind, [SV]))
forall b a. (b, a) -> (a, b)
swap ([((Kind, Kind, [SV]), Int)] -> [(Int, (Kind, Kind, [SV]))])
-> (TableMap -> [((Kind, Kind, [SV]), Int)])
-> TableMap
-> [(Int, (Kind, Kind, [SV]))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TableMap -> [((Kind, Kind, [SV]), Int)]
forall k a. Map k a -> [(k, a)]
Map.toList (TableMap -> [((Int, Kind, Kind), [SV])])
-> IO TableMap -> IO [((Int, Kind, Kind), [SV])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef TableMap -> IO TableMap
forall a. IORef a -> IO a
readIORef IORef TableMap
tables
   [(Int, ArrayInfo)]
arrs  <- ArrayMap -> [(Int, ArrayInfo)]
forall a. IntMap a -> [(Int, a)]
IMap.toAscList (ArrayMap -> [(Int, ArrayInfo)])
-> IO ArrayMap -> IO [(Int, ArrayInfo)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef ArrayMap -> IO ArrayMap
forall a. IORef a -> IO a
readIORef IORef ArrayMap
arrays
   [(String, SBVType)]
unint <- UIMap -> [(String, SBVType)]
forall k a. Map k a -> [(k, a)]
Map.toList (UIMap -> [(String, SBVType)])
-> IO UIMap -> IO [(String, SBVType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef UIMap -> IO UIMap
forall a. IORef a -> IO a
readIORef IORef UIMap
uis
   [(String, [String])]
axs   <- [(String, [String])] -> [(String, [String])]
forall a. [a] -> [a]
reverse ([(String, [String])] -> [(String, [String])])
-> IO [(String, [String])] -> IO [(String, [String])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef [(String, [String])] -> IO [(String, [String])]
forall a. IORef a -> IO a
readIORef IORef [(String, [String])]
axioms
   Set Kind
knds  <- IORef (Set Kind) -> IO (Set Kind)
forall a. IORef a -> IO a
readIORef IORef (Set Kind)
usedKinds
   [(String, [String])]
cgMap <- CgMap -> [(String, [String])]
forall k a. Map k a -> [(k, a)]
Map.toList (CgMap -> [(String, [String])])
-> IO CgMap -> IO [(String, [String])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef CgMap -> IO CgMap
forall a. IORef a -> IO a
readIORef IORef CgMap
cgs

   [(String, CV)]
traceVals   <- [(String, CV)] -> [(String, CV)]
forall a. [a] -> [a]
reverse ([(String, CV)] -> [(String, CV)])
-> IO [(String, CV)] -> IO [(String, CV)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef [(String, CV)] -> IO [(String, CV)]
forall a. IORef a -> IO a
readIORef IORef [(String, CV)]
cInfo
   [(String, CV -> Bool, SV)]
observables <- [(String, CV -> Bool, SV)] -> [(String, CV -> Bool, SV)]
forall a. [a] -> [a]
reverse ([(String, CV -> Bool, SV)] -> [(String, CV -> Bool, SV)])
-> IO [(String, CV -> Bool, SV)] -> IO [(String, CV -> Bool, SV)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef [(String, CV -> Bool, SV)] -> IO [(String, CV -> Bool, SV)]
forall a. IORef a -> IO a
readIORef IORef [(String, CV -> Bool, SV)]
observes
   Seq (Bool, [(String, String)], SV)
extraCstrs  <- IORef (Seq (Bool, [(String, String)], SV))
-> IO (Seq (Bool, [(String, String)], SV))
forall a. IORef a -> IO a
readIORef IORef (Seq (Bool, [(String, String)], SV))
cstrs
   [(String, Maybe CallStack, SV)]
assertions  <- [(String, Maybe CallStack, SV)] -> [(String, Maybe CallStack, SV)]
forall a. [a] -> [a]
reverse ([(String, Maybe CallStack, SV)]
 -> [(String, Maybe CallStack, SV)])
-> IO [(String, Maybe CallStack, SV)]
-> IO [(String, Maybe CallStack, SV)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef [(String, Maybe CallStack, SV)]
-> IO [(String, Maybe CallStack, SV)]
forall a. IORef a -> IO a
readIORef IORef [(String, Maybe CallStack, SV)]
asserts

   Result -> IO Result
forall (m :: * -> *) a. Monad m => a -> m a
return (Result -> IO Result) -> Result -> IO Result
forall a b. (a -> b) -> a -> b
$ Set Kind
-> [(String, CV)]
-> [(String, CV -> Bool, SV)]
-> [(String, [String])]
-> ([(Quantifier, NamedSymVar)], [NamedSymVar])
-> [(SV, CV)]
-> [((Int, Kind, Kind), [SV])]
-> [(Int, ArrayInfo)]
-> [(String, SBVType)]
-> [(String, [String])]
-> SBVPgm
-> Seq (Bool, [(String, String)], SV)
-> [(String, Maybe CallStack, SV)]
-> [SV]
-> Result
Result Set Kind
knds [(String, CV)]
traceVals [(String, CV -> Bool, SV)]
observables [(String, [String])]
cgMap ([(Quantifier, NamedSymVar)], [NamedSymVar])
inpsO [(SV, CV)]
cnsts [((Int, Kind, Kind), [SV])]
tbls [(Int, ArrayInfo)]
arrs [(String, SBVType)]
unint [(String, [String])]
axs (Seq (SV, SBVExpr) -> SBVPgm
SBVPgm Seq (SV, SBVExpr)
rpgm) Seq (Bool, [(String, String)], SV)
extraCstrs [(String, Maybe CallStack, SV)]
assertions [SV]
outsO

-- | Generalization of 'Data.SBV.addNewSMTOption'
addNewSMTOption :: MonadSymbolic m => SMTOption -> m ()
addNewSMTOption :: SMTOption -> m ()
addNewSMTOption o :: SMTOption
o = do State
st <- m State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv
                       IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ State
-> (State -> IORef [SMTOption])
-> ([SMTOption] -> [SMTOption])
-> IO ()
-> IO ()
forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State -> IORef [SMTOption]
rSMTOptions (SMTOption
oSMTOption -> [SMTOption] -> [SMTOption]
forall a. a -> [a] -> [a]
:) (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())

-- | Generalization of 'Data.SBV.imposeConstraint'
imposeConstraint :: MonadSymbolic m => Bool -> [(String, String)] -> SVal -> m ()
imposeConstraint :: Bool -> [(String, String)] -> SVal -> m ()
imposeConstraint isSoft :: Bool
isSoft attrs :: [(String, String)]
attrs c :: SVal
c = do State
st <- m State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv
                                     SBVRunMode
rm <- IO SBVRunMode -> m SBVRunMode
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SBVRunMode -> m SBVRunMode) -> IO SBVRunMode -> m SBVRunMode
forall a b. (a -> b) -> a -> b
$ IORef SBVRunMode -> IO SBVRunMode
forall a. IORef a -> IO a
readIORef (State -> IORef SBVRunMode
runMode State
st)

                                     case SBVRunMode
rm of
                                       CodeGen -> String -> m ()
forall a. HasCallStack => String -> a
error "SBV: constraints are not allowed in code-generation"
                                       _       -> IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ do (String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> State -> String -> IO ()
registerLabel "Constraint" State
st) [String
nm | (":named",  nm :: String
nm) <- [(String, String)]
attrs]
                                                              State -> Bool -> [(String, String)] -> SVal -> IO ()
internalConstraint State
st Bool
isSoft [(String, String)]
attrs SVal
c

-- | Require a boolean condition to be true in the state. Only used for internal purposes.
internalConstraint :: State -> Bool -> [(String, String)] -> SVal -> IO ()
internalConstraint :: State -> Bool -> [(String, String)] -> SVal -> IO ()
internalConstraint st :: State
st isSoft :: Bool
isSoft attrs :: [(String, String)]
attrs b :: SVal
b = do SV
v <- State -> SVal -> IO SV
svToSV State
st SVal
b

                                          SBVRunMode
rm <- IO SBVRunMode -> IO SBVRunMode
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SBVRunMode -> IO SBVRunMode) -> IO SBVRunMode -> IO SBVRunMode
forall a b. (a -> b) -> a -> b
$ IORef SBVRunMode -> IO SBVRunMode
forall a. IORef a -> IO a
readIORef (State -> IORef SBVRunMode
runMode State
st)

                                          -- Are we running validation? If so, we always want to
                                          -- add the constraint for debug purposes. Otherwie
                                          -- we only add it if it's interesting; i.e., not directly
                                          -- true or has some attributes.
                                          let isValidating :: Bool
isValidating = case SBVRunMode
rm of
                                                               SMTMode _ _ _ cfg :: SMTConfig
cfg -> SMTConfig -> Bool
validationRequested SMTConfig
cfg
                                                               CodeGen           -> Bool
False
                                                               Concrete Nothing  -> Bool
False
                                                               Concrete (Just _) -> Bool
True   -- The case when we *are* running the validation

                                          let c :: (Bool, [(String, String)], SV)
c           = (Bool
isSoft, [(String, String)]
attrs, SV
v)
                                              interesting :: Bool
interesting = SV
v SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
/= SV
trueSV Bool -> Bool -> Bool
|| Bool -> Bool
not ([(String, String)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, String)]
attrs)

                                          Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
isValidating Bool -> Bool -> Bool
|| Bool
interesting) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
                                               State
-> (State -> IORef (Seq (Bool, [(String, String)], SV)))
-> (Seq (Bool, [(String, String)], SV)
    -> Seq (Bool, [(String, String)], SV))
-> IO ()
-> IO ()
forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State -> IORef (Seq (Bool, [(String, String)], SV))
rConstraints (Seq (Bool, [(String, String)], SV)
-> (Bool, [(String, String)], SV)
-> Seq (Bool, [(String, String)], SV)
forall a. Seq a -> a -> Seq a
S.|> (Bool, [(String, String)], SV)
c)
                                                            (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ State
-> (IncState -> IORef (Seq (Bool, [(String, String)], SV)))
-> (Seq (Bool, [(String, String)], SV)
    -> Seq (Bool, [(String, String)], SV))
-> IO ()
forall a. State -> (IncState -> IORef a) -> (a -> a) -> IO ()
modifyIncState State
st IncState -> IORef (Seq (Bool, [(String, String)], SV))
rNewConstraints (Seq (Bool, [(String, String)], SV)
-> (Bool, [(String, String)], SV)
-> Seq (Bool, [(String, String)], SV)
forall a. Seq a -> a -> Seq a
S.|> (Bool, [(String, String)], SV)
c)

-- | Generalization of 'Data.SBV.addSValOptGoal'
addSValOptGoal :: MonadSymbolic m => Objective SVal -> m ()
addSValOptGoal :: Objective SVal -> m ()
addSValOptGoal obj :: Objective SVal
obj = do State
st <- m State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv

                        -- create the tracking variable here for the metric
                        let mkGoal :: String -> SVal -> m (SV, SV)
mkGoal nm :: String
nm orig :: SVal
orig = IO (SV, SV) -> m (SV, SV)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (SV, SV) -> m (SV, SV)) -> IO (SV, SV) -> m (SV, SV)
forall a b. (a -> b) -> a -> b
$ do SV
origSV  <- State -> SVal -> IO SV
svToSV State
st SVal
orig
                                                         SVal
track   <- Kind -> String -> State -> IO SVal
svMkTrackerVar (SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
orig) String
nm State
st
                                                         SV
trackSV <- State -> SVal -> IO SV
svToSV State
st SVal
track
                                                         (SV, SV) -> IO (SV, SV)
forall (m :: * -> *) a. Monad m => a -> m a
return (SV
origSV, SV
trackSV)

                        let walk :: Objective SVal -> m (Objective (SV, SV))
walk (Minimize          nm :: String
nm v :: SVal
v)     = String -> (SV, SV) -> Objective (SV, SV)
forall a. String -> a -> Objective a
Minimize String
nm                     ((SV, SV) -> Objective (SV, SV))
-> m (SV, SV) -> m (Objective (SV, SV))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> SVal -> m (SV, SV)
mkGoal String
nm SVal
v
                            walk (Maximize          nm :: String
nm v :: SVal
v)     = String -> (SV, SV) -> Objective (SV, SV)
forall a. String -> a -> Objective a
Maximize String
nm                     ((SV, SV) -> Objective (SV, SV))
-> m (SV, SV) -> m (Objective (SV, SV))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> SVal -> m (SV, SV)
mkGoal String
nm SVal
v
                            walk (AssertWithPenalty nm :: String
nm v :: SVal
v mbP :: Penalty
mbP) = ((SV, SV) -> Penalty -> Objective (SV, SV))
-> Penalty -> (SV, SV) -> Objective (SV, SV)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (String -> (SV, SV) -> Penalty -> Objective (SV, SV)
forall a. String -> a -> Penalty -> Objective a
AssertWithPenalty String
nm) Penalty
mbP ((SV, SV) -> Objective (SV, SV))
-> m (SV, SV) -> m (Objective (SV, SV))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> SVal -> m (SV, SV)
mkGoal String
nm SVal
v

                        Objective (SV, SV)
obj' <- Objective SVal -> m (Objective (SV, SV))
walk Objective SVal
obj
                        IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ State
-> (State -> IORef [Objective (SV, SV)])
-> ([Objective (SV, SV)] -> [Objective (SV, SV)])
-> IO ()
-> IO ()
forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State -> IORef [Objective (SV, SV)]
rOptGoals (Objective (SV, SV)
obj' Objective (SV, SV) -> [Objective (SV, SV)] -> [Objective (SV, SV)]
forall a. a -> [a] -> [a]
:)
                                           (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> IO ()
forall a. [String] -> a
noInteractive [ "Adding an optimization objective:"
                                                           , "  Objective: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Objective SVal -> String
forall a. Show a => a -> String
show Objective SVal
obj
                                                           ]

-- | Generalization of 'Data.SBV.outputSVal'
outputSVal :: MonadSymbolic m => SVal -> m ()
outputSVal :: SVal -> m ()
outputSVal (SVal _ (Left c :: CV
c)) = do
  State
st <- m State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv
  SV
sv <- IO SV -> m SV
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SV -> m SV) -> IO SV -> m SV
forall a b. (a -> b) -> a -> b
$ State -> CV -> IO SV
newConst State
st CV
c
  IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ State -> (State -> IORef [SV]) -> ([SV] -> [SV]) -> IO () -> IO ()
forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State -> IORef [SV]
routs (SV
svSV -> [SV] -> [SV]
forall a. a -> [a] -> [a]
:) (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
outputSVal (SVal _ (Right f :: Cached SV
f)) = do
  State
st <- m State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv
  SV
sv <- IO SV -> m SV
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SV -> m SV) -> IO SV -> m SV
forall a b. (a -> b) -> a -> b
$ Cached SV -> State -> IO SV
uncache Cached SV
f State
st
  IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ State -> (State -> IORef [SV]) -> ([SV] -> [SV]) -> IO () -> IO ()
forall a. State -> (State -> IORef a) -> (a -> a) -> IO () -> IO ()
modifyState State
st State -> IORef [SV]
routs (SV
svSV -> [SV] -> [SV]
forall a. a -> [a] -> [a]
:) (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())

---------------------------------------------------------------------------------
-- * Cached values
---------------------------------------------------------------------------------

-- | We implement a peculiar caching mechanism, applicable to the use case in
-- implementation of SBV's.  Whenever we do a state based computation, we do
-- not want to keep on evaluating it in the then-current state. That will
-- produce essentially a semantically equivalent value. Thus, we want to run
-- it only once, and reuse that result, capturing the sharing at the Haskell
-- level. This is similar to the "type-safe observable sharing" work, but also
-- takes into the account of how symbolic simulation executes.
--
-- See Andy Gill's type-safe obervable sharing trick for the inspiration behind
-- this technique: <http://ku-fpg.github.io/files/Gill-09-TypeSafeReification.pdf>
--
-- Note that this is *not* a general memo utility!
newtype Cached a = Cached (State -> IO a)

-- | Cache a state-based computation
cache :: (State -> IO a) -> Cached a
cache :: (State -> IO a) -> Cached a
cache = (State -> IO a) -> Cached a
forall a. (State -> IO a) -> Cached a
Cached

-- | Uncache a previously cached computation
uncache :: Cached SV -> State -> IO SV
uncache :: Cached SV -> State -> IO SV
uncache = (State -> IORef (Cache SV)) -> Cached SV -> State -> IO SV
forall a. (State -> IORef (Cache a)) -> Cached a -> State -> IO a
uncacheGen State -> IORef (Cache SV)
rSVCache

-- | An SMT array index is simply an int value
newtype ArrayIndex = ArrayIndex { ArrayIndex -> Int
unArrayIndex :: Int } deriving (ArrayIndex -> ArrayIndex -> Bool
(ArrayIndex -> ArrayIndex -> Bool)
-> (ArrayIndex -> ArrayIndex -> Bool) -> Eq ArrayIndex
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ArrayIndex -> ArrayIndex -> Bool
$c/= :: ArrayIndex -> ArrayIndex -> Bool
== :: ArrayIndex -> ArrayIndex -> Bool
$c== :: ArrayIndex -> ArrayIndex -> Bool
Eq, Eq ArrayIndex
Eq ArrayIndex =>
(ArrayIndex -> ArrayIndex -> Ordering)
-> (ArrayIndex -> ArrayIndex -> Bool)
-> (ArrayIndex -> ArrayIndex -> Bool)
-> (ArrayIndex -> ArrayIndex -> Bool)
-> (ArrayIndex -> ArrayIndex -> Bool)
-> (ArrayIndex -> ArrayIndex -> ArrayIndex)
-> (ArrayIndex -> ArrayIndex -> ArrayIndex)
-> Ord ArrayIndex
ArrayIndex -> ArrayIndex -> Bool
ArrayIndex -> ArrayIndex -> Ordering
ArrayIndex -> ArrayIndex -> ArrayIndex
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ArrayIndex -> ArrayIndex -> ArrayIndex
$cmin :: ArrayIndex -> ArrayIndex -> ArrayIndex
max :: ArrayIndex -> ArrayIndex -> ArrayIndex
$cmax :: ArrayIndex -> ArrayIndex -> ArrayIndex
>= :: ArrayIndex -> ArrayIndex -> Bool
$c>= :: ArrayIndex -> ArrayIndex -> Bool
> :: ArrayIndex -> ArrayIndex -> Bool
$c> :: ArrayIndex -> ArrayIndex -> Bool
<= :: ArrayIndex -> ArrayIndex -> Bool
$c<= :: ArrayIndex -> ArrayIndex -> Bool
< :: ArrayIndex -> ArrayIndex -> Bool
$c< :: ArrayIndex -> ArrayIndex -> Bool
compare :: ArrayIndex -> ArrayIndex -> Ordering
$ccompare :: ArrayIndex -> ArrayIndex -> Ordering
$cp1Ord :: Eq ArrayIndex
Ord)

-- | We simply show indexes as the underlying integer
instance Show ArrayIndex where
  show :: ArrayIndex -> String
show (ArrayIndex i :: Int
i) = Int -> String
forall a. Show a => a -> String
show Int
i

-- | A functional array index is simply an int value
newtype FArrayIndex = FArrayIndex { FArrayIndex -> Int
unFArrayIndex :: Int } deriving (FArrayIndex -> FArrayIndex -> Bool
(FArrayIndex -> FArrayIndex -> Bool)
-> (FArrayIndex -> FArrayIndex -> Bool) -> Eq FArrayIndex
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FArrayIndex -> FArrayIndex -> Bool
$c/= :: FArrayIndex -> FArrayIndex -> Bool
== :: FArrayIndex -> FArrayIndex -> Bool
$c== :: FArrayIndex -> FArrayIndex -> Bool
Eq, Eq FArrayIndex
Eq FArrayIndex =>
(FArrayIndex -> FArrayIndex -> Ordering)
-> (FArrayIndex -> FArrayIndex -> Bool)
-> (FArrayIndex -> FArrayIndex -> Bool)
-> (FArrayIndex -> FArrayIndex -> Bool)
-> (FArrayIndex -> FArrayIndex -> Bool)
-> (FArrayIndex -> FArrayIndex -> FArrayIndex)
-> (FArrayIndex -> FArrayIndex -> FArrayIndex)
-> Ord FArrayIndex
FArrayIndex -> FArrayIndex -> Bool
FArrayIndex -> FArrayIndex -> Ordering
FArrayIndex -> FArrayIndex -> FArrayIndex
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: FArrayIndex -> FArrayIndex -> FArrayIndex
$cmin :: FArrayIndex -> FArrayIndex -> FArrayIndex
max :: FArrayIndex -> FArrayIndex -> FArrayIndex
$cmax :: FArrayIndex -> FArrayIndex -> FArrayIndex
>= :: FArrayIndex -> FArrayIndex -> Bool
$c>= :: FArrayIndex -> FArrayIndex -> Bool
> :: FArrayIndex -> FArrayIndex -> Bool
$c> :: FArrayIndex -> FArrayIndex -> Bool
<= :: FArrayIndex -> FArrayIndex -> Bool
$c<= :: FArrayIndex -> FArrayIndex -> Bool
< :: FArrayIndex -> FArrayIndex -> Bool
$c< :: FArrayIndex -> FArrayIndex -> Bool
compare :: FArrayIndex -> FArrayIndex -> Ordering
$ccompare :: FArrayIndex -> FArrayIndex -> Ordering
$cp1Ord :: Eq FArrayIndex
Ord)

-- | We simply show indexes as the underlying integer
instance Show FArrayIndex where
  show :: FArrayIndex -> String
show (FArrayIndex i :: Int
i) = Int -> String
forall a. Show a => a -> String
show Int
i

-- | Uncache, retrieving SMT array indexes
uncacheAI :: Cached ArrayIndex -> State -> IO ArrayIndex
uncacheAI :: Cached ArrayIndex -> State -> IO ArrayIndex
uncacheAI = (State -> IORef (Cache ArrayIndex))
-> Cached ArrayIndex -> State -> IO ArrayIndex
forall a. (State -> IORef (Cache a)) -> Cached a -> State -> IO a
uncacheGen State -> IORef (Cache ArrayIndex)
rAICache

-- | Uncache, retrieving Functional array indexes
uncacheFAI :: Cached FArrayIndex -> State -> IO FArrayIndex
uncacheFAI :: Cached FArrayIndex -> State -> IO FArrayIndex
uncacheFAI = (State -> IORef (Cache FArrayIndex))
-> Cached FArrayIndex -> State -> IO FArrayIndex
forall a. (State -> IORef (Cache a)) -> Cached a -> State -> IO a
uncacheGen State -> IORef (Cache FArrayIndex)
rFAICache

-- | Generic uncaching. Note that this is entirely safe, since we do it in the IO monad.
uncacheGen :: (State -> IORef (Cache a)) -> Cached a -> State -> IO a
uncacheGen :: (State -> IORef (Cache a)) -> Cached a -> State -> IO a
uncacheGen getCache :: State -> IORef (Cache a)
getCache (Cached f :: State -> IO a
f) st :: State
st = do
        let rCache :: IORef (Cache a)
rCache = State -> IORef (Cache a)
getCache State
st
        Cache a
stored <- IORef (Cache a) -> IO (Cache a)
forall a. IORef a -> IO a
readIORef IORef (Cache a)
rCache
        StableName (State -> IO a)
sn <- State -> IO a
f (State -> IO a)
-> IO (StableName (State -> IO a))
-> IO (StableName (State -> IO a))
forall a b. a -> b -> b
`seq` (State -> IO a) -> IO (StableName (State -> IO a))
forall a. a -> IO (StableName a)
makeStableName State -> IO a
f
        let h :: Int
h = StableName (State -> IO a) -> Int
forall a. StableName a -> Int
hashStableName StableName (State -> IO a)
sn
        case (Int
h Int -> Cache a -> Maybe [(StableName (State -> IO a), a)]
forall a. Int -> IntMap a -> Maybe a
`IMap.lookup` Cache a
stored) Maybe [(StableName (State -> IO a), a)]
-> ([(StableName (State -> IO a), a)] -> Maybe a) -> Maybe a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (StableName (State -> IO a)
sn StableName (State -> IO a)
-> [(StableName (State -> IO a), a)] -> Maybe a
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup`) of
          Just r :: a
r  -> a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r
          Nothing -> do a
r <- State -> IO a
f State
st
                        a
r a -> IO () -> IO ()
forall a b. a -> b -> b
`seq` IORef (Cache a) -> (Cache a -> Cache a) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
R.modifyIORef' IORef (Cache a)
rCache (([(StableName (State -> IO a), a)]
 -> [(StableName (State -> IO a), a)]
 -> [(StableName (State -> IO a), a)])
-> Int -> [(StableName (State -> IO a), a)] -> Cache a -> Cache a
forall a. (a -> a -> a) -> Int -> a -> IntMap a -> IntMap a
IMap.insertWith [(StableName (State -> IO a), a)]
-> [(StableName (State -> IO a), a)]
-> [(StableName (State -> IO a), a)]
forall a. [a] -> [a] -> [a]
(++) Int
h [(StableName (State -> IO a)
sn, a
r)])
                        a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r

-- | Representation of SMTLib Program versions. As of June 2015, we're dropping support
-- for SMTLib1, and supporting SMTLib2 only. We keep this data-type around in case
-- SMTLib3 comes along and we want to support 2 and 3 simultaneously.
data SMTLibVersion = SMTLib2
                   deriving (SMTLibVersion
SMTLibVersion -> SMTLibVersion -> Bounded SMTLibVersion
forall a. a -> a -> Bounded a
maxBound :: SMTLibVersion
$cmaxBound :: SMTLibVersion
minBound :: SMTLibVersion
$cminBound :: SMTLibVersion
Bounded, Int -> SMTLibVersion
SMTLibVersion -> Int
SMTLibVersion -> [SMTLibVersion]
SMTLibVersion -> SMTLibVersion
SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]
SMTLibVersion -> SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]
(SMTLibVersion -> SMTLibVersion)
-> (SMTLibVersion -> SMTLibVersion)
-> (Int -> SMTLibVersion)
-> (SMTLibVersion -> Int)
-> (SMTLibVersion -> [SMTLibVersion])
-> (SMTLibVersion -> SMTLibVersion -> [SMTLibVersion])
-> (SMTLibVersion -> SMTLibVersion -> [SMTLibVersion])
-> (SMTLibVersion
    -> SMTLibVersion -> SMTLibVersion -> [SMTLibVersion])
-> Enum SMTLibVersion
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: SMTLibVersion -> SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]
$cenumFromThenTo :: SMTLibVersion -> SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]
enumFromTo :: SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]
$cenumFromTo :: SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]
enumFromThen :: SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]
$cenumFromThen :: SMTLibVersion -> SMTLibVersion -> [SMTLibVersion]
enumFrom :: SMTLibVersion -> [SMTLibVersion]
$cenumFrom :: SMTLibVersion -> [SMTLibVersion]
fromEnum :: SMTLibVersion -> Int
$cfromEnum :: SMTLibVersion -> Int
toEnum :: Int -> SMTLibVersion
$ctoEnum :: Int -> SMTLibVersion
pred :: SMTLibVersion -> SMTLibVersion
$cpred :: SMTLibVersion -> SMTLibVersion
succ :: SMTLibVersion -> SMTLibVersion
$csucc :: SMTLibVersion -> SMTLibVersion
Enum, SMTLibVersion -> SMTLibVersion -> Bool
(SMTLibVersion -> SMTLibVersion -> Bool)
-> (SMTLibVersion -> SMTLibVersion -> Bool) -> Eq SMTLibVersion
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SMTLibVersion -> SMTLibVersion -> Bool
$c/= :: SMTLibVersion -> SMTLibVersion -> Bool
== :: SMTLibVersion -> SMTLibVersion -> Bool
$c== :: SMTLibVersion -> SMTLibVersion -> Bool
Eq, Int -> SMTLibVersion -> ShowS
[SMTLibVersion] -> ShowS
SMTLibVersion -> String
(Int -> SMTLibVersion -> ShowS)
-> (SMTLibVersion -> String)
-> ([SMTLibVersion] -> ShowS)
-> Show SMTLibVersion
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SMTLibVersion] -> ShowS
$cshowList :: [SMTLibVersion] -> ShowS
show :: SMTLibVersion -> String
$cshow :: SMTLibVersion -> String
showsPrec :: Int -> SMTLibVersion -> ShowS
$cshowsPrec :: Int -> SMTLibVersion -> ShowS
Show)

-- | The extension associated with the version
smtLibVersionExtension :: SMTLibVersion -> String
smtLibVersionExtension :: SMTLibVersion -> String
smtLibVersionExtension SMTLib2 = "smt2"

-- | Representation of an SMT-Lib program. In between pre and post goes the refuted models
data SMTLibPgm = SMTLibPgm SMTLibVersion [String]

instance NFData SMTLibVersion where rnf :: SMTLibVersion -> ()
rnf a :: SMTLibVersion
a               = SMTLibVersion
a SMTLibVersion -> () -> ()
forall a b. a -> b -> b
`seq` ()
instance NFData SMTLibPgm     where rnf :: SMTLibPgm -> ()
rnf (SMTLibPgm v :: SMTLibVersion
v p :: [String]
p) = SMTLibVersion -> ()
forall a. NFData a => a -> ()
rnf SMTLibVersion
v () -> () -> ()
forall a b. a -> b -> b
`seq` [String] -> ()
forall a. NFData a => a -> ()
rnf [String]
p

instance Show SMTLibPgm where
  show :: SMTLibPgm -> String
show (SMTLibPgm _ pre :: [String]
pre) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n" [String]
pre

-- Other Technicalities..
instance NFData CV where
  rnf :: CV -> ()
rnf (CV x :: Kind
x y :: CVal
y) = Kind
x Kind -> () -> ()
forall a b. a -> b -> b
`seq` CVal
y CVal -> () -> ()
forall a b. a -> b -> b
`seq` ()

instance NFData GeneralizedCV where
  rnf :: GeneralizedCV -> ()
rnf (ExtendedCV e :: ExtCV
e) = ExtCV
e ExtCV -> () -> ()
forall a b. a -> b -> b
`seq` ()
  rnf (RegularCV  c :: CV
c) = CV
c CV -> () -> ()
forall a b. a -> b -> b
`seq` ()

#if MIN_VERSION_base(4,9,0)
#else
-- Can't really force this, but not a big deal
instance NFData CallStack where
  rnf _ = ()
#endif

instance NFData Result where
  rnf :: Result -> ()
rnf (Result kindInfo :: Set Kind
kindInfo qcInfo :: [(String, CV)]
qcInfo obs :: [(String, CV -> Bool, SV)]
obs cgs :: [(String, [String])]
cgs inps :: ([(Quantifier, NamedSymVar)], [NamedSymVar])
inps consts :: [(SV, CV)]
consts tbls :: [((Int, Kind, Kind), [SV])]
tbls arrs :: [(Int, ArrayInfo)]
arrs uis :: [(String, SBVType)]
uis axs :: [(String, [String])]
axs pgm :: SBVPgm
pgm cstr :: Seq (Bool, [(String, String)], SV)
cstr asserts :: [(String, Maybe CallStack, SV)]
asserts outs :: [SV]
outs)
        = Set Kind -> ()
forall a. NFData a => a -> ()
rnf Set Kind
kindInfo () -> () -> ()
forall a b. a -> b -> b
`seq` [(String, CV)] -> ()
forall a. NFData a => a -> ()
rnf [(String, CV)]
qcInfo  () -> () -> ()
forall a b. a -> b -> b
`seq` [(String, CV -> Bool, SV)] -> ()
forall a. NFData a => a -> ()
rnf [(String, CV -> Bool, SV)]
obs    () -> () -> ()
forall a b. a -> b -> b
`seq` [(String, [String])] -> ()
forall a. NFData a => a -> ()
rnf [(String, [String])]
cgs
                       () -> () -> ()
forall a b. a -> b -> b
`seq` ([(Quantifier, NamedSymVar)], [NamedSymVar]) -> ()
forall a. NFData a => a -> ()
rnf ([(Quantifier, NamedSymVar)], [NamedSymVar])
inps    () -> () -> ()
forall a b. a -> b -> b
`seq` [(SV, CV)] -> ()
forall a. NFData a => a -> ()
rnf [(SV, CV)]
consts () -> () -> ()
forall a b. a -> b -> b
`seq` [((Int, Kind, Kind), [SV])] -> ()
forall a. NFData a => a -> ()
rnf [((Int, Kind, Kind), [SV])]
tbls
                       () -> () -> ()
forall a b. a -> b -> b
`seq` [(Int, ArrayInfo)] -> ()
forall a. NFData a => a -> ()
rnf [(Int, ArrayInfo)]
arrs    () -> () -> ()
forall a b. a -> b -> b
`seq` [(String, SBVType)] -> ()
forall a. NFData a => a -> ()
rnf [(String, SBVType)]
uis    () -> () -> ()
forall a b. a -> b -> b
`seq` [(String, [String])] -> ()
forall a. NFData a => a -> ()
rnf [(String, [String])]
axs
                       () -> () -> ()
forall a b. a -> b -> b
`seq` SBVPgm -> ()
forall a. NFData a => a -> ()
rnf SBVPgm
pgm     () -> () -> ()
forall a b. a -> b -> b
`seq` Seq (Bool, [(String, String)], SV) -> ()
forall a. NFData a => a -> ()
rnf Seq (Bool, [(String, String)], SV)
cstr   () -> () -> ()
forall a b. a -> b -> b
`seq` [(String, Maybe CallStack, SV)] -> ()
forall a. NFData a => a -> ()
rnf [(String, Maybe CallStack, SV)]
asserts
                       () -> () -> ()
forall a b. a -> b -> b
`seq` [SV] -> ()
forall a. NFData a => a -> ()
rnf [SV]
outs
instance NFData Kind         where rnf :: Kind -> ()
rnf a :: Kind
a          = Kind -> () -> ()
forall a b. a -> b -> b
seq Kind
a ()
instance NFData ArrayContext where rnf :: ArrayContext -> ()
rnf a :: ArrayContext
a          = ArrayContext -> () -> ()
forall a b. a -> b -> b
seq ArrayContext
a ()
instance NFData SV           where rnf :: SV -> ()
rnf a :: SV
a          = SV -> () -> ()
forall a b. a -> b -> b
seq SV
a ()
instance NFData SBVExpr      where rnf :: SBVExpr -> ()
rnf a :: SBVExpr
a          = SBVExpr -> () -> ()
forall a b. a -> b -> b
seq SBVExpr
a ()
instance NFData Quantifier   where rnf :: Quantifier -> ()
rnf a :: Quantifier
a          = Quantifier -> () -> ()
forall a b. a -> b -> b
seq Quantifier
a ()
instance NFData SBVType      where rnf :: SBVType -> ()
rnf a :: SBVType
a          = SBVType -> () -> ()
forall a b. a -> b -> b
seq SBVType
a ()
instance NFData SBVPgm       where rnf :: SBVPgm -> ()
rnf a :: SBVPgm
a          = SBVPgm -> () -> ()
forall a b. a -> b -> b
seq SBVPgm
a ()
instance NFData (Cached a)   where rnf :: Cached a -> ()
rnf (Cached f :: State -> IO a
f) = State -> IO a
f (State -> IO a) -> () -> ()
forall a b. a -> b -> b
`seq` ()
instance NFData SVal         where rnf :: SVal -> ()
rnf (SVal x :: Kind
x y :: Either CV (Cached SV)
y) = Kind -> ()
forall a. NFData a => a -> ()
rnf Kind
x () -> () -> ()
forall a b. a -> b -> b
`seq` Either CV (Cached SV) -> ()
forall a. NFData a => a -> ()
rnf Either CV (Cached SV)
y

instance NFData SMTResult where
  rnf :: SMTResult -> ()
rnf (Unsatisfiable _ xs :: Maybe [String]
xs   ) = Maybe [String] -> ()
forall a. NFData a => a -> ()
rnf Maybe [String]
xs
  rnf (Satisfiable _   xs :: SMTModel
xs   ) = SMTModel -> ()
forall a. NFData a => a -> ()
rnf SMTModel
xs
  rnf (SatExtField _   xs :: SMTModel
xs   ) = SMTModel -> ()
forall a. NFData a => a -> ()
rnf SMTModel
xs
  rnf (Unknown _       xs :: SMTReasonUnknown
xs   ) = SMTReasonUnknown -> ()
forall a. NFData a => a -> ()
rnf SMTReasonUnknown
xs
  rnf (ProofError _    xs :: [String]
xs mr :: Maybe SMTResult
mr) = [String] -> ()
forall a. NFData a => a -> ()
rnf [String]
xs () -> () -> ()
forall a b. a -> b -> b
`seq` Maybe SMTResult -> ()
forall a. NFData a => a -> ()
rnf Maybe SMTResult
mr

instance NFData SMTModel where
  rnf :: SMTModel -> ()
rnf (SMTModel objs :: [(String, GeneralizedCV)]
objs bndgs :: Maybe [((Quantifier, NamedSymVar), Maybe CV)]
bndgs assocs :: [(String, CV)]
assocs uifuns :: [(String, (SBVType, ([([CV], CV)], CV)))]
uifuns) = [(String, GeneralizedCV)] -> ()
forall a. NFData a => a -> ()
rnf [(String, GeneralizedCV)]
objs () -> () -> ()
forall a b. a -> b -> b
`seq` Maybe [((Quantifier, NamedSymVar), Maybe CV)] -> ()
forall a. NFData a => a -> ()
rnf Maybe [((Quantifier, NamedSymVar), Maybe CV)]
bndgs () -> () -> ()
forall a b. a -> b -> b
`seq` [(String, CV)] -> ()
forall a. NFData a => a -> ()
rnf [(String, CV)]
assocs () -> () -> ()
forall a b. a -> b -> b
`seq` [(String, (SBVType, ([([CV], CV)], CV)))] -> ()
forall a. NFData a => a -> ()
rnf [(String, (SBVType, ([([CV], CV)], CV)))]
uifuns

instance NFData SMTScript where
  rnf :: SMTScript -> ()
rnf (SMTScript b :: String
b m :: [String]
m) = String -> ()
forall a. NFData a => a -> ()
rnf String
b () -> () -> ()
forall a b. a -> b -> b
`seq` [String] -> ()
forall a. NFData a => a -> ()
rnf [String]
m

-- | Translation tricks needed for specific capabilities afforded by each solver
data SolverCapabilities = SolverCapabilities {
         SolverCapabilities -> Bool
supportsQuantifiers        :: Bool           -- ^ Supports SMT-Lib2 style quantifiers?
       , SolverCapabilities -> Bool
supportsUninterpretedSorts :: Bool           -- ^ Supports SMT-Lib2 style uninterpreted-sorts
       , SolverCapabilities -> Bool
supportsUnboundedInts      :: Bool           -- ^ Supports unbounded integers?
       , SolverCapabilities -> Bool
supportsReals              :: Bool           -- ^ Supports reals?
       , SolverCapabilities -> Bool
supportsApproxReals        :: Bool           -- ^ Supports printing of approximations of reals?
       , SolverCapabilities -> Bool
supportsIEEE754            :: Bool           -- ^ Supports floating point numbers?
       , SolverCapabilities -> Bool
supportsSets               :: Bool           -- ^ Supports set operations?
       , SolverCapabilities -> Bool
supportsOptimization       :: Bool           -- ^ Supports optimization routines?
       , SolverCapabilities -> Bool
supportsPseudoBooleans     :: Bool           -- ^ Supports pseudo-boolean operations?
       , SolverCapabilities -> Bool
supportsCustomQueries      :: Bool           -- ^ Supports interactive queries per SMT-Lib?
       , SolverCapabilities -> Bool
supportsGlobalDecls        :: Bool           -- ^ Supports global declarations? (Needed for push-pop.)
       , SolverCapabilities -> Bool
supportsDataTypes          :: Bool           -- ^ Supports datatypes?
       , SolverCapabilities -> Maybe [String]
supportsFlattenedModels    :: Maybe [String] -- ^ Supports flattened model output? (With given config lines.)
       }

-- | Rounding mode to be used for the IEEE floating-point operations.
-- Note that Haskell's default is 'RoundNearestTiesToEven'. If you use
-- a different rounding mode, then the counter-examples you get may not
-- match what you observe in Haskell.
data RoundingMode = RoundNearestTiesToEven  -- ^ Round to nearest representable floating point value.
                                            -- If precisely at half-way, pick the even number.
                                            -- (In this context, /even/ means the lowest-order bit is zero.)
                  | RoundNearestTiesToAway  -- ^ Round to nearest representable floating point value.
                                            -- If precisely at half-way, pick the number further away from 0.
                                            -- (That is, for positive values, pick the greater; for negative values, pick the smaller.)
                  | RoundTowardPositive     -- ^ Round towards positive infinity. (Also known as rounding-up or ceiling.)
                  | RoundTowardNegative     -- ^ Round towards negative infinity. (Also known as rounding-down or floor.)
                  | RoundTowardZero         -- ^ Round towards zero. (Also known as truncation.)
                  deriving (RoundingMode -> RoundingMode -> Bool
(RoundingMode -> RoundingMode -> Bool)
-> (RoundingMode -> RoundingMode -> Bool) -> Eq RoundingMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RoundingMode -> RoundingMode -> Bool
$c/= :: RoundingMode -> RoundingMode -> Bool
== :: RoundingMode -> RoundingMode -> Bool
$c== :: RoundingMode -> RoundingMode -> Bool
Eq, Eq RoundingMode
Eq RoundingMode =>
(RoundingMode -> RoundingMode -> Ordering)
-> (RoundingMode -> RoundingMode -> Bool)
-> (RoundingMode -> RoundingMode -> Bool)
-> (RoundingMode -> RoundingMode -> Bool)
-> (RoundingMode -> RoundingMode -> Bool)
-> (RoundingMode -> RoundingMode -> RoundingMode)
-> (RoundingMode -> RoundingMode -> RoundingMode)
-> Ord RoundingMode
RoundingMode -> RoundingMode -> Bool
RoundingMode -> RoundingMode -> Ordering
RoundingMode -> RoundingMode -> RoundingMode
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: RoundingMode -> RoundingMode -> RoundingMode
$cmin :: RoundingMode -> RoundingMode -> RoundingMode
max :: RoundingMode -> RoundingMode -> RoundingMode
$cmax :: RoundingMode -> RoundingMode -> RoundingMode
>= :: RoundingMode -> RoundingMode -> Bool
$c>= :: RoundingMode -> RoundingMode -> Bool
> :: RoundingMode -> RoundingMode -> Bool
$c> :: RoundingMode -> RoundingMode -> Bool
<= :: RoundingMode -> RoundingMode -> Bool
$c<= :: RoundingMode -> RoundingMode -> Bool
< :: RoundingMode -> RoundingMode -> Bool
$c< :: RoundingMode -> RoundingMode -> Bool
compare :: RoundingMode -> RoundingMode -> Ordering
$ccompare :: RoundingMode -> RoundingMode -> Ordering
$cp1Ord :: Eq RoundingMode
Ord, Int -> RoundingMode -> ShowS
[RoundingMode] -> ShowS
RoundingMode -> String
(Int -> RoundingMode -> ShowS)
-> (RoundingMode -> String)
-> ([RoundingMode] -> ShowS)
-> Show RoundingMode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RoundingMode] -> ShowS
$cshowList :: [RoundingMode] -> ShowS
show :: RoundingMode -> String
$cshow :: RoundingMode -> String
showsPrec :: Int -> RoundingMode -> ShowS
$cshowsPrec :: Int -> RoundingMode -> ShowS
Show, ReadPrec [RoundingMode]
ReadPrec RoundingMode
Int -> ReadS RoundingMode
ReadS [RoundingMode]
(Int -> ReadS RoundingMode)
-> ReadS [RoundingMode]
-> ReadPrec RoundingMode
-> ReadPrec [RoundingMode]
-> Read RoundingMode
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [RoundingMode]
$creadListPrec :: ReadPrec [RoundingMode]
readPrec :: ReadPrec RoundingMode
$creadPrec :: ReadPrec RoundingMode
readList :: ReadS [RoundingMode]
$creadList :: ReadS [RoundingMode]
readsPrec :: Int -> ReadS RoundingMode
$creadsPrec :: Int -> ReadS RoundingMode
Read, Typeable RoundingMode
DataType
Constr
Typeable RoundingMode =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> RoundingMode -> c RoundingMode)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c RoundingMode)
-> (RoundingMode -> Constr)
-> (RoundingMode -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c RoundingMode))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c RoundingMode))
-> ((forall b. Data b => b -> b) -> RoundingMode -> RoundingMode)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> RoundingMode -> r)
-> (forall u. (forall d. Data d => d -> u) -> RoundingMode -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> RoundingMode -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode)
-> Data RoundingMode
RoundingMode -> DataType
RoundingMode -> Constr
(forall b. Data b => b -> b) -> RoundingMode -> RoundingMode
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RoundingMode -> c RoundingMode
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RoundingMode
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> RoundingMode -> u
forall u. (forall d. Data d => d -> u) -> RoundingMode -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RoundingMode
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RoundingMode -> c RoundingMode
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RoundingMode)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c RoundingMode)
$cRoundTowardZero :: Constr
$cRoundTowardNegative :: Constr
$cRoundTowardPositive :: Constr
$cRoundNearestTiesToAway :: Constr
$cRoundNearestTiesToEven :: Constr
$tRoundingMode :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
gmapMp :: (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
gmapM :: (forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RoundingMode -> m RoundingMode
gmapQi :: Int -> (forall d. Data d => d -> u) -> RoundingMode -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> RoundingMode -> u
gmapQ :: (forall d. Data d => d -> u) -> RoundingMode -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> RoundingMode -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RoundingMode -> r
gmapT :: (forall b. Data b => b -> b) -> RoundingMode -> RoundingMode
$cgmapT :: (forall b. Data b => b -> b) -> RoundingMode -> RoundingMode
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c RoundingMode)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c RoundingMode)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c RoundingMode)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RoundingMode)
dataTypeOf :: RoundingMode -> DataType
$cdataTypeOf :: RoundingMode -> DataType
toConstr :: RoundingMode -> Constr
$ctoConstr :: RoundingMode -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RoundingMode
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RoundingMode
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RoundingMode -> c RoundingMode
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RoundingMode -> c RoundingMode
$cp1Data :: Typeable RoundingMode
G.Data, RoundingMode
RoundingMode -> RoundingMode -> Bounded RoundingMode
forall a. a -> a -> Bounded a
maxBound :: RoundingMode
$cmaxBound :: RoundingMode
minBound :: RoundingMode
$cminBound :: RoundingMode
Bounded, Int -> RoundingMode
RoundingMode -> Int
RoundingMode -> [RoundingMode]
RoundingMode -> RoundingMode
RoundingMode -> RoundingMode -> [RoundingMode]
RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode]
(RoundingMode -> RoundingMode)
-> (RoundingMode -> RoundingMode)
-> (Int -> RoundingMode)
-> (RoundingMode -> Int)
-> (RoundingMode -> [RoundingMode])
-> (RoundingMode -> RoundingMode -> [RoundingMode])
-> (RoundingMode -> RoundingMode -> [RoundingMode])
-> (RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode])
-> Enum RoundingMode
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode]
$cenumFromThenTo :: RoundingMode -> RoundingMode -> RoundingMode -> [RoundingMode]
enumFromTo :: RoundingMode -> RoundingMode -> [RoundingMode]
$cenumFromTo :: RoundingMode -> RoundingMode -> [RoundingMode]
enumFromThen :: RoundingMode -> RoundingMode -> [RoundingMode]
$cenumFromThen :: RoundingMode -> RoundingMode -> [RoundingMode]
enumFrom :: RoundingMode -> [RoundingMode]
$cenumFrom :: RoundingMode -> [RoundingMode]
fromEnum :: RoundingMode -> Int
$cfromEnum :: RoundingMode -> Int
toEnum :: Int -> RoundingMode
$ctoEnum :: Int -> RoundingMode
pred :: RoundingMode -> RoundingMode
$cpred :: RoundingMode -> RoundingMode
succ :: RoundingMode -> RoundingMode
$csucc :: RoundingMode -> RoundingMode
Enum)

-- | 'RoundingMode' kind
instance HasKind RoundingMode

-- | Solver configuration. See also 'Data.SBV.z3', 'Data.SBV.yices', 'Data.SBV.cvc4', 'Data.SBV.boolector', 'Data.SBV.mathSAT', etc.
-- which are instantiations of this type for those solvers, with reasonable defaults. In particular, custom configuration can be
-- created by varying those values. (Such as @z3{verbose=True}@.)
--
-- Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does
-- not necessarily have finite decimal representations, and hence we have to stop printing at some depth. It is important to
-- emphasize that such values always have infinite precision internally. The issue is merely with how we print such an infinite
-- precision value on the screen. The field 'printRealPrec' controls the printing precision, by specifying the number of digits after
-- the decimal point. The default value is 16, but it can be set to any positive integer.
--
-- When printing, SBV will add the suffix @...@ at the and of a real-value, if the given bound is not sufficient to represent the real-value
-- exactly. Otherwise, the number will be written out in standard decimal notation. Note that SBV will always print the whole value if it
-- is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation
-- of the real value is not finite, i.e., if it is not rational.
--
-- The 'printBase' field can be used to print numbers in base 2, 10, or 16. If base 2 or 16 is used, then floating-point values will
-- be printed in their internal memory-layout format as well, which can come in handy for bit-precise analysis.
data SMTConfig = SMTConfig {
         SMTConfig -> Bool
verbose                     :: Bool           -- ^ Debug mode
       , SMTConfig -> Timing
timing                      :: Timing         -- ^ Print timing information on how long different phases took (construction, solving, etc.)
       , SMTConfig -> Int
printBase                   :: Int            -- ^ Print integral literals in this base (2, 10, and 16 are supported.)
       , SMTConfig -> Int
printRealPrec               :: Int            -- ^ Print algebraic real values with this precision. (SReal, default: 16)
       , SMTConfig -> String
satCmd                      :: String         -- ^ Usually "(check-sat)". However, users might tweak it based on solver characteristics.
       , SMTConfig -> Maybe Int
allSatMaxModelCount         :: Maybe Int      -- ^ In a 'Data.SBV.allSat' call, return at most this many models. If nothing, return all.
       , SMTConfig -> Bool
allSatPrintAlong            :: Bool           -- ^ In a 'Data.SBV.allSat' call, print models as they are found.
       , SMTConfig -> Bool
satTrackUFs                 :: Bool           -- ^ In a 'Data.SBV.sat' call, should we try to extract values of uninterpreted functions?
       , SMTConfig -> String -> Bool
isNonModelVar               :: String -> Bool -- ^ When constructing a model, ignore variables whose name satisfy this predicate. (Default: (const False), i.e., don't ignore anything)
       , SMTConfig -> Bool
validateModel               :: Bool           -- ^ If set, SBV will attempt to validate the model it gets back from the solver.
       , SMTConfig -> Bool
optimizeValidateConstraints :: Bool           -- ^ Validate optimization results. NB: Does NOT make sure the model is optimal, just checks they satisfy the constraints.
       , SMTConfig -> Maybe String
transcript                  :: Maybe FilePath -- ^ If Just, the entire interaction will be recorded as a playable file (for debugging purposes mostly)
       , SMTConfig -> SMTLibVersion
smtLibVersion               :: SMTLibVersion  -- ^ What version of SMT-lib we use for the tool
       , SMTConfig -> SMTSolver
solver                      :: SMTSolver      -- ^ The actual SMT solver.
       , SMTConfig -> Bool
allowQuantifiedQueries      :: Bool           -- ^ Should we permit use of quantifiers in the query mode? (Default: False. See <http://github.com/LeventErkok/sbv/issues/459> for why.)
       , SMTConfig -> RoundingMode
roundingMode                :: RoundingMode   -- ^ Rounding mode to use for floating-point conversions
       , SMTConfig -> [SMTOption]
solverSetOptions            :: [SMTOption]    -- ^ Options to set as we start the solver
       , SMTConfig -> Bool
ignoreExitCode              :: Bool           -- ^ If true, we shall ignore the exit code upon exit. Otherwise we require ExitSuccess.
       , SMTConfig -> Maybe String
redirectVerbose             :: Maybe FilePath -- ^ Redirect the verbose output to this file if given. If Nothing, stdout is implied.
       }

-- | Returns true if we have to perform validation
validationRequested :: SMTConfig -> Bool
validationRequested :: SMTConfig -> Bool
validationRequested SMTConfig{Bool
validateModel :: Bool
validateModel :: SMTConfig -> Bool
validateModel, Bool
optimizeValidateConstraints :: Bool
optimizeValidateConstraints :: SMTConfig -> Bool
optimizeValidateConstraints} = Bool
validateModel Bool -> Bool -> Bool
|| Bool
optimizeValidateConstraints

-- We're just seq'ing top-level here, it shouldn't really matter. (i.e., no need to go deeper.)
instance NFData SMTConfig where
  rnf :: SMTConfig -> ()
rnf SMTConfig{} = ()

-- | A model, as returned by a solver
data SMTModel = SMTModel {
       SMTModel -> [(String, GeneralizedCV)]
modelObjectives :: [(String, GeneralizedCV)]                     -- ^ Mapping of symbolic values to objective values.
     , SMTModel -> Maybe [((Quantifier, NamedSymVar), Maybe CV)]
modelBindings   :: Maybe [((Quantifier, NamedSymVar), Maybe CV)] -- ^ Mapping of input variables as reported by the solver. Only collected if model validation is requested.
     , SMTModel -> [(String, CV)]
modelAssocs     :: [(String, CV)]                                -- ^ Mapping of symbolic values to constants.
     , SMTModel -> [(String, (SBVType, ([([CV], CV)], CV)))]
modelUIFuns     :: [(String, (SBVType, ([([CV], CV)], CV)))]     -- ^ Mapping of uninterpreted functions to association lists in the model.
                                                                        -- Note that an uninterpreted constant (function of arity 0) will be stored
                                                                        -- in the 'modelAssocs' field.
     }
     deriving Int -> SMTModel -> ShowS
[SMTModel] -> ShowS
SMTModel -> String
(Int -> SMTModel -> ShowS)
-> (SMTModel -> String) -> ([SMTModel] -> ShowS) -> Show SMTModel
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SMTModel] -> ShowS
$cshowList :: [SMTModel] -> ShowS
show :: SMTModel -> String
$cshow :: SMTModel -> String
showsPrec :: Int -> SMTModel -> ShowS
$cshowsPrec :: Int -> SMTModel -> ShowS
Show

-- | The result of an SMT solver call. Each constructor is tagged with
-- the 'SMTConfig' that created it so that further tools can inspect it
-- and build layers of results, if needed. For ordinary uses of the library,
-- this type should not be needed, instead use the accessor functions on
-- it. (Custom Show instances and model extractors.)
data SMTResult = Unsatisfiable SMTConfig (Maybe [String])            -- ^ Unsatisfiable. If unsat-cores are enabled, they will be returned in the second parameter.
               | Satisfiable   SMTConfig SMTModel                    -- ^ Satisfiable with model
               | SatExtField   SMTConfig SMTModel                    -- ^ Prover returned a model, but in an extension field containing Infinite/epsilon
               | Unknown       SMTConfig SMTReasonUnknown            -- ^ Prover returned unknown, with the given reason
               | ProofError    SMTConfig [String] (Maybe SMTResult)  -- ^ Prover errored out, with possibly a bogus result

-- | A script, to be passed to the solver.
data SMTScript = SMTScript {
          SMTScript -> String
scriptBody  :: String   -- ^ Initial feed
        , SMTScript -> [String]
scriptModel :: [String] -- ^ Continuation script, to extract results
        }

-- | An SMT engine
type SMTEngine =  forall res.
                  SMTConfig         -- ^ current configuration
               -> State             -- ^ the state in which to run the engine
               -> String            -- ^ program
               -> (State -> IO res) -- ^ continuation
               -> IO res

-- | Solvers that SBV is aware of
data Solver = Z3
            | Yices
            | Boolector
            | CVC4
            | MathSAT
            | ABC
            deriving (Int -> Solver -> ShowS
[Solver] -> ShowS
Solver -> String
(Int -> Solver -> ShowS)
-> (Solver -> String) -> ([Solver] -> ShowS) -> Show Solver
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Solver] -> ShowS
$cshowList :: [Solver] -> ShowS
show :: Solver -> String
$cshow :: Solver -> String
showsPrec :: Int -> Solver -> ShowS
$cshowsPrec :: Int -> Solver -> ShowS
Show, Int -> Solver
Solver -> Int
Solver -> [Solver]
Solver -> Solver
Solver -> Solver -> [Solver]
Solver -> Solver -> Solver -> [Solver]
(Solver -> Solver)
-> (Solver -> Solver)
-> (Int -> Solver)
-> (Solver -> Int)
-> (Solver -> [Solver])
-> (Solver -> Solver -> [Solver])
-> (Solver -> Solver -> [Solver])
-> (Solver -> Solver -> Solver -> [Solver])
-> Enum Solver
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Solver -> Solver -> Solver -> [Solver]
$cenumFromThenTo :: Solver -> Solver -> Solver -> [Solver]
enumFromTo :: Solver -> Solver -> [Solver]
$cenumFromTo :: Solver -> Solver -> [Solver]
enumFromThen :: Solver -> Solver -> [Solver]
$cenumFromThen :: Solver -> Solver -> [Solver]
enumFrom :: Solver -> [Solver]
$cenumFrom :: Solver -> [Solver]
fromEnum :: Solver -> Int
$cfromEnum :: Solver -> Int
toEnum :: Int -> Solver
$ctoEnum :: Int -> Solver
pred :: Solver -> Solver
$cpred :: Solver -> Solver
succ :: Solver -> Solver
$csucc :: Solver -> Solver
Enum, Solver
Solver -> Solver -> Bounded Solver
forall a. a -> a -> Bounded a
maxBound :: Solver
$cmaxBound :: Solver
minBound :: Solver
$cminBound :: Solver
Bounded)

-- | An SMT solver
data SMTSolver = SMTSolver {
         SMTSolver -> Solver
name           :: Solver                -- ^ The solver in use
       , SMTSolver -> String
executable     :: String                -- ^ The path to its executable
       , SMTSolver -> ShowS
preprocess     :: String -> String      -- ^ Each line sent to the solver will be passed through this function (typically id)
       , SMTSolver -> SMTConfig -> [String]
options        :: SMTConfig -> [String] -- ^ Options to provide to the solver
       , SMTSolver
-> forall res.
   SMTConfig -> State -> String -> (State -> IO res) -> IO res
engine         :: SMTEngine             -- ^ The solver engine, responsible for interpreting solver output
       , SMTSolver -> SolverCapabilities
capabilities   :: SolverCapabilities    -- ^ Various capabilities of the solver
       }

-- | Query execution context
data QueryContext = QueryInternal       -- ^ Triggered from inside SBV
                  | QueryExternal       -- ^ Triggered from user code

-- | Show instance for 'QueryContext', for debugging purposes
instance Show QueryContext where
   show :: QueryContext -> String
show QueryInternal = "Internal Query"
   show QueryExternal = "User Query"

{-# ANN type FPOp ("HLint: ignore Use camelCase" :: String) #-}
{-# ANN type PBOp ("HLint: ignore Use camelCase" :: String) #-}
{-# ANN type OvOp ("HLint: ignore Use camelCase" :: String) #-}