{- |
Description: Simplification of 'PropositionalFormula's.
License: GNU LGPLv3
Maintainer: paul.bittner@uni-ulm.de

Functions for simplification of 'PropositionalFormula's.
-}
module Simplify (
    removeRedundancy
) where

import Logic
import Propositions
    ( simplify,
      PropositionalFormula(..) )
import SAT ( contradicts, taut )
import Data.List

{- |
This is a naive implementation for presence condition simplification as described in

@
    A. von Rhein, A. Grebhahn, S. Apel, N. Siegmund, D. Beyer, and T. Berger.
    Presence-Condition Simplification in Highly Configurable Systems.
    In Proceedings of the IEEE/ACM International Conference on Software Engineering (ICSE), pages 178–188.
    IEEE Computer Society, May 2015.
@

This function simplifies a propositional formula (second argument) within the context of another propositional formula (first argument).
Assuming, that the first given formula is always satisfied (i.e., it is an axiom) this function simplifies the second formula.
For example, in pseudo-code @removeRedundancy (A) (A and B) == B@ as @A@ is redundant in the second formula if its already satisfied in the first formula.
-}
removeRedundancy :: (Ord a, Show a) => PropositionalFormula a -> PropositionalFormula a -> PropositionalFormula a
removeRedundancy :: PropositionalFormula a
-> PropositionalFormula a -> PropositionalFormula a
removeRedundancy axiom :: PropositionalFormula a
axiom (PAnd cs :: [PropositionalFormula a]
cs) =
    if PropositionalFormula a -> Bool
forall a. (Show a, Ord a) => PropositionalFormula a -> Bool
contradicts (PropositionalFormula a -> Bool) -> PropositionalFormula a -> Bool
forall a b. (a -> b) -> a -> b
$ [PropositionalFormula a] -> PropositionalFormula a
forall a. [PropositionalFormula a] -> PropositionalFormula a
PAnd ([PropositionalFormula a] -> PropositionalFormula a)
-> [PropositionalFormula a] -> PropositionalFormula a
forall a b. (a -> b) -> a -> b
$ PropositionalFormula a
axiomPropositionalFormula a
-> [PropositionalFormula a] -> [PropositionalFormula a]
forall a. a -> [a] -> [a]
:[PropositionalFormula a]
cs
    then PropositionalFormula a
forall a. PropositionalFormula a
PFalse
    else
        PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
simplify (PropositionalFormula a -> PropositionalFormula a)
-> PropositionalFormula a -> PropositionalFormula a
forall a b. (a -> b) -> a -> b
$
        [PropositionalFormula a] -> PropositionalFormula a
forall a. [PropositionalFormula a] -> PropositionalFormula a
PAnd ([PropositionalFormula a] -> PropositionalFormula a)
-> [PropositionalFormula a] -> PropositionalFormula a
forall a b. (a -> b) -> a -> b
$
        (PropositionalFormula a
 -> [PropositionalFormula a] -> [PropositionalFormula a])
-> [PropositionalFormula a]
-> [PropositionalFormula a]
-> [PropositionalFormula a]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\elementToInspect :: PropositionalFormula a
elementToInspect b :: [PropositionalFormula a]
b -> if PropositionalFormula a -> Bool
forall a. (Show a, Ord a) => PropositionalFormula a -> Bool
taut (PropositionalFormula a -> Bool) -> PropositionalFormula a -> Bool
forall a b. (a -> b) -> a -> b
$ PropositionalFormula a
-> PropositionalFormula a -> PropositionalFormula a
forall l. Logic l => l -> l -> l
limplies PropositionalFormula a
axiom ([PropositionalFormula a] -> PropositionalFormula a
forall a. [PropositionalFormula a] -> PropositionalFormula a
PAnd ([PropositionalFormula a] -> PropositionalFormula a)
-> [PropositionalFormula a] -> PropositionalFormula a
forall a b. (a -> b) -> a -> b
$ PropositionalFormula a
elementToInspectPropositionalFormula a
-> [PropositionalFormula a] -> [PropositionalFormula a]
forall a. a -> [a] -> [a]
:[PropositionalFormula a]
b) then [PropositionalFormula a]
b else PropositionalFormula a
elementToInspectPropositionalFormula a
-> [PropositionalFormula a] -> [PropositionalFormula a]
forall a. a -> [a] -> [a]
:[PropositionalFormula a]
b) [] ([PropositionalFormula a] -> [PropositionalFormula a])
-> [PropositionalFormula a] -> [PropositionalFormula a]
forall a b. (a -> b) -> a -> b
$
        -- (\c -> removeRedundancy (PAnd $ axiom:(delete c cs)) c) <$> cs
        PropositionalFormula a
-> PropositionalFormula a -> PropositionalFormula a
forall a.
(Ord a, Show a) =>
PropositionalFormula a
-> PropositionalFormula a -> PropositionalFormula a
removeRedundancy PropositionalFormula a
axiom (PropositionalFormula a -> PropositionalFormula a)
-> [PropositionalFormula a] -> [PropositionalFormula a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PropositionalFormula a]
cs
removeRedundancy axiom :: PropositionalFormula a
axiom (POr cs :: [PropositionalFormula a]
cs) =
      PropositionalFormula a
-> PropositionalFormula a -> PropositionalFormula a
forall a.
(Ord a, Show a) =>
PropositionalFormula a
-> PropositionalFormula a -> PropositionalFormula a
removeRedundancyBase PropositionalFormula a
axiom (PropositionalFormula a -> PropositionalFormula a)
-> PropositionalFormula a -> PropositionalFormula a
forall a b. (a -> b) -> a -> b
$
    --   simplify $
      [PropositionalFormula a] -> PropositionalFormula a
forall a. [PropositionalFormula a] -> PropositionalFormula a
POr ([PropositionalFormula a] -> PropositionalFormula a)
-> [PropositionalFormula a] -> PropositionalFormula a
forall a b. (a -> b) -> a -> b
$
      (PropositionalFormula a
 -> [PropositionalFormula a] -> [PropositionalFormula a])
-> [PropositionalFormula a]
-> [PropositionalFormula a]
-> [PropositionalFormula a]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\elementToInspect :: PropositionalFormula a
elementToInspect b :: [PropositionalFormula a]
b -> if PropositionalFormula a -> Bool
forall a. (Show a, Ord a) => PropositionalFormula a -> Bool
contradicts (PropositionalFormula a -> Bool) -> PropositionalFormula a -> Bool
forall a b. (a -> b) -> a -> b
$ [PropositionalFormula a] -> PropositionalFormula a
forall a. [PropositionalFormula a] -> PropositionalFormula a
PAnd [PropositionalFormula a
elementToInspect, PropositionalFormula a
axiom] then [PropositionalFormula a]
b else PropositionalFormula a
elementToInspectPropositionalFormula a
-> [PropositionalFormula a] -> [PropositionalFormula a]
forall a. a -> [a] -> [a]
:[PropositionalFormula a]
b) [] ([PropositionalFormula a] -> [PropositionalFormula a])
-> [PropositionalFormula a] -> [PropositionalFormula a]
forall a b. (a -> b) -> a -> b
$
      (PropositionalFormula a
-> PropositionalFormula a -> PropositionalFormula a
forall a.
(Ord a, Show a) =>
PropositionalFormula a
-> PropositionalFormula a -> PropositionalFormula a
removeRedundancy PropositionalFormula a
axiom) (PropositionalFormula a -> PropositionalFormula a)
-> [PropositionalFormula a] -> [PropositionalFormula a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PropositionalFormula a]
cs
removeRedundancy axiom :: PropositionalFormula a
axiom x :: PropositionalFormula a
x =
    let y :: PropositionalFormula a
y = PropositionalFormula a
-> PropositionalFormula a -> PropositionalFormula a
forall a.
(Ord a, Show a) =>
PropositionalFormula a
-> PropositionalFormula a -> PropositionalFormula a
removeRedundancyBase PropositionalFormula a
axiom PropositionalFormula a
x in
    if PropositionalFormula a -> Bool
forall a. (Show a, Ord a) => PropositionalFormula a -> Bool
contradicts (PropositionalFormula a -> Bool) -> PropositionalFormula a -> Bool
forall a b. (a -> b) -> a -> b
$ [PropositionalFormula a] -> PropositionalFormula a
forall a. [PropositionalFormula a] -> PropositionalFormula a
PAnd [PropositionalFormula a
y, PropositionalFormula a
axiom] then PropositionalFormula a
forall a. PropositionalFormula a
PFalse else PropositionalFormula a
y

-- | Base case for simplification with 'removeRedundancy'.
-- If the @axiom@ always implies @x@ (i.e., @axiom => x@ is a tautology), then @x@ can be simplified to /true/.
removeRedundancyBase :: (Ord a, Show a) => PropositionalFormula a -> PropositionalFormula a -> PropositionalFormula a
removeRedundancyBase :: PropositionalFormula a
-> PropositionalFormula a -> PropositionalFormula a
removeRedundancyBase axiom :: PropositionalFormula a
axiom x :: PropositionalFormula a
x = PropositionalFormula a -> PropositionalFormula a
forall a. PropositionalFormula a -> PropositionalFormula a
simplify (PropositionalFormula a -> PropositionalFormula a)
-> PropositionalFormula a -> PropositionalFormula a
forall a b. (a -> b) -> a -> b
$ if PropositionalFormula a -> Bool
forall a. (Show a, Ord a) => PropositionalFormula a -> Bool
taut (PropositionalFormula a -> Bool) -> PropositionalFormula a -> Bool
forall a b. (a -> b) -> a -> b
$ PropositionalFormula a
-> PropositionalFormula a -> PropositionalFormula a
forall l. Logic l => l -> l -> l
limplies PropositionalFormula a
axiom PropositionalFormula a
x then PropositionalFormula a
forall a. PropositionalFormula a
PTrue else PropositionalFormula a
x