{-# LANGUAGE OverloadedStrings #-}

-- | A very bad SAT solver written by reduction to ECTA
--
--  Also a constructive proof of the NP-hardness of finding
--  a term represented by an ECTA

module Application.SAT (
  -- * Data types
    Var
  , mkVar
  , CNF(..)
  , Clause(..)
  , Lit(..)

  -- * Solving
  , toEcta
  , allSolutions

  -- * Examples
  , ex1
  , ex2
  , ex3
  ) where

import Data.Hashable ( Hashable )
import Data.HashMap.Strict ( HashMap )
import qualified Data.HashMap.Strict as HashMap
import Data.HashSet ( HashSet )
import qualified Data.HashSet as HashSet
import Data.List ( elemIndex, sort )
import Data.Maybe ( fromJust )
import Data.String (IsString(..) )
import Data.Text ( Text )

import GHC.Generics ( Generic )

import Data.List.Index ( imap )

import Data.ECTA
import Data.ECTA.Paths
import Data.ECTA.Term
import Data.Text.Extended.Pretty
import Utility.Fixpoint

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

-------------------------------------------------------------------
------------------------- SAT variables ---------------------------
-------------------------------------------------------------------


newtype Var = Var { Var -> Text
unVar :: Text }
  deriving ( Var -> Var -> Bool
(Var -> Var -> Bool) -> (Var -> Var -> Bool) -> Eq Var
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Var -> Var -> Bool
$c/= :: Var -> Var -> Bool
== :: Var -> Var -> Bool
$c== :: Var -> Var -> Bool
Eq, Eq Var
Eq Var
-> (Var -> Var -> Ordering)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Var)
-> (Var -> Var -> Var)
-> Ord Var
Var -> Var -> Bool
Var -> Var -> Ordering
Var -> Var -> Var
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
min :: Var -> Var -> Var
$cmin :: Var -> Var -> Var
max :: Var -> Var -> Var
$cmax :: Var -> Var -> Var
>= :: Var -> Var -> Bool
$c>= :: Var -> Var -> Bool
> :: Var -> Var -> Bool
$c> :: Var -> Var -> Bool
<= :: Var -> Var -> Bool
$c<= :: Var -> Var -> Bool
< :: Var -> Var -> Bool
$c< :: Var -> Var -> Bool
compare :: Var -> Var -> Ordering
$ccompare :: Var -> Var -> Ordering
$cp1Ord :: Eq Var
Ord, Int -> Var -> ShowS
[Var] -> ShowS
Var -> String
(Int -> Var -> ShowS)
-> (Var -> String) -> ([Var] -> ShowS) -> Show Var
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Var] -> ShowS
$cshowList :: [Var] -> ShowS
show :: Var -> String
$cshow :: Var -> String
showsPrec :: Int -> Var -> ShowS
$cshowsPrec :: Int -> Var -> ShowS
Show, (forall x. Var -> Rep Var x)
-> (forall x. Rep Var x -> Var) -> Generic Var
forall x. Rep Var x -> Var
forall x. Var -> Rep Var x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Var x -> Var
$cfrom :: forall x. Var -> Rep Var x
Generic )

instance Hashable Var

instance IsString Var where
  fromString :: String -> Var
fromString = Text -> Var
Var (Text -> Var) -> (String -> Text) -> String -> Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
forall a. IsString a => String -> a
fromString

mkVar :: Text -> Var
mkVar :: Text -> Var
mkVar = Text -> Var
Var

_varToSymbol :: Var -> Symbol
_varToSymbol :: Var -> Symbol
_varToSymbol = Text -> Symbol
Symbol (Text -> Symbol) -> (Var -> Text) -> Var -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Text
unVar

_varToNegSymbol :: Var -> Symbol
_varToNegSymbol :: Var -> Symbol
_varToNegSymbol Var
v = Text -> Symbol
Symbol (Text
"~" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Var -> Text
unVar Var
v)


-------------------------------------------------------------------
----------------------- CNF representation ------------------------
-------------------------------------------------------------------

-- | Our construction generalizes to arbitrary NNF formulas,
--   and possibly to arbitrary SAT,
--   but we don't need to bother; just CNF is good enough

data CNF = And [Clause]
  deriving ( CNF -> CNF -> Bool
(CNF -> CNF -> Bool) -> (CNF -> CNF -> Bool) -> Eq CNF
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CNF -> CNF -> Bool
$c/= :: CNF -> CNF -> Bool
== :: CNF -> CNF -> Bool
$c== :: CNF -> CNF -> Bool
Eq, Eq CNF
Eq CNF
-> (CNF -> CNF -> Ordering)
-> (CNF -> CNF -> Bool)
-> (CNF -> CNF -> Bool)
-> (CNF -> CNF -> Bool)
-> (CNF -> CNF -> Bool)
-> (CNF -> CNF -> CNF)
-> (CNF -> CNF -> CNF)
-> Ord CNF
CNF -> CNF -> Bool
CNF -> CNF -> Ordering
CNF -> CNF -> CNF
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
min :: CNF -> CNF -> CNF
$cmin :: CNF -> CNF -> CNF
max :: CNF -> CNF -> CNF
$cmax :: CNF -> CNF -> CNF
>= :: CNF -> CNF -> Bool
$c>= :: CNF -> CNF -> Bool
> :: CNF -> CNF -> Bool
$c> :: CNF -> CNF -> Bool
<= :: CNF -> CNF -> Bool
$c<= :: CNF -> CNF -> Bool
< :: CNF -> CNF -> Bool
$c< :: CNF -> CNF -> Bool
compare :: CNF -> CNF -> Ordering
$ccompare :: CNF -> CNF -> Ordering
$cp1Ord :: Eq CNF
Ord, Int -> CNF -> ShowS
[CNF] -> ShowS
CNF -> String
(Int -> CNF -> ShowS)
-> (CNF -> String) -> ([CNF] -> ShowS) -> Show CNF
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CNF] -> ShowS
$cshowList :: [CNF] -> ShowS
show :: CNF -> String
$cshow :: CNF -> String
showsPrec :: Int -> CNF -> ShowS
$cshowsPrec :: Int -> CNF -> ShowS
Show, (forall x. CNF -> Rep CNF x)
-> (forall x. Rep CNF x -> CNF) -> Generic CNF
forall x. Rep CNF x -> CNF
forall x. CNF -> Rep CNF x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep CNF x -> CNF
$cfrom :: forall x. CNF -> Rep CNF x
Generic )

instance Hashable CNF

data Clause = Or [Lit]
  deriving ( Clause -> Clause -> Bool
(Clause -> Clause -> Bool)
-> (Clause -> Clause -> Bool) -> Eq Clause
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Clause -> Clause -> Bool
$c/= :: Clause -> Clause -> Bool
== :: Clause -> Clause -> Bool
$c== :: Clause -> Clause -> Bool
Eq, Eq Clause
Eq Clause
-> (Clause -> Clause -> Ordering)
-> (Clause -> Clause -> Bool)
-> (Clause -> Clause -> Bool)
-> (Clause -> Clause -> Bool)
-> (Clause -> Clause -> Bool)
-> (Clause -> Clause -> Clause)
-> (Clause -> Clause -> Clause)
-> Ord Clause
Clause -> Clause -> Bool
Clause -> Clause -> Ordering
Clause -> Clause -> Clause
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
min :: Clause -> Clause -> Clause
$cmin :: Clause -> Clause -> Clause
max :: Clause -> Clause -> Clause
$cmax :: Clause -> Clause -> Clause
>= :: Clause -> Clause -> Bool
$c>= :: Clause -> Clause -> Bool
> :: Clause -> Clause -> Bool
$c> :: Clause -> Clause -> Bool
<= :: Clause -> Clause -> Bool
$c<= :: Clause -> Clause -> Bool
< :: Clause -> Clause -> Bool
$c< :: Clause -> Clause -> Bool
compare :: Clause -> Clause -> Ordering
$ccompare :: Clause -> Clause -> Ordering
$cp1Ord :: Eq Clause
Ord, Int -> Clause -> ShowS
[Clause] -> ShowS
Clause -> String
(Int -> Clause -> ShowS)
-> (Clause -> String) -> ([Clause] -> ShowS) -> Show Clause
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Clause] -> ShowS
$cshowList :: [Clause] -> ShowS
show :: Clause -> String
$cshow :: Clause -> String
showsPrec :: Int -> Clause -> ShowS
$cshowsPrec :: Int -> Clause -> ShowS
Show, (forall x. Clause -> Rep Clause x)
-> (forall x. Rep Clause x -> Clause) -> Generic Clause
forall x. Rep Clause x -> Clause
forall x. Clause -> Rep Clause x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Clause x -> Clause
$cfrom :: forall x. Clause -> Rep Clause x
Generic )

instance Hashable Clause

data Lit = PosLit Var
         | NegLit Var
  deriving ( Lit -> Lit -> Bool
(Lit -> Lit -> Bool) -> (Lit -> Lit -> Bool) -> Eq Lit
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Lit -> Lit -> Bool
$c/= :: Lit -> Lit -> Bool
== :: Lit -> Lit -> Bool
$c== :: Lit -> Lit -> Bool
Eq, Eq Lit
Eq Lit
-> (Lit -> Lit -> Ordering)
-> (Lit -> Lit -> Bool)
-> (Lit -> Lit -> Bool)
-> (Lit -> Lit -> Bool)
-> (Lit -> Lit -> Bool)
-> (Lit -> Lit -> Lit)
-> (Lit -> Lit -> Lit)
-> Ord Lit
Lit -> Lit -> Bool
Lit -> Lit -> Ordering
Lit -> Lit -> Lit
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
min :: Lit -> Lit -> Lit
$cmin :: Lit -> Lit -> Lit
max :: Lit -> Lit -> Lit
$cmax :: Lit -> Lit -> Lit
>= :: Lit -> Lit -> Bool
$c>= :: Lit -> Lit -> Bool
> :: Lit -> Lit -> Bool
$c> :: Lit -> Lit -> Bool
<= :: Lit -> Lit -> Bool
$c<= :: Lit -> Lit -> Bool
< :: Lit -> Lit -> Bool
$c< :: Lit -> Lit -> Bool
compare :: Lit -> Lit -> Ordering
$ccompare :: Lit -> Lit -> Ordering
$cp1Ord :: Eq Lit
Ord, Int -> Lit -> ShowS
[Lit] -> ShowS
Lit -> String
(Int -> Lit -> ShowS)
-> (Lit -> String) -> ([Lit] -> ShowS) -> Show Lit
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Lit] -> ShowS
$cshowList :: [Lit] -> ShowS
show :: Lit -> String
$cshow :: Lit -> String
showsPrec :: Int -> Lit -> ShowS
$cshowsPrec :: Int -> Lit -> ShowS
Show, (forall x. Lit -> Rep Lit x)
-> (forall x. Rep Lit x -> Lit) -> Generic Lit
forall x. Rep Lit x -> Lit
forall x. Lit -> Rep Lit x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Lit x -> Lit
$cfrom :: forall x. Lit -> Rep Lit x
Generic )

instance Hashable Lit

instance Pretty Lit where
  pretty :: Lit -> Text
pretty (PosLit Var
v) = Var -> Text
unVar Var
v
  pretty (NegLit Var
v) = Text
"~" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Var -> Text
unVar Var
v

getLitVar :: Lit -> Var
getLitVar :: Lit -> Var
getLitVar (PosLit Var
v) = Var
v
getLitVar (NegLit Var
v) = Var
v

---------------------
-------- Traversals
---------------------

-- | This is an updatable fold algebra; see "Dealing with Large Bananas"
data CNFAlg a  = CNFAlg { CNFAlg a -> CNF -> [a] -> a
runCNF    :: CNF    -> [a] -> a
                        , CNFAlg a -> Clause -> [a] -> a
runClause :: Clause -> [a] -> a
                        , CNFAlg a -> Lit -> a
runLit    :: Lit           -> a
                        }

_emptyAlg :: (Monoid m) => CNFAlg m
_emptyAlg :: CNFAlg m
_emptyAlg = (CNF -> [m] -> m) -> (Clause -> [m] -> m) -> (Lit -> m) -> CNFAlg m
forall a.
(CNF -> [a] -> a) -> (Clause -> [a] -> a) -> (Lit -> a) -> CNFAlg a
CNFAlg (([m] -> m) -> CNF -> [m] -> m
forall a b. a -> b -> a
const [m] -> m
forall a. Monoid a => a
mempty) (([m] -> m) -> Clause -> [m] -> m
forall a b. a -> b -> a
const [m] -> m
forall a. Monoid a => a
mempty) (m -> Lit -> m
forall a b. a -> b -> a
const m
forall a. Monoid a => a
mempty)


class FoldAlg a where
  foldAlg :: CNFAlg m -> a -> m

instance FoldAlg CNF where
  foldAlg :: CNFAlg m -> CNF -> m
foldAlg CNFAlg m
alg c :: CNF
c@(And [Clause]
clauses) = CNFAlg m -> CNF -> [m] -> m
forall a. CNFAlg a -> CNF -> [a] -> a
runCNF CNFAlg m
alg CNF
c ((Clause -> m) -> [Clause] -> [m]
forall a b. (a -> b) -> [a] -> [b]
map (CNFAlg m -> Clause -> m
forall a m. FoldAlg a => CNFAlg m -> a -> m
foldAlg CNFAlg m
alg) [Clause]
clauses)

instance FoldAlg Clause where
  foldAlg :: CNFAlg m -> Clause -> m
foldAlg CNFAlg m
alg c :: Clause
c@(Or [Lit]
lits) = CNFAlg m -> Clause -> [m] -> m
forall a. CNFAlg a -> Clause -> [a] -> a
runClause CNFAlg m
alg Clause
c ((Lit -> m) -> [Lit] -> [m]
forall a b. (a -> b) -> [a] -> [b]
map (CNFAlg m -> Lit -> m
forall a m. FoldAlg a => CNFAlg m -> a -> m
foldAlg CNFAlg m
alg) [Lit]
lits)

instance FoldAlg Lit where
  foldAlg :: CNFAlg m -> Lit -> m
foldAlg CNFAlg m
alg Lit
l = CNFAlg m -> Lit -> m
forall m. CNFAlg m -> Lit -> m
runLit CNFAlg m
alg Lit
l

crushAlg :: (Monoid m) => (Lit -> m) -> CNFAlg m
crushAlg :: (Lit -> m) -> CNFAlg m
crushAlg Lit -> m
f = (CNF -> [m] -> m) -> (Clause -> [m] -> m) -> (Lit -> m) -> CNFAlg m
forall a.
(CNF -> [a] -> a) -> (Clause -> [a] -> a) -> (Lit -> a) -> CNFAlg a
CNFAlg (([m] -> m) -> CNF -> [m] -> m
forall a b. a -> b -> a
const [m] -> m
forall a. Monoid a => [a] -> a
mconcat) (([m] -> m) -> Clause -> [m] -> m
forall a b. a -> b -> a
const [m] -> m
forall a. Monoid a => [a] -> a
mconcat) Lit -> m
f

getVars :: CNF -> HashSet Var
getVars :: CNF -> HashSet Var
getVars = CNFAlg (HashSet Var) -> CNF -> HashSet Var
forall a m. FoldAlg a => CNFAlg m -> a -> m
foldAlg ((Lit -> HashSet Var) -> CNFAlg (HashSet Var)
forall m. Monoid m => (Lit -> m) -> CNFAlg m
crushAlg (Var -> HashSet Var
forall a. Hashable a => a -> HashSet a
HashSet.singleton  (Var -> HashSet Var) -> (Lit -> Var) -> Lit -> HashSet Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lit -> Var
getLitVar))

-----
-- Lit paths
-----

newtype LitPaths = LitPaths { LitPaths -> HashMap Lit [Path]
unLitPaths :: HashMap Lit [Path] }

instance Semigroup LitPaths where
  LitPaths
lp1 <> :: LitPaths -> LitPaths -> LitPaths
<> LitPaths
lp2 = HashMap Lit [Path] -> LitPaths
LitPaths (HashMap Lit [Path] -> LitPaths) -> HashMap Lit [Path] -> LitPaths
forall a b. (a -> b) -> a -> b
$ ([Path] -> [Path] -> [Path])
-> HashMap Lit [Path] -> HashMap Lit [Path] -> HashMap Lit [Path]
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> HashMap k v -> HashMap k v -> HashMap k v
HashMap.unionWith [Path] -> [Path] -> [Path]
forall a. Monoid a => a -> a -> a
mappend (LitPaths -> HashMap Lit [Path]
unLitPaths LitPaths
lp1) (LitPaths -> HashMap Lit [Path]
unLitPaths LitPaths
lp2)

instance Monoid LitPaths where
  mempty :: LitPaths
mempty  = HashMap Lit [Path] -> LitPaths
LitPaths HashMap Lit [Path]
forall k v. HashMap k v
HashMap.empty

getLitPathsAlg :: CNFAlg LitPaths
getLitPathsAlg :: CNFAlg LitPaths
getLitPathsAlg = CNFAlg :: forall a.
(CNF -> [a] -> a) -> (Clause -> [a] -> a) -> (Lit -> a) -> CNFAlg a
CNFAlg { runCNF :: CNF -> [LitPaths] -> LitPaths
runCNF    = \CNF
_ [LitPaths]
lps -> [LitPaths] -> LitPaths
forall a. Monoid a => [a] -> a
mconcat ([LitPaths] -> LitPaths) -> [LitPaths] -> LitPaths
forall a b. (a -> b) -> a -> b
$ (Int -> LitPaths -> LitPaths) -> [LitPaths] -> [LitPaths]
forall a b. (Int -> a -> b) -> [a] -> [b]
imap (\Int
i LitPaths
lp -> HashMap Lit [Path] -> LitPaths
LitPaths (HashMap Lit [Path] -> LitPaths) -> HashMap Lit [Path] -> LitPaths
forall a b. (a -> b) -> a -> b
$ ([Path] -> [Path]) -> HashMap Lit [Path] -> HashMap Lit [Path]
forall v1 v2 k. (v1 -> v2) -> HashMap k v1 -> HashMap k v2
HashMap.map ((Path -> Path) -> [Path] -> [Path]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Path -> Path
ConsPath Int
i)) (HashMap Lit [Path] -> HashMap Lit [Path])
-> HashMap Lit [Path] -> HashMap Lit [Path]
forall a b. (a -> b) -> a -> b
$ LitPaths -> HashMap Lit [Path]
unLitPaths LitPaths
lp) [LitPaths]
lps
                        , runClause :: Clause -> [LitPaths] -> LitPaths
runClause = \Clause
_ [LitPaths]
lps -> [LitPaths] -> LitPaths
forall a. Monoid a => [a] -> a
mconcat [LitPaths]
lps
                        , runLit :: Lit -> LitPaths
runLit    = \Lit
lit -> HashMap Lit [Path] -> LitPaths
LitPaths (HashMap Lit [Path] -> LitPaths) -> HashMap Lit [Path] -> LitPaths
forall a b. (a -> b) -> a -> b
$ Lit -> [Path] -> HashMap Lit [Path]
forall k v. Hashable k => k -> v -> HashMap k v
HashMap.singleton Lit
lit [Path
EmptyPath]
                         }

_getLitPaths :: CNF -> LitPaths
_getLitPaths :: CNF -> LitPaths
_getLitPaths = CNFAlg LitPaths -> CNF -> LitPaths
forall a m. FoldAlg a => CNFAlg m -> a -> m
foldAlg CNFAlg LitPaths
getLitPathsAlg

-------------------------------------------------------------------
------------------------- ECTA conversion -------------------------
-------------------------------------------------------------------

aNode :: Node
aNode :: Node
aNode = [Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge Symbol
"a" []]

bNode :: Node
bNode :: Node
bNode = [Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge Symbol
"b" []]

falseNode :: Node
falseNode :: Node
falseNode = [Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge Symbol
"0" []]

trueNode :: Node
trueNode :: Node
trueNode = [Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge Symbol
"1" []]

falseTerm :: Term
falseTerm :: Term
falseTerm = [Term] -> Term
forall a. [a] -> a
head ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ Node -> [Term]
naiveDenotation Node
falseNode

trueTerm :: Term
trueTerm :: Term
trueTerm = [Term] -> Term
forall a. [a] -> a
head ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ Node -> [Term]
naiveDenotation Node
trueNode

_trueOrFalseNode :: Node
_trueOrFalseNode :: Node
_trueOrFalseNode = [Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge Symbol
"0" [], Symbol -> [Node] -> Edge
Edge Symbol
"1" []]

posVarNode :: Node
posVarNode :: Node
posVarNode = [Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge Symbol
"" [Node
falseNode, Node
aNode], Symbol -> [Node] -> Edge
Edge Symbol
"" [Node
trueNode, Node
bNode]]

negVarNode :: Node
negVarNode :: Node
negVarNode = [Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge Symbol
"" [Node
falseNode, Node
bNode], Symbol -> [Node] -> Edge
Edge Symbol
"" [Node
trueNode, Node
aNode]]



-- | Encoding:
--   formula(assnNode, formulaNode)
--
-- assnNode:
--  * One edge, with one child per literal (2*numVars total)
--  * Each literal has two choices, true or false
--  * Use constraints to force each positive/negative pair of literals to match.
--     * E.g.: x1 node = choice of (0, a) or (1, b). ~x1 node = choice of (0, b) or (1, a)
--             If x1/~x1 have indices 0/1, then the constraint 0.1=1.1 constrains
--             x1/~x1 to be either true/false or false/true
--
-- formulaNode:
--  * One edge, having one child per clause
--
-- Clause nodes:
--  * One edge per literal in the clause, each corresponding to a choice of which variable
--    makes the clause true.
--  * Each edge has 2*numVars children containing a copy of the assnNode, followed by
--    a single child containing "1"
--  * Constrain said final child to be equal to the truth value of the corresponding literal
--    in those 2*numVars children which copy the assnNode
--
-- Top level constraints:
--  * Constrain the variable nodes in each clause node to be equal to the global variable assignments.

toEcta :: CNF -> Node
toEcta :: CNF -> Node
toEcta CNF
formula = [Edge] -> Node
Node [Symbol -> [Node] -> EqConstraints -> Edge
mkEdge Symbol
"formula" [Node
assnNode, Node
formulaNode] EqConstraints
litCopyingConstraints]
  where
    clauses :: [Clause]
    And [Clause]
clauses = CNF
formula

    numClauses :: Int
    numClauses :: Int
numClauses = [Clause] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Clause]
clauses

    sortedVars :: [Var]
    sortedVars :: [Var]
sortedVars = [Var] -> [Var]
forall a. Ord a => [a] -> [a]
sort ([Var] -> [Var]) -> [Var] -> [Var]
forall a b. (a -> b) -> a -> b
$ HashSet Var -> [Var]
forall a. HashSet a -> [a]
HashSet.toList (HashSet Var -> [Var]) -> HashSet Var -> [Var]
forall a b. (a -> b) -> a -> b
$ CNF -> HashSet Var
getVars CNF
formula

    numVars :: Int
    numVars :: Int
numVars = [Var] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
sortedVars

    litToIndex :: Lit -> Int
    litToIndex :: Lit -> Int
litToIndex (PosLit Var
v) = Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust (Var -> [Var] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex Var
v [Var]
sortedVars)
    litToIndex (NegLit Var
v) = Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust (Var -> [Var] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
elemIndex Var
v [Var]
sortedVars) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1

    assnNode :: Node
    assnNode :: Node
assnNode = [Edge] -> Node
Node [Symbol -> [Node] -> EqConstraints -> Edge
mkEdge Symbol
"assignment" ((Var -> [Node]) -> [Var] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Node] -> Var -> [Node]
forall a b. a -> b -> a
const [Node
posVarNode, Node
negVarNode]) [Var]
sortedVars)
                                         ([[Path]] -> EqConstraints
mkEqConstraints ([[Path]] -> EqConstraints) -> [[Path]] -> EqConstraints
forall a b. (a -> b) -> a -> b
$ (Int -> [Path]) -> [Int] -> [[Path]]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> [[Int] -> Path
path [Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
i, Int
1], [Int] -> Path
path [Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1, Int
1]])
                                                                [Int
0..Int
numVars Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1])
                    ]

    formulaNode :: Node
    formulaNode :: Node
formulaNode = [Edge] -> Node
Node [Symbol -> [Node] -> Edge
Edge Symbol
"clauses" ((Clause -> Node) -> [Clause] -> [Node]
forall a b. (a -> b) -> [a] -> [b]
map Clause -> Node
mkClauseNode [Clause]
clauses)]

    mkClauseNode :: Clause -> Node
    mkClauseNode :: Clause -> Node
mkClauseNode (Or [Lit]
lits) = [Edge] -> Node
Node ((Lit -> Edge) -> [Lit] -> [Edge]
forall a b. (a -> b) -> [a] -> [b]
map Lit -> Edge
mkLitChoiceEdge [Lit]
lits)
      where
        mkLitChoiceEdge :: Lit -> Edge
        mkLitChoiceEdge :: Lit -> Edge
mkLitChoiceEdge Lit
lit = Symbol -> [Node] -> EqConstraints -> Edge
mkEdge (Text -> Symbol
Symbol (Text -> Symbol) -> Text -> Symbol
forall a b. (a -> b) -> a -> b
$ Text
"choice[" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Lit -> Text
forall a. Pretty a => a -> Text
pretty Lit
lit Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"]")
                                      ((Var -> [Node]) -> [Var] -> [Node]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Node] -> Var -> [Node]
forall a b. a -> b -> a
const [Node
posVarNode, Node
negVarNode]) [Var]
sortedVars [Node] -> [Node] -> [Node]
forall a. [a] -> [a] -> [a]
++ [Node
trueNode])
                                      ([[Path]] -> EqConstraints
mkEqConstraints [[[Int] -> Path
path [Lit -> Int
litToIndex Lit
lit, Int
0],  [Int] -> Path
path [Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
numVars]]])


    litCopyingConstraints :: EqConstraints
    litCopyingConstraints :: EqConstraints
litCopyingConstraints = [[Path]] -> EqConstraints
mkEqConstraints [[Int] -> Path
path [Int
0, Int
i] Path -> [Path] -> [Path]
forall a. a -> [a] -> [a]
: [[Int] -> Path
path [Int
1, Int
c, Int
i] | Int
c <- [Int
0..Int
numClausesInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1]]
                                               | Int
i <- [Int
0..Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
numVars Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
                                            ]


allSolutions :: CNF -> HashSet (HashMap Var Bool)
allSolutions :: CNF -> HashSet (HashMap Var Bool)
allSolutions CNF
formula = (Term -> HashSet (HashMap Var Bool))
-> [Term] -> HashSet (HashMap Var Bool)
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (HashMap Var Bool -> HashSet (HashMap Var Bool)
forall a. Hashable a => a -> HashSet a
HashSet.singleton (HashMap Var Bool -> HashSet (HashMap Var Bool))
-> (Term -> HashMap Var Bool) -> Term -> HashSet (HashMap Var Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> HashMap Var Bool
termToAssignment) ([Term] -> HashSet (HashMap Var Bool))
-> [Term] -> HashSet (HashMap Var Bool)
forall a b. (a -> b) -> a -> b
$ Node -> [Term]
getAllTerms (Node -> [Term]) -> Node -> [Term]
forall a b. (a -> b) -> a -> b
$ (Node -> Node) -> Node -> Node
forall a. Eq a => (a -> a) -> a -> a
fixUnbounded Node -> Node
reducePartially (Node -> Node) -> Node -> Node
forall a b. (a -> b) -> a -> b
$ CNF -> Node
toEcta CNF
formula
  where
    sortedVars :: [Var]
    sortedVars :: [Var]
sortedVars = [Var] -> [Var]
forall a. Ord a => [a] -> [a]
sort ([Var] -> [Var]) -> [Var] -> [Var]
forall a b. (a -> b) -> a -> b
$ HashSet Var -> [Var]
forall a. HashSet a -> [a]
HashSet.toList (HashSet Var -> [Var]) -> HashSet Var -> [Var]
forall a b. (a -> b) -> a -> b
$ CNF -> HashSet Var
getVars CNF
formula

    evens :: [a] -> [a]
    evens :: [a] -> [a]
evens []       = []
    evens [a
x]      = [a
x]
    evens (a
x:a
_:[a]
l) = a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a] -> [a]
forall a. [a] -> [a]
evens [a]
l

    termToAssignment :: Term -> HashMap Var Bool
    termToAssignment :: Term -> HashMap Var Bool
termToAssignment (Term Symbol
_ [Term Symbol
_ [Term]
litVals, Term
_]) = ((Var, Term) -> HashMap Var Bool)
-> [(Var, Term)] -> HashMap Var Bool
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\(Var
var, Term Symbol
"" [Term
val, Term
_]) -> Var -> Bool -> HashMap Var Bool
forall k v. Hashable k => k -> v -> HashMap k v
HashMap.singleton Var
var (Term -> Bool
termToBool Term
val))
                                                            ([Var] -> [Term] -> [(Var, Term)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
sortedVars ([Term] -> [Term]
forall a. [a] -> [a]
evens [Term]
litVals))
    termToAssignment Term
x    = String -> HashMap Var Bool
forall a. HasCallStack => String -> a
error (String -> HashMap Var Bool) -> String -> HashMap Var Bool
forall a b. (a -> b) -> a -> b
$ String
"Unexpected " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Term -> String
forall a. Show a => a -> String
show Term
x

    termToBool :: Term -> Bool
    termToBool :: Term -> Bool
termToBool Term
t | Term
t Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
falseTerm = Bool
False
                 | Term
t Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
trueTerm  = Bool
True
                 | Bool
otherwise      = String -> Bool
forall a. HasCallStack => String -> a
error String
"termToBool: Invalid argument"


-------------------------------------------------------------------
------------------------ Example formulae -------------------------
-------------------------------------------------------------------

-- Naive generation: 2^30 * 3^4 possibilities
ex1 :: CNF
ex1 :: CNF
ex1 = [Clause] -> CNF
And [ [Lit] -> Clause
Or [Var -> Lit
PosLit Var
"x1", Var -> Lit
PosLit Var
"x2", Var -> Lit
PosLit Var
"x3"]
          , [Lit] -> Clause
Or [Var -> Lit
NegLit Var
"x1", Var -> Lit
PosLit Var
"x2", Var -> Lit
PosLit Var
"x3"]
          , [Lit] -> Clause
Or [Var -> Lit
PosLit Var
"x1", Var -> Lit
NegLit Var
"x2", Var -> Lit
PosLit Var
"x3"]
          , [Lit] -> Clause
Or [Var -> Lit
PosLit Var
"x1", Var -> Lit
PosLit Var
"x2", Var -> Lit
NegLit Var
"x3"]
          ]

-- Naive generation: 2^14
ex2 :: CNF
ex2 :: CNF
ex2 = [Clause] -> CNF
And [ [Lit] -> Clause
Or [Var -> Lit
PosLit Var
"x1", Var -> Lit
PosLit Var
"x2"]
          , [Lit] -> Clause
Or [Var -> Lit
NegLit Var
"x1", Var -> Lit
NegLit Var
"x2"]
          ]


-- Partial reduction of the ECTA effectively performs unit propagation, solving this quickly.
ex3 :: CNF
ex3 :: CNF
ex3 = [Clause] -> CNF
And [ [Lit] -> Clause
Or [Var -> Lit
NegLit Var
"x1"]
          , [Lit] -> Clause
Or [Var -> Lit
PosLit Var
"x1", Var -> Lit
PosLit Var
"x2"]
          , [Lit] -> Clause
Or [Var -> Lit
NegLit Var
"x2", Var -> Lit
PosLit Var
"x3"]
          ]