msakai / toysolver / 513

Committed 24 Nov 2024 08:49AM UTC coverage: 68.675% (-1.0%) from 69.681%

Build # 513

Build Type

push

github

Committed by

web-flow

Commit Message

Merge 496ed4263 into 46e1509c4

Run Details

5 of 121 new or added lines in 7 files covered. (4.13%)

105 existing lines in 14 files now uncovered.

9745 of 14190 relevant lines covered (68.68%)

0.69 hits per line

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

87.16

/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 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.Var, 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 m1 = [(v, andB [Atom l1 | l1 <- IntSet.toList ls]) | (ls, (v, _, _)) <- Map.toList tableConj]
      m2 = [(v, ite (Atom c) (Atom t) (Atom e)) | ((c,t,e), (v, _, _)) <- Map.toList tableITE]
      m3 = [(v, (Atom a .||. Atom b) .&&. (Atom (-a) .||. Atom (-b))) | ((a,b), (v, _, _)) <- Map.toList tableXOR]
      m4 = [(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 = [(v, orB [andB [Atom l | l <- ls] | ls <- [[a,b],[a,c],[b,c]]])
             | ((a,b,c), (v, _, _)) <- Map.toList tableFACarry]
  return $ concat [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 Data.Map (Map)
93	import qualified Data.Map as Map
94	import qualified Data.IntSet as IntSet
95	import ToySolver.Data.Boolean
96	import ToySolver.SAT.Formula
97	import qualified ToySolver.SAT.Types as SAT
98
99	-- ------------------------------------------------------------------------
100
101	-- \| Encoder instance
102	data Encoder m =
103	forall a. SAT.AddClause m a =>
104	Encoder
105	{ encBase :: a	×
106	, encAddPBAtLeast :: Maybe (SAT.PBLinSum -> Integer -> m ())	1✔
107	, encUsePB :: !(MutVar (PrimState m) Bool)	1✔
108	, encConjTable :: !(MutVar (PrimState m) (Map SAT.LitSet (SAT.Var, Bool, Bool)))	1✔
109	, encITETable :: !(MutVar (PrimState m) (Map (SAT.Lit, SAT.Lit, SAT.Lit) (SAT.Var, Bool, Bool)))	1✔
110	, encXORTable :: !(MutVar (PrimState m) (Map (SAT.Lit, SAT.Lit) (SAT.Var, Bool, Bool)))	1✔
111	, encFASumTable :: !(MutVar (PrimState m) (Map (SAT.Lit, SAT.Lit, SAT.Lit) (SAT.Var, Bool, Bool)))	1✔
112	, encFACarryTable :: !(MutVar (PrimState m) (Map (SAT.Lit, SAT.Lit, SAT.Lit) (SAT.Var, Bool, Bool)))	1✔
113	}
114
115	instance Monad m => SAT.NewVar m (Encoder m) where
116	newVar Encoder{ encBase = a } = SAT.newVar a	1✔
117	newVars Encoder{ encBase = a } = SAT.newVars a	1✔
118	newVars_ Encoder{ encBase = a } = SAT.newVars_ a	×
119
120	instance Monad m => SAT.AddClause m (Encoder m) where
121	addClause Encoder{ encBase = a } = SAT.addClause a	1✔
122
123	-- \| Create a @Encoder@ instance.
124	-- If the encoder is built using this function, 'setUsePB' has no effect.
125	newEncoder :: PrimMonad m => SAT.AddClause m a => a -> m (Encoder m)
126	newEncoder solver = do	1✔
127	usePBRef <- newMutVar False	×
128	tableConj <- newMutVar Map.empty	1✔
129	tableITE <- newMutVar Map.empty	1✔
130	tableXOR <- newMutVar Map.empty	1✔
131	tableFASum <- newMutVar Map.empty	1✔
132	tableFACarry <- newMutVar Map.empty	1✔
133	return $	1✔
134	Encoder	1✔
135	{ encBase = solver	1✔
136	, encAddPBAtLeast = Nothing	1✔
137	, encUsePB = usePBRef	1✔
138	, encConjTable = tableConj	1✔
139	, encITETable = tableITE	1✔
140	, encXORTable = tableXOR	1✔
141	, encFASumTable = tableFASum	1✔
142	, encFACarryTable = tableFACarry	1✔
143	}
144
145	-- \| Create a @Encoder@ instance.
146	-- If the encoder is built using this function, 'setUsePB' has an effect.
147	newEncoderWithPBLin :: PrimMonad m => SAT.AddPBLin m a => a -> m (Encoder m)
148	newEncoderWithPBLin solver = do	×
149	usePBRef <- newMutVar False	×
150	tableConj <- newMutVar Map.empty	×
151	tableITE <- newMutVar Map.empty	×
152	tableXOR <- newMutVar Map.empty	×
153	tableFASum <- newMutVar Map.empty	×
154	tableFACarry <- newMutVar Map.empty	×
155	return $	×
156	Encoder	×
157	{ encBase = solver	×
158	, encAddPBAtLeast = Just (SAT.addPBAtLeast solver)	×
159	, encUsePB = usePBRef	×
160	, encConjTable = tableConj	×
161	, encITETable = tableITE	×
162	, encXORTable = tableXOR	×
163	, encFASumTable = tableFASum	×
164	, encFACarryTable = tableFACarry	×
165	}
166
167	-- \| Use /pseudo boolean constraints/ or use only /clauses/.
168	-- This option has an effect only when the encoder is built using 'newEncoderWithPBLin'.
169	setUsePB :: PrimMonad m => Encoder m -> Bool -> m ()
170	setUsePB encoder usePB = writeMutVar (encUsePB encoder) usePB	×
171
172	-- \| Assert a given formula to underlying SAT solver by using
173	-- Tseitin encoding.
174	addFormula :: PrimMonad m => Encoder m -> Formula -> m ()
175	addFormula encoder formula = do	1✔
176	case formula of	1✔
177	And xs -> mapM_ (addFormula encoder) xs	1✔
178	Equiv a b -> do	1✔
179	lit1 <- encodeFormula encoder a	1✔
180	lit2 <- encodeFormula encoder b	1✔
181	SAT.addClause encoder [SAT.litNot lit1, lit2] -- a→b	1✔
182	SAT.addClause encoder [SAT.litNot lit2, lit1] -- b→a	1✔
UNCOV 183	Not (Not a) -> addFormula encoder a	×
184	Not (Or xs) -> addFormula encoder (andB (map notB xs))	1✔
185	Not (Imply a b) -> addFormula encoder (a .&&. notB b)	1✔
186	Not (Equiv a b) -> do	1✔
187	lit1 <- encodeFormula encoder a	1✔
188	lit2 <- encodeFormula encoder b	1✔
189	SAT.addClause encoder [lit1, lit2] -- a ∨ b	1✔
190	SAT.addClause encoder [SAT.litNot lit1, SAT.litNot lit2] -- ¬a ∨ ¬b	1✔
191	ITE c t e -> do	1✔
192	c' <- encodeFormula encoder c	1✔
193	t' <- encodeFormulaWithPolarity encoder polarityPos t	1✔
194	e' <- encodeFormulaWithPolarity encoder polarityPos e	1✔
195	SAT.addClause encoder [-c', t'] -- c' → t'	1✔
196	SAT.addClause encoder [ c', e'] -- ¬c' → e'	1✔
197	_ -> do	1✔
198	c <- encodeToClause encoder formula	1✔
199	SAT.addClause encoder c	1✔
200
201	encodeToClause :: PrimMonad m => Encoder m -> Formula -> m SAT.Clause
202	encodeToClause encoder formula =	1✔
203	case formula of	1✔
204	And [x] -> encodeToClause encoder x	1✔
205	Or xs -> do	1✔
206	cs <- mapM (encodeToClause encoder) xs	1✔
207	return $ concat cs	1✔
208	Not (Not x) -> encodeToClause encoder x	1✔
209	Not (And xs) -> do	1✔
210	encodeToClause encoder (orB (map notB xs))	1✔
211	Imply a b -> do	1✔
212	encodeToClause encoder (notB a .\|\|. b)	1✔
213	_ -> do	1✔
214	l <- encodeFormulaWithPolarity encoder polarityPos formula	1✔
215	return [l]	1✔
216
217	encodeFormula :: PrimMonad m => Encoder m -> Formula -> m SAT.Lit
218	encodeFormula encoder = encodeFormulaWithPolarity encoder polarityBoth	1✔
219
220	encodeWithPolarityHelper
221	:: (PrimMonad m, Ord k)
222	=> Encoder m
223	-> MutVar (PrimState m) (Map k (SAT.Var, Bool, Bool))
224	-> (SAT.Lit -> m ()) -> (SAT.Lit -> m ())
225	-> Polarity
226	-> k
227	-> m SAT.Var
228	encodeWithPolarityHelper encoder tableRef definePos defineNeg (Polarity pos neg) k = do	1✔
229	table <- readMutVar tableRef	1✔
230	case Map.lookup k table of	1✔
231	Just (v, posDefined, negDefined) -> do	1✔
232	when (pos && not posDefined) $ definePos v	1✔
233	when (neg && not negDefined) $ defineNeg v	1✔
234	when (posDefined < pos \|\| negDefined < neg) $	1✔
235	modifyMutVar' tableRef (Map.insert k (v, (max posDefined pos), (max negDefined neg)))	1✔
236	return v	1✔
237	Nothing -> do	1✔
238	v <- SAT.newVar encoder	1✔
239	when pos $ definePos v	1✔
240	when neg $ defineNeg v	1✔
241	modifyMutVar' tableRef (Map.insert k (v, pos, neg))	1✔
242	return v	1✔
243
244
245	encodeFormulaWithPolarity :: PrimMonad m => Encoder m -> Polarity -> Formula -> m SAT.Lit
246	encodeFormulaWithPolarity encoder p formula = do	1✔
247	case formula of	1✔
248	Atom l -> return l	1✔
249	And xs -> encodeConjWithPolarity encoder p =<< mapM (encodeFormulaWithPolarity encoder p) xs	1✔
250	Or xs -> encodeDisjWithPolarity encoder p =<< mapM (encodeFormulaWithPolarity encoder p) xs	1✔
251	Not x -> liftM SAT.litNot $ encodeFormulaWithPolarity encoder (negatePolarity p) x	1✔
252	Imply x y -> do	1✔
253	encodeFormulaWithPolarity encoder p (notB x .\|\|. y)	1✔
254	Equiv x y -> do	1✔
255	lit1 <- encodeFormulaWithPolarity encoder polarityBoth x	1✔
256	lit2 <- encodeFormulaWithPolarity encoder polarityBoth y	1✔
257	encodeFormulaWithPolarity encoder p $	1✔
258	(Atom lit1 .=>. Atom lit2) .&&. (Atom lit2 .=>. Atom lit1)	1✔
259	ITE c t e -> do	1✔
260	c' <- encodeFormulaWithPolarity encoder polarityBoth c	1✔
261	t' <- encodeFormulaWithPolarity encoder p t	1✔
262	e' <- encodeFormulaWithPolarity encoder p e	1✔
263	encodeITEWithPolarity encoder p c' t' e'	1✔
264
265	-- \| Return an literal which is equivalent to a given conjunction.
266	--
267	-- @
268	-- encodeConj encoder = 'encodeConjWithPolarity' encoder 'polarityBoth'
269	-- @
270	encodeConj :: PrimMonad m => Encoder m -> [SAT.Lit] -> m SAT.Lit
271	encodeConj encoder = encodeConjWithPolarity encoder polarityBoth	1✔
272
273	-- \| Return an literal which is equivalent to a given conjunction which occurs only in specified polarity.
274	encodeConjWithPolarity :: forall m. PrimMonad m => Encoder m -> Polarity -> [SAT.Lit] -> m SAT.Lit
275	encodeConjWithPolarity _ _ [l] = return l	1✔
276	encodeConjWithPolarity encoder polarity ls = do	1✔
277	usePB <- readMutVar (encUsePB encoder)	1✔
278	table <- readMutVar (encConjTable encoder)	1✔
279	let ls3 = IntSet.fromList ls	1✔
280	ls2 = case Map.lookup IntSet.empty table of	1✔
281	Nothing -> ls3	1✔
282	Just (litTrue, _, _)
283	\| litFalse `IntSet.member` ls3 -> IntSet.singleton litFalse	1✔
284	\| otherwise -> IntSet.delete litTrue ls3	×
285	where litFalse = SAT.litNot litTrue	1✔
286
287	if IntSet.size ls2 == 1 then do	1✔
288	return $ head $ IntSet.toList ls2	1✔
289	else do	1✔
290	let -- If F is monotone, F(A ∧ B) ⇔ ∃x. F(x) ∧ (x → A∧B)
291	definePos :: SAT.Lit -> m ()
292	definePos l = do	1✔
293	case encAddPBAtLeast encoder of	1✔
294	Just addPBAtLeast \| usePB -> do	×
295	-- ∀i.(l → li) ⇔ Σli >= nl ⇔ Σli - nl >= 0
296	let n = IntSet.size ls2	×
297	addPBAtLeast ((- fromIntegral n, l) : [(1,li) \| li <- IntSet.toList ls2]) 0	×
298	_ -> do	1✔
299	forM_ (IntSet.toList ls2) $ \li -> do	1✔
300	-- (l → li) ⇔ (¬l ∨ li)
301	SAT.addClause encoder [SAT.litNot l, li]	1✔
302	-- If F is anti-monotone, F(A ∧ B) ⇔ ∃x. F(x) ∧ (x ← A∧B) ⇔ ∃x. F(x) ∧ (x∨¬A∨¬B).
303	defineNeg :: SAT.Lit -> m ()
304	defineNeg l = do	1✔
305	-- ((l1 ∧ l2 ∧ … ∧ ln) → l) ⇔ (¬l1 ∨ ¬l2 ∨ … ∨ ¬ln ∨ l)
306	SAT.addClause encoder (l : map SAT.litNot (IntSet.toList ls2))	1✔
307	encodeWithPolarityHelper encoder (encConjTable encoder) definePos defineNeg polarity ls2	1✔
308
309	-- \| Return an literal which is equivalent to a given disjunction.
310	--
311	-- @
312	-- encodeDisj encoder = 'encodeDisjWithPolarity' encoder 'polarityBoth'
313	-- @
314	encodeDisj :: PrimMonad m => Encoder m -> [SAT.Lit] -> m SAT.Lit
315	encodeDisj encoder = encodeDisjWithPolarity encoder polarityBoth	1✔
316
317	-- \| Return an literal which is equivalent to a given disjunction which occurs only in specified polarity.
318	encodeDisjWithPolarity :: PrimMonad m => Encoder m -> Polarity -> [SAT.Lit] -> m SAT.Lit
319	encodeDisjWithPolarity _ _ [l] = return l	1✔
320	encodeDisjWithPolarity encoder p ls = do	1✔
321	-- ¬l ⇔ ¬(¬l1 ∧ … ∧ ¬ln) ⇔ (l1 ∨ … ∨ ln)
322	l <- encodeConjWithPolarity encoder (negatePolarity p) [SAT.litNot li \| li <- ls]	1✔
323	return $ SAT.litNot l	1✔
324
325	-- \| Return an literal which is equivalent to a given if-then-else.
326	--
327	-- @
328	-- encodeITE encoder = 'encodeITEWithPolarity' encoder 'polarityBoth'
329	-- @
330	encodeITE :: PrimMonad m => Encoder m -> SAT.Lit -> SAT.Lit -> SAT.Lit -> m SAT.Lit
331	encodeITE encoder = encodeITEWithPolarity encoder polarityBoth	1✔
332
333	-- \| Return an literal which is equivalent to a given if-then-else which occurs only in specified polarity.
334	encodeITEWithPolarity :: forall m. PrimMonad m => Encoder m -> Polarity -> SAT.Lit -> SAT.Lit -> SAT.Lit -> m SAT.Lit
335	encodeITEWithPolarity encoder p c t e \| c < 0 =	1✔
336	encodeITEWithPolarity encoder p (- c) e t	1✔
337	encodeITEWithPolarity encoder polarity c t e = do	1✔
338	let definePos :: SAT.Lit -> m ()
339	definePos x = do	1✔
340	-- x → ite(c,t,e)
341	-- ⇔ x → (c∧t ∨ ¬c∧e)
342	-- ⇔ (x∧c → t) ∧ (x∧¬c → e)
343	-- ⇔ (¬x∨¬c∨t) ∧ (¬x∨c∨e)
344	SAT.addClause encoder [-x, -c, t]	1✔
345	SAT.addClause encoder [-x, c, e]	1✔
346	SAT.addClause encoder [t, e, -x] -- redundant, but will increase the strength of unit propagation.	1✔
347
348	defineNeg :: SAT.Lit -> m ()
349	defineNeg x = do	1✔
350	-- ite(c,t,e) → x
351	-- ⇔ (c∧t ∨ ¬c∧e) → x
352	-- ⇔ (c∧t → x) ∨ (¬c∧e →x)
353	-- ⇔ (¬c∨¬t∨x) ∨ (c∧¬e∨x)
354	SAT.addClause encoder [-c, -t, x]	1✔
355	SAT.addClause encoder [c, -e, x]	1✔
356	SAT.addClause encoder [-t, -e, x] -- redundant, but will increase the strength of unit propagation.	1✔
357
358	encodeWithPolarityHelper encoder (encITETable encoder) definePos defineNeg polarity (c,t,e)	1✔
359
360	-- \| Return an literal which is equivalent to an XOR of given two literals.
361	--
362	-- @
363	-- encodeXOR encoder = 'encodeXORWithPolarity' encoder 'polarityBoth'
364	-- @
365	encodeXOR :: PrimMonad m => Encoder m -> SAT.Lit -> SAT.Lit -> m SAT.Lit
366	encodeXOR encoder = encodeXORWithPolarity encoder polarityBoth	1✔
367
368	-- \| Return an literal which is equivalent to an XOR of given two literals which occurs only in specified polarity.
369	encodeXORWithPolarity :: forall m. PrimMonad m => Encoder m -> Polarity -> SAT.Lit -> SAT.Lit -> m SAT.Lit
370	encodeXORWithPolarity encoder polarity a b = do	1✔
371	let defineNeg x = do	1✔
372	-- (a ⊕ b) → x
373	SAT.addClause encoder [a, -b, x] -- ¬a ∧ b → x	1✔
374	SAT.addClause encoder [-a, b, x] -- a ∧ ¬b → x	1✔
375	definePos x = do	1✔
376	-- x → (a ⊕ b)
377	SAT.addClause encoder [a, b, -x] -- ¬a ∧ ¬b → ¬x	1✔
378	SAT.addClause encoder [-a, -b, -x] -- a ∧ b → ¬x	1✔
379	encodeWithPolarityHelper encoder (encXORTable encoder) definePos defineNeg polarity (a,b)	1✔
380
381	-- \| Return an "sum"-pin of a full-adder.
382	--
383	-- @
384	-- encodeFASum encoder = 'encodeFASumWithPolarity' encoder 'polarityBoth'
385	-- @
386	encodeFASum :: forall m. PrimMonad m => Encoder m -> SAT.Lit -> SAT.Lit -> SAT.Lit -> m SAT.Lit
387	encodeFASum encoder = encodeFASumWithPolarity encoder polarityBoth	1✔
388
389	-- \| Return an "sum"-pin of a full-adder which occurs only in specified polarity.
390	encodeFASumWithPolarity :: forall m. PrimMonad m => Encoder m -> Polarity -> SAT.Lit -> SAT.Lit -> SAT.Lit -> m SAT.Lit
391	encodeFASumWithPolarity encoder polarity a b c = do	1✔
392	let defineNeg x = do	1✔
393	-- FASum(a,b,c) → x
394	SAT.addClause encoder [-a,-b,-c,x] -- a ∧ b ∧ c → x	1✔
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	definePos x = do	1✔
399	-- x → FASum(a,b,c)
400	-- ⇔ ¬FASum(a,b,c) → ¬x
401	SAT.addClause encoder [a,b,c,-x] -- ¬a ∧ ¬b ∧ ¬c → ¬x	1✔
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	encodeWithPolarityHelper encoder (encFASumTable encoder) definePos defineNeg polarity (a,b,c)	1✔
406
407	-- \| Return an "carry"-pin of a full-adder.
408	--
409	-- @
410	-- encodeFACarry encoder = 'encodeFACarryWithPolarity' encoder 'polarityBoth'
411	-- @
412	encodeFACarry :: forall m. PrimMonad m => Encoder m -> SAT.Lit -> SAT.Lit -> SAT.Lit -> m SAT.Lit
413	encodeFACarry encoder = encodeFACarryWithPolarity encoder polarityBoth	1✔
414
415	-- \| Return an "carry"-pin of a full-adder which occurs only in specified polarity.
416	encodeFACarryWithPolarity :: forall m. PrimMonad m => Encoder m -> Polarity -> SAT.Lit -> SAT.Lit -> SAT.Lit -> m SAT.Lit
417	encodeFACarryWithPolarity encoder polarity a b c = do	1✔
418	let defineNeg x = do	1✔
419	-- FACarry(a,b,c) → x
420	SAT.addClause encoder [-a,-b,x] -- a ∧ b → x	1✔
421	SAT.addClause encoder [-a,-c,x] -- a ∧ c → x	1✔
422	SAT.addClause encoder [-b,-c,x] -- b ∧ c → x	1✔
423	definePos x = do	1✔
424	-- x → FACarry(a,b,c)
425	-- ⇔ ¬FACarry(a,b,c) → ¬x
426	SAT.addClause encoder [a,b,-x] -- ¬a ∧ ¬b → ¬x	1✔
427	SAT.addClause encoder [a,c,-x] -- ¬a ∧ ¬c → ¬x	1✔
428	SAT.addClause encoder [b,c,-x] -- ¬b ∧ ¬c → ¬x	1✔
429	encodeWithPolarityHelper encoder (encFACarryTable encoder) definePos defineNeg polarity (a,b,c)	1✔
430
431
432	getDefinitions :: PrimMonad m => Encoder m -> m [(SAT.Var, Formula)]
433	getDefinitions encoder = do	1✔
434	tableConj <- readMutVar (encConjTable encoder)	1✔
435	tableITE <- readMutVar (encITETable encoder)	1✔
436	tableXOR <- readMutVar (encXORTable encoder)	1✔
437	tableFASum <- readMutVar (encFASumTable encoder)	1✔
438	tableFACarry <- readMutVar (encFACarryTable encoder)	1✔
439	let m1 = [(v, andB [Atom l1 \| l1 <- IntSet.toList ls]) \| (ls, (v, _, _)) <- Map.toList tableConj]	1✔
440	m2 = [(v, ite (Atom c) (Atom t) (Atom e)) \| ((c,t,e), (v, _, _)) <- Map.toList tableITE]	×
441	m3 = [(v, (Atom a .\|\|. Atom b) .&&. (Atom (-a) .\|\|. Atom (-b))) \| ((a,b), (v, _, _)) <- Map.toList tableXOR]	1✔
442	m4 = [(v, orB [andB [Atom l \| l <- ls] \| ls <- [[a,b,c],[a,-b,-c],[-a,b,-c],[-a,-b,c]]])	1✔
443	\| ((a,b,c), (v, _, _)) <- Map.toList tableFASum]	1✔
444	m5 = [(v, orB [andB [Atom l \| l <- ls] \| ls <- [[a,b],[a,c],[b,c]]])	1✔
445	\| ((a,b,c), (v, _, _)) <- Map.toList tableFACarry]	1✔
446	return $ concat [m1, m2, m3, m4, m5]	1✔
447
448
449	data Polarity
450	= Polarity
451	{ polarityPosOccurs :: Bool	1✔
452	, polarityNegOccurs :: Bool	1✔
453	}
454	deriving (Eq, Show)	×
455
456	negatePolarity :: Polarity -> Polarity
457	negatePolarity (Polarity pos neg) = (Polarity neg pos)	1✔
458
459	polarityPos :: Polarity
460	polarityPos = Polarity True False	1✔
461
462	polarityNeg :: Polarity
463	polarityNeg = Polarity False True	1✔
464
465	polarityBoth :: Polarity
466	polarityBoth = Polarity True True	1✔
467
468	polarityNone :: Polarity
469	polarityNone = Polarity False False	1✔
470

msakai / toysolver / 513

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