content: {-# Language BangPatterns #-}
  {-# OPTIONS_GHC -Wall #-}
  {-# OPTIONS_HADDOCK show-extensions #-}
  ----------------------------------------------------------------------
  -- |
  -- Module      :  ToySolver.SAT.ExistentialQuantification
  -- Copyright   :  (c) Masahiro Sakai 2017
  -- License     :  BSD-style
  --
  -- Maintainer  :  masahiro.sakai@gmail.com
  -- Stability   :  provisional
  -- Portability :  non-portable
  --
  -- References:
  --
  -- * [BrauerKingKriener2011] Jörg Brauer, Andy King, and Jael Kriener,
  --   "Existential quantification as incremental SAT," in Computer Aided
  --   Verification (CAV 2011), G. Gopalakrishnan and S. Qadeer, Eds.
  --   pp. 191-207.
  --   <https://www.cs.kent.ac.uk/pubs/2011/3094/content.pdf>
  --
  ----------------------------------------------------------------------
  module ToySolver.SAT.ExistentialQuantification
    ( project
    , shortestImplicantsE
    , negateCNF
    ) where
  
  import Control.Monad
  import qualified Data.IntMap as IntMap
  import qualified Data.IntSet as IntSet
  import Data.IORef
  import qualified Data.Vector.Generic as VG
  import ToySolver.FileFormat.CNF as CNF
  import ToySolver.SAT as SAT
  import ToySolver.SAT.Types as SAT
  
  -- -------------------------------------------------------------------
  
  data Info
    = Info
    { forwardMap :: SAT.VarMap (SAT.Var, SAT.Var)
    , backwardMap :: SAT.VarMap SAT.Lit
    }
  
  -- | Given a set of variables \(X = \{x_1, \ldots, x_k\}\) and CNF formula \(\phi\), this function
  --
  -- * duplicates \(X\) with \(X^+ = \{x^+_1,\ldots,x^+_k\}\) and \(X^- = \{x^-_1,\ldots,x^-_k\}\),
  --
  -- * replaces positive literals \(x_i\) with \(x^+_i\), and negative literals \(\neg x_i\) with \(x^-_i\), and
  --
  -- * adds constraints \(\neg x^+_i \vee \neg x^-_i\).
  dualRailEncoding
    :: SAT.VarSet -- ^ \(X\)
    -> CNF.CNF    -- ^ \(\phi\)
    -> (CNF.CNF, Info)
  dualRailEncoding vs cnf =
    ( cnf'
    , Info
      { forwardMap = forward
      , backwardMap = backward
      }
    )
    where
      cnf' =
        CNF.CNF
        { CNF.cnfNumVars = CNF.cnfNumVars cnf + IntSet.size vs
        , CNF.cnfNumClauses = CNF.cnfNumClauses cnf + IntSet.size vs
        , CNF.cnfClauses =
            [ VG.map f c | c <- CNF.cnfClauses cnf ] ++
            [ SAT.packClause [-xp,-xn] | (xp,xn) <- IntMap.elems forward ]
        }
      f x =
        case IntMap.lookup (abs (SAT.unpackLit x)) forward of
          Nothing -> x
          Just (xp,xn) -> SAT.packLit $ if x > 0 then xp else xn
      forward =
        IntMap.fromList
        [ (x, (x,x'))
        | (x,x') <- zip (IntSet.toList vs) [CNF.cnfNumVars cnf + 1 ..]
        ]
      backward = IntMap.fromList $ concat $
        [ [(xp,x), (xn,-x)]
        | (x, (xp,xn)) <- IntMap.toList forward
        ]
  
  {-
  forwardLit :: Info -> Lit -> Lit
  forwardLit info l =
    case IntMap.lookup (abs l) (forwardMap info) of
      Nothing -> l
      Just (xp,xn) -> if l > 0 then xp else xn
  -}
  
  -- -------------------------------------------------------------------
  
  cube :: Info -> SAT.Model -> LitSet
  cube info m = IntSet.fromList $ concat $
    [ if SAT.evalLit m xp then [x]
      else if SAT.evalLit m xn then [-x]
      else []
    | (x, (xp,xn)) <- IntMap.toList (forwardMap info)
    ]
  
  blockingClause :: Info -> SAT.Model -> Clause
  blockingClause info m = [-y | y <- IntMap.keys (backwardMap info), SAT.evalLit m y]
  
  -- | Given a set of variables \(X = \{x_1, \ldots, x_k\}\) and CNF formula \(\phi\),
  -- this function computes shortest implicants of \(\exists X. \phi\).
  --
  -- Resulting shortest implicants form a DNF (disjunctive normal form) formula that is
  -- equivalent to the original formula \(\exists X. \phi\).
  shortestImplicantsE
    :: SAT.VarSet  -- ^ \(X\)
    -> CNF.CNF     -- ^ \(\phi\)
    -> IO [LitSet]
  shortestImplicantsE xs formula = do
    let (tau_formula, info) = dualRailEncoding (IntSet.fromList [1 .. CNF.cnfNumVars formula] IntSet.\\ xs) formula
    solver <- SAT.newSolver
    SAT.newVars_ solver (CNF.cnfNumVars tau_formula)
    forM_ (CNF.cnfClauses tau_formula) $ \c -> do
      SAT.addClause solver (SAT.unpackClause c)
  
    ref <- newIORef []
  
    let lim = IntMap.size (forwardMap info)
  
        loop !n | n > lim = return ()
        loop !n = do
          sel <- SAT.newVar solver
          SAT.addPBAtMostSoft solver sel [(1,l) | l <- IntMap.keys (backwardMap info)] (fromIntegral n)
          let loop2 = do
                b <- SAT.solveWith solver [sel]
                when b $ do
                  m <- SAT.getModel solver
                  let c = cube info m
                  modifyIORef ref (c:)
                  SAT.addClause solver (blockingClause info m)
                  loop2
          loop2
          SAT.addClause solver [-sel]
          loop (n+1)
  
    loop 0
    reverse <$> readIORef ref
  
  -- | Given a CNF formula \(\phi\), this function returns another CNF formula \(\psi\)
  -- that is equivalent to \(\neg\phi\).
  negateCNF
    :: CNF.CNF    -- ^ \(\phi\)
    -> IO CNF.CNF -- ^ \(\psi \equiv \neg\phi\)
  negateCNF formula = do
    implicants <- shortestImplicantsE IntSet.empty formula
    return $
      CNF.CNF
      { CNF.cnfNumVars = CNF.cnfNumVars formula
      , CNF.cnfNumClauses = length implicants
      , CNF.cnfClauses = map (SAT.packClause . map negate . IntSet.toList) implicants
      }
  
  -- | Given a set of variables \(X = \{x_1, \ldots, x_k\}\) and CNF formula \(\phi\),
  -- this function computes a CNF formula \(\psi\) that is equivalent to \(\exists X. \phi\)
  -- (i.e. \((\exists X. \phi) \leftrightarrow \psi\)).
  project
    :: SAT.VarSet  -- ^ \(X\)
    -> CNF.CNF     -- ^ \(\phi\)
    -> IO CNF.CNF  -- ^ \(\psi\)
  project xs cnf = do
    let ys = IntSet.fromList [1 .. CNF.cnfNumVars cnf] IntSet.\\ xs
        nv = if IntSet.null ys then 0 else IntSet.findMax ys
    implicants <- shortestImplicantsE xs cnf
    let cnf' =
          CNF.CNF
          { CNF.cnfNumVars = nv
          , CNF.cnfNumClauses = length implicants
          , CNF.cnfClauses = map (SAT.packClause . map negate . IntSet.toList) implicants
          }
    negated_implicates <- shortestImplicantsE xs cnf'
    let implicates = map (SAT.packClause . map negate . IntSet.toList) negated_implicates
    return $
      CNF.CNF
      { CNF.cnfNumVars = nv
      , CNF.cnfNumClauses = length implicates
      , CNF.cnfClauses = implicates
      }
  