msakai / toysolver / 767

Committed 22 May 2025 12:57PM UTC coverage: 71.847% (-0.06%) from 71.906%

Build # 767

Build Type

push

github

Committed by

web-flow

Commit Message

Merge f4d92f6d1 into c10d256d2

Run Details

11104 of 15455 relevant lines covered (71.85%)

0.72 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

95.96

/src/ToySolver/SAT/Encoder/Tseitin.hs

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

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

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

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

  -- * Retrieving definitions
  , getDefinitions
  ) where

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

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

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

instance Monad m => SAT.AddClause m (Encoder m) where
  addClause Encoder{ encBase = a } = SAT.addClause 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 solver = do
  usePBRef <- newMutVar False
  tableConj <- newMutVar Map.empty
  tableITE <- newMutVar Map.empty
  tableXOR <- newMutVar Map.empty
  tableFASum <- newMutVar Map.empty
  tableFACarry <- newMutVar Map.empty
  return $
    Encoder
    { encBase = solver
    , encAddPBAtLeast = Nothing
    , encUsePB  = usePBRef
    , encConjTable = tableConj
    , encITETable = tableITE
    , encXORTable = tableXOR
    , encFASumTable = tableFASum
    , encFACarryTable = 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 solver = do
  usePBRef <- newMutVar False
  tableConj <- newMutVar Map.empty
  tableITE <- newMutVar Map.empty
  tableXOR <- newMutVar Map.empty
  tableFASum <- newMutVar Map.empty
  tableFACarry <- newMutVar Map.empty
  return $
    Encoder
    { encBase = solver
    , encAddPBAtLeast = Just (SAT.addPBAtLeast solver)
    , encUsePB  = usePBRef
    , encConjTable = tableConj
    , encITETable = tableITE
    , encXORTable = tableXOR
    , encFASumTable = tableFASum
    , encFACarryTable = 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 usePB = writeMutVar (encUsePB encoder) usePB

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

encodeToClause :: PrimMonad m => Encoder m -> Formula -> m SAT.Clause
encodeToClause encoder formula =
  case formula of
    And [x] -> encodeToClause encoder x
    Or xs -> do
      cs <- mapM (encodeToClause encoder) xs
      return $ concat cs
    Not (Not x)  -> encodeToClause encoder x
    Not (And xs) -> do
      encodeToClause encoder (orB (map notB xs))
    Imply a b -> do
      encodeToClause encoder (notB a .||. b)
    _ -> do
      l <- encodeFormulaWithPolarity encoder polarityPos formula
      return [l]

encodeFormula :: PrimMonad m => Encoder m -> Formula -> m SAT.Lit
encodeFormula encoder = encodeFormulaWithPolarity encoder 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 tableRef definePos defineNeg (Polarity pos neg) k = do
  table <- readMutVar tableRef
  case Map.lookup k table of
    Just (v, posDefined, negDefined) -> do
      when (pos && not posDefined) $ definePos v
      when (neg && not negDefined) $ defineNeg v
      when (posDefined < pos || negDefined < neg) $
        modifyMutVar' tableRef (Map.insert k (v, (max posDefined pos), (max negDefined neg)))
      return v
    Nothing -> do
      v <- SAT.newVar encoder
      when pos $ definePos v
      when neg $ defineNeg v
      modifyMutVar' tableRef (Map.insert k (v, pos, neg))
      return v


encodeFormulaWithPolarity :: PrimMonad m => Encoder m -> Polarity -> Formula -> m SAT.Lit
encodeFormulaWithPolarity encoder p formula = do
  case formula of
    Atom l -> return l
    And xs -> encodeConjWithPolarity encoder p =<< mapM (encodeFormulaWithPolarity encoder p) xs
    Or xs  -> encodeDisjWithPolarity encoder p =<< mapM (encodeFormulaWithPolarity encoder p) xs
    Not x -> liftM SAT.litNot $ encodeFormulaWithPolarity encoder (negatePolarity p) x
    Imply x y -> do
      encodeFormulaWithPolarity encoder p (notB x .||. y)
    Equiv x y -> do
      lit1 <- encodeFormulaWithPolarity encoder polarityBoth x
      lit2 <- encodeFormulaWithPolarity encoder polarityBoth y
      encodeFormulaWithPolarity encoder p $
        (Atom lit1 .=>. Atom lit2) .&&. (Atom lit2 .=>. Atom lit1)
    ITE c t e -> do
      c' <- encodeFormulaWithPolarity encoder polarityBoth c
      t' <- encodeFormulaWithPolarity encoder p t
      e' <- encodeFormulaWithPolarity encoder p e
      encodeITEWithPolarity encoder p c' t' 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 = encodeConjWithPolarity encoder 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 _ _ [l] =  return l
encodeConjWithPolarity encoder polarity ls = do
  usePB <- readMutVar (encUsePB encoder)
  table <- readMutVar (encConjTable encoder)
  let ls3 = IntSet.fromList ls
      ls2 = case Map.lookup IntSet.empty table of
              Nothing -> ls3
              Just (litTrue, _, _)
                | litFalse `IntSet.member` ls3 -> IntSet.singleton litFalse
                | otherwise -> IntSet.delete litTrue ls3
                where litFalse = SAT.litNot litTrue

  if IntSet.size ls2 == 1 then do
    return $ head $ IntSet.toList ls2
  else do
    let -- If F is monotone, F(A ∧ B) ⇔ ∃x. F(x) ∧ (x → A∧B)
        definePos :: SAT.Lit -> m ()
        definePos l = do
          case encAddPBAtLeast encoder of
            Just addPBAtLeast | usePB -> do
              -- ∀i.(l → li) ⇔ Σli >= n*l ⇔ Σli - n*l >= 0
              let n = IntSet.size ls2
              addPBAtLeast ((- fromIntegral n, l) : [(1,li) | li <- IntSet.toList ls2]) 0
            _ -> do
              forM_ (IntSet.toList ls2) $ \li -> do
                -- (l → li)  ⇔  (¬l ∨ li)
                SAT.addClause encoder [SAT.litNot l, 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 l = do
          -- ((l1 ∧ l2 ∧ … ∧ ln) → l)  ⇔  (¬l1 ∨ ¬l2 ∨ … ∨ ¬ln ∨ l)
          SAT.addClause encoder (l : map SAT.litNot (IntSet.toList ls2))
    encodeWithPolarityHelper encoder (encConjTable encoder) definePos defineNeg polarity 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 = encodeDisjWithPolarity encoder 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 _ _ [l] =  return l
encodeDisjWithPolarity encoder p ls = do
  -- ¬l ⇔ ¬(¬l1 ∧ … ∧ ¬ln) ⇔ (l1 ∨ … ∨ ln)
  l <- encodeConjWithPolarity encoder (negatePolarity p) [SAT.litNot li | li <- ls]
  return $ SAT.litNot 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 = encodeITEWithPolarity encoder 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 p c t e | c < 0 =
  encodeITEWithPolarity encoder p (- c) e t
encodeITEWithPolarity encoder polarity c t e = do
  let definePos :: SAT.Lit -> m ()
      definePos x = do
        -- x → ite(c,t,e)
        -- ⇔ x → (c∧t ∨ ¬c∧e)
        -- ⇔ (x∧c → t) ∧ (x∧¬c → e)
        -- ⇔ (¬x∨¬c∨t) ∧ (¬x∨c∨e)
        SAT.addClause encoder [-x, -c, t]
        SAT.addClause encoder [-x, c, e]
        SAT.addClause encoder [t, e, -x] -- redundant, but will increase the strength of unit propagation.

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

  encodeWithPolarityHelper encoder (encITETable encoder) definePos defineNeg polarity (c,t,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 = encodeXORWithPolarity encoder 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 polarity a b = do
  let defineNeg x = do
        -- (a ⊕ b) → x
        SAT.addClause encoder [a, -b, x]   -- ¬a ∧  b → x
        SAT.addClause encoder [-a, b, x]   --  a ∧ ¬b → x
      definePos x = do
        -- x → (a ⊕ b)
        SAT.addClause encoder [a, b, -x]   -- ¬a ∧ ¬b → ¬x
        SAT.addClause encoder [-a, -b, -x] --  a ∧  b → ¬x
  encodeWithPolarityHelper encoder (encXORTable encoder) definePos defineNeg polarity (a,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 = encodeFASumWithPolarity encoder 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 polarity a b c = do
  let defineNeg x = do
        -- FASum(a,b,c) → x
        SAT.addClause encoder [-a,-b,-c,x] --  a ∧  b ∧  c → x
        SAT.addClause encoder [-a,b,c,x]   --  a ∧ ¬b ∧ ¬c → x
        SAT.addClause encoder [a,-b,c,x]   -- ¬a ∧  b ∧ ¬c → x
        SAT.addClause encoder [a,b,-c,x]   -- ¬a ∧ ¬b ∧  c → x
      definePos x = do
        -- x → FASum(a,b,c)
        -- ⇔ ¬FASum(a,b,c) → ¬x
        SAT.addClause encoder [a,b,c,-x]   -- ¬a ∧ ¬b ∧ ¬c → ¬x
        SAT.addClause encoder [a,-b,-c,-x] -- ¬a ∧  b ∧  c → ¬x
        SAT.addClause encoder [-a,b,-c,-x] --  a ∧ ¬b ∧  c → ¬x
        SAT.addClause encoder [-a,-b,c,-x] --  a ∧  b ∧ ¬c → ¬x
  encodeWithPolarityHelper encoder (encFASumTable encoder) definePos defineNeg polarity (a,b,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 = encodeFACarryWithPolarity encoder 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 polarity a b c = do
  let defineNeg x = do
        -- FACarry(a,b,c) → x
        SAT.addClause encoder [-a,-b,x] -- a ∧ b → x
        SAT.addClause encoder [-a,-c,x] -- a ∧ c → x
        SAT.addClause encoder [-b,-c,x] -- b ∧ c → x
      definePos x = do
        -- x → FACarry(a,b,c)
        -- ⇔ ¬FACarry(a,b,c) → ¬x
        SAT.addClause encoder [a,b,-x]  --  ¬a ∧ ¬b → ¬x
        SAT.addClause encoder [a,c,-x]  --  ¬a ∧ ¬c → ¬x
        SAT.addClause encoder [b,c,-x]  --  ¬b ∧ ¬c → ¬x
  encodeWithPolarityHelper encoder (encFACarryTable encoder) definePos defineNeg polarity (a,b,c)


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


data Polarity
  = Polarity
  { polarityPosOccurs :: Bool
  , polarityNegOccurs :: Bool
  }
  deriving (Eq, Show)

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

polarityPos :: Polarity
polarityPos = Polarity True False

polarityNeg :: Polarity
polarityNeg = Polarity False True

polarityBoth :: Polarity
polarityBoth = Polarity True True

polarityNone :: Polarity
polarityNone = Polarity False False


1	{-# OPTIONS_GHC -Wall #-}
2	{-# OPTIONS_HADDOCK show-extensions #-}
3	{-# LANGUAGE ExistentialQuantification #-}
4	{-# LANGUAGE FlexibleInstances #-}
5	{-# LANGUAGE MultiParamTypeClasses #-}
6	{-# LANGUAGE ScopedTypeVariables #-}
7	-----------------------------------------------------------------------------
8	-- \|
9	-- Module : ToySolver.SAT.Encoder.Tseitin
10	-- Copyright : (c) Masahiro Sakai 2012
11	-- License : BSD-style
12	--
13	-- Maintainer : masahiro.sakai@gmail.com
14	-- Stability : provisional
15	-- Portability : non-portable
16	--
17	-- Tseitin encoding
18	--
19	-- TODO:
20	--
21	-- * reduce variables.
22	--
23	-- References:
24	--
25	-- * [Tse83] G. Tseitin. On the complexity of derivation in propositional
26	-- calculus. Automation of Reasoning: Classical Papers in Computational
27	-- Logic, 2:466-483, 1983. Springer-Verlag.
28	--
29	-- * [For60] R. Fortet. Application de l'algèbre de Boole en rechercheop
30	-- opérationelle. Revue Française de Recherche Opérationelle, 4:17-26,
31	-- 1960.
32	--
33	-- * [BM84a] E. Balas and J. B. Mazzola. Nonlinear 0-1 programming:
34	-- I. Linearization techniques. Mathematical Programming, 30(1):1-21,
35	-- 1984.
36	--
37	-- * [BM84b] E. Balas and J. B. Mazzola. Nonlinear 0-1 programming:
38	-- II. Dominance relations and algorithms. Mathematical Programming,
39	-- 30(1):22-45, 1984.
40	--
41	-- * [PG86] D. Plaisted and S. Greenbaum. A Structure-preserving
42	-- Clause Form Translation. In Journal on Symbolic Computation,
43	-- volume 2, 1986.
44	--
45	-- * [ES06] N. Eén and N. Sörensson. Translating Pseudo-Boolean
46	-- Constraints into SAT. JSAT 2:1–26, 2006.
47	--
48	-----------------------------------------------------------------------------
49	module ToySolver.SAT.Encoder.Tseitin
50	(
51	-- * The @Encoder@ type
52	Encoder
53	, newEncoder
54	, newEncoderWithPBLin
55	, setUsePB
56
57	-- * Polarity
58	, Polarity (..)
59	, negatePolarity
60	, polarityPos
61	, polarityNeg
62	, polarityBoth
63	, polarityNone
64
65	-- * Boolean formula type
66	, module ToySolver.SAT.Formula
67
68	-- * Encoding of boolean formulas
69	, addFormula
70	, encodeFormula
71	, encodeFormulaWithPolarity
72	, encodeConj
73	, encodeConjWithPolarity
74	, encodeDisj
75	, encodeDisjWithPolarity
76	, encodeITE
77	, encodeITEWithPolarity
78	, encodeXOR
79	, encodeXORWithPolarity
80	, encodeFASum
81	, encodeFASumWithPolarity
82	, encodeFACarry
83	, encodeFACarryWithPolarity
84
85	-- * Retrieving definitions
86	, getDefinitions
87	) where
88
89	import Control.Monad
90	import Control.Monad.Primitive
91	import Data.Primitive.MutVar
92	import qualified Data.IntMap.Lazy as IntMap
93	import Data.Map (Map)
94	import qualified Data.Map as Map
95	import qualified Data.IntSet as IntSet
96	import ToySolver.Data.Boolean
97	import ToySolver.SAT.Formula
98	import qualified ToySolver.SAT.Types as SAT
99
100	-- ------------------------------------------------------------------------
101
102	-- \| Encoder instance
103	data Encoder m =
104	forall a. SAT.AddClause m a =>
105	Encoder
106	{ encBase :: a	×
107	, encAddPBAtLeast :: Maybe (SAT.PBLinSum -> Integer -> m ())	1✔
108	, encUsePB :: !(MutVar (PrimState m) Bool)	1✔
109	, encConjTable :: !(MutVar (PrimState m) (Map SAT.LitSet (SAT.Var, Bool, Bool)))	1✔
110	, encITETable :: !(MutVar (PrimState m) (Map (SAT.Lit, SAT.Lit, SAT.Lit) (SAT.Var, Bool, Bool)))	1✔
111	, encXORTable :: !(MutVar (PrimState m) (Map (SAT.Lit, SAT.Lit) (SAT.Var, Bool, Bool)))	1✔
112	, encFASumTable :: !(MutVar (PrimState m) (Map (SAT.Lit, SAT.Lit, SAT.Lit) (SAT.Var, Bool, Bool)))	1✔
113	, encFACarryTable :: !(MutVar (PrimState m) (Map (SAT.Lit, SAT.Lit, SAT.Lit) (SAT.Var, Bool, Bool)))	1✔
114	}
115
116	instance Monad m => SAT.NewVar m (Encoder m) where
117	newVar Encoder{ encBase = a } = SAT.newVar a	1✔
118	newVars Encoder{ encBase = a } = SAT.newVars a	1✔
119	newVars_ Encoder{ encBase = a } = SAT.newVars_ a	×
120
121	instance Monad m => SAT.AddClause m (Encoder m) where
122	addClause Encoder{ encBase = a } = SAT.addClause a	1✔
123
124	-- \| Create a @Encoder@ instance.
125	-- If the encoder is built using this function, 'setUsePB' has no effect.
126	newEncoder :: PrimMonad m => SAT.AddClause m a => a -> m (Encoder m)
127	newEncoder solver = do	1✔
128	usePBRef <- newMutVar False	×
129	tableConj <- newMutVar Map.empty	1✔
130	tableITE <- newMutVar Map.empty	1✔
131	tableXOR <- newMutVar Map.empty	1✔
132	tableFASum <- newMutVar Map.empty	1✔
133	tableFACarry <- newMutVar Map.empty	1✔
134	return $	1✔
135	Encoder	1✔
136	{ encBase = solver	1✔
137	, encAddPBAtLeast = Nothing	1✔
138	, encUsePB = usePBRef	1✔
139	, encConjTable = tableConj	1✔
140	, encITETable = tableITE	1✔
141	, encXORTable = tableXOR	1✔
142	, encFASumTable = tableFASum	1✔
143	, encFACarryTable = tableFACarry	1✔
144	}
145
146	-- \| Create a @Encoder@ instance.
147	-- If the encoder is built using this function, 'setUsePB' has an effect.
148	newEncoderWithPBLin :: PrimMonad m => SAT.AddPBLin m a => a -> m (Encoder m)
149	newEncoderWithPBLin solver = do	1✔
150	usePBRef <- newMutVar False	×
151	tableConj <- newMutVar Map.empty	1✔
152	tableITE <- newMutVar Map.empty	1✔
153	tableXOR <- newMutVar Map.empty	1✔
154	tableFASum <- newMutVar Map.empty	1✔
155	tableFACarry <- newMutVar Map.empty	1✔
156	return $	1✔
157	Encoder	1✔
158	{ encBase = solver	1✔
159	, encAddPBAtLeast = Just (SAT.addPBAtLeast solver)	1✔
160	, encUsePB = usePBRef	1✔
161	, encConjTable = tableConj	1✔
162	, encITETable = tableITE	1✔
163	, encXORTable = tableXOR	1✔
164	, encFASumTable = tableFASum	1✔
165	, encFACarryTable = tableFACarry	1✔
166	}
167
168	-- \| Use /pseudo boolean constraints/ or use only /clauses/.
169	-- This option has an effect only when the encoder is built using 'newEncoderWithPBLin'.
170	setUsePB :: PrimMonad m => Encoder m -> Bool -> m ()
171	setUsePB encoder usePB = writeMutVar (encUsePB encoder) usePB	1✔
172
173	-- \| Assert a given formula to underlying SAT solver by using
174	-- Tseitin encoding.
175	addFormula :: PrimMonad m => Encoder m -> Formula -> m ()
176	addFormula encoder formula = do	1✔
177	case formula of	1✔
178	And xs -> mapM_ (addFormula encoder) xs	1✔
179	Equiv a b -> do	1✔
180	lit1 <- encodeFormula encoder a	1✔
181	lit2 <- encodeFormula encoder b	1✔
182	SAT.addClause encoder [SAT.litNot lit1, lit2] -- a→b	1✔
183	SAT.addClause encoder [SAT.litNot lit2, lit1] -- b→a	1✔
184	Not (Not a) -> addFormula encoder a	1✔
185	Not (Or xs) -> addFormula encoder (andB (map notB xs))	1✔
186	Not (Imply a b) -> addFormula encoder (a .&&. notB b)	1✔
187	Not (Equiv a b) -> do	1✔
188	lit1 <- encodeFormula encoder a	1✔
189	lit2 <- encodeFormula encoder b	1✔
190	SAT.addClause encoder [lit1, lit2] -- a ∨ b	1✔
191	SAT.addClause encoder [SAT.litNot lit1, SAT.litNot lit2] -- ¬a ∨ ¬b	1✔
192	ITE c t e -> do	1✔
193	c' <- encodeFormula encoder c	1✔
194	t' <- encodeFormulaWithPolarity encoder polarityPos t	1✔
195	e' <- encodeFormulaWithPolarity encoder polarityPos e	1✔
196	SAT.addClause encoder [-c', t'] -- c' → t'	1✔
197	SAT.addClause encoder [ c', e'] -- ¬c' → e'	1✔
198	_ -> do	1✔
199	c <- encodeToClause encoder formula	1✔
200	SAT.addClause encoder c	1✔
201
202	encodeToClause :: PrimMonad m => Encoder m -> Formula -> m SAT.Clause
203	encodeToClause encoder formula =	1✔
204	case formula of	1✔
205	And [x] -> encodeToClause encoder x	1✔
206	Or xs -> do	1✔
207	cs <- mapM (encodeToClause encoder) xs	1✔
208	return $ concat cs	1✔
209	Not (Not x) -> encodeToClause encoder x	×
210	Not (And xs) -> do	1✔
211	encodeToClause encoder (orB (map notB xs))	1✔
212	Imply a b -> do	1✔
213	encodeToClause encoder (notB a .\|\|. b)	1✔
214	_ -> do	1✔
215	l <- encodeFormulaWithPolarity encoder polarityPos formula	1✔
216	return [l]	1✔
217
218	encodeFormula :: PrimMonad m => Encoder m -> Formula -> m SAT.Lit
219	encodeFormula encoder = encodeFormulaWithPolarity encoder polarityBoth	1✔
220
221	encodeWithPolarityHelper
222	:: (PrimMonad m, Ord k)
223	=> Encoder m
224	-> MutVar (PrimState m) (Map k (SAT.Var, Bool, Bool))
225	-> (SAT.Lit -> m ()) -> (SAT.Lit -> m ())
226	-> Polarity
227	-> k
228	-> m SAT.Var
229	encodeWithPolarityHelper encoder tableRef definePos defineNeg (Polarity pos neg) k = do	1✔
230	table <- readMutVar tableRef	1✔
231	case Map.lookup k table of	1✔
232	Just (v, posDefined, negDefined) -> do	1✔
233	when (pos && not posDefined) $ definePos v	1✔
234	when (neg && not negDefined) $ defineNeg v	1✔
235	when (posDefined < pos \|\| negDefined < neg) $	1✔
236	modifyMutVar' tableRef (Map.insert k (v, (max posDefined pos), (max negDefined neg)))	1✔
237	return v	1✔
238	Nothing -> do	1✔
239	v <- SAT.newVar encoder	1✔
240	when pos $ definePos v	1✔
241	when neg $ defineNeg v	1✔
242	modifyMutVar' tableRef (Map.insert k (v, pos, neg))	1✔
243	return v	1✔
244
245
246	encodeFormulaWithPolarity :: PrimMonad m => Encoder m -> Polarity -> Formula -> m SAT.Lit
247	encodeFormulaWithPolarity encoder p formula = do	1✔
248	case formula of	1✔
249	Atom l -> return l	1✔
250	And xs -> encodeConjWithPolarity encoder p =<< mapM (encodeFormulaWithPolarity encoder p) xs	1✔
251	Or xs -> encodeDisjWithPolarity encoder p =<< mapM (encodeFormulaWithPolarity encoder p) xs	1✔
252	Not x -> liftM SAT.litNot $ encodeFormulaWithPolarity encoder (negatePolarity p) x	1✔
253	Imply x y -> do	1✔
254	encodeFormulaWithPolarity encoder p (notB x .\|\|. y)	1✔
255	Equiv x y -> do	1✔
256	lit1 <- encodeFormulaWithPolarity encoder polarityBoth x	1✔
257	lit2 <- encodeFormulaWithPolarity encoder polarityBoth y	1✔
258	encodeFormulaWithPolarity encoder p $	1✔
259	(Atom lit1 .=>. Atom lit2) .&&. (Atom lit2 .=>. Atom lit1)	1✔
260	ITE c t e -> do	1✔
261	c' <- encodeFormulaWithPolarity encoder polarityBoth c	1✔
262	t' <- encodeFormulaWithPolarity encoder p t	1✔
263	e' <- encodeFormulaWithPolarity encoder p e	1✔
264	encodeITEWithPolarity encoder p c' t' e'	1✔
265
266	-- \| Return an literal which is equivalent to a given conjunction.
267	--
268	-- @
269	-- encodeConj encoder = 'encodeConjWithPolarity' encoder 'polarityBoth'
270	-- @
271	encodeConj :: PrimMonad m => Encoder m -> [SAT.Lit] -> m SAT.Lit
272	encodeConj encoder = encodeConjWithPolarity encoder polarityBoth	1✔
273
274	-- \| Return an literal which is equivalent to a given conjunction which occurs only in specified polarity.
275	encodeConjWithPolarity :: forall m. PrimMonad m => Encoder m -> Polarity -> [SAT.Lit] -> m SAT.Lit
276	encodeConjWithPolarity _ _ [l] = return l	1✔
277	encodeConjWithPolarity encoder polarity ls = do	1✔
278	usePB <- readMutVar (encUsePB encoder)	1✔
279	table <- readMutVar (encConjTable encoder)	1✔
280	let ls3 = IntSet.fromList ls	1✔
281	ls2 = case Map.lookup IntSet.empty table of	1✔
282	Nothing -> ls3	1✔
283	Just (litTrue, _, _)
284	\| litFalse `IntSet.member` ls3 -> IntSet.singleton litFalse	1✔
285	\| otherwise -> IntSet.delete litTrue ls3	×
286	where litFalse = SAT.litNot litTrue	1✔
287
288	if IntSet.size ls2 == 1 then do	1✔
289	return $ head $ IntSet.toList ls2	1✔
290	else do	1✔
291	let -- If F is monotone, F(A ∧ B) ⇔ ∃x. F(x) ∧ (x → A∧B)
292	definePos :: SAT.Lit -> m ()
293	definePos l = do	1✔
294	case encAddPBAtLeast encoder of	1✔
295	Just addPBAtLeast \| usePB -> do	1✔
296	-- ∀i.(l → li) ⇔ Σli >= nl ⇔ Σli - nl >= 0
297	let n = IntSet.size ls2	1✔
298	addPBAtLeast ((- fromIntegral n, l) : [(1,li) \| li <- IntSet.toList ls2]) 0	1✔
299	_ -> do	1✔
300	forM_ (IntSet.toList ls2) $ \li -> do	1✔
301	-- (l → li) ⇔ (¬l ∨ li)
302	SAT.addClause encoder [SAT.litNot l, li]	1✔
303	-- If F is anti-monotone, F(A ∧ B) ⇔ ∃x. F(x) ∧ (x ← A∧B) ⇔ ∃x. F(x) ∧ (x∨¬A∨¬B).
304	defineNeg :: SAT.Lit -> m ()
305	defineNeg l = do	1✔
306	-- ((l1 ∧ l2 ∧ … ∧ ln) → l) ⇔ (¬l1 ∨ ¬l2 ∨ … ∨ ¬ln ∨ l)
307	SAT.addClause encoder (l : map SAT.litNot (IntSet.toList ls2))	1✔
308	encodeWithPolarityHelper encoder (encConjTable encoder) definePos defineNeg polarity ls2	1✔
309
310	-- \| Return an literal which is equivalent to a given disjunction.
311	--
312	-- @
313	-- encodeDisj encoder = 'encodeDisjWithPolarity' encoder 'polarityBoth'
314	-- @
315	encodeDisj :: PrimMonad m => Encoder m -> [SAT.Lit] -> m SAT.Lit
316	encodeDisj encoder = encodeDisjWithPolarity encoder polarityBoth	1✔
317
318	-- \| Return an literal which is equivalent to a given disjunction which occurs only in specified polarity.
319	encodeDisjWithPolarity :: PrimMonad m => Encoder m -> Polarity -> [SAT.Lit] -> m SAT.Lit
320	encodeDisjWithPolarity _ _ [l] = return l	1✔
321	encodeDisjWithPolarity encoder p ls = do	1✔
322	-- ¬l ⇔ ¬(¬l1 ∧ … ∧ ¬ln) ⇔ (l1 ∨ … ∨ ln)
323	l <- encodeConjWithPolarity encoder (negatePolarity p) [SAT.litNot li \| li <- ls]	1✔
324	return $ SAT.litNot l	1✔
325
326	-- \| Return an literal which is equivalent to a given if-then-else.
327	--
328	-- @
329	-- encodeITE encoder = 'encodeITEWithPolarity' encoder 'polarityBoth'
330	-- @
331	encodeITE :: PrimMonad m => Encoder m -> SAT.Lit -> SAT.Lit -> SAT.Lit -> m SAT.Lit
332	encodeITE encoder = encodeITEWithPolarity encoder polarityBoth	1✔
333
334	-- \| Return an literal which is equivalent to a given if-then-else which occurs only in specified polarity.
335	encodeITEWithPolarity :: forall m. PrimMonad m => Encoder m -> Polarity -> SAT.Lit -> SAT.Lit -> SAT.Lit -> m SAT.Lit
336	encodeITEWithPolarity encoder p c t e \| c < 0 =	1✔
337	encodeITEWithPolarity encoder p (- c) e t	1✔
338	encodeITEWithPolarity encoder polarity c t e = do	1✔
339	let definePos :: SAT.Lit -> m ()
340	definePos x = do	1✔
341	-- x → ite(c,t,e)
342	-- ⇔ x → (c∧t ∨ ¬c∧e)
343	-- ⇔ (x∧c → t) ∧ (x∧¬c → e)
344	-- ⇔ (¬x∨¬c∨t) ∧ (¬x∨c∨e)
345	SAT.addClause encoder [-x, -c, t]	1✔
346	SAT.addClause encoder [-x, c, e]	1✔
347	SAT.addClause encoder [t, e, -x] -- redundant, but will increase the strength of unit propagation.	1✔
348
349	defineNeg :: SAT.Lit -> m ()
350	defineNeg x = do	1✔
351	-- ite(c,t,e) → x
352	-- ⇔ (c∧t ∨ ¬c∧e) → x
353	-- ⇔ (c∧t → x) ∨ (¬c∧e →x)
354	-- ⇔ (¬c∨¬t∨x) ∨ (c∧¬e∨x)
355	SAT.addClause encoder [-c, -t, x]	1✔
356	SAT.addClause encoder [c, -e, x]	1✔
357	SAT.addClause encoder [-t, -e, x] -- redundant, but will increase the strength of unit propagation.	1✔
358
359	encodeWithPolarityHelper encoder (encITETable encoder) definePos defineNeg polarity (c,t,e)	1✔
360
361	-- \| Return an literal which is equivalent to an XOR of given two literals.
362	--
363	-- @
364	-- encodeXOR encoder = 'encodeXORWithPolarity' encoder 'polarityBoth'
365	-- @
366	encodeXOR :: PrimMonad m => Encoder m -> SAT.Lit -> SAT.Lit -> m SAT.Lit
367	encodeXOR encoder = encodeXORWithPolarity encoder polarityBoth	1✔
368
369	-- \| Return an literal which is equivalent to an XOR of given two literals which occurs only in specified polarity.
370	encodeXORWithPolarity :: forall m. PrimMonad m => Encoder m -> Polarity -> SAT.Lit -> SAT.Lit -> m SAT.Lit
371	encodeXORWithPolarity encoder polarity a b = do	1✔
372	let defineNeg x = do	1✔
373	-- (a ⊕ b) → x
374	SAT.addClause encoder [a, -b, x] -- ¬a ∧ b → x	1✔
375	SAT.addClause encoder [-a, b, x] -- a ∧ ¬b → x	1✔
376	definePos x = do	1✔
377	-- x → (a ⊕ b)
378	SAT.addClause encoder [a, b, -x] -- ¬a ∧ ¬b → ¬x	1✔
379	SAT.addClause encoder [-a, -b, -x] -- a ∧ b → ¬x	1✔
380	encodeWithPolarityHelper encoder (encXORTable encoder) definePos defineNeg polarity (a,b)	1✔
381
382	-- \| Return an "sum"-pin of a full-adder.
383	--
384	-- @
385	-- encodeFASum encoder = 'encodeFASumWithPolarity' encoder 'polarityBoth'
386	-- @
387	encodeFASum :: forall m. PrimMonad m => Encoder m -> SAT.Lit -> SAT.Lit -> SAT.Lit -> m SAT.Lit
388	encodeFASum encoder = encodeFASumWithPolarity encoder polarityBoth	1✔
389
390	-- \| Return an "sum"-pin of a full-adder which occurs only in specified polarity.
391	encodeFASumWithPolarity :: forall m. PrimMonad m => Encoder m -> Polarity -> SAT.Lit -> SAT.Lit -> SAT.Lit -> m SAT.Lit
392	encodeFASumWithPolarity encoder polarity a b c = do	1✔
393	let defineNeg x = do	1✔
394	-- FASum(a,b,c) → x
395	SAT.addClause encoder [-a,-b,-c,x] -- a ∧ b ∧ c → x	1✔
396	SAT.addClause encoder [-a,b,c,x] -- a ∧ ¬b ∧ ¬c → x	1✔
397	SAT.addClause encoder [a,-b,c,x] -- ¬a ∧ b ∧ ¬c → x	1✔
398	SAT.addClause encoder [a,b,-c,x] -- ¬a ∧ ¬b ∧ c → x	1✔
399	definePos x = do	1✔
400	-- x → FASum(a,b,c)
401	-- ⇔ ¬FASum(a,b,c) → ¬x
402	SAT.addClause encoder [a,b,c,-x] -- ¬a ∧ ¬b ∧ ¬c → ¬x	1✔
403	SAT.addClause encoder [a,-b,-c,-x] -- ¬a ∧ b ∧ c → ¬x	1✔
404	SAT.addClause encoder [-a,b,-c,-x] -- a ∧ ¬b ∧ c → ¬x	1✔
405	SAT.addClause encoder [-a,-b,c,-x] -- a ∧ b ∧ ¬c → ¬x	1✔
406	encodeWithPolarityHelper encoder (encFASumTable encoder) definePos defineNeg polarity (a,b,c)	1✔
407
408	-- \| Return an "carry"-pin of a full-adder.
409	--
410	-- @
411	-- encodeFACarry encoder = 'encodeFACarryWithPolarity' encoder 'polarityBoth'
412	-- @
413	encodeFACarry :: forall m. PrimMonad m => Encoder m -> SAT.Lit -> SAT.Lit -> SAT.Lit -> m SAT.Lit
414	encodeFACarry encoder = encodeFACarryWithPolarity encoder polarityBoth	1✔
415
416	-- \| Return an "carry"-pin of a full-adder which occurs only in specified polarity.
417	encodeFACarryWithPolarity :: forall m. PrimMonad m => Encoder m -> Polarity -> SAT.Lit -> SAT.Lit -> SAT.Lit -> m SAT.Lit
418	encodeFACarryWithPolarity encoder polarity a b c = do	1✔
419	let defineNeg x = do	1✔
420	-- FACarry(a,b,c) → x
421	SAT.addClause encoder [-a,-b,x] -- a ∧ b → x	1✔
422	SAT.addClause encoder [-a,-c,x] -- a ∧ c → x	1✔
423	SAT.addClause encoder [-b,-c,x] -- b ∧ c → x	1✔
424	definePos x = do	1✔
425	-- x → FACarry(a,b,c)
426	-- ⇔ ¬FACarry(a,b,c) → ¬x
427	SAT.addClause encoder [a,b,-x] -- ¬a ∧ ¬b → ¬x	1✔
428	SAT.addClause encoder [a,c,-x] -- ¬a ∧ ¬c → ¬x	1✔
429	SAT.addClause encoder [b,c,-x] -- ¬b ∧ ¬c → ¬x	1✔
430	encodeWithPolarityHelper encoder (encFACarryTable encoder) definePos defineNeg polarity (a,b,c)	1✔
431
432
433	getDefinitions :: PrimMonad m => Encoder m -> m (SAT.VarMap Formula)
434	getDefinitions encoder = do	1✔
435	tableConj <- readMutVar (encConjTable encoder)	1✔
436	tableITE <- readMutVar (encITETable encoder)	1✔
437	tableXOR <- readMutVar (encXORTable encoder)	1✔
438	tableFASum <- readMutVar (encFASumTable encoder)	1✔
439	tableFACarry <- readMutVar (encFACarryTable encoder)	1✔
440	let atom l	1✔
441	\| l < 0 = Not (Atom (- l))	1✔
442	\| otherwise = Atom l	×
443	m1 = IntMap.fromList [(v, andB [atom l1 \| l1 <- IntSet.toList ls]) \| (ls, (v, _, _)) <- Map.toList tableConj]	1✔
444	m2 = IntMap.fromList [(v, ite (atom c) (atom t) (atom e)) \| ((c,t,e), (v, _, _)) <- Map.toList tableITE]	×
445	m3 = IntMap.fromList [(v, (atom a .\|\|. atom b) .&&. (atom (-a) .\|\|. atom (-b))) \| ((a,b), (v, _, _)) <- Map.toList tableXOR]	1✔
446	m4 = IntMap.fromList	1✔
447	[ (v, orB [andB [atom l \| l <- ls] \| ls <- [[a,b,c],[a,-b,-c],[-a,b,-c],[-a,-b,c]]])	1✔
448	\| ((a,b,c), (v, _, _)) <- Map.toList tableFASum	1✔
449	]
450	m5 = IntMap.fromList	1✔
451	[ (v, orB [andB [atom l \| l <- ls] \| ls <- [[a,b],[a,c],[b,c]]])	1✔
452	\| ((a,b,c), (v, _, _)) <- Map.toList tableFACarry	1✔
453	]
454	return $ IntMap.unions [m1, m2, m3, m4, m5]	1✔
455
456
457	data Polarity
458	= Polarity
459	{ polarityPosOccurs :: Bool	1✔
460	, polarityNegOccurs :: Bool	1✔
461	}
462	deriving (Eq, Show)	×
463
464	negatePolarity :: Polarity -> Polarity
465	negatePolarity (Polarity pos neg) = (Polarity neg pos)	1✔
466
467	polarityPos :: Polarity
468	polarityPos = Polarity True False	1✔
469
470	polarityNeg :: Polarity
471	polarityNeg = Polarity False True	1✔
472
473	polarityBoth :: Polarity
474	polarityBoth = Polarity True True	1✔
475
476	polarityNone :: Polarity
477	polarityNone = Polarity False False	1✔
478

msakai / toysolver / 767

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous