Tseitin.hs

{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeFamilies #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.Converter.Tseitin
-- Copyright   :  (c) Masahiro Sakai 2018
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  experimental
-- Portability :  non-portable
--
-----------------------------------------------------------------------------
module ToySolver.Converter.Tseitin
  ( TseitinInfo (..)
  ) where

import qualified Data.Aeson as J
import qualified Data.Aeson.Types as J
import Data.Aeson ((.=), (.:))
import Data.Array.IArray
import qualified Data.IntMap.Strict as IntMap
import qualified Data.Map.Lazy as Map
import qualified Data.Text as T
import ToySolver.Converter.Base
import ToySolver.Internal.JSON
import qualified ToySolver.SAT.Formula as SAT
import ToySolver.SAT.Internal.JSON
import qualified ToySolver.SAT.Types as SAT
import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin

data TseitinInfo = TseitinInfo !Int !Int (SAT.VarMap Tseitin.Formula)
  deriving (Show, Read, Eq)

instance Transformer TseitinInfo where
  type Source TseitinInfo = SAT.Model
  type Target TseitinInfo = SAT.Model

instance ForwardTransformer TseitinInfo where
  transformForward (TseitinInfo _nv1 nv2 defs) m = array (1, nv2) (assocs a)
    where
      -- Use BOXED array to tie the knot
      a :: Array SAT.Var Bool
      a = array (1, nv2) $
            assocs m ++ [(v, Tseitin.evalFormula a phi) | (v, phi) <- IntMap.toList defs]

instance BackwardTransformer TseitinInfo where
  transformBackward (TseitinInfo nv1 _nv2 _defs) = SAT.restrictModel nv1

instance J.ToJSON TseitinInfo where
  toJSON (TseitinInfo nv1 nv2 defs) =
    J.object
    [ "type" .= ("TseitinInfo" :: J.Value)
    , "num_original_variables" .= nv1
    , "num_transformed_variables" .= nv2
    , "definitions" .= J.object
        [ jVarName v .= formula
        | (v, formula) <- IntMap.toList defs
        ]
    ]

instance J.FromJSON TseitinInfo where
  parseJSON = withTypedObject "TseitinInfo" $ \obj -> do
    defs <- obj .: "definitions"
    TseitinInfo
      <$> obj .: "num_original_variables"
      <*> obj .: "num_transformed_variables"
      <*> (IntMap.fromList <$> mapM f (Map.toList defs))
    where
      f :: (T.Text, SAT.Formula) -> J.Parser (SAT.Var, SAT.Formula)
      f (name, formula) = do
        x <- parseVarNameText name
        pure (x, formula)

-- -----------------------------------------------------------------------------