hasmtlib-2.7.1: src/Language/Hasmtlib/Type/Expr.hs
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE DerivingStrategies #-}
{- |
This module provides the data-type 'Expr'.
It represents SMTLib-expressions via an abstract syntax tree (AST), implemented as GADT.
Variables are just 'Int's wrapped in a newtype 'SMTVar' with a phantom-type 'SMTSort'.
Usually the end user of this library does not need to deal with this representation.
Instead he should rely on the provided instances for building expressions.
Some of the main classes of these include:
1. 'Equatable' and 'Orderable' for symbolic comparisons,
2. 'Iteable' for symbolic branching via 'ite',
3. 'Boolean' for symbolic bool operations,
4. Prelude classics like: 'Num', 'Floating', 'Integral', 'Bounded', ... for arithmetics
5. 'Bits.Bits' for BitVec-operations
Besides that, there are also some operations defined by the SMTLib-Standard Version 2.6 that do not fit into any classes
and therefore are exported as plain functions, like 'for_all' or 'bvConcat'.
-}
module Language.Hasmtlib.Type.Expr
(
-- * SMTVar
SMTVar(..), varId
-- * Expr type
, Expr(..), isLeaf, exprSize
-- * Compare
-- ** Equatable
-- *** Class
, Equatable(..)
, equal, distinct
-- *** Generic
, GEquatable(..)
-- ** Orderable
-- *** Class
, Orderable(..)
, min', max'
-- *** Generic
, GOrderable(..)
-- ** Iteable
, Iteable(..)
-- * Non-class functions
-- ** Quantifier
, for_all, exists
-- ** BitVec
, bvConcat
-- ** Array
, select, store
-- ** String
, strLength, strAt, strSubstring, strPrefixOf, strSuffixOf, strContains, strIndexOf, strReplace, strReplaceAll
-- ** Conversion
, toRealSort, toIntSort, isIntSort
)
where
import Prelude hiding (not, and, or, any, all, (&&), (||))
import Language.Hasmtlib.Internal.Uniplate1
import Language.Hasmtlib.Type.Bitvec (BvEnc(..), KnownBvEnc(..), SBvEnc(..))
import Language.Hasmtlib.Type.SMTSort
import Language.Hasmtlib.Type.Value
import Language.Hasmtlib.Boolean
import Data.GADT.Compare
import Data.GADT.DeepSeq
import Data.Coerce
import Data.Proxy
import Data.Int
import Data.Word
import Data.Void
import qualified Data.Bits as Bits
import Data.Sequence (Seq)
import Data.Tree (Tree)
import Data.STRef
import Data.Monoid (Sum, Product, First, Last, Dual)
import Data.String (IsString(..))
import Data.Text (pack)
import Data.List(genericLength)
import Data.Foldable (toList)
import qualified Data.Vector.Sized as V
import Control.Lens hiding (from, to)
import Control.Monad.ST
import Control.Monad
import GHC.TypeLits hiding (someNatVal)
import GHC.TypeNats (someNatVal)
import GHC.Generics
-- | An internal SMT variable with a phantom-type which holds an 'Int' as it's identifier.
type role SMTVar phantom
newtype SMTVar (t :: SMTSort) = SMTVar { _varId :: Int }
deriving stock (Show, Generic)
deriving newtype (Eq, Ord)
$(makeLenses ''SMTVar)
-- | An SMT-Expression.
-- For building expressions use the corresponding instances.
--
-- With a lot of criminal energy you may build invalid expressions regarding the SMTLib Version 2.6 - specification.
-- Therefore it is highly recommended to rely on the instances.
data Expr (t :: SMTSort) where
Var :: KnownSMTSort t => SMTVar t -> Expr t
Constant :: Value t -> Expr t
Plus :: Num (HaskellType t) => Expr t -> Expr t -> Expr t
Minus :: Num (HaskellType t) => Expr t -> Expr t -> Expr t
Neg :: Num (HaskellType t) => Expr t -> Expr t
Mul :: Num (HaskellType t) => Expr t -> Expr t -> Expr t
Abs :: Num (HaskellType t) => Expr t -> Expr t
Mod :: Integral (HaskellType t) => Expr t -> Expr t -> Expr t
Rem :: Integral (HaskellType t) => Expr t -> Expr t -> Expr t
IDiv :: Integral (HaskellType t) => Expr t -> Expr t -> Expr t
Div :: Expr RealSort -> Expr RealSort -> Expr RealSort
LTH :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
LTHE :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
EQU :: (Eq (HaskellType t), KnownSMTSort t, KnownNat n) => V.Vector (n + 2) (Expr t) -> Expr BoolSort
Distinct :: (Eq (HaskellType t), KnownSMTSort t, KnownNat n) => V.Vector (n + 2) (Expr t) -> Expr BoolSort
GTHE :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
GTH :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort
Not :: Boolean (HaskellType t) => Expr t -> Expr t
And :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
Or :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
Impl :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
Xor :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t
Pi :: Expr RealSort
Sqrt :: Expr RealSort -> Expr RealSort
Exp :: Expr RealSort -> Expr RealSort
Sin :: Expr RealSort -> Expr RealSort
Cos :: Expr RealSort -> Expr RealSort
Tan :: Expr RealSort -> Expr RealSort
Asin :: Expr RealSort -> Expr RealSort
Acos :: Expr RealSort -> Expr RealSort
Atan :: Expr RealSort -> Expr RealSort
ToReal :: Expr IntSort -> Expr RealSort
ToInt :: Expr RealSort -> Expr IntSort
IsInt :: Expr RealSort -> Expr BoolSort
Ite :: Expr BoolSort -> Expr t -> Expr t -> Expr t
BvNand :: (KnownBvEnc enc, KnownNat n) => Expr (BvSort enc n) -> Expr (BvSort enc n) -> Expr (BvSort enc n)
BvNor :: (KnownBvEnc enc, KnownNat n) => Expr (BvSort enc n) -> Expr (BvSort enc n) -> Expr (BvSort enc n)
BvShL :: (KnownBvEnc enc, KnownNat n) => Expr (BvSort enc n) -> Expr (BvSort enc n) -> Expr (BvSort enc n)
BvLShR :: KnownNat n => Expr (BvSort Unsigned n) -> Expr (BvSort Unsigned n) -> Expr (BvSort Unsigned n)
BvAShR :: KnownNat n => Expr (BvSort Signed n) -> Expr (BvSort Signed n) -> Expr (BvSort Signed n)
BvConcat :: (KnownBvEnc enc , KnownNat n, KnownNat m) => Expr (BvSort enc n) -> Expr (BvSort enc m) -> Expr (BvSort enc (n + m))
BvRotL :: (KnownBvEnc enc, KnownNat n, Integral a) => a -> Expr (BvSort enc n) -> Expr (BvSort enc n)
BvRotR :: (KnownBvEnc enc, KnownNat n, Integral a) => a -> Expr (BvSort enc n) -> Expr (BvSort enc n)
ArrSelect :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => Expr (ArraySort k v) -> Expr k -> Expr v
ArrStore :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v -> Expr (ArraySort k v)
StrConcat :: Expr StringSort -> Expr StringSort -> Expr StringSort
StrLength :: Expr StringSort -> Expr IntSort
StrAt :: Expr StringSort -> Expr IntSort -> Expr StringSort
StrSubstring :: Expr StringSort -> Expr IntSort -> Expr IntSort -> Expr StringSort
StrPrefixOf :: Expr StringSort -> Expr StringSort -> Expr BoolSort
StrSuffixOf :: Expr StringSort -> Expr StringSort -> Expr BoolSort
StrContains :: Expr StringSort -> Expr StringSort -> Expr BoolSort
StrIndexOf :: Expr StringSort -> Expr StringSort -> Expr IntSort -> Expr IntSort
StrReplace :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort
StrReplaceAll :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort
-- | Just v if quantified var has been created already, Nothing otherwise
ForAll :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort
-- | Just v if quantified var has been created already, Nothing otherwise
Exists :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort
-- | Indicates whether an expression is a leaf.
-- All non-recursive contructors are leafs.
isLeaf :: Expr t -> Bool
isLeaf (Var _) = True
isLeaf (Constant _) = True
isLeaf Pi = True
isLeaf _ = False
{-# INLINE isLeaf #-}
-- | Size of the expression.
--
-- Counts the amount of operations.
--
-- ==== __Examples__
--
-- >>> nodeSize $ x + y === x + y
-- 3
-- >>> nodeSize $ false
-- 0
exprSize :: KnownSMTSort t => Expr t -> Integer
exprSize expr = runST $ do
nodesRef <- newSTRef 0
_ <- transformM1
(\expr' -> do
unless (isLeaf expr') $ modifySTRef' nodesRef (+1)
return expr')
expr
readSTRef nodesRef
-- | Class that allows branching on predicates of type @b@ on branches of type @a@.
--
-- If predicate (p :: b) then (t :: a) else (f :: a).
--
-- There is a default implementation if your type is an 'Applicative'.
--
-- ==== __Examples__
--
-- >>> ite True "1" "2"
-- "1"
-- >>> ite False 100 42
-- 42
class Iteable b a where
ite :: b -> a -> a -> a
default ite :: (Iteable b c, Applicative f, f c ~ a) => b -> a -> a -> a
ite p t f = ite p <$> t <*> f
instance Iteable (Expr BoolSort) (Expr t) where
ite (Constant (BoolValue False)) _ f = f
ite (Constant (BoolValue True)) t _ = t
ite p t@(Ite p' t' f') f@(Ite p'' t'' f'')
| p' == p'' && t' == t'' = Ite p' t' (Ite p f' f'')
| p' == p'' && f' == f'' = Ite (not p') f' (Ite p t' t'')
| otherwise = Ite p t f
ite p t f@(Ite p' t' f')
| p == p' = Ite p t f'
| t == t' = Ite (p || p') t f'
| otherwise = Ite p t f
ite p t@(Ite p' t' f') f
| p == p' = Ite p t' f
| f == f' = Ite (p && p') t' f
| otherwise = Ite p t f
ite p t f
| t == f = t
| otherwise = Ite p t f
{-# INLINEABLE ite #-}
instance Iteable Bool a where
ite p t f = if p then t else f
{-# INLINE ite #-}
instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) [a]
instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Maybe a)
instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Seq a)
instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Tree a)
instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Sum a)
instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Product a)
instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (First a)
instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Last a)
instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Dual a)
instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Identity a)
instance Iteable (Expr BoolSort) () where
ite _ _ _ = ()
instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b) => Iteable (Expr BoolSort) (a,b) where
ite p (a,b) (a',b') = (ite p a a', ite p b b')
instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c) => Iteable (Expr BoolSort) (a,b,c) where
ite p (a,b,c) (a',b',c') = (ite p a a', ite p b b', ite p c c')
instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d) => Iteable (Expr BoolSort) (a,b,c,d) where
ite p (a,b,c,d) (a',b',c',d') = (ite p a a', ite p b b', ite p c c', ite p d d')
instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e) => Iteable (Expr BoolSort) (a,b,c,d,e) where
ite p (a,b,c,d,e) (a',b',c',d',e') = (ite p a a', ite p b b', ite p c c', ite p d d', ite p e e')
instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e, Iteable (Expr BoolSort) f) => Iteable (Expr BoolSort) (a,b,c,d,e,f) where
ite p (a,b,c,d,e,f) (a',b',c',d',e',f') = (ite p a a', ite p b b', ite p c c', ite p d d', ite p e e', ite p f f')
instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e, Iteable (Expr BoolSort) f, Iteable (Expr BoolSort) g) => Iteable (Expr BoolSort) (a,b,c,d,e,f,g) where
ite p (a,b,c,d,e,f,g) (a',b',c',d',e',f',g') = (ite p a a', ite p b b', ite p c c', ite p d d', ite p e e', ite p f f', ite p g g')
instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e, Iteable (Expr BoolSort) f, Iteable (Expr BoolSort) g, Iteable (Expr BoolSort) h) => Iteable (Expr BoolSort) (a,b,c,d,e,f,g,h) where
ite p (a,b,c,d,e,f,g,h) (a',b',c',d',e',f',g',h') = (ite p a a', ite p b b', ite p c c', ite p d d', ite p e e', ite p f f', ite p g g', ite p h h')
-- | Symbolically test two values on equality.
--
-- A generic default implementation with 'GEquatable' is possible.
--
-- ==== __Example__
--
-- @
-- x <- var @RealType
-- y <- var
-- assert $ y === x && not (y /== x) && x === 42
-- @
class Equatable a where
-- | Test whether two values are equal in the SMT-Problem.
(===) :: a -> a -> Expr BoolSort
default (===) :: (Generic a, GEquatable (Rep a)) => a -> a -> Expr BoolSort
a === b = from a ===# from b
-- | Test whether two values are not equal in the SMT-Problem.
(/==) :: a -> a -> Expr BoolSort
x /== y = not $ x === y
infix 4 ===, /==
instance (KnownSMTSort t, Eq (HaskellType t)) => Equatable (Expr t) where
x === y = EQU $ V.fromTuple (x,y)
{-# INLINE (===) #-}
x /== y = Distinct $ V.fromTuple (x,y)
{-# INLINE (/==) #-}
class GEquatable f where
(===#) :: f a -> f a -> Expr BoolSort
instance GEquatable U1 where
U1 ===# U1 = true
instance GEquatable V1 where
x ===# y = x `seq` y `seq` error "GEquatable[V1].===#"
instance (GEquatable f, GEquatable g) => GEquatable (f :*: g) where
(a :*: b) ===# (c :*: d) = (a ===# c) && (b ===# d)
instance (GEquatable f, GEquatable g) => GEquatable (f :+: g) where
L1 a ===# L1 b = a ===# b
R1 a ===# R1 b = a ===# b
_ ===# _ = false
instance GEquatable f => GEquatable (M1 i c f) where
M1 x ===# M1 y = x ===# y
instance Equatable a => GEquatable (K1 i a) where
K1 a ===# K1 b = a === b
instance Equatable () where _ === _ = true
instance Equatable Void where x === y = x `seq` y `seq` error "Equatable[Void].==="
instance Equatable Int where x === y = bool (x == y)
instance Equatable Integer where x === y = bool (x == y)
instance Equatable Natural where x === y = bool (x == y)
instance Equatable Word where x === y = bool (x == y)
instance Equatable Word8 where x === y = bool (x == y)
instance Equatable Word16 where x === y = bool (x == y)
instance Equatable Word32 where x === y = bool (x == y)
instance Equatable Word64 where x === y = bool (x == y)
instance Equatable Int8 where x === y = bool (x == y)
instance Equatable Int16 where x === y = bool (x == y)
instance Equatable Int32 where x === y = bool (x == y)
instance Equatable Int64 where x === y = bool (x == y)
instance Equatable Char where x === y = bool (x == y)
instance Equatable Float where x === y = bool (x == y)
instance Equatable Double where x === y = bool (x == y)
instance Equatable Ordering where x === y = bool (x == y)
instance Equatable Bool where x === y = bool (x == y)
instance (Equatable a, Equatable b) => Equatable (a,b)
instance (Equatable a, Equatable b, Equatable c) => Equatable (a,b,c)
instance (Equatable a, Equatable b, Equatable c, Equatable d) => Equatable (a,b,c,d)
instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e) => Equatable (a,b,c,d,e)
instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e, Equatable f) => Equatable (a,b,c,d,e,f)
instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e, Equatable f, Equatable g) => Equatable (a,b,c,d,e,f,g)
instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e, Equatable f, Equatable g, Equatable h) => Equatable (a,b,c,d,e,f,g,h)
instance Equatable a => Equatable [a]
instance Equatable a => Equatable (Tree a)
instance Equatable a => Equatable (Maybe a)
instance (Equatable a, Equatable b) => Equatable (Either a b)
instance Equatable a => Equatable (Sum a)
instance Equatable a => Equatable (Product a)
instance Equatable a => Equatable (First a)
instance Equatable a => Equatable (Last a)
instance Equatable a => Equatable (Dual a)
instance Equatable a => Equatable (Identity a)
-- | Symbolically compare two values.
--
-- A generic default implementation with 'GOrderable' is possible.
--
-- ==== __Example__
--
-- @
-- x <- var @RealSort
-- y <- var
-- assert $ x >? y
-- assert $ x === min' 42 100
-- @
--
class Equatable a => Orderable a where
(<=?) :: a -> a -> Expr BoolSort
default (<=?) :: (Generic a, GOrderable (Rep a)) => a -> a -> Expr BoolSort
x <=? y = from x <=?# from y
(>=?) :: a -> a -> Expr BoolSort
x >=? y = y <=? x
(<?) :: a -> a -> Expr BoolSort
x <? y = not $ y <=? x
(>?) :: a -> a -> Expr BoolSort
x >? y = not $ x <=? y
infix 4 <?, <=?, >=?, >?
-- | Symbolic evaluation of the minimum of two symbolic values.
min' :: (Orderable a, Iteable (Expr BoolSort) a) => a -> a -> a
min' x y = ite (x <=? y) x y
-- | Symbolic evaluation of the maximum of two symbolic values.
max' :: (Orderable a, Iteable (Expr BoolSort) a) => a -> a -> a
max' x y = ite (y <=? x) x y
instance (KnownSMTSort t, Ord (HaskellType t)) => Orderable (Expr t) where
(<?) = LTH
{-# INLINE (<?) #-}
(<=?) = LTHE
{-# INLINE (<=?) #-}
(>=?) = GTHE
{-# INLINE (>=?) #-}
(>?) = GTH
{-# INLINE (>?) #-}
class GEquatable f => GOrderable f where
(<?#) :: f a -> f a -> Expr BoolSort
(<=?#) :: f a -> f a -> Expr BoolSort
instance GOrderable U1 where
U1 <?# U1 = false
U1 <=?# U1 = true
instance GOrderable V1 where
x <?# y = x `seq` y `seq` error "GOrderable[V1].<?#"
x <=?# y = x `seq` y `seq` error "GOrderable[V1].<=?#"
instance (GOrderable f, GOrderable g) => GOrderable (f :*: g) where
(a :*: b) <?# (c :*: d) = (a <?# c) || (a ===# c && b <?# d)
(a :*: b) <=?# (c :*: d) = (a <?# c) || (a ===# c && b <=?# d)
instance (GOrderable f, GOrderable g) => GOrderable (f :+: g) where
L1 _ <?# R1 _ = true
L1 a <?# L1 b = a <?# b
R1 a <?# R1 b = a <?# b
R1 _ <?# L1 _ = false
L1 _ <=?# R1 _ = true
L1 a <=?# L1 b = a <=?# b
R1 a <=?# R1 b = a <=?# b
R1 _ <=?# L1 _ = false
instance GOrderable f => GOrderable (M1 i c f) where
M1 x <?# M1 y = x <?# y
M1 x <=?# M1 y = x <=?# y
instance Orderable a => GOrderable (K1 i a) where
K1 a <?# K1 b = a <? b
K1 a <=?# K1 b = a <=? b
-- Boring instances that end up being useful when deriving Orderable with Generics
instance Orderable () where _ <? _ = false
_ <=? _ = true
instance Orderable Void where x <? y = x `seq` y `seq` error "Orderable[Void].<?"
x <=? y = x `seq` y `seq` error "Orderable[Void].<=?"
instance Orderable Int where x <? y = bool (x < y)
x <=? y = bool (x <= y)
instance Orderable Integer where x <? y = bool (x < y)
x <=? y = bool (x <= y)
instance Orderable Natural where x <? y = bool (x < y)
x <=? y = bool (x <= y)
instance Orderable Word where x <? y = bool (x < y)
x <=? y = bool (x <= y)
instance Orderable Word8 where x <? y = bool (x < y)
x <=? y = bool (x <= y)
instance Orderable Word16 where x <? y = bool (x < y)
x <=? y = bool (x <= y)
instance Orderable Word32 where x <? y = bool (x < y)
x <=? y = bool (x <= y)
instance Orderable Word64 where x <? y = bool (x < y)
x <=? y = bool (x <= y)
instance Orderable Int8 where x <? y = bool (x < y)
x <=? y = bool (x <= y)
instance Orderable Int16 where x <? y = bool (x < y)
x <=? y = bool (x <= y)
instance Orderable Int32 where x <? y = bool (x < y)
x <=? y = bool (x <= y)
instance Orderable Int64 where x <? y = bool (x < y)
x <=? y = bool (x <= y)
instance Orderable Char where x <? y = bool (x < y)
x <=? y = bool (x <= y)
instance Orderable Float where x <? y = bool (x < y)
x <=? y = bool (x <= y)
instance Orderable Double where x <? y = bool (x < y)
x <=? y = bool (x <= y)
instance Orderable Ordering where x <? y = bool (x < y)
x <=? y = bool (x <= y)
instance Orderable Bool where x <? y = bool (x < y)
x <=? y = bool (x <= y)
instance (Orderable a, Orderable b) => Orderable (a,b)
instance (Orderable a, Orderable b, Orderable c) => Orderable (a,b,c)
instance (Orderable a, Orderable b, Orderable c, Orderable d) => Orderable (a,b,c,d)
instance (Orderable a, Orderable b, Orderable c, Orderable d, Orderable e) => Orderable (a,b,c,d,e)
instance (Orderable a, Orderable b, Orderable c, Orderable d, Orderable e, Orderable f) => Orderable (a,b,c,d,e,f)
instance (Orderable a, Orderable b, Orderable c, Orderable d, Orderable e, Orderable f, Orderable g) => Orderable (a,b,c,d,e,f,g)
instance (Orderable a, Orderable b, Orderable c, Orderable d, Orderable e, Orderable f, Orderable g, Orderable h) => Orderable (a,b,c,d,e,f,g,h)
instance Orderable a => Orderable [a]
instance Orderable a => Orderable (Tree a)
instance Orderable a => Orderable (Maybe a)
instance (Orderable a, Orderable b) => Orderable (Either a b)
instance Orderable a => Orderable (Sum a)
instance Orderable a => Orderable (Product a)
instance Orderable a => Orderable (First a)
instance Orderable a => Orderable (Last a)
instance Orderable a => Orderable (Dual a)
instance Orderable a => Orderable (Identity a)
-- | Symbolically test multiple expressions on equality.
--
-- Returns 'true' if given less than two arguments.
equal :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort
equal (toList -> (a:b:xs)) = case someNatVal (genericLength xs) of
SomeNat n -> case V.fromListN' n xs of
Nothing -> EQU $ V.fromTuple (a,b)
Just xs' -> EQU $ xs' V.++ V.fromTuple (a,b)
equal (toList -> _) = true
-- | Symbolically test multiple expressions on distinctness.
--
-- Returns 'true' if given less than two arguments.
distinct :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort
distinct (toList -> (a:b:xs)) = case someNatVal (genericLength xs) of
SomeNat n -> case V.fromListN' n xs of
Nothing -> Distinct $ V.fromTuple (a,b)
Just xs' -> Distinct $ xs' V.++ V.fromTuple (a,b)
distinct (toList -> _) = true
-- | Universal quantification for any specific 'SMTSort'.
--
-- ==== __Example__
--
-- @
-- assert $
-- for_all @IntSort $ \x ->
-- x + 0 === x && 0 + x === x
-- @
--
-- The lambdas 'x' is all-quantified here.
-- It will only be scoped for the lambdas body.
for_all :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort
for_all = ForAll Nothing
{-# INLINE for_all #-}
-- | Existential quantification for any specific 'SMTSort'
--
-- ==== __Example__
--
-- @
-- assert $
-- for_all @(BvSort Unsigned 8) $ \x ->
-- exists $ \y ->
-- x - y === 0
-- @
--
-- The lambdas 'y' is existentially quantified here.
-- It will only be scoped for the lambdas body.
exists :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort
exists = Exists Nothing
{-# INLINE exists #-}
-- | Select a value from an array.
select :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => Expr (ArraySort k v) -> Expr k -> Expr v
select = ArrSelect
{-# INLINE select #-}
-- | Store a value in an array.
store :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v -> Expr (ArraySort k v)
store = ArrStore
{-# INLINE store #-}
-- | Concats two bitvectors.
bvConcat :: (KnownBvEnc enc, KnownNat n, KnownNat m) => Expr (BvSort enc n) -> Expr (BvSort enc m) -> Expr (BvSort enc (n + m))
bvConcat = BvConcat
{-# INLINE bvConcat #-}
-- | Converts an expression of type 'IntSort' to type 'RealSort'.
toRealSort :: Expr IntSort -> Expr RealSort
toRealSort = ToReal
{-# INLINE toRealSort #-}
-- | Converts an expression of type 'RealSort' to type 'IntSort'.
toIntSort :: Expr RealSort -> Expr IntSort
toIntSort = ToInt
{-# INLINE toIntSort #-}
-- | Checks whether an expression of type 'RealSort' may be safely converted to type 'IntSort'.
isIntSort :: Expr RealSort -> Expr BoolSort
isIntSort = IsInt
{-# INLINE isIntSort #-}
-- | Length of a string.
strLength :: Expr StringSort -> Expr IntSort
strLength = StrLength
{-# INLINE strLength #-}
-- | Singleton string containing a character at given position
-- or empty string when position is out of range.
-- The leftmost position is 0.
strAt :: Expr StringSort -> Expr IntSort -> Expr StringSort
strAt = StrAt
{-# INLINE strAt #-}
-- | @(strSubstring s i n)@ evaluates to the longest (unscattered) substring
-- of @s@ of length at most @n@ starting at position @i@.
-- It evaluates to the empty string if @n@ is negative or @i@ is not in
-- the interval @[0,l-1]@ where @l@ is the length of @s@.
strSubstring :: Expr StringSort -> Expr IntSort -> Expr IntSort -> Expr StringSort
strSubstring = StrSubstring
{-# INLINE strSubstring #-}
-- | First string is a prefix of second one.
-- @(strPrefixof s t)@ is @true@ iff @s@ is a prefix of @t@.
strPrefixOf :: Expr StringSort -> Expr StringSort -> Expr BoolSort
strPrefixOf = StrPrefixOf
{-# INLINE strPrefixOf #-}
-- | First string is a suffix of second one.
-- @(strSuffixof s t)@ is @true@ iff @s@ is a suffix of @t@.
strSuffixOf :: Expr StringSort -> Expr StringSort -> Expr BoolSort
strSuffixOf = StrSuffixOf
{-# INLINE strSuffixOf #-}
-- | First string contains second one
-- @(strContains s t)@ iff @s@ contains @t@.
strContains :: Expr StringSort -> Expr StringSort -> Expr BoolSort
strContains = StrContains
{-# INLINE strContains #-}
-- | Index of first occurrence of second string in first one starting at the position specified by the third argument.
-- @(strIndexof s t i)@, with @0 <= i <= |s|@ is the position of the first
-- occurrence of @t@ in @s@ at or after position @i@, if any.
-- Otherwise, it is @-1@. Note that the result is @i@ whenever @i@ is within
-- the range @[0, |s|]@ and @t@ is empty.
strIndexOf :: Expr StringSort -> Expr StringSort -> Expr IntSort -> Expr IntSort
strIndexOf = StrIndexOf
{-# INLINE strIndexOf #-}
-- | @(strReplace s t t')@ is the string obtained by replacing the first
-- occurrence of @t@ in @s@, if any, by @t'@. Note that if @t@ is empty, the
-- result is to prepend @t'@ to @s@; also, if @t@ does not occur in @s@ then
-- the result is @s@.
strReplace :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort
strReplace = StrReplace
{-# INLINE strReplace #-}
-- | @(strReplaceAll s t t’)@ is @s@ if @t@ is the empty string. Otherwise, it
-- is the string obtained from @s@ by replacing all occurrences of @t@ in @s@
-- by @t’@, starting with the first occurrence and proceeding in left-to-right order.
strReplaceAll :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort
strReplaceAll = StrReplaceAll
{-# INLINE strReplaceAll #-}
instance (KnownSMTSort t, Num (HaskellType t), Ord (HaskellType t)) => Num (Expr t) where
fromInteger = Constant . wrapValue . fromInteger
{-# INLINE fromInteger #-}
(Constant 0) + y = y
x + (Constant 0) = x
(Constant x) + (Constant y) = Constant (x + y)
x + y = Plus x y
{-# INLINE (+) #-}
x - (Constant 0) = x
(Constant x) - (Constant y) = Constant (x - y)
(Constant 0) - x = negate x
x - y = Minus x y
{-# INLINE (-) #-}
(Constant 0) * _ = 0
_ * (Constant 0) = 0
(Constant 1) * y = y
x * (Constant 1) = x
(Constant (-1)) * x = negate x
x * (Constant (-1)) = negate x
(Constant x) * (Constant y) = Constant (x * y)
x * y = Mul x y
{-# INLINE (*) #-}
negate (Constant x) = Constant $ negate x
negate (Neg x) = x
negate x = Neg x
{-# INLINE negate #-}
abs (Constant x) = Constant $ abs x
abs x = Abs x
{-# INLINE abs #-}
signum (Constant x) = Constant $ signum x
signum x = ite (x === 0) 0 $ ite (x <? 0) (-1) 1
{-# INLINE signum #-}
instance Fractional (Expr RealSort) where
fromRational = Constant . RealValue . fromRational
{-# INLINE fromRational #-}
x / (Constant 1) = x
(Constant 0) / _ = 0
(Constant x) / (Constant y) = Constant (x / y)
x / y = Div x y
{-# INLINE (/) #-}
-- | Not part of the SMTLib standard Version 2.6.
-- Some solvers support it. At least valid for CVC5 and MathSAT.
instance Floating (Expr RealSort) where
pi = Pi
{-# INLINE pi #-}
exp = Exp
{-# INLINE exp #-}
log = error "SMT-Solvers currently do not support log"
sqrt = Sqrt
{-# INLINE sqrt #-}
sin = Sin
{-# INLINE sin #-}
cos = Cos
{-# INLINE cos #-}
tan = Tan
{-# INLINE tan #-}
asin = Asin
{-# INLINE asin #-}
acos = Acos
{-# INLINE acos #-}
atan = Atan
{-# INLINE atan #-}
sinh = error "SMT-Solvers currently do not support sinh"
cosh = error "SMT-Solvers currently do not support cosh"
tanh = error "SMT-Solvers currently do not support tanh"
asinh = error "SMT-Solvers currently do not support asinh"
acosh = error "SMT-Solvers currently do not support acosh"
atanh = error "SMT-Solvers currently do not support atanh"
-- | This instance is __partial__ for 'toRational', this method is only intended for use with constants.
instance (KnownSMTSort t, Real (HaskellType t)) => Real (Expr t) where
toRational (Constant x) = toRational $ unwrapValue x
toRational _ = error $ "Real#toRational[Expr " <> show (sortSing @t) <> "] only supported for constants."
{-# INLINE toRational #-}
-- | This instance is __partial__ for 'fromEnum', this method is only intended for use with constants.
instance (KnownSMTSort t, Enum (HaskellType t)) => Enum (Expr t) where
fromEnum (Constant x) = fromEnum $ unwrapValue x
fromEnum _ = error $ "Enum#fromEnum[Expr " <> show (sortSing @t) <> "] only supported for constants."
{-# INLINE fromEnum #-}
toEnum = Constant . wrapValue . toEnum
{-# INLINE toEnum #-}
-- | This instance is __partial__ for 'toInteger', this method is only intended for use with constants.
instance (KnownSMTSort t, Integral (HaskellType t)) => Integral (Expr t) where
quotRem x y = (IDiv x y, Rem x y)
{-# INLINE quotRem #-}
divMod x y = (IDiv x y, Mod x y)
{-# INLINE divMod #-}
toInteger (Constant x) = toInteger $ unwrapValue x
toInteger _ = error $ "Integer#toInteger[Expr " <> show (sortSing @t) <> "] only supported for constants."
{-# INLINE toInteger #-}
instance Boolean (Expr BoolSort) where
bool = Constant . BoolValue
{-# INLINE bool #-}
(Constant (BoolValue x)) && y = if x then y else false
x && (Constant (BoolValue y)) = if y then x else false
x && y = And x y
{-# INLINE (&&) #-}
(Constant (BoolValue x)) || y = if x then true else y
x || (Constant (BoolValue y)) = if y then true else x
x || y = Or x y
{-# INLINE (||) #-}
not (Constant x) = Constant $ not x
not (Not x) = x
not x = Not x
{-# INLINE not #-}
xor (Constant (BoolValue x)) y = if x then not y else y
xor x (Constant (BoolValue y)) = if y then not x else x
xor x y = Xor x y
{-# INLINE xor #-}
(Constant (BoolValue False)) ==> _ = true
x ==> y = Impl x y
{-# INLINE (==>) #-}
(<==>) = (===)
{-# INLINE (<==>) #-}
instance (KnownBvEnc enc, KnownNat n) => Boolean (Expr (BvSort enc n)) where
bool = Constant . BvValue . bool
{-# INLINE bool #-}
(&&) = And
{-# INLINE (&&) #-}
(||) = Or
{-# INLINE (||) #-}
not (Not x) = x
not x = Not x
{-# INLINE not #-}
xor = Xor
{-# INLINE xor #-}
instance Bounded (Expr BoolSort) where
minBound = false
{-# INLINE minBound #-}
maxBound = true
{-# INLINE maxBound #-}
instance (KnownBvEnc enc, KnownNat n) => Bounded (Expr (BvSort enc n)) where
minBound = Constant $ BvValue minBound
{-# INLINE minBound #-}
maxBound = Constant $ BvValue maxBound
{-# INLINE maxBound #-}
-- | This instance is __partial__ for 'testBit' and 'popCount', it's only intended for use with constants ('Constant').
instance Bits.Bits (Expr BoolSort) where
(.&.) = And
{-# INLINE (.&.) #-}
(.|.) = Or
{-# INLINE (.|.) #-}
xor = Xor
{-# INLINE xor #-}
complement = Not
{-# INLINE complement #-}
zeroBits = false
{-# INLINE zeroBits #-}
bit _ = true
{-# INLINE bit #-}
setBit _ _ = true
{-# INLINE setBit #-}
clearBit _ _ = false
{-# INLINE clearBit #-}
complementBit b _ = Not b
{-# INLINE complementBit #-}
testBit (Constant (BoolValue b)) _ = b
testBit _ _ = error "Bits#testBit[Expr BoolSort] is only supported for constants."
{-# INLINE testBit #-}
bitSizeMaybe _ = Just 1
{-# INLINE bitSizeMaybe #-}
bitSize _ = 1
{-# INLINE bitSize #-}
isSigned _ = False
{-# INLINE isSigned #-}
shiftL b 0 = b
shiftL _ _ = false
{-# INLINE shiftL #-}
shiftR b 0 = b
shiftR _ _ = false
{-# INLINE shiftR #-}
rotateL b _ = b
{-# INLINE rotateL #-}
rotateR b _ = b
{-# INLINE rotateR #-}
popCount (Constant (BoolValue b)) = if b then 1 else 0
popCount _ = error "Bits#popCount[Expr BoolSort] is only supported for constants."
{-# INLINE popCount #-}
-- | This instance is __partial__ for 'testBit' and 'popCount', it's only intended for use with constants ('Constant').
instance (KnownBvEnc enc, KnownNat n) => Bits.Bits (Expr (BvSort enc n)) where
(.&.) = And
{-# INLINE (.&.) #-}
(.|.) = Or
{-# INLINE (.|.) #-}
xor = Xor
{-# INLINE xor #-}
complement = Not
{-# INLINE complement #-}
zeroBits = false
{-# INLINE zeroBits #-}
bit = Constant . BvValue . Bits.bit
{-# INLINE bit #-}
testBit (Constant (BvValue b)) i = Bits.testBit b i
testBit _ _ = error "Bits#testBit[Expr BvSort] is only supported for constants."
{-# INLINE testBit #-}
bitSizeMaybe _ = Just $ fromIntegral $ natVal $ Proxy @n
{-# INLINE bitSizeMaybe #-}
bitSize _ = fromIntegral $ natVal $ Proxy @n
{-# INLINE bitSize #-}
isSigned _ = case bvEncSing @enc of
SUnsigned -> False
SSigned -> True
{-# INLINE isSigned #-}
shiftL b i = BvShL b (fromIntegral i)
{-# INLINE shiftL #-}
shiftR b i = case bvEncSing @enc of
SUnsigned -> BvLShR b (fromIntegral i)
SSigned -> BvAShR b (fromIntegral i)
{-# INLINE shiftR #-}
rotateL b i = BvRotL i b
{-# INLINE rotateL #-}
rotateR b i = BvRotR i b
{-# INLINE rotateR #-}
popCount (Constant (BvValue b)) = Bits.popCount b
popCount _ = error $ "Bits#popCount[Expr BvSort] is only supported for constants."
{-# INLINE popCount #-}
instance Semigroup (Expr StringSort) where
(<>) = StrConcat
{-# INLINE (<>) #-}
instance Monoid (Expr StringSort) where
mempty = Constant $ StringValue mempty
{-# INLINE mempty #-}
mappend = (<>)
{-# INLINE mappend #-}
instance IsString (Expr StringSort) where
fromString = Constant . StringValue . pack
{-# INLINE fromString #-}
type instance Index (Expr StringSort) = Expr IntSort
type instance IxValue (Expr StringSort) = Expr StringSort
instance Ixed (Expr StringSort) where
ix i f s = f (strAt s i) <&> \a ->
let l = strSubstring a 0 i
r = strSubstring a i (strLength a)
in l <> strReplace r (strAt a i) s
instance AsEmpty (Expr StringSort) where
_Empty = prism'
(const mempty)
(\s -> ite @(Expr BoolSort) (s === mempty) (Just ()) Nothing)
instance Prefixed (Expr StringSort) where
prefixed p = prism'
(p <>)
(\s -> ite (p `strPrefixOf` s) (Just $ strReplace s p mempty) Nothing)
instance Suffixed (Expr StringSort) where
suffixed qs = prism'
(<> qs)
(\s -> ite (qs `strSuffixOf` s) (Just $ strSubstring s 0 (strLength s - strLength qs)) Nothing)
instance Cons (Expr StringSort) (Expr StringSort) (Expr StringSort) (Expr StringSort) where
_Cons = prism'
(uncurry (<>))
(\s -> ite @(Expr BoolSort) (strLength s >? 0) (Just (strAt s 0, strSubstring s 1 (strLength s))) Nothing)
instance Snoc (Expr StringSort) (Expr StringSort) (Expr StringSort) (Expr StringSort) where
_Snoc = prism'
(uncurry (<>))
(\s -> ite @(Expr BoolSort) (strLength s >? 0) (Just (strSubstring s 0 (strLength s - 1), strAt s (strLength s - 1))) Nothing)
type instance Index (Expr (ArraySort k v)) = Expr k
type instance IxValue (Expr (ArraySort k v)) = Expr v
instance (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => Ixed (Expr (ArraySort k v)) where
ix i f arr = f (select arr i) <&> store arr i
-- | __Caution for quantified expressions:__ 'uniplate1' will only be applied if quantification has taken place already.
instance Uniplate1 Expr '[KnownSMTSort] where
uniplate1 _ expr@(Var _) = pure expr
uniplate1 _ expr@(Constant _) = pure expr
uniplate1 f (Plus x y) = Plus <$> f x <*> f y
uniplate1 f (Minus x y) = Minus <$> f x <*> f y
uniplate1 f (Neg x) = Neg <$> f x
uniplate1 f (Mul x y) = Mul <$> f x <*> f y
uniplate1 f (Abs x) = Abs <$> f x
uniplate1 f (Mod x y) = Mod <$> f x <*> f y
uniplate1 f (Rem x y) = Rem <$> f x <*> f y
uniplate1 f (IDiv x y) = IDiv <$> f x <*> f y
uniplate1 f (Div x y) = Div <$> f x <*> f y
uniplate1 f (LTH x y) = LTH <$> f x <*> f y
uniplate1 f (LTHE x y) = LTHE <$> f x <*> f y
uniplate1 f (EQU xs) = EQU <$> traverse f xs
uniplate1 f (Distinct xs) = Distinct <$> traverse f xs
uniplate1 f (GTHE x y) = GTHE <$> f x <*> f y
uniplate1 f (GTH x y) = GTH <$> f x <*> f y
uniplate1 f (Not x) = Not <$> f x
uniplate1 f (And x y) = And <$> f x <*> f y
uniplate1 f (Or x y) = Or <$> f x <*> f y
uniplate1 f (Impl x y) = Impl <$> f x <*> f y
uniplate1 f (Xor x y) = Xor <$> f x <*> f y
uniplate1 _ Pi = pure Pi
uniplate1 f (Sqrt x) = Sqrt <$> f x
uniplate1 f (Exp x) = Exp <$> f x
uniplate1 f (Sin x) = Sin <$> f x
uniplate1 f (Cos x) = Cos <$> f x
uniplate1 f (Tan x) = Tan <$> f x
uniplate1 f (Asin x) = Asin <$> f x
uniplate1 f (Acos x) = Acos <$> f x
uniplate1 f (Atan x) = Atan <$> f x
uniplate1 f (ToReal x) = ToReal <$> f x
uniplate1 f (ToInt x) = ToInt <$> f x
uniplate1 f (IsInt x) = IsInt <$> f x
uniplate1 f (Ite p t n) = Ite <$> f p <*> f t <*> f n
uniplate1 f (BvNand x y) = BvNand <$> f x <*> f y
uniplate1 f (BvNor x y) = BvNor <$> f x <*> f y
uniplate1 f (BvShL x y) = BvShL <$> f x <*> f y
uniplate1 f (BvLShR x y) = BvLShR <$> f x <*> f y
uniplate1 f (BvAShR x y) = BvAShR <$> f x <*> f y
uniplate1 f (BvConcat x y) = BvConcat <$> f x <*> f y
uniplate1 f (BvRotL i x) = BvRotL i <$> f x
uniplate1 f (BvRotR i x) = BvRotR i <$> f x
uniplate1 f (ArrSelect i arr) = ArrSelect i <$> f arr
uniplate1 f (ArrStore i x arr) = ArrStore i <$> f x <*> f arr
uniplate1 f (StrConcat x y) = StrConcat <$> f x <*> f y
uniplate1 f (StrLength x) = StrLength <$> f x
uniplate1 f (StrAt x i) = StrAt <$> f x <*> f i
uniplate1 f (StrSubstring x i j) = StrSubstring <$> f x <*> f i <*> f j
uniplate1 f (StrPrefixOf x y) = StrPrefixOf <$> f x <*> f y
uniplate1 f (StrSuffixOf x y) = StrSuffixOf <$> f x <*> f y
uniplate1 f (StrContains x y) = StrContains <$> f x <*> f y
uniplate1 f (StrIndexOf x y i) = StrIndexOf <$> f x <*> f y <*> f i
uniplate1 f (StrReplace x y y') = StrReplace <$> f x <*> f y <*> f y'
uniplate1 f (StrReplaceAll x y y') = StrReplaceAll <$> f x <*> f y <*> f y'
uniplate1 f (ForAll (Just qv) expr) = ForAll (Just qv) . const <$> f (expr (Var qv))
uniplate1 _ (ForAll Nothing expr) = pure $ ForAll Nothing expr
uniplate1 f (Exists (Just qv) expr) = Exists (Just qv) . const <$> f (expr (Var qv))
uniplate1 _ (Exists Nothing expr) = pure $ Exists Nothing expr
-- | __Caution for quantified expressions:__ 'plate' will only be applied if quantification has taken place already.
instance KnownSMTSort t => Plated (Expr t) where
plate f = uniplate1 (tryPlate f)
where
tryPlate :: forall s f. (KnownSMTSort s, Applicative f) => (Expr s -> f (Expr s)) -> (forall r. KnownSMTSort r => Expr r -> f (Expr r))
tryPlate f' expr = case geq (sortSing @s) (sortSing' expr) of
Just Refl -> f' expr
Nothing -> case expr of
Var _ -> pure expr
Constant _ -> pure expr
Plus x y -> Plus <$> tryPlate f' x <*> tryPlate f' y
Minus x y -> Minus <$> tryPlate f' x <*> tryPlate f' y
Neg x -> Neg <$> tryPlate f' x
Mul x y -> Mul <$> tryPlate f' x <*> tryPlate f' y
Abs x -> Abs <$> tryPlate f' x
Mod x y -> Mod <$> tryPlate f' x <*> tryPlate f' y
Rem x y -> Mod <$> tryPlate f' x <*> tryPlate f' y
IDiv x y -> IDiv <$> tryPlate f' x <*> tryPlate f' y
Div x y -> Div <$> tryPlate f' x <*> tryPlate f' y
LTH x y -> LTH <$> tryPlate f' x <*> tryPlate f' y
LTHE x y -> LTHE <$> tryPlate f' x <*> tryPlate f' y
EQU xs -> EQU <$> traverse (tryPlate f') xs
Distinct xs -> Distinct <$> traverse (tryPlate f') xs
GTHE x y -> GTHE <$> tryPlate f' x <*> tryPlate f' y
GTH x y -> GTH <$> tryPlate f' x <*> tryPlate f' y
Not x -> Not <$> tryPlate f' x
And x y -> And <$> tryPlate f' x <*> tryPlate f' y
Or x y -> Or <$> tryPlate f' x <*> tryPlate f' y
Impl x y -> Impl <$> tryPlate f' x <*> tryPlate f' y
Xor x y -> Xor <$> tryPlate f' x <*> tryPlate f' y
Pi -> pure Pi
Sqrt x -> Sqrt <$> tryPlate f' x
Exp x -> Exp <$> tryPlate f' x
Sin x -> Sin <$> tryPlate f' x
Cos x -> Cos <$> tryPlate f' x
Tan x -> Tan <$> tryPlate f' x
Asin x -> Asin <$> tryPlate f' x
Acos x -> Acos <$> tryPlate f' x
Atan x -> Atan <$> tryPlate f' x
ToReal x -> ToReal <$> tryPlate f' x
ToInt x -> ToInt <$> tryPlate f' x
IsInt x -> IsInt <$> tryPlate f' x
Ite p t n -> Ite <$> tryPlate f' p <*> tryPlate f' t <*> tryPlate f' n
BvNand x y -> BvNand <$> tryPlate f' x <*> tryPlate f' y
BvNor x y -> BvNor <$> tryPlate f' x <*> tryPlate f' y
BvShL x y -> BvShL <$> tryPlate f' x <*> tryPlate f' y
BvLShR x y -> BvLShR <$> tryPlate f' x <*> tryPlate f' y
BvAShR x y -> BvAShR <$> tryPlate f' x <*> tryPlate f' y
BvConcat x y -> BvConcat <$> tryPlate f' x <*> tryPlate f' y
BvRotL i x -> BvRotL i <$> tryPlate f' x
BvRotR i x -> BvRotR i <$> tryPlate f' x
ArrSelect i arr -> ArrSelect i <$> tryPlate f' arr
ArrStore i x arr -> ArrStore i <$> tryPlate f' x <*> tryPlate f' arr
StrConcat x y -> StrConcat <$> tryPlate f' x <*> tryPlate f' y
StrLength x -> StrLength <$> tryPlate f' x
StrAt x i -> StrAt <$> tryPlate f' x <*> tryPlate f' i
StrSubstring x i j -> StrSubstring <$> tryPlate f' x <*> tryPlate f' i <*> tryPlate f' j
StrPrefixOf x y -> StrPrefixOf <$> tryPlate f' x <*> tryPlate f' y
StrSuffixOf x y -> StrSuffixOf <$> tryPlate f' x <*> tryPlate f' y
StrContains x y -> StrContains <$> tryPlate f' x <*> tryPlate f' y
StrIndexOf x y i -> StrIndexOf <$> tryPlate f' x <*> tryPlate f' y <*> tryPlate f' i
StrReplace x y y' -> StrReplace <$> tryPlate f' x <*> tryPlate f' y <*> tryPlate f' y'
StrReplaceAll x y y' -> StrReplaceAll <$> tryPlate f' x <*> tryPlate f' y <*> tryPlate f' y'
ForAll (Just qv) qexpr -> ForAll (Just qv) . const <$> tryPlate f' (qexpr (Var qv))
ForAll Nothing qexpr -> pure $ ForAll Nothing qexpr
Exists (Just qv) qexpr -> Exists (Just qv) . const <$> tryPlate f' (qexpr (Var qv))
Exists Nothing qexpr -> pure $ Exists Nothing qexpr
instance GNFData Expr where
grnf expr = case expr of
Var (SMTVar vId) -> vId `seq` ()
Constant c -> c `seq` ()
Plus e1 e2 -> grnf e1 `seq` grnf e2
Minus e1 e2 -> grnf e1 `seq` grnf e2
Neg e -> grnf e
Mul e1 e2 -> grnf e1 `seq` grnf e2
Abs e -> grnf e
Mod e1 e2 -> grnf e1 `seq` grnf e2
Rem e1 e2 -> grnf e1 `seq` grnf e2
IDiv e1 e2 -> grnf e1 `seq` grnf e2
Div e1 e2 -> grnf e1 `seq` grnf e2
LTH e1 e2 -> grnf e1 `seq` grnf e2
LTHE e1 e2 -> grnf e1 `seq` grnf e2
EQU vec -> vec `seq` V.foldl' (const grnf) () vec
Distinct vec -> vec `seq` V.foldl' (const grnf) () vec
GTHE e1 e2 -> grnf e1 `seq` grnf e2
GTH e1 e2 -> grnf e1 `seq` grnf e2
Not e -> grnf e
And e1 e2 -> grnf e1 `seq` grnf e2
Or e1 e2 -> grnf e1 `seq` grnf e2
Impl e1 e2 -> grnf e1 `seq` grnf e2
Xor e1 e2 -> grnf e1 `seq` grnf e2
Pi -> ()
Sqrt e -> grnf e
Exp e -> grnf e
Sin e -> grnf e
Cos e -> grnf e
Tan e -> grnf e
Asin e -> grnf e
Acos e -> grnf e
Atan e -> grnf e
ToReal e -> grnf e
ToInt e -> grnf e
IsInt e -> grnf e
Ite c e1 e2 -> grnf c `seq` grnf e1 `seq` grnf e2
BvNand e1 e2 -> grnf e1 `seq` grnf e2
BvNor e1 e2 -> grnf e1 `seq` grnf e2
BvShL e1 e2 -> grnf e1 `seq` grnf e2
BvLShR e1 e2 -> grnf e1 `seq` grnf e2
BvAShR e1 e2 -> grnf e1 `seq` grnf e2
BvConcat e1 e2 -> grnf e1 `seq` grnf e2
BvRotL _ e -> grnf e
BvRotR _ e -> grnf e
ArrSelect e1 e2 -> grnf e1 `seq` grnf e2
ArrStore e1 e2 e3 -> grnf e1 `seq` grnf e2 `seq` grnf e3
StrConcat e1 e2 -> grnf e1 `seq` grnf e2
StrLength e -> grnf e
StrAt e1 e2 -> grnf e1 `seq` grnf e2
StrSubstring e1 e2 e3 -> grnf e1 `seq` grnf e2 `seq` grnf e3
StrPrefixOf e1 e2 -> grnf e1 `seq` grnf e2
StrSuffixOf e1 e2 -> grnf e1 `seq` grnf e2
StrContains e1 e2 -> grnf e1 `seq` grnf e2
StrIndexOf e1 e2 e3 -> grnf e1 `seq` grnf e2 `seq` grnf e3
StrReplace e1 e2 e3 -> grnf e1 `seq` grnf e2 `seq` grnf e3
StrReplaceAll e1 e2 e3 -> grnf e1 `seq` grnf e2 `seq` grnf e3
ForAll Nothing _ -> ()
ForAll (Just qv) f -> grnf $ f $ Var qv
Exists Nothing _ -> ()
Exists (Just qv) f -> grnf $ f $ Var qv
instance Eq (Expr t) where
(==) = defaultEq
instance Ord (Expr t) where
compare = defaultCompare
instance GEq Expr where
geq = defaultGeq
gcomparing :: GCompare f => [(f a, f b)] -> GOrdering a b
gcomparing [] = GLT
gcomparing ((x,y):xys) = case gcompare x y of
GEQ -> gcomparing xys
o -> o
instance GCompare Expr where
gcompare (Var v) (Var v') = case gcompare (sortSing' v) (sortSing' v') of
GLT -> GLT
GEQ -> case compare (coerce @_ @Int v) (coerce v') of
LT -> GLT
EQ -> GEQ
GT -> GGT
GGT -> GGT
gcompare (Var _) _ = GLT
gcompare _ (Var _) = GGT
gcompare (Constant c) (Constant c') = gcompare c c'
gcompare (Constant _) _ = GLT
gcompare _ (Constant _) = GGT
gcompare (Plus x y) (Plus x' y') = gcomparing [(x,x'), (y,y')]
gcompare (Plus _ _) _ = GLT
gcompare _ (Plus _ _) = GGT
gcompare (Minus x y) (Minus x' y') = gcomparing [(x,x'), (y,y')]
gcompare (Minus _ _) _ = GLT
gcompare _ (Minus _ _) = GGT
gcompare (Neg x) (Neg x') = gcompare x x'
gcompare (Neg _) _ = GLT
gcompare _ (Neg _) = GGT
gcompare (Mul x y) (Mul x' y') = gcomparing [(x,x'), (y,y')]
gcompare (Mul _ _) _ = GLT
gcompare _ (Mul _ _) = GGT
gcompare (Abs x) (Abs x') = gcompare x x'
gcompare (Abs _) _ = GLT
gcompare _ (Abs _) = GGT
gcompare (Mod x y) (Mod x' y') = gcomparing [(x,x'), (y,y')]
gcompare (Mod _ _) _ = GLT
gcompare _ (Mod _ _) = GGT
gcompare (Rem x y) (Rem x' y') = gcomparing [(x,x'), (y,y')]
gcompare (Rem _ _) _ = GLT
gcompare _ (Rem _ _) = GGT
gcompare (IDiv x y) (IDiv x' y') = gcomparing [(x,x'), (y,y')]
gcompare (IDiv _ _) _ = GLT
gcompare _ (IDiv _ _) = GGT
gcompare (Div x y) (Div x' y') = gcomparing [(x,x'), (y,y')]
gcompare (Div _ _) _ = GLT
gcompare _ (Div _ _) = GGT
gcompare (LTH x y) (LTH x' y') = case gcomparing [(x,x'), (y,y')] of
GLT -> GLT
GEQ -> GEQ
GGT -> GGT
gcompare (LTH _ _) _ = GLT
gcompare _ (LTH _ _) = GGT
gcompare (LTHE x y) (LTHE x' y') = case gcomparing [(x,x'), (y,y')] of
GLT -> GLT
GEQ -> GEQ
GGT -> GGT
gcompare (LTHE _ _) _ = GLT
gcompare _ (LTHE _ _) = GGT
gcompare (EQU (V.toList -> xs)) (EQU (V.toList -> xs')) = case compare (length xs ) (length xs') of
LT -> GLT
EQ -> case gcomparing $ zip xs xs' of
GGT -> GGT
GEQ -> GEQ
GLT -> GLT
GT -> GGT
gcompare (EQU _) _ = GLT
gcompare _ (EQU _) = GGT
gcompare (Distinct (V.toList -> xs)) (Distinct (V.toList -> xs')) = case compare (length xs ) (length xs') of
LT -> GLT
EQ -> case gcomparing $ zip xs xs' of
GGT -> GGT
GEQ -> GEQ
GLT -> GLT
GT -> GGT
gcompare (Distinct _) _ = GLT
gcompare _ (Distinct _) = GGT
gcompare (GTHE x y) (GTHE x' y') = case gcomparing [(x,x'), (y,y')] of
GLT -> GLT
GEQ -> GEQ
GGT -> GGT
gcompare (GTHE _ _) _ = GLT
gcompare _ (GTHE _ _) = GGT
gcompare (GTH x y) (GTH x' y') = case gcomparing [(x,x'), (y,y')] of
GLT -> GLT
GEQ -> GEQ
GGT -> GGT
gcompare (GTH _ _) _ = GLT
gcompare _ (GTH _ _) = GGT
gcompare (Not x) (Not x') = gcompare x x'
gcompare (Not _) _ = GLT
gcompare _ (Not _) = GGT
gcompare (And x y) (And x' y') = gcomparing [(x,x'), (y,y')]
gcompare (And _ _) _ = GLT
gcompare _ (And _ _) = GGT
gcompare (Or x y) (Or x' y') = gcomparing [(x,x'), (y,y')]
gcompare (Or _ _) _ = GLT
gcompare _ (Or _ _) = GGT
gcompare (Impl x y) (Impl x' y') = gcomparing [(x,x'), (y,y')]
gcompare (Impl _ _) _ = GLT
gcompare _ (Impl _ _) = GGT
gcompare (Xor x y) (Xor x' y') = gcomparing [(x,x'), (y,y')]
gcompare (Xor _ _) _ = GLT
gcompare _ (Xor _ _) = GGT
gcompare Pi Pi = GEQ
gcompare Pi _ = GLT
gcompare _ Pi = GGT
gcompare (Sqrt x) (Sqrt x') = gcompare x x'
gcompare (Sqrt _) _ = GLT
gcompare _ (Sqrt _) = GGT
gcompare (Exp x) (Exp x') = gcompare x x'
gcompare (Exp _) _ = GLT
gcompare _ (Exp _) = GGT
gcompare (Sin x) (Sin x') = gcompare x x'
gcompare (Sin _) _ = GLT
gcompare _ (Sin _) = GGT
gcompare (Cos x) (Cos x') = gcompare x x'
gcompare (Cos _) _ = GLT
gcompare _ (Cos _) = GGT
gcompare (Tan x) (Tan x') = gcompare x x'
gcompare (Tan _) _ = GLT
gcompare _ (Tan _) = GGT
gcompare (Asin x) (Asin x') = gcompare x x'
gcompare (Asin _) _ = GLT
gcompare _ (Asin _) = GGT
gcompare (Acos x) (Acos x') = gcompare x x'
gcompare (Acos _) _ = GLT
gcompare _ (Acos _) = GGT
gcompare (Atan x) (Atan x') = gcompare x x'
gcompare (Atan _) _ = GLT
gcompare _ (Atan _) = GGT
gcompare (ToReal x) (ToReal x') = case gcompare x x' of
GLT -> GLT
GEQ -> GEQ
GGT -> GGT
gcompare (ToReal _) _ = GLT
gcompare _ (ToReal _) = GGT
gcompare (ToInt x) (ToInt x') = case gcompare x x' of
GLT -> GLT
GEQ -> GEQ
GGT -> GGT
gcompare (ToInt _) _ = GLT
gcompare _ (ToInt _) = GGT
gcompare (IsInt x) (IsInt x') = case gcompare x x' of
GLT -> GLT
GEQ -> GEQ
GGT -> GGT
gcompare (IsInt _) _ = GLT
gcompare _ (IsInt _) = GGT
gcompare (Ite p t n) (Ite p' t' n') = case gcompare p p' of
GLT -> GLT
GEQ -> gcomparing [(t,t'), (n,n')]
GGT -> GGT
gcompare (Ite _ _ _) _ = GLT
gcompare _ (Ite _ _ _) = GGT
gcompare (BvNand x y) (BvNand x' y') = gcomparing [(x,x'), (y,y')]
gcompare (BvNand _ _) _ = GLT
gcompare _ (BvNand _ _) = GGT
gcompare (BvNor x y) (BvNor x' y') = gcomparing [(x,x'), (y,y')]
gcompare (BvNor _ _) _ = GLT
gcompare _ (BvNor _ _) = GGT
gcompare (BvShL x y) (BvShL x' y') = gcomparing [(x,x'), (y,y')]
gcompare (BvShL _ _) _ = GLT
gcompare _ (BvShL _ _) = GGT
gcompare (BvLShR x y) (BvLShR x' y') = gcomparing [(x,x'), (y,y')]
gcompare (BvLShR _ _) _ = GLT
gcompare _ (BvLShR _ _) = GGT
gcompare (BvAShR x y) (BvAShR x' y') = gcomparing [(x,x'), (y,y')]
gcompare (BvAShR _ _) _ = GLT
gcompare _ (BvAShR _ _) = GGT
gcompare (BvConcat x y) (BvConcat x' y') = case gcompare (sortSing' x) (sortSing' x') of
GLT -> GLT
GEQ -> case gcompare x x' of
GLT -> GLT
GEQ -> case gcompare (sortSing' y) (sortSing' y') of
GLT -> GLT
GEQ -> case gcompare y y' of
GLT -> GLT
GEQ -> GEQ
GGT -> GGT
GGT -> GGT
GGT -> GGT
GGT -> GGT
gcompare (BvConcat _ _) _ = GLT
gcompare _ (BvConcat _ _) = GGT
gcompare (BvRotL i x) (BvRotL i' x') = case compare (fromIntegral i :: Integer) (fromIntegral i') of
LT -> GLT
EQ -> gcompare x x'
GT -> GGT
gcompare (BvRotL _ _) _ = GLT
gcompare _ (BvRotL _ _) = GGT
gcompare (BvRotR i x) (BvRotR i' x') = case compare (fromIntegral i :: Integer) (fromIntegral i') of
LT -> GLT
EQ -> gcompare x x'
GT -> GGT
gcompare (BvRotR _ _) _ = GLT
gcompare _ (BvRotR _ _) = GGT
gcompare (ArrSelect arr i) (ArrSelect arr' i') = case gcompare arr arr' of
GLT -> GLT
GEQ -> case gcompare i i' of
GLT -> GLT
GEQ -> GEQ
GGT -> GGT
GGT -> GGT
gcompare (ArrSelect _ _) _ = GLT
gcompare _ (ArrSelect _ _) = GGT
gcompare (ArrStore arr k v) (ArrStore arr' k' v') = case gcompare arr arr' of
GLT -> GLT
GEQ -> case gcompare k k' of
GLT -> GLT
GEQ -> case gcompare v v' of
GLT -> GLT
GEQ -> GEQ
GGT -> GGT
GGT -> GGT
GGT -> GGT
gcompare (ArrStore _ _ _) _ = GLT
gcompare _ (ArrStore _ _ _) = GGT
gcompare (StrConcat x y) (StrConcat x' y') = gcomparing [(x,x'), (y,y')]
gcompare (StrConcat _ _) _ = GLT
gcompare _ (StrConcat _ _) = GGT
gcompare (StrLength x) (StrLength x') = case gcompare x x' of
GLT -> GLT
GEQ -> GEQ
GGT -> GGT
gcompare (StrLength _) _ = GLT
gcompare _ (StrLength _) = GGT
gcompare (StrAt x i) (StrAt x' i') = case gcompare x x' of
GLT -> GLT
GEQ -> case gcompare i i' of
GLT -> GLT
GEQ -> GEQ
GGT -> GGT
GGT -> GGT
gcompare (StrAt _ _) _ = GLT
gcompare _ (StrAt _ _) = GGT
gcompare (StrSubstring x i j) (StrSubstring x' i' j') = case gcompare x x' of
GLT -> GLT
GEQ -> case gcomparing [(i,i'), (j,j')] of
GLT -> GLT
GEQ -> GEQ
GGT -> GGT
GGT -> GGT
gcompare (StrSubstring _ _ _) _ = GLT
gcompare _ (StrSubstring _ _ _) = GGT
gcompare (StrPrefixOf x y) (StrPrefixOf x' y') = case gcomparing [(x,x'), (y,y')] of
GLT -> GLT
GEQ -> GEQ
GGT -> GGT
gcompare (StrPrefixOf _ _) _ = GLT
gcompare _ (StrPrefixOf _ _) = GGT
gcompare (StrSuffixOf x y) (StrSuffixOf x' y') = case gcomparing [(x,x'), (y,y')] of
GLT -> GLT
GEQ -> GEQ
GGT -> GGT
gcompare (StrSuffixOf _ _) _ = GLT
gcompare _ (StrSuffixOf _ _) = GGT
gcompare (StrContains x y) (StrContains x' y') = case gcomparing [(x,x'), (y,y')] of
GLT -> GLT
GEQ -> GEQ
GGT -> GGT
gcompare (StrContains _ _) _ = GLT
gcompare _ (StrContains _ _) = GGT
gcompare (StrIndexOf x y i) (StrIndexOf x' y' i') = case gcomparing [(x,x'), (y,y')] of
GLT -> GLT
GEQ -> gcompare i i'
GGT -> GGT
gcompare (StrIndexOf _ _ _) _ = GLT
gcompare _ (StrIndexOf _ _ _) = GGT
gcompare (StrReplace source target replacement) (StrReplace source' target' replacement') = gcomparing [(source, source'), (target, target'), (replacement, replacement')]
gcompare (StrReplace _ _ _) _ = GLT
gcompare _ (StrReplace _ _ _) = GGT
gcompare (StrReplaceAll source target replacement) (StrReplaceAll source' target' replacement') = gcomparing [(source, source'), (target, target'), (replacement, replacement')]
gcompare (StrReplaceAll _ _ _) _ = GLT
gcompare _ (StrReplaceAll _ _ _) = GGT
gcompare (ForAll _ expr) (ForAll _ expr') = gcompare (expr $ Var (SMTVar (-1))) (expr' $ Var (SMTVar (-1)))
gcompare (ForAll _ _) _ = GLT
gcompare _ (ForAll _ _) = GGT
gcompare (Exists _ expr) (Exists _ expr') = gcompare (expr $ Var (SMTVar (-1))) (expr' $ Var (SMTVar (-1)))
-- gcompare (Exists _ _) _ = GLT
-- gcompare _ (Exists _ _) = GGT