module ToySolver.Converter.PB2SAT (convert) where
import Control.Monad
import Control.Monad.ST
import Data.Array.IArray
import qualified Data.PseudoBoolean as PBFile
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
import qualified ToySolver.SAT.Encoder.PB as PB
import qualified ToySolver.SAT.Encoder.PBNLC as PBNLC
import ToySolver.SAT.Store.CNF
import qualified ToySolver.Text.CNF as CNF
convert :: PBFile.Formula -> (CNF.CNF, SAT.Model -> SAT.Model, SAT.Model -> SAT.Model)
convert formula = runST $ do
db <- newCNFStore
let nv1 = PBFile.pbNumVars formula
SAT.newVars_ db nv1
tseitin <- Tseitin.newEncoder db
pb <- PB.newEncoder tseitin
pbnlc <- PBNLC.newEncoder pb tseitin
forM_ (PBFile.pbConstraints formula) $ \(lhs,op,rhs) -> do
case op of
PBFile.Ge -> SAT.addPBNLAtLeast pbnlc lhs rhs
PBFile.Eq -> SAT.addPBNLExactly pbnlc lhs rhs
cnf <- getCNFFormula db
defs <- Tseitin.getDefinitions tseitin
let extendModel :: SAT.Model -> SAT.Model
extendModel m = array (1, CNF.numVars cnf) (assocs a)
where
a :: Array SAT.Var Bool
a = array (1, CNF.numVars cnf) $
assocs m ++ [(v, Tseitin.evalFormula a phi) | (v, phi) <- defs]
return (cnf, extendModel, SAT.restrictModel nv1)