{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Uninterpreted.UISortAllSat where
import Data.SBV
data L
mkUninterpretedSort ''L
classify :: SL -> SInteger
classify :: SL -> SInteger
classify = String -> SL -> SInteger
forall a. SMTDefinable a => String -> a
uninterpret String
"classify"
genLs :: Predicate
genLs :: Predicate
genLs = do [SL
l, SL
l0, SL
l1, SL
l2] <- [String] -> Symbolic [SL]
forall a. SymVal a => [String] -> Symbolic [SBV a]
symbolics [String
"l", String
"l0", String
"l1", String
"l2"]
SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SL -> SInteger
classify SL
l0 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
0
SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SL -> SInteger
classify SL
l1 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
1
SBool -> SymbolicT IO ()
forall a. QuantifiedBool a => a -> SymbolicT IO ()
forall (m :: * -> *) a.
(SolverContext m, QuantifiedBool a) =>
a -> m ()
constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
forall a b. (a -> b) -> a -> b
$ SL -> SInteger
classify SL
l2 SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
2
SBool -> Predicate
forall a. a -> SymbolicT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SBool -> Predicate) -> SBool -> Predicate
forall a b. (a -> b) -> a -> b
$ SL
l SL -> SL -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SL
l0 SBool -> SBool -> SBool
.|| SL
l SL -> SL -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SL
l1 SBool -> SBool -> SBool
.|| SL
l SL -> SL -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SL
l2