content: -- | Example of a simple SAT solver (simply constructs the truth table) in
  -- Copilot.
  
  -- {-# LANGUAGE RebindableSyntax #-}
  
  module Sat where
  
  import Language.Copilot
  import qualified Prelude as P
  import Control.Monad (foldM_)
  
  ---------------------------------------------------------------------------------
  
  -- | Number of sat variables and a Boolean function over those variables.
  type SatFunc = (Int, [Stream Bool] -> Stream Bool)
  
  -- Takes a Sat function and returns the stream of variables and a SAT function.
  sat :: SatFunc -> ([Stream Bool], Stream Bool)
  sat (i,f) = (xs, res)
    where
    -- If it becomes true, it stays true.
    res   = [False] ++ (f xs || res)
  
    xs  = xs' i
  
    xs' 0 = []
    xs' n = clk (period $ 2 P.^ n) (phase (0 :: Int)) : xs' (n P.- 1)
  
  satSpec :: SatFunc -> Spec
  satSpec f = do
    observer "sat" (snd $ sat f)
    observer "done" done
    foldM_ mkObs (0 :: Int) xs
  
    where
    xs = fst $ sat f
    cnt :: Stream Word64 -- Would need to be extended depending on number of
                         -- variables.
    cnt = [1] ++ cnt + 1
    done = cnt == (2 P.^ length xs)
    mkObs idx strm = do observer ("obs" P.++ show idx) strm
                        return (idx P.+ 1)
  
  
  f0 :: SatFunc
  --f0 = (3, \[a,b,c] -> a && (b || (not c)))
  f0 = (3, f) 
    where 
    f [a,b,c] = a && (b || (not c))
    f _       = error "Bad SAT function."
  
  f1 :: SatFunc
  f1 = (9, f')
    where
    f' [a,b,c,d,e,f,g,h,i] = 
      a && b && c && d && e && 
        f && g && h && i && i && not i
    f' _ = error "Bad SAT function."
  
  -- | Run the interpreter long enough to get an answer.
  runFunc :: SatFunc -> IO ()
  runFunc f = interpret (2 P.^ fst f) (satSpec f)
  
  satExamples :: IO ()
  satExamples = runFunc f0 >> runFunc f1
  
  ---------------------------------------------------------------------------------
  