{-# OPTIONS_GHC -fdefer-typed-holes #-}

import Ersatz
import Prelude hiding (and, or, not, (&&), (||))
import Ersatz.Relation
import Ersatz.Solver
import Ersatz.Solver.Minisat

main = do
  result <- solveWith minisat $ do
    r <- relation ((1,1),(2,2))
    s <- relation ((1,1),(2,2))

    -- fill in the holes!
    assert $ and [ transitive r
                 , _
                 , _
                 ]
      
    return (r,s)
  case result of
    (Satisfied, Just (r,s)) -> do
      print (r,s)
      putStrLn $ table r
      putStrLn $ table s