{-# 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
  , 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 (Var, Bool, Bool))
encConjTable :: !(MutVar (PrimState m) (Map SAT.LitSet (SAT.Var, Bool, Bool)))
  , 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)))
  , Encoder m
-> MutVar (PrimState m) (Map (Var, Var) (Var, Bool, Bool))
encXORTable  :: !(MutVar (PrimState m) (Map (SAT.Lit, SAT.Lit) (SAT.Var, Bool, Bool)))
  , 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)))
  , Encoder m
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
encFACarryTable :: !(MutVar (PrimState m) (Map (SAT.Lit, SAT.Lit, SAT.Lit) (SAT.Var, Bool, Bool)))
  }

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

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

-- | Create a @Encoder@ instance.
-- If the encoder is built using this function, 'setUsePB' has no effect.
newEncoder :: PrimMonad m => SAT.AddClause m a => a -> m (Encoder m)
newEncoder :: a -> m (Encoder m)
newEncoder a
solver = do
  MutVar (PrimState m) Bool
usePBRef <- Bool -> m (MutVar (PrimState m) Bool)
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Bool
False
  MutVar (PrimState m) (Map LitSet (Var, Bool, Bool))
tableConj <- Map LitSet (Var, Bool, Bool)
-> m (MutVar (PrimState m) (Map LitSet (Var, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map LitSet (Var, Bool, Bool)
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
tableITE <- Map (Var, Var, Var) (Var, Bool, Bool)
-> m (MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Var, Var, Var) (Var, Bool, Bool)
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Var, Var) (Var, Bool, Bool))
tableXOR <- Map (Var, Var) (Var, Bool, Bool)
-> m (MutVar (PrimState m) (Map (Var, Var) (Var, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Var, Var) (Var, Bool, Bool)
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
tableFASum <- Map (Var, Var, Var) (Var, Bool, Bool)
-> m (MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Var, Var, Var) (Var, Bool, Bool)
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
tableFACarry <- Map (Var, Var, Var) (Var, Bool, Bool)
-> m (MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Var, Var, Var) (Var, Bool, Bool)
forall k a. Map k a
Map.empty
  Encoder m -> m (Encoder m)
forall (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 (Var, Bool, Bool))
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
-> MutVar (PrimState m) (Map (Var, Var) (Var, Bool, Bool))
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, 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 (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 :: a -> m (Encoder m)
newEncoderWithPBLin a
solver = do
  MutVar (PrimState m) Bool
usePBRef <- Bool -> m (MutVar (PrimState m) Bool)
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Bool
False
  MutVar (PrimState m) (Map LitSet (Var, Bool, Bool))
tableConj <- Map LitSet (Var, Bool, Bool)
-> m (MutVar (PrimState m) (Map LitSet (Var, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map LitSet (Var, Bool, Bool)
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
tableITE <- Map (Var, Var, Var) (Var, Bool, Bool)
-> m (MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Var, Var, Var) (Var, Bool, Bool)
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Var, Var) (Var, Bool, Bool))
tableXOR <- Map (Var, Var) (Var, Bool, Bool)
-> m (MutVar (PrimState m) (Map (Var, Var) (Var, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Var, Var) (Var, Bool, Bool)
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
tableFASum <- Map (Var, Var, Var) (Var, Bool, Bool)
-> m (MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Var, Var, Var) (Var, Bool, Bool)
forall k a. Map k a
Map.empty
  MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
tableFACarry <- Map (Var, Var, Var) (Var, Bool, Bool)
-> m (MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool)))
forall (m :: * -> *) a.
PrimMonad m =>
a -> m (MutVar (PrimState m) a)
newMutVar Map (Var, Var, Var) (Var, Bool, Bool)
forall k a. Map k a
Map.empty
  Encoder m -> m (Encoder m)
forall (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 (Var, Bool, Bool))
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
-> MutVar (PrimState m) (Map (Var, Var) (Var, Bool, Bool))
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, Bool, Bool))
-> MutVar (PrimState m) (Map (Var, Var, Var) (Var, 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 (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 :: 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
      Var
lit1 <- Encoder m -> Formula -> m Var
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Var
encodeFormula Encoder m
encoder Formula
a
      Var
lit2 <- Encoder m -> Formula -> m Var
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Var
encodeFormula Encoder m
encoder Formula
b
      Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var -> Var
SAT.litNot Var
lit1, Var
lit2] -- a→b
      Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var -> Var
SAT.litNot Var
lit2, Var
lit1] -- b→a
    Not (Not Formula
a)     -> Encoder m -> Formula -> m ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
addFormula Encoder m
encoder Formula
a
    Not (Or [Formula]
xs)     -> Encoder m -> Formula -> m ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
addFormula Encoder m
encoder ([Formula] -> Formula
forall a. MonotoneBoolean a => [a] -> a
andB ((Formula -> Formula) -> [Formula] -> [Formula]
forall a b. (a -> b) -> [a] -> [b]
map Formula -> Formula
forall a. Complement a => a -> a
notB [Formula]
xs))
    Not (Imply Formula
a Formula
b) -> Encoder m -> Formula -> m ()
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m ()
addFormula Encoder m
encoder (Formula
a Formula -> Formula -> Formula
forall a. MonotoneBoolean a => a -> a -> a
.&&. Formula -> Formula
forall a. Complement a => a -> a
notB Formula
b)
    Not (Equiv Formula
a Formula
b) -> do
      Var
lit1 <- Encoder m -> Formula -> m Var
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Var
encodeFormula Encoder m
encoder Formula
a
      Var
lit2 <- Encoder m -> Formula -> m Var
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Var
encodeFormula Encoder m
encoder Formula
b
      Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var
lit1, Var
lit2] -- a ∨ b
      Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var -> Var
SAT.litNot Var
lit1, Var -> Var
SAT.litNot Var
lit2] -- ¬a ∨ ¬b
    ITE Formula
c Formula
t Formula
e -> do
      Var
c' <- Encoder m -> Formula -> m Var
forall (m :: * -> *). PrimMonad m => Encoder m -> Formula -> m Var
encodeFormula Encoder m
encoder Formula
c
      Var
t' <- Encoder m -> Polarity -> Formula -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
polarityPos Formula
t
      Var
e' <- Encoder m -> Polarity -> Formula -> m Var
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Polarity -> Formula -> m Var
encodeFormulaWithPolarity Encoder m
encoder Polarity
polarityPos Formula
e
      Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [-Var
c', Var
t'] --  c' → t'
      Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [ Var
c', Var
e'] -- ¬c' → e'
    Formula
_ -> do
      [Var]
c <- Encoder m -> Formula -> m [Var]
forall (m :: * -> *).
PrimMonad m =>
Encoder m -> Formula -> m [Var]
encodeToClause Encoder m
encoder Formula
formula
      Encoder m -> [Var] -> m ()
forall (m :: * -> *) a. AddClause m a => a -> [Var] -> m ()
SAT.addClause Encoder m
encoder [Var]
c

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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