-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Uninterpreted.EUFLogic
-- License   : BSD3
-- Stability : experimental
--
-- Demonstrates the ability to generate uninterpreted functions of arbitrarily
-- many arguments, whose types are generated programmatically. The high-level
-- idea of this module is to provide a strongly-typed representation, using a
-- GADT, of a logic that includes uninterpreted functions. This module then
-- defines an interpretation of this logic into SBV, which it uses to perform
-- SMT queries in the logic.
-----------------------------------------------------------------------------

{-# LANGUAGE CPP                  #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE GADTs                #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

module Documentation.SBV.Examples.Uninterpreted.EUFLogic where

import Data.SBV

import Control.Monad.State

import Data.Kind
import Data.Type.Equality
import Data.Map (Map)
import qualified Data.Map as Map

import GHC.TypeLits

#ifdef DOCTEST
-- $setup
-- >>> import Data.SBV
#endif

----------------------------------------------------------------------
-- * Types of the EUF Logic
----------------------------------------------------------------------

-- | The datakind for the types in our EUF logic.
data EUFType = Tp_Bool | Tp_BV Natural

-- | A singleton type for natural numbers that can be used as the widths of bitvectors.
data BVWidth w = (KnownNat w, BVIsNonZero w) => BVWidth (SNat w)

-- | Create a t'BVWidth' object for a 'KnownNat' that is non-zero
knownBVWidth :: (KnownNat w, BVIsNonZero w) => BVWidth w
knownBVWidth :: forall (w :: Nat). (KnownNat w, BVIsNonZero w) => BVWidth w
knownBVWidth = SNat w -> BVWidth w
forall (w :: Nat).
(KnownNat w, BVIsNonZero w) =>
SNat w -> BVWidth w
BVWidth SNat w
forall (n :: Nat). KnownNat n => SNat n
natSing

-- | TestEquality instance for BVWidth.
instance TestEquality BVWidth where
  testEquality :: forall (a :: Nat) (b :: Nat).
BVWidth a -> BVWidth b -> Maybe (a :~: b)
testEquality (BVWidth SNat a
w1) (BVWidth SNat b
w2) | Just a :~: b
Refl <- SNat a -> SNat b -> Maybe (a :~: b)
forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality SNat a
w1 SNat b
w2 = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
                                         | Bool
True                            = Maybe (a :~: b)
forall a. Maybe a
Nothing

-- | A singleton type that represents type-level 'EUFType's at the object level
data TypeRepr (tp :: EUFType) where
  Repr_Bool :: TypeRepr Tp_Bool
  Repr_BV   :: BVWidth w -> TypeRepr (Tp_BV w)

-- | TestEquality instance for Type representations
instance TestEquality TypeRepr where
  testEquality :: forall (a :: EUFType) (b :: EUFType).
TypeRepr a -> TypeRepr b -> Maybe (a :~: b)
testEquality TypeRepr a
Repr_Bool    TypeRepr b
Repr_Bool                                      = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality (Repr_BV BVWidth w
w1) (Repr_BV BVWidth w
w2) | Just w :~: w
Refl <- BVWidth w -> BVWidth w -> Maybe (w :~: w)
forall (a :: Nat) (b :: Nat).
BVWidth a -> BVWidth b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality BVWidth w
w1 BVWidth w
w2 = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality TypeRepr a
_            TypeRepr b
_                                              = Maybe (a :~: b)
forall a. Maybe a
Nothing

-- | A list of 'TypeRepr's for each type in a type-level list
data TypeReprs tps where
  Repr_Nil  :: TypeReprs '[]
  Repr_Cons :: TypeRepr tp -> TypeReprs tps -> TypeReprs (tp ': tps)

instance TestEquality TypeReprs where
  testEquality :: forall (a :: [EUFType]) (b :: [EUFType]).
TypeReprs a -> TypeReprs b -> Maybe (a :~: b)
testEquality TypeReprs a
Repr_Nil             TypeReprs b
Repr_Nil                                                    = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality (Repr_Cons TypeRepr tp
tps1 TypeReprs tps
tp1) (Repr_Cons TypeRepr tp
tps2 TypeReprs tps
tp2) | Just tp :~: tp
Refl <- TypeRepr tp -> TypeRepr tp -> Maybe (tp :~: tp)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: EUFType) (b :: EUFType).
TypeRepr a -> TypeRepr b -> Maybe (a :~: b)
testEquality TypeRepr tp
tps1 TypeRepr tp
tps2
                                                         , Just tps :~: tps
Refl <- TypeReprs tps -> TypeReprs tps -> Maybe (tps :~: tps)
forall (a :: [EUFType]) (b :: [EUFType]).
TypeReprs a -> TypeReprs b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality TypeReprs tps
tp1  TypeReprs tps
tp2   = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
  testEquality TypeReprs a
_                    TypeReprs b
_                                                           = Maybe (a :~: b)
forall a. Maybe a
Nothing

-- | An 'EUFType' with a known 'TypeRepr' representation
class KnownEUFType tp where
  knownEUFType :: TypeRepr tp

-- | Mapping from Tp_Bool
instance KnownEUFType Tp_Bool where
  knownEUFType :: TypeRepr 'Tp_Bool
knownEUFType = TypeRepr 'Tp_Bool
Repr_Bool

-- | Mapping from Tp_BV
instance (KnownNat w, BVIsNonZero w) => KnownEUFType (Tp_BV w) where
  knownEUFType :: TypeRepr ('Tp_BV w)
knownEUFType = BVWidth w -> TypeRepr ('Tp_BV w)
forall (w :: Nat). BVWidth w -> TypeRepr ('Tp_BV w)
Repr_BV (SNat w -> BVWidth w
forall (w :: Nat).
(KnownNat w, BVIsNonZero w) =>
SNat w -> BVWidth w
BVWidth SNat w
forall (n :: Nat). KnownNat n => SNat n
natSing)

-- | A sequence of types t'EUFType' with a known 'TypeReprs' representation
class KnownEUFTypes tps where
  knownEUFTypes :: TypeReprs tps

instance KnownEUFTypes '[] where
  knownEUFTypes :: TypeReprs '[]
knownEUFTypes = TypeReprs '[]
Repr_Nil

instance (KnownEUFType tp, KnownEUFTypes tps) => KnownEUFTypes (tp ': tps) where
  knownEUFTypes :: TypeReprs (tp : tps)
knownEUFTypes = TypeRepr tp -> TypeReprs tps -> TypeReprs (tp : tps)
forall (w :: EUFType) (tps :: [EUFType]).
TypeRepr w -> TypeReprs tps -> TypeReprs (w : tps)
Repr_Cons TypeRepr tp
forall (tp :: EUFType). KnownEUFType tp => TypeRepr tp
knownEUFType TypeReprs tps
forall (tps :: [EUFType]). KnownEUFTypes tps => TypeReprs tps
knownEUFTypes

----------------------------------------------------------------------
-- * Operations of the EUF Logic
----------------------------------------------------------------------

-- | An uninterpreted function in our EUF logic, which is a string name plus the input and output types.
data UnintOp (ins :: [EUFType]) (out :: EUFType) = UnintOp { forall (ins :: [EUFType]) (out :: EUFType).
UnintOp ins out -> String
unintOpName :: String
                                                           , forall (ins :: [EUFType]) (out :: EUFType).
UnintOp ins out -> TypeReprs ins
unintOpIns :: TypeReprs ins
                                                           , forall (ins :: [EUFType]) (out :: EUFType).
UnintOp ins out -> TypeRepr out
unintOpOut :: TypeRepr  out
                                                           }

-- | The operations of our EUF logic, which are indexed by a list of 0 or more
-- input types and a single output type.
data Op (ins :: [EUFType]) (out :: EUFType) where
  -- Uninterpreted functions
  Op_Unint :: UnintOp ins out -> Op ins out

  -- Boolean operations
  Op_And        :: Op (Tp_Bool ': Tp_Bool ': '[]) Tp_Bool
  Op_Or         :: Op (Tp_Bool ': Tp_Bool ': '[]) Tp_Bool
  Op_Not        :: Op (Tp_Bool ': '[])            Tp_Bool
  Op_BoolLit    :: Bool -> Op '[] Tp_Bool
  Op_IfThenElse :: TypeRepr a -> Op (Tp_Bool ': a ': a ': '[]) a

  -- Bitvector operations
  Op_Plus   :: BVWidth w -> Op (Tp_BV w ': Tp_BV w ': '[]) (Tp_BV w)
  Op_Minus  :: BVWidth w -> Op (Tp_BV w ': Tp_BV w ': '[]) (Tp_BV w)
  Op_Times  :: BVWidth w -> Op (Tp_BV w ': Tp_BV w ': '[]) (Tp_BV w)

  Op_Abs    :: BVWidth w -> Op (Tp_BV w ': '[]) (Tp_BV w)
  Op_Signum :: BVWidth w -> Op (Tp_BV w ': '[]) (Tp_BV w)

  Op_BVLit  :: BVWidth w -> Integer -> Op '[] (Tp_BV w)

  Op_BVEq   :: BVWidth w -> Op (Tp_BV w ': Tp_BV w ': '[]) Tp_Bool
  Op_BVLt   :: BVWidth w -> Op (Tp_BV w ': Tp_BV w ': '[]) Tp_Bool

-- | Create an uninterpreted 'Op' of known type
mkUnintOp :: (KnownEUFTypes ins, KnownEUFType out) => String -> Op ins out
mkUnintOp :: forall (ins :: [EUFType]) (out :: EUFType).
(KnownEUFTypes ins, KnownEUFType out) =>
String -> Op ins out
mkUnintOp String
nm = UnintOp ins out -> Op ins out
forall (ins :: [EUFType]) (out :: EUFType).
UnintOp ins out -> Op ins out
Op_Unint (UnintOp ins out -> Op ins out) -> UnintOp ins out -> Op ins out
forall a b. (a -> b) -> a -> b
$ String -> TypeReprs ins -> TypeRepr out -> UnintOp ins out
forall (ins :: [EUFType]) (out :: EUFType).
String -> TypeReprs ins -> TypeRepr out -> UnintOp ins out
UnintOp String
nm TypeReprs ins
forall (tps :: [EUFType]). KnownEUFTypes tps => TypeReprs tps
knownEUFTypes TypeRepr out
forall (tp :: EUFType). KnownEUFType tp => TypeRepr tp
knownEUFType

-- | Get the input types and output type of an 'Op'
opInsOut :: Op ins out -> (TypeReprs ins, TypeRepr out)
opInsOut :: forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> (TypeReprs ins, TypeRepr out)
opInsOut (Op_Unint UnintOp ins out
uop)                      = (UnintOp ins out -> TypeReprs ins
forall (ins :: [EUFType]) (out :: EUFType).
UnintOp ins out -> TypeReprs ins
unintOpIns UnintOp ins out
uop, UnintOp ins out -> TypeRepr out
forall (ins :: [EUFType]) (out :: EUFType).
UnintOp ins out -> TypeRepr out
unintOpOut UnintOp ins out
uop)
opInsOut Op ins out
Op_And                              = (TypeReprs ins
forall (tps :: [EUFType]). KnownEUFTypes tps => TypeReprs tps
knownEUFTypes, TypeRepr out
forall (tp :: EUFType). KnownEUFType tp => TypeRepr tp
knownEUFType)
opInsOut Op ins out
Op_Or                               = (TypeReprs ins
forall (tps :: [EUFType]). KnownEUFTypes tps => TypeReprs tps
knownEUFTypes, TypeRepr out
forall (tp :: EUFType). KnownEUFType tp => TypeRepr tp
knownEUFType)
opInsOut Op ins out
Op_Not                              = (TypeReprs ins
forall (tps :: [EUFType]). KnownEUFTypes tps => TypeReprs tps
knownEUFTypes, TypeRepr out
forall (tp :: EUFType). KnownEUFType tp => TypeRepr tp
knownEUFType)
opInsOut (Op_BoolLit Bool
_)                      = (TypeReprs ins
forall (tps :: [EUFType]). KnownEUFTypes tps => TypeReprs tps
knownEUFTypes, TypeRepr out
forall (tp :: EUFType). KnownEUFType tp => TypeRepr tp
knownEUFType)
opInsOut (Op_IfThenElse TypeRepr out
Repr_Bool)           = (TypeReprs ins
forall (tps :: [EUFType]). KnownEUFTypes tps => TypeReprs tps
knownEUFTypes, TypeRepr out
forall (tp :: EUFType). KnownEUFType tp => TypeRepr tp
knownEUFType)
opInsOut (Op_IfThenElse (Repr_BV BVWidth{})) = (TypeReprs ins
forall (tps :: [EUFType]). KnownEUFTypes tps => TypeReprs tps
knownEUFTypes, TypeRepr out
forall (tp :: EUFType). KnownEUFType tp => TypeRepr tp
knownEUFType)
opInsOut (Op_Plus       BVWidth{})           = (TypeReprs ins
forall (tps :: [EUFType]). KnownEUFTypes tps => TypeReprs tps
knownEUFTypes, TypeRepr out
forall (tp :: EUFType). KnownEUFType tp => TypeRepr tp
knownEUFType)
opInsOut (Op_Minus      BVWidth{})           = (TypeReprs ins
forall (tps :: [EUFType]). KnownEUFTypes tps => TypeReprs tps
knownEUFTypes, TypeRepr out
forall (tp :: EUFType). KnownEUFType tp => TypeRepr tp
knownEUFType)
opInsOut (Op_Times      BVWidth{})           = (TypeReprs ins
forall (tps :: [EUFType]). KnownEUFTypes tps => TypeReprs tps
knownEUFTypes, TypeRepr out
forall (tp :: EUFType). KnownEUFType tp => TypeRepr tp
knownEUFType)
opInsOut (Op_Abs        BVWidth{})           = (TypeReprs ins
forall (tps :: [EUFType]). KnownEUFTypes tps => TypeReprs tps
knownEUFTypes, TypeRepr out
forall (tp :: EUFType). KnownEUFType tp => TypeRepr tp
knownEUFType)
opInsOut (Op_Signum     BVWidth{})           = (TypeReprs ins
forall (tps :: [EUFType]). KnownEUFTypes tps => TypeReprs tps
knownEUFTypes, TypeRepr out
forall (tp :: EUFType). KnownEUFType tp => TypeRepr tp
knownEUFType)
opInsOut (Op_BVLit      BVWidth{} Integer
_)         = (TypeReprs ins
forall (tps :: [EUFType]). KnownEUFTypes tps => TypeReprs tps
knownEUFTypes, TypeRepr out
forall (tp :: EUFType). KnownEUFType tp => TypeRepr tp
knownEUFType)
opInsOut (Op_BVEq       BVWidth{})           = (TypeReprs ins
forall (tps :: [EUFType]). KnownEUFTypes tps => TypeReprs tps
knownEUFTypes, TypeRepr out
forall (tp :: EUFType). KnownEUFType tp => TypeRepr tp
knownEUFType)
opInsOut (Op_BVLt       BVWidth{})           = (TypeReprs ins
forall (tps :: [EUFType]). KnownEUFTypes tps => TypeReprs tps
knownEUFTypes, TypeRepr out
forall (tp :: EUFType). KnownEUFType tp => TypeRepr tp
knownEUFType)

-- | Get the input types of an 'Op'
opIns :: Op ins out -> TypeReprs ins
opIns :: forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> TypeReprs ins
opIns = (TypeReprs ins, TypeRepr out) -> TypeReprs ins
forall a b. (a, b) -> a
fst ((TypeReprs ins, TypeRepr out) -> TypeReprs ins)
-> (Op ins out -> (TypeReprs ins, TypeRepr out))
-> Op ins out
-> TypeReprs ins
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Op ins out -> (TypeReprs ins, TypeRepr out)
forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> (TypeReprs ins, TypeRepr out)
opInsOut

----------------------------------------------------------------------
-- * Expressions of the EUF Logic
----------------------------------------------------------------------

-- | The expressions of our EUF logic, which are just operations applied to argument expressions.
data EUFExpr tp where
  EUFExpr :: Op ins out -> EUFExprs ins -> EUFExpr out

-- | A sequence of expressions for each type in a type-level list
data EUFExprs tps where
  EUFExprsNil  :: EUFExprs '[]
  EUFExprsCons :: EUFExpr tp -> EUFExprs tps -> EUFExprs (tp ': tps)

-- | Build the type @t'EUFExpr' in1 -> ... -> t'EUFExpr' inn -> out@
type family EUFExprFun (ins :: [EUFType]) (out :: EUFType) :: Type where
  EUFExprFun '[]         out = EUFExpr out
  EUFExprFun (tp ': tps) out = EUFExpr tp -> EUFExprFun tps out

-- | Build an t'EUFExprFun' from a function on t'EUFExprs'
lambdaEUFExprFun :: TypeReprs ins -> (EUFExprs ins -> EUFExpr out) -> EUFExprFun ins out
lambdaEUFExprFun :: forall (ins :: [EUFType]) (out :: EUFType).
TypeReprs ins
-> (EUFExprs ins -> EUFExpr out) -> EUFExprFun ins out
lambdaEUFExprFun TypeReprs ins
Repr_Nil          EUFExprs ins -> EUFExpr out
f = EUFExprs ins -> EUFExpr out
f EUFExprs ins
EUFExprs '[]
EUFExprsNil
lambdaEUFExprFun (Repr_Cons TypeRepr tp
_ TypeReprs tps
tps) EUFExprs ins -> EUFExpr out
f = \EUFExpr tp
e -> TypeReprs tps
-> (EUFExprs tps -> EUFExpr out) -> EUFExprFun tps out
forall (ins :: [EUFType]) (out :: EUFType).
TypeReprs ins
-> (EUFExprs ins -> EUFExpr out) -> EUFExprFun ins out
lambdaEUFExprFun TypeReprs tps
tps (EUFExprs ins -> EUFExpr out
f (EUFExprs ins -> EUFExpr out)
-> (EUFExprs tps -> EUFExprs ins) -> EUFExprs tps -> EUFExpr out
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EUFExpr tp -> EUFExprs tps -> EUFExprs (tp : tps)
forall (w :: EUFType) (tps :: [EUFType]).
EUFExpr w -> EUFExprs tps -> EUFExprs (w : tps)
EUFExprsCons EUFExpr tp
e)

-- | Apply an 'Op' to t'EUFExprs' for its input types, returning an t'EUFExpr' for its output type
applyOp :: Op ins out -> EUFExprFun ins out
applyOp :: forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> EUFExprFun ins out
applyOp Op ins out
op = TypeReprs ins
-> (EUFExprs ins -> EUFExpr out) -> EUFExprFun ins out
forall (ins :: [EUFType]) (out :: EUFType).
TypeReprs ins
-> (EUFExprs ins -> EUFExpr out) -> EUFExprFun ins out
lambdaEUFExprFun (Op ins out -> TypeReprs ins
forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> TypeReprs ins
opIns Op ins out
op) (Op ins out -> EUFExprs ins -> EUFExpr out
forall (w :: [EUFType]) (out :: EUFType).
Op w out -> EUFExprs w -> EUFExpr out
EUFExpr Op ins out
op)

instance (KnownNat w, BVIsNonZero w) => Num (EUFExpr (Tp_BV w)) where
  fromInteger :: Integer -> EUFExpr ('Tp_BV w)
fromInteger Integer
i = Op '[] ('Tp_BV w) -> EUFExprFun '[] ('Tp_BV w)
forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> EUFExprFun ins out
applyOp (BVWidth w -> Integer -> Op '[] ('Tp_BV w)
forall (w :: Nat). BVWidth w -> Integer -> Op '[] ('Tp_BV w)
Op_BVLit BVWidth w
forall (w :: Nat). (KnownNat w, BVIsNonZero w) => BVWidth w
knownBVWidth Integer
i)

  EUFExpr ('Tp_BV w)
e1 + :: EUFExpr ('Tp_BV w) -> EUFExpr ('Tp_BV w) -> EUFExpr ('Tp_BV w)
+ EUFExpr ('Tp_BV w)
e2 = Op '[ 'Tp_BV w, 'Tp_BV w] ('Tp_BV w)
-> EUFExprFun '[ 'Tp_BV w, 'Tp_BV w] ('Tp_BV w)
forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> EUFExprFun ins out
applyOp (BVWidth w -> Op '[ 'Tp_BV w, 'Tp_BV w] ('Tp_BV w)
forall (w :: Nat).
BVWidth w -> Op '[ 'Tp_BV w, 'Tp_BV w] ('Tp_BV w)
Op_Plus  BVWidth w
forall (w :: Nat). (KnownNat w, BVIsNonZero w) => BVWidth w
knownBVWidth) EUFExpr ('Tp_BV w)
e1 EUFExpr ('Tp_BV w)
e2
  EUFExpr ('Tp_BV w)
e1 - :: EUFExpr ('Tp_BV w) -> EUFExpr ('Tp_BV w) -> EUFExpr ('Tp_BV w)
- EUFExpr ('Tp_BV w)
e2 = Op '[ 'Tp_BV w, 'Tp_BV w] ('Tp_BV w)
-> EUFExprFun '[ 'Tp_BV w, 'Tp_BV w] ('Tp_BV w)
forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> EUFExprFun ins out
applyOp (BVWidth w -> Op '[ 'Tp_BV w, 'Tp_BV w] ('Tp_BV w)
forall (w :: Nat).
BVWidth w -> Op '[ 'Tp_BV w, 'Tp_BV w] ('Tp_BV w)
Op_Minus BVWidth w
forall (w :: Nat). (KnownNat w, BVIsNonZero w) => BVWidth w
knownBVWidth) EUFExpr ('Tp_BV w)
e1 EUFExpr ('Tp_BV w)
e2
  EUFExpr ('Tp_BV w)
e1 * :: EUFExpr ('Tp_BV w) -> EUFExpr ('Tp_BV w) -> EUFExpr ('Tp_BV w)
* EUFExpr ('Tp_BV w)
e2 = Op '[ 'Tp_BV w, 'Tp_BV w] ('Tp_BV w)
-> EUFExprFun '[ 'Tp_BV w, 'Tp_BV w] ('Tp_BV w)
forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> EUFExprFun ins out
applyOp (BVWidth w -> Op '[ 'Tp_BV w, 'Tp_BV w] ('Tp_BV w)
forall (w :: Nat).
BVWidth w -> Op '[ 'Tp_BV w, 'Tp_BV w] ('Tp_BV w)
Op_Times BVWidth w
forall (w :: Nat). (KnownNat w, BVIsNonZero w) => BVWidth w
knownBVWidth) EUFExpr ('Tp_BV w)
e1 EUFExpr ('Tp_BV w)
e2

  abs :: EUFExpr ('Tp_BV w) -> EUFExpr ('Tp_BV w)
abs    EUFExpr ('Tp_BV w)
e = Op '[ 'Tp_BV w] ('Tp_BV w) -> EUFExprFun '[ 'Tp_BV w] ('Tp_BV w)
forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> EUFExprFun ins out
applyOp (BVWidth w -> Op '[ 'Tp_BV w] ('Tp_BV w)
forall (w :: Nat). BVWidth w -> Op '[ 'Tp_BV w] ('Tp_BV w)
Op_Abs    BVWidth w
forall (w :: Nat). (KnownNat w, BVIsNonZero w) => BVWidth w
knownBVWidth) EUFExpr ('Tp_BV w)
e
  signum :: EUFExpr ('Tp_BV w) -> EUFExpr ('Tp_BV w)
signum EUFExpr ('Tp_BV w)
e = Op '[ 'Tp_BV w] ('Tp_BV w) -> EUFExprFun '[ 'Tp_BV w] ('Tp_BV w)
forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> EUFExprFun ins out
applyOp (BVWidth w -> Op '[ 'Tp_BV w] ('Tp_BV w)
forall (w :: Nat). BVWidth w -> Op '[ 'Tp_BV w] ('Tp_BV w)
Op_Signum BVWidth w
forall (w :: Nat). (KnownNat w, BVIsNonZero w) => BVWidth w
knownBVWidth) EUFExpr ('Tp_BV w)
e

-- | Build an expression from an uninterpreted operation of a known type
mkUnintExpr :: KnownEUFType tp => String -> EUFExpr tp
mkUnintExpr :: forall (tp :: EUFType). KnownEUFType tp => String -> EUFExpr tp
mkUnintExpr String
nm = Op '[] tp -> EUFExprs '[] -> EUFExpr tp
forall (w :: [EUFType]) (out :: EUFType).
Op w out -> EUFExprs w -> EUFExpr out
EUFExpr (String -> Op '[] tp
forall (ins :: [EUFType]) (out :: EUFType).
(KnownEUFTypes ins, KnownEUFType out) =>
String -> Op ins out
mkUnintOp String
nm) EUFExprs '[]
EUFExprsNil

----------------------------------------------------------------------
-- * Interpreting the EUF Logic into SBV
----------------------------------------------------------------------

-- | Convert an 'EUFType' to a type of SBV expressions
type family Type2SBV (tp :: EUFType) :: Type where
  Type2SBV Tp_Bool   = SBool
  Type2SBV (Tp_BV w) = SBV (WordN w)

-- | Convert the type inputs plus output of an 'Op' to a function over 'SBV' values
type family OpTypes2SBV (ins :: [EUFType]) (out :: EUFType) :: Type where
  OpTypes2SBV '[] out         = Type2SBV out
  OpTypes2SBV (tp ': tps) out = Type2SBV tp -> OpTypes2SBV tps out

-- | Create an 'SMTDefinable' instance for the type returned by 'OpTypes2SBV' and pass it to a local function
withSMTDefOpTypes :: TypeReprs ins -> TypeRepr out -> (SMTDefinable (OpTypes2SBV ins out) => a) -> a
withSMTDefOpTypes :: forall (ins :: [EUFType]) (out :: EUFType) a.
TypeReprs ins
-> TypeRepr out -> (SMTDefinable (OpTypes2SBV ins out) => a) -> a
withSMTDefOpTypes TypeReprs ins
Repr_Nil                            TypeRepr out
Repr_Bool           SMTDefinable (OpTypes2SBV ins out) => a
f = a
SMTDefinable (OpTypes2SBV ins out) => a
f
withSMTDefOpTypes TypeReprs ins
Repr_Nil                            (Repr_BV BVWidth{}) SMTDefinable (OpTypes2SBV ins out) => a
f = a
SMTDefinable (OpTypes2SBV ins out) => a
f
withSMTDefOpTypes (Repr_Cons TypeRepr tp
Repr_Bool TypeReprs tps
ins)           TypeRepr out
out                 SMTDefinable (OpTypes2SBV ins out) => a
f = TypeReprs tps
-> TypeRepr out -> (SMTDefinable (OpTypes2SBV tps out) => a) -> a
forall (ins :: [EUFType]) (out :: EUFType) a.
TypeReprs ins
-> TypeRepr out -> (SMTDefinable (OpTypes2SBV ins out) => a) -> a
withSMTDefOpTypes TypeReprs tps
ins TypeRepr out
out a
SMTDefinable (OpTypes2SBV ins out) => a
SMTDefinable (OpTypes2SBV tps out) => a
f
withSMTDefOpTypes (Repr_Cons (Repr_BV BVWidth{}) TypeReprs tps
ins) TypeRepr out
out                 SMTDefinable (OpTypes2SBV ins out) => a
f = TypeReprs tps
-> TypeRepr out -> (SMTDefinable (OpTypes2SBV tps out) => a) -> a
forall (ins :: [EUFType]) (out :: EUFType) a.
TypeReprs ins
-> TypeRepr out -> (SMTDefinable (OpTypes2SBV ins out) => a) -> a
withSMTDefOpTypes TypeReprs tps
ins TypeRepr out
out a
SMTDefinable (OpTypes2SBV ins out) => a
SMTDefinable (OpTypes2SBV tps out) => a
f

-- | An uninterpreted function that has been resolved to an 'SBV' function
data ResolvedUnintOp = forall ins out. ResolvedUnintOp (UnintOp ins out) (OpTypes2SBV ins out)

-- | A 'Map' for resolving uninterpreted operations
type UnintMap = Map String ResolvedUnintOp

-- | Look up the uninterpreted op associated with a 'String' in an 'UnintMap' at
-- a particular type, raising an error if that 'String' is associated with a
-- different type. If the 'String' is not associated with any uninterpreted
-- function, create one and return it, updating the 'UnintMap'.
unintEnsure :: UnintOp ins out -> UnintMap -> (OpTypes2SBV ins out, UnintMap)
unintEnsure :: forall (ins :: [EUFType]) (out :: EUFType).
UnintOp ins out -> UnintMap -> (OpTypes2SBV ins out, UnintMap)
unintEnsure UnintOp ins out
uop UnintMap
m
  | Just (ResolvedUnintOp UnintOp ins out
uop' OpTypes2SBV ins out
f) <- String -> UnintMap -> Maybe ResolvedUnintOp
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (UnintOp ins out -> String
forall (ins :: [EUFType]) (out :: EUFType).
UnintOp ins out -> String
unintOpName UnintOp ins out
uop) UnintMap
m
  , Just ins :~: ins
Refl <- TypeReprs ins -> TypeReprs ins -> Maybe (ins :~: ins)
forall (a :: [EUFType]) (b :: [EUFType]).
TypeReprs a -> TypeReprs b -> Maybe (a :~: b)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (UnintOp ins out -> TypeReprs ins
forall (ins :: [EUFType]) (out :: EUFType).
UnintOp ins out -> TypeReprs ins
unintOpIns UnintOp ins out
uop) (UnintOp ins out -> TypeReprs ins
forall (ins :: [EUFType]) (out :: EUFType).
UnintOp ins out -> TypeReprs ins
unintOpIns UnintOp ins out
uop')
  , Just out :~: out
Refl <- TypeRepr out -> TypeRepr out -> Maybe (out :~: out)
forall {k} (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: EUFType) (b :: EUFType).
TypeRepr a -> TypeRepr b -> Maybe (a :~: b)
testEquality (UnintOp ins out -> TypeRepr out
forall (ins :: [EUFType]) (out :: EUFType).
UnintOp ins out -> TypeRepr out
unintOpOut UnintOp ins out
uop) (UnintOp ins out -> TypeRepr out
forall (ins :: [EUFType]) (out :: EUFType).
UnintOp ins out -> TypeRepr out
unintOpOut UnintOp ins out
uop')
  = (OpTypes2SBV ins out
OpTypes2SBV ins out
f, UnintMap
m)
unintEnsure UnintOp ins out
uop UnintMap
m
  | Just ResolvedUnintOp
_ <- String -> UnintMap -> Maybe ResolvedUnintOp
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (UnintOp ins out -> String
forall (ins :: [EUFType]) (out :: EUFType).
UnintOp ins out -> String
unintOpName UnintOp ins out
uop) UnintMap
m
  = String -> (OpTypes2SBV ins out, UnintMap)
forall a. HasCallStack => String -> a
error (String -> (OpTypes2SBV ins out, UnintMap))
-> String -> (OpTypes2SBV ins out, UnintMap)
forall a b. (a -> b) -> a -> b
$ String
"unintEnsure: uninterpreted op " String -> String -> String
forall a. [a] -> [a] -> [a]
++ UnintOp ins out -> String
forall (ins :: [EUFType]) (out :: EUFType).
UnintOp ins out -> String
unintOpName UnintOp ins out
uop String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" used at incorrect type"
unintEnsure UnintOp ins out
uop UnintMap
m =
  TypeReprs ins
-> TypeRepr out
-> (SMTDefinable (OpTypes2SBV ins out) =>
    (OpTypes2SBV ins out, UnintMap))
-> (OpTypes2SBV ins out, UnintMap)
forall (ins :: [EUFType]) (out :: EUFType) a.
TypeReprs ins
-> TypeRepr out -> (SMTDefinable (OpTypes2SBV ins out) => a) -> a
withSMTDefOpTypes (UnintOp ins out -> TypeReprs ins
forall (ins :: [EUFType]) (out :: EUFType).
UnintOp ins out -> TypeReprs ins
unintOpIns UnintOp ins out
uop) (UnintOp ins out -> TypeRepr out
forall (ins :: [EUFType]) (out :: EUFType).
UnintOp ins out -> TypeRepr out
unintOpOut UnintOp ins out
uop)
     ((SMTDefinable (OpTypes2SBV ins out) =>
  (OpTypes2SBV ins out, UnintMap))
 -> (OpTypes2SBV ins out, UnintMap))
-> (SMTDefinable (OpTypes2SBV ins out) =>
    (OpTypes2SBV ins out, UnintMap))
-> (OpTypes2SBV ins out, UnintMap)
forall a b. (a -> b) -> a -> b
$ let f :: OpTypes2SBV ins out
f = String -> OpTypes2SBV ins out
forall a. SMTDefinable a => String -> a
uninterpret (UnintOp ins out -> String
forall (ins :: [EUFType]) (out :: EUFType).
UnintOp ins out -> String
unintOpName UnintOp ins out
uop)
       in (OpTypes2SBV ins out
f, String -> ResolvedUnintOp -> UnintMap -> UnintMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (UnintOp ins out -> String
forall (ins :: [EUFType]) (out :: EUFType).
UnintOp ins out -> String
unintOpName UnintOp ins out
uop) (UnintOp ins out -> OpTypes2SBV ins out -> ResolvedUnintOp
forall (ins :: [EUFType]) (out :: EUFType).
UnintOp ins out -> OpTypes2SBV ins out -> ResolvedUnintOp
ResolvedUnintOp UnintOp ins out
uop OpTypes2SBV ins out
f) UnintMap
m)

-- | The monad for interpreting t'EUFExpr's into SBV, which is just a state monad
-- over an 'UnintMap'
type InterpM = State UnintMap

-- | Run an 'InterpM' computation starting with the empty 'UnintMap'
runInterpM :: InterpM a -> a
runInterpM :: forall a. InterpM a -> a
runInterpM = (InterpM a -> UnintMap -> a) -> UnintMap -> InterpM a -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip InterpM a -> UnintMap -> a
forall s a. State s a -> s -> a
evalState UnintMap
forall k a. Map k a
Map.empty

-- | Interpret an 'Op' into a function over SBV values
interpOp :: Op ins out -> InterpM (OpTypes2SBV ins out)
interpOp :: forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> InterpM (OpTypes2SBV ins out)
interpOp (Op_Unint UnintOp ins out
uop)                      = (UnintMap -> (OpTypes2SBV ins out, UnintMap))
-> StateT UnintMap Identity (OpTypes2SBV ins out)
forall a. (UnintMap -> (a, UnintMap)) -> StateT UnintMap Identity a
forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
state (UnintOp ins out -> UnintMap -> (OpTypes2SBV ins out, UnintMap)
forall (ins :: [EUFType]) (out :: EUFType).
UnintOp ins out -> UnintMap -> (OpTypes2SBV ins out, UnintMap)
unintEnsure UnintOp ins out
uop)
interpOp Op ins out
Op_And                              = (SBool -> SBool -> SBool)
-> StateT UnintMap Identity (SBool -> SBool -> SBool)
forall a. a -> StateT UnintMap Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return SBool -> SBool -> SBool
(.&&)
interpOp Op ins out
Op_Or                               = (SBool -> SBool -> SBool)
-> StateT UnintMap Identity (SBool -> SBool -> SBool)
forall a. a -> StateT UnintMap Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return SBool -> SBool -> SBool
(.||)
interpOp Op ins out
Op_Not                              = (SBool -> SBool) -> StateT UnintMap Identity (SBool -> SBool)
forall a. a -> StateT UnintMap Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return SBool -> SBool
sNot
interpOp (Op_BoolLit    Bool
b)                   = SBool -> StateT UnintMap Identity SBool
forall a. a -> StateT UnintMap Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> StateT UnintMap Identity SBool)
-> SBool -> StateT UnintMap Identity SBool
forall a b. (a -> b) -> a -> b
$ Bool -> SBool
fromBool Bool
b
interpOp (Op_IfThenElse TypeRepr out
Repr_Bool)           = (SBool -> SBool -> SBool -> SBool)
-> StateT UnintMap Identity (SBool -> SBool -> SBool -> SBool)
forall a. a -> StateT UnintMap Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite
interpOp (Op_IfThenElse (Repr_BV BVWidth{})) = (SBool -> SBV (WordN w) -> SBV (WordN w) -> SBV (WordN w))
-> StateT
     UnintMap
     Identity
     (SBool -> SBV (WordN w) -> SBV (WordN w) -> SBV (WordN w))
forall a. a -> StateT UnintMap Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return SBool -> SBV (WordN w) -> SBV (WordN w) -> SBV (WordN w)
forall a. Mergeable a => SBool -> a -> a -> a
ite
interpOp (Op_Plus       BVWidth{})           = (SBV (WordN w) -> SBV (WordN w) -> SBV (WordN w))
-> StateT
     UnintMap Identity (SBV (WordN w) -> SBV (WordN w) -> SBV (WordN w))
forall a. a -> StateT UnintMap Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return SBV (WordN w) -> SBV (WordN w) -> SBV (WordN w)
forall a. Num a => a -> a -> a
(+)
interpOp (Op_Minus      BVWidth{})           = (SBV (WordN w) -> SBV (WordN w) -> SBV (WordN w))
-> StateT
     UnintMap Identity (SBV (WordN w) -> SBV (WordN w) -> SBV (WordN w))
forall a. a -> StateT UnintMap Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (-)
interpOp (Op_Times      BVWidth{})           = (SBV (WordN w) -> SBV (WordN w) -> SBV (WordN w))
-> StateT
     UnintMap Identity (SBV (WordN w) -> SBV (WordN w) -> SBV (WordN w))
forall a. a -> StateT UnintMap Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return SBV (WordN w) -> SBV (WordN w) -> SBV (WordN w)
forall a. Num a => a -> a -> a
(*)
interpOp (Op_Abs        BVWidth{})           = (SBV (WordN w) -> SBV (WordN w))
-> StateT UnintMap Identity (SBV (WordN w) -> SBV (WordN w))
forall a. a -> StateT UnintMap Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return SBV (WordN w) -> SBV (WordN w)
forall a. Num a => a -> a
abs
interpOp (Op_Signum     BVWidth{})           = (SBV (WordN w) -> SBV (WordN w))
-> StateT UnintMap Identity (SBV (WordN w) -> SBV (WordN w))
forall a. a -> StateT UnintMap Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return SBV (WordN w) -> SBV (WordN w)
forall a. Num a => a -> a
signum
interpOp (Op_BVLit      BVWidth{} Integer
i)         = OpTypes2SBV ins out
-> StateT UnintMap Identity (OpTypes2SBV ins out)
forall a. a -> StateT UnintMap Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (OpTypes2SBV ins out
 -> StateT UnintMap Identity (OpTypes2SBV ins out))
-> OpTypes2SBV ins out
-> StateT UnintMap Identity (OpTypes2SBV ins out)
forall a b. (a -> b) -> a -> b
$ Integer -> SBV (WordN w)
forall a. Num a => Integer -> a
fromInteger Integer
i
interpOp (Op_BVEq       BVWidth{})           = (SBV (WordN w) -> SBV (WordN w) -> SBool)
-> StateT
     UnintMap Identity (SBV (WordN w) -> SBV (WordN w) -> SBool)
forall a. a -> StateT UnintMap Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return SBV (WordN w) -> SBV (WordN w) -> SBool
forall a. EqSymbolic a => a -> a -> SBool
(.==)
interpOp (Op_BVLt       BVWidth{})           = (SBV (WordN w) -> SBV (WordN w) -> SBool)
-> StateT
     UnintMap Identity (SBV (WordN w) -> SBV (WordN w) -> SBool)
forall a. a -> StateT UnintMap Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return SBV (WordN w) -> SBV (WordN w) -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
(.<)

-- | Interpret an t'EUFExpr' into an SBV value.
interpEUFExpr :: EUFExpr tp -> InterpM (Type2SBV tp)
interpEUFExpr :: forall (tp :: EUFType). EUFExpr tp -> InterpM (Type2SBV tp)
interpEUFExpr (EUFExpr Op ins tp
op EUFExprs ins
args) = do OpTypes2SBV ins tp
f <- Op ins tp -> StateT UnintMap Identity (OpTypes2SBV ins tp)
forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> InterpM (OpTypes2SBV ins out)
interpOp Op ins tp
op
                                     Op ins tp
-> OpTypes2SBV ins tp -> EUFExprs ins -> InterpM (Type2SBV tp)
forall (ghost :: EUFType -> *) (out :: EUFType) (ins :: [EUFType]).
ghost out
-> OpTypes2SBV ins out -> EUFExprs ins -> InterpM (Type2SBV out)
interpApplyEUFExprs Op ins tp
op OpTypes2SBV ins tp
f EUFExprs ins
args

-- | Apply an interpretation of an operator to the interpretations of a sequence of arguments for it.
interpApplyEUFExprs :: ghost out -> OpTypes2SBV ins out -> EUFExprs ins -> InterpM (Type2SBV out)
interpApplyEUFExprs :: forall (ghost :: EUFType -> *) (out :: EUFType) (ins :: [EUFType]).
ghost out
-> OpTypes2SBV ins out -> EUFExprs ins -> InterpM (Type2SBV out)
interpApplyEUFExprs ghost out
_   OpTypes2SBV ins out
f EUFExprs ins
EUFExprsNil         = Type2SBV out -> StateT UnintMap Identity (Type2SBV out)
forall a. a -> StateT UnintMap Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return OpTypes2SBV ins out
Type2SBV out
f
interpApplyEUFExprs ghost out
out OpTypes2SBV ins out
f (EUFExprsCons EUFExpr tp
e EUFExprs tps
es) = do OpTypes2SBV tps out
f_app <- OpTypes2SBV ins out
Type2SBV tp -> OpTypes2SBV tps out
f (Type2SBV tp -> OpTypes2SBV tps out)
-> StateT UnintMap Identity (Type2SBV tp)
-> StateT UnintMap Identity (OpTypes2SBV tps out)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> EUFExpr tp -> StateT UnintMap Identity (Type2SBV tp)
forall (tp :: EUFType). EUFExpr tp -> InterpM (Type2SBV tp)
interpEUFExpr EUFExpr tp
e
                                                   ghost out
-> OpTypes2SBV tps out
-> EUFExprs tps
-> StateT UnintMap Identity (Type2SBV out)
forall (ghost :: EUFType -> *) (out :: EUFType) (ins :: [EUFType]).
ghost out
-> OpTypes2SBV ins out -> EUFExprs ins -> InterpM (Type2SBV out)
interpApplyEUFExprs ghost out
out OpTypes2SBV tps out
f_app EUFExprs tps
es

-- | Top-level call to interpret an t'EUFExpr' to an 'SBV' value
interpEUF :: EUFExpr a -> Type2SBV a
interpEUF :: forall (a :: EUFType). EUFExpr a -> Type2SBV a
interpEUF = InterpM (Type2SBV a) -> Type2SBV a
forall a. InterpM a -> a
runInterpM (InterpM (Type2SBV a) -> Type2SBV a)
-> (EUFExpr a -> InterpM (Type2SBV a)) -> EUFExpr a -> Type2SBV a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EUFExpr a -> InterpM (Type2SBV a)
forall (tp :: EUFType). EUFExpr tp -> InterpM (Type2SBV tp)
interpEUFExpr

----------------------------------------------------------------------
-- * Examples
----------------------------------------------------------------------

-- | Example EUF problem
--
-- > f (f (a) - f (b)) /= f (c), b >= a, a >= b + c, c >= 0
--
-- from <https://goto.ucsd.edu/~rjhala/classes/sp13/cse291/slides/lec-smt.markdown.pdf>
-- noting that @x >= y@ is the same as @not (x < y)@. We have:
--
-- >>> sat $ interpEUF example
-- Satisfiable. Model:
--   a =  996506182 :: Word32
--   b = 3298461113 :: Word32
--   c = 1445036292 :: Word32
-- <BLANKLINE>
--   f :: Word32 -> Word32
--   f 0          = 4188219399
--   f 1445036292 = 285239361
--   f 3298461113 = 4054018119
--   f 996506182  = 4054018119
--   f _          = 0
--
--  Note that the original example is unsatisfiable over integers. It is however satisfiable
--  over 32-bit words, hence the model above.
example :: EUFExpr Tp_Bool
example :: EUFExpr 'Tp_Bool
example =
  Op '[ 'Tp_Bool, 'Tp_Bool] 'Tp_Bool
-> EUFExprFun '[ 'Tp_Bool, 'Tp_Bool] 'Tp_Bool
forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> EUFExprFun ins out
applyOp Op '[ 'Tp_Bool, 'Tp_Bool] 'Tp_Bool
Op_And (Op '[ 'Tp_Bool] 'Tp_Bool -> EUFExprFun '[ 'Tp_Bool] 'Tp_Bool
forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> EUFExprFun ins out
applyOp Op '[ 'Tp_Bool] 'Tp_Bool
Op_Not (Op '[ 'Tp_BV 32, 'Tp_BV 32] 'Tp_Bool
-> EUFExprFun '[ 'Tp_BV 32, 'Tp_BV 32] 'Tp_Bool
forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> EUFExprFun ins out
applyOp (BVWidth 32 -> Op '[ 'Tp_BV 32, 'Tp_BV 32] 'Tp_Bool
forall (w :: Nat). BVWidth w -> Op '[ 'Tp_BV w, 'Tp_BV w] 'Tp_Bool
Op_BVEq BVWidth 32
forall (w :: Nat). (KnownNat w, BVIsNonZero w) => BVWidth w
knownBVWidth)
                                          (Op '[ 'Tp_BV 32] ('Tp_BV 32)
-> EUFExprFun '[ 'Tp_BV 32] ('Tp_BV 32)
forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> EUFExprFun ins out
applyOp Op '[ 'Tp_BV 32] ('Tp_BV 32)
f (Op '[ 'Tp_BV 32] ('Tp_BV 32)
-> EUFExprFun '[ 'Tp_BV 32] ('Tp_BV 32)
forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> EUFExprFun ins out
applyOp Op '[ 'Tp_BV 32] ('Tp_BV 32)
f EUFExpr ('Tp_BV 32)
a EUFExpr ('Tp_BV 32) -> EUFExpr ('Tp_BV 32) -> EUFExpr ('Tp_BV 32)
forall a. Num a => a -> a -> a
- Op '[ 'Tp_BV 32] ('Tp_BV 32)
-> EUFExprFun '[ 'Tp_BV 32] ('Tp_BV 32)
forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> EUFExprFun ins out
applyOp Op '[ 'Tp_BV 32] ('Tp_BV 32)
f EUFExpr ('Tp_BV 32)
b))
                                          (Op '[ 'Tp_BV 32] ('Tp_BV 32)
-> EUFExprFun '[ 'Tp_BV 32] ('Tp_BV 32)
forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> EUFExprFun ins out
applyOp Op '[ 'Tp_BV 32] ('Tp_BV 32)
f EUFExpr ('Tp_BV 32)
c)))
                 (Op '[ 'Tp_Bool, 'Tp_Bool] 'Tp_Bool
-> EUFExprFun '[ 'Tp_Bool, 'Tp_Bool] 'Tp_Bool
forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> EUFExprFun ins out
applyOp Op '[ 'Tp_Bool, 'Tp_Bool] 'Tp_Bool
Op_And (Op '[ 'Tp_Bool] 'Tp_Bool -> EUFExprFun '[ 'Tp_Bool] 'Tp_Bool
forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> EUFExprFun ins out
applyOp Op '[ 'Tp_Bool] 'Tp_Bool
Op_Not (Op '[ 'Tp_BV 32, 'Tp_BV 32] 'Tp_Bool
-> EUFExprFun '[ 'Tp_BV 32, 'Tp_BV 32] 'Tp_Bool
forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> EUFExprFun ins out
applyOp (BVWidth 32 -> Op '[ 'Tp_BV 32, 'Tp_BV 32] 'Tp_Bool
forall (w :: Nat). BVWidth w -> Op '[ 'Tp_BV w, 'Tp_BV w] 'Tp_Bool
Op_BVLt BVWidth 32
forall (w :: Nat). (KnownNat w, BVIsNonZero w) => BVWidth w
knownBVWidth) EUFExpr ('Tp_BV 32)
b EUFExpr ('Tp_BV 32)
a))
                                 (Op '[ 'Tp_Bool, 'Tp_Bool] 'Tp_Bool
-> EUFExprFun '[ 'Tp_Bool, 'Tp_Bool] 'Tp_Bool
forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> EUFExprFun ins out
applyOp Op '[ 'Tp_Bool, 'Tp_Bool] 'Tp_Bool
Op_And
                                          (Op '[ 'Tp_Bool] 'Tp_Bool -> EUFExprFun '[ 'Tp_Bool] 'Tp_Bool
forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> EUFExprFun ins out
applyOp Op '[ 'Tp_Bool] 'Tp_Bool
Op_Not (Op '[ 'Tp_BV 32, 'Tp_BV 32] 'Tp_Bool
-> EUFExprFun '[ 'Tp_BV 32, 'Tp_BV 32] 'Tp_Bool
forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> EUFExprFun ins out
applyOp (BVWidth 32 -> Op '[ 'Tp_BV 32, 'Tp_BV 32] 'Tp_Bool
forall (w :: Nat). BVWidth w -> Op '[ 'Tp_BV w, 'Tp_BV w] 'Tp_Bool
Op_BVLt BVWidth 32
forall (w :: Nat). (KnownNat w, BVIsNonZero w) => BVWidth w
knownBVWidth) EUFExpr ('Tp_BV 32)
a (EUFExpr ('Tp_BV 32)
b EUFExpr ('Tp_BV 32) -> EUFExpr ('Tp_BV 32) -> EUFExpr ('Tp_BV 32)
forall a. Num a => a -> a -> a
+ EUFExpr ('Tp_BV 32)
c)))
                                          (Op '[ 'Tp_Bool] 'Tp_Bool -> EUFExprFun '[ 'Tp_Bool] 'Tp_Bool
forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> EUFExprFun ins out
applyOp Op '[ 'Tp_Bool] 'Tp_Bool
Op_Not (Op '[ 'Tp_BV 32, 'Tp_BV 32] 'Tp_Bool
-> EUFExprFun '[ 'Tp_BV 32, 'Tp_BV 32] 'Tp_Bool
forall (ins :: [EUFType]) (out :: EUFType).
Op ins out -> EUFExprFun ins out
applyOp (BVWidth 32 -> Op '[ 'Tp_BV 32, 'Tp_BV 32] 'Tp_Bool
forall (w :: Nat). BVWidth w -> Op '[ 'Tp_BV w, 'Tp_BV w] 'Tp_Bool
Op_BVLt BVWidth 32
forall (w :: Nat). (KnownNat w, BVIsNonZero w) => BVWidth w
knownBVWidth) EUFExpr ('Tp_BV 32)
c EUFExpr ('Tp_BV 32)
0))))
  where
    f :: Op '[Tp_BV 32] (Tp_BV 32)
    f :: Op '[ 'Tp_BV 32] ('Tp_BV 32)
f = String -> Op '[ 'Tp_BV 32] ('Tp_BV 32)
forall (ins :: [EUFType]) (out :: EUFType).
(KnownEUFTypes ins, KnownEUFType out) =>
String -> Op ins out
mkUnintOp String
"f"

    a, b, c :: EUFExpr (Tp_BV 32)
    a :: EUFExpr ('Tp_BV 32)
a = String -> EUFExpr ('Tp_BV 32)
forall (tp :: EUFType). KnownEUFType tp => String -> EUFExpr tp
mkUnintExpr String
"a"
    b :: EUFExpr ('Tp_BV 32)
b = String -> EUFExpr ('Tp_BV 32)
forall (tp :: EUFType). KnownEUFType tp => String -> EUFExpr tp
mkUnintExpr String
"b"
    c :: EUFExpr ('Tp_BV 32)
c = String -> EUFExpr ('Tp_BV 32)
forall (tp :: EUFType). KnownEUFType tp => String -> EUFExpr tp
mkUnintExpr String
"c"

{- HLint ignore "Use camelCase" -}
{- HLint ignore "Eta reduce"    -}