{-# LANGUAGE OverloadedStrings #-}
module Application.SAT (
Var
, mkVar
, CNF(..)
, Clause(..)
, Lit(..)
, toEcta
, allSolutions
, 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
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)
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
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))
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
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]]
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"
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"]
]
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"]
]
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"]
]