-- | The Davis-Putnam and Davis-Putnam-Loveland-Logemann procedures.
--
-- Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}

module Data.Logic.ATP.DP
    ( dp,   dpsat,   dptaut
    , dpli, dplisat, dplitaut
    , dpll, dpllsat, dplltaut
    , dplb, dplbsat, dplbtaut
    , testDP
    ) where

import Data.Logic.ATP.DefCNF (NumAtom(ai, ma), defcnfs)
import Data.Logic.ATP.Formulas (IsFormula(AtomOf))
import Data.Logic.ATP.Lib (Failing(Success, Failure), failing, allpairs, minimize, maximize, defined, (|->), setmapfilter, flatten)
import Data.Logic.ATP.Lit (IsLiteral, (.~.), negative, positive, negate, negated)
import Data.Logic.ATP.Prop (trivial, JustPropositional, PFormula)
import Data.Logic.ATP.PropExamples (Knows(K), prime)
import Data.Map.Strict as Map (empty, Map)
import Data.Set as Set (delete, difference, empty, filter, findMin, fold, insert, intersection, map, member,
                        minView, null, partition, Set, singleton, size, union)
import Prelude hiding (negate, pure)
import Test.HUnit

instance NumAtom (Knows Integer) where
    ma :: Integer -> Knows Integer
ma Integer
n = String -> Integer -> Maybe Integer -> Knows Integer
forall a. String -> a -> Maybe a -> Knows a
K String
"p" Integer
n Maybe Integer
forall a. Maybe a
Nothing
    ai :: Knows Integer -> Integer
ai (K String
_ Integer
n Maybe Integer
_) = Integer
n

-- | The DP procedure.
dp :: (IsLiteral lit, Ord lit) => Set (Set lit) -> Bool
dp :: forall lit. (IsLiteral lit, Ord lit) => Set (Set lit) -> Bool
dp Set (Set lit)
clauses
  | Set (Set lit) -> Bool
forall a. Set a -> Bool
Set.null Set (Set lit)
clauses = Bool
True
  | Set lit -> Set (Set lit) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Set lit
forall a. Set a
Set.empty Set (Set lit)
clauses = Bool
False
  | Bool
otherwise = Bool
try1
  where
    try1 :: Bool
    try1 :: Bool
try1 = ([String] -> Bool)
-> (Set (Set lit) -> Bool) -> Failing (Set (Set lit)) -> Bool
forall b a. ([String] -> b) -> (a -> b) -> Failing a -> b
failing (Bool -> [String] -> Bool
forall a b. a -> b -> a
const Bool
try2) Set (Set lit) -> Bool
forall lit. (IsLiteral lit, Ord lit) => Set (Set lit) -> Bool
dp (Set (Set lit) -> Failing (Set (Set lit))
forall lit.
(IsLiteral lit, Ord lit) =>
Set (Set lit) -> Failing (Set (Set lit))
one_literal_rule Set (Set lit)
clauses)
    try2 :: Bool
    try2 :: Bool
try2 = ([String] -> Bool)
-> (Set (Set lit) -> Bool) -> Failing (Set (Set lit)) -> Bool
forall b a. ([String] -> b) -> (a -> b) -> Failing a -> b
failing (Bool -> [String] -> Bool
forall a b. a -> b -> a
const Bool
try3) Set (Set lit) -> Bool
forall lit. (IsLiteral lit, Ord lit) => Set (Set lit) -> Bool
dp (Set (Set lit) -> Failing (Set (Set lit))
forall lit.
(IsLiteral lit, Ord lit) =>
Set (Set lit) -> Failing (Set (Set lit))
affirmative_negative_rule Set (Set lit)
clauses)
    try3 :: Bool
    try3 :: Bool
try3 = Set (Set lit) -> Bool
forall lit. (IsLiteral lit, Ord lit) => Set (Set lit) -> Bool
dp (Set (Set lit) -> Set (Set lit)
forall lit.
(IsLiteral lit, Ord lit) =>
Set (Set lit) -> Set (Set lit)
resolution_rule Set (Set lit)
clauses)

one_literal_rule :: (IsLiteral lit, Ord lit) => Set (Set lit) -> Failing (Set (Set lit))
one_literal_rule :: forall lit.
(IsLiteral lit, Ord lit) =>
Set (Set lit) -> Failing (Set (Set lit))
one_literal_rule Set (Set lit)
clauses =
    case Set (Set lit) -> Maybe (Set lit, Set (Set lit))
forall a. Set a -> Maybe (a, Set a)
Set.minView ((Set lit -> Bool) -> Set (Set lit) -> Set (Set lit)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\ Set lit
cl -> Set lit -> Int
forall a. Set a -> Int
Set.size Set lit
cl Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1) Set (Set lit)
clauses) of
      Maybe (Set lit, Set (Set lit))
Nothing -> [String] -> Failing (Set (Set lit))
forall a. [String] -> Failing a
Failure [String
"one_literal_rule"]
      Just (Set lit
s, Set (Set lit)
_) ->
          let u :: lit
u = Set lit -> lit
forall a. Set a -> a
Set.findMin Set lit
s in
          let u' :: lit
u' = lit -> lit
forall formula. IsLiteral formula => formula -> formula
(.~.) lit
u in
          let clauses1 :: Set (Set lit)
clauses1 = (Set lit -> Bool) -> Set (Set lit) -> Set (Set lit)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\ Set lit
cl -> Bool -> Bool
not (lit -> Set lit -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member lit
u Set lit
cl)) Set (Set lit)
clauses in
          Set (Set lit) -> Failing (Set (Set lit))
forall a. a -> Failing a
Success ((Set lit -> Set lit) -> Set (Set lit) -> Set (Set lit)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ Set lit
cl -> lit -> Set lit -> Set lit
forall a. Ord a => a -> Set a -> Set a
Set.delete lit
u' Set lit
cl) Set (Set lit)
clauses1)

affirmative_negative_rule :: (IsLiteral lit, Ord lit) => Set (Set lit) -> Failing (Set (Set lit))
affirmative_negative_rule :: forall lit.
(IsLiteral lit, Ord lit) =>
Set (Set lit) -> Failing (Set (Set lit))
affirmative_negative_rule Set (Set lit)
clauses =
  let (Set lit
neg',Set lit
pos) = (lit -> Bool) -> Set lit -> (Set lit, Set lit)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition lit -> Bool
forall formula. IsLiteral formula => formula -> Bool
negative (Set (Set lit) -> Set lit
forall a. Ord a => Set (Set a) -> Set a
flatten Set (Set lit)
clauses) in
  let neg :: Set lit
neg = (lit -> lit) -> Set lit -> Set lit
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map lit -> lit
forall formula. IsLiteral formula => formula -> formula
(.~.) Set lit
neg' in
  let pos_only :: Set lit
pos_only = Set lit -> Set lit -> Set lit
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set lit
pos Set lit
neg
      neg_only :: Set lit
neg_only = Set lit -> Set lit -> Set lit
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set lit
neg Set lit
pos in
  let pure :: Set lit
pure = Set lit -> Set lit -> Set lit
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set lit
pos_only ((lit -> lit) -> Set lit -> Set lit
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map lit -> lit
forall formula. IsLiteral formula => formula -> formula
(.~.) Set lit
neg_only) in
  if Set lit -> Bool
forall a. Set a -> Bool
Set.null Set lit
pure
  then [String] -> Failing (Set (Set lit))
forall a. [String] -> Failing a
Failure [String
"affirmative_negative_rule"]
  else Set (Set lit) -> Failing (Set (Set lit))
forall a. a -> Failing a
Success ((Set lit -> Bool) -> Set (Set lit) -> Set (Set lit)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\ Set lit
cl -> Set lit -> Bool
forall a. Set a -> Bool
Set.null (Set lit -> Set lit -> Set lit
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set lit
cl Set lit
pure)) Set (Set lit)
clauses)

resolve_on :: (IsLiteral lit, Ord lit) => lit -> Set (Set lit) -> Set (Set lit)
resolve_on :: forall lit.
(IsLiteral lit, Ord lit) =>
lit -> Set (Set lit) -> Set (Set lit)
resolve_on lit
p Set (Set lit)
clauses =
  let p' :: lit
p' = lit -> lit
forall formula. IsLiteral formula => formula -> formula
(.~.) lit
p
      (Set (Set lit)
pos,Set (Set lit)
notpos) = (Set lit -> Bool)
-> Set (Set lit) -> (Set (Set lit), Set (Set lit))
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition (lit -> Set lit -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member lit
p) Set (Set lit)
clauses in
  let (Set (Set lit)
neg,Set (Set lit)
other) = (Set lit -> Bool)
-> Set (Set lit) -> (Set (Set lit), Set (Set lit))
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition (lit -> Set lit -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member lit
p') Set (Set lit)
notpos in
  let pos' :: Set (Set lit)
pos' = (Set lit -> Set lit) -> Set (Set lit) -> Set (Set lit)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((lit -> Bool) -> Set lit -> Set lit
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\ lit
l -> lit
l lit -> lit -> Bool
forall a. Eq a => a -> a -> Bool
/= lit
p)) Set (Set lit)
pos
      neg' :: Set (Set lit)
neg' = (Set lit -> Set lit) -> Set (Set lit) -> Set (Set lit)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((lit -> Bool) -> Set lit -> Set lit
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\ lit
l -> lit
l lit -> lit -> Bool
forall a. Eq a => a -> a -> Bool
/= lit
p')) Set (Set lit)
neg in
  let res0 :: Set (Set lit)
res0 = (Set lit -> Set lit -> Set lit)
-> Set (Set lit) -> Set (Set lit) -> Set (Set lit)
forall a b c (set :: * -> *).
(SetLike set, Ord c) =>
(a -> b -> c) -> set a -> set b -> set c
allpairs Set lit -> Set lit -> Set lit
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (Set lit)
pos' Set (Set lit)
neg' in
  Set (Set lit) -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (Set lit)
other ((Set lit -> Bool) -> Set (Set lit) -> Set (Set lit)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool) -> (Set lit -> Bool) -> Set lit -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set lit -> Bool
forall lit. (Ord lit, IsLiteral lit) => Set lit -> Bool
trivial) Set (Set lit)
res0)

resolution_blowup :: (IsLiteral lit, Ord lit) => Set (Set lit) -> lit -> Int
resolution_blowup :: forall lit. (IsLiteral lit, Ord lit) => Set (Set lit) -> lit -> Int
resolution_blowup Set (Set lit)
cls lit
l =
  let m :: Int
m = Set (Set lit) -> Int
forall a. Set a -> Int
Set.size ((Set lit -> Bool) -> Set (Set lit) -> Set (Set lit)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (lit -> Set lit -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member lit
l) Set (Set lit)
cls)
      n :: Int
n = Set (Set lit) -> Int
forall a. Set a -> Int
Set.size ((Set lit -> Bool) -> Set (Set lit) -> Set (Set lit)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (lit -> Set lit -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (lit -> lit
forall formula. IsLiteral formula => formula -> formula
(.~.) lit
l)) Set (Set lit)
cls) in
  Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n

resolution_rule :: (IsLiteral lit, Ord lit) => Set (Set lit) -> Set (Set lit)
resolution_rule :: forall lit.
(IsLiteral lit, Ord lit) =>
Set (Set lit) -> Set (Set lit)
resolution_rule Set (Set lit)
clauses = lit -> Set (Set lit) -> Set (Set lit)
forall lit.
(IsLiteral lit, Ord lit) =>
lit -> Set (Set lit) -> Set (Set lit)
resolve_on lit
p Set (Set lit)
clauses
    where
      pvs :: Set lit
pvs = (lit -> Bool) -> Set lit -> Set lit
forall a. (a -> Bool) -> Set a -> Set a
Set.filter lit -> Bool
forall formula. IsLiteral formula => formula -> Bool
positive (Set (Set lit) -> Set lit
forall a. Ord a => Set (Set a) -> Set a
flatten Set (Set lit)
clauses)
      Just lit
p = (lit -> Int) -> Set lit -> Maybe lit
forall b (s :: * -> *) a.
(Ord b, SetLike s, Foldable s) =>
(a -> b) -> s a -> Maybe a
minimize (Set (Set lit) -> lit -> Int
forall lit. (IsLiteral lit, Ord lit) => Set (Set lit) -> lit -> Int
resolution_blowup Set (Set lit)
clauses) Set lit
pvs

-- | Davis-Putnam satisfiability tester.
dpsat :: (JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> Bool
dpsat :: forall pf.
(JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
pf -> Bool
dpsat = Set (Set (LFormula (AtomOf pf))) -> Bool
forall lit. (IsLiteral lit, Ord lit) => Set (Set lit) -> Bool
dp (Set (Set (LFormula (AtomOf pf))) -> Bool)
-> (pf -> Set (Set (LFormula (AtomOf pf)))) -> pf -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. pf -> Set (Set (LFormula (AtomOf pf)))
forall pf.
(IsPropositional pf, JustPropositional pf, Ord pf,
 NumAtom (AtomOf pf)) =>
pf -> Set (Set (LFormula (AtomOf pf)))
defcnfs

-- | Davis-Putnam tautology checker.
dptaut :: (JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> Bool
dptaut :: forall pf.
(JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
pf -> Bool
dptaut = Bool -> Bool
not (Bool -> Bool) -> (pf -> Bool) -> pf -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. pf -> Bool
forall pf.
(JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
pf -> Bool
dpsat (pf -> Bool) -> (pf -> pf) -> pf -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. pf -> pf
forall formula. IsLiteral formula => formula -> formula
negate

-- Examples.

test01 :: Test
test01 :: Test
test01 = Assertion -> Test
TestCase (String -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"dptaut(prime 11) p. 84" Bool
True (PFormula (Knows Integer) -> Bool
forall pf.
(JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
pf -> Bool
dptaut (Integer -> PFormula (Knows Integer)
forall formula.
(IsPropositional formula, Ord formula,
 AtomOf formula ~ Knows Integer) =>
Integer -> formula
prime Integer
11 :: PFormula (Knows Integer))))

-- | The same thing but with the DPLL procedure. (p. 84)
dpll :: (IsLiteral lit, Ord lit) => Set (Set lit) -> Bool
dpll :: forall lit. (IsLiteral lit, Ord lit) => Set (Set lit) -> Bool
dpll Set (Set lit)
clauses
  | Set (Set lit) -> Bool
forall a. Set a -> Bool
Set.null Set (Set lit)
clauses = Bool
True
  | Set lit -> Set (Set lit) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Set lit
forall a. Set a
Set.empty Set (Set lit)
clauses = Bool
False
  | Bool
otherwise = Bool
try1
  where
    try1 :: Bool
try1 = ([String] -> Bool)
-> (Set (Set lit) -> Bool) -> Failing (Set (Set lit)) -> Bool
forall b a. ([String] -> b) -> (a -> b) -> Failing a -> b
failing (Bool -> [String] -> Bool
forall a b. a -> b -> a
const Bool
try2) Set (Set lit) -> Bool
forall lit. (IsLiteral lit, Ord lit) => Set (Set lit) -> Bool
dpll (Set (Set lit) -> Failing (Set (Set lit))
forall lit.
(IsLiteral lit, Ord lit) =>
Set (Set lit) -> Failing (Set (Set lit))
one_literal_rule Set (Set lit)
clauses)
    try2 :: Bool
try2 = ([String] -> Bool)
-> (Set (Set lit) -> Bool) -> Failing (Set (Set lit)) -> Bool
forall b a. ([String] -> b) -> (a -> b) -> Failing a -> b
failing (Bool -> [String] -> Bool
forall a b. a -> b -> a
const Bool
try3) Set (Set lit) -> Bool
forall lit. (IsLiteral lit, Ord lit) => Set (Set lit) -> Bool
dpll (Set (Set lit) -> Failing (Set (Set lit))
forall lit.
(IsLiteral lit, Ord lit) =>
Set (Set lit) -> Failing (Set (Set lit))
affirmative_negative_rule Set (Set lit)
clauses)
    try3 :: Bool
try3 = Set (Set lit) -> Bool
forall lit. (IsLiteral lit, Ord lit) => Set (Set lit) -> Bool
dpll (Set lit -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => a -> Set a -> Set a
Set.insert (lit -> Set lit
forall a. a -> Set a
Set.singleton lit
p) Set (Set lit)
clauses) Bool -> Bool -> Bool
|| Set (Set lit) -> Bool
forall lit. (IsLiteral lit, Ord lit) => Set (Set lit) -> Bool
dpll (Set lit -> Set (Set lit) -> Set (Set lit)
forall a. Ord a => a -> Set a -> Set a
Set.insert (lit -> Set lit
forall a. a -> Set a
Set.singleton (lit -> lit
forall formula. IsLiteral formula => formula -> formula
negate lit
p)) Set (Set lit)
clauses)
    Just lit
p = (lit -> Int) -> Set lit -> Maybe lit
forall b (s :: * -> *) a.
(Ord b, SetLike s, Foldable s) =>
(a -> b) -> s a -> Maybe a
maximize (Set (Set lit) -> lit -> Int
forall lit. (IsLiteral lit, Ord lit) => Set (Set lit) -> lit -> Int
posneg_count Set (Set lit)
clauses) Set lit
pvs
    pvs :: Set lit
pvs = (lit -> Bool) -> Set lit -> Set lit
forall a. (a -> Bool) -> Set a -> Set a
Set.filter lit -> Bool
forall formula. IsLiteral formula => formula -> Bool
positive (Set (Set lit) -> Set lit
forall a. Ord a => Set (Set a) -> Set a
flatten Set (Set lit)
clauses)
{-
  | failing (const try3)
  | otherwise =
      case one_literal_rule clauses >>= dpll of
        Success x -> Success x
        Failure _ ->
            case affirmative_negative_rule clauses >>= dpll of
              Success x -> Success x
              Failure _ ->
                  let pvs = Set.filter positive (flatten clauses) in
                  case maximize (posneg_count clauses) pvs of
                    Nothing -> Failure ["dpll"]
                    Just p ->
                        case (dpll (Set.insert (Set.singleton p) clauses), dpll (Set.insert (Set.singleton (negate p)) clauses)) of
                          (Success a, Success b) -> Success (a || b)
                          (Failure a, Failure b) -> Failure (a ++ b)
                          (Failure a, _) -> Failure a
                          (_, Failure b) -> Failure b
-}

posneg_count :: (IsLiteral formula, Ord formula) => Set (Set formula) -> formula -> Int
posneg_count :: forall lit. (IsLiteral lit, Ord lit) => Set (Set lit) -> lit -> Int
posneg_count Set (Set formula)
cls formula
l =
  let m :: Int
m = Set (Set formula) -> Int
forall a. Set a -> Int
Set.size((Set formula -> Bool) -> Set (Set formula) -> Set (Set formula)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (formula -> Set formula -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member formula
l) Set (Set formula)
cls)
      n :: Int
n = Set (Set formula) -> Int
forall a. Set a -> Int
Set.size((Set formula -> Bool) -> Set (Set formula) -> Set (Set formula)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (formula -> Set formula -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (formula -> formula
forall formula. IsLiteral formula => formula -> formula
negate formula
l)) Set (Set formula)
cls) in
  Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n

dpllsat :: (JustPropositional pf, Ord pf, AtomOf pf ~ Knows Integer) => pf -> Bool
dpllsat :: forall pf.
(JustPropositional pf, Ord pf, AtomOf pf ~ Knows Integer) =>
pf -> Bool
dpllsat = Set (Set (LFormula (Knows Integer))) -> Bool
forall lit. (IsLiteral lit, Ord lit) => Set (Set lit) -> Bool
dpll (Set (Set (LFormula (Knows Integer))) -> Bool)
-> (pf -> Set (Set (LFormula (Knows Integer)))) -> pf -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. pf -> Set (Set (LFormula (AtomOf pf)))
pf -> Set (Set (LFormula (Knows Integer)))
forall pf.
(IsPropositional pf, JustPropositional pf, Ord pf,
 NumAtom (AtomOf pf)) =>
pf -> Set (Set (LFormula (AtomOf pf)))
defcnfs

dplltaut :: (JustPropositional pf, Ord pf, AtomOf pf ~ Knows Integer) => pf -> Bool
dplltaut :: forall pf.
(JustPropositional pf, Ord pf, AtomOf pf ~ Knows Integer) =>
pf -> Bool
dplltaut = Bool -> Bool
not (Bool -> Bool) -> (pf -> Bool) -> pf -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. pf -> Bool
forall pf.
(JustPropositional pf, Ord pf, AtomOf pf ~ Knows Integer) =>
pf -> Bool
dpllsat (pf -> Bool) -> (pf -> pf) -> pf -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. pf -> pf
forall formula. IsLiteral formula => formula -> formula
negate

-- Example.
test02 :: Test
test02 :: Test
test02 = Assertion -> Test
TestCase (String -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"dplltaut(prime 11)" Bool
True (PFormula (Knows Integer) -> Bool
forall pf.
(JustPropositional pf, Ord pf, AtomOf pf ~ Knows Integer) =>
pf -> Bool
dplltaut (Integer -> PFormula (Knows Integer)
forall formula.
(IsPropositional formula, Ord formula,
 AtomOf formula ~ Knows Integer) =>
Integer -> formula
prime Integer
11 :: PFormula (Knows Integer))))

-- | Iterative implementation with explicit trail instead of recursion.
dpli :: (IsLiteral formula, Ord formula) => Set (formula, TrailMix) -> Set (Set formula) -> Bool
dpli :: forall formula.
(IsLiteral formula, Ord formula) =>
Set (formula, TrailMix) -> Set (Set formula) -> Bool
dpli Set (formula, TrailMix)
trail Set (Set formula)
cls =
  let (Set (Set formula)
cls', Set (formula, TrailMix)
trail') = (Set (Set formula), Set (formula, TrailMix))
-> (Set (Set formula), Set (formula, TrailMix))
forall t.
(IsLiteral t, Ord t) =>
(Set (Set t), Set (t, TrailMix))
-> (Set (Set t), Set (t, TrailMix))
unit_propagate (Set (Set formula)
cls, Set (formula, TrailMix)
trail) in
  if Set formula -> Set (Set formula) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Set formula
forall a. Set a
Set.empty Set (Set formula)
cls' then
    case Set (formula, TrailMix)
-> Maybe ((formula, TrailMix), Set (formula, TrailMix))
forall a. Set a -> Maybe (a, Set a)
Set.minView Set (formula, TrailMix)
trail of
      Just ((formula
p,TrailMix
Guessed), Set (formula, TrailMix)
tt) -> Set (formula, TrailMix) -> Set (Set formula) -> Bool
forall formula.
(IsLiteral formula, Ord formula) =>
Set (formula, TrailMix) -> Set (Set formula) -> Bool
dpli ((formula, TrailMix)
-> Set (formula, TrailMix) -> Set (formula, TrailMix)
forall a. Ord a => a -> Set a -> Set a
Set.insert (formula -> formula
forall formula. IsLiteral formula => formula -> formula
negate formula
p, TrailMix
Deduced) Set (formula, TrailMix)
tt) Set (Set formula)
cls
      Maybe ((formula, TrailMix), Set (formula, TrailMix))
_ -> Bool
False
  else
      case Set (Set formula) -> Set (formula, TrailMix) -> Set formula
forall formula.
(IsLiteral formula, Ord formula, Eq formula) =>
Set (Set formula) -> Set (formula, TrailMix) -> Set formula
unassigned Set (Set formula)
cls (Set (formula, TrailMix)
trail' {-:: Set (pf, TrailMix)-}) of
        Set formula
s | Set formula -> Bool
forall a. Set a -> Bool
Set.null Set formula
s -> Bool
True
        Set formula
ps -> let Just formula
p = (formula -> Int) -> Set formula -> Maybe formula
forall b (s :: * -> *) a.
(Ord b, SetLike s, Foldable s) =>
(a -> b) -> s a -> Maybe a
maximize (Set (Set formula) -> formula -> Int
forall lit. (IsLiteral lit, Ord lit) => Set (Set lit) -> lit -> Int
posneg_count Set (Set formula)
cls') Set formula
ps in
              Set (formula, TrailMix) -> Set (Set formula) -> Bool
forall formula.
(IsLiteral formula, Ord formula) =>
Set (formula, TrailMix) -> Set (Set formula) -> Bool
dpli ((formula, TrailMix)
-> Set (formula, TrailMix) -> Set (formula, TrailMix)
forall a. Ord a => a -> Set a -> Set a
Set.insert (formula
p {-:: pf-}, TrailMix
Guessed) Set (formula, TrailMix)
trail') Set (Set formula)
cls

data TrailMix = Guessed | Deduced deriving (TrailMix -> TrailMix -> Bool
(TrailMix -> TrailMix -> Bool)
-> (TrailMix -> TrailMix -> Bool) -> Eq TrailMix
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TrailMix -> TrailMix -> Bool
== :: TrailMix -> TrailMix -> Bool
$c/= :: TrailMix -> TrailMix -> Bool
/= :: TrailMix -> TrailMix -> Bool
Eq, Eq TrailMix
Eq TrailMix =>
(TrailMix -> TrailMix -> Ordering)
-> (TrailMix -> TrailMix -> Bool)
-> (TrailMix -> TrailMix -> Bool)
-> (TrailMix -> TrailMix -> Bool)
-> (TrailMix -> TrailMix -> Bool)
-> (TrailMix -> TrailMix -> TrailMix)
-> (TrailMix -> TrailMix -> TrailMix)
-> Ord TrailMix
TrailMix -> TrailMix -> Bool
TrailMix -> TrailMix -> Ordering
TrailMix -> TrailMix -> TrailMix
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
$ccompare :: TrailMix -> TrailMix -> Ordering
compare :: TrailMix -> TrailMix -> Ordering
$c< :: TrailMix -> TrailMix -> Bool
< :: TrailMix -> TrailMix -> Bool
$c<= :: TrailMix -> TrailMix -> Bool
<= :: TrailMix -> TrailMix -> Bool
$c> :: TrailMix -> TrailMix -> Bool
> :: TrailMix -> TrailMix -> Bool
$c>= :: TrailMix -> TrailMix -> Bool
>= :: TrailMix -> TrailMix -> Bool
$cmax :: TrailMix -> TrailMix -> TrailMix
max :: TrailMix -> TrailMix -> TrailMix
$cmin :: TrailMix -> TrailMix -> TrailMix
min :: TrailMix -> TrailMix -> TrailMix
Ord)

unassigned :: (IsLiteral formula, Ord formula, Eq formula) => Set (Set formula) -> Set (formula, TrailMix) -> Set formula
unassigned :: forall formula.
(IsLiteral formula, Ord formula, Eq formula) =>
Set (Set formula) -> Set (formula, TrailMix) -> Set formula
unassigned Set (Set formula)
cls Set (formula, TrailMix)
trail =
    Set formula -> Set formula -> Set formula
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Set (Set formula) -> Set formula
forall a. Ord a => Set (Set a) -> Set a
flatten ((Set formula -> Set formula)
-> Set (Set formula) -> Set (Set formula)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((formula -> formula) -> Set formula -> Set formula
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map formula -> formula
forall formula. IsLiteral formula => formula -> formula
litabs) Set (Set formula)
cls)) (((formula, TrailMix) -> formula)
-> Set (formula, TrailMix) -> Set formula
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (formula -> formula
forall formula. IsLiteral formula => formula -> formula
litabs (formula -> formula)
-> ((formula, TrailMix) -> formula)
-> (formula, TrailMix)
-> formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (formula, TrailMix) -> formula
forall a b. (a, b) -> a
fst) Set (formula, TrailMix)
trail)
    where litabs :: formula -> formula
litabs formula
p = if formula -> Bool
forall formula. IsLiteral formula => formula -> Bool
negated formula
p then formula -> formula
forall formula. IsLiteral formula => formula -> formula
negate formula
p else formula
p

unit_subpropagate :: (IsLiteral formula, Ord formula) =>
                     (Set (Set formula), Map formula (), Set (formula, TrailMix))
                  -> (Set (Set formula), Map formula (), Set (formula, TrailMix))
unit_subpropagate :: forall formula.
(IsLiteral formula, Ord formula) =>
(Set (Set formula), Map formula (), Set (formula, TrailMix))
-> (Set (Set formula), Map formula (), Set (formula, TrailMix))
unit_subpropagate (Set (Set formula)
cls,Map formula ()
fn,Set (formula, TrailMix)
trail) =
  let cls' :: Set (Set formula)
cls' = (Set formula -> Set formula)
-> Set (Set formula) -> Set (Set formula)
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((formula -> Bool) -> Set formula -> Set formula
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool) -> (formula -> Bool) -> formula -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map formula () -> formula -> Bool
forall t a. Ord t => Map t a -> t -> Bool
defined Map formula ()
fn (formula -> Bool) -> (formula -> formula) -> formula -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. formula -> formula
forall formula. IsLiteral formula => formula -> formula
negate)) Set (Set formula)
cls in
  let uu :: Set formula -> Failing (Set formula)
uu Set formula
cs =
          case Set formula -> Maybe (formula, Set formula)
forall a. Set a -> Maybe (a, Set a)
Set.minView Set formula
cs of
            Maybe (formula, Set formula)
Nothing -> [String] -> Failing (Set formula)
forall a. [String] -> Failing a
Failure [String
"unit_subpropagate"]
            Just (formula
c, Set formula
_) -> if Set formula -> Int
forall a. Set a -> Int
Set.size Set formula
cs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& Bool -> Bool
not (Map formula () -> formula -> Bool
forall t a. Ord t => Map t a -> t -> Bool
defined Map formula ()
fn formula
c)
                           then Set formula -> Failing (Set formula)
forall a. a -> Failing a
Success Set formula
cs
                           else [String] -> Failing (Set formula)
forall a. [String] -> Failing a
Failure [String
"unit_subpropagate"] in
  let newunits :: Set formula
newunits = Set (Set formula) -> Set formula
forall a. Ord a => Set (Set a) -> Set a
flatten ((Set formula -> Failing (Set formula))
-> Set (Set formula) -> Set (Set formula)
forall b a. Ord b => (a -> Failing b) -> Set a -> Set b
setmapfilter Set formula -> Failing (Set formula)
uu Set (Set formula)
cls') in
  if Set formula -> Bool
forall a. Set a -> Bool
Set.null Set formula
newunits then (Set (Set formula)
cls',Map formula ()
fn,Set (formula, TrailMix)
trail) else
  let trail' :: Set (formula, TrailMix)
trail' = (formula -> Set (formula, TrailMix) -> Set (formula, TrailMix))
-> Set (formula, TrailMix)
-> Set formula
-> Set (formula, TrailMix)
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ formula
p Set (formula, TrailMix)
t -> (formula, TrailMix)
-> Set (formula, TrailMix) -> Set (formula, TrailMix)
forall a. Ord a => a -> Set a -> Set a
Set.insert (formula
p,TrailMix
Deduced) Set (formula, TrailMix)
t) Set (formula, TrailMix)
trail Set formula
newunits
      fn' :: Map formula ()
fn' = (formula -> Map formula () -> Map formula ())
-> Map formula () -> Set formula -> Map formula ()
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ formula
u -> (formula
u formula -> () -> Map formula () -> Map formula ()
forall k a. Ord k => k -> a -> Map k a -> Map k a
|-> ())) Map formula ()
fn Set formula
newunits in
  (Set (Set formula), Map formula (), Set (formula, TrailMix))
-> (Set (Set formula), Map formula (), Set (formula, TrailMix))
forall formula.
(IsLiteral formula, Ord formula) =>
(Set (Set formula), Map formula (), Set (formula, TrailMix))
-> (Set (Set formula), Map formula (), Set (formula, TrailMix))
unit_subpropagate (Set (Set formula)
cls',Map formula ()
fn',Set (formula, TrailMix)
trail')

unit_propagate :: forall t. (IsLiteral t, Ord t) =>
                  (Set (Set t), Set (t, TrailMix))
               -> (Set (Set t), Set (t, TrailMix))
unit_propagate :: forall t.
(IsLiteral t, Ord t) =>
(Set (Set t), Set (t, TrailMix))
-> (Set (Set t), Set (t, TrailMix))
unit_propagate (Set (Set t)
cls,Set (t, TrailMix)
trail) =
  let fn :: Map t ()
fn = ((t, TrailMix) -> Map t () -> Map t ())
-> Map t () -> Set (t, TrailMix) -> Map t ()
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ (t
x,TrailMix
_) -> (t
x t -> () -> Map t () -> Map t ()
forall k a. Ord k => k -> a -> Map k a -> Map k a
|-> ())) Map t ()
forall k a. Map k a
Map.empty Set (t, TrailMix)
trail in
  let (Set (Set t)
cls',Map t ()
_fn',Set (t, TrailMix)
trail') = (Set (Set t), Map t (), Set (t, TrailMix))
-> (Set (Set t), Map t (), Set (t, TrailMix))
forall formula.
(IsLiteral formula, Ord formula) =>
(Set (Set formula), Map formula (), Set (formula, TrailMix))
-> (Set (Set formula), Map formula (), Set (formula, TrailMix))
unit_subpropagate (Set (Set t)
cls,Map t ()
fn,Set (t, TrailMix)
trail) in (Set (Set t)
cls',Set (t, TrailMix)
trail')

backtrack :: forall t. Set (t, TrailMix) -> Set (t, TrailMix)
backtrack :: forall t. Set (t, TrailMix) -> Set (t, TrailMix)
backtrack Set (t, TrailMix)
trail =
  case Set (t, TrailMix) -> Maybe ((t, TrailMix), Set (t, TrailMix))
forall a. Set a -> Maybe (a, Set a)
Set.minView Set (t, TrailMix)
trail of
    Just ((t
_p,TrailMix
Deduced), Set (t, TrailMix)
tt) -> Set (t, TrailMix) -> Set (t, TrailMix)
forall t. Set (t, TrailMix) -> Set (t, TrailMix)
backtrack Set (t, TrailMix)
tt
    Maybe ((t, TrailMix), Set (t, TrailMix))
_ -> Set (t, TrailMix)
trail

dplisat :: (JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> Bool
dplisat :: forall pf.
(JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
pf -> Bool
dplisat = Set (LFormula (AtomOf pf), TrailMix)
-> Set (Set (LFormula (AtomOf pf))) -> Bool
forall formula.
(IsLiteral formula, Ord formula) =>
Set (formula, TrailMix) -> Set (Set formula) -> Bool
dpli Set (LFormula (AtomOf pf), TrailMix)
forall a. Set a
Set.empty (Set (Set (LFormula (AtomOf pf))) -> Bool)
-> (pf -> Set (Set (LFormula (AtomOf pf)))) -> pf -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. pf -> Set (Set (LFormula (AtomOf pf)))
forall pf.
(IsPropositional pf, JustPropositional pf, Ord pf,
 NumAtom (AtomOf pf)) =>
pf -> Set (Set (LFormula (AtomOf pf)))
defcnfs

dplitaut :: (JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> Bool
dplitaut :: forall pf.
(JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
pf -> Bool
dplitaut = Bool -> Bool
not (Bool -> Bool) -> (pf -> Bool) -> pf -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. pf -> Bool
forall pf.
(JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
pf -> Bool
dplisat (pf -> Bool) -> (pf -> pf) -> pf -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. pf -> pf
forall formula. IsLiteral formula => formula -> formula
negate

-- | With simple non-chronological backjumping and learning.
dplb :: (IsLiteral formula, Ord formula) => Set (formula, TrailMix) -> Set (Set formula) -> Bool
dplb :: forall formula.
(IsLiteral formula, Ord formula) =>
Set (formula, TrailMix) -> Set (Set formula) -> Bool
dplb Set (formula, TrailMix)
trail Set (Set formula)
cls =
  let (Set (Set formula)
cls',Set (formula, TrailMix)
trail') = (Set (Set formula), Set (formula, TrailMix))
-> (Set (Set formula), Set (formula, TrailMix))
forall t.
(IsLiteral t, Ord t) =>
(Set (Set t), Set (t, TrailMix))
-> (Set (Set t), Set (t, TrailMix))
unit_propagate (Set (Set formula)
cls,Set (formula, TrailMix)
trail) in
  if Set formula -> Set (Set formula) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Set formula
forall a. Set a
Set.empty Set (Set formula)
cls' then
    case Set (formula, TrailMix)
-> Maybe ((formula, TrailMix), Set (formula, TrailMix))
forall a. Set a -> Maybe (a, Set a)
Set.minView (Set (formula, TrailMix) -> Set (formula, TrailMix)
forall t. Set (t, TrailMix) -> Set (t, TrailMix)
backtrack Set (formula, TrailMix)
trail) of
      Just ((formula
p,TrailMix
Guessed), Set (formula, TrailMix)
tt) ->
        let trail'' :: Set (formula, TrailMix)
trail'' = Set (Set formula)
-> formula -> Set (formula, TrailMix) -> Set (formula, TrailMix)
forall a.
(IsLiteral a, Ord a) =>
Set (Set a) -> a -> Set (a, TrailMix) -> Set (a, TrailMix)
backjump Set (Set formula)
cls formula
p Set (formula, TrailMix)
tt in
        let declits :: Set (formula, TrailMix)
declits = ((formula, TrailMix) -> Bool)
-> Set (formula, TrailMix) -> Set (formula, TrailMix)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\ (formula
_,TrailMix
d) -> TrailMix
d TrailMix -> TrailMix -> Bool
forall a. Eq a => a -> a -> Bool
== TrailMix
Guessed) Set (formula, TrailMix)
trail'' in
        let conflict :: Set formula
conflict = formula -> Set formula -> Set formula
forall a. Ord a => a -> Set a -> Set a
Set.insert (formula -> formula
forall formula. IsLiteral formula => formula -> formula
negate formula
p) (((formula, TrailMix) -> formula)
-> Set (formula, TrailMix) -> Set formula
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (formula -> formula
forall formula. IsLiteral formula => formula -> formula
negate (formula -> formula)
-> ((formula, TrailMix) -> formula)
-> (formula, TrailMix)
-> formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (formula, TrailMix) -> formula
forall a b. (a, b) -> a
fst) Set (formula, TrailMix)
declits) in
        Set (formula, TrailMix) -> Set (Set formula) -> Bool
forall formula.
(IsLiteral formula, Ord formula) =>
Set (formula, TrailMix) -> Set (Set formula) -> Bool
dplb ((formula, TrailMix)
-> Set (formula, TrailMix) -> Set (formula, TrailMix)
forall a. Ord a => a -> Set a -> Set a
Set.insert (formula -> formula
forall formula. IsLiteral formula => formula -> formula
negate formula
p, TrailMix
Deduced) Set (formula, TrailMix)
trail'') (Set formula -> Set (Set formula) -> Set (Set formula)
forall a. Ord a => a -> Set a -> Set a
Set.insert Set formula
conflict Set (Set formula)
cls)
      Maybe ((formula, TrailMix), Set (formula, TrailMix))
_ -> Bool
False
  else
    case Set (Set formula) -> Set (formula, TrailMix) -> Set formula
forall formula.
(IsLiteral formula, Ord formula, Eq formula) =>
Set (Set formula) -> Set (formula, TrailMix) -> Set formula
unassigned Set (Set formula)
cls Set (formula, TrailMix)
trail' of
      Set formula
s | Set formula -> Bool
forall a. Set a -> Bool
Set.null Set formula
s -> Bool
True
      Set formula
ps -> let Just formula
p = (formula -> Int) -> Set formula -> Maybe formula
forall b (s :: * -> *) a.
(Ord b, SetLike s, Foldable s) =>
(a -> b) -> s a -> Maybe a
maximize (Set (Set formula) -> formula -> Int
forall lit. (IsLiteral lit, Ord lit) => Set (Set lit) -> lit -> Int
posneg_count Set (Set formula)
cls') Set formula
ps in
            Set (formula, TrailMix) -> Set (Set formula) -> Bool
forall formula.
(IsLiteral formula, Ord formula) =>
Set (formula, TrailMix) -> Set (Set formula) -> Bool
dplb ((formula, TrailMix)
-> Set (formula, TrailMix) -> Set (formula, TrailMix)
forall a. Ord a => a -> Set a -> Set a
Set.insert (formula
p,TrailMix
Guessed) Set (formula, TrailMix)
trail') Set (Set formula)
cls

backjump :: (IsLiteral a, Ord a) => Set (Set a) -> a -> Set (a, TrailMix) -> Set (a, TrailMix)
backjump :: forall a.
(IsLiteral a, Ord a) =>
Set (Set a) -> a -> Set (a, TrailMix) -> Set (a, TrailMix)
backjump Set (Set a)
cls a
p Set (a, TrailMix)
trail =
  case Set (a, TrailMix) -> Maybe ((a, TrailMix), Set (a, TrailMix))
forall a. Set a -> Maybe (a, Set a)
Set.minView (Set (a, TrailMix) -> Set (a, TrailMix)
forall t. Set (t, TrailMix) -> Set (t, TrailMix)
backtrack Set (a, TrailMix)
trail) of
    Just ((a
_q,TrailMix
Guessed), Set (a, TrailMix)
tt) ->
        let (Set (Set a)
cls',Set (a, TrailMix)
_trail') = (Set (Set a), Set (a, TrailMix))
-> (Set (Set a), Set (a, TrailMix))
forall t.
(IsLiteral t, Ord t) =>
(Set (Set t), Set (t, TrailMix))
-> (Set (Set t), Set (t, TrailMix))
unit_propagate (Set (Set a)
cls, (a, TrailMix) -> Set (a, TrailMix) -> Set (a, TrailMix)
forall a. Ord a => a -> Set a -> Set a
Set.insert (a
p,TrailMix
Guessed) Set (a, TrailMix)
tt) in
        if Set a -> Set (Set a) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Set a
forall a. Set a
Set.empty Set (Set a)
cls' then Set (Set a) -> a -> Set (a, TrailMix) -> Set (a, TrailMix)
forall a.
(IsLiteral a, Ord a) =>
Set (Set a) -> a -> Set (a, TrailMix) -> Set (a, TrailMix)
backjump Set (Set a)
cls a
p Set (a, TrailMix)
tt else Set (a, TrailMix)
trail
    Maybe ((a, TrailMix), Set (a, TrailMix))
_ -> Set (a, TrailMix)
trail

dplbsat :: (JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> Bool
dplbsat :: forall pf.
(JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
pf -> Bool
dplbsat = Set (LFormula (AtomOf pf), TrailMix)
-> Set (Set (LFormula (AtomOf pf))) -> Bool
forall formula.
(IsLiteral formula, Ord formula) =>
Set (formula, TrailMix) -> Set (Set formula) -> Bool
dplb Set (LFormula (AtomOf pf), TrailMix)
forall a. Set a
Set.empty (Set (Set (LFormula (AtomOf pf))) -> Bool)
-> (pf -> Set (Set (LFormula (AtomOf pf)))) -> pf -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. pf -> Set (Set (LFormula (AtomOf pf)))
forall pf.
(IsPropositional pf, JustPropositional pf, Ord pf,
 NumAtom (AtomOf pf)) =>
pf -> Set (Set (LFormula (AtomOf pf)))
defcnfs

dplbtaut :: (JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) => pf -> Bool
dplbtaut :: forall pf.
(JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
pf -> Bool
dplbtaut = Bool -> Bool
not (Bool -> Bool) -> (pf -> Bool) -> pf -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. pf -> Bool
forall pf.
(JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
pf -> Bool
dplbsat (pf -> Bool) -> (pf -> pf) -> pf -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. pf -> pf
forall formula. IsLiteral formula => formula -> formula
negate

-- | Examples.
test03 :: Test
test03 :: Test
test03 = [Test] -> Test
TestList [Assertion -> Test
TestCase (String -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"dplitaut(prime 101)" Bool
True (PFormula (Knows Integer) -> Bool
forall pf.
(JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
pf -> Bool
dplitaut (Integer -> PFormula (Knows Integer)
forall formula.
(IsPropositional formula, Ord formula,
 AtomOf formula ~ Knows Integer) =>
Integer -> formula
prime Integer
101 :: PFormula (Knows Integer)))),
                   Assertion -> Test
TestCase (String -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"dplbtaut(prime 101)" Bool
True (PFormula (Knows Integer) -> Bool
forall pf.
(JustPropositional pf, Ord pf, NumAtom (AtomOf pf)) =>
pf -> Bool
dplbtaut (Integer -> PFormula (Knows Integer)
forall formula.
(IsPropositional formula, Ord formula,
 AtomOf formula ~ Knows Integer) =>
Integer -> formula
prime Integer
101 :: PFormula (Knows Integer))))]

testDP :: Test
testDP :: Test
testDP = String -> Test -> Test
TestLabel String
"DP" ([Test] -> Test
TestList [Test
test01, Test
test02, Test
test03])