{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  ToySolver.SAT.Encoder.Tseitin
-- Copyright   :  (c) Masahiro Sakai 2012
-- License     :  BSD-style
--
-- Maintainer  :  masahiro.sakai@gmail.com
-- Stability   :  provisional
-- Portability :  non-portable
--
-- Tseitin encoding
--
-- TODO:
--
-- * reduce variables.
--
-- References:
--
-- * [Tse83] G. Tseitin. On the complexity of derivation in propositional
--   calculus. Automation of Reasoning: Classical Papers in Computational
--   Logic, 2:466-483, 1983. Springer-Verlag.
--
-- * [For60] R. Fortet. Application de l'algèbre de Boole en rechercheop
--   opérationelle. Revue Française de Recherche Opérationelle, 4:17-26,
--   1960.
--
-- * [BM84a] E. Balas and J. B. Mazzola. Nonlinear 0-1 programming:
--   I. Linearization techniques. Mathematical Programming, 30(1):1-21,
--   1984.
--
-- * [BM84b] E. Balas and J. B. Mazzola. Nonlinear 0-1 programming:
--   II. Dominance relations and algorithms. Mathematical Programming,
--   30(1):22-45, 1984.
--
-- * [PG86] D. Plaisted and S. Greenbaum. A Structure-preserving
--    Clause Form Translation. In Journal on Symbolic Computation,
--    volume 2, 1986.
--
-- * [ES06] N. Eén and N. Sörensson. Translating Pseudo-Boolean
--   Constraints into SAT. JSAT 2:1–26, 2006.
--
-----------------------------------------------------------------------------
module ToySolver.SAT.Encoder.Tseitin
  (
  -- * The @Encoder@ type
    Encoder
  , newEncoder
  , newEncoderWithPBLin
  , setUsePB

  -- * Polarity
  , Polarity (..)
  , negatePolarity
  , polarityPos
  , polarityNeg
  , polarityBoth
  , polarityNone

  -- * Boolean formula type
  , module ToySolver.SAT.Formula

  -- * Encoding of boolean formulas
  , addFormula
  , encodeFormula
  , encodeFormulaWithPolarity
  , encodeConj
  , encodeConjWithPolarity
  , encodeDisj
  , encodeDisjWithPolarity
  , encodeITE
  , encodeITEWithPolarity
  , encodeXOR
  , encodeXORWithPolarity
  , encodeFASum
  , encodeFASumWithPolarity
  , encodeFACarry
  , encodeFACarryWithPolarity

  -- * Retrieving definitions
  , getDefinitions
  ) where

import Control.Monad
import Control.Monad.Primitive
import Data.Primitive.MutVar
import qualified Data.IntMap.Lazy as IntMap
import Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.IntSet as IntSet
import ToySolver.Data.Boolean
import ToySolver.SAT.Formula
import qualified ToySolver.SAT.Types as SAT

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

-- | Encoder instance
data Encoder m =
  forall a. SAT.AddClause m a =>
  Encoder
  { ()
encBase :: a
  , forall (m :: * -> *).
Encoder m -> Maybe (PBLinSum -> Integer -> m ())
encAddPBAtLeast :: Maybe (SAT.PBLinSum -> Integer -> m ())
  , forall (m :: * -> *). Encoder m -> MutVar (PrimState m) Bool
encUsePB     :: !(MutVar (PrimState m) Bool)
  , forall (m :: * -> *).
Encoder m -> MutVar (PrimState m) (Map LitSet (Var, Bool, Bool))
encConjTable :: !(MutVar (PrimState m) (Map SAT.LitSet (SAT.Var, Bool, Bool)))
  , forall (m :: * -> *).
Encoder m
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
encITETable  :: !(MutVar (PrimState m) (Map (SAT.Lit, SAT.Lit, SAT.Lit) (SAT.Var, Bool, Bool)))
  , forall (m :: * -> *).
Encoder m
-> MutVar (PrimState m) (Map (Var, Var) (Var, Bool, Bool))
encXORTable  :: !(MutVar (PrimState m) (Map (SAT.Lit, SAT.Lit) (SAT.Var, Bool, Bool)))
  , forall (m :: * -> *).
Encoder m
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
encFASumTable   :: !(MutVar (PrimState m) (Map (SAT.Lit, SAT.Lit, SAT.Lit) (SAT.Var, Bool, Bool)))
  , forall (m :: * -> *).
Encoder m
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
encFACarryTable :: !(MutVar (PrimState m) (Map (SAT.Lit, SAT.Lit, SAT.Lit) (SAT.Var, Bool, Bool)))
  }

instance Monad m => SAT.NewVar m (Encoder m) where
  newVar :: Encoder m -> m Var
newVar   Encoder{ encBase :: ()
encBase = a
a } = a -> m Var
forall (m :: * -> *) a. NewVar m a => a -> m Var
SAT.newVar a
a
  newVars :: Encoder m -> Var -> m [Var]
newVars  Encoder{ encBase :: ()
encBase = a
a } = a -> Var -> m [Var]
forall (m :: * -> *) a. NewVar m a => a -> Var -> m [Var]
SAT.newVars a
a
  newVars_ :: Encoder m -> Var -> m ()
newVars_ Encoder{ encBase :: ()
encBase = a
a } = a -> Var -> m ()
forall (m :: * -> *) a. NewVar m a => a -> Var -> m ()
SAT.newVars_ a
a

instance Monad m => SAT.AddClause m (Encoder m) where
  addClause :: Encoder m -> [Var] -> m ()
addClause Encoder{ encBase :: ()
encBase = a
a } = a -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause a
a

-- | Create a @Encoder@ instance.
-- If the encoder is built using this function, 'setUsePB' has no effect.
newEncoder :: PrimMonad m => SAT.AddClause m a => a -> m (Encoder m)
newEncoder :: forall (m :: * -> *) a.
(PrimMonad m, AddClause m a) =>
a -> m (Encoder m)
newEncoder a
solver = do
  MutVar (PrimState m) Bool
usePBRef <- Bool -> m (MutVar (PrimState m) Bool)
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Bool
False
  MutVar (PrimState m) (Map LitSet (Var, Bool, Bool))
tableConj <- Map LitSet (Var, Bool, Bool)
-> m (MutVar (PrimState m) (Map LitSet (Var, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map LitSet (Var, Bool, Bool)
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
tableITE <- Map (Var, Var, Var) (Var, Bool, Bool)
-> m (MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Var, Var, Var) (Var, Bool, Bool)
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Var, Var) (Var, Bool, Bool))
tableXOR <- Map (Var, Var) (Var, Bool, Bool)
-> m (MutVar (PrimState m) (Map (Var, Var) (Var, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Var, Var) (Var, Bool, Bool)
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
tableFASum <- Map (Var, Var, Var) (Var, Bool, Bool)
-> m (MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Var, Var, Var) (Var, Bool, Bool)
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
tableFACarry <- Map (Var, Var, Var) (Var, Bool, Bool)
-> m (MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Var, Var, Var) (Var, Bool, Bool)
forall k a. Map k a
Map.empty
  Encoder m -> m (Encoder m)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Encoder m -> m (Encoder m)) -> Encoder m -> m (Encoder m)
forall a b. (a -> b) -> a -> b
$
    Encoder
    { encBase :: a
encBase = a
solver
    , encAddPBAtLeast :: Maybe (PBLinSum -> Integer -> m ())
encAddPBAtLeast = Maybe (PBLinSum -> Integer -> m ())
forall a. Maybe a
Nothing
    , encUsePB :: MutVar (PrimState m) Bool
encUsePB  = MutVar (PrimState m) Bool
usePBRef
    , encConjTable :: MutVar (PrimState m) (Map LitSet (Var, Bool, Bool))
encConjTable = MutVar (PrimState m) (Map LitSet (Var, Bool, Bool))
tableConj
    , encITETable :: MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
encITETable = MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
tableITE
    , encXORTable :: MutVar (PrimState m) (Map (Var, Var) (Var, Bool, Bool))
encXORTable = MutVar (PrimState m) (Map (Var, Var) (Var, Bool, Bool))
tableXOR
    , encFASumTable :: MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
encFASumTable = MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
tableFASum
    , encFACarryTable :: MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
encFACarryTable = MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
tableFACarry
    }

-- | Create a @Encoder@ instance.
-- If the encoder is built using this function, 'setUsePB' has an effect.
newEncoderWithPBLin :: PrimMonad m => SAT.AddPBLin m a => a -> m (Encoder m)
newEncoderWithPBLin :: forall (m :: * -> *) a.
(PrimMonad m, AddPBLin m a) =>
a -> m (Encoder m)
newEncoderWithPBLin a
solver = do
  MutVar (PrimState m) Bool
usePBRef <- Bool -> m (MutVar (PrimState m) Bool)
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Bool
False
  MutVar (PrimState m) (Map LitSet (Var, Bool, Bool))
tableConj <- Map LitSet (Var, Bool, Bool)
-> m (MutVar (PrimState m) (Map LitSet (Var, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map LitSet (Var, Bool, Bool)
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
tableITE <- Map (Var, Var, Var) (Var, Bool, Bool)
-> m (MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Var, Var, Var) (Var, Bool, Bool)
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Var, Var) (Var, Bool, Bool))
tableXOR <- Map (Var, Var) (Var, Bool, Bool)
-> m (MutVar (PrimState m) (Map (Var, Var) (Var, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Var, Var) (Var, Bool, Bool)
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
tableFASum <- Map (Var, Var, Var) (Var, Bool, Bool)
-> m (MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Var, Var, Var) (Var, Bool, Bool)
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
tableFACarry <- Map (Var, Var, Var) (Var, Bool, Bool)
-> m (MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Var, Var, Var) (Var, Bool, Bool)
forall k a. Map k a
Map.empty
  Encoder m -> m (Encoder m)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Encoder m -> m (Encoder m)) -> Encoder m -> m (Encoder m)
forall a b. (a -> b) -> a -> b
$
    Encoder
    { encBase :: a
encBase = a
solver
    , encAddPBAtLeast :: Maybe (PBLinSum -> Integer -> m ())
encAddPBAtLeast = (PBLinSum -> Integer -> m ())
-> Maybe (PBLinSum -> Integer -> m ())
forall a. a -> Maybe a
Just (a -> PBLinSum -> Integer -> m ()
forall (m :: * -> *) a.
AddPBLin m a =>
a -> PBLinSum -> Integer -> m ()
SAT.addPBAtLeast a
solver)
    , encUsePB :: MutVar (PrimState m) Bool
encUsePB  = MutVar (PrimState m) Bool
usePBRef
    , encConjTable :: MutVar (PrimState m) (Map LitSet (Var, Bool, Bool))
encConjTable = MutVar (PrimState m) (Map LitSet (Var, Bool, Bool))
tableConj
    , encITETable :: MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
encITETable = MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
tableITE
    , encXORTable :: MutVar (PrimState m) (Map (Var, Var) (Var, Bool, Bool))
encXORTable = MutVar (PrimState m) (Map (Var, Var) (Var, Bool, Bool))
tableXOR
    , encFASumTable :: MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
encFASumTable = MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
tableFASum
    , encFACarryTable :: MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
encFACarryTable = MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
tableFACarry
    }

-- | Use /pseudo boolean constraints/ or use only /clauses/.
-- This option has an effect only when the encoder is built using 'newEncoderWithPBLin'.
setUsePB :: PrimMonad m => Encoder m -> Bool -> m ()
setUsePB :: forall (m :: * -> *). PrimMonad m => Encoder m -> Bool -> m ()
setUsePB Encoder m
encoder Bool
usePB = MutVar (PrimState m) Bool -> Bool -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (Encoder m -> MutVar (PrimState m) Bool
forall (m :: * -> *). Encoder m -> MutVar (PrimState m) Bool
encUsePB Encoder m
encoder) Bool
usePB

-- | Assert a given formula to underlying SAT solver by using
-- Tseitin encoding.
addFormula :: PrimMonad m => Encoder m -> Formula -> m ()
addFormula :: forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
addFormula Encoder m
encoder Formula
formula = do
  case Formula
formula of
    And [Formula]
xs -> (Formula -> m ()) -> [Formula] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Encoder m -> Formula -> m ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
addFormula Encoder m
encoder) [Formula]
xs
    Equiv Formula
a Formula
b -> do
      Var
lit1 <- Encoder m -> Formula -> m Var
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Var
encodeFormula Encoder m
encoder Formula
a
      Var
lit2 <- Encoder m -> Formula -> m Var
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Var
encodeFormula Encoder m
encoder Formula
b
      Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var -> Var
SAT.litNot Var
lit1, Var
lit2] -- a→b
      Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var -> Var
SAT.litNot Var
lit2, Var
lit1] -- b→a
    Not (Not Formula
a)     -> Encoder m -> Formula -> m ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
addFormula Encoder m
encoder Formula
a
    Not (Or [Formula]
xs)     -> Encoder m -> Formula -> m ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
addFormula Encoder m
encoder ([Formula] -> Formula
forall a. MonotoneBoolean a => [a] -> a
andB ((Formula -> Formula) -> [Formula] -> [Formula]
forall a b. (a -> b) -> [a] -> [b]
map Formula -> Formula
forall a. Complement a => a -> a
notB [Formula]
xs))
    Not (Imply Formula
a Formula
b) -> Encoder m -> Formula -> m ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
addFormula Encoder m
encoder (Formula
a Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. Formula -> Formula
forall a. Complement a => a -> a
notB Formula
b)
    Not (Equiv Formula
a Formula
b) -> do
      Var
lit1 <- Encoder m -> Formula -> m Var
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Var
encodeFormula Encoder m
encoder Formula
a
      Var
lit2 <- Encoder m -> Formula -> m Var
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Var
encodeFormula Encoder m
encoder Formula
b
      Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var
lit1, Var
lit2] -- a ∨ b
      Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var -> Var
SAT.litNot Var
lit1, Var -> Var
SAT.litNot Var
lit2] -- ¬a ∨ ¬b
    ITE Formula
c Formula
t Formula
e -> do
      Var
c' <- Encoder m -> Formula -> m Var
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Var
encodeFormula Encoder m
encoder Formula
c
      Var
t' <- Encoder m -> Polarity -> Formula -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
polarityPos Formula
t
      Var
e' <- Encoder m -> Polarity -> Formula -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
polarityPos Formula
e
      Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [-Var
c', Var
t'] --  c' → t'
      Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [ Var
c', Var
e'] -- ¬c' → e'
    Formula
_ -> do
      [Var]
c <- Encoder m -> Formula -> m [Var]
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Formula -> m [Var]
encodeToClause Encoder m
encoder Formula
formula
      Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var]
c

encodeToClause :: PrimMonad m => Encoder m -> Formula -> m SAT.Clause
encodeToClause :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Formula -> m [Var]
encodeToClause Encoder m
encoder Formula
formula =
  case Formula
formula of
    And [Formula
x] -> Encoder m -> Formula -> m [Var]
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Formula -> m [Var]
encodeToClause Encoder m
encoder Formula
x
    Or [Formula]
xs -> do
      [[Var]]
cs <- (Formula -> m [Var]) -> [Formula] -> m [[Var]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Encoder m -> Formula -> m [Var]
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Formula -> m [Var]
encodeToClause Encoder m
encoder) [Formula]
xs
      [Var] -> m [Var]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Var] -> m [Var]) -> [Var] -> m [Var]
forall a b. (a -> b) -> a -> b
$ [[Var]] -> [Var]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Var]]
cs
    Not (Not Formula
x)  -> Encoder m -> Formula -> m [Var]
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Formula -> m [Var]
encodeToClause Encoder m
encoder Formula
x
    Not (And [Formula]
xs) -> do
      Encoder m -> Formula -> m [Var]
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Formula -> m [Var]
encodeToClause Encoder m
encoder ([Formula] -> Formula
forall a. MonotoneBoolean a => [a] -> a
orB ((Formula -> Formula) -> [Formula] -> [Formula]
forall a b. (a -> b) -> [a] -> [b]
map Formula -> Formula
forall a. Complement a => a -> a
notB [Formula]
xs))
    Imply Formula
a Formula
b -> do
      Encoder m -> Formula -> m [Var]
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Formula -> m [Var]
encodeToClause Encoder m
encoder (Formula -> Formula
forall a. Complement a => a -> a
notB Formula
a Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.||. Formula
b)
    Formula
_ -> do
      Var
l <- Encoder m -> Polarity -> Formula -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
polarityPos Formula
formula
      [Var] -> m [Var]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [Var
l]

encodeFormula :: PrimMonad m => Encoder m -> Formula -> m SAT.Lit
encodeFormula :: forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Var
encodeFormula Encoder m
encoder = Encoder m -> Polarity -> Formula -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
polarityBoth

encodeWithPolarityHelper
  :: (PrimMonad m, Ord k)
  => Encoder m
  -> MutVar (PrimState m) (Map k (SAT.Var, Bool, Bool))
  -> (SAT.Lit -> m ()) -> (SAT.Lit -> m ())
  -> Polarity
  -> k
  -> m SAT.Var
encodeWithPolarityHelper :: forall (m :: * -> *) k.
(PrimMonad m, Ord k) =>
Encoder m
-> MutVar (PrimState m) (Map k (Var, Bool, Bool))
-> (Var -> m ())
-> (Var -> m ())
-> Polarity
-> k
-> m Var
encodeWithPolarityHelper Encoder m
encoder MutVar (PrimState m) (Map k (Var, Bool, Bool))
tableRef Var -> m ()
definePos Var -> m ()
defineNeg (Polarity Bool
pos Bool
neg) k
k = do
  Map k (Var, Bool, Bool)
table <- MutVar (PrimState m) (Map k (Var, Bool, Bool))
-> m (Map k (Var, Bool, Bool))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar MutVar (PrimState m) (Map k (Var, Bool, Bool))
tableRef
  case k -> Map k (Var, Bool, Bool) -> Maybe (Var, Bool, Bool)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
k Map k (Var, Bool, Bool)
table of
    Just (Var
v, Bool
posDefined, Bool
negDefined) -> do
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
pos Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
posDefined) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Var -> m ()
definePos Var
v
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
neg Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
negDefined) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Var -> m ()
defineNeg Var
v
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
posDefined Bool -> Bool -> Bool
forall a. Ord a => a -> a -> Bool
< Bool
pos Bool -> Bool -> Bool
|| Bool
negDefined Bool -> Bool -> Bool
forall a. Ord a => a -> a -> Bool
< Bool
neg) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
        MutVar (PrimState m) (Map k (Var, Bool, Bool))
-> (Map k (Var, Bool, Bool) -> Map k (Var, Bool, Bool)) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar' MutVar (PrimState m) (Map k (Var, Bool, Bool))
tableRef (k
-> (Var, Bool, Bool)
-> Map k (Var, Bool, Bool)
-> Map k (Var, Bool, Bool)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
k (Var
v, (Bool -> Bool -> Bool
forall a. Ord a => a -> a -> a
max Bool
posDefined Bool
pos), (Bool -> Bool -> Bool
forall a. Ord a => a -> a -> a
max Bool
negDefined Bool
neg)))
      Var -> m Var
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Var
v
    Maybe (Var, Bool, Bool)
Nothing -> do
      Var
v <- Encoder m -> m Var
forall (m :: * -> *) a. NewVar m a => a -> m Var
SAT.newVar Encoder m
encoder
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
pos (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Var -> m ()
definePos Var
v
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
neg (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Var -> m ()
defineNeg Var
v
      MutVar (PrimState m) (Map k (Var, Bool, Bool))
-> (Map k (Var, Bool, Bool) -> Map k (Var, Bool, Bool)) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar' MutVar (PrimState m) (Map k (Var, Bool, Bool))
tableRef (k
-> (Var, Bool, Bool)
-> Map k (Var, Bool, Bool)
-> Map k (Var, Bool, Bool)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
k (Var
v, Bool
pos, Bool
neg))
      Var -> m Var
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Var
v


encodeFormulaWithPolarity :: PrimMonad m => Encoder m -> Polarity -> Formula -> m SAT.Lit
encodeFormulaWithPolarity :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
p Formula
formula = do
  case Formula
formula of
    Atom Var
l -> Var -> m Var
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Var
l
    And [Formula]
xs -> Encoder m -> Polarity -> [Var] -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> [Var] -> m Var
encodeConjWithPolarity Encoder m
encoder Polarity
p ([Var] -> m Var) -> m [Var] -> m Var
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Formula -> m Var) -> [Formula] -> m [Var]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Encoder m -> Polarity -> Formula -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
p) [Formula]
xs
    Or [Formula]
xs  -> Encoder m -> Polarity -> [Var] -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> [Var] -> m Var
encodeDisjWithPolarity Encoder m
encoder Polarity
p ([Var] -> m Var) -> m [Var] -> m Var
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Formula -> m Var) -> [Formula] -> m [Var]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Encoder m -> Polarity -> Formula -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
p) [Formula]
xs
    Not Formula
x -> (Var -> Var) -> m Var -> m Var
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Var -> Var
SAT.litNot (m Var -> m Var) -> m Var -> m Var
forall a b. (a -> b) -> a -> b
$ Encoder m -> Polarity -> Formula -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder (Polarity -> Polarity
negatePolarity Polarity
p) Formula
x
    Imply Formula
x Formula
y -> do
      Encoder m -> Polarity -> Formula -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
p (Formula -> Formula
forall a. Complement a => a -> a
notB Formula
x Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.||. Formula
y)
    Equiv Formula
x Formula
y -> do
      Var
lit1 <- Encoder m -> Polarity -> Formula -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
polarityBoth Formula
x
      Var
lit2 <- Encoder m -> Polarity -> Formula -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
polarityBoth Formula
y
      Encoder m -> Polarity -> Formula -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
p (Formula -> m Var) -> Formula -> m Var
forall a b. (a -> b) -> a -> b
$
        (Var -> Formula
Atom Var
lit1 Formula -> Formula -> Formula
forall a. Boolean a => a -> a -> a
.=>. Var -> Formula
Atom Var
lit2) Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. (Var -> Formula
Atom Var
lit2 Formula -> Formula -> Formula
forall a. Boolean a => a -> a -> a
.=>. Var -> Formula
Atom Var
lit1)
    ITE Formula
c Formula
t Formula
e -> do
      Var
c' <- Encoder m -> Polarity -> Formula -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
polarityBoth Formula
c
      Var
t' <- Encoder m -> Polarity -> Formula -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
p Formula
t
      Var
e' <- Encoder m -> Polarity -> Formula -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
p Formula
e
      Encoder m -> Polarity -> Var -> Var -> Var -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Var -> Var -> Var -> m Var
encodeITEWithPolarity Encoder m
encoder Polarity
p Var
c' Var
t' Var
e'

-- | Return an literal which is equivalent to a given conjunction.
--
-- @
--   encodeConj encoder = 'encodeConjWithPolarity' encoder 'polarityBoth'
-- @
encodeConj :: PrimMonad m => Encoder m -> [SAT.Lit] -> m SAT.Lit
encodeConj :: forall (m :: * -> *). PrimMonad m => Encoder m -> [Var] -> m Var
encodeConj Encoder m
encoder = Encoder m -> Polarity -> [Var] -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> [Var] -> m Var
encodeConjWithPolarity Encoder m
encoder Polarity
polarityBoth

-- | Return an literal which is equivalent to a given conjunction which occurs only in specified polarity.
encodeConjWithPolarity :: forall m. PrimMonad m => Encoder m -> Polarity -> [SAT.Lit] -> m SAT.Lit
encodeConjWithPolarity :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> [Var] -> m Var
encodeConjWithPolarity Encoder m
_ Polarity
_ [Var
l] =  Var -> m Var
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Var
l
encodeConjWithPolarity Encoder m
encoder Polarity
polarity [Var]
ls = do
  Bool
usePB <- MutVar (PrimState m) Bool -> m Bool
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (Encoder m -> MutVar (PrimState m) Bool
forall (m :: * -> *). Encoder m -> MutVar (PrimState m) Bool
encUsePB Encoder m
encoder)
  Map LitSet (Var, Bool, Bool)
table <- MutVar (PrimState m) (Map LitSet (Var, Bool, Bool))
-> m (Map LitSet (Var, Bool, Bool))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (Encoder m -> MutVar (PrimState m) (Map LitSet (Var, Bool, Bool))
forall (m :: * -> *).
Encoder m -> MutVar (PrimState m) (Map LitSet (Var, Bool, Bool))
encConjTable Encoder m
encoder)
  let ls3 :: LitSet
ls3 = [Var] -> LitSet
IntSet.fromList [Var]
ls
      ls2 :: LitSet
ls2 = case LitSet -> Map LitSet (Var, Bool, Bool) -> Maybe (Var, Bool, Bool)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup LitSet
IntSet.empty Map LitSet (Var, Bool, Bool)
table of
              Maybe (Var, Bool, Bool)
Nothing -> LitSet
ls3
              Just (Var
litTrue, Bool
_, Bool
_)
                | Var
litFalse Var -> LitSet -> Bool
`IntSet.member` LitSet
ls3 -> Var -> LitSet
IntSet.singleton Var
litFalse
                | Bool
otherwise -> Var -> LitSet -> LitSet
IntSet.delete Var
litTrue LitSet
ls3
                where litFalse :: Var
litFalse = Var -> Var
SAT.litNot Var
litTrue

  if LitSet -> Var
IntSet.size LitSet
ls2 Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
1 then do
    Var -> m Var
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> m Var) -> Var -> m Var
forall a b. (a -> b) -> a -> b
$ [Var] -> Var
forall a. HasCallStack => [a] -> a
head ([Var] -> Var) -> [Var] -> Var
forall a b. (a -> b) -> a -> b
$ LitSet -> [Var]
IntSet.toList LitSet
ls2
  else do
    let -- If F is monotone, F(A ∧ B) ⇔ ∃x. F(x) ∧ (x → A∧B)
        definePos :: SAT.Lit -> m ()
        definePos :: Var -> m ()
definePos Var
l = do
          case Encoder m -> Maybe (PBLinSum -> Integer -> m ())
forall (m :: * -> *).
Encoder m -> Maybe (PBLinSum -> Integer -> m ())
encAddPBAtLeast Encoder m
encoder of
            Just PBLinSum -> Integer -> m ()
addPBAtLeast | Bool
usePB -> do
              -- ∀i.(l → li) ⇔ Σli >= n*l ⇔ Σli - n*l >= 0
              let n :: Var
n = LitSet -> Var
IntSet.size LitSet
ls2
              PBLinSum -> Integer -> m ()
addPBAtLeast ((- Var -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Var
n, Var
l) PBLinTerm -> PBLinSum -> PBLinSum
forall a. a -> [a] -> [a]
: [(Integer
1,Var
li) | Var
li <- LitSet -> [Var]
IntSet.toList LitSet
ls2]) Integer
0
            Maybe (PBLinSum -> Integer -> m ())
_ -> do
              [Var] -> (Var -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (LitSet -> [Var]
IntSet.toList LitSet
ls2) ((Var -> m ()) -> m ()) -> (Var -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \Var
li -> do
                -- (l → li)  ⇔  (¬l ∨ li)
                Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var -> Var
SAT.litNot Var
l, Var
li]
        -- If F is anti-monotone, F(A ∧ B) ⇔ ∃x. F(x) ∧ (x ← A∧B) ⇔ ∃x. F(x) ∧ (x∨¬A∨¬B).
        defineNeg :: SAT.Lit -> m ()
        defineNeg :: Var -> m ()
defineNeg Var
l = do
          -- ((l1 ∧ l2 ∧ … ∧ ln) → l)  ⇔  (¬l1 ∨ ¬l2 ∨ … ∨ ¬ln ∨ l)
          Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder (Var
l Var -> [Var] -> [Var]
forall a. a -> [a] -> [a]
: (Var -> Var) -> [Var] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map Var -> Var
SAT.litNot (LitSet -> [Var]
IntSet.toList LitSet
ls2))
    Encoder m
-> MutVar (PrimState m) (Map LitSet (Var, Bool, Bool))
-> (Var -> m ())
-> (Var -> m ())
-> Polarity
-> LitSet
-> m Var
forall (m :: * -> *) k.
(PrimMonad m, Ord k) =>
Encoder m
-> MutVar (PrimState m) (Map k (Var, Bool, Bool))
-> (Var -> m ())
-> (Var -> m ())
-> Polarity
-> k
-> m Var
encodeWithPolarityHelper Encoder m
encoder (Encoder m -> MutVar (PrimState m) (Map LitSet (Var, Bool, Bool))
forall (m :: * -> *).
Encoder m -> MutVar (PrimState m) (Map LitSet (Var, Bool, Bool))
encConjTable Encoder m
encoder) Var -> m ()
definePos Var -> m ()
defineNeg Polarity
polarity LitSet
ls2

-- | Return an literal which is equivalent to a given disjunction.
--
-- @
--   encodeDisj encoder = 'encodeDisjWithPolarity' encoder 'polarityBoth'
-- @
encodeDisj :: PrimMonad m => Encoder m -> [SAT.Lit] -> m SAT.Lit
encodeDisj :: forall (m :: * -> *). PrimMonad m => Encoder m -> [Var] -> m Var
encodeDisj Encoder m
encoder = Encoder m -> Polarity -> [Var] -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> [Var] -> m Var
encodeDisjWithPolarity Encoder m
encoder Polarity
polarityBoth

-- | Return an literal which is equivalent to a given disjunction which occurs only in specified polarity.
encodeDisjWithPolarity :: PrimMonad m => Encoder m -> Polarity -> [SAT.Lit] -> m SAT.Lit
encodeDisjWithPolarity :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> [Var] -> m Var
encodeDisjWithPolarity Encoder m
_ Polarity
_ [Var
l] =  Var -> m Var
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Var
l
encodeDisjWithPolarity Encoder m
encoder Polarity
p [Var]
ls = do
  -- ¬l ⇔ ¬(¬l1 ∧ … ∧ ¬ln) ⇔ (l1 ∨ … ∨ ln)
  Var
l <- Encoder m -> Polarity -> [Var] -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> [Var] -> m Var
encodeConjWithPolarity Encoder m
encoder (Polarity -> Polarity
negatePolarity Polarity
p) [Var -> Var
SAT.litNot Var
li | Var
li <- [Var]
ls]
  Var -> m Var
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> m Var) -> Var -> m Var
forall a b. (a -> b) -> a -> b
$ Var -> Var
SAT.litNot Var
l

-- | Return an literal which is equivalent to a given if-then-else.
--
-- @
--   encodeITE encoder = 'encodeITEWithPolarity' encoder 'polarityBoth'
-- @
encodeITE :: PrimMonad m => Encoder m -> SAT.Lit -> SAT.Lit -> SAT.Lit -> m SAT.Lit
encodeITE :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Var -> Var -> Var -> m Var
encodeITE Encoder m
encoder = Encoder m -> Polarity -> Var -> Var -> Var -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Var -> Var -> Var -> m Var
encodeITEWithPolarity Encoder m
encoder Polarity
polarityBoth

-- | Return an literal which is equivalent to a given if-then-else which occurs only in specified polarity.
encodeITEWithPolarity :: forall m. PrimMonad m => Encoder m -> Polarity -> SAT.Lit -> SAT.Lit -> SAT.Lit -> m SAT.Lit
encodeITEWithPolarity :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Var -> Var -> Var -> m Var
encodeITEWithPolarity Encoder m
encoder Polarity
p Var
c Var
t Var
e | Var
c Var -> Var -> Bool
forall a. Ord a => a -> a -> Bool
< Var
0 =
  Encoder m -> Polarity -> Var -> Var -> Var -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Var -> Var -> Var -> m Var
encodeITEWithPolarity Encoder m
encoder Polarity
p (- Var
c) Var
e Var
t
encodeITEWithPolarity Encoder m
encoder Polarity
polarity Var
c Var
t Var
e = do
  let definePos :: SAT.Lit -> m ()
      definePos :: Var -> m ()
definePos Var
x = do
        -- x → ite(c,t,e)
        -- ⇔ x → (c∧t ∨ ¬c∧e)
        -- ⇔ (x∧c → t) ∧ (x∧¬c → e)
        -- ⇔ (¬x∨¬c∨t) ∧ (¬x∨c∨e)
        Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [-Var
x, -Var
c, Var
t]
        Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [-Var
x, Var
c, Var
e]
        Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var
t, Var
e, -Var
x] -- redundant, but will increase the strength of unit propagation.

      defineNeg :: SAT.Lit -> m ()
      defineNeg :: Var -> m ()
defineNeg Var
x = do
        -- ite(c,t,e) → x
        -- ⇔ (c∧t ∨ ¬c∧e) → x
        -- ⇔ (c∧t → x) ∨ (¬c∧e →x)
        -- ⇔ (¬c∨¬t∨x) ∨ (c∧¬e∨x)
        Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [-Var
c, -Var
t, Var
x]
        Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var
c, -Var
e, Var
x]
        Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [-Var
t, -Var
e, Var
x] -- redundant, but will increase the strength of unit propagation.

  Encoder m
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
-> (Var -> m ())
-> (Var -> m ())
-> Polarity
-> (Var, Var, Var)
-> m Var
forall (m :: * -> *) k.
(PrimMonad m, Ord k) =>
Encoder m
-> MutVar (PrimState m) (Map k (Var, Bool, Bool))
-> (Var -> m ())
-> (Var -> m ())
-> Polarity
-> k
-> m Var
encodeWithPolarityHelper Encoder m
encoder (Encoder m
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
forall (m :: * -> *).
Encoder m
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
encITETable Encoder m
encoder) Var -> m ()
definePos Var -> m ()
defineNeg Polarity
polarity (Var
c,Var
t,Var
e)

-- | Return an literal which is equivalent to an XOR of given two literals.
--
-- @
--   encodeXOR encoder = 'encodeXORWithPolarity' encoder 'polarityBoth'
-- @
encodeXOR :: PrimMonad m => Encoder m -> SAT.Lit -> SAT.Lit -> m SAT.Lit
encodeXOR :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Var -> Var -> m Var
encodeXOR Encoder m
encoder = Encoder m -> Polarity -> Var -> Var -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Var -> Var -> m Var
encodeXORWithPolarity Encoder m
encoder Polarity
polarityBoth

-- | Return an literal which is equivalent to an XOR of given two literals which occurs only in specified polarity.
encodeXORWithPolarity :: forall m. PrimMonad m => Encoder m -> Polarity -> SAT.Lit -> SAT.Lit -> m SAT.Lit
encodeXORWithPolarity :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Var -> Var -> m Var
encodeXORWithPolarity Encoder m
encoder Polarity
polarity Var
a Var
b = do
  let defineNeg :: Var -> m ()
defineNeg Var
x = do
        -- (a ⊕ b) → x
        Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var
a, -Var
b, Var
x]   -- ¬a ∧  b → x
        Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [-Var
a, Var
b, Var
x]   --  a ∧ ¬b → x
      definePos :: Var -> m ()
definePos Var
x = do
        -- x → (a ⊕ b)
        Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var
a, Var
b, -Var
x]   -- ¬a ∧ ¬b → ¬x
        Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [-Var
a, -Var
b, -Var
x] --  a ∧  b → ¬x
  Encoder m
-> MutVar (PrimState m) (Map (Var, Var) (Var, Bool, Bool))
-> (Var -> m ())
-> (Var -> m ())
-> Polarity
-> (Var, Var)
-> m Var
forall (m :: * -> *) k.
(PrimMonad m, Ord k) =>
Encoder m
-> MutVar (PrimState m) (Map k (Var, Bool, Bool))
-> (Var -> m ())
-> (Var -> m ())
-> Polarity
-> k
-> m Var
encodeWithPolarityHelper Encoder m
encoder (Encoder m
-> MutVar (PrimState m) (Map (Var, Var) (Var, Bool, Bool))
forall (m :: * -> *).
Encoder m
-> MutVar (PrimState m) (Map (Var, Var) (Var, Bool, Bool))
encXORTable Encoder m
encoder) Var -> m ()
definePos Var -> m ()
defineNeg Polarity
polarity (Var
a,Var
b)

-- | Return an "sum"-pin of a full-adder.
--
-- @
--   encodeFASum encoder = 'encodeFASumWithPolarity' encoder 'polarityBoth'
-- @
encodeFASum :: forall m. PrimMonad m => Encoder m -> SAT.Lit -> SAT.Lit -> SAT.Lit -> m SAT.Lit
encodeFASum :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Var -> Var -> Var -> m Var
encodeFASum Encoder m
encoder = Encoder m -> Polarity -> Var -> Var -> Var -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Var -> Var -> Var -> m Var
encodeFASumWithPolarity Encoder m
encoder Polarity
polarityBoth

-- | Return an "sum"-pin of a full-adder which occurs only in specified polarity.
encodeFASumWithPolarity :: forall m. PrimMonad m => Encoder m -> Polarity -> SAT.Lit -> SAT.Lit -> SAT.Lit -> m SAT.Lit
encodeFASumWithPolarity :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Var -> Var -> Var -> m Var
encodeFASumWithPolarity Encoder m
encoder Polarity
polarity Var
a Var
b Var
c = do
  let defineNeg :: Var -> m ()
defineNeg Var
x = do
        -- FASum(a,b,c) → x
        Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [-Var
a,-Var
b,-Var
c,Var
x] --  a ∧  b ∧  c → x
        Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [-Var
a,Var
b,Var
c,Var
x]   --  a ∧ ¬b ∧ ¬c → x
        Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var
a,-Var
b,Var
c,Var
x]   -- ¬a ∧  b ∧ ¬c → x
        Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var
a,Var
b,-Var
c,Var
x]   -- ¬a ∧ ¬b ∧  c → x
      definePos :: Var -> m ()
definePos Var
x = do
        -- x → FASum(a,b,c)
        -- ⇔ ¬FASum(a,b,c) → ¬x
        Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var
a,Var
b,Var
c,-Var
x]   -- ¬a ∧ ¬b ∧ ¬c → ¬x
        Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var
a,-Var
b,-Var
c,-Var
x] -- ¬a ∧  b ∧  c → ¬x
        Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [-Var
a,Var
b,-Var
c,-Var
x] --  a ∧ ¬b ∧  c → ¬x
        Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [-Var
a,-Var
b,Var
c,-Var
x] --  a ∧  b ∧ ¬c → ¬x
  Encoder m
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
-> (Var -> m ())
-> (Var -> m ())
-> Polarity
-> (Var, Var, Var)
-> m Var
forall (m :: * -> *) k.
(PrimMonad m, Ord k) =>
Encoder m
-> MutVar (PrimState m) (Map k (Var, Bool, Bool))
-> (Var -> m ())
-> (Var -> m ())
-> Polarity
-> k
-> m Var
encodeWithPolarityHelper Encoder m
encoder (Encoder m
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
forall (m :: * -> *).
Encoder m
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
encFASumTable Encoder m
encoder) Var -> m ()
definePos Var -> m ()
defineNeg Polarity
polarity (Var
a,Var
b,Var
c)

-- | Return an "carry"-pin of a full-adder.
--
-- @
--   encodeFACarry encoder = 'encodeFACarryWithPolarity' encoder 'polarityBoth'
-- @
encodeFACarry :: forall m. PrimMonad m => Encoder m -> SAT.Lit -> SAT.Lit -> SAT.Lit -> m SAT.Lit
encodeFACarry :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Var -> Var -> Var -> m Var
encodeFACarry Encoder m
encoder = Encoder m -> Polarity -> Var -> Var -> Var -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Var -> Var -> Var -> m Var
encodeFACarryWithPolarity Encoder m
encoder Polarity
polarityBoth

-- | Return an "carry"-pin of a full-adder which occurs only in specified polarity.
encodeFACarryWithPolarity :: forall m. PrimMonad m => Encoder m -> Polarity -> SAT.Lit -> SAT.Lit -> SAT.Lit -> m SAT.Lit
encodeFACarryWithPolarity :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Var -> Var -> Var -> m Var
encodeFACarryWithPolarity Encoder m
encoder Polarity
polarity Var
a Var
b Var
c = do
  let defineNeg :: Var -> m ()
defineNeg Var
x = do
        -- FACarry(a,b,c) → x
        Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [-Var
a,-Var
b,Var
x] -- a ∧ b → x
        Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [-Var
a,-Var
c,Var
x] -- a ∧ c → x
        Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [-Var
b,-Var
c,Var
x] -- b ∧ c → x
      definePos :: Var -> m ()
definePos Var
x = do
        -- x → FACarry(a,b,c)
        -- ⇔ ¬FACarry(a,b,c) → ¬x
        Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var
a,Var
b,-Var
x]  --  ¬a ∧ ¬b → ¬x
        Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var
a,Var
c,-Var
x]  --  ¬a ∧ ¬c → ¬x
        Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var
b,Var
c,-Var
x]  --  ¬b ∧ ¬c → ¬x
  Encoder m
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
-> (Var -> m ())
-> (Var -> m ())
-> Polarity
-> (Var, Var, Var)
-> m Var
forall (m :: * -> *) k.
(PrimMonad m, Ord k) =>
Encoder m
-> MutVar (PrimState m) (Map k (Var, Bool, Bool))
-> (Var -> m ())
-> (Var -> m ())
-> Polarity
-> k
-> m Var
encodeWithPolarityHelper Encoder m
encoder (Encoder m
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
forall (m :: * -> *).
Encoder m
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
encFACarryTable Encoder m
encoder) Var -> m ()
definePos Var -> m ()
defineNeg Polarity
polarity (Var
a,Var
b,Var
c)


getDefinitions :: PrimMonad m => Encoder m -> m (SAT.VarMap Formula)
getDefinitions :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> m (VarMap Formula)
getDefinitions Encoder m
encoder = do
  Map LitSet (Var, Bool, Bool)
tableConj <- MutVar (PrimState m) (Map LitSet (Var, Bool, Bool))
-> m (Map LitSet (Var, Bool, Bool))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (Encoder m -> MutVar (PrimState m) (Map LitSet (Var, Bool, Bool))
forall (m :: * -> *).
Encoder m -> MutVar (PrimState m) (Map LitSet (Var, Bool, Bool))
encConjTable Encoder m
encoder)
  Map (Var, Var, Var) (Var, Bool, Bool)
tableITE <- MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
-> m (Map (Var, Var, Var) (Var, Bool, Bool))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (Encoder m
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
forall (m :: * -> *).
Encoder m
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
encITETable Encoder m
encoder)
  Map (Var, Var) (Var, Bool, Bool)
tableXOR <- MutVar (PrimState m) (Map (Var, Var) (Var, Bool, Bool))
-> m (Map (Var, Var) (Var, Bool, Bool))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (Encoder m
-> MutVar (PrimState m) (Map (Var, Var) (Var, Bool, Bool))
forall (m :: * -> *).
Encoder m
-> MutVar (PrimState m) (Map (Var, Var) (Var, Bool, Bool))
encXORTable Encoder m
encoder)
  Map (Var, Var, Var) (Var, Bool, Bool)
tableFASum <- MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
-> m (Map (Var, Var, Var) (Var, Bool, Bool))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (Encoder m
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
forall (m :: * -> *).
Encoder m
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
encFASumTable Encoder m
encoder)
  Map (Var, Var, Var) (Var, Bool, Bool)
tableFACarry <- MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
-> m (Map (Var, Var, Var) (Var, Bool, Bool))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (Encoder m
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
forall (m :: * -> *).
Encoder m
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
encFACarryTable Encoder m
encoder)
  let atom :: Var -> Formula
atom Var
l
        | Var
l Var -> Var -> Bool
forall a. Ord a => a -> a -> Bool
< Var
0 = Formula -> Formula
Not (Var -> Formula
Atom (- Var
l))
        | Bool
otherwise = Var -> Formula
Atom Var
l
      m1 :: VarMap Formula
m1 = [(Var, Formula)] -> VarMap Formula
forall a. [(Var, a)] -> IntMap a
IntMap.fromList [(Var
v, [Formula] -> Formula
forall a. MonotoneBoolean a => [a] -> a
andB [Var -> Formula
atom Var
l1 | Var
l1 <- LitSet -> [Var]
IntSet.toList LitSet
ls]) | (LitSet
ls, (Var
v, Bool
_, Bool
_)) <- Map LitSet (Var, Bool, Bool) -> [(LitSet, (Var, Bool, Bool))]
forall k a. Map k a -> [(k, a)]
Map.toList Map LitSet (Var, Bool, Bool)
tableConj]
      m2 :: VarMap Formula
m2 = [(Var, Formula)] -> VarMap Formula
forall a. [(Var, a)] -> IntMap a
IntMap.fromList [(Var
v, Formula -> Formula -> Formula -> Formula
forall b a. IfThenElse b a => b -> a -> a -> a
ite (Var -> Formula
atom Var
c) (Var -> Formula
atom Var
t) (Var -> Formula
atom Var
e)) | ((Var
c,Var
t,Var
e), (Var
v, Bool
_, Bool
_)) <- Map (Var, Var, Var) (Var, Bool, Bool)
-> [((Var, Var, Var), (Var, Bool, Bool))]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Var, Var, Var) (Var, Bool, Bool)
tableITE]
      m3 :: VarMap Formula
m3 = [(Var, Formula)] -> VarMap Formula
forall a. [(Var, a)] -> IntMap a
IntMap.fromList [(Var
v, (Var -> Formula
atom Var
a Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.||. Var -> Formula
atom Var
b) Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. (Var -> Formula
atom (-Var
a) Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.||. Var -> Formula
atom (-Var
b))) | ((Var
a,Var
b), (Var
v, Bool
_, Bool
_)) <- Map (Var, Var) (Var, Bool, Bool)
-> [((Var, Var), (Var, Bool, Bool))]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Var, Var) (Var, Bool, Bool)
tableXOR]
      m4 :: VarMap Formula
m4 = [(Var, Formula)] -> VarMap Formula
forall a. [(Var, a)] -> IntMap a
IntMap.fromList
             [ (Var
v, [Formula] -> Formula
forall a. MonotoneBoolean a => [a] -> a
orB [[Formula] -> Formula
forall a. MonotoneBoolean a => [a] -> a
andB [Var -> Formula
atom Var
l | Var
l <- [Var]
ls] | [Var]
ls <- [[Var
a,Var
b,Var
c],[Var
a,-Var
b,-Var
c],[-Var
a,Var
b,-Var
c],[-Var
a,-Var
b,Var
c]]])
             | ((Var
a,Var
b,Var
c), (Var
v, Bool
_, Bool
_)) <- Map (Var, Var, Var) (Var, Bool, Bool)
-> [((Var, Var, Var), (Var, Bool, Bool))]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Var, Var, Var) (Var, Bool, Bool)
tableFASum
             ]
      m5 :: VarMap Formula
m5 = [(Var, Formula)] -> VarMap Formula
forall a. [(Var, a)] -> IntMap a
IntMap.fromList
             [ (Var
v, [Formula] -> Formula
forall a. MonotoneBoolean a => [a] -> a
orB [[Formula] -> Formula
forall a. MonotoneBoolean a => [a] -> a
andB [Var -> Formula
atom Var
l | Var
l <- [Var]
ls] | [Var]
ls <- [[Var
a,Var
b],[Var
a,Var
c],[Var
b,Var
c]]])
             | ((Var
a,Var
b,Var
c), (Var
v, Bool
_, Bool
_)) <- Map (Var, Var, Var) (Var, Bool, Bool)
-> [((Var, Var, Var), (Var, Bool, Bool))]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Var, Var, Var) (Var, Bool, Bool)
tableFACarry
             ]
  VarMap Formula -> m (VarMap Formula)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (VarMap Formula -> m (VarMap Formula))
-> VarMap Formula -> m (VarMap Formula)
forall a b. (a -> b) -> a -> b
$ [VarMap Formula] -> VarMap Formula
forall (f :: * -> *) a. Foldable f => f (IntMap a) -> IntMap a
IntMap.unions [VarMap Formula
m1, VarMap Formula
m2, VarMap Formula
m3, VarMap Formula
m4, VarMap Formula
m5]


data Polarity
  = Polarity
  { Polarity -> Bool
polarityPosOccurs :: Bool
  , Polarity -> Bool
polarityNegOccurs :: Bool
  }
  deriving (Polarity -> Polarity -> Bool
(Polarity -> Polarity -> Bool)
-> (Polarity -> Polarity -> Bool) -> Eq Polarity
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Polarity -> Polarity -> Bool
== :: Polarity -> Polarity -> Bool
$c/= :: Polarity -> Polarity -> Bool
/= :: Polarity -> Polarity -> Bool
Eq, Var -> Polarity -> ShowS
[Polarity] -> ShowS
Polarity -> String
(Var -> Polarity -> ShowS)
-> (Polarity -> String) -> ([Polarity] -> ShowS) -> Show Polarity
forall a.
(Var -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Var -> Polarity -> ShowS
showsPrec :: Var -> Polarity -> ShowS
$cshow :: Polarity -> String
show :: Polarity -> String
$cshowList :: [Polarity] -> ShowS
showList :: [Polarity] -> ShowS
Show)

negatePolarity :: Polarity -> Polarity
negatePolarity :: Polarity -> Polarity
negatePolarity (Polarity Bool
pos Bool
neg) = (Bool -> Bool -> Polarity
Polarity Bool
neg Bool
pos)

polarityPos :: Polarity
polarityPos :: Polarity
polarityPos = Bool -> Bool -> Polarity
Polarity Bool
True Bool
False

polarityNeg :: Polarity
polarityNeg :: Polarity
polarityNeg = Bool -> Bool -> Polarity
Polarity Bool
False Bool
True

polarityBoth :: Polarity
polarityBoth :: Polarity
polarityBoth = Bool -> Bool -> Polarity
Polarity Bool
True Bool
True

polarityNone :: Polarity
polarityNone :: Polarity
polarityNone = Bool -> Bool -> Polarity
Polarity Bool
False Bool
False