Atom.hs

-- |
-- Atomic predicates
--

module Z3.Base.Atom (Atom(..)) where

import Z3.Base.Class
import Z3.Monad

import qualified Data.Map as M
import qualified Data.Set as S

data Atom 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 -> Atom
    -- | v is in s
    -- XXX: s should be any "term", too strong now
    InSet    :: forall v. (Z3Encoded v, Z3Sorted v) => v -> S.Set v -> Atom
    -- | 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 -> Atom
    LessE    :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Atom
    GreaterE :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Atom
    Less     :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Atom
    Greater  :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Atom

instance Z3Encoded Atom 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