import Ersatz
import Prelude hiding (and, or, not, (&&), (||), any, all)
import Ersatz.Solver
import Ersatz.Solver.Minisat
import Data.List (transpose)
import Control.Monad (replicateM)

main = do
      -- this has got nothing to do with cryptominisat itself,
      -- but kissat (which we want to call) has the same CLI
      -- (different from minisat's, which is frozen) 
  result <- solveWith (cryptominisat5Path "kissat") $ do
    let bits = 2
        dim = 3
        number = Bits <$> replicateM bits exists
        matrix = replicateM dim $ replicateM dim $ number
        monotone m = head (head m) >=? 1 && last (last m) >=? 1
        gt p q = geq p q && last (head p) >? last (head q)
        geq p q = and $ do
          (xs,ys) <- zip p q ; (x,y) <- zip xs ys ; return $ x >=? y
    a <- matrix ; assert $ monotone a
    b <- matrix ; assert $ monotone b
    let 
      a2 = times a a ; b2 = times b b
      a3 = times a2 a; b3 = times b2 b
      lhs = times a2 b2 ; rhs = times b3 a3
      -- lhs = times a b ; rhs = times b a
    assert $ gt lhs rhs
    return [a,b,lhs,rhs]
  case result of
    (Satisfied, Just ms) -> print $ map Vertical ms

times a b =
  flip map a $ \ row ->
  flip map (transpose b) $ \ col ->
  sum $ zipWith (*) row col

-- crude formatting:

newtype Vertical a = Vertical [a]
instance Show a => Show (Vertical a) where
  show (Vertical xs) =
    unlines $ zipWith (<>) ("[ " : repeat " , ") (map show xs)
            <> [ " ]" ]