module Satchmo.Internal
( SAT
, fresh, fresh_forall
, emit
, sat
)
where
import Satchmo.Data
import Control.Monad.State.Strict
import Control.Monad.Writer.Strict
data Quantified = Forall [ Int ] | Exists [ Int ]
data Accu = Accu
{ next :: ! Int
, quantified :: [ Quantified ]
, size :: ! Int
}
start :: Accu
start = Accu
{ next = 1
, quantified = []
, 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 ) ]
: do q <- reverse $ interesting $ quantified accu
return $ case q of
Forall xs -> unwords $ "a" : map show ( reverse xs ++ [0] )
Exists xs -> unwords $ "e" : map show ( reverse xs ++ [0] )
++ map show w
, a
)
interesting [ Exists _ ] = []
interesting xs = xs
fresh :: SAT Literal
fresh = do
a <- get
let n = next a
let q = case quantified a of
Exists xs : rest -> Exists (n : xs) : rest
rest -> Exists [n] : rest
put $ a { next = n + 1, quantified = q }
return $ literal n
fresh_forall :: SAT Literal
fresh_forall = do
a <- get
let n = next a
let q = case quantified a of
Forall xs : rest -> Forall (n : xs) : rest
rest -> Forall [n] : rest
put $ a { next = n + 1, quantified = q }
return $ literal n
emit :: Clause -> SAT ()
emit clause = do
a <- get
tell [ clause ]
put $ a
{ size = size a + 1
}