{-# 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 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 } = 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 } = 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 } = 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 } = 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 <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Bool
False
  MutVar (PrimState m) (Map LitSet (Var, Bool, Bool))
tableConj <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
tableITE <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Var, Var) (Var, Bool, Bool))
tableXOR <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
tableFASum <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
tableFACarry <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall k a. Map k a
Map.empty
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    Encoder
    { encBase :: a
encBase = a
solver
    , encAddPBAtLeast :: Maybe (PBLinSum -> Integer -> m ())
encAddPBAtLeast = 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 <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Bool
False
  MutVar (PrimState m) (Map LitSet (Var, Bool, Bool))
tableConj <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
tableITE <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Var, Var) (Var, Bool, Bool))
tableXOR <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
tableFASum <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
tableFACarry <- forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar forall k a. Map k a
Map.empty
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
    Encoder
    { encBase :: a
encBase = a
solver
    , encAddPBAtLeast :: Maybe (PBLinSum -> Integer -> m ())
encAddPBAtLeast = forall a. a -> Maybe a
Just (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 = forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> a -> m ()
writeMutVar (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 -> forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
addFormula Encoder m
encoder) [Formula]
xs
    Equiv Formula
a Formula
b -> do
      Var
lit1 <- forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Var
encodeFormula Encoder m
encoder Formula
a
      Var
lit2 <- forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Var
encodeFormula Encoder m
encoder Formula
b
      forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var -> Var
SAT.litNot Var
lit1, Var
lit2] -- a→b
      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)     -> forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
addFormula Encoder m
encoder Formula
a
    Not (Or [Formula]
xs)     -> forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
addFormula Encoder m
encoder (forall a. MonotoneBoolean a => [a] -> a
andB (forall a b. (a -> b) -> [a] -> [b]
map forall a. Complement a => a -> a
notB [Formula]
xs))
    Not (Imply Formula
a Formula
b) -> forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
addFormula Encoder m
encoder (Formula
a forall a. MonotoneBoolean a => a -> a -> a
.&&. forall a. Complement a => a -> a
notB Formula
b)
    Not (Equiv Formula
a Formula
b) -> do
      Var
lit1 <- forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Var
encodeFormula Encoder m
encoder Formula
a
      Var
lit2 <- forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Var
encodeFormula Encoder m
encoder Formula
b
      forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var
lit1, Var
lit2] -- a ∨ b
      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' <- forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Var
encodeFormula Encoder m
encoder Formula
c
      Var
t' <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
polarityPos Formula
t
      Var
e' <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
polarityPos Formula
e
      forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [-Var
c', Var
t'] --  c' → t'
      forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [ Var
c', Var
e'] -- ¬c' → e'
    Formula
_ -> do
      [Var]
c <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Formula -> m [Var]
encodeToClause Encoder m
encoder Formula
formula
      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] -> forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Formula -> m [Var]
encodeToClause Encoder m
encoder Formula
x
    Or [Formula]
xs -> do
      [[Var]]
cs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Formula -> m [Var]
encodeToClause Encoder m
encoder) [Formula]
xs
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Var]]
cs
    Not (Not Formula
x)  -> forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Formula -> m [Var]
encodeToClause Encoder m
encoder Formula
x
    Not (And [Formula]
xs) -> do
      forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Formula -> m [Var]
encodeToClause Encoder m
encoder (forall a. MonotoneBoolean a => [a] -> a
orB (forall a b. (a -> b) -> [a] -> [b]
map forall a. Complement a => a -> a
notB [Formula]
xs))
    Imply Formula
a Formula
b -> do
      forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Formula -> m [Var]
encodeToClause Encoder m
encoder (forall a. Complement a => a -> a
notB Formula
a forall a. MonotoneBoolean a => a -> a -> a
.||. Formula
b)
    Formula
_ -> do
      Var
l <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
polarityPos Formula
formula
      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 = 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 <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar MutVar (PrimState m) (Map k (Var, Bool, Bool))
tableRef
  case 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
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
pos Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
posDefined) forall a b. (a -> b) -> a -> b
$ Var -> m ()
definePos Var
v
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
neg Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
negDefined) forall a b. (a -> b) -> a -> b
$ Var -> m ()
defineNeg Var
v
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
posDefined forall a. Ord a => a -> a -> Bool
< Bool
pos Bool -> Bool -> Bool
|| Bool
negDefined forall a. Ord a => a -> a -> Bool
< Bool
neg) forall a b. (a -> b) -> a -> b
$
        forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar' MutVar (PrimState m) (Map k (Var, Bool, Bool))
tableRef (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
k (Var
v, (forall a. Ord a => a -> a -> a
max Bool
posDefined Bool
pos), (forall a. Ord a => a -> a -> a
max Bool
negDefined Bool
neg)))
      forall (m :: * -> *) a. Monad m => a -> m a
return Var
v
    Maybe (Var, Bool, Bool)
Nothing -> do
      Var
v <- forall (m :: * -> *) a. NewVar m a => a -> m Var
SAT.newVar Encoder m
encoder
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
pos forall a b. (a -> b) -> a -> b
$ Var -> m ()
definePos Var
v
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
neg forall a b. (a -> b) -> a -> b
$ Var -> m ()
defineNeg Var
v
      forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> (a -> a) -> m ()
modifyMutVar' MutVar (PrimState m) (Map k (Var, Bool, Bool))
tableRef (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
k (Var
v, Bool
pos, Bool
neg))
      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 -> forall (m :: * -> *) a. Monad m => a -> m a
return Var
l
    And [Formula]
xs -> forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> [Var] -> m Var
encodeConjWithPolarity Encoder m
encoder Polarity
p forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
p) [Formula]
xs
    Or [Formula]
xs  -> forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> [Var] -> m Var
encodeDisjWithPolarity Encoder m
encoder Polarity
p forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
p) [Formula]
xs
    Not Formula
x -> forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Var -> Var
SAT.litNot forall a b. (a -> b) -> a -> b
$ 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
      forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
p (forall a. Complement a => a -> a
notB Formula
x forall a. MonotoneBoolean a => a -> a -> a
.||. Formula
y)
    Equiv Formula
x Formula
y -> do
      Var
lit1 <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
polarityBoth Formula
x
      Var
lit2 <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
polarityBoth Formula
y
      forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
p forall a b. (a -> b) -> a -> b
$
        (Var -> Formula
Atom Var
lit1 forall a. Boolean a => a -> a -> a
.=>. Var -> Formula
Atom Var
lit2) forall a. MonotoneBoolean a => a -> a -> a
.&&. (Var -> Formula
Atom Var
lit2 forall a. Boolean a => a -> a -> a
.=>. Var -> Formula
Atom Var
lit1)
    ITE Formula
c Formula
t Formula
e -> do
      Var
c' <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
polarityBoth Formula
c
      Var
t' <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
p Formula
t
      Var
e' <- forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
p Formula
e
      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 = 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] =  forall (m :: * -> *) a. Monad m => a -> m a
return Var
l
encodeConjWithPolarity Encoder m
encoder Polarity
polarity [Var]
ls = do
  Bool
usePB <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *). Encoder m -> MutVar (PrimState m) Bool
encUsePB Encoder m
encoder)
  Map LitSet (Var, Bool, Bool)
table <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (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 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 forall a. Eq a => a -> a -> Bool
== Var
1 then do
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
head 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 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 ((- forall a b. (Integral a, Num b) => a -> b
fromIntegral Var
n, Var
l) forall a. a -> [a] -> [a]
: [(Integer
1,Var
li) | Var
li <- LitSet -> [Var]
IntSet.toList LitSet
ls2]) Integer
0
            Maybe (PBLinSum -> Integer -> m ())
_ -> do
              forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (LitSet -> [Var]
IntSet.toList LitSet
ls2) forall a b. (a -> b) -> a -> b
$ \Var
li -> do
                -- (l → li)  ⇔  (¬l ∨ li)
                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)
          forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder (Var
l forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map Var -> Var
SAT.litNot (LitSet -> [Var]
IntSet.toList LitSet
ls2))
    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 (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 = 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] =  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 <- 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]
  forall (m :: * -> *) a. Monad m => a -> m a
return 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 = 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 forall a. Ord a => a -> a -> Bool
< Var
0 =
  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)
        forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [-Var
x, -Var
c, Var
t]
        forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [-Var
x, Var
c, Var
e]
        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)
        forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [-Var
c, -Var
t, Var
x]
        forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var
c, -Var
e, Var
x]
        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.

  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 (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 = 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
        forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var
a, -Var
b, Var
x]   -- ¬a ∧  b → x
        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)
        forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var
a, Var
b, -Var
x]   -- ¬a ∧ ¬b → ¬x
        forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [-Var
a, -Var
b, -Var
x] --  a ∧  b → ¬x
  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 (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 = 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
        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
        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
        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
        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
        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
        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
        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
        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
  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 (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 = 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
        forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [-Var
a,-Var
b,Var
x] -- a ∧ b → x
        forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [-Var
a,-Var
c,Var
x] -- a ∧ c → x
        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
        forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var
a,Var
b,-Var
x]  --  ¬a ∧ ¬b → ¬x
        forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var
a,Var
c,-Var
x]  --  ¬a ∧ ¬c → ¬x
        forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var
b,Var
c,-Var
x]  --  ¬b ∧ ¬c → ¬x
  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 (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.Var, Formula)]
getDefinitions :: forall (m :: * -> *).
PrimMonad m =>
Encoder m -> m [(Var, Formula)]
getDefinitions Encoder m
encoder = do
  Map LitSet (Var, Bool, Bool)
tableConj <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *).
Encoder m -> MutVar (PrimState m) (Map LitSet (Var, Bool, Bool))
encConjTable Encoder m
encoder)
  Map (Var, Var, Var) (Var, Bool, Bool)
tableITE <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (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 <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (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 <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (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 <- forall (m :: * -> *) a.
PrimMonad m =>
MutVar (PrimState m) a -> m a
readMutVar (forall (m :: * -> *).
Encoder m
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
encFACarryTable Encoder m
encoder)
  let m1 :: [(Var, Formula)]
m1 = [(Var
v, 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
_)) <- forall k a. Map k a -> [(k, a)]
Map.toList Map LitSet (Var, Bool, Bool)
tableConj]
      m2 :: [(Var, Formula)]
m2 = [(Var
v, 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
_)) <- forall k a. Map k a -> [(k, a)]
Map.toList Map (Var, Var, Var) (Var, Bool, Bool)
tableITE]
      m3 :: [(Var, Formula)]
m3 = [(Var
v, (Var -> Formula
Atom Var
a forall a. MonotoneBoolean a => a -> a -> a
.||. Var -> Formula
Atom Var
b) forall a. MonotoneBoolean a => a -> a -> a
.&&. (Var -> Formula
Atom (-Var
a) forall a. MonotoneBoolean a => a -> a -> a
.||. Var -> Formula
Atom (-Var
b))) | ((Var
a,Var
b), (Var
v, Bool
_, Bool
_)) <- forall k a. Map k a -> [(k, a)]
Map.toList Map (Var, Var) (Var, Bool, Bool)
tableXOR]
      m4 :: [(Var, Formula)]
m4 = [(Var
v, forall a. MonotoneBoolean a => [a] -> a
orB [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
_)) <- forall k a. Map k a -> [(k, a)]
Map.toList Map (Var, Var, Var) (Var, Bool, Bool)
tableFASum]
      m5 :: [(Var, Formula)]
m5 = [(Var
v, forall a. MonotoneBoolean a => [a] -> a
orB [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
_)) <- forall k a. Map k a -> [(k, a)]
Map.toList Map (Var, Var, Var) (Var, Bool, Bool)
tableFACarry]
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(Var, Formula)]
m1, [(Var, Formula)]
m2, [(Var, Formula)]
m3, [(Var, Formula)]
m4, [(Var, Formula)]
m5]


data Polarity
  = Polarity
  { Polarity -> Bool
polarityPosOccurs :: Bool
  , Polarity -> Bool
polarityNegOccurs :: Bool
  }
  deriving (Polarity -> Polarity -> Bool
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, Var -> Polarity -> ShowS
[Polarity] -> ShowS
Polarity -> String
forall a.
(Var -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Polarity] -> ShowS
$cshowList :: [Polarity] -> ShowS
show :: Polarity -> String
$cshow :: Polarity -> String
showsPrec :: Var -> Polarity -> ShowS
$cshowsPrec :: Var -> 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