module Satchmo.Internal 

( SAT
, fresh, emit
, sat
)

where

import Satchmo.Data

import Control.Monad.State.Strict
import Control.Monad.Writer.Strict

data Accu = Accu 
          { next :: ! Int
          , size :: ! Int
          }

start :: Accu
start = Accu 
      { next = 1
      , size = 0
      }

type SAT a = WriterT [ Clause ] (State Accu) a

sat :: SAT a -> ( String, a )
sat m = 
    let ~( ~(a,w), accu) = runState ( runWriterT m ) start
    in  ( unlines $ unwords [ "p", "cnf", show ( next accu - 1), show ( size accu ) ]
                    : map show w
        , a
        )
    
fresh :: SAT Literal
fresh = do
    a <- get
    put $ a { next = next a + 1 }
    return $ literal $ next a

emit :: Clause -> SAT ()
emit clause = do
    a <- get
    tell [ clause ]
    put $ a 
        { size = size a + 1 
        }