{- |
Module      :  ./QBF/Tools.hs
Description :  folding function for propositional formulas extended with QBFs
Copyright   :  (c) Jonathan von Schroeder, DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  <jonathan.von_schroeder@dfki.de>
Stability   :  provisional
Portability :  portable

folding and simplification of propositional formulas

-}

module QBF.Tools where

import Common.Id
import QBF.AS_BASIC_QBF

import qualified Data.Map as Map

import Data.List (nub, (\\))

import qualified Data.Set as Set

data FoldRecord a = FoldRecord
  { FoldRecord a -> a -> Range -> a
foldNegation :: a -> Range -> a
  , FoldRecord a -> [a] -> Range -> a
foldConjunction :: [a] -> Range -> a
  , FoldRecord a -> [a] -> Range -> a
foldDisjunction :: [a] -> Range -> a
  , FoldRecord a -> a -> a -> Range -> a
foldImplication :: a -> a -> Range -> a
  , FoldRecord a -> a -> a -> Range -> a
foldEquivalence :: a -> a -> Range -> a
  , FoldRecord a -> Range -> a
foldTrueAtom :: Range -> a
  , FoldRecord a -> Range -> a
foldFalseAtom :: Range -> a
  , FoldRecord a -> Token -> a
foldPredication :: Token -> a
  , FoldRecord a -> [Token] -> a -> Range -> a
foldForAll :: [Token] -> a -> Range -> a
  , FoldRecord a -> [Token] -> a -> Range -> a
foldExists :: [Token] -> a -> Range -> a }

foldFormula :: FoldRecord a -> FORMULA -> a
foldFormula :: FoldRecord a -> FORMULA -> a
foldFormula r :: FoldRecord a
r frm :: FORMULA
frm = case FORMULA
frm of
   Negation f :: FORMULA
f n :: Range
n -> FoldRecord a -> a -> Range -> a
forall a. FoldRecord a -> a -> Range -> a
foldNegation FoldRecord a
r (FoldRecord a -> FORMULA -> a
forall a. FoldRecord a -> FORMULA -> a
foldFormula FoldRecord a
r FORMULA
f) Range
n
   Conjunction xs :: [FORMULA]
xs n :: Range
n -> FoldRecord a -> [a] -> Range -> a
forall a. FoldRecord a -> [a] -> Range -> a
foldConjunction FoldRecord a
r ((FORMULA -> a) -> [FORMULA] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (FoldRecord a -> FORMULA -> a
forall a. FoldRecord a -> FORMULA -> a
foldFormula FoldRecord a
r) [FORMULA]
xs) Range
n
   Disjunction xs :: [FORMULA]
xs n :: Range
n -> FoldRecord a -> [a] -> Range -> a
forall a. FoldRecord a -> [a] -> Range -> a
foldDisjunction FoldRecord a
r ((FORMULA -> a) -> [FORMULA] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (FoldRecord a -> FORMULA -> a
forall a. FoldRecord a -> FORMULA -> a
foldFormula FoldRecord a
r) [FORMULA]
xs) Range
n
   Implication x :: FORMULA
x y :: FORMULA
y n :: Range
n -> FoldRecord a -> a -> a -> Range -> a
forall a. FoldRecord a -> a -> a -> Range -> a
foldImplication FoldRecord a
r (FoldRecord a -> FORMULA -> a
forall a. FoldRecord a -> FORMULA -> a
foldFormula FoldRecord a
r FORMULA
x) (FoldRecord a -> FORMULA -> a
forall a. FoldRecord a -> FORMULA -> a
foldFormula FoldRecord a
r FORMULA
y) Range
n
   Equivalence x :: FORMULA
x y :: FORMULA
y n :: Range
n -> FoldRecord a -> a -> a -> Range -> a
forall a. FoldRecord a -> a -> a -> Range -> a
foldEquivalence FoldRecord a
r (FoldRecord a -> FORMULA -> a
forall a. FoldRecord a -> FORMULA -> a
foldFormula FoldRecord a
r FORMULA
x) (FoldRecord a -> FORMULA -> a
forall a. FoldRecord a -> FORMULA -> a
foldFormula FoldRecord a
r FORMULA
y) Range
n
   TrueAtom n :: Range
n -> FoldRecord a -> Range -> a
forall a. FoldRecord a -> Range -> a
foldTrueAtom FoldRecord a
r Range
n
   FalseAtom n :: Range
n -> FoldRecord a -> Range -> a
forall a. FoldRecord a -> Range -> a
foldFalseAtom FoldRecord a
r Range
n
   Predication x :: Token
x -> FoldRecord a -> Token -> a
forall a. FoldRecord a -> Token -> a
foldPredication FoldRecord a
r Token
x
   ForAll xs :: [Token]
xs f :: FORMULA
f n :: Range
n -> FoldRecord a -> [Token] -> a -> Range -> a
forall a. FoldRecord a -> [Token] -> a -> Range -> a
foldForAll FoldRecord a
r [Token]
xs (FoldRecord a -> FORMULA -> a
forall a. FoldRecord a -> FORMULA -> a
foldFormula FoldRecord a
r FORMULA
f) Range
n
   Exists xs :: [Token]
xs f :: FORMULA
f n :: Range
n -> FoldRecord a -> [Token] -> a -> Range -> a
forall a. FoldRecord a -> [Token] -> a -> Range -> a
foldExists FoldRecord a
r [Token]
xs (FoldRecord a -> FORMULA -> a
forall a. FoldRecord a -> FORMULA -> a
foldFormula FoldRecord a
r FORMULA
f) Range
n

mapRecord :: FoldRecord FORMULA
mapRecord :: FoldRecord FORMULA
mapRecord = FoldRecord :: forall a.
(a -> Range -> a)
-> ([a] -> Range -> a)
-> ([a] -> Range -> a)
-> (a -> a -> Range -> a)
-> (a -> a -> Range -> a)
-> (Range -> a)
-> (Range -> a)
-> (Token -> a)
-> ([Token] -> a -> Range -> a)
-> ([Token] -> a -> Range -> a)
-> FoldRecord a
FoldRecord
  { foldNegation :: FORMULA -> Range -> FORMULA
foldNegation = FORMULA -> Range -> FORMULA
Negation
  , foldConjunction :: [FORMULA] -> Range -> FORMULA
foldConjunction = [FORMULA] -> Range -> FORMULA
Conjunction
  , foldDisjunction :: [FORMULA] -> Range -> FORMULA
foldDisjunction = [FORMULA] -> Range -> FORMULA
Disjunction
  , foldImplication :: FORMULA -> FORMULA -> Range -> FORMULA
foldImplication = FORMULA -> FORMULA -> Range -> FORMULA
Implication
  , foldEquivalence :: FORMULA -> FORMULA -> Range -> FORMULA
foldEquivalence = FORMULA -> FORMULA -> Range -> FORMULA
Equivalence
  , foldTrueAtom :: Range -> FORMULA
foldTrueAtom = Range -> FORMULA
TrueAtom
  , foldFalseAtom :: Range -> FORMULA
foldFalseAtom = Range -> FORMULA
FalseAtom
  , foldPredication :: Token -> FORMULA
foldPredication = Token -> FORMULA
Predication
  , foldForAll :: [Token] -> FORMULA -> Range -> FORMULA
foldForAll = [Token] -> FORMULA -> Range -> FORMULA
ForAll
  , foldExists :: [Token] -> FORMULA -> Range -> FORMULA
foldExists = [Token] -> FORMULA -> Range -> FORMULA
Exists }

isNeg :: FORMULA -> Bool
isNeg :: FORMULA -> Bool
isNeg f :: FORMULA
f = case FORMULA
f of
  Negation _ _ -> Bool
True
  ForAll _ x :: FORMULA
x _ -> FORMULA -> Bool
isNeg FORMULA
x
  Exists _ x :: FORMULA
x _ -> FORMULA -> Bool
isNeg FORMULA
x
  _ -> Bool
False

isQuantified :: FORMULA -> Bool
isQuantified :: FORMULA -> Bool
isQuantified f :: FORMULA
f = case FORMULA
f of
  FalseAtom _ -> Bool
False
  TrueAtom _ -> Bool
False
  Predication _ -> Bool
False
  Negation f1 :: FORMULA
f1 _ -> FORMULA -> Bool
isQuantified FORMULA
f1
  Conjunction xs :: [FORMULA]
xs _ -> (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any FORMULA -> Bool
isQuantified [FORMULA]
xs
  Disjunction xs :: [FORMULA]
xs _ -> (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any FORMULA -> Bool
isQuantified [FORMULA]
xs
  Implication x :: FORMULA
x y :: FORMULA
y _ -> (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any FORMULA -> Bool
isQuantified [FORMULA
x, FORMULA
y]
  Equivalence x :: FORMULA
x y :: FORMULA
y _ -> (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any FORMULA -> Bool
isQuantified [FORMULA
x, FORMULA
y]
  ForAll {} -> Bool
True
  Exists {} -> Bool
True

getLits :: Set.Set FORMULA -> Set.Set FORMULA
getLits :: Set FORMULA -> Set FORMULA
getLits = (FORMULA -> Set FORMULA -> Set FORMULA)
-> Set FORMULA -> Set FORMULA -> Set FORMULA
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ f :: FORMULA
f -> case FORMULA
f of
  Negation x :: FORMULA
x _ -> FORMULA -> Set FORMULA -> Set FORMULA
forall a. Ord a => a -> Set a -> Set a
Set.insert FORMULA
x
  ForAll ts :: [Token]
ts f1 :: FORMULA
f1 n :: Range
n -> case FORMULA
f1 of
    Negation x :: FORMULA
x _ -> FORMULA -> Set FORMULA -> Set FORMULA
forall a. Ord a => a -> Set a -> Set a
Set.insert ([Token] -> FORMULA -> Range -> FORMULA
ForAll [Token]
ts FORMULA
x Range
n)
    _ -> FORMULA -> Set FORMULA -> Set FORMULA
forall a. Ord a => a -> Set a -> Set a
Set.insert ([Token] -> FORMULA -> Range -> FORMULA
ForAll [Token]
ts FORMULA
f Range
n)
  _ -> FORMULA -> Set FORMULA -> Set FORMULA
forall a. Ord a => a -> Set a -> Set a
Set.insert FORMULA
f) Set FORMULA
forall a. Set a
Set.empty

bothLits :: Set.Set FORMULA -> Bool
bothLits :: Set FORMULA -> Bool
bothLits fs :: Set FORMULA
fs = let
  (ns :: Set FORMULA
ns, ps :: Set FORMULA
ps) = (FORMULA -> Bool) -> Set FORMULA -> (Set FORMULA, Set FORMULA)
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition FORMULA -> Bool
isNeg Set FORMULA
fs
  in Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set FORMULA -> Bool
forall a. Set a -> Bool
Set.null (Set FORMULA -> Bool) -> Set FORMULA -> Bool
forall a b. (a -> b) -> a -> b
$ Set FORMULA -> Set FORMULA -> Set FORMULA
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection (Set FORMULA -> Set FORMULA
getLits Set FORMULA
ns) (Set FORMULA -> Set FORMULA
getLits Set FORMULA
ps)

getConj :: FORMULA -> [FORMULA]
getConj :: FORMULA -> [FORMULA]
getConj f :: FORMULA
f = case FORMULA
f of
  Conjunction xs :: [FORMULA]
xs _ -> [FORMULA]
xs
  _ -> [FORMULA
f]

getDisj :: FORMULA -> [FORMULA]
getDisj :: FORMULA -> [FORMULA]
getDisj f :: FORMULA
f = case FORMULA
f of
  Disjunction xs :: [FORMULA]
xs _ -> [FORMULA]
xs
  _ -> [FORMULA
f]

flatConj :: [FORMULA] -> Set.Set FORMULA
flatConj :: [FORMULA] -> Set FORMULA
flatConj = [FORMULA] -> Set FORMULA
forall a. Ord a => [a] -> Set a
Set.fromList
  ([FORMULA] -> Set FORMULA)
-> ([FORMULA] -> [FORMULA]) -> [FORMULA] -> Set FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA -> [FORMULA]) -> [FORMULA] -> [FORMULA]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ f :: FORMULA
f -> case FORMULA
f of
      TrueAtom _ -> []
      Conjunction fs :: [FORMULA]
fs _ -> [FORMULA]
fs
      _ -> [FORMULA
f])

mkConj :: [FORMULA] -> Range -> FORMULA
mkConj :: [FORMULA] -> Range -> FORMULA
mkConj fs :: [FORMULA]
fs n :: Range
n = let s :: Set FORMULA
s = [FORMULA] -> Set FORMULA
flatConj [FORMULA]
fs in
  if FORMULA -> Set FORMULA -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Range -> FORMULA
FalseAtom Range
nullRange) Set FORMULA
s Bool -> Bool -> Bool
|| Set FORMULA -> Bool
bothLits Set FORMULA
s then Range -> FORMULA
FalseAtom Range
n else
  case Set FORMULA -> [FORMULA]
forall a. Set a -> [a]
Set.toList Set FORMULA
s of
    [] -> Range -> FORMULA
TrueAtom Range
n
    [x :: FORMULA
x] -> FORMULA
x
    ls :: [FORMULA]
ls -> [FORMULA] -> Range -> FORMULA
Conjunction ((Set FORMULA -> FORMULA) -> [Set FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (([FORMULA] -> Range -> FORMULA) -> Range -> [FORMULA] -> FORMULA
forall a b c. (a -> b -> c) -> b -> a -> c
flip [FORMULA] -> Range -> FORMULA
mkDisj Range
n ([FORMULA] -> FORMULA)
-> (Set FORMULA -> [FORMULA]) -> Set FORMULA -> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set FORMULA -> [FORMULA]
forall a. Set a -> [a]
Set.toList)
      ([Set FORMULA] -> [FORMULA]) -> [Set FORMULA] -> [FORMULA]
forall a b. (a -> b) -> a -> b
$ (FORMULA -> [Set FORMULA] -> [Set FORMULA])
-> [Set FORMULA] -> [FORMULA] -> [Set FORMULA]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((\ l :: Set FORMULA
l ll :: [Set FORMULA]
ll ->
        if (Set FORMULA -> Bool) -> [Set FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Set FORMULA -> Set FORMULA -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set FORMULA
l) [Set FORMULA]
ll then [Set FORMULA]
ll else
          Set FORMULA
l Set FORMULA -> [Set FORMULA] -> [Set FORMULA]
forall a. a -> [a] -> [a]
: (Set FORMULA -> Bool) -> [Set FORMULA] -> [Set FORMULA]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Set FORMULA -> Bool) -> Set FORMULA -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set FORMULA -> Set FORMULA -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set FORMULA
l) [Set FORMULA]
ll)
          (Set FORMULA -> [Set FORMULA] -> [Set FORMULA])
-> (FORMULA -> Set FORMULA)
-> FORMULA
-> [Set FORMULA]
-> [Set FORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [FORMULA] -> Set FORMULA
forall a. Ord a => [a] -> Set a
Set.fromList ([FORMULA] -> Set FORMULA)
-> (FORMULA -> [FORMULA]) -> FORMULA -> Set FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> [FORMULA]
getConj)
        [] [FORMULA]
ls) Range
n

flatDisj :: [FORMULA] -> Set.Set FORMULA
flatDisj :: [FORMULA] -> Set FORMULA
flatDisj = [FORMULA] -> Set FORMULA
forall a. Ord a => [a] -> Set a
Set.fromList
  ([FORMULA] -> Set FORMULA)
-> ([FORMULA] -> [FORMULA]) -> [FORMULA] -> Set FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA -> [FORMULA]) -> [FORMULA] -> [FORMULA]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ f :: FORMULA
f -> case FORMULA
f of
      FalseAtom _ -> []
      Disjunction fs :: [FORMULA]
fs _ -> [FORMULA]
fs
      _ -> [FORMULA
f])

mkDisj :: [FORMULA] -> Range -> FORMULA
mkDisj :: [FORMULA] -> Range -> FORMULA
mkDisj fs :: [FORMULA]
fs n :: Range
n = let s :: Set FORMULA
s = [FORMULA] -> Set FORMULA
flatDisj [FORMULA]
fs in
  if FORMULA -> Set FORMULA -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Range -> FORMULA
TrueAtom Range
nullRange) Set FORMULA
s Bool -> Bool -> Bool
|| Set FORMULA -> Bool
bothLits Set FORMULA
s then Range -> FORMULA
TrueAtom Range
n else
  case Set FORMULA -> [FORMULA]
forall a. Set a -> [a]
Set.toList Set FORMULA
s of
    [] -> Range -> FORMULA
FalseAtom Range
n
    [x :: FORMULA
x] -> FORMULA
x
    ls :: [FORMULA]
ls -> [FORMULA] -> Range -> FORMULA
Disjunction ((Set FORMULA -> FORMULA) -> [Set FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (([FORMULA] -> Range -> FORMULA) -> Range -> [FORMULA] -> FORMULA
forall a b c. (a -> b -> c) -> b -> a -> c
flip [FORMULA] -> Range -> FORMULA
mkConj Range
n ([FORMULA] -> FORMULA)
-> (Set FORMULA -> [FORMULA]) -> Set FORMULA -> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set FORMULA -> [FORMULA]
forall a. Set a -> [a]
Set.toList)
      ([Set FORMULA] -> [FORMULA]) -> [Set FORMULA] -> [FORMULA]
forall a b. (a -> b) -> a -> b
$ (FORMULA -> [Set FORMULA] -> [Set FORMULA])
-> [Set FORMULA] -> [FORMULA] -> [Set FORMULA]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((\ l :: Set FORMULA
l ll :: [Set FORMULA]
ll ->
        if (Set FORMULA -> Bool) -> [Set FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Set FORMULA -> Set FORMULA -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set FORMULA
l) [Set FORMULA]
ll then [Set FORMULA]
ll else
          Set FORMULA
l Set FORMULA -> [Set FORMULA] -> [Set FORMULA]
forall a. a -> [a] -> [a]
: (Set FORMULA -> Bool) -> [Set FORMULA] -> [Set FORMULA]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Set FORMULA -> Bool) -> Set FORMULA -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set FORMULA -> Set FORMULA -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set FORMULA
l) [Set FORMULA]
ll)
          (Set FORMULA -> [Set FORMULA] -> [Set FORMULA])
-> (FORMULA -> Set FORMULA)
-> FORMULA
-> [Set FORMULA]
-> [Set FORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [FORMULA] -> Set FORMULA
forall a. Ord a => [a] -> Set a
Set.fromList ([FORMULA] -> Set FORMULA)
-> (FORMULA -> [FORMULA]) -> FORMULA -> Set FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> [FORMULA]
getConj)
      [] [FORMULA]
ls) Range
n

simplify :: FORMULA -> FORMULA
simplify :: FORMULA -> FORMULA
simplify = FoldRecord FORMULA -> FORMULA -> FORMULA
forall a. FoldRecord a -> FORMULA -> a
foldFormula FoldRecord FORMULA
mapRecord
  { foldNegation :: FORMULA -> Range -> FORMULA
foldNegation = \ f :: FORMULA
f n :: Range
n -> case FORMULA
f of
    TrueAtom p :: Range
p -> Range -> FORMULA
FalseAtom Range
p
    FalseAtom p :: Range
p -> Range -> FORMULA
TrueAtom Range
p
    Negation g :: FORMULA
g _ -> FORMULA
g
    s :: FORMULA
s -> FORMULA -> Range -> FORMULA
Negation FORMULA
s Range
n
  , foldConjunction :: [FORMULA] -> Range -> FORMULA
foldConjunction = [FORMULA] -> Range -> FORMULA
mkConj
  , foldDisjunction :: [FORMULA] -> Range -> FORMULA
foldDisjunction = [FORMULA] -> Range -> FORMULA
mkDisj
  , foldImplication :: FORMULA -> FORMULA -> Range -> FORMULA
foldImplication = \ x :: FORMULA
x y :: FORMULA
y n :: Range
n -> case FORMULA
x of
    FalseAtom p :: Range
p -> Range -> FORMULA
TrueAtom Range
p
    _ -> if FORMULA
x FORMULA -> FORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== FORMULA
y then Range -> FORMULA
TrueAtom Range
n else case FORMULA
x of
           TrueAtom _ -> FORMULA
y
           FalseAtom _ -> Range -> FORMULA
TrueAtom Range
n
           Negation z :: FORMULA
z _ | FORMULA
z FORMULA -> FORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== FORMULA
y -> FORMULA
x
           _ -> case FORMULA
y of
             Negation z :: FORMULA
z _ | FORMULA
z FORMULA -> FORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== FORMULA
x -> FORMULA
x
             _ -> FORMULA -> FORMULA -> Range -> FORMULA
Implication FORMULA
x FORMULA
y Range
n
  , foldEquivalence :: FORMULA -> FORMULA -> Range -> FORMULA
foldEquivalence = \ x :: FORMULA
x y :: FORMULA
y n :: Range
n -> case FORMULA -> FORMULA -> Ordering
forall a. Ord a => a -> a -> Ordering
compare FORMULA
x FORMULA
y of
    LT -> case FORMULA
y of
      Negation z :: FORMULA
z _ | FORMULA
x FORMULA -> FORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== FORMULA
z -> Range -> FORMULA
FalseAtom Range
n
      _ -> FORMULA -> FORMULA -> Range -> FORMULA
Equivalence FORMULA
x FORMULA
y Range
n
    EQ -> Range -> FORMULA
TrueAtom Range
n
    GT -> case FORMULA
x of
      Negation z :: FORMULA
z _ | FORMULA
z FORMULA -> FORMULA -> Bool
forall a. Eq a => a -> a -> Bool
== FORMULA
y -> Range -> FORMULA
FalseAtom Range
n
      _ -> FORMULA -> FORMULA -> Range -> FORMULA
Equivalence FORMULA
y FORMULA
x Range
n }

elimEquiv :: FORMULA -> FORMULA
elimEquiv :: FORMULA -> FORMULA
elimEquiv = FoldRecord FORMULA -> FORMULA -> FORMULA
forall a. FoldRecord a -> FORMULA -> a
foldFormula FoldRecord FORMULA
mapRecord
  { foldEquivalence :: FORMULA -> FORMULA -> Range -> FORMULA
foldEquivalence = \ x :: FORMULA
x y :: FORMULA
y n :: Range
n ->
    [FORMULA] -> Range -> FORMULA
Conjunction [FORMULA -> FORMULA -> Range -> FORMULA
Implication FORMULA
x FORMULA
y Range
n, FORMULA -> FORMULA -> Range -> FORMULA
Implication FORMULA
y FORMULA
x Range
n] Range
n }

elimImpl :: FORMULA -> FORMULA
elimImpl :: FORMULA -> FORMULA
elimImpl = FoldRecord FORMULA -> FORMULA -> FORMULA
forall a. FoldRecord a -> FORMULA -> a
foldFormula FoldRecord FORMULA
mapRecord
  { foldImplication :: FORMULA -> FORMULA -> Range -> FORMULA
foldImplication = \ x :: FORMULA
x y :: FORMULA
y n :: Range
n ->
    [FORMULA] -> Range -> FORMULA
Disjunction [FORMULA -> Range -> FORMULA
Negation FORMULA
x Range
n, FORMULA
y] Range
n }

negForm :: Range -> FORMULA -> FORMULA
negForm :: Range -> FORMULA -> FORMULA
negForm r :: Range
r frm :: FORMULA
frm = case FORMULA
frm of
  Negation f :: FORMULA
f _ -> FORMULA
f
  Conjunction xs :: [FORMULA]
xs n :: Range
n -> [FORMULA] -> Range -> FORMULA
Disjunction ((FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (Range -> FORMULA -> FORMULA
negForm Range
r) [FORMULA]
xs) Range
n
  Disjunction xs :: [FORMULA]
xs n :: Range
n -> [FORMULA] -> Range -> FORMULA
Conjunction ((FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (Range -> FORMULA -> FORMULA
negForm Range
r) [FORMULA]
xs) Range
n
  TrueAtom n :: Range
n -> Range -> FORMULA
FalseAtom Range
n
  FalseAtom n :: Range
n -> Range -> FORMULA
TrueAtom Range
n
  ForAll ts :: [Token]
ts f :: FORMULA
f n :: Range
n -> [Token] -> FORMULA -> Range -> FORMULA
ForAll [Token]
ts (Range -> FORMULA -> FORMULA
negForm Range
r FORMULA
f) Range
n
  Exists ts :: [Token]
ts f :: FORMULA
f n :: Range
n -> [Token] -> FORMULA -> Range -> FORMULA
Exists [Token]
ts (Range -> FORMULA -> FORMULA
negForm Range
r FORMULA
f) Range
n
  _ -> FORMULA -> Range -> FORMULA
Negation FORMULA
frm Range
r

moveNegIn :: FORMULA -> FORMULA
moveNegIn :: FORMULA -> FORMULA
moveNegIn frm :: FORMULA
frm = case FORMULA
frm of
  Negation f :: FORMULA
f n :: Range
n -> Range -> FORMULA -> FORMULA
negForm Range
n FORMULA
f
  Conjunction xs :: [FORMULA]
xs n :: Range
n -> [FORMULA] -> Range -> FORMULA
Conjunction ((FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> FORMULA
moveNegIn [FORMULA]
xs) Range
n
  Disjunction xs :: [FORMULA]
xs n :: Range
n -> [FORMULA] -> Range -> FORMULA
Disjunction ((FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> FORMULA
moveNegIn [FORMULA]
xs) Range
n
  ForAll ts :: [Token]
ts f :: FORMULA
f n :: Range
n -> [Token] -> FORMULA -> Range -> FORMULA
ForAll [Token]
ts (FORMULA -> FORMULA
moveNegIn FORMULA
f) Range
n
  Exists ts :: [Token]
ts f :: FORMULA
f n :: Range
n -> [Token] -> FORMULA -> Range -> FORMULA
Exists [Token]
ts (FORMULA -> FORMULA
moveNegIn FORMULA
f) Range
n
  _ -> FORMULA
frm

distributeAndOverOr :: FORMULA -> FORMULA
distributeAndOverOr :: FORMULA -> FORMULA
distributeAndOverOr f :: FORMULA
f = case FORMULA
f of
  Conjunction xs :: [FORMULA]
xs n :: Range
n -> [FORMULA] -> Range -> FORMULA
mkConj ((FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> FORMULA
distributeAndOverOr [FORMULA]
xs) Range
n
  Disjunction xs :: [FORMULA]
xs n :: Range
n -> if (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all FORMULA -> Bool
isPrimForm [FORMULA]
xs then [FORMULA] -> Range -> FORMULA
mkDisj [FORMULA]
xs Range
n else
    FORMULA -> FORMULA
distributeAndOverOr
    (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall a b. (a -> b) -> a -> b
$ [FORMULA] -> Range -> FORMULA
mkConj (([FORMULA] -> FORMULA) -> [[FORMULA]] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map ([FORMULA] -> Range -> FORMULA
`mkDisj` Range
n) ([[FORMULA]] -> [FORMULA])
-> ([[FORMULA]] -> [[FORMULA]]) -> [[FORMULA]] -> [FORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[FORMULA]] -> [[FORMULA]]
forall a. [[a]] -> [[a]]
combine ([[FORMULA]] -> [FORMULA]) -> [[FORMULA]] -> [FORMULA]
forall a b. (a -> b) -> a -> b
$ (FORMULA -> [FORMULA]) -> [FORMULA] -> [[FORMULA]]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> [FORMULA]
getConj [FORMULA]
xs) Range
n
  ForAll ts :: [Token]
ts x :: FORMULA
x n :: Range
n -> [Token] -> FORMULA -> Range -> FORMULA
ForAll [Token]
ts (FORMULA -> FORMULA
distributeAndOverOr FORMULA
x) Range
n
  Exists ts :: [Token]
ts x :: FORMULA
x n :: Range
n -> [Token] -> FORMULA -> Range -> FORMULA
Exists [Token]
ts (FORMULA -> FORMULA
distributeAndOverOr FORMULA
x) Range
n
  _ -> FORMULA
f

{- note: won't work fully if the formula is quantified because
it can't distribute through quantifications -}
cnf :: FORMULA -> FORMULA
cnf :: FORMULA -> FORMULA
cnf = FORMULA -> FORMULA
distributeAndOverOr (FORMULA -> FORMULA) -> (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> FORMULA
moveNegIn (FORMULA -> FORMULA) -> (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> FORMULA
elimImpl (FORMULA -> FORMULA) -> (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> FORMULA
elimEquiv

distributeOrOverAnd :: FORMULA -> FORMULA
distributeOrOverAnd :: FORMULA -> FORMULA
distributeOrOverAnd f :: FORMULA
f = case FORMULA
f of
  Disjunction xs :: [FORMULA]
xs n :: Range
n -> [FORMULA] -> Range -> FORMULA
mkDisj ((FORMULA -> FORMULA) -> [FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> FORMULA
distributeOrOverAnd [FORMULA]
xs) Range
n
  Conjunction xs :: [FORMULA]
xs n :: Range
n -> if (FORMULA -> Bool) -> [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all FORMULA -> Bool
isPrimForm [FORMULA]
xs then [FORMULA] -> Range -> FORMULA
mkConj [FORMULA]
xs Range
n else
    FORMULA -> FORMULA
distributeOrOverAnd
    (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall a b. (a -> b) -> a -> b
$ [FORMULA] -> Range -> FORMULA
mkDisj (([FORMULA] -> FORMULA) -> [[FORMULA]] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map ([FORMULA] -> Range -> FORMULA
`mkConj` Range
n) ([[FORMULA]] -> [FORMULA])
-> ([[FORMULA]] -> [[FORMULA]]) -> [[FORMULA]] -> [FORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[FORMULA]] -> [[FORMULA]]
forall a. [[a]] -> [[a]]
combine ([[FORMULA]] -> [FORMULA]) -> [[FORMULA]] -> [FORMULA]
forall a b. (a -> b) -> a -> b
$ (FORMULA -> [FORMULA]) -> [FORMULA] -> [[FORMULA]]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> [FORMULA]
getDisj [FORMULA]
xs) Range
n
  _ -> FORMULA
f

{- note: won't work fully if the formula is quantified because
it can't distribute through quantifications -}
dnf :: FORMULA -> FORMULA
dnf :: FORMULA -> FORMULA
dnf = FORMULA -> FORMULA
distributeOrOverAnd (FORMULA -> FORMULA) -> (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> FORMULA
moveNegIn (FORMULA -> FORMULA) -> (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> FORMULA
elimImpl (FORMULA -> FORMULA) -> (FORMULA -> FORMULA) -> FORMULA -> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> FORMULA
elimEquiv

combine :: [[a]] -> [[a]]
combine :: [[a]] -> [[a]]
combine l :: [[a]]
l = case [[a]]
l of
  [] -> [[]]
  h :: [a]
h : t :: [[a]]
t -> ([a] -> [[a]]) -> [[a]] -> [[a]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (((a -> [a]) -> [a] -> [[a]]) -> [a] -> (a -> [a]) -> [[a]]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> [a]) -> [a] -> [[a]]
forall a b. (a -> b) -> [a] -> [b]
map [a]
h ((a -> [a]) -> [[a]]) -> ([a] -> a -> [a]) -> [a] -> [[a]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> [a] -> [a]) -> [a] -> a -> [a]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (:)) ([[a]] -> [[a]]
forall a. [[a]] -> [[a]]
combine [[a]]
t)

containsAtoms :: FORMULA -> (Bool, Bool)
containsAtoms :: FORMULA -> (Bool, Bool)
containsAtoms f :: FORMULA
f = let
    join :: (Bool, Bool) -> (Bool, Bool) -> (Bool, Bool)
join (x :: Bool
x, y :: Bool
y) (x1 :: Bool
x1, y1 :: Bool
y1) = (Bool
x Bool -> Bool -> Bool
&& Bool
x1, Bool
y Bool -> Bool -> Bool
&& Bool
y1)
  in
    case FORMULA
f of
      (Negation x :: FORMULA
x _ ) -> FORMULA -> (Bool, Bool)
containsAtoms FORMULA
x
      (Conjunction fs :: [FORMULA]
fs _ ) -> ((Bool, Bool) -> (Bool, Bool) -> (Bool, Bool))
-> (Bool, Bool) -> [(Bool, Bool)] -> (Bool, Bool)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Bool, Bool) -> (Bool, Bool) -> (Bool, Bool)
join (Bool
False, Bool
False) ((FORMULA -> (Bool, Bool)) -> [FORMULA] -> [(Bool, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> (Bool, Bool)
containsAtoms [FORMULA]
fs)
      (Disjunction fs :: [FORMULA]
fs _ ) -> ((Bool, Bool) -> (Bool, Bool) -> (Bool, Bool))
-> (Bool, Bool) -> [(Bool, Bool)] -> (Bool, Bool)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Bool, Bool) -> (Bool, Bool) -> (Bool, Bool)
join (Bool
False, Bool
False) ((FORMULA -> (Bool, Bool)) -> [FORMULA] -> [(Bool, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> (Bool, Bool)
containsAtoms [FORMULA]
fs)
      (Implication f1 :: FORMULA
f1 f2 :: FORMULA
f2 _ ) -> (Bool, Bool) -> (Bool, Bool) -> (Bool, Bool)
join (FORMULA -> (Bool, Bool)
containsAtoms FORMULA
f1) (FORMULA -> (Bool, Bool)
containsAtoms FORMULA
f2)
      (Equivalence f1 :: FORMULA
f1 f2 :: FORMULA
f2 _ ) -> (Bool, Bool) -> (Bool, Bool) -> (Bool, Bool)
join (FORMULA -> (Bool, Bool)
containsAtoms FORMULA
f1) (FORMULA -> (Bool, Bool)
containsAtoms FORMULA
f2)
      (TrueAtom _) -> (Bool
True, Bool
False)
      (FalseAtom _) -> (Bool
False, Bool
True)
      (Predication _) -> (Bool
False, Bool
False)
      (ForAll _ x :: FORMULA
x _) -> FORMULA -> (Bool, Bool)
containsAtoms FORMULA
x
      (Exists _ x :: FORMULA
x _) -> FORMULA -> (Bool, Bool)
containsAtoms FORMULA
x

getVars :: FORMULA -> [Token]
getVars :: FORMULA -> [Token]
getVars (Negation x :: FORMULA
x _) = FORMULA -> [Token]
getVars FORMULA
x
getVars (Conjunction xs :: [FORMULA]
xs _) = [Token] -> [Token]
forall a. Eq a => [a] -> [a]
nub ((FORMULA -> [Token]) -> [FORMULA] -> [Token]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap FORMULA -> [Token]
getVars [FORMULA]
xs)
getVars (Disjunction xs :: [FORMULA]
xs _) = [Token] -> [Token]
forall a. Eq a => [a] -> [a]
nub ((FORMULA -> [Token]) -> [FORMULA] -> [Token]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap FORMULA -> [Token]
getVars [FORMULA]
xs)
getVars (Implication x1 :: FORMULA
x1 x2 :: FORMULA
x2 _) = [Token] -> [Token]
forall a. Eq a => [a] -> [a]
nub (FORMULA -> [Token]
getVars FORMULA
x1 [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ FORMULA -> [Token]
getVars FORMULA
x2)
getVars (Equivalence x1 :: FORMULA
x1 x2 :: FORMULA
x2 _) = [Token] -> [Token]
forall a. Eq a => [a] -> [a]
nub (FORMULA -> [Token]
getVars FORMULA
x1 [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ FORMULA -> [Token]
getVars FORMULA
x2)
getVars (Predication t :: Token
t) = [Token
t]
getVars (ForAll _ x :: FORMULA
x _) = FORMULA -> [Token]
getVars FORMULA
x
getVars (Exists _ x :: FORMULA
x _) = FORMULA -> [Token]
getVars FORMULA
x
getVars _ = []

uniqueQuantifiedVars :: Int -> String -> FORMULA -> (Int, FORMULA)
uniqueQuantifiedVars :: Int -> String -> FORMULA -> (Int, FORMULA)
uniqueQuantifiedVars c :: Int
c = Int -> Map Token Token -> String -> FORMULA -> (Int, FORMULA)
uniqueQuantifiedVars' Int
c Map Token Token
forall k a. Map k a
Map.empty

uniqueQuantifiedVars' :: Int -> Map.Map Token Token
  -> String -> FORMULA -> (Int, FORMULA)
uniqueQuantifiedVars' :: Int -> Map Token Token -> String -> FORMULA -> (Int, FORMULA)
uniqueQuantifiedVars' c :: Int
c m :: Map Token Token
m p :: String
p f :: FORMULA
f = let
  u :: FORMULA -> (Int, FORMULA)
u = Int -> Map Token Token -> String -> FORMULA -> (Int, FORMULA)
uniqueQuantifiedVars' Int
c Map Token Token
m String
p
  handleQuantified :: [Token] -> FORMULA -> ((Int, FORMULA), [Token])
handleQuantified ts :: [Token]
ts x :: FORMULA
x = let
   c1 :: Int
c1 = Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Token] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Token]
ts
   (m1 :: Map Token Token
m1, ts1 :: [Token]
ts1) = (Int -> (Map Token Token, [Token]) -> (Map Token Token, [Token]))
-> (Map Token Token, [Token])
-> [Int]
-> (Map Token Token, [Token])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ i :: Int
i (m' :: Map Token Token
m', ts' :: [Token]
ts') ->
          (Token -> Token -> Map Token Token -> Map Token Token
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert ([Token]
ts [Token] -> Int -> Token
forall a. [a] -> Int -> a
!! (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
c)) (String -> Range -> Token
Token (String
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i) Range
nullRange) Map Token Token
m',
            String -> Range -> Token
Token (String
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i) Range
nullRange Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ts')) (Map Token Token
m, []) [Int
c .. (Int
c1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1)]
   in (Int -> Map Token Token -> String -> FORMULA -> (Int, FORMULA)
uniqueQuantifiedVars' Int
c1 Map Token Token
m1 String
p FORMULA
x, [Token]
ts1)
 in
  case FORMULA
f of
    (Negation x :: FORMULA
x n :: Range
n) -> let (c1 :: Int
c1, x1 :: FORMULA
x1) = FORMULA -> (Int, FORMULA)
u FORMULA
x in (Int
c1, FORMULA -> Range -> FORMULA
Negation FORMULA
x1 Range
n)
    (Conjunction fs :: [FORMULA]
fs n :: Range
n) -> let
        (c1 :: Int
c1, fs1 :: [FORMULA]
fs1) = (FORMULA -> (Int, [FORMULA]) -> (Int, [FORMULA]))
-> (Int, [FORMULA]) -> [FORMULA] -> (Int, [FORMULA])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ x :: FORMULA
x (cx1 :: Int
cx1, xs :: [FORMULA]
xs) -> let
          (cx2 :: Int
cx2, fx :: FORMULA
fx) = Int -> Map Token Token -> String -> FORMULA -> (Int, FORMULA)
uniqueQuantifiedVars' Int
cx1 Map Token Token
m String
p FORMULA
x in (Int
cx2, FORMULA
fx FORMULA -> [FORMULA] -> [FORMULA]
forall a. a -> [a] -> [a]
: [FORMULA]
xs))
          (0, []) [FORMULA]
fs
      in (Int
c1, [FORMULA] -> Range -> FORMULA
Conjunction [FORMULA]
fs1 Range
n)
    (Disjunction fs :: [FORMULA]
fs n :: Range
n) -> let
        (c1 :: Int
c1, fs1 :: [FORMULA]
fs1) = (FORMULA -> (Int, [FORMULA]) -> (Int, [FORMULA]))
-> (Int, [FORMULA]) -> [FORMULA] -> (Int, [FORMULA])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ x :: FORMULA
x (cx1 :: Int
cx1, xs :: [FORMULA]
xs) -> let
          (cx2 :: Int
cx2, fx :: FORMULA
fx) = Int -> Map Token Token -> String -> FORMULA -> (Int, FORMULA)
uniqueQuantifiedVars' Int
cx1 Map Token Token
m String
p FORMULA
x in (Int
cx2, FORMULA
fx FORMULA -> [FORMULA] -> [FORMULA]
forall a. a -> [a] -> [a]
: [FORMULA]
xs))
          (0, []) [FORMULA]
fs
      in (Int
c1, [FORMULA] -> Range -> FORMULA
Disjunction [FORMULA]
fs1 Range
n)
    (Implication x1 :: FORMULA
x1 x2 :: FORMULA
x2 n :: Range
n) -> let
        (c1 :: Int
c1, x1' :: FORMULA
x1') = FORMULA -> (Int, FORMULA)
u FORMULA
x1
        (c2 :: Int
c2, x2' :: FORMULA
x2') = Int -> Map Token Token -> String -> FORMULA -> (Int, FORMULA)
uniqueQuantifiedVars' Int
c1 Map Token Token
m String
p FORMULA
x2
      in (Int
c2, FORMULA -> FORMULA -> Range -> FORMULA
Implication FORMULA
x1' FORMULA
x2' Range
n)
    (Equivalence x1 :: FORMULA
x1 x2 :: FORMULA
x2 n :: Range
n) -> let
        (c1 :: Int
c1, x1' :: FORMULA
x1') = FORMULA -> (Int, FORMULA)
u FORMULA
x1
        (c2 :: Int
c2, x2' :: FORMULA
x2') = Int -> Map Token Token -> String -> FORMULA -> (Int, FORMULA)
uniqueQuantifiedVars' Int
c1 Map Token Token
m String
p FORMULA
x2
      in (Int
c2, FORMULA -> FORMULA -> Range -> FORMULA
Equivalence FORMULA
x1' FORMULA
x2' Range
n)
    a :: FORMULA
a@(TrueAtom _) -> (Int
c, FORMULA
a)
    a :: FORMULA
a@(FalseAtom _) -> (Int
c, FORMULA
a)
    (Predication t :: Token
t) -> case Token -> Map Token Token -> Maybe Token
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Token
t Map Token Token
m of
                         Nothing -> (Int
c, Token -> FORMULA
Predication Token
t)
                         Just t1 :: Token
t1 -> (Int
c, Token -> FORMULA
Predication Token
t1)
    (ForAll ts :: [Token]
ts x :: FORMULA
x n :: Range
n) -> let
        ((c2 :: Int
c2, x' :: FORMULA
x'), ts1 :: [Token]
ts1) = [Token] -> FORMULA -> ((Int, FORMULA), [Token])
handleQuantified [Token]
ts FORMULA
x
      in
        (Int
c2, [Token] -> FORMULA -> Range -> FORMULA
ForAll [Token]
ts1 FORMULA
x' Range
n)
    (Exists ts :: [Token]
ts x :: FORMULA
x n :: Range
n) -> let
        ((c2 :: Int
c2, x' :: FORMULA
x'), ts1 :: [Token]
ts1) = [Token] -> FORMULA -> ((Int, FORMULA), [Token])
handleQuantified [Token]
ts FORMULA
x
      in
        (Int
c2, [Token] -> FORMULA -> Range -> FORMULA
Exists [Token]
ts1 FORMULA
x' Range
n)

removeQuantifiers :: FORMULA -> FORMULA
removeQuantifiers :: FORMULA -> FORMULA
removeQuantifiers = FoldRecord FORMULA -> FORMULA -> FORMULA
forall a. FoldRecord a -> FORMULA -> a
foldFormula FoldRecord FORMULA
mapRecord
  { foldForAll :: [Token] -> FORMULA -> Range -> FORMULA
foldForAll = \ _ x :: FORMULA
x _ -> FORMULA
x
  , foldExists :: [Token] -> FORMULA -> Range -> FORMULA
foldExists = \ _ x :: FORMULA
x _ -> FORMULA
x }

data QuantifiedVars = QuantifiedVars
  { QuantifiedVars -> [Token]
universallyQ :: [Token]
  , QuantifiedVars -> [Token]
existentiallyQ :: [Token]
  , QuantifiedVars -> [Token]
notQ :: [Token] } deriving (Int -> QuantifiedVars -> String -> String
[QuantifiedVars] -> String -> String
QuantifiedVars -> String
(Int -> QuantifiedVars -> String -> String)
-> (QuantifiedVars -> String)
-> ([QuantifiedVars] -> String -> String)
-> Show QuantifiedVars
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [QuantifiedVars] -> String -> String
$cshowList :: [QuantifiedVars] -> String -> String
show :: QuantifiedVars -> String
$cshow :: QuantifiedVars -> String
showsPrec :: Int -> QuantifiedVars -> String -> String
$cshowsPrec :: Int -> QuantifiedVars -> String -> String
Show)

quantifiedVars :: QuantifiedVars
quantifiedVars :: QuantifiedVars
quantifiedVars = QuantifiedVars :: [Token] -> [Token] -> [Token] -> QuantifiedVars
QuantifiedVars
  { universallyQ :: [Token]
universallyQ = []
  , existentiallyQ :: [Token]
existentiallyQ = []
  , notQ :: [Token]
notQ = [] }

joinQuantifiedVars :: QuantifiedVars -> QuantifiedVars -> QuantifiedVars
joinQuantifiedVars :: QuantifiedVars -> QuantifiedVars -> QuantifiedVars
joinQuantifiedVars q1 :: QuantifiedVars
q1 q2 :: QuantifiedVars
q2 = let
    u :: [Token]
u = [Token] -> [Token]
forall a. Eq a => [a] -> [a]
nub (QuantifiedVars -> [Token]
universallyQ QuantifiedVars
q1 [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ QuantifiedVars -> [Token]
universallyQ QuantifiedVars
q2)
    e :: [Token]
e = [Token] -> [Token]
forall a. Eq a => [a] -> [a]
nub (QuantifiedVars -> [Token]
existentiallyQ QuantifiedVars
q1 [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ QuantifiedVars -> [Token]
existentiallyQ QuantifiedVars
q2) [Token] -> [Token] -> [Token]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Token]
u
    n :: [Token]
n = [Token] -> [Token]
forall a. Eq a => [a] -> [a]
nub (QuantifiedVars -> [Token]
notQ QuantifiedVars
q1 [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ QuantifiedVars -> [Token]
notQ QuantifiedVars
q2) [Token] -> [Token] -> [Token]
forall a. Eq a => [a] -> [a] -> [a]
\\ ([Token]
u [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token]
e) {- if all formulas have been
    sanitized properly (NotQ q1) \\ (u++e) == (NotQ q1) and
    (NotQ q2) \\ (u++e) == (NotQ q2) should hold -
    see ProverState.hs - showQDIMACSProblem for an example on how
    to use uniqueQuantifiedVars to achieve that -}
  in
    QuantifiedVars :: [Token] -> [Token] -> [Token] -> QuantifiedVars
QuantifiedVars
    { universallyQ :: [Token]
universallyQ = [Token]
u
    , existentiallyQ :: [Token]
existentiallyQ = [Token]
e
    , notQ :: [Token]
notQ = [Token]
n }

getQuantifiedVars :: FORMULA -> QuantifiedVars
getQuantifiedVars :: FORMULA -> QuantifiedVars
getQuantifiedVars f :: FORMULA
f = case FORMULA
f of
  (Negation x :: FORMULA
x _) -> FORMULA -> QuantifiedVars
getQuantifiedVars FORMULA
x
  (Conjunction xs :: [FORMULA]
xs _) -> (FORMULA -> QuantifiedVars -> QuantifiedVars)
-> QuantifiedVars -> [FORMULA] -> QuantifiedVars
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (QuantifiedVars -> QuantifiedVars -> QuantifiedVars
joinQuantifiedVars (QuantifiedVars -> QuantifiedVars -> QuantifiedVars)
-> (FORMULA -> QuantifiedVars)
-> FORMULA
-> QuantifiedVars
-> QuantifiedVars
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> QuantifiedVars
getQuantifiedVars)
    QuantifiedVars
quantifiedVars [FORMULA]
xs
  (Disjunction xs :: [FORMULA]
xs _) -> (FORMULA -> QuantifiedVars -> QuantifiedVars)
-> QuantifiedVars -> [FORMULA] -> QuantifiedVars
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (QuantifiedVars -> QuantifiedVars -> QuantifiedVars
joinQuantifiedVars (QuantifiedVars -> QuantifiedVars -> QuantifiedVars)
-> (FORMULA -> QuantifiedVars)
-> FORMULA
-> QuantifiedVars
-> QuantifiedVars
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> QuantifiedVars
getQuantifiedVars)
    QuantifiedVars
quantifiedVars [FORMULA]
xs
  (Implication x1 :: FORMULA
x1 x2 :: FORMULA
x2 _) -> QuantifiedVars -> QuantifiedVars -> QuantifiedVars
joinQuantifiedVars (FORMULA -> QuantifiedVars
getQuantifiedVars FORMULA
x1)
    (FORMULA -> QuantifiedVars
getQuantifiedVars FORMULA
x2)
  (Equivalence x1 :: FORMULA
x1 x2 :: FORMULA
x2 _) -> QuantifiedVars -> QuantifiedVars -> QuantifiedVars
joinQuantifiedVars (FORMULA -> QuantifiedVars
getQuantifiedVars FORMULA
x1)
    (FORMULA -> QuantifiedVars
getQuantifiedVars FORMULA
x2)
  (Predication t :: Token
t) -> QuantifiedVars
quantifiedVars { notQ :: [Token]
notQ = [Token
t] }
  (ForAll ts :: [Token]
ts x :: FORMULA
x _) -> QuantifiedVars -> QuantifiedVars -> QuantifiedVars
joinQuantifiedVars
    (QuantifiedVars
quantifiedVars { universallyQ :: [Token]
universallyQ = [Token]
ts }) (FORMULA -> QuantifiedVars
getQuantifiedVars FORMULA
x)
  (Exists ts :: [Token]
ts x :: FORMULA
x _) -> QuantifiedVars -> QuantifiedVars -> QuantifiedVars
joinQuantifiedVars
    (QuantifiedVars
quantifiedVars { existentiallyQ :: [Token]
existentiallyQ = [Token]
ts }) (FORMULA -> QuantifiedVars
getQuantifiedVars FORMULA
x)
  _ -> QuantifiedVars
quantifiedVars

{- | the flatten functions use associtivity to "flatten" the syntax
tree of the formulae -}

{- | flatten \"flattens\" formulae under the assumption of the
semantics of basic specs, this means that we put each
\"clause\" into a single formula for CNF we really will obtain
clauses -}

flatten :: FORMULA -> [FORMULA]
flatten :: FORMULA -> [FORMULA]
flatten f :: FORMULA
f = case FORMULA
f of
      Conjunction fs :: [FORMULA]
fs _ -> (FORMULA -> [FORMULA]) -> [FORMULA] -> [FORMULA]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap FORMULA -> [FORMULA]
flatten [FORMULA]
fs
      _ -> [FORMULA
f]

-- | "flattening" for disjunctions
flattenDis :: FORMULA -> [FORMULA]
flattenDis :: FORMULA -> [FORMULA]
flattenDis f :: FORMULA
f = case FORMULA
f of
      Disjunction fs :: [FORMULA]
fs _ -> (FORMULA -> [FORMULA]) -> [FORMULA] -> [FORMULA]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap FORMULA -> [FORMULA]
flattenDis [FORMULA]
fs
      _ -> [FORMULA
f]

-- | negate a formula
negateFormula :: FORMULA -> FORMULA
negateFormula :: FORMULA -> FORMULA
negateFormula f :: FORMULA
f = case FORMULA
f of
  FalseAtom ps :: Range
ps -> Range -> FORMULA
TrueAtom Range
ps
  TrueAtom ps :: Range
ps -> Range -> FORMULA
FalseAtom Range
ps
  Negation nf :: FORMULA
nf _ -> FORMULA
nf
  _ -> FORMULA -> Range -> FORMULA
Negation FORMULA
f Range
nullRange