{-# 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
  , Formula
  , evalFormula

  -- * 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 Data.Map (Map)
import qualified Data.Map as Map
import qualified Data.IntSet as IntSet
import ToySolver.Data.Boolean
import ToySolver.Data.BoolExpr
import qualified ToySolver.SAT.Types as SAT

-- | Arbitrary formula not restricted to CNF
type Formula = BoolExpr SAT.Lit

evalFormula :: SAT.IModel m => m -> Formula -> Bool
evalFormula :: m -> Formula -> Bool
evalFormula m
m = (Lit -> Bool) -> Formula -> Bool
forall b atom. Boolean b => (atom -> b) -> BoolExpr atom -> b
fold (m -> Lit -> Bool
forall m. IModel m => m -> Lit -> Bool
SAT.evalLit m
m)

-- | Encoder instance
data Encoder m =
  forall a. SAT.AddClause m a =>
  Encoder
  { ()
encBase :: a
  , Encoder m -> Maybe (PBLinSum -> Integer -> m ())
encAddPBAtLeast :: Maybe (SAT.PBLinSum -> Integer -> m ())
  , Encoder m -> MutVar (PrimState m) Bool
encUsePB     :: !(MutVar (PrimState m) Bool)
  , Encoder m -> MutVar (PrimState m) (Map LitSet (Lit, Bool, Bool))
encConjTable :: !(MutVar (PrimState m) (Map SAT.LitSet (SAT.Var, Bool, Bool)))
  , Encoder m
-> MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
encITETable  :: !(MutVar (PrimState m) (Map (SAT.Lit, SAT.Lit, SAT.Lit) (SAT.Var, Bool, Bool)))
  , Encoder m
-> MutVar (PrimState m) (Map (Lit, Lit) (Lit, Bool, Bool))
encXORTable  :: !(MutVar (PrimState m) (Map (SAT.Lit, SAT.Lit) (SAT.Var, Bool, Bool)))
  , Encoder m
-> MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
encFASumTable   :: !(MutVar (PrimState m) (Map (SAT.Lit, SAT.Lit, SAT.Lit) (SAT.Var, Bool, Bool)))
  , Encoder m
-> MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, 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 Lit
newVar   Encoder{ encBase :: ()
encBase = a
a } = a -> m Lit
forall (m :: * -> *) a. NewVar m a => a -> m Lit
SAT.newVar a
a
  newVars :: Encoder m -> Lit -> m [Lit]
newVars  Encoder{ encBase :: ()
encBase = a
a } = a -> Lit -> m [Lit]
forall (m :: * -> *) a. NewVar m a => a -> Lit -> m [Lit]
SAT.newVars a
a
  newVars_ :: Encoder m -> Lit -> m ()
newVars_ Encoder{ encBase :: ()
encBase = a
a } = a -> Lit -> m ()
forall (m :: * -> *) a. NewVar m a => a -> Lit -> m ()
SAT.newVars_ a
a

instance Monad m => SAT.AddClause m (Encoder m) where
  addClause :: Encoder m -> [Lit] -> m ()
addClause Encoder{ encBase :: ()
encBase = a
a } = a -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> 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 :: 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 (Lit, Bool, Bool))
tableConj <- Map LitSet (Lit, Bool, Bool)
-> m (MutVar (PrimState m) (Map LitSet (Lit, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map LitSet (Lit, Bool, Bool)
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
tableITE <- Map (Lit, Lit, Lit) (Lit, Bool, Bool)
-> m (MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Lit, Lit, Lit) (Lit, Bool, Bool)
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Lit, Lit) (Lit, Bool, Bool))
tableXOR <- Map (Lit, Lit) (Lit, Bool, Bool)
-> m (MutVar (PrimState m) (Map (Lit, Lit) (Lit, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Lit, Lit) (Lit, Bool, Bool)
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
tableFASum <- Map (Lit, Lit, Lit) (Lit, Bool, Bool)
-> m (MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Lit, Lit, Lit) (Lit, Bool, Bool)
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
tableFACarry <- Map (Lit, Lit, Lit) (Lit, Bool, Bool)
-> m (MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Lit, Lit, Lit) (Lit, Bool, Bool)
forall k a. Map k a
Map.empty
  Encoder m -> m (Encoder m)
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 :: forall (m :: * -> *) a.
AddClause m a =>
a
-> Maybe (PBLinSum -> Integer -> m ())
-> MutVar (PrimState m) Bool
-> MutVar (PrimState m) (Map LitSet (Lit, Bool, Bool))
-> MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
-> MutVar (PrimState m) (Map (Lit, Lit) (Lit, Bool, Bool))
-> MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
-> MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
-> Encoder m
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 (Lit, Bool, Bool))
encConjTable = MutVar (PrimState m) (Map LitSet (Lit, Bool, Bool))
tableConj
    , encITETable :: MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
encITETable = MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
tableITE
    , encXORTable :: MutVar (PrimState m) (Map (Lit, Lit) (Lit, Bool, Bool))
encXORTable = MutVar (PrimState m) (Map (Lit, Lit) (Lit, Bool, Bool))
tableXOR
    , encFASumTable :: MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
encFASumTable = MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
tableFASum
    , encFACarryTable :: MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
encFACarryTable = MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, 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 :: 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 (Lit, Bool, Bool))
tableConj <- Map LitSet (Lit, Bool, Bool)
-> m (MutVar (PrimState m) (Map LitSet (Lit, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map LitSet (Lit, Bool, Bool)
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
tableITE <- Map (Lit, Lit, Lit) (Lit, Bool, Bool)
-> m (MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Lit, Lit, Lit) (Lit, Bool, Bool)
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Lit, Lit) (Lit, Bool, Bool))
tableXOR <- Map (Lit, Lit) (Lit, Bool, Bool)
-> m (MutVar (PrimState m) (Map (Lit, Lit) (Lit, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Lit, Lit) (Lit, Bool, Bool)
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
tableFASum <- Map (Lit, Lit, Lit) (Lit, Bool, Bool)
-> m (MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Lit, Lit, Lit) (Lit, Bool, Bool)
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
tableFACarry <- Map (Lit, Lit, Lit) (Lit, Bool, Bool)
-> m (MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Lit, Lit, Lit) (Lit, Bool, Bool)
forall k a. Map k a
Map.empty
  Encoder m -> m (Encoder m)
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 :: forall (m :: * -> *) a.
AddClause m a =>
a
-> Maybe (PBLinSum -> Integer -> m ())
-> MutVar (PrimState m) Bool
-> MutVar (PrimState m) (Map LitSet (Lit, Bool, Bool))
-> MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
-> MutVar (PrimState m) (Map (Lit, Lit) (Lit, Bool, Bool))
-> MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
-> MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
-> Encoder m
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 (Lit, Bool, Bool))
encConjTable = MutVar (PrimState m) (Map LitSet (Lit, Bool, Bool))
tableConj
    , encITETable :: MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
encITETable = MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
tableITE
    , encXORTable :: MutVar (PrimState m) (Map (Lit, Lit) (Lit, Bool, Bool))
encXORTable = MutVar (PrimState m) (Map (Lit, Lit) (Lit, Bool, Bool))
tableXOR
    , encFASumTable :: MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
encFASumTable = MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
tableFASum
    , encFACarryTable :: MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
encFACarryTable = MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, 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 :: 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 :: 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
      Lit
lit1 <- Encoder m -> Formula -> m Lit
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Lit
encodeFormula Encoder m
encoder Formula
a
      Lit
lit2 <- Encoder m -> Formula -> m Lit
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Lit
encodeFormula Encoder m
encoder Formula
b
      Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [Lit -> Lit
SAT.litNot Lit
lit1, Lit
lit2] -- a→b
      Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [Lit -> Lit
SAT.litNot Lit
lit2, Lit
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
      Lit
lit1 <- Encoder m -> Formula -> m Lit
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Lit
encodeFormula Encoder m
encoder Formula
a
      Lit
lit2 <- Encoder m -> Formula -> m Lit
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Lit
encodeFormula Encoder m
encoder Formula
b
      Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [Lit
lit1, Lit
lit2] -- a ∨ b
      Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [Lit -> Lit
SAT.litNot Lit
lit1, Lit -> Lit
SAT.litNot Lit
lit2] -- ¬a ∨ ¬b
    ITE Formula
c Formula
t Formula
e -> do
      Lit
c' <- Encoder m -> Formula -> m Lit
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Lit
encodeFormula Encoder m
encoder Formula
c
      Lit
t' <- Encoder m -> Polarity -> Formula -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Lit
encodeFormulaWithPolarity Encoder m
encoder Polarity
polarityPos Formula
t
      Lit
e' <- Encoder m -> Polarity -> Formula -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Lit
encodeFormulaWithPolarity Encoder m
encoder Polarity
polarityPos Formula
e
      Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [-Lit
c', Lit
t'] --  c' → t'
      Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [ Lit
c', Lit
e'] -- ¬c' → e'
    Formula
_ -> do
      [Lit]
c <- Encoder m -> Formula -> m [Lit]
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Formula -> m [Lit]
encodeToClause Encoder m
encoder Formula
formula
      Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [Lit]
c

encodeToClause :: PrimMonad m => Encoder m -> Formula -> m SAT.Clause
encodeToClause :: Encoder m -> Formula -> m [Lit]
encodeToClause Encoder m
encoder Formula
formula =
  case Formula
formula of
    And [Formula
x] -> Encoder m -> Formula -> m [Lit]
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Formula -> m [Lit]
encodeToClause Encoder m
encoder Formula
x
    Or [Formula]
xs -> do
      [[Lit]]
cs <- (Formula -> m [Lit]) -> [Formula] -> m [[Lit]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Encoder m -> Formula -> m [Lit]
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Formula -> m [Lit]
encodeToClause Encoder m
encoder) [Formula]
xs
      [Lit] -> m [Lit]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Lit] -> m [Lit]) -> [Lit] -> m [Lit]
forall a b. (a -> b) -> a -> b
$ [[Lit]] -> [Lit]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Lit]]
cs
    Not (Not Formula
x)  -> Encoder m -> Formula -> m [Lit]
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Formula -> m [Lit]
encodeToClause Encoder m
encoder Formula
x
    Not (And [Formula]
xs) -> do
      Encoder m -> Formula -> m [Lit]
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Formula -> m [Lit]
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 [Lit]
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Formula -> m [Lit]
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
      Lit
l <- Encoder m -> Polarity -> Formula -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Lit
encodeFormulaWithPolarity Encoder m
encoder Polarity
polarityPos Formula
formula
      [Lit] -> m [Lit]
forall (m :: * -> *) a. Monad m => a -> m a
return [Lit
l]

encodeFormula :: PrimMonad m => Encoder m -> Formula -> m SAT.Lit
encodeFormula :: Encoder m -> Formula -> m Lit
encodeFormula Encoder m
encoder = Encoder m -> Polarity -> Formula -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Lit
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 :: Encoder m
-> MutVar (PrimState m) (Map k (Lit, Bool, Bool))
-> (Lit -> m ())
-> (Lit -> m ())
-> Polarity
-> k
-> m Lit
encodeWithPolarityHelper Encoder m
encoder MutVar (PrimState m) (Map k (Lit, Bool, Bool))
tableRef Lit -> m ()
definePos Lit -> m ()
defineNeg (Polarity Bool
pos Bool
neg) k
k = do
  Map k (Lit, Bool, Bool)
table <- MutVar (PrimState m) (Map k (Lit, Bool, Bool))
-> m (Map k (Lit, Bool, Bool))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar MutVar (PrimState m) (Map k (Lit, Bool, Bool))
tableRef
  case k -> Map k (Lit, Bool, Bool) -> Maybe (Lit, Bool, Bool)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
k Map k (Lit, Bool, Bool)
table of
    Just (Lit
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
$ Lit -> m ()
definePos Lit
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
$ Lit -> m ()
defineNeg Lit
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 (Lit, Bool, Bool))
-> (Map k (Lit, Bool, Bool) -> Map k (Lit, Bool, Bool)) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar' MutVar (PrimState m) (Map k (Lit, Bool, Bool))
tableRef (k
-> (Lit, Bool, Bool)
-> Map k (Lit, Bool, Bool)
-> Map k (Lit, Bool, Bool)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
k (Lit
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)))
      Lit -> m Lit
forall (m :: * -> *) a. Monad m => a -> m a
return Lit
v
    Maybe (Lit, Bool, Bool)
Nothing -> do
      Lit
v <- Encoder m -> m Lit
forall (m :: * -> *) a. NewVar m a => a -> m Lit
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
$ Lit -> m ()
definePos Lit
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
$ Lit -> m ()
defineNeg Lit
v
      MutVar (PrimState m) (Map k (Lit, Bool, Bool))
-> (Map k (Lit, Bool, Bool) -> Map k (Lit, Bool, Bool)) -> m ()
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar' MutVar (PrimState m) (Map k (Lit, Bool, Bool))
tableRef (k
-> (Lit, Bool, Bool)
-> Map k (Lit, Bool, Bool)
-> Map k (Lit, Bool, Bool)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
k (Lit
v, Bool
pos, Bool
neg))
      Lit -> m Lit
forall (m :: * -> *) a. Monad m => a -> m a
return Lit
v


encodeFormulaWithPolarity :: PrimMonad m => Encoder m -> Polarity -> Formula -> m SAT.Lit
encodeFormulaWithPolarity :: Encoder m -> Polarity -> Formula -> m Lit
encodeFormulaWithPolarity Encoder m
encoder Polarity
p Formula
formula = do
  case Formula
formula of
    Atom Lit
l -> Lit -> m Lit
forall (m :: * -> *) a. Monad m => a -> m a
return Lit
l
    And [Formula]
xs -> Encoder m -> Polarity -> [Lit] -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> [Lit] -> m Lit
encodeConjWithPolarity Encoder m
encoder Polarity
p ([Lit] -> m Lit) -> m [Lit] -> m Lit
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Formula -> m Lit) -> [Formula] -> m [Lit]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Encoder m -> Polarity -> Formula -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Lit
encodeFormulaWithPolarity Encoder m
encoder Polarity
p) [Formula]
xs
    Or [Formula]
xs  -> Encoder m -> Polarity -> [Lit] -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> [Lit] -> m Lit
encodeDisjWithPolarity Encoder m
encoder Polarity
p ([Lit] -> m Lit) -> m [Lit] -> m Lit
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Formula -> m Lit) -> [Formula] -> m [Lit]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Encoder m -> Polarity -> Formula -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Lit
encodeFormulaWithPolarity Encoder m
encoder Polarity
p) [Formula]
xs
    Not Formula
x -> (Lit -> Lit) -> m Lit -> m Lit
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Lit -> Lit
SAT.litNot (m Lit -> m Lit) -> m Lit -> m Lit
forall a b. (a -> b) -> a -> b
$ Encoder m -> Polarity -> Formula -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Lit
encodeFormulaWithPolarity Encoder m
encoder (Polarity -> Polarity
negatePolarity Polarity
p) Formula
x
    Imply Formula
x Formula
y -> do
      Encoder m -> Polarity -> Formula -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Lit
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
      Lit
lit1 <- Encoder m -> Polarity -> Formula -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Lit
encodeFormulaWithPolarity Encoder m
encoder Polarity
polarityBoth Formula
x
      Lit
lit2 <- Encoder m -> Polarity -> Formula -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Lit
encodeFormulaWithPolarity Encoder m
encoder Polarity
polarityBoth Formula
y
      Encoder m -> Polarity -> Formula -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Lit
encodeFormulaWithPolarity Encoder m
encoder Polarity
p (Formula -> m Lit) -> Formula -> m Lit
forall a b. (a -> b) -> a -> b
$
        (Lit -> Formula
forall a. a -> BoolExpr a
Atom Lit
lit1 Formula -> Formula -> Formula
forall a. Boolean a => a -> a -> a
.=>. Lit -> Formula
forall a. a -> BoolExpr a
Atom Lit
lit2) Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. (Lit -> Formula
forall a. a -> BoolExpr a
Atom Lit
lit2 Formula -> Formula -> Formula
forall a. Boolean a => a -> a -> a
.=>. Lit -> Formula
forall a. a -> BoolExpr a
Atom Lit
lit1)
    ITE Formula
c Formula
t Formula
e -> do
      Lit
c' <- Encoder m -> Polarity -> Formula -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Lit
encodeFormulaWithPolarity Encoder m
encoder Polarity
polarityBoth Formula
c
      Lit
t' <- Encoder m -> Polarity -> Formula -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Lit
encodeFormulaWithPolarity Encoder m
encoder Polarity
p Formula
t
      Lit
e' <- Encoder m -> Polarity -> Formula -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Lit
encodeFormulaWithPolarity Encoder m
encoder Polarity
p Formula
e
      Encoder m -> Polarity -> Lit -> Lit -> Lit -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Lit -> Lit -> Lit -> m Lit
encodeITEWithPolarity Encoder m
encoder Polarity
p Lit
c' Lit
t' Lit
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 :: Encoder m -> [Lit] -> m Lit
encodeConj Encoder m
encoder = Encoder m -> Polarity -> [Lit] -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> [Lit] -> m Lit
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 :: Encoder m -> Polarity -> [Lit] -> m Lit
encodeConjWithPolarity Encoder m
_ Polarity
_ [Lit
l] =  Lit -> m Lit
forall (m :: * -> *) a. Monad m => a -> m a
return Lit
l
encodeConjWithPolarity Encoder m
encoder Polarity
polarity [Lit]
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 (Lit, Bool, Bool)
table <- MutVar (PrimState m) (Map LitSet (Lit, Bool, Bool))
-> m (Map LitSet (Lit, Bool, Bool))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (Encoder m -> MutVar (PrimState m) (Map LitSet (Lit, Bool, Bool))
forall (m :: * -> *).
Encoder m -> MutVar (PrimState m) (Map LitSet (Lit, Bool, Bool))
encConjTable Encoder m
encoder)
  let ls3 :: LitSet
ls3 = [Lit] -> LitSet
IntSet.fromList [Lit]
ls
      ls2 :: LitSet
ls2 = case LitSet -> Map LitSet (Lit, Bool, Bool) -> Maybe (Lit, Bool, Bool)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup LitSet
IntSet.empty Map LitSet (Lit, Bool, Bool)
table of
              Maybe (Lit, Bool, Bool)
Nothing -> LitSet
ls3
              Just (Lit
litTrue, Bool
_, Bool
_)
                | Lit
litFalse Lit -> LitSet -> Bool
`IntSet.member` LitSet
ls3 -> Lit -> LitSet
IntSet.singleton Lit
litFalse
                | Bool
otherwise -> Lit -> LitSet -> LitSet
IntSet.delete Lit
litTrue LitSet
ls3
                where litFalse :: Lit
litFalse = Lit -> Lit
SAT.litNot Lit
litTrue

  if LitSet -> Lit
IntSet.size LitSet
ls2 Lit -> Lit -> Bool
forall a. Eq a => a -> a -> Bool
== Lit
1 then do
    Lit -> m Lit
forall (m :: * -> *) a. Monad m => a -> m a
return (Lit -> m Lit) -> Lit -> m Lit
forall a b. (a -> b) -> a -> b
$ [Lit] -> Lit
forall a. [a] -> a
head ([Lit] -> Lit) -> [Lit] -> Lit
forall a b. (a -> b) -> a -> b
$ LitSet -> [Lit]
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 :: Lit -> m ()
definePos Lit
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 :: Lit
n = LitSet -> Lit
IntSet.size LitSet
ls2
              PBLinSum -> Integer -> m ()
addPBAtLeast ((- Lit -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Lit
n, Lit
l) (Integer, Lit) -> PBLinSum -> PBLinSum
forall a. a -> [a] -> [a]
: [(Integer
1,Lit
li) | Lit
li <- LitSet -> [Lit]
IntSet.toList LitSet
ls2]) Integer
0
            Maybe (PBLinSum -> Integer -> m ())
_ -> do
              [Lit] -> (Lit -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (LitSet -> [Lit]
IntSet.toList LitSet
ls2) ((Lit -> m ()) -> m ()) -> (Lit -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \Lit
li -> do
                -- (l → li)  ⇔  (¬l ∨ li)
                Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [Lit -> Lit
SAT.litNot Lit
l, Lit
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 :: Lit -> m ()
defineNeg Lit
l = do
          -- ((l1 ∧ l2 ∧ … ∧ ln) → l)  ⇔  (¬l1 ∨ ¬l2 ∨ … ∨ ¬ln ∨ l)
          Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder (Lit
l Lit -> [Lit] -> [Lit]
forall a. a -> [a] -> [a]
: (Lit -> Lit) -> [Lit] -> [Lit]
forall a b. (a -> b) -> [a] -> [b]
map Lit -> Lit
SAT.litNot (LitSet -> [Lit]
IntSet.toList LitSet
ls2))
    Encoder m
-> MutVar (PrimState m) (Map LitSet (Lit, Bool, Bool))
-> (Lit -> m ())
-> (Lit -> m ())
-> Polarity
-> LitSet
-> m Lit
forall (m :: * -> *) k.
(PrimMonad m, Ord k) =>
Encoder m
-> MutVar (PrimState m) (Map k (Lit, Bool, Bool))
-> (Lit -> m ())
-> (Lit -> m ())
-> Polarity
-> k
-> m Lit
encodeWithPolarityHelper Encoder m
encoder (Encoder m -> MutVar (PrimState m) (Map LitSet (Lit, Bool, Bool))
forall (m :: * -> *).
Encoder m -> MutVar (PrimState m) (Map LitSet (Lit, Bool, Bool))
encConjTable Encoder m
encoder) Lit -> m ()
definePos Lit -> 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 :: Encoder m -> [Lit] -> m Lit
encodeDisj Encoder m
encoder = Encoder m -> Polarity -> [Lit] -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> [Lit] -> m Lit
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 :: Encoder m -> Polarity -> [Lit] -> m Lit
encodeDisjWithPolarity Encoder m
_ Polarity
_ [Lit
l] =  Lit -> m Lit
forall (m :: * -> *) a. Monad m => a -> m a
return Lit
l
encodeDisjWithPolarity Encoder m
encoder Polarity
p [Lit]
ls = do
  -- ¬l ⇔ ¬(¬l1 ∧ … ∧ ¬ln) ⇔ (l1 ∨ … ∨ ln)
  Lit
l <- Encoder m -> Polarity -> [Lit] -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> [Lit] -> m Lit
encodeConjWithPolarity Encoder m
encoder (Polarity -> Polarity
negatePolarity Polarity
p) [Lit -> Lit
SAT.litNot Lit
li | Lit
li <- [Lit]
ls]
  Lit -> m Lit
forall (m :: * -> *) a. Monad m => a -> m a
return (Lit -> m Lit) -> Lit -> m Lit
forall a b. (a -> b) -> a -> b
$ Lit -> Lit
SAT.litNot Lit
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 :: Encoder m -> Lit -> Lit -> Lit -> m Lit
encodeITE Encoder m
encoder = Encoder m -> Polarity -> Lit -> Lit -> Lit -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Lit -> Lit -> Lit -> m Lit
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 :: Encoder m -> Polarity -> Lit -> Lit -> Lit -> m Lit
encodeITEWithPolarity Encoder m
encoder Polarity
p Lit
c Lit
t Lit
e | Lit
c Lit -> Lit -> Bool
forall a. Ord a => a -> a -> Bool
< Lit
0 =
  Encoder m -> Polarity -> Lit -> Lit -> Lit -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Lit -> Lit -> Lit -> m Lit
encodeITEWithPolarity Encoder m
encoder Polarity
p (- Lit
c) Lit
e Lit
t
encodeITEWithPolarity Encoder m
encoder Polarity
polarity Lit
c Lit
t Lit
e = do
  let definePos :: SAT.Lit -> m ()
      definePos :: Lit -> m ()
definePos Lit
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 -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [-Lit
x, -Lit
c, Lit
t]
        Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [-Lit
x, Lit
c, Lit
e]
        Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [Lit
t, Lit
e, -Lit
x] -- redundant, but will increase the strength of unit propagation.

      defineNeg :: SAT.Lit -> m ()
      defineNeg :: Lit -> m ()
defineNeg Lit
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 -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [-Lit
c, -Lit
t, Lit
x]
        Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [Lit
c, -Lit
e, Lit
x]
        Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [-Lit
t, -Lit
e, Lit
x] -- redundant, but will increase the strength of unit propagation.

  Encoder m
-> MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
-> (Lit -> m ())
-> (Lit -> m ())
-> Polarity
-> (Lit, Lit, Lit)
-> m Lit
forall (m :: * -> *) k.
(PrimMonad m, Ord k) =>
Encoder m
-> MutVar (PrimState m) (Map k (Lit, Bool, Bool))
-> (Lit -> m ())
-> (Lit -> m ())
-> Polarity
-> k
-> m Lit
encodeWithPolarityHelper Encoder m
encoder (Encoder m
-> MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
forall (m :: * -> *).
Encoder m
-> MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
encITETable Encoder m
encoder) Lit -> m ()
definePos Lit -> m ()
defineNeg Polarity
polarity (Lit
c,Lit
t,Lit
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 :: Encoder m -> Lit -> Lit -> m Lit
encodeXOR Encoder m
encoder = Encoder m -> Polarity -> Lit -> Lit -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Lit -> Lit -> m Lit
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 :: Encoder m -> Polarity -> Lit -> Lit -> m Lit
encodeXORWithPolarity Encoder m
encoder Polarity
polarity Lit
a Lit
b = do
  let defineNeg :: Lit -> m ()
defineNeg Lit
x = do
        -- (a ⊕ b) → x
        Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [Lit
a, -Lit
b, Lit
x]   -- ¬a ∧  b → x
        Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [-Lit
a, Lit
b, Lit
x]   --  a ∧ ¬b → x
      definePos :: Lit -> m ()
definePos Lit
x = do
        -- x → (a ⊕ b)
        Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [Lit
a, Lit
b, -Lit
x]   -- ¬a ∧ ¬b → ¬x
        Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [-Lit
a, -Lit
b, -Lit
x] --  a ∧  b → ¬x
  Encoder m
-> MutVar (PrimState m) (Map (Lit, Lit) (Lit, Bool, Bool))
-> (Lit -> m ())
-> (Lit -> m ())
-> Polarity
-> (Lit, Lit)
-> m Lit
forall (m :: * -> *) k.
(PrimMonad m, Ord k) =>
Encoder m
-> MutVar (PrimState m) (Map k (Lit, Bool, Bool))
-> (Lit -> m ())
-> (Lit -> m ())
-> Polarity
-> k
-> m Lit
encodeWithPolarityHelper Encoder m
encoder (Encoder m
-> MutVar (PrimState m) (Map (Lit, Lit) (Lit, Bool, Bool))
forall (m :: * -> *).
Encoder m
-> MutVar (PrimState m) (Map (Lit, Lit) (Lit, Bool, Bool))
encXORTable Encoder m
encoder) Lit -> m ()
definePos Lit -> m ()
defineNeg Polarity
polarity (Lit
a,Lit
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 :: Encoder m -> Lit -> Lit -> Lit -> m Lit
encodeFASum Encoder m
encoder = Encoder m -> Polarity -> Lit -> Lit -> Lit -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Lit -> Lit -> Lit -> m Lit
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 :: Encoder m -> Polarity -> Lit -> Lit -> Lit -> m Lit
encodeFASumWithPolarity Encoder m
encoder Polarity
polarity Lit
a Lit
b Lit
c = do
  let defineNeg :: Lit -> m ()
defineNeg Lit
x = do
        -- FASum(a,b,c) → x
        Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [-Lit
a,-Lit
b,-Lit
c,Lit
x] --  a ∧  b ∧  c → x
        Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [-Lit
a,Lit
b,Lit
c,Lit
x]   --  a ∧ ¬b ∧ ¬c → x
        Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [Lit
a,-Lit
b,Lit
c,Lit
x]   -- ¬a ∧  b ∧ ¬c → x
        Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [Lit
a,Lit
b,-Lit
c,Lit
x]   -- ¬a ∧ ¬b ∧  c → x
      definePos :: Lit -> m ()
definePos Lit
x = do
        -- x → FASum(a,b,c)
        -- ⇔ ¬FASum(a,b,c) → ¬x
        Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [Lit
a,Lit
b,Lit
c,-Lit
x]   -- ¬a ∧ ¬b ∧ ¬c → ¬x
        Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [Lit
a,-Lit
b,-Lit
c,-Lit
x] -- ¬a ∧  b ∧  c → ¬x
        Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [-Lit
a,Lit
b,-Lit
c,-Lit
x] --  a ∧ ¬b ∧  c → ¬x
        Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [-Lit
a,-Lit
b,Lit
c,-Lit
x] --  a ∧  b ∧ ¬c → ¬x
  Encoder m
-> MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
-> (Lit -> m ())
-> (Lit -> m ())
-> Polarity
-> (Lit, Lit, Lit)
-> m Lit
forall (m :: * -> *) k.
(PrimMonad m, Ord k) =>
Encoder m
-> MutVar (PrimState m) (Map k (Lit, Bool, Bool))
-> (Lit -> m ())
-> (Lit -> m ())
-> Polarity
-> k
-> m Lit
encodeWithPolarityHelper Encoder m
encoder (Encoder m
-> MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
forall (m :: * -> *).
Encoder m
-> MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
encFASumTable Encoder m
encoder) Lit -> m ()
definePos Lit -> m ()
defineNeg Polarity
polarity (Lit
a,Lit
b,Lit
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 :: Encoder m -> Lit -> Lit -> Lit -> m Lit
encodeFACarry Encoder m
encoder = Encoder m -> Polarity -> Lit -> Lit -> Lit -> m Lit
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Lit -> Lit -> Lit -> m Lit
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 :: Encoder m -> Polarity -> Lit -> Lit -> Lit -> m Lit
encodeFACarryWithPolarity Encoder m
encoder Polarity
polarity Lit
a Lit
b Lit
c = do
  let defineNeg :: Lit -> m ()
defineNeg Lit
x = do
        -- FACarry(a,b,c) → x
        Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [-Lit
a,-Lit
b,Lit
x] -- a ∧ b → x
        Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [-Lit
a,-Lit
c,Lit
x] -- a ∧ c → x
        Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [-Lit
b,-Lit
c,Lit
x] -- b ∧ c → x
      definePos :: Lit -> m ()
definePos Lit
x = do
        -- x → FACarry(a,b,c)
        -- ⇔ ¬FACarry(a,b,c) → ¬x
        Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [Lit
a,Lit
b,-Lit
x]  --  ¬a ∧ ¬b → ¬x
        Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [Lit
a,Lit
c,-Lit
x]  --  ¬a ∧ ¬c → ¬x
        Encoder m -> [Lit] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Lit] -> m ()
SAT.addClause Encoder m
encoder [Lit
b,Lit
c,-Lit
x]  --  ¬b ∧ ¬c → ¬x
  Encoder m
-> MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
-> (Lit -> m ())
-> (Lit -> m ())
-> Polarity
-> (Lit, Lit, Lit)
-> m Lit
forall (m :: * -> *) k.
(PrimMonad m, Ord k) =>
Encoder m
-> MutVar (PrimState m) (Map k (Lit, Bool, Bool))
-> (Lit -> m ())
-> (Lit -> m ())
-> Polarity
-> k
-> m Lit
encodeWithPolarityHelper Encoder m
encoder (Encoder m
-> MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
forall (m :: * -> *).
Encoder m
-> MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
encFACarryTable Encoder m
encoder) Lit -> m ()
definePos Lit -> m ()
defineNeg Polarity
polarity (Lit
a,Lit
b,Lit
c)


getDefinitions :: PrimMonad m => Encoder m -> m [(SAT.Var, Formula)]
getDefinitions :: Encoder m -> m [(Lit, Formula)]
getDefinitions Encoder m
encoder = do
  Map LitSet (Lit, Bool, Bool)
tableConj <- MutVar (PrimState m) (Map LitSet (Lit, Bool, Bool))
-> m (Map LitSet (Lit, Bool, Bool))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (Encoder m -> MutVar (PrimState m) (Map LitSet (Lit, Bool, Bool))
forall (m :: * -> *).
Encoder m -> MutVar (PrimState m) (Map LitSet (Lit, Bool, Bool))
encConjTable Encoder m
encoder)
  Map (Lit, Lit, Lit) (Lit, Bool, Bool)
tableITE <- MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
-> m (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (Encoder m
-> MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
forall (m :: * -> *).
Encoder m
-> MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
encITETable Encoder m
encoder)
  Map (Lit, Lit) (Lit, Bool, Bool)
tableXOR <- MutVar (PrimState m) (Map (Lit, Lit) (Lit, Bool, Bool))
-> m (Map (Lit, Lit) (Lit, Bool, Bool))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (Encoder m
-> MutVar (PrimState m) (Map (Lit, Lit) (Lit, Bool, Bool))
forall (m :: * -> *).
Encoder m
-> MutVar (PrimState m) (Map (Lit, Lit) (Lit, Bool, Bool))
encXORTable Encoder m
encoder)
  Map (Lit, Lit, Lit) (Lit, Bool, Bool)
tableFASum <- MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
-> m (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (Encoder m
-> MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
forall (m :: * -> *).
Encoder m
-> MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
encFASumTable Encoder m
encoder)
  Map (Lit, Lit, Lit) (Lit, Bool, Bool)
tableFACarry <- MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
-> m (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (Encoder m
-> MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
forall (m :: * -> *).
Encoder m
-> MutVar (PrimState m) (Map (Lit, Lit, Lit) (Lit, Bool, Bool))
encFACarryTable Encoder m
encoder)
  let m1 :: [(Lit, Formula)]
m1 = [(Lit
v, [Formula] -> Formula
forall a. MonotoneBoolean a => [a] -> a
andB [Lit -> Formula
forall a. a -> BoolExpr a
Atom Lit
l1 | Lit
l1 <- LitSet -> [Lit]
IntSet.toList LitSet
ls]) | (LitSet
ls, (Lit
v, Bool
_, Bool
_)) <- Map LitSet (Lit, Bool, Bool) -> [(LitSet, (Lit, Bool, Bool))]
forall k a. Map k a -> [(k, a)]
Map.toList Map LitSet (Lit, Bool, Bool)
tableConj]
      m2 :: [(Lit, Formula)]
m2 = [(Lit
v, Formula -> Formula -> Formula -> Formula
forall b a. IfThenElse b a => b -> a -> a -> a
ite (Lit -> Formula
forall a. a -> BoolExpr a
Atom Lit
c) (Lit -> Formula
forall a. a -> BoolExpr a
Atom Lit
t) (Lit -> Formula
forall a. a -> BoolExpr a
Atom Lit
e)) | ((Lit
c,Lit
t,Lit
e), (Lit
v, Bool
_, Bool
_)) <- Map (Lit, Lit, Lit) (Lit, Bool, Bool)
-> [((Lit, Lit, Lit), (Lit, Bool, Bool))]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Lit, Lit, Lit) (Lit, Bool, Bool)
tableITE]
      m3 :: [(Lit, Formula)]
m3 = [(Lit
v, (Lit -> Formula
forall a. a -> BoolExpr a
Atom Lit
a Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.||. Lit -> Formula
forall a. a -> BoolExpr a
Atom Lit
b) Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. (Lit -> Formula
forall a. a -> BoolExpr a
Atom (-Lit
a) Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.||. Lit -> Formula
forall a. a -> BoolExpr a
Atom (-Lit
b))) | ((Lit
a,Lit
b), (Lit
v, Bool
_, Bool
_)) <- Map (Lit, Lit) (Lit, Bool, Bool)
-> [((Lit, Lit), (Lit, Bool, Bool))]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Lit, Lit) (Lit, Bool, Bool)
tableXOR]
      m4 :: [(Lit, Formula)]
m4 = [(Lit
v, [Formula] -> Formula
forall a. MonotoneBoolean a => [a] -> a
orB [[Formula] -> Formula
forall a. MonotoneBoolean a => [a] -> a
andB [Lit -> Formula
forall a. a -> BoolExpr a
Atom Lit
l | Lit
l <- [Lit]
ls] | [Lit]
ls <- [[Lit
a,Lit
b,Lit
c],[Lit
a,-Lit
b,-Lit
c],[-Lit
a,Lit
b,-Lit
c],[-Lit
a,-Lit
b,Lit
c]]])
             | ((Lit
a,Lit
b,Lit
c), (Lit
v, Bool
_, Bool
_)) <- Map (Lit, Lit, Lit) (Lit, Bool, Bool)
-> [((Lit, Lit, Lit), (Lit, Bool, Bool))]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Lit, Lit, Lit) (Lit, Bool, Bool)
tableFASum]
      m5 :: [(Lit, Formula)]
m5 = [(Lit
v, [Formula] -> Formula
forall a. MonotoneBoolean a => [a] -> a
orB [[Formula] -> Formula
forall a. MonotoneBoolean a => [a] -> a
andB [Lit -> Formula
forall a. a -> BoolExpr a
Atom Lit
l | Lit
l <- [Lit]
ls] | [Lit]
ls <- [[Lit
a,Lit
b],[Lit
a,Lit
c],[Lit
b,Lit
c]]])
             | ((Lit
a,Lit
b,Lit
c), (Lit
v, Bool
_, Bool
_)) <- Map (Lit, Lit, Lit) (Lit, Bool, Bool)
-> [((Lit, Lit, Lit), (Lit, Bool, Bool))]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Lit, Lit, Lit) (Lit, Bool, Bool)
tableFACarry]
  [(Lit, Formula)] -> m [(Lit, Formula)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Lit, Formula)] -> m [(Lit, Formula)])
-> [(Lit, Formula)] -> m [(Lit, Formula)]
forall a b. (a -> b) -> a -> b
$ [[(Lit, Formula)]] -> [(Lit, Formula)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Lit, Formula)]
m1, [(Lit, Formula)]
m2, [(Lit, Formula)]
m3, [(Lit, Formula)]
m4, [(Lit, 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
/= :: Polarity -> Polarity -> Bool
$c/= :: Polarity -> Polarity -> Bool
== :: Polarity -> Polarity -> Bool
$c== :: Polarity -> Polarity -> Bool
Eq, Lit -> Polarity -> ShowS
[Polarity] -> ShowS
Polarity -> String
(Lit -> Polarity -> ShowS)
-> (Polarity -> String) -> ([Polarity] -> ShowS) -> Show Polarity
forall a.
(Lit -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Polarity] -> ShowS
$cshowList :: [Polarity] -> ShowS
show :: Polarity -> String
$cshow :: Polarity -> String
showsPrec :: Lit -> Polarity -> ShowS
$cshowsPrec :: Lit -> 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