module Data.Algorithm.SatSolver.Fml.Some (
fml1
, fml2
, fml3
, fml4
, fml5
, fml6
, fml7
, fml8
, fml9
, fml10
, fml11
, fmlEvt1
, fmlEvt2
) where
import qualified Data.Algorithm.SatSolver.Clause as Clause
import qualified Data.Algorithm.SatSolver.Fml as Fml
import qualified Data.Algorithm.SatSolver.Lit.Some as Lit.Some
fml1 :: Fml.Fml Int
fml1 = Fml.mk []
fml2 :: Fml.Fml Int
fml2 = Fml.mk [c1]
where
c1 = Clause.mk [Lit.Some.posLit1, Lit.Some.negLit2, Lit.Some.negLit3, Lit.Some.posLit4]
fml3 :: Fml.Fml Int
fml3 = Fml.mk [c1, c2, c3, c4, c5, c6, c7]
where
c1 = Clause.mk [Lit.Some.posLit1, Lit.Some.negLit3]
c2 = Clause.mk [Lit.Some.posLit1, Lit.Some.posLit4, Lit.Some.negLit5]
c3 = Clause.mk [Lit.Some.posLit2, Lit.Some.posLit3, Lit.Some.posLit4]
c4 = Clause.mk [Lit.Some.negLit1, Lit.Some.negLit3, Lit.Some.negLit5]
c5 = Clause.mk [Lit.Some.posLit4, Lit.Some.posLit5]
c6 = Clause.mk [Lit.Some.negLit3, Lit.Some.negLit4, Lit.Some.posLit5]
c7 = Clause.mk [Lit.Some.posLit2]
fml4 :: Fml.Fml Int
fml4 = Fml.mk [c1, c2, c3]
where
c1 = Clause.mk [Lit.Some.posLit1, Lit.Some.negLit3, Lit.Some.negLit1]
c2 = Clause.mk [Lit.Some.posLit1, Lit.Some.posLit4, Lit.Some.negLit5, Lit.Some.posLit6, Lit.Some.negLit7]
c3 = Clause.mk [Lit.Some.posLit2, Lit.Some.posLit3, Lit.Some.posLit4, Lit.Some.posLit8, Lit.Some.posLit9]
fml5 = Fml.mk [c1, c2, c3, c4, c5]
where
c1 = Clause.mk [Lit.Some.posLit1, Lit.Some.negLit2]
c2 = Clause.mk [Lit.Some.posLit1, Lit.Some.posLit4]
c3 = Clause.mk [Lit.Some.posLit8, Lit.Some.posLit9]
c4 = Clause.mk [Lit.Some.negLit1, Lit.Some.negLit8]
c5 = Clause.mk [Lit.Some.posLit4, Lit.Some.posLit5]
fml6 :: Fml.Fml Int
fml6 = Fml.mk [c1, c2, c3, c4]
where
c1 = Clause.mk [Lit.Some.posLit1, Lit.Some.posLit2]
c2 = Clause.mk [Lit.Some.negLit1, Lit.Some.posLit2]
c3 = Clause.mk [Lit.Some.posLit1, Lit.Some.negLit2]
c4 = Clause.mk [Lit.Some.negLit1, Lit.Some.negLit2]
fml7 :: Fml.Fml Int
fml7 = Fml.mk [c1, c2, c3, c4, c5, c6, c7, c8, c9]
where
c1 = Clause.mk [Lit.Some.posLit1]
c2 = Clause.mk [Lit.Some.negLit2]
c3 = Clause.mk [Lit.Some.posLit3]
c4 = Clause.mk [Lit.Some.posLit4]
c5 = Clause.mk [Lit.Some.negLit5]
c6 = Clause.mk [Lit.Some.posLit6]
c7 = Clause.mk [Lit.Some.negLit7]
c8 = Clause.mk [Lit.Some.negLit8]
c9 = Clause.mk [Lit.Some.negLit9]
fml8 :: Fml.Fml Int
fml8 = Fml.mk [c1, c2, c3, c4, c5, c6, c7, c8, c9]
where
c1 = Clause.mk [Lit.Some.posLit1, Lit.Some.posLit2]
c2 = Clause.mk [Lit.Some.posLit2, Lit.Some.negLit3]
c3 = Clause.mk [Lit.Some.negLit3, Lit.Some.posLit4]
c4 = Clause.mk [Lit.Some.posLit4, Lit.Some.negLit5]
c5 = Clause.mk [Lit.Some.negLit5, Lit.Some.posLit6]
c6 = Clause.mk [Lit.Some.posLit6, Lit.Some.negLit7]
c7 = Clause.mk [Lit.Some.negLit7, Lit.Some.posLit8]
c8 = Clause.mk [Lit.Some.posLit8, Lit.Some.negLit9]
c9 = Clause.mk [Lit.Some.negLit9, Lit.Some.negLit1]
fml9 :: Fml.Fml Int
fml9 = Fml.mk [c1, c2, c3, c4, c5, c6, c7, c8, c9]
where
c1 = Clause.mk [Lit.Some.posLit1]
c2 = Clause.mk [Lit.Some.negLit2]
c3 = Clause.mk [Lit.Some.posLit3]
c4 = Clause.mk [Lit.Some.negLit1, Lit.Some.posLit2, Lit.Some.negLit4]
c5 = Clause.mk [Lit.Some.negLit3, Lit.Some.negLit5]
c6 = Clause.mk [Lit.Some.posLit4, Lit.Some.posLit5, Lit.Some.negLit6]
c7 = Clause.mk [Lit.Some.posLit6, Lit.Some.posLit7]
c8 = Clause.mk [Lit.Some.negLit7, Lit.Some.posLit8]
c9 = Clause.mk [Lit.Some.negLit8, Lit.Some.posLit9]
fml10 :: Fml.Fml Int
fml10 = Fml.mk [c1, c2, c3, c4, c5, c6, c7, c8, c9]
where
c1 = Clause.mk [Lit.Some.posLit1]
c2 = Clause.mk [Lit.Some.posLit2]
c3 = Clause.mk [Lit.Some.posLit3]
c4 = Clause.mk [Lit.Some.negLit1, Lit.Some.posLit4]
c5 = Clause.mk [Lit.Some.negLit2, Lit.Some.posLit5]
c6 = Clause.mk [Lit.Some.negLit3, Lit.Some.posLit6]
c7 = Clause.mk [Lit.Some.negLit4, Lit.Some.posLit7]
c8 = Clause.mk [Lit.Some.negLit5, Lit.Some.posLit8]
c9 = Clause.mk [Lit.Some.negLit7, Lit.Some.negLit8]
fml11 :: Fml.Fml Int
fml11 = Fml.mk [c1, c2, c3, c4, c5, c6, c7, c8, c9]
where
c1 = Clause.mk [Lit.Some.posLit1, Lit.Some.posLit2]
c2 = Clause.mk [Lit.Some.negLit2, Lit.Some.negLit3]
c3 = Clause.mk [Lit.Some.posLit3, Lit.Some.posLit4]
c4 = Clause.mk [Lit.Some.negLit4, Lit.Some.negLit5]
c5 = Clause.mk [Lit.Some.posLit5, Lit.Some.posLit6]
c6 = Clause.mk [Lit.Some.negLit6, Lit.Some.negLit7]
c7 = Clause.mk [Lit.Some.posLit7, Lit.Some.posLit8]
c8 = Clause.mk [Lit.Some.negLit8, Lit.Some.negLit9]
c9 = Clause.mk [Lit.Some.posLit9, Lit.Some.negLit1]
fmlEvt1 :: Fml.Fml String
fmlEvt1 = Fml.mk [c1, c2, c3]
where
c1 = Clause.mk [Lit.Some.posLitEvtA, Lit.Some.posLitEvtB]
c2 = Clause.mk [Lit.Some.negLitEvtA, Lit.Some.posLitEvtC]
c3 = Clause.mk [Lit.Some.posLitEvtA, Lit.Some.negLitEvtB, Lit.Some.negLitEvtC]
fmlEvt2 :: Fml.Fml String
fmlEvt2 = Fml.mk [c1, c2, c3, c4]
where
c1 = Clause.mk [Lit.Some.posLitEvtA]
c2 = Clause.mk [Lit.Some.negLitEvtA, Lit.Some.posLitEvtB]
c3 = Clause.mk [Lit.Some.negLitEvtB, Lit.Some.negLitEvtC]
c4 = Clause.mk [Lit.Some.negLitEvtA, Lit.Some.negLitEvtB, Lit.Some.posLitEvtC]