-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Uninterpreted.Sort
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Demonstrates uninterpreted sorts, together with axioms.
-----------------------------------------------------------------------------

{-# LANGUAGE DeriveAnyClass     #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell    #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Uninterpreted.Sort where

import Data.SBV

-- | A new data-type that we expect to use in an uninterpreted fashion
-- in the backend SMT solver.
data Q

-- | Make 'Q' an uinterpreted sort. This will automatically introduce the
-- type 'SQ' into our environment, which is the symbolic version of the
-- carrier type 'Q'.
mkUninterpretedSort ''Q

-- | Declare an uninterpreted function that works over Q's
f :: SQ -> SQ
f :: SBV Q -> SBV Q
f = String -> SBV Q -> SBV Q
forall a. Uninterpreted a => String -> a
uninterpret String
"f"

-- | A satisfiable example, stating that there is an element of the domain
-- 'Q' such that 'f' returns a different element. Note that this is valid only
-- when the domain 'Q' has at least two elements. We have:
--
-- >>> t1
-- Satisfiable. Model:
--   x = Q!val!0 :: Q
-- <BLANKLINE>
--   f :: Q -> Q
--   f _ = Q!val!1
t1 :: IO SatResult
t1 :: IO SatResult
t1 = SymbolicT IO SBool -> IO SatResult
forall a. Provable a => a -> IO SatResult
sat (SymbolicT IO SBool -> IO SatResult)
-> SymbolicT IO SBool -> IO SatResult
forall a b. (a -> b) -> a -> b
$ do SBV Q
x <- String -> Symbolic (SBV Q)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"x"
              SBool -> SymbolicT IO SBool
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ SBV Q -> SBV Q
f SBV Q
x SBV Q -> SBV Q -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SBV Q
x

-- | This is a variant on the first example, except we also add an axiom
-- for the sort, stating that the domain 'Q' has only one element. In this case
-- the problem naturally becomes unsat. We have:
--
-- >>> t2
-- Unsatisfiable
t2 :: IO SatResult
t2 :: IO SatResult
t2 = SymbolicT IO SBool -> IO SatResult
forall a. Provable a => a -> IO SatResult
sat (SymbolicT IO SBool -> IO SatResult)
-> SymbolicT IO SBool -> IO SatResult
forall a b. (a -> b) -> a -> b
$ do SBV Q
x <- String -> Symbolic (SBV Q)
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"x"
              String -> [String] -> SymbolicT IO ()
forall (m :: * -> *). SolverContext m => String -> [String] -> m ()
addAxiom String
"Q" [String
"(assert (forall ((x Q) (y Q)) (= x y)))"]
              SBool -> SymbolicT IO SBool
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ SBV Q -> SBV Q
f SBV Q
x SBV Q -> SBV Q -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SBV Q
x