-- Copyright (C) 2016 Peter Selinger.
--
-- This file is free software and may be distributed under the terms
-- of the MIT license. Please see the file LICENSE for details.

-- | This module extends the SAT solver to arbitrary boolean formulas
-- (not necessarily in conjunctive normal form). This is done by the
-- standard trick of translating each boolean formula to a CNF,
-- preserving satisfiability and the number of solutions. The
-- translation is carefully done in such a way that the size of the
-- CNF is linear in the size of the formula.

module SAT.MiniSat.Formula where

import SAT.MiniSat.Variable
import SAT.MiniSat.Literals

import Control.Monad.Trans.State
import Control.Monad
import qualified Data.Map as Map
import Data.Map (Map)
import Data.Maybe
import Prelude hiding (all)

-- ----------------------------------------------------------------------
-- * Boolean formulas

-- | The type of boolean formulas. It is parametric over a set of
-- variables /v/. We provide the usual boolean operators, including
-- implications and exclusive or. For convenience, we also provide the
-- list quantifiers 'All', 'Some', 'None', 'ExactlyOne', and
-- 'AtMostOne', as well as a general 'Let' operator that can be
-- used to reduce the size of repetitive formulas.

data Formula v =
  Var v                       -- ^ A variable.
  | Yes                       -- ^ The formula /true/.
  | No                        -- ^ The formula /false/.
  | Not (Formula v)           -- ^ Negation.
  | Formula v :&&: Formula v  -- ^ Conjunction.
  | Formula v :||: Formula v  -- ^ Disjunction.
  | Formula v :++: Formula v  -- ^ Exclusive or.
  | Formula v :->: Formula v  -- ^ Implication.
  | Formula v :<->: Formula v -- ^ If and only if.
  | All [Formula v]           -- ^ All are true.
  | Some [Formula v]          -- ^ At least one is true.
  | None [Formula v]          -- ^ None are true.
  | ExactlyOne [Formula v]    -- ^ Exactly one is true.
  | AtMostOne [Formula v]     -- ^ At most one is true.
  | Let (Formula v) (Formula v -> Formula v)
        -- ^ 'Let' /a/ /f/ is the formula \"let /x/=/a/ in /fx/\",
        -- which permits the subexpression /a/ to be re-used. It
        -- is logically equivalent to /fa/, but typically smaller.
  | Bound Integer             -- ^ For internal use only.

infixr 6 :&&:
infixr 5 :||:
infixr 4 :++:
infixr 2 :->:
infix  1 :<->:

instance (Eq v) => Eq (Formula v) where
  Formula v
a == :: Formula v -> Formula v -> Bool
== Formula v
b = Integer -> Formula v -> ExFormula v
forall v. Integer -> Formula v -> ExFormula v
exformula Integer
0 Formula v
a ExFormula v -> ExFormula v -> Bool
forall a. Eq a => a -> a -> Bool
== Integer -> Formula v -> ExFormula v
forall v. Integer -> Formula v -> ExFormula v
exformula Integer
0 Formula v
b

instance (Ord v) => Ord (Formula v) where
  compare :: Formula v -> Formula v -> Ordering
compare Formula v
a Formula v
b = ExFormula v -> ExFormula v -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Integer -> Formula v -> ExFormula v
forall v. Integer -> Formula v -> ExFormula v
exformula Integer
0 Formula v
a) (Integer -> Formula v -> ExFormula v
forall v. Integer -> Formula v -> ExFormula v
exformula Integer
0 Formula v
b)

instance (Show v) => Show (Formula v) where
  showsPrec :: Int -> Formula v -> ShowS
showsPrec Int
d Formula v
a = Int -> ExFormula v -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d (Integer -> Formula v -> ExFormula v
forall v. Integer -> Formula v -> ExFormula v
exformula Integer
0 Formula v
a)

-- ----------------------------------------------------------------------
-- * Explicit formulas

-- | Same as 'Formula', except it uses explicit bound variables. This is
-- only used to define 'Eq', 'Ord', and 'Show' instances for
-- 'Formula'.
data ExFormula v =
  ExVar v                             -- ^ A variable.
  | ExTrue                            -- ^ The formula /true/.
  | ExFalse                           -- ^ The formula /false/.
  | ExNot (ExFormula v)               -- ^ Negation.
  | ExAnd (ExFormula v) (ExFormula v) -- ^ Conjunction.
  | ExOr (ExFormula v) (ExFormula v)  -- ^ Disjunction.
  | ExXOr (ExFormula v) (ExFormula v) -- ^ Exclusive or.
  | ExImp (ExFormula v) (ExFormula v) -- ^ Implication.
  | ExIff (ExFormula v) (ExFormula v) -- ^ If and only if.
  | ExAll [ExFormula v]               -- ^ All are true.
  | ExSome [ExFormula v]              -- ^ At least one is true.
  | ExNone [ExFormula v]              -- ^ None are true.
  | ExExactlyOne [ExFormula v]        -- ^ Exactly one is true.
  | ExAtMostOne [ExFormula v]         -- ^ At most one is true.
  | ExLet Integer (ExFormula v) (ExFormula v) -- ^ Let.
  | ExBound Integer                   -- ^ Bound variable.
  deriving (ExFormula v -> ExFormula v -> Bool
(ExFormula v -> ExFormula v -> Bool)
-> (ExFormula v -> ExFormula v -> Bool) -> Eq (ExFormula v)
forall v. Eq v => ExFormula v -> ExFormula v -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall v. Eq v => ExFormula v -> ExFormula v -> Bool
== :: ExFormula v -> ExFormula v -> Bool
$c/= :: forall v. Eq v => ExFormula v -> ExFormula v -> Bool
/= :: ExFormula v -> ExFormula v -> Bool
Eq, Eq (ExFormula v)
Eq (ExFormula v) =>
(ExFormula v -> ExFormula v -> Ordering)
-> (ExFormula v -> ExFormula v -> Bool)
-> (ExFormula v -> ExFormula v -> Bool)
-> (ExFormula v -> ExFormula v -> Bool)
-> (ExFormula v -> ExFormula v -> Bool)
-> (ExFormula v -> ExFormula v -> ExFormula v)
-> (ExFormula v -> ExFormula v -> ExFormula v)
-> Ord (ExFormula v)
ExFormula v -> ExFormula v -> Bool
ExFormula v -> ExFormula v -> Ordering
ExFormula v -> ExFormula v -> ExFormula v
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall v. Ord v => Eq (ExFormula v)
forall v. Ord v => ExFormula v -> ExFormula v -> Bool
forall v. Ord v => ExFormula v -> ExFormula v -> Ordering
forall v. Ord v => ExFormula v -> ExFormula v -> ExFormula v
$ccompare :: forall v. Ord v => ExFormula v -> ExFormula v -> Ordering
compare :: ExFormula v -> ExFormula v -> Ordering
$c< :: forall v. Ord v => ExFormula v -> ExFormula v -> Bool
< :: ExFormula v -> ExFormula v -> Bool
$c<= :: forall v. Ord v => ExFormula v -> ExFormula v -> Bool
<= :: ExFormula v -> ExFormula v -> Bool
$c> :: forall v. Ord v => ExFormula v -> ExFormula v -> Bool
> :: ExFormula v -> ExFormula v -> Bool
$c>= :: forall v. Ord v => ExFormula v -> ExFormula v -> Bool
>= :: ExFormula v -> ExFormula v -> Bool
$cmax :: forall v. Ord v => ExFormula v -> ExFormula v -> ExFormula v
max :: ExFormula v -> ExFormula v -> ExFormula v
$cmin :: forall v. Ord v => ExFormula v -> ExFormula v -> ExFormula v
min :: ExFormula v -> ExFormula v -> ExFormula v
Ord)

-- | Convert a 'Formula' to an 'ExFormula'. The first argument is the
-- current nesting depth of let binders.
exformula :: Integer -> Formula v -> ExFormula v
exformula :: forall v. Integer -> Formula v -> ExFormula v
exformula Integer
i (Var v
v) = v -> ExFormula v
forall v. v -> ExFormula v
ExVar v
v
exformula Integer
i Formula v
Yes = ExFormula v
forall v. ExFormula v
ExTrue
exformula Integer
i Formula v
No = ExFormula v
forall v. ExFormula v
ExFalse
exformula Integer
i (Not Formula v
a) = ExFormula v -> ExFormula v
forall v. ExFormula v -> ExFormula v
ExNot (Integer -> Formula v -> ExFormula v
forall v. Integer -> Formula v -> ExFormula v
exformula Integer
i Formula v
a)
exformula Integer
i (Formula v
a :&&: Formula v
b) = ExFormula v -> ExFormula v -> ExFormula v
forall v. ExFormula v -> ExFormula v -> ExFormula v
ExAnd (Integer -> Formula v -> ExFormula v
forall v. Integer -> Formula v -> ExFormula v
exformula Integer
i Formula v
a) (Integer -> Formula v -> ExFormula v
forall v. Integer -> Formula v -> ExFormula v
exformula Integer
i Formula v
b)
exformula Integer
i (Formula v
a :||: Formula v
b) = ExFormula v -> ExFormula v -> ExFormula v
forall v. ExFormula v -> ExFormula v -> ExFormula v
ExOr (Integer -> Formula v -> ExFormula v
forall v. Integer -> Formula v -> ExFormula v
exformula Integer
i Formula v
a) (Integer -> Formula v -> ExFormula v
forall v. Integer -> Formula v -> ExFormula v
exformula Integer
i Formula v
b)
exformula Integer
i (Formula v
a :++: Formula v
b) = ExFormula v -> ExFormula v -> ExFormula v
forall v. ExFormula v -> ExFormula v -> ExFormula v
ExXOr (Integer -> Formula v -> ExFormula v
forall v. Integer -> Formula v -> ExFormula v
exformula Integer
i Formula v
a) (Integer -> Formula v -> ExFormula v
forall v. Integer -> Formula v -> ExFormula v
exformula Integer
i Formula v
b)
exformula Integer
i (Formula v
a :->: Formula v
b) = ExFormula v -> ExFormula v -> ExFormula v
forall v. ExFormula v -> ExFormula v -> ExFormula v
ExImp (Integer -> Formula v -> ExFormula v
forall v. Integer -> Formula v -> ExFormula v
exformula Integer
i Formula v
a) (Integer -> Formula v -> ExFormula v
forall v. Integer -> Formula v -> ExFormula v
exformula Integer
i Formula v
b)
exformula Integer
i (Formula v
a :<->: Formula v
b) = ExFormula v -> ExFormula v -> ExFormula v
forall v. ExFormula v -> ExFormula v -> ExFormula v
ExIff (Integer -> Formula v -> ExFormula v
forall v. Integer -> Formula v -> ExFormula v
exformula Integer
i Formula v
a) (Integer -> Formula v -> ExFormula v
forall v. Integer -> Formula v -> ExFormula v
exformula Integer
i Formula v
b)
exformula Integer
i (All [Formula v]
vs) = [ExFormula v] -> ExFormula v
forall v. [ExFormula v] -> ExFormula v
ExAll [Integer -> Formula v -> ExFormula v
forall v. Integer -> Formula v -> ExFormula v
exformula Integer
i Formula v
v | Formula v
v <- [Formula v]
vs]
exformula Integer
i (Some [Formula v]
vs) = [ExFormula v] -> ExFormula v
forall v. [ExFormula v] -> ExFormula v
ExSome [Integer -> Formula v -> ExFormula v
forall v. Integer -> Formula v -> ExFormula v
exformula Integer
i Formula v
v | Formula v
v <- [Formula v]
vs]
exformula Integer
i (None [Formula v]
vs) = [ExFormula v] -> ExFormula v
forall v. [ExFormula v] -> ExFormula v
ExNone [Integer -> Formula v -> ExFormula v
forall v. Integer -> Formula v -> ExFormula v
exformula Integer
i Formula v
v | Formula v
v <- [Formula v]
vs]
exformula Integer
i (ExactlyOne [Formula v]
vs) = [ExFormula v] -> ExFormula v
forall v. [ExFormula v] -> ExFormula v
ExExactlyOne [Integer -> Formula v -> ExFormula v
forall v. Integer -> Formula v -> ExFormula v
exformula Integer
i Formula v
v | Formula v
v <- [Formula v]
vs]
exformula Integer
i (AtMostOne [Formula v]
vs) = [ExFormula v] -> ExFormula v
forall v. [ExFormula v] -> ExFormula v
ExAtMostOne [Integer -> Formula v -> ExFormula v
forall v. Integer -> Formula v -> ExFormula v
exformula Integer
i Formula v
v | Formula v
v <- [Formula v]
vs]
exformula Integer
i (Let Formula v
a Formula v -> Formula v
f) = Integer -> ExFormula v -> ExFormula v -> ExFormula v
forall v. Integer -> ExFormula v -> ExFormula v -> ExFormula v
ExLet Integer
i (Integer -> Formula v -> ExFormula v
forall v. Integer -> Formula v -> ExFormula v
exformula Integer
i Formula v
a) (Integer -> Formula v -> ExFormula v
forall v. Integer -> Formula v -> ExFormula v
exformula (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) (Formula v -> Formula v
f (Integer -> Formula v
forall v. Integer -> Formula v
Bound Integer
i)))
exformula Integer
i (Bound Integer
x)
  | Integer
0 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
x Bool -> Bool -> Bool
&& Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
i = Integer -> ExFormula v
forall v. Integer -> ExFormula v
ExBound Integer
x
  | Bool
otherwise = String -> ExFormula v
forall a. HasCallStack => String -> a
error String
"MiniSat.Formula: 'Bound' is for internal use only"

-- | Names for bound variables.
variables :: [String]
variables :: [String]
variables = [String]
vs [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n | Integer
n <- [Integer
1..], String
v <- [String]
vs ]
  where
    vs :: [String]
vs = [String
"x", String
"y", String
"z", String
"u", String
"v", String
"w", String
"r", String
"s", String
"t"]

-- | Convert an integer to a bound variable name.
showBound :: Integer -> ShowS
showBound :: Integer -> ShowS
showBound Integer
i = String -> ShowS
showString ([String]
variables [String] -> Int -> String
forall a. HasCallStack => [a] -> Int -> a
!! (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
i))

-- | The 'Show' instance of 'ExFormula' actually shows the corresponding
-- 'Formula'. We omit parentheses between associative identical
-- operators, but show some additional parentheses between different
-- operators for clarity.
instance (Show v) => Show (ExFormula v) where
  showsPrec :: Int -> ExFormula v -> ShowS
showsPrec Int
d (ExVar v
v) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    String -> ShowS
showString String
"Var " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> v -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
d v
v
  showsPrec Int
d ExFormula v
ExTrue = String -> ShowS
showString String
"Yes"
  showsPrec Int
d ExFormula v
ExFalse = String -> ShowS
showString String
"No"
  showsPrec Int
d (ExNot ExFormula v
a) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    String -> ShowS
showString String
"Not " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ExFormula v -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 ExFormula v
a
  showsPrec Int
d (ExAnd ExFormula v
a ExFormula v
b) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
6 Bool -> Bool -> Bool
|| Int
d Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
4 Bool -> Bool -> Bool
|| Int
d Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
5) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    Int -> ExFormula v -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
6 ExFormula v
a ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" :&&: " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ExFormula v -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
6 ExFormula v
b
  showsPrec Int
d (ExOr ExFormula v
a ExFormula v
b) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
5 Bool -> Bool -> Bool
|| Int
d Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
4) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    Int -> ExFormula v -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
5 ExFormula v
a ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" :||: " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ExFormula v -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
5 ExFormula v
b
  showsPrec Int
d (ExXOr ExFormula v
a ExFormula v
b) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
4) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    Int -> ExFormula v -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
4 ExFormula v
a ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" :++: " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ExFormula v -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
4 ExFormula v
b
  showsPrec Int
d (ExImp ExFormula v
a ExFormula v
b) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
2) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    Int -> ExFormula v -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
3 ExFormula v
a ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" :->: " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ExFormula v -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
2 ExFormula v
b
  showsPrec Int
d (ExIff ExFormula v
a ExFormula v
b) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    Int -> ExFormula v -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
3 ExFormula v
a ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" :<->: " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ExFormula v -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
3 ExFormula v
b
  showsPrec Int
d (ExAll [ExFormula v]
as) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    String -> ShowS
showString String
"All " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [ExFormula v] -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 [ExFormula v]
as
  showsPrec Int
d (ExSome [ExFormula v]
as) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    String -> ShowS
showString String
"Some " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [ExFormula v] -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 [ExFormula v]
as
  showsPrec Int
d (ExNone [ExFormula v]
as) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    String -> ShowS
showString String
"None " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [ExFormula v] -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 [ExFormula v]
as
  showsPrec Int
d (ExExactlyOne [ExFormula v]
as) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    String -> ShowS
showString String
"ExactlyOne " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [ExFormula v] -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 [ExFormula v]
as
  showsPrec Int
d (ExAtMostOne [ExFormula v]
as) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    String -> ShowS
showString String
"AtMostOne " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [ExFormula v] -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 [ExFormula v]
as
  showsPrec Int
d (ExLet Integer
i ExFormula v
a ExFormula v
b) = Bool -> ShowS -> ShowS
showParen (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
    String -> ShowS
showString String
"Let " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ExFormula v -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 ExFormula v
a ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" (\\"
    ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> ShowS
showBound Integer
i ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
" -> " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> ExFormula v -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
0 ExFormula v
b ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
")"
  showsPrec Int
d (ExBound Integer
i) = Integer -> ShowS
showBound Integer
i

-- ----------------------------------------------------------------------
-- * Desugaring

-- | A version of 'Let' that binds a list of variables.
let_list :: [Formula v] -> ([Formula v] -> Formula v) -> Formula v
let_list :: forall v. [Formula v] -> ([Formula v] -> Formula v) -> Formula v
let_list [] [Formula v] -> Formula v
f = [Formula v] -> Formula v
f []
let_list (Formula v
a:[Formula v]
as) [Formula v] -> Formula v
f = Formula v -> (Formula v -> Formula v) -> Formula v
forall v. Formula v -> (Formula v -> Formula v) -> Formula v
Let Formula v
a (\Formula v
x -> [Formula v] -> ([Formula v] -> Formula v) -> Formula v
forall v. [Formula v] -> ([Formula v] -> Formula v) -> Formula v
let_list [Formula v]
as (\[Formula v]
xs -> [Formula v] -> Formula v
f (Formula v
xFormula v -> [Formula v] -> [Formula v]
forall a. a -> [a] -> [a]
:[Formula v]
xs)))

-- | Implementation of 'All'.
all :: [Formula v] -> Formula v
all :: forall v. [Formula v] -> Formula v
all [Formula v]
vs = (Formula v -> Formula v -> Formula v)
-> Formula v -> [Formula v] -> Formula v
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Formula v -> Formula v -> Formula v
forall v. Formula v -> Formula v -> Formula v
(:&&:) Formula v
forall v. Formula v
Yes [Formula v]
vs

-- | Implementation of 'Some'.
some :: [Formula v] -> Formula v
some :: forall v. [Formula v] -> Formula v
some [Formula v]
vs = (Formula v -> Formula v -> Formula v)
-> Formula v -> [Formula v] -> Formula v
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Formula v -> Formula v -> Formula v
forall v. Formula v -> Formula v -> Formula v
(:||:) Formula v
forall v. Formula v
No [Formula v]
vs

-- | Implementation of 'None'.
none :: [Formula v] -> Formula v
none :: forall v. [Formula v] -> Formula v
none [Formula v]
vs = Formula v -> Formula v
forall v. Formula v -> Formula v
Not ([Formula v] -> Formula v
forall v. [Formula v] -> Formula v
some [Formula v]
vs)

-- | Implementation of 'AtMostOne'. Note that this translation is linear.
-- Without 'Let', the size of the translated formula would be /O/(/n/^2).
atMostOne :: [Formula v] -> Formula v
atMostOne :: forall v. [Formula v] -> Formula v
atMostOne [] = Formula v
forall v. Formula v
Yes
atMostOne [Formula v
a] = Formula v
forall v. Formula v
Yes
atMostOne (Formula v
a1:Formula v
a2:[Formula v]
as) =
  Formula v -> (Formula v -> Formula v) -> Formula v
forall v. Formula v -> (Formula v -> Formula v) -> Formula v
Let Formula v
a1 (\Formula v
x1 ->
  Formula v -> (Formula v -> Formula v) -> Formula v
forall v. Formula v -> (Formula v -> Formula v) -> Formula v
Let Formula v
a2 (\Formula v
x2 ->
    Formula v -> Formula v
forall v. Formula v -> Formula v
Not (Formula v
x1 Formula v -> Formula v -> Formula v
forall v. Formula v -> Formula v -> Formula v
:&&: Formula v
x2) Formula v -> Formula v -> Formula v
forall v. Formula v -> Formula v -> Formula v
:&&: [Formula v] -> Formula v
forall v. [Formula v] -> Formula v
atMostOne ((Formula v
x1 Formula v -> Formula v -> Formula v
forall v. Formula v -> Formula v -> Formula v
:||: Formula v
x2) Formula v -> [Formula v] -> [Formula v]
forall a. a -> [a] -> [a]
: [Formula v]
as)))

-- | Implementation of 'ExactlyOne'.
exactlyOne :: [Formula v] -> Formula v
exactlyOne :: forall v. [Formula v] -> Formula v
exactlyOne [Formula v]
as = [Formula v] -> ([Formula v] -> Formula v) -> Formula v
forall v. [Formula v] -> ([Formula v] -> Formula v) -> Formula v
let_list [Formula v]
as (\[Formula v]
xs -> [Formula v] -> Formula v
forall v. [Formula v] -> Formula v
some [Formula v]
xs Formula v -> Formula v -> Formula v
forall v. Formula v -> Formula v -> Formula v
:&&: [Formula v] -> Formula v
forall v. [Formula v] -> Formula v
atMostOne [Formula v]
xs)

-- ----------------------------------------------------------------------
-- * Reduced boolean formulas

-- | A reduced boolean formula doesn't contain the constants \"true\" or
-- \"false\", nor the connectives \"and\", \"implies\", or \"iff\",
-- nor list quantifiers. We use reduced formulas as an intermediate
-- representation between boolean formulas and De Morgan normal forms.
-- The primary purpose of this is to get rid of the constants \"true\"
-- and \"false\" in absorbing positions (i.e., \"/a/ or true\", \"/b/
-- and false\").
data RFormula v =
  RFVar v                           -- ^ A variable.
  | RFBound Integer                 -- ^ A bound variable.
  | RFNot (RFormula v)              -- ^ Negation.
  | RFOr (RFormula v) (RFormula v)  -- ^ Disjunction.
  | RFXOr (RFormula v) (RFormula v) -- ^ Exclusive or.
  | RFLet Integer (RFormula v) (RFormula v) -- ^ Let /x/ = /a/ in /b/.
    deriving (Int -> RFormula v -> ShowS
[RFormula v] -> ShowS
RFormula v -> String
(Int -> RFormula v -> ShowS)
-> (RFormula v -> String)
-> ([RFormula v] -> ShowS)
-> Show (RFormula v)
forall v. Show v => Int -> RFormula v -> ShowS
forall v. Show v => [RFormula v] -> ShowS
forall v. Show v => RFormula v -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall v. Show v => Int -> RFormula v -> ShowS
showsPrec :: Int -> RFormula v -> ShowS
$cshow :: forall v. Show v => RFormula v -> String
show :: RFormula v -> String
$cshowList :: forall v. Show v => [RFormula v] -> ShowS
showList :: [RFormula v] -> ShowS
Show)

-- | Translate a boolean formula to reduced form, or one of the
-- constants 'True' or 'False'. The integer argument is the current
-- nesting depth of let binders, and is used to number local bound
-- variables.
rformula :: Integer -> Formula v -> Either Bool (RFormula v)
rformula :: forall v. Integer -> Formula v -> Either Bool (RFormula v)
rformula Integer
i (Var v
v) = RFormula v -> Either Bool (RFormula v)
forall a b. b -> Either a b
Right (v -> RFormula v
forall v. v -> RFormula v
RFVar v
v)
rformula Integer
i Formula v
Yes = Bool -> Either Bool (RFormula v)
forall a b. a -> Either a b
Left Bool
True
rformula Integer
i Formula v
No = Bool -> Either Bool (RFormula v)
forall a b. a -> Either a b
Left Bool
False
rformula Integer
i (Not Formula v
a) =
  case Integer -> Formula v -> Either Bool (RFormula v)
forall v. Integer -> Formula v -> Either Bool (RFormula v)
rformula Integer
i Formula v
a of
    Left Bool
x -> Bool -> Either Bool (RFormula v)
forall a b. a -> Either a b
Left (Bool -> Bool
not Bool
x)
    Right RFormula v
a'' -> RFormula v -> Either Bool (RFormula v)
forall a b. b -> Either a b
Right (RFormula v -> RFormula v
forall v. RFormula v -> RFormula v
RFNot RFormula v
a'')
rformula Integer
i (Formula v
a :||: Formula v
b) =
  case (Integer -> Formula v -> Either Bool (RFormula v)
forall v. Integer -> Formula v -> Either Bool (RFormula v)
rformula Integer
i Formula v
a, Integer -> Formula v -> Either Bool (RFormula v)
forall v. Integer -> Formula v -> Either Bool (RFormula v)
rformula Integer
i Formula v
b) of
    (Left Bool
True, Either Bool (RFormula v)
b'') -> Bool -> Either Bool (RFormula v)
forall a b. a -> Either a b
Left Bool
True
    (Left Bool
False, Either Bool (RFormula v)
b'') -> Either Bool (RFormula v)
b''
    (Either Bool (RFormula v)
a'', Left Bool
True) -> Bool -> Either Bool (RFormula v)
forall a b. a -> Either a b
Left Bool
True
    (Either Bool (RFormula v)
a'', Left Bool
False) -> Either Bool (RFormula v)
a''
    (Right RFormula v
a'', Right RFormula v
b'') -> RFormula v -> Either Bool (RFormula v)
forall a b. b -> Either a b
Right (RFormula v -> RFormula v -> RFormula v
forall v. RFormula v -> RFormula v -> RFormula v
RFOr RFormula v
a'' RFormula v
b'')
rformula Integer
i (Formula v
a :++: Formula v
b) =
  case (Integer -> Formula v -> Either Bool (RFormula v)
forall v. Integer -> Formula v -> Either Bool (RFormula v)
rformula Integer
i Formula v
a, Integer -> Formula v -> Either Bool (RFormula v)
forall v. Integer -> Formula v -> Either Bool (RFormula v)
rformula Integer
i Formula v
b) of
   (Left Bool
x, Left Bool
y) -> Bool -> Either Bool (RFormula v)
forall a b. a -> Either a b
Left (Bool
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool
y)
   (Left Bool
True, Right RFormula v
b'') -> RFormula v -> Either Bool (RFormula v)
forall a b. b -> Either a b
Right (RFormula v -> RFormula v
forall v. RFormula v -> RFormula v
RFNot RFormula v
b'')
   (Left Bool
False, Right RFormula v
b'') -> RFormula v -> Either Bool (RFormula v)
forall a b. b -> Either a b
Right RFormula v
b''
   (Right RFormula v
a'', Left Bool
True) -> RFormula v -> Either Bool (RFormula v)
forall a b. b -> Either a b
Right (RFormula v -> RFormula v
forall v. RFormula v -> RFormula v
RFNot RFormula v
a'')
   (Right RFormula v
a'', Left Bool
False) -> RFormula v -> Either Bool (RFormula v)
forall a b. b -> Either a b
Right RFormula v
a''
   (Right RFormula v
a'', Right RFormula v
b'') -> RFormula v -> Either Bool (RFormula v)
forall a b. b -> Either a b
Right (RFormula v -> RFormula v -> RFormula v
forall v. RFormula v -> RFormula v -> RFormula v
RFXOr RFormula v
a'' RFormula v
b'')
rformula Integer
i (Formula v
a :&&: Formula v
b) = Integer -> Formula v -> Either Bool (RFormula v)
forall v. Integer -> Formula v -> Either Bool (RFormula v)
rformula Integer
i (Formula v -> Formula v
forall v. Formula v -> Formula v
Not (Formula v -> Formula v
forall v. Formula v -> Formula v
Not Formula v
a Formula v -> Formula v -> Formula v
forall v. Formula v -> Formula v -> Formula v
:||: Formula v -> Formula v
forall v. Formula v -> Formula v
Not Formula v
b))
rformula Integer
i (Formula v
a :->: Formula v
b) = Integer -> Formula v -> Either Bool (RFormula v)
forall v. Integer -> Formula v -> Either Bool (RFormula v)
rformula Integer
i (Formula v -> Formula v
forall v. Formula v -> Formula v
Not Formula v
a Formula v -> Formula v -> Formula v
forall v. Formula v -> Formula v -> Formula v
:||: Formula v
b)
rformula Integer
i (Formula v
a :<->: Formula v
b) = Integer -> Formula v -> Either Bool (RFormula v)
forall v. Integer -> Formula v -> Either Bool (RFormula v)
rformula Integer
i (Formula v -> Formula v
forall v. Formula v -> Formula v
Not Formula v
a Formula v -> Formula v -> Formula v
forall v. Formula v -> Formula v -> Formula v
:++: Formula v
b)
rformula Integer
i (All [Formula v]
vs) = Integer -> Formula v -> Either Bool (RFormula v)
forall v. Integer -> Formula v -> Either Bool (RFormula v)
rformula Integer
i ([Formula v] -> Formula v
forall v. [Formula v] -> Formula v
all [Formula v]
vs)
rformula Integer
i (Some [Formula v]
vs) = Integer -> Formula v -> Either Bool (RFormula v)
forall v. Integer -> Formula v -> Either Bool (RFormula v)
rformula Integer
i ([Formula v] -> Formula v
forall v. [Formula v] -> Formula v
some [Formula v]
vs)
rformula Integer
i (None [Formula v]
vs) = Integer -> Formula v -> Either Bool (RFormula v)
forall v. Integer -> Formula v -> Either Bool (RFormula v)
rformula Integer
i ([Formula v] -> Formula v
forall v. [Formula v] -> Formula v
none [Formula v]
vs)
rformula Integer
i (AtMostOne [Formula v]
vs) = Integer -> Formula v -> Either Bool (RFormula v)
forall v. Integer -> Formula v -> Either Bool (RFormula v)
rformula Integer
i ([Formula v] -> Formula v
forall v. [Formula v] -> Formula v
atMostOne [Formula v]
vs)
rformula Integer
i (ExactlyOne [Formula v]
vs) = Integer -> Formula v -> Either Bool (RFormula v)
forall v. Integer -> Formula v -> Either Bool (RFormula v)
rformula Integer
i ([Formula v] -> Formula v
forall v. [Formula v] -> Formula v
exactlyOne [Formula v]
vs)
rformula Integer
i (Let Formula v
a Formula v -> Formula v
f) =
  case Integer -> Formula v -> Either Bool (RFormula v)
forall v. Integer -> Formula v -> Either Bool (RFormula v)
rformula Integer
i Formula v
a of
    Left Bool
True -> Integer -> Formula v -> Either Bool (RFormula v)
forall v. Integer -> Formula v -> Either Bool (RFormula v)
rformula Integer
i (Formula v -> Formula v
f Formula v
forall v. Formula v
Yes)
    Left Bool
False -> Integer -> Formula v -> Either Bool (RFormula v)
forall v. Integer -> Formula v -> Either Bool (RFormula v)
rformula Integer
i (Formula v -> Formula v
f Formula v
forall v. Formula v
No)
    Right RFormula v
a'' ->
      case Integer -> Formula v -> Either Bool (RFormula v)
forall v. Integer -> Formula v -> Either Bool (RFormula v)
rformula (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) (Formula v -> Formula v
f (Integer -> Formula v
forall v. Integer -> Formula v
Bound Integer
i)) of
        Left Bool
x -> Bool -> Either Bool (RFormula v)
forall a b. a -> Either a b
Left Bool
x
        Right RFormula v
b'' -> RFormula v -> Either Bool (RFormula v)
forall a b. b -> Either a b
Right (Integer -> RFormula v -> RFormula v -> RFormula v
forall v. Integer -> RFormula v -> RFormula v -> RFormula v
RFLet Integer
i RFormula v
a'' RFormula v
b'')
rformula Integer
i (Bound Integer
x) = RFormula v -> Either Bool (RFormula v)
forall a b. b -> Either a b
Right (Integer -> RFormula v
forall v. Integer -> RFormula v
RFBound Integer
x)

-- ----------------------------------------------------------------------
-- * De Morgan formulas

-- | Formulas in De Morgan standard form. We omit the constant formulas
-- 'True' and 'False', as they should only occur at the top level.
data DMFormula v =
  DMPos v                                     -- ^ A positive literal.
  | DMNeg v                                   -- ^ A negative literal.
  | DMPosBound Integer                        -- ^ A positive bound variable.
  | DMNegBound Integer                        -- ^ A negative bound variable.
  | DMAnd (DMFormula v) (DMFormula v)         -- ^ Conjunction.
  | DMOr (DMFormula v) (DMFormula v)          -- ^ Disjunction.
  | DMXOr (DMFormula v) (DMFormula v)         -- ^ Exclusive or.
  | DMLet Integer (DMFormula v) (DMFormula v) -- ^ let /x/ = /a/ in /b/.
    
-- | Translate a reduced formula to De Morgan standard form.
demorgan :: RFormula v -> DMFormula v
demorgan :: forall v. RFormula v -> DMFormula v
demorgan (RFVar v
v) = v -> DMFormula v
forall v. v -> DMFormula v
DMPos v
v
demorgan (RFBound Integer
x) = Integer -> DMFormula v
forall v. Integer -> DMFormula v
DMPosBound Integer
x
demorgan (RFNot RFormula v
a) = RFormula v -> DMFormula v
forall v. RFormula v -> DMFormula v
demorgan_neg RFormula v
a
demorgan (RFOr RFormula v
a RFormula v
b) = DMFormula v -> DMFormula v -> DMFormula v
forall v. DMFormula v -> DMFormula v -> DMFormula v
DMOr (RFormula v -> DMFormula v
forall v. RFormula v -> DMFormula v
demorgan RFormula v
a) (RFormula v -> DMFormula v
forall v. RFormula v -> DMFormula v
demorgan RFormula v
b)
demorgan (RFXOr RFormula v
a RFormula v
b) = DMFormula v -> DMFormula v -> DMFormula v
forall v. DMFormula v -> DMFormula v -> DMFormula v
DMXOr (RFormula v -> DMFormula v
forall v. RFormula v -> DMFormula v
demorgan RFormula v
a) (RFormula v -> DMFormula v
forall v. RFormula v -> DMFormula v
demorgan RFormula v
b)
demorgan (RFLet Integer
x RFormula v
a RFormula v
b) = Integer -> DMFormula v -> DMFormula v -> DMFormula v
forall v. Integer -> DMFormula v -> DMFormula v -> DMFormula v
DMLet Integer
x (RFormula v -> DMFormula v
forall v. RFormula v -> DMFormula v
demorgan RFormula v
a) (RFormula v -> DMFormula v
forall v. RFormula v -> DMFormula v
demorgan RFormula v
b)

-- | Translate the negation of a reduced formula to De Morgan standard
-- form.
demorgan_neg :: RFormula v -> DMFormula v
demorgan_neg :: forall v. RFormula v -> DMFormula v
demorgan_neg (RFVar v
v) = v -> DMFormula v
forall v. v -> DMFormula v
DMNeg v
v
demorgan_neg (RFBound Integer
x) = Integer -> DMFormula v
forall v. Integer -> DMFormula v
DMNegBound Integer
x
demorgan_neg (RFNot RFormula v
a) = RFormula v -> DMFormula v
forall v. RFormula v -> DMFormula v
demorgan RFormula v
a
demorgan_neg (RFOr RFormula v
a RFormula v
b) = DMFormula v -> DMFormula v -> DMFormula v
forall v. DMFormula v -> DMFormula v -> DMFormula v
DMAnd (RFormula v -> DMFormula v
forall v. RFormula v -> DMFormula v
demorgan_neg RFormula v
a) (RFormula v -> DMFormula v
forall v. RFormula v -> DMFormula v
demorgan_neg RFormula v
b)
demorgan_neg (RFXOr RFormula v
a RFormula v
b) = DMFormula v -> DMFormula v -> DMFormula v
forall v. DMFormula v -> DMFormula v -> DMFormula v
DMXOr (RFormula v -> DMFormula v
forall v. RFormula v -> DMFormula v
demorgan_neg RFormula v
a) (RFormula v -> DMFormula v
forall v. RFormula v -> DMFormula v
demorgan RFormula v
b)
demorgan_neg (RFLet Integer
x RFormula v
a RFormula v
b) = Integer -> DMFormula v -> DMFormula v -> DMFormula v
forall v. Integer -> DMFormula v -> DMFormula v -> DMFormula v
DMLet Integer
x (RFormula v -> DMFormula v
forall v. RFormula v -> DMFormula v
demorgan RFormula v
a) (RFormula v -> DMFormula v
forall v. RFormula v -> DMFormula v
demorgan_neg RFormula v
b)

-- ----------------------------------------------------------------------
-- * A monad for translation to CNF

-- | Literals over a set /v/, extended with countably many additional elements.
type ELit v = Lit (Either Integer v)

-- | A monad for translation to CNF. This monad keeps track of two kinds
-- of state: an integer counter to provide a supply of fresh
-- variables, and a list of definitional clauses.
data Trans v a = Trans (Integer -> (a, Integer, [[ELit v]]))

instance Monad (Trans v) where
  return :: forall a. a -> Trans v a
return a
a = (Integer -> (a, Integer, [[ELit v]])) -> Trans v a
forall v a. (Integer -> (a, Integer, [[ELit v]])) -> Trans v a
Trans (\Integer
n -> (a
a, Integer
n, []))
  (Trans Integer -> (a, Integer, [[ELit v]])
f) >>= :: forall a b. Trans v a -> (a -> Trans v b) -> Trans v b
>>= a -> Trans v b
g = (Integer -> (b, Integer, [[ELit v]])) -> Trans v b
forall v a. (Integer -> (a, Integer, [[ELit v]])) -> Trans v a
Trans (\Integer
n ->
                            let (a
a1, Integer
n1, [[ELit v]]
l1) = Integer -> (a, Integer, [[ELit v]])
f Integer
n in
                            let Trans Integer -> (b, Integer, [[ELit v]])
h = a -> Trans v b
g a
a1 in
                            let (b
a2, Integer
n2, [[ELit v]]
l2) = Integer -> (b, Integer, [[ELit v]])
h Integer
n1 in
                            (b
a2, Integer
n2, [[ELit v]]
l1 [[ELit v]] -> [[ELit v]] -> [[ELit v]]
forall a. [a] -> [a] -> [a]
++ [[ELit v]]
l2))
  
instance Applicative (Trans v) where
  pure :: forall a. a -> Trans v a
pure = a -> Trans v a
forall a. a -> Trans v a
forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: forall a b. Trans v (a -> b) -> Trans v a -> Trans v b
(<*>) = Trans v (a -> b) -> Trans v a -> Trans v b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
  
instance Functor (Trans v) where
  fmap :: forall a b. (a -> b) -> Trans v a -> Trans v b
fmap = (a -> b) -> Trans v a -> Trans v b
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM

-- | Run the 'Trans' monad.
runTrans :: Trans v a -> (a, [[ELit v]])
runTrans :: forall v a. Trans v a -> (a, [[ELit v]])
runTrans (Trans Integer -> (a, Integer, [[ELit v]])
f) = (a
a, [[ELit v]]
l)
  where
    (a
a, Integer
_, [[ELit v]]
l) = Integer -> (a, Integer, [[ELit v]])
f Integer
0

-- | Return a fresh literal.
fresh_lit :: Trans v (ELit v)
fresh_lit :: forall v. Trans v (ELit v)
fresh_lit = (Integer -> (ELit v, Integer, [[ELit v]])) -> Trans v (ELit v)
forall v a. (Integer -> (a, Integer, [[ELit v]])) -> Trans v a
Trans (\Integer
n -> (Either Integer v -> ELit v
forall a. a -> Lit a
Pos (Integer -> Either Integer v
forall a b. a -> Either a b
Left Integer
n), Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1, []))

-- | Add some definitional clauses.
add_cnf :: [[ELit v]] -> Trans v ()
add_cnf :: forall v. [[ELit v]] -> Trans v ()
add_cnf [[ELit v]]
cs = (Integer -> ((), Integer, [[ELit v]])) -> Trans v ()
forall v a. (Integer -> (a, Integer, [[ELit v]])) -> Trans v a
Trans (\Integer
n -> ((), Integer
n, [[ELit v]]
cs))

-- ----------------------------------------------------------------------
-- * Translation from De Morgan to CNF

-- $ The simplest way to translate a formula, say
--
-- > (A ∧ B) ∨ (C ∧ (D ∨ E ∨ F)),
-- 
-- is to introduce a new variable for each intermediate result, i.e.,
-- to give clauses
--
-- > X, X ↔ Y ∨ Z, Y ↔ A ∧ B, Z ↔ C ∧ W, W ↔ D ∨ V, V ↔ E ∨ F.
--
-- (Each equivalence \"↔\" can be translated into CNF
-- straightforwardly).  Our translation is basically an optimized
-- version of this. The optimizations are: introduce additional
-- variables only when necessary; if the input formula is a CNF, leave
-- it unchanged. We give specialized translations of some formulas
-- depending on the context; for example, an exclusive or can be
-- translated in several different ways. For the above example, our
-- translation yields:
--
-- > Y ∨ Z, X ↔ A ∧ B, Z ↔ C ∧ W, W ↔ D ∨ E ∨ F.

-- | An environment is a mapping from local bound variables to
-- literals.
type Env v = Map Integer (ELit v)

-- | Translate a De Morgan formula to a SAT-equivalent CNF.  Since this
-- requires the introduction of fresh variables, the CNF is over a
-- larger variable set, and we work in the 'Trans' monad. Moreover,
-- the translation depends on an environment.
trans_cnf :: Env v -> DMFormula v -> Trans v [[ELit v]]
trans_cnf :: forall v. Env v -> DMFormula v -> Trans v [[ELit v]]
trans_cnf Env v
env (DMPos v
v) = [[ELit v]] -> Trans v [[ELit v]]
forall a. a -> Trans v a
forall (m :: * -> *) a. Monad m => a -> m a
return [[Either Integer v -> ELit v
forall a. a -> Lit a
Pos (v -> Either Integer v
forall a b. b -> Either a b
Right v
v)]]
trans_cnf Env v
env (DMNeg v
v) = [[ELit v]] -> Trans v [[ELit v]]
forall a. a -> Trans v a
forall (m :: * -> *) a. Monad m => a -> m a
return [[Either Integer v -> ELit v
forall a. a -> Lit a
Neg (v -> Either Integer v
forall a b. b -> Either a b
Right v
v)]]
trans_cnf Env v
env (DMPosBound Integer
n) = [[ELit v]] -> Trans v [[ELit v]]
forall a. a -> Trans v a
forall (m :: * -> *) a. Monad m => a -> m a
return [[ELit v
x]]
  where
    x :: ELit v
x = Env v
env Env v -> Integer -> ELit v
forall k a. Ord k => Map k a -> k -> a
Map.! Integer
n
trans_cnf Env v
env (DMNegBound Integer
n) = [[ELit v]] -> Trans v [[ELit v]]
forall a. a -> Trans v a
forall (m :: * -> *) a. Monad m => a -> m a
return [[ELit v -> ELit v
forall a. Lit a -> Lit a
neg ELit v
x]]
  where
    x :: ELit v
x = Env v
env Env v -> Integer -> ELit v
forall k a. Ord k => Map k a -> k -> a
Map.! Integer
n
trans_cnf Env v
env (DMAnd DMFormula v
a DMFormula v
b) = do
  [[ELit v]]
a' <- Env v -> DMFormula v -> Trans v [[ELit v]]
forall v. Env v -> DMFormula v -> Trans v [[ELit v]]
trans_cnf Env v
env DMFormula v
a
  [[ELit v]]
b' <- Env v -> DMFormula v -> Trans v [[ELit v]]
forall v. Env v -> DMFormula v -> Trans v [[ELit v]]
trans_cnf Env v
env DMFormula v
b
  [[ELit v]] -> Trans v [[ELit v]]
forall a. a -> Trans v a
forall (m :: * -> *) a. Monad m => a -> m a
return ([[ELit v]]
a' [[ELit v]] -> [[ELit v]] -> [[ELit v]]
forall a. [a] -> [a] -> [a]
++ [[ELit v]]
b')
trans_cnf Env v
env (DMOr DMFormula v
a DMFormula v
b) = do
  [ELit v]
a' <- Env v -> DMFormula v -> Trans v [ELit v]
forall v. Env v -> DMFormula v -> Trans v [ELit v]
trans_or Env v
env DMFormula v
a
  [ELit v]
b' <- Env v -> DMFormula v -> Trans v [ELit v]
forall v. Env v -> DMFormula v -> Trans v [ELit v]
trans_or Env v
env DMFormula v
b
  [[ELit v]] -> Trans v [[ELit v]]
forall a. a -> Trans v a
forall (m :: * -> *) a. Monad m => a -> m a
return [[ELit v]
a' [ELit v] -> [ELit v] -> [ELit v]
forall a. [a] -> [a] -> [a]
++ [ELit v]
b']
trans_cnf Env v
env (DMXOr DMFormula v
a DMFormula v
b) = do
  ELit v
x <- Env v -> DMFormula v -> Trans v (ELit v)
forall v. Env v -> DMFormula v -> Trans v (ELit v)
trans_lit Env v
env DMFormula v
a
  ELit v
y <- Env v -> DMFormula v -> Trans v (ELit v)
forall v. Env v -> DMFormula v -> Trans v (ELit v)
trans_lit Env v
env DMFormula v
b
  [[ELit v]] -> Trans v [[ELit v]]
forall a. a -> Trans v a
forall (m :: * -> *) a. Monad m => a -> m a
return [[ELit v
x, ELit v
y], [ELit v -> ELit v
forall a. Lit a -> Lit a
neg ELit v
x, ELit v -> ELit v
forall a. Lit a -> Lit a
neg ELit v
y]]
trans_cnf Env v
env (DMLet Integer
n DMFormula v
a DMFormula v
b) = do
  Env v
-> Integer
-> DMFormula v
-> DMFormula v
-> (Env v -> DMFormula v -> Trans v [[ELit v]])
-> Trans v [[ELit v]]
forall v a.
Env v
-> Integer
-> DMFormula v
-> DMFormula v
-> (Env v -> DMFormula v -> Trans v a)
-> Trans v a
do_let Env v
env Integer
n DMFormula v
a DMFormula v
b Env v -> DMFormula v -> Trans v [[ELit v]]
forall v. Env v -> DMFormula v -> Trans v [[ELit v]]
trans_cnf

-- | Translate a De Morgan formula to a disjunction of literals.
trans_or :: Env v -> DMFormula v -> Trans v [ELit v]
trans_or :: forall v. Env v -> DMFormula v -> Trans v [ELit v]
trans_or Env v
env (DMXOr DMFormula v
a DMFormula v
b) = do
  ELit v
x <- Env v -> DMFormula v -> Trans v (ELit v)
forall v. Env v -> DMFormula v -> Trans v (ELit v)
trans_lit Env v
env (DMFormula v -> DMFormula v -> DMFormula v
forall v. DMFormula v -> DMFormula v -> DMFormula v
DMXOr DMFormula v
a DMFormula v
b)
  [ELit v] -> Trans v [ELit v]
forall a. a -> Trans v a
forall (m :: * -> *) a. Monad m => a -> m a
return [ELit v
x]
trans_or Env v
env (DMLet Integer
n DMFormula v
a DMFormula v
b) = do
  Env v
-> Integer
-> DMFormula v
-> DMFormula v
-> (Env v -> DMFormula v -> Trans v [ELit v])
-> Trans v [ELit v]
forall v a.
Env v
-> Integer
-> DMFormula v
-> DMFormula v
-> (Env v -> DMFormula v -> Trans v a)
-> Trans v a
do_let Env v
env Integer
n DMFormula v
a DMFormula v
b Env v -> DMFormula v -> Trans v [ELit v]
forall v. Env v -> DMFormula v -> Trans v [ELit v]
trans_or
trans_or Env v
env DMFormula v
a = do
  [[ELit v]]
c <- Env v -> DMFormula v -> Trans v [[ELit v]]
forall v. Env v -> DMFormula v -> Trans v [[ELit v]]
trans_cnf Env v
env DMFormula v
a
  [[ELit v]] -> Trans v [ELit v]
forall v. [[ELit v]] -> Trans v [ELit v]
or_of_cnf [[ELit v]]
c

-- | Translate a De Morgan formula to a single literal.
trans_lit :: Env v -> DMFormula v -> Trans v (ELit v)
trans_lit :: forall v. Env v -> DMFormula v -> Trans v (ELit v)
trans_lit Env v
env (DMXOr DMFormula v
a DMFormula v
b) = do
  ELit v
x <- Env v -> DMFormula v -> Trans v (ELit v)
forall v. Env v -> DMFormula v -> Trans v (ELit v)
trans_lit Env v
env DMFormula v
a
  ELit v
y <- Env v -> DMFormula v -> Trans v (ELit v)
forall v. Env v -> DMFormula v -> Trans v (ELit v)
trans_lit Env v
env DMFormula v
b
  ELit v
z <- ELit v -> ELit v -> Trans v (ELit v)
forall v. ELit v -> ELit v -> Trans v (ELit v)
lit_of_xor ELit v
x ELit v
y
  ELit v -> Trans v (ELit v)
forall a. a -> Trans v a
forall (m :: * -> *) a. Monad m => a -> m a
return ELit v
z
trans_lit Env v
env (DMLet Integer
n DMFormula v
a DMFormula v
b) = do
  Env v
-> Integer
-> DMFormula v
-> DMFormula v
-> (Env v -> DMFormula v -> Trans v (ELit v))
-> Trans v (ELit v)
forall v a.
Env v
-> Integer
-> DMFormula v
-> DMFormula v
-> (Env v -> DMFormula v -> Trans v a)
-> Trans v a
do_let Env v
env Integer
n DMFormula v
a DMFormula v
b Env v -> DMFormula v -> Trans v (ELit v)
forall v. Env v -> DMFormula v -> Trans v (ELit v)
trans_lit
trans_lit Env v
env DMFormula v
a = do
  [[ELit v]]
c <- Env v -> DMFormula v -> Trans v [[ELit v]]
forall v. Env v -> DMFormula v -> Trans v [[ELit v]]
trans_cnf Env v
env DMFormula v
a
  [[ELit v]] -> Trans v (ELit v)
forall v. [[ELit v]] -> Trans v (ELit v)
lit_of_cnf [[ELit v]]
c

-- | Polymorphically translate a 'DMLet' expression. The fifth
-- argument is usually one of 'trans_cnf', 'trans_or', or 'trans_lit',
-- and is used to translate the body of the \"let\".
do_let :: Env v -> Integer -> DMFormula v -> DMFormula v -> (Env v -> DMFormula v -> Trans v a) -> Trans v a
do_let :: forall v a.
Env v
-> Integer
-> DMFormula v
-> DMFormula v
-> (Env v -> DMFormula v -> Trans v a)
-> Trans v a
do_let Env v
env Integer
n DMFormula v
a DMFormula v
b Env v -> DMFormula v -> Trans v a
cont = do
  ELit v
x <- Env v -> DMFormula v -> Trans v (ELit v)
forall v. Env v -> DMFormula v -> Trans v (ELit v)
trans_lit Env v
env DMFormula v
a
  let env' :: Env v
env' = Integer -> ELit v -> Env v -> Env v
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Integer
n ELit v
x Env v
env
  Env v -> DMFormula v -> Trans v a
cont Env v
env' DMFormula v
b
  
-- | Convert a CNF to a disjunction of literals.
or_of_cnf :: [[ELit v]] -> Trans v [ELit v]
or_of_cnf :: forall v. [[ELit v]] -> Trans v [ELit v]
or_of_cnf [[ELit v]
d] = [ELit v] -> Trans v [ELit v]
forall a. a -> Trans v a
forall (m :: * -> *) a. Monad m => a -> m a
return [ELit v]
d
or_of_cnf [[ELit v]]
ds = do
  ELit v
x <- [[ELit v]] -> Trans v (ELit v)
forall v. [[ELit v]] -> Trans v (ELit v)
lit_of_cnf [[ELit v]]
ds
  [ELit v] -> Trans v [ELit v]
forall a. a -> Trans v a
forall (m :: * -> *) a. Monad m => a -> m a
return [ELit v
x]

-- | Convert a CNF to a single literal.
lit_of_cnf :: [[ELit v]] -> Trans v (ELit v)
lit_of_cnf :: forall v. [[ELit v]] -> Trans v (ELit v)
lit_of_cnf [[ELit v]]
ds = do
  [ELit v]
xs <- [Trans v (ELit v)] -> Trans v [ELit v]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence (([ELit v] -> Trans v (ELit v)) -> [[ELit v]] -> [Trans v (ELit v)]
forall a b. (a -> b) -> [a] -> [b]
map [ELit v] -> Trans v (ELit v)
forall v. [ELit v] -> Trans v (ELit v)
lit_of_or [[ELit v]]
ds)
  ELit v
y <- [ELit v] -> Trans v (ELit v)
forall v. [ELit v] -> Trans v (ELit v)
lit_of_and [ELit v]
xs
  ELit v -> Trans v (ELit v)
forall a. a -> Trans v a
forall (m :: * -> *) a. Monad m => a -> m a
return ELit v
y

-- | Convert a conjunction of literals to a single literal.
lit_of_and :: [ELit v] -> Trans v (ELit v)
lit_of_and :: forall v. [ELit v] -> Trans v (ELit v)
lit_of_and [ELit v
l] = ELit v -> Trans v (ELit v)
forall a. a -> Trans v a
forall (m :: * -> *) a. Monad m => a -> m a
return ELit v
l
lit_of_and [ELit v]
cs = do
  ELit v
x <- Trans v (ELit v)
forall v. Trans v (ELit v)
fresh_lit
  -- Define x <-> c1 ∧ ... ∧ cn
  [[ELit v]] -> Trans v ()
forall v. [[ELit v]] -> Trans v ()
add_cnf [[ELit v -> ELit v
forall a. Lit a -> Lit a
neg ELit v
x, ELit v
c] | ELit v
c <- [ELit v]
cs ]
  [[ELit v]] -> Trans v ()
forall v. [[ELit v]] -> Trans v ()
add_cnf [[ELit v
x] [ELit v] -> [ELit v] -> [ELit v]
forall a. [a] -> [a] -> [a]
++ [ELit v -> ELit v
forall a. Lit a -> Lit a
neg ELit v
c | ELit v
c <- [ELit v]
cs]]  
  ELit v -> Trans v (ELit v)
forall a. a -> Trans v a
forall (m :: * -> *) a. Monad m => a -> m a
return ELit v
x

-- | Convert a disjunction of literals to a single literal.
lit_of_or :: [ELit v] -> Trans v (ELit v)
lit_of_or :: forall v. [ELit v] -> Trans v (ELit v)
lit_of_or [ELit v
l] = ELit v -> Trans v (ELit v)
forall a. a -> Trans v a
forall (m :: * -> *) a. Monad m => a -> m a
return ELit v
l
lit_of_or [ELit v]
ds = do
  ELit v
x <- Trans v (ELit v)
forall v. Trans v (ELit v)
fresh_lit
  -- Define x <-> d1 ∨ ... ∨ dn
  [[ELit v]] -> Trans v ()
forall v. [[ELit v]] -> Trans v ()
add_cnf [ [ELit v
x, ELit v -> ELit v
forall a. Lit a -> Lit a
neg ELit v
d] | ELit v
d <- [ELit v]
ds ]
  [[ELit v]] -> Trans v ()
forall v. [[ELit v]] -> Trans v ()
add_cnf [[ELit v -> ELit v
forall a. Lit a -> Lit a
neg ELit v
x] [ELit v] -> [ELit v] -> [ELit v]
forall a. [a] -> [a] -> [a]
++ [ELit v
d | ELit v
d <- [ELit v]
ds]]
  ELit v -> Trans v (ELit v)
forall a. a -> Trans v a
forall (m :: * -> *) a. Monad m => a -> m a
return ELit v
x

-- | Convert an exclusive or of two literals to a single literal.
lit_of_xor :: ELit v -> ELit v -> Trans v (ELit v)
lit_of_xor :: forall v. ELit v -> ELit v -> Trans v (ELit v)
lit_of_xor ELit v
x ELit v
y = do
  ELit v
z <- Trans v (ELit v)
forall v. Trans v (ELit v)
fresh_lit
  -- Define z <-> x ⊕ y
  [[ELit v]] -> Trans v ()
forall v. [[ELit v]] -> Trans v ()
add_cnf [[ELit v
z, ELit v
x, ELit v -> ELit v
forall a. Lit a -> Lit a
neg ELit v
y]]
  [[ELit v]] -> Trans v ()
forall v. [[ELit v]] -> Trans v ()
add_cnf [[ELit v
z, ELit v -> ELit v
forall a. Lit a -> Lit a
neg ELit v
x, ELit v
y]]
  [[ELit v]] -> Trans v ()
forall v. [[ELit v]] -> Trans v ()
add_cnf [[ELit v -> ELit v
forall a. Lit a -> Lit a
neg ELit v
z, ELit v
x, ELit v
y]]
  [[ELit v]] -> Trans v ()
forall v. [[ELit v]] -> Trans v ()
add_cnf [[ELit v -> ELit v
forall a. Lit a -> Lit a
neg ELit v
z, ELit v -> ELit v
forall a. Lit a -> Lit a
neg ELit v
x, ELit v -> ELit v
forall a. Lit a -> Lit a
neg ELit v
y]]
  ELit v -> Trans v (ELit v)
forall a. a -> Trans v a
forall (m :: * -> *) a. Monad m => a -> m a
return ELit v
z

-- ----------------------------------------------------------------------
-- * Top-level functions

-- | Translate a De Morgan formula to a SAT-equivalent CNF.
cnf_of_dm :: DMFormula v -> [[ELit v]]
cnf_of_dm :: forall v. DMFormula v -> [[ELit v]]
cnf_of_dm DMFormula v
f = [[ELit v]]
l [[ELit v]] -> [[ELit v]] -> [[ELit v]]
forall a. [a] -> [a] -> [a]
++ [[ELit v]]
a
  where
    env :: Map k a
env = Map k a
forall k a. Map k a
Map.empty
    ([[ELit v]]
a, [[ELit v]]
l) = Trans v [[ELit v]] -> ([[ELit v]], [[ELit v]])
forall v a. Trans v a -> (a, [[ELit v]])
runTrans (Env v -> DMFormula v -> Trans v [[ELit v]]
forall v. Env v -> DMFormula v -> Trans v [[ELit v]]
trans_cnf Env v
forall k a. Map k a
env DMFormula v
f)

-- | Translate a boolean formula to a SAT-equivalent CNF.
cnf_of_formula :: Formula v -> [[ELit v]]
cnf_of_formula :: forall v. Formula v -> [[ELit v]]
cnf_of_formula Formula v
f =
  case Integer -> Formula v -> Either Bool (RFormula v)
forall v. Integer -> Formula v -> Either Bool (RFormula v)
rformula Integer
0 Formula v
f of
   Left Bool
True -> []
   Left Bool
False -> [[]]
   Right RFormula v
rf -> DMFormula v -> [[ELit v]]
forall v. DMFormula v -> [[ELit v]]
cnf_of_dm (RFormula v -> DMFormula v
forall v. RFormula v -> DMFormula v
demorgan RFormula v
rf)    

-- ----------------------------------------------------------------------
-- * SAT solver API for boolean formulas

-- | Check whether a boolean formula is satisfiable.
satisfiable :: (Ord v) => Formula v -> Bool
satisfiable :: forall v. Ord v => Formula v -> Bool
satisfiable Formula v
a = Maybe (Map v Bool) -> Bool
forall a. Maybe a -> Bool
isJust (Formula v -> Maybe (Map v Bool)
forall v. Ord v => Formula v -> Maybe (Map v Bool)
solve Formula v
a)

-- | Return a satisfying assignment for the boolean formula, if any.
solve :: (Ord v) => Formula v -> Maybe (Map v Bool)
solve :: forall v. Ord v => Formula v -> Maybe (Map v Bool)
solve Formula v
a = [Map v Bool] -> Maybe (Map v Bool)
forall a. [a] -> Maybe a
listToMaybe (Formula v -> [Map v Bool]
forall v. Ord v => Formula v -> [Map v Bool]
solve_all Formula v
a)

-- | Lazily enumerate all satisfying assignments for the boolean formula.
solve_all :: (Ord v) => Formula v -> [Map v Bool]
solve_all :: forall v. Ord v => Formula v -> [Map v Bool]
solve_all Formula v
a = [Map v Bool]
res
  where
    a' :: [[ELit v]]
a' = Formula v -> [[ELit v]]
forall v. Formula v -> [[ELit v]]
cnf_of_formula Formula v
a
    res' :: [Map (Either Integer v) Bool]
res' = [[ELit v]] -> [Map (Either Integer v) Bool]
forall v. Ord v => [[Lit v]] -> [Map v Bool]
cnf_solve_all [[ELit v]]
a'
    res :: [Map v Bool]
res = (Map (Either Integer v) Bool -> Map v Bool)
-> [Map (Either Integer v) Bool] -> [Map v Bool]
forall a b. (a -> b) -> [a] -> [b]
map Map (Either Integer v) Bool -> Map v Bool
forall {k} {a} {a}. Ord k => Map (Either a k) a -> Map k a
restrict [Map (Either Integer v) Bool]
res'
    restrict :: Map (Either a k) a -> Map k a
restrict Map (Either a k) a
ans = [(k, a)] -> Map k a
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (k
v, a
b) | (Right k
v, a
b) <- Map (Either a k) a -> [(Either a k, a)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (Either a k) a
ans ]