consider polarity in ToySolver.SAT.Encoder.Cardinality.Internal.Naive

msakai · Aug 10, 2022 · 8759d5d · 8759d5d
1 parent b172dae
commit 8759d5d
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 9 deletions.
diff --git a/src/ToySolver/SAT/Encoder/Cardinality.hs b/src/ToySolver/SAT/Encoder/Cardinality.hs
@@ -108,9 +108,9 @@ encodeAtLeast :: PrimMonad m => Encoder m -> SAT.AtLeast -> m SAT.Lit
 encodeAtLeast enc = encodeAtLeastWithPolarity enc polarityBoth
 
 encodeAtLeastWithPolarity :: PrimMonad m => Encoder m -> Polarity -> SAT.AtLeast -> m SAT.Lit
-encodeAtLeastWithPolarity (Encoder base@(Totalizer.Encoder tseitin _) strategy) _polarity =
+encodeAtLeastWithPolarity (Encoder base@(Totalizer.Encoder tseitin _) strategy) polarity =
   case strategy of
-    Naive -> encodeAtLeastNaive tseitin
+    Naive -> encodeAtLeastWithPolarityNaive tseitin polarity
     ParallelCounter -> encodeAtLeastParallelCounter tseitin
     SequentialCounter -> \(lhs,rhs) -> BDD.encodePBLinAtLeastBDD tseitin ([(1,l) | l <- lhs], fromIntegral rhs)
     Totalizer -> Totalizer.encodeAtLeast base
diff --git a/src/ToySolver/SAT/Encoder/Cardinality/Internal/Naive.hs b/src/ToySolver/SAT/Encoder/Cardinality/Internal/Naive.hs
@@ -12,12 +12,13 @@
 -----------------------------------------------------------------------------
 module ToySolver.SAT.Encoder.Cardinality.Internal.Naive
   ( addAtLeastNaive
-  , encodeAtLeastNaive
+  , encodeAtLeastWithPolarityNaive
   ) where
 
 import Control.Monad.Primitive
 import qualified ToySolver.SAT.Types as SAT
 import qualified ToySolver.SAT.Encoder.Tseitin as Tseitin
+import ToySolver.SAT.Encoder.Tseitin (Polarity ())
 
 addAtLeastNaive :: PrimMonad m => Tseitin.Encoder m -> SAT.AtLeast -> m ()
 addAtLeastNaive enc (lhs,rhs) = do
@@ -27,15 +28,14 @@ addAtLeastNaive enc (lhs,rhs) = do
   else do
     mapM_ (SAT.addClause enc) (comb (n - rhs + 1) lhs)
 
--- TODO: consider polarity
-encodeAtLeastNaive :: PrimMonad m => Tseitin.Encoder m -> SAT.AtLeast -> m SAT.Lit
-encodeAtLeastNaive enc (lhs,rhs) = do
+encodeAtLeastWithPolarityNaive :: PrimMonad m => Tseitin.Encoder m -> Polarity -> SAT.AtLeast -> m SAT.Lit
+encodeAtLeastWithPolarityNaive enc polarity (lhs,rhs) = do
   let n = length lhs
   if n < rhs then do
-    Tseitin.encodeDisj enc []
+    Tseitin.encodeDisjWithPolarity enc polarity []
   else do
-    ls <- mapM (Tseitin.encodeDisj enc) (comb (n - rhs + 1) lhs)
-    Tseitin.encodeConj enc ls
+    ls <- mapM (Tseitin.encodeDisjWithPolarity enc polarity) (comb (n - rhs + 1) lhs)
+    Tseitin.encodeConjWithPolarity enc polarity ls
 
 comb :: Int -> [a] -> [[a]]
 comb 0 _ = [[]]