import Prelude hiding (and,or,all,any,not,(&&),(||))
import Ersatz
import qualified Ersatz.Counting as C

import qualified Ersatz.Bit.Display as D
import Control.Monad (replicateM)
import qualified Data.Text.IO as T

-- | print dot expression to stdout
main :: IO ()
main = T.putStrLn $ D.toDot $ fst $ runSAT' mkBit

-- | render and display.
-- will open a window and block ghci,
-- hit 'q' in window to close window and unblock ghci.
run :: IO ()
run = D.display mkBit

mkBit :: MonadSAT s m => m Bit
mkBit = do
  xs <- replicateM 4 (exists @Bit)
  return $ C.exactly 1 xs