content: {- |
  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
    { foldNegation :: a -> Range -> a
    , foldConjunction :: [a] -> Range -> a
    , foldDisjunction :: [a] -> Range -> a
    , foldImplication :: a -> a -> Range -> a
    , foldEquivalence :: a -> a -> Range -> a
    , foldTrueAtom :: Range -> a
    , foldFalseAtom :: Range -> a
    , foldPredication :: Token -> a
    , foldForAll :: [Token] -> a -> Range -> a
    , foldExists :: [Token] -> a -> Range -> a }
  
  foldFormula :: FoldRecord a -> FORMULA -> a
  foldFormula r frm = case frm of
     Negation f n -> foldNegation r (foldFormula r f) n
     Conjunction xs n -> foldConjunction r (map (foldFormula r) xs) n
     Disjunction xs n -> foldDisjunction r (map (foldFormula r) xs) n
     Implication x y n -> foldImplication r (foldFormula r x) (foldFormula r y) n
     Equivalence x y n -> foldEquivalence r (foldFormula r x) (foldFormula r y) n
     TrueAtom n -> foldTrueAtom r n
     FalseAtom n -> foldFalseAtom r n
     Predication x -> foldPredication r x
     ForAll xs f n -> foldForAll r xs (foldFormula r f) n
     Exists xs f n -> foldExists r xs (foldFormula r f) n
  
  mapRecord :: FoldRecord FORMULA
  mapRecord = FoldRecord
    { foldNegation = Negation
    , foldConjunction = Conjunction
    , foldDisjunction = Disjunction
    , foldImplication = Implication
    , foldEquivalence = Equivalence
    , foldTrueAtom = TrueAtom
    , foldFalseAtom = FalseAtom
    , foldPredication = Predication
    , foldForAll = ForAll
    , foldExists = Exists }
  
  isNeg :: FORMULA -> Bool
  isNeg f = case f of
    Negation _ _ -> True
    ForAll _ x _ -> isNeg x
    Exists _ x _ -> isNeg x
    _ -> False
  
  isQuantified :: FORMULA -> Bool
  isQuantified f = case f of
    FalseAtom _ -> False
    TrueAtom _ -> False
    Predication _ -> False
    Negation f1 _ -> isQuantified f1
    Conjunction xs _ -> any isQuantified xs
    Disjunction xs _ -> any isQuantified xs
    Implication x y _ -> any isQuantified [x, y]
    Equivalence x y _ -> any isQuantified [x, y]
    ForAll {} -> True
    Exists {} -> True
  
  getLits :: Set.Set FORMULA -> Set.Set FORMULA
  getLits = Set.fold (\ f -> case f of
    Negation x _ -> Set.insert x
    ForAll ts f1 n -> case f1 of
      Negation x _ -> Set.insert (ForAll ts x n)
      _ -> Set.insert (ForAll ts f n)
    _ -> Set.insert f) Set.empty
  
  bothLits :: Set.Set FORMULA -> Bool
  bothLits fs = let
    (ns, ps) = Set.partition isNeg fs
    in not $ Set.null $ Set.intersection (getLits ns) (getLits ps)
  
  getConj :: FORMULA -> [FORMULA]
  getConj f = case f of
    Conjunction xs _ -> xs
    _ -> [f]
  
  getDisj :: FORMULA -> [FORMULA]
  getDisj f = case f of
    Disjunction xs _ -> xs
    _ -> [f]
  
  flatConj :: [FORMULA] -> Set.Set FORMULA
  flatConj = Set.fromList
    . concatMap (\ f -> case f of
        TrueAtom _ -> []
        Conjunction fs _ -> fs
        _ -> [f])
  
  mkConj :: [FORMULA] -> Range -> FORMULA
  mkConj fs n = let s = flatConj fs in
    if Set.member (FalseAtom nullRange) s || bothLits s then FalseAtom n else
    case Set.toList s of
      [] -> TrueAtom n
      [x] -> x
      ls -> Conjunction (map (flip mkDisj n . Set.toList)
        $ foldr ((\ l ll ->
          if any (`Set.isSubsetOf` l) ll then ll else
            l : filter (not . Set.isSubsetOf l) ll)
            . Set.fromList . getConj)
          [] ls) n
  
  flatDisj :: [FORMULA] -> Set.Set FORMULA
  flatDisj = Set.fromList
    . concatMap (\ f -> case f of
        FalseAtom _ -> []
        Disjunction fs _ -> fs
        _ -> [f])
  
  mkDisj :: [FORMULA] -> Range -> FORMULA
  mkDisj fs n = let s = flatDisj fs in
    if Set.member (TrueAtom nullRange) s || bothLits s then TrueAtom n else
    case Set.toList s of
      [] -> FalseAtom n
      [x] -> x
      ls -> Disjunction (map (flip mkConj n . Set.toList)
        $ foldr ((\ l ll ->
          if any (`Set.isSubsetOf` l) ll then ll else
            l : filter (not . Set.isSubsetOf l) ll)
            . Set.fromList . getConj)
        [] ls) n
  
  simplify :: FORMULA -> FORMULA
  simplify = foldFormula mapRecord
    { foldNegation = \ f n -> case f of
      TrueAtom p -> FalseAtom p
      FalseAtom p -> TrueAtom p
      Negation g _ -> g
      s -> Negation s n
    , foldConjunction = mkConj
    , foldDisjunction = mkDisj
    , foldImplication = \ x y n -> case x of
      FalseAtom p -> TrueAtom p
      _ -> if x == y then TrueAtom n else case x of
             TrueAtom _ -> y
             FalseAtom _ -> TrueAtom n
             Negation z _ | z == y -> x
             _ -> case y of
               Negation z _ | z == x -> x
               _ -> Implication x y n
    , foldEquivalence = \ x y n -> case compare x y of
      LT -> case y of
        Negation z _ | x == z -> FalseAtom n
        _ -> Equivalence x y n
      EQ -> TrueAtom n
      GT -> case x of
        Negation z _ | z == y -> FalseAtom n
        _ -> Equivalence y x n }
  
  elimEquiv :: FORMULA -> FORMULA
  elimEquiv = foldFormula mapRecord
    { foldEquivalence = \ x y n ->
      Conjunction [Implication x y n, Implication y x n] n }
  
  elimImpl :: FORMULA -> FORMULA
  elimImpl = foldFormula mapRecord
    { foldImplication = \ x y n ->
      Disjunction [Negation x n, y] n }
  
  negForm :: Range -> FORMULA -> FORMULA
  negForm r frm = case frm of
    Negation f _ -> f
    Conjunction xs n -> Disjunction (map (negForm r) xs) n
    Disjunction xs n -> Conjunction (map (negForm r) xs) n
    TrueAtom n -> FalseAtom n
    FalseAtom n -> TrueAtom n
    ForAll ts f n -> ForAll ts (negForm r f) n
    Exists ts f n -> Exists ts (negForm r f) n
    _ -> Negation frm r
  
  moveNegIn :: FORMULA -> FORMULA
  moveNegIn frm = case frm of
    Negation f n -> negForm n f
    Conjunction xs n -> Conjunction (map moveNegIn xs) n
    Disjunction xs n -> Disjunction (map moveNegIn xs) n
    ForAll ts f n -> ForAll ts (moveNegIn f) n
    Exists ts f n -> Exists ts (moveNegIn f) n
    _ -> frm
  
  distributeAndOverOr :: FORMULA -> FORMULA
  distributeAndOverOr f = case f of
    Conjunction xs n -> mkConj (map distributeAndOverOr xs) n
    Disjunction xs n -> if all isPrimForm xs then mkDisj xs n else
      distributeAndOverOr
      $ mkConj (map (`mkDisj` n) . combine $ map getConj xs) n
    ForAll ts x n -> ForAll ts (distributeAndOverOr x) n
    Exists ts x n -> Exists ts (distributeAndOverOr x) n
    _ -> f
  
  {- note: won't work fully if the formula is quantified because
  it can't distribute through quantifications -}
  cnf :: FORMULA -> FORMULA
  cnf = distributeAndOverOr . moveNegIn . elimImpl . elimEquiv
  
  distributeOrOverAnd :: FORMULA -> FORMULA
  distributeOrOverAnd f = case f of
    Disjunction xs n -> mkDisj (map distributeOrOverAnd xs) n
    Conjunction xs n -> if all isPrimForm xs then mkConj xs n else
      distributeOrOverAnd
      $ mkDisj (map (`mkConj` n) . combine $ map getDisj xs) n
    _ -> f
  
  {- note: won't work fully if the formula is quantified because
  it can't distribute through quantifications -}
  dnf :: FORMULA -> FORMULA
  dnf = distributeOrOverAnd . moveNegIn . elimImpl . elimEquiv
  
  combine :: [[a]] -> [[a]]
  combine l = case l of
    [] -> [[]]
    h : t -> concatMap (flip map h . flip (:)) (combine t)
  
  containsAtoms :: FORMULA -> (Bool, Bool)
  containsAtoms f = let
      join (x, y) (x1, y1) = (x && x1, y && y1)
    in
      case f of
        (Negation x _ ) -> containsAtoms x
        (Conjunction fs _ ) -> foldl join (False, False) (map containsAtoms fs)
        (Disjunction fs _ ) -> foldl join (False, False) (map containsAtoms fs)
        (Implication f1 f2 _ ) -> join (containsAtoms f1) (containsAtoms f2)
        (Equivalence f1 f2 _ ) -> join (containsAtoms f1) (containsAtoms f2)
        (TrueAtom _) -> (True, False)
        (FalseAtom _) -> (False, True)
        (Predication _) -> (False, False)
        (ForAll _ x _) -> containsAtoms x
        (Exists _ x _) -> containsAtoms x
  
  getVars :: FORMULA -> [Token]
  getVars (Negation x _) = getVars x
  getVars (Conjunction xs _) = nub (concatMap getVars xs)
  getVars (Disjunction xs _) = nub (concatMap getVars xs)
  getVars (Implication x1 x2 _) = nub (getVars x1 ++ getVars x2)
  getVars (Equivalence x1 x2 _) = nub (getVars x1 ++ getVars x2)
  getVars (Predication t) = [t]
  getVars (ForAll _ x _) = getVars x
  getVars (Exists _ x _) = getVars x
  getVars _ = []
  
  uniqueQuantifiedVars :: Int -> String -> FORMULA -> (Int, FORMULA)
  uniqueQuantifiedVars c = uniqueQuantifiedVars' c Map.empty
  
  uniqueQuantifiedVars' :: Int -> Map.Map Token Token
    -> String -> FORMULA -> (Int, FORMULA)
  uniqueQuantifiedVars' c m p f = let
    u = uniqueQuantifiedVars' c m p
    handleQuantified ts x = let
     c1 = c + length ts
     (m1, ts1) = foldr (\ i (m', ts') ->
            (Map.insert (ts !! (i - c)) (Token (p ++ show i) nullRange) m',
              Token (p ++ show i) nullRange : ts')) (m, []) [c .. (c1 - 1)]
     in (uniqueQuantifiedVars' c1 m1 p x, ts1)
   in
    case f of
      (Negation x n) -> let (c1, x1) = u x in (c1, Negation x1 n)
      (Conjunction fs n) -> let
          (c1, fs1) = foldr (\ x (cx1, xs) -> let
            (cx2, fx) = uniqueQuantifiedVars' cx1 m p x in (cx2, fx : xs))
            (0, []) fs
        in (c1, Conjunction fs1 n)
      (Disjunction fs n) -> let
          (c1, fs1) = foldr (\ x (cx1, xs) -> let
            (cx2, fx) = uniqueQuantifiedVars' cx1 m p x in (cx2, fx : xs))
            (0, []) fs
        in (c1, Disjunction fs1 n)
      (Implication x1 x2 n) -> let
          (c1, x1') = u x1
          (c2, x2') = uniqueQuantifiedVars' c1 m p x2
        in (c2, Implication x1' x2' n)
      (Equivalence x1 x2 n) -> let
          (c1, x1') = u x1
          (c2, x2') = uniqueQuantifiedVars' c1 m p x2
        in (c2, Equivalence x1' x2' n)
      a@(TrueAtom _) -> (c, a)
      a@(FalseAtom _) -> (c, a)
      (Predication t) -> case Map.lookup t m of
                           Nothing -> (c, Predication t)
                           Just t1 -> (c, Predication t1)
      (ForAll ts x n) -> let
          ((c2, x'), ts1) = handleQuantified ts x
        in
          (c2, ForAll ts1 x' n)
      (Exists ts x n) -> let
          ((c2, x'), ts1) = handleQuantified ts x
        in
          (c2, Exists ts1 x' n)
  
  removeQuantifiers :: FORMULA -> FORMULA
  removeQuantifiers = foldFormula mapRecord
    { foldForAll = \ _ x _ -> x
    , foldExists = \ _ x _ -> x }
  
  data QuantifiedVars = QuantifiedVars
    { universallyQ :: [Token]
    , existentiallyQ :: [Token]
    , notQ :: [Token] } deriving (Show)
  
  quantifiedVars :: QuantifiedVars
  quantifiedVars = QuantifiedVars
    { universallyQ = []
    , existentiallyQ = []
    , notQ = [] }
  
  joinQuantifiedVars :: QuantifiedVars -> QuantifiedVars -> QuantifiedVars
  joinQuantifiedVars q1 q2 = let
      u = nub (universallyQ q1 ++ universallyQ q2)
      e = nub (existentiallyQ q1 ++ existentiallyQ q2) \\ u
      n = nub (notQ q1 ++ notQ q2) \\ (u ++ 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
      { universallyQ = u
      , existentiallyQ = e
      , notQ = n }
  
  getQuantifiedVars :: FORMULA -> QuantifiedVars
  getQuantifiedVars f = case f of
    (Negation x _) -> getQuantifiedVars x
    (Conjunction xs _) -> foldr (joinQuantifiedVars . getQuantifiedVars)
      quantifiedVars xs
    (Disjunction xs _) -> foldr (joinQuantifiedVars . getQuantifiedVars)
      quantifiedVars xs
    (Implication x1 x2 _) -> joinQuantifiedVars (getQuantifiedVars x1)
      (getQuantifiedVars x2)
    (Equivalence x1 x2 _) -> joinQuantifiedVars (getQuantifiedVars x1)
      (getQuantifiedVars x2)
    (Predication t) -> quantifiedVars { notQ = [t] }
    (ForAll ts x _) -> joinQuantifiedVars
      (quantifiedVars { universallyQ = ts }) (getQuantifiedVars x)
    (Exists ts x _) -> joinQuantifiedVars
      (quantifiedVars { existentiallyQ = ts }) (getQuantifiedVars x)
    _ -> 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 f = case f of
        Conjunction fs _ -> concatMap flatten fs
        _ -> [f]
  
  -- | "flattening" for disjunctions
  flattenDis :: FORMULA -> [FORMULA]
  flattenDis f = case f of
        Disjunction fs _ -> concatMap flattenDis fs
        _ -> [f]
  
  -- | negate a formula
  negateFormula :: FORMULA -> FORMULA
  negateFormula f = case f of
    FalseAtom ps -> TrueAtom ps
    TrueAtom ps -> FalseAtom ps
    Negation nf _ -> nf
    _ -> Negation f nullRange
  