content: -- |
  -- Assertions provided by libraries *for convenience*
  -- It is not hard-coded into Z3.Logic.Pred
  --
  
  module Ntha.Z3.Assertion (Assertion(..)) where
  
  import Ntha.Z3.Class
  import Ntha.Z3.Encoding()
  import Z3.Monad
  
  import qualified Data.Map as M
  import qualified Data.Set as S
  
  data Assertion where
      -- | k is mapped to v in (m :: M.Map k v)
      -- XXX: m should be any "term", too strong now
      InMap    :: forall k v. (Z3Sorted k, Z3Encoded k, Z3Sorted v, Z3Reserved v) => k -> v -> M.Map k v -> Assertion
      -- | v is in s
      -- XXX: s should be any "term", too strong now
      InSet    :: forall v. (Z3Encoded v, Z3Sorted v) => v -> S.Set v -> Assertion
      -- | All below are binary relationships
      -- XXX: Should make sure v1 ~ v2, too weak now
      Equal    :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion
      LessE    :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion
      GreaterE :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion
      Less     :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion
      Greater  :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion
  
  instance Z3Encoded Assertion where
      encode (InMap k v m) = do
          kTm <- encode k
          vTm <- encode v
          mTm <- encode m
          lhs <- mkSelect mTm kTm
          mkEq lhs vTm
      encode (InSet e s) = do
          eTm <- encode e
          sTm <- encode s
          lhs <- mkSelect sTm eTm
          -- XXX: magic number
          one <- (mkIntSort >>= mkInt 1)
          mkEq one lhs
      encode (Equal t1 t2) = do
          a1 <- encode t1
          a2 <- encode t2
          mkEq a1 a2
      encode (LessE t1 t2) = do
          a1 <- encode t1
          a2 <- encode t2
          mkLe a1 a2
      encode (GreaterE t1 t2) = do
          a1 <- encode t1
          a2 <- encode t2
          mkGe a1 a2
      encode (Less t1 t2) = do
          a1 <- encode t1
          a2 <- encode t2
          mkLt a1 a2
      encode (Greater t1 t2) = do
          a1 <- encode t1
          a2 <- encode t2
          mkGt a1 a2
  