{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Uninterpreted.Sort where
import Data.SBV
data Q
mkUninterpretedSort ''Q
f :: SQ -> SQ
f :: SQ -> SQ
f = String -> SQ -> SQ
forall a. SMTDefinable a => String -> a
uninterpret String
"f"
t1 :: IO SatResult
t1 :: IO SatResult
t1 = SymbolicT IO SBool -> IO SatResult
forall a. Satisfiable a => a -> IO SatResult
sat (SymbolicT IO SBool -> IO SatResult)
-> SymbolicT IO SBool -> IO SatResult
forall a b. (a -> b) -> a -> b
$ do SQ
x <- String -> Symbolic SQ
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"x"
SBool -> SymbolicT IO SBool
forall a. a -> SymbolicT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ SQ -> SQ
f SQ
x SQ -> SQ -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SQ
x
t2 :: IO SatResult
t2 :: IO SatResult
t2 = SymbolicT IO SBool -> IO SatResult
forall a. Satisfiable a => a -> IO SatResult
sat (SymbolicT IO SBool -> IO SatResult)
-> SymbolicT IO SBool -> IO SatResult
forall a b. (a -> b) -> a -> b
$ do SQ
x <- String -> Symbolic SQ
forall a. SymVal a => String -> Symbolic (SBV a)
free String
"x"
(Forall Any Q -> Forall Any Q -> SBool) -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain ((Forall Any Q -> Forall Any Q -> SBool) -> SymbolicT IO ())
-> (Forall Any Q -> Forall Any Q -> SBool) -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ \(Forall SQ
a) (Forall SQ
b) -> SQ
a SQ -> SQ -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== (SQ
b :: SQ)
SBool -> SymbolicT IO SBool
forall a. a -> SymbolicT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> SymbolicT IO SBool) -> SBool -> SymbolicT IO SBool
forall a b. (a -> b) -> a -> b
$ SQ -> SQ
f SQ
x SQ -> SQ -> SBool
forall a. EqSymbolic a => a -> a -> SBool
./= SQ
x