{-# LANGUAGE TypeOperators, BangPatterns, CPP, PatternGuards #-}
module Jukebox.Tools.Clausify where

import Jukebox.Form hiding (run)
import qualified Jukebox.Form as Form
import Jukebox.Name
import Data.List( maximumBy, sortBy, partition )
import Data.Ord
import Control.Monad
import Control.Monad.Trans.Class
import Control.Monad.Trans.Reader
import Jukebox.Utils
import Jukebox.Options
import qualified Data.Set as Set
import Data.Set(Set)
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative
#endif

newtype ClausifyFlags = ClausifyFlags { ClausifyFlags -> Bool
splitting :: Bool } deriving Int -> ClausifyFlags -> ShowS
[ClausifyFlags] -> ShowS
ClausifyFlags -> String
(Int -> ClausifyFlags -> ShowS)
-> (ClausifyFlags -> String)
-> ([ClausifyFlags] -> ShowS)
-> Show ClausifyFlags
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ClausifyFlags] -> ShowS
$cshowList :: [ClausifyFlags] -> ShowS
show :: ClausifyFlags -> String
$cshow :: ClausifyFlags -> String
showsPrec :: Int -> ClausifyFlags -> ShowS
$cshowsPrec :: Int -> ClausifyFlags -> ShowS
Show

clausifyFlags :: OptionParser ClausifyFlags
clausifyFlags =
  String -> OptionParser ClausifyFlags -> OptionParser ClausifyFlags
forall a. String -> OptionParser a -> OptionParser a
inGroup String
"Input and clausifier options" (OptionParser ClausifyFlags -> OptionParser ClausifyFlags)
-> OptionParser ClausifyFlags -> OptionParser ClausifyFlags
forall a b. (a -> b) -> a -> b
$
  Bool -> ClausifyFlags
ClausifyFlags (Bool -> ClausifyFlags)
-> Annotated [Flag] ParParser Bool -> OptionParser ClausifyFlags
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    String -> [String] -> Bool -> Annotated [Flag] ParParser Bool
bool String
"split"
      [String
"Split the conjecture into several sub-conjectures (off by default)."]
      Bool
False

----------------------------------------------------------------------
-- clausify

clausify :: ClausifyFlags -> Problem Form -> CNF
clausify :: ClausifyFlags -> Problem Form -> CNF
clausify ClausifyFlags
flags Problem Form
inps = Problem Form -> (Problem Form -> NameM CNF) -> CNF
forall a b. Symbolic a => a -> (a -> NameM b) -> b
Form.run Problem Form
inps (M CNF -> NameM CNF
forall a. M a -> NameM a
run (M CNF -> NameM CNF)
-> (Problem Form -> M CNF) -> Problem Form -> NameM CNF
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Input Clause] -> [[Input Clause]] -> Problem Form -> M CNF
clausifyInputs [] [])
 where
  clausifyInputs :: [Input Clause] -> [[Input Clause]] -> Problem Form -> M CNF
clausifyInputs [Input Clause]
theory [[Input Clause]]
obligs [] =
    do CNF -> M CNF
forall (m :: * -> *) a. Monad m => a -> m a
return ([Input Clause] -> [[Input Clause]] -> CNF
toCNF ([Input Clause] -> [Input Clause]
forall a. [a] -> [a]
reverse [Input Clause]
theory) ([[Input Clause]] -> [[Input Clause]]
forall a. [a] -> [a]
reverse [[Input Clause]]
obligs))

  -- If using --split, translate a negated_conjecture p
  -- into a conjecture ~p, to allow splitting to occur.
  clausifyInputs [Input Clause]
theory [[Input Clause]]
obligs (Input Form
inp:Problem Form
inps)
    | ClausifyFlags -> Bool
splitting ClausifyFlags
flags, Ax AxKind
NegatedConjecture <- Input Form -> Kind
forall a. Input a -> Kind
kind Input Form
inp =
      [Input Clause] -> [[Input Clause]] -> Problem Form -> M CNF
clausifyInputs [Input Clause]
theory [[Input Clause]]
obligs (Input Form
inp'Input Form -> Problem Form -> Problem Form
forall a. a -> [a] -> [a]
:Problem Form
inps)
    where
      inp' :: Input Form
inp' =
        Input Form
inp {
          kind :: Kind
kind = ConjKind -> Kind
Conj ConjKind
Conjecture,
          what :: Form
what = Form -> Form
Not (Input Form -> Form
forall a. Input a -> a
what Input Form
inp) }

  clausifyInputs [Input Clause]
theory [[Input Clause]]
obligs (Input Form
inp:Problem Form
inps)
    | Ax AxKind
axiom <- Input Form -> Kind
forall a. Input a -> Kind
kind Input Form
inp =
    do [Input Clause]
cs <- AxKind -> Input Form -> M [Input Clause]
clausForm AxKind
axiom Input Form
inp
       [Input Clause] -> [[Input Clause]] -> Problem Form -> M CNF
clausifyInputs ([Input Clause]
cs [Input Clause] -> [Input Clause] -> [Input Clause]
forall a. [a] -> [a] -> [a]
++ [Input Clause]
theory) [[Input Clause]]
obligs Problem Form
inps

  clausifyInputs [Input Clause]
theory [[Input Clause]]
obligs (Input Form
inp:Problem Form
inps)
      -- XX translate question in answer literal
    | Conj ConjKind
_ <- Input Form -> Kind
forall a. Input a -> Kind
kind Input Form
inp =
    do [Input Clause]
-> [[Input Clause]]
-> Input Form
-> [Form]
-> Problem Form
-> M CNF
clausifyObligs [Input Clause]
theory [[Input Clause]]
obligs Input Form
inp (Form -> [Form]
split' (Input Form -> Form
forall a. Input a -> a
what Input Form
inp)) Problem Form
inps

  clausifyObligs :: [Input Clause]
-> [[Input Clause]]
-> Input Form
-> [Form]
-> Problem Form
-> M CNF
clausifyObligs [Input Clause]
theory [[Input Clause]]
obligs Input Form
_ [] Problem Form
inps =
    do [Input Clause] -> [[Input Clause]] -> Problem Form -> M CNF
clausifyInputs [Input Clause]
theory [[Input Clause]]
obligs Problem Form
inps
  
  clausifyObligs [Input Clause]
theory [[Input Clause]]
obligs Input Form
inp (Form
a:[Form]
as) Problem Form
inps =
    do [Input Clause]
cs <-
         AxKind -> Input Form -> M [Input Clause]
clausForm AxKind
NegatedConjecture Input Form
inp {
           what :: Form
what = Form -> Form
nt Form
a,
           source :: InputSource
source = String -> String -> Problem Form -> InputSource
inference String
"negate_conjecture" String
"cth" [Input Form
inp] }
       [Input Clause]
-> [[Input Clause]]
-> Input Form
-> [Form]
-> Problem Form
-> M CNF
clausifyObligs [Input Clause]
theory ([Input Clause]
cs[Input Clause] -> [[Input Clause]] -> [[Input Clause]]
forall a. a -> [a] -> [a]
:[[Input Clause]]
obligs) Input Form
inp [Form]
as Problem Form
inps

  split' :: Form -> [Form]
split' Form
a | ClausifyFlags -> Bool
splitting ClausifyFlags
flags = if [Form] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Form]
split_a then [Form
true] else [Form]
split_a
    where split_a :: [Form]
split_a = Form -> [Form]
split Form
a
  split' Form
a                   = [Form
a]

split :: Form -> [Form]
split :: Form -> [Form]
split Form
p =
  case Form -> Form
positive Form
p of
    ForAll (Bind Set Variable
xs Form
p) ->
      [ Bind Form -> Form
ForAll (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind Set Variable
xs Form
p') | Form
p' <- Form -> [Form]
split Form
p ]
    
    And [Form]
ps -> (Form -> [Form]) -> [Form] -> [Form]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Form -> [Form]
split [Form]
ps
    
    Form
p `Equiv` Form
q ->
      Form -> [Form]
split (Form -> Form
nt Form
p Form -> Form -> Form
\/ Form
q) [Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ Form -> [Form]
split (Form
p Form -> Form -> Form
\/ Form -> Form
nt Form
q)

    Or [Form]
ps ->
      (Int, [Form]) -> [Form]
forall a b. (a, b) -> b
snd ((Int, [Form]) -> [Form]) -> (Int, [Form]) -> [Form]
forall a b. (a -> b) -> a -> b
$
      ((Int, [Form]) -> (Int, [Form]) -> Ordering)
-> [(Int, [Form])] -> (Int, [Form])
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
maximumBy (((Int, [Form]) -> Int)
-> (Int, [Form]) -> (Int, [Form]) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Int, [Form]) -> Int
forall a b. (a, b) -> a
fst)
      [ (Form -> Int
siz Form
q, [ [Form] -> Form
Or (Form
q'Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
:[Form]
qs) | Form
q' <- [Form]
sq ])
      | (Form
q,[Form]
qs) <- [Form] -> [(Form, [Form])]
forall a. [a] -> [(a, [a])]
select [Form]
ps
      , let sq :: [Form]
sq = Form -> [Form]
split Form
q
      ]

    Form
_ ->
      [Form
p]
 where
  select :: [a] -> [(a, [a])]
select []     = []
  select (a
x:[a]
xs) = (a
x,[a]
xs) (a, [a]) -> [(a, [a])] -> [(a, [a])]
forall a. a -> [a] -> [a]
: [ (a
y,a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ys) | (a
y,[a]
ys) <- [a] -> [(a, [a])]
select [a]
xs ]
  
  siz :: Form -> Int
siz (And [Form]
ps)            = [Form] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Form]
ps
  siz (ForAll (Bind Set Variable
_ Form
p)) = Form -> Int
siz Form
p
  siz (Form
_ `Equiv` Form
_)       = Int
2
  siz Form
_                   = Int
0

{-  
    Or ps | length ps > 0 && n > 0 ->
      [ Or (p':ps') | p' <- split p ]
     where
      pns = [(p,siz p) | p <- ps]
      ((p,n),pns') = getMax (head pns) [] (tail pns)
      ps' = [ p' | (p',_) <- pns' ]
    
  getMax pn@(p,n) pns [] = (pn,pns)
  getMax pn@(p,n) pns (qm@(q,m):qms)
    | m > n     = getMax qm (pn:pns) qms
    | otherwise = getMax pn (qm:pns) qms
-}

----------------------------------------------------------------------
-- core clausification algorithm

clausForm :: AxKind -> Input Form -> M [Input Clause]
clausForm :: AxKind -> Input Form -> M [Input Clause]
clausForm AxKind
kind Input Form
inp =
  String -> M [Input Clause] -> M [Input Clause]
forall a. String -> M a -> M a
withName (Input Form -> String
forall a. Input a -> String
tag Input Form
inp) (M [Input Clause] -> M [Input Clause])
-> M [Input Clause] -> M [Input Clause]
forall a b. (a -> b) -> a -> b
$
    do Form
miniscoped      <- Form -> M Form
miniscope (Form -> M Form) -> (Form -> Form) -> Form -> M Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Form -> Form
forall a. Symbolic a => a -> a
check (Form -> Form) -> (Form -> Form) -> Form -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Form -> Form
simplify         (Form -> Form) -> (Form -> Form) -> Form -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Form -> Form
forall a. Symbolic a => a -> a
check (Form -> M Form) -> Form -> M Form
forall a b. (a -> b) -> a -> b
$ Input Form -> Form
forall a. Input a -> a
what Input Form
inp
       [Form]
noEquivPs       <- Form -> M [Form]
removeEquiv                          (Form -> M [Form]) -> (Form -> Form) -> Form -> M [Form]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Form -> Form
forall a. Symbolic a => a -> a
check (Form -> M [Form]) -> Form -> M [Form]
forall a b. (a -> b) -> a -> b
$ Form
miniscoped
       [Form]
noExistsPs      <- (Form -> M Form) -> [Form] -> M [Form]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Form -> M Form
removeExists                    ([Form] -> M [Form]) -> ([Form] -> [Form]) -> [Form] -> M [Form]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Form] -> [Form]
forall a. Symbolic a => a -> a
check ([Form] -> M [Form]) -> [Form] -> M [Form]
forall a b. (a -> b) -> a -> b
$ [Form]
noEquivPs
       [Form]
noExpensiveOrPs <- ([[Form]] -> [Form]) -> ReaderT String NameM [[Form]] -> M [Form]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[Form]] -> [Form]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (ReaderT String NameM [[Form]] -> M [Form])
-> ([Form] -> ReaderT String NameM [[Form]]) -> [Form] -> M [Form]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Form -> M [Form]) -> [Form] -> ReaderT String NameM [[Form]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Form -> M [Form]
removeExpensiveOr ([Form] -> ReaderT String NameM [[Form]])
-> ([Form] -> [Form]) -> [Form] -> ReaderT String NameM [[Form]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Form] -> [Form]
forall a. Symbolic a => a -> a
check ([Form] -> M [Form]) -> [Form] -> M [Form]
forall a b. (a -> b) -> a -> b
$ [Form]
noExistsPs
       [Form]
noForAllPs      <- NameM [Form] -> M [Form]
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (NameM [Form] -> M [Form])
-> ([Form] -> NameM [Form]) -> [Form] -> M [Form]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Form -> NameM Form) -> [Form] -> NameM [Form]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Form -> NameM Form
forall a. Symbolic a => a -> NameM a
uniqueNames              ([Form] -> NameM [Form])
-> ([Form] -> [Form]) -> [Form] -> NameM [Form]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Form] -> [Form]
forall a. Symbolic a => a -> a
check ([Form] -> M [Form]) -> [Form] -> M [Form]
forall a b. (a -> b) -> a -> b
$ [Form]
noExpensiveOrPs
       let !thm :: Input Form
thm         = String -> Kind -> InputSource -> Form -> Input Form
forall a. String -> Kind -> InputSource -> a -> Input a
Input String
"skolemised" (AxKind -> Kind
Ax AxKind
kind) (String -> String -> Problem Form -> InputSource
inference String
"clausify" String
"esa" [Input Form
inp]) ([Form] -> Form
And [Form]
noForAllPs)
           !cnf_ :: [[Literal]]
cnf_        = (Form -> [[Literal]]) -> [Form] -> [[Literal]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Form -> [[Literal]]
cnf                        ([Form] -> [[Literal]])
-> ([Form] -> [Form]) -> [Form] -> [[Literal]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Form] -> [Form]
forall a. Symbolic a => a -> a
check ([Form] -> [[Literal]]) -> [Form] -> [[Literal]]
forall a b. (a -> b) -> a -> b
$ [Form]
noForAllPs
           !simp :: [[Literal]]
simp        = [[Literal]] -> [[Literal]]
simplifyCNF                          ([[Literal]] -> [[Literal]])
-> ([[Literal]] -> [[Literal]]) -> [[Literal]] -> [[Literal]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Literal]] -> [[Literal]]
forall a. Symbolic a => a -> a
check ([[Literal]] -> [[Literal]]) -> [[Literal]] -> [[Literal]]
forall a b. (a -> b) -> a -> b
$ [[Literal]]
cnf_
           cs :: [Clause]
cs           = ([Literal] -> Clause) -> [[Literal]] -> [Clause]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Literal] -> Clause
clause                                  ([[Literal]] -> [Clause]) -> [[Literal]] -> [Clause]
forall a b. (a -> b) -> a -> b
$ [[Literal]]
simp
           inps :: [Input Clause]
inps         = [ String -> Kind -> InputSource -> Clause -> Input Clause
forall a. String -> Kind -> InputSource -> a -> Input a
Input (Input Form -> String
forall a. Input a -> String
tag Input Form
inp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
i) (AxKind -> Kind
Ax AxKind
kind) (String -> String -> Problem Form -> InputSource
inference String
"clausify" String
"thm" [Input Form
thm]) Clause
c
                          | (Clause
c, String
i) <- [Clause] -> [String] -> [(Clause, String)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Clause]
cs (String
""String -> [String] -> [String]
forall a. a -> [a] -> [a]
:
                                        [ Char
'_'Char -> ShowS
forall a. a -> [a] -> [a]
:Integer -> String
forall a. Show a => a -> String
show Integer
i | Integer
i <- [Integer
1..] ]) ]
       [Input Clause] -> M [Input Clause]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Input Clause] -> M [Input Clause])
-> [Input Clause] -> M [Input Clause]
forall a b. (a -> b) -> a -> b
$! [Input Clause] -> [Input Clause]
forall a. Symbolic a => a -> a
force ([Input Clause] -> [Input Clause])
-> ([Input Clause] -> [Input Clause])
-> [Input Clause]
-> [Input Clause]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Input Clause] -> [Input Clause]
forall a. Symbolic a => a -> a
check                                         ([Input Clause] -> [Input Clause])
-> [Input Clause] -> [Input Clause]
forall a b. (a -> b) -> a -> b
$ [Input Clause]
inps

----------------------------------------------------------------------
-- miniscoping
miniscope :: Form -> M Form
miniscope :: Form -> M Form
miniscope t :: Form
t@Literal{} = Form -> M Form
forall (m :: * -> *) a. Monad m => a -> m a
return Form
t
miniscope (Not Form
f) = (Form -> Form) -> M Form -> M Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Form -> Form
Not (Form -> M Form
miniscope Form
f)
miniscope (And [Form]
fs) = ([Form] -> Form) -> M [Form] -> M Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Form] -> Form
And ((Form -> M Form) -> [Form] -> M [Form]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Form -> M Form
miniscope [Form]
fs)
miniscope (Or [Form]
fs) = ([Form] -> Form) -> M [Form] -> M Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Form] -> Form
Or ((Form -> M Form) -> [Form] -> M [Form]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Form -> M Form
miniscope [Form]
fs)
miniscope (Equiv Form
f Form
g) = (Form -> Form -> Form) -> M Form -> M Form -> M Form
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Form -> Form -> Form
Equiv (Form -> M Form
miniscope Form
f) (Form -> M Form
miniscope Form
g)
miniscope (ForAll (Bind Set Variable
xs Form
f)) = Form -> M Form
miniscope Form
f M Form -> (Form -> M Form) -> M Form
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Set Variable -> Form -> M Form
forAll Set Variable
xs
miniscope (Exists (Bind Set Variable
xs Form
f)) = Form -> M Form
miniscope Form
f M Form -> (Form -> M Form) -> M Form
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Set Variable -> Form -> M Form
forAll Set Variable
xs (Form -> M Form) -> (Form -> Form) -> Form -> M Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Form -> Form
nt M Form -> (Form -> M Form) -> M Form
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Form -> M Form
forall (m :: * -> *) a. Monad m => a -> m a
return (Form -> M Form) -> (Form -> Form) -> Form -> M Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Form -> Form
nt

forAll :: Set Variable -> Form -> M Form
forAll :: Set Variable -> Form -> M Form
forAll Set Variable
xs Form
a
  | Set Variable -> Bool
forall a. Set a -> Bool
Set.null Set Variable
ys = Form -> M Form
forall (m :: * -> *) a. Monad m => a -> m a
return Form
a
  | Bool
otherwise =
    case Form -> Form
positive Form
a of
      And [Form]
as ->
        ([Form] -> Form) -> M [Form] -> M Form
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Form] -> Form
And ((Form -> M Form) -> [Form] -> M [Form]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Set Variable -> Form -> M Form
forAll Set Variable
ys) [Form]
as)

      ForAll (Bind Set Variable
zs Form
a) ->
        -- invariant: no variable bound twice on same path
        Set Variable -> Form -> M Form
forAll (Set Variable -> Set Variable -> Set Variable
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Variable
ys Set Variable
zs) Form
a

      Or [Form]
as ->
        Set Variable -> [(Form, Set Variable)] -> M Form
forAllOr Set Variable
ys [ (Form
a, Form -> Set Variable
forall a. Symbolic a => a -> Set Variable
free Form
a) | Form
a <- [Form]
as ]

      Form
_ -> Form -> M Form
forall (m :: * -> *) a. Monad m => a -> m a
return (Bind Form -> Form
ForAll (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind Set Variable
ys Form
a))
  where
    -- no need to quantify over anything not used
    ys :: Set Variable
ys = Set Variable
xs Set Variable -> Set Variable -> Set Variable
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Form -> Set Variable
forall a. Symbolic a => a -> Set Variable
free Form
a

forAllOr :: Set Variable -> [(Form, Set Variable)] -> M Form
forAllOr :: Set Variable -> [(Form, Set Variable)] -> M Form
forAllOr Set Variable
_  [] = Form -> M Form
forall (m :: * -> *) a. Monad m => a -> m a
return Form
false
forAllOr Set Variable
xs [(Form
f, Set Variable
_)] = Set Variable -> Form -> M Form
forAll Set Variable
xs Form
f
forAllOr Set Variable
xs [(Form, Set Variable)]
fs
  | Set Variable -> Bool
forall a. Set a -> Bool
Set.null Set Variable
xs = Form -> M Form
forall (m :: * -> *) a. Monad m => a -> m a
return ((Form -> Form -> Form) -> Form -> [Form] -> Form
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Form -> Form -> Form
(\/) Form
false (((Form, Set Variable) -> Form) -> [(Form, Set Variable)] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Form, Set Variable) -> Form
forall a b. (a, b) -> a
fst [(Form, Set Variable)]
fs))
  | Bool
otherwise = do
    let
      -- Pick a variable to push inwards first
      (Variable
x, Set Variable
xs') = Set Variable -> (Variable, Set Variable)
forall a. Set a -> (a, Set a)
Set.deleteFindMin Set Variable
xs
      ([(Form, Set Variable)]
bs1,[(Form, Set Variable)]
bs2) = ((Form, Set Variable) -> Bool)
-> [(Form, Set Variable)]
-> ([(Form, Set Variable)], [(Form, Set Variable)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((Variable
x Variable -> Set Variable -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member`) (Set Variable -> Bool)
-> ((Form, Set Variable) -> Set Variable)
-> (Form, Set Variable)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Form, Set Variable) -> Set Variable
forall a b. (a, b) -> b
snd) [(Form, Set Variable)]
fs
      -- Also quantify over all variables common to bs1 and bs2
      common :: Set Variable
common = [Set Variable] -> Set Variable
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (((Form, Set Variable) -> Set Variable)
-> [(Form, Set Variable)] -> [Set Variable]
forall a b. (a -> b) -> [a] -> [b]
map (Form, Set Variable) -> Set Variable
forall a b. (a, b) -> b
snd [(Form, Set Variable)]
bs1) Set Variable -> Set Variable -> Set Variable
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` [Set Variable] -> Set Variable
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions (((Form, Set Variable) -> Set Variable)
-> [(Form, Set Variable)] -> [Set Variable]
forall a b. (a -> b) -> [a] -> [b]
map (Form, Set Variable) -> Set Variable
forall a b. (a, b) -> b
snd [(Form, Set Variable)]
bs2) Set Variable -> Set Variable -> Set Variable
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set Variable
xs

    -- (forall x. bs1) \/ bs2
    Form
f <- Set Variable -> [(Form, Set Variable)] -> M Form
forAllOr (Set Variable
xs' Set Variable -> Set Variable -> Set Variable
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set Variable
common) [(Form, Set Variable)]
bs1
    Form
g <- Set Variable -> [(Form, Set Variable)] -> M Form
forAllOr (Set Variable
xs' Set Variable -> Set Variable -> Set Variable
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set Variable
common) [(Form, Set Variable)]
bs2
    Form -> M Form
forall (m :: * -> *) a. Monad m => a -> m a
return (Bind Form -> Form
ForAll (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind Set Variable
common (Bind Form -> Form
ForAll (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind (Variable -> Set Variable
forall a. a -> Set a
Set.singleton Variable
x) Form
f) Form -> Form -> Form
\/ Form
g)))

----------------------------------------------------------------------
-- removing equivalences

-- removeEquiv p -> ps :
--   POST: And ps is equivalent to p (modulo extra symbols)
--   POST: ps has no Equiv and no Not
removeEquiv :: Form -> M [Form]
removeEquiv :: Form -> M [Form]
removeEquiv Form
p =
  do ([Form]
defs,Form
pos,Form
_) <- Bool -> Form -> M ([Form], Form, Form)
removeEquivAux Bool
False Form
p
     [Form] -> M [Form]
forall (m :: * -> *) a. Monad m => a -> m a
return (Form
posForm -> [Form] -> [Form]
forall a. a -> [a] -> [a]
:[Form]
defs)

-- removeEquivAux inEquiv p -> (defs,pos,neg) :
--   PRE: inEquiv is True when we are "under" an Equiv
--   POST: defs is a list of definitions, under which
--         pos is equivalent to p and neg is equivalent to nt p
-- (the reason why "neg" and "nt pos" can be different, is
-- because we want to always code an equivalence as
-- a conjunction of two disjunctions, which leads to fewer
-- clauses -- the "neg" part of the result for the case Equiv
-- below makes use of this)
removeEquivAux :: Bool -> Form -> M ([Form],Form,Form)
removeEquivAux :: Bool -> Form -> M ([Form], Form, Form)
removeEquivAux Bool
inEquiv Form
p =
  case Form -> Form
simple Form
p of
    Not Form
p ->
      do ([Form]
defs,Form
pos,Form
neg) <- Bool -> Form -> M ([Form], Form, Form)
removeEquivAux Bool
inEquiv Form
p
         ([Form], Form, Form) -> M ([Form], Form, Form)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Form]
defs,Form
neg,Form
pos)
  
    And [Form]
ps ->
      do [([Form], Form, Form)]
dps <- [M ([Form], Form, Form)]
-> ReaderT String NameM [([Form], Form, Form)]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ Bool -> Form -> M ([Form], Form, Form)
removeEquivAux Bool
inEquiv Form
p | Form
p <- [Form]
ps ]
         let ([[Form]]
defss,[Form]
poss,[Form]
negs) = [([Form], Form, Form)] -> ([[Form]], [Form], [Form])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 [([Form], Form, Form)]
dps
         ([Form], Form, Form) -> M ([Form], Form, Form)
forall (m :: * -> *) a. Monad m => a -> m a
return ( [[Form]] -> [Form]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Form]]
defss
                , [Form] -> Form
And [Form]
poss
                , [Form] -> Form
Or  [Form]
negs
                )

    ForAll (Bind Set Variable
xs Form
p) ->
      do ([Form]
defs,Form
pos,Form
neg) <- Bool -> Form -> M ([Form], Form, Form)
removeEquivAux Bool
inEquiv Form
p
         ([Form], Form, Form) -> M ([Form], Form, Form)
forall (m :: * -> *) a. Monad m => a -> m a
return ( [Form]
defs
                , Bind Form -> Form
ForAll (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind Set Variable
xs Form
pos)
                , Bind Form -> Form
Exists (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind Set Variable
xs Form
neg)
                )

    Form
p `Equiv` Form
q ->
      do ([Form]
defsp,Form
posp,Form
negp)    <- Bool -> Form -> M ([Form], Form, Form)
removeEquivAux Bool
True Form
p
         ([Form]
defsq,Form
posq,Form
negq)    <- Bool -> Form -> M ([Form], Form, Form)
removeEquivAux Bool
True Form
q
         ([Form]
defsp',Form
posp',Form
negp') <- Bool -> Form -> Form -> M ([Form], Form, Form)
makeCopyable Bool
inEquiv Form
posp Form
negp
         ([Form]
defsq',Form
posq',Form
negq') <- Bool -> Form -> Form -> M ([Form], Form, Form)
makeCopyable Bool
inEquiv Form
posq Form
negq
         ([Form], Form, Form) -> M ([Form], Form, Form)
forall (m :: * -> *) a. Monad m => a -> m a
return ( [[Form]] -> [Form]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Form]
defsp, [Form]
defsq, [Form]
defsp', [Form]
defsq']
                , (Form
negp' Form -> Form -> Form
\/ Form
posq') Form -> Form -> Form
/\ (Form
posp' Form -> Form -> Form
\/ Form
negq')
                , (Form
negp' Form -> Form -> Form
\/ Form
negq') Form -> Form -> Form
/\ (Form
posp' Form -> Form -> Form
\/ Form
posq')
                )

    Literal Literal
l ->
      do ([Form], Form, Form) -> M ([Form], Form, Form)
forall (m :: * -> *) a. Monad m => a -> m a
return ([],Literal -> Form
Literal Literal
l,Literal -> Form
Literal (Literal -> Literal
forall a. Signed a -> Signed a
neg Literal
l))

-- makeCopyable turns an argument to an Equiv into something that we are
-- willing to copy. There are two such cases: (1) when the Equiv is
-- not under another Equiv (because we have to copy arguments to an Equiv
-- at least once anyway), (2) if the formula is small.
-- All other formulas will be made small (by means of a definition)
-- before we copy them.
makeCopyable :: Bool -> Form -> Form -> M ([Form],Form,Form)
makeCopyable :: Bool -> Form -> Form -> M ([Form], Form, Form)
makeCopyable Bool
inEquiv Form
pos Form
neg
  | Form -> Bool
isSmall Form
pos Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
inEquiv =
    -- we skolemize here so that we reuse the skolem function
    -- (if we do this after copying, we get several skolemfunctions)
    do Form
pos' <- Form -> M Form
removeExists Form
pos
       Form
neg' <- Form -> M Form
removeExists Form
neg
       ([Form], Form, Form) -> M ([Form], Form, Form)
forall (m :: * -> *) a. Monad m => a -> m a
return ([],Form
pos',Form
neg')

  | Bool
otherwise =
    do Atomic
dp <- String -> Set Variable -> M Atomic
literal String
"equiv" (Form -> Set Variable
forall a. Symbolic a => a -> Set Variable
free Form
pos)
       ([Form], Form, Form) -> M ([Form], Form, Form)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Literal -> Form
Literal (Atomic -> Literal
forall a. a -> Signed a
Neg Atomic
dp) Form -> Form -> Form
\/ Form
pos, Literal -> Form
Literal (Atomic -> Literal
forall a. a -> Signed a
Pos Atomic
dp) Form -> Form -> Form
\/ Form
neg], Literal -> Form
Literal (Atomic -> Literal
forall a. a -> Signed a
Pos Atomic
dp), Literal -> Form
Literal (Atomic -> Literal
forall a. a -> Signed a
Neg Atomic
dp))
 where
  -- a formula is small if it is already a literal
  isSmall :: Form -> Bool
isSmall (Literal Literal
_)         = Bool
True
  isSmall (Not Form
p)             = Form -> Bool
isSmall Form
p
  isSmall (ForAll (Bind Set Variable
_ Form
p)) = Form -> Bool
isSmall Form
p
  isSmall (Exists (Bind Set Variable
_ Form
p)) = Form -> Bool
isSmall Form
p
  isSmall Form
_                   = Bool
False

----------------------------------------------------------------------
-- skolemization

-- removeExists p -> p'
--   PRE: p has no Equiv and no Not
--   POST: p' is equivalent to p (modulo extra symbols)
--   POST: p' has no Equiv, no Exists, and no Not
removeExists :: Form -> M Form
removeExists :: Form -> M Form
removeExists (And [Form]
ps) =
  do [Form]
ps <- [M Form] -> M [Form]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ Form -> M Form
removeExists Form
p | Form
p <- [Form]
ps ]
     Form -> M Form
forall (m :: * -> *) a. Monad m => a -> m a
return ([Form] -> Form
And [Form]
ps)

removeExists (Or [Form]
ps) =
  do [Form]
ps <- [M Form] -> M [Form]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ Form -> M Form
removeExists Form
p | Form
p <- [Form]
ps ]
     Form -> M Form
forall (m :: * -> *) a. Monad m => a -> m a
return ([Form] -> Form
Or [Form]
ps)
    
removeExists (ForAll (Bind Set Variable
xs Form
p)) =
  do Form
p' <- Form -> M Form
removeExists Form
p
     Form -> M Form
forall (m :: * -> *) a. Monad m => a -> m a
return (Bind Form -> Form
ForAll (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind Set Variable
xs Form
p'))
    
removeExists t :: Form
t@(Exists (Bind Set Variable
xs Form
p)) =
  -- skolemterms have only variables as arguments, arities are large(r)
  do [Subst]
ss <- [ReaderT String NameM Subst] -> ReaderT String NameM [Subst]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ (Term -> Subst)
-> ReaderT String NameM Term -> ReaderT String NameM Subst
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Variable
x Variable -> Term -> Subst
|=>) (Variable -> Set Variable -> ReaderT String NameM Term
skolem Variable
x (Form -> Set Variable
forall a. Symbolic a => a -> Set Variable
free Form
t)) | Variable
x <- Set Variable -> [Variable]
forall a. Set a -> [a]
Set.toList Set Variable
xs ]
     Form -> M Form
removeExists (Subst -> Form -> Form
forall a. Symbolic a => Subst -> a -> a
subst ((Subst -> Subst -> Subst) -> Subst -> [Subst] -> Subst
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Subst -> Subst -> Subst
(|+|) Subst
ids [Subst]
ss) Form
p)
  {-
  -- skolemterms can have other skolemterms as arguments, arities are small(er)
  -- disadvantage: skolemterms are very complicated and deep
  do p' <- skolemize p
     t <- skolem x (delete x (free p'))
     return (subst (x |=> t) p')
  -}

removeExists Form
lit =
  do Form -> M Form
forall (m :: * -> *) a. Monad m => a -> m a
return Form
lit

-- TODO: Avoid recomputing "free" at every step, by having
-- skolemize return the set of free variables as well

-- TODO: Investigate skolemizing top-down instead, find the right
-- optimization

----------------------------------------------------------------------
-- make cheap Ors

removeExpensiveOr :: Form -> M [Form]
removeExpensiveOr :: Form -> M [Form]
removeExpensiveOr Form
p =
  do ([Form]
defs,Form
p',Cost
_) <- Form -> M ([Form], Form, Cost)
removeExpensiveOrAux Form
p
     [Form] -> M [Form]
forall (m :: * -> *) a. Monad m => a -> m a
return (Form
p'Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
:[Form]
defs)

-- cost: represents how it expensive it is to clausify a formula
type Cost = (Integer,Integer) -- (#clauses, #literals)

unitCost :: Cost
unitCost :: Cost
unitCost = (Integer
1,Integer
1)

andCost :: [Cost] -> Cost
andCost :: [Cost] -> Cost
andCost [Cost]
cs = ([Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((Cost -> Integer) -> [Cost] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map Cost -> Integer
forall a b. (a, b) -> a
fst [Cost]
cs), [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ((Cost -> Integer) -> [Cost] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map Cost -> Integer
forall a b. (a, b) -> b
snd [Cost]
cs))

orCost :: [Cost] -> Cost
orCost :: [Cost] -> Cost
orCost []           = (Integer
1,Integer
0)
orCost [Cost
c]          = Cost
c
orCost ((Integer
c1,Integer
l1):[Cost]
cs) = (Integer
c1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
c2, Integer
c1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
l2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
c2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
l1)
 where
  (Integer
c2,Integer
l2) = [Cost] -> Cost
orCost [Cost]
cs
  
removeExpensiveOrAux :: Form -> M ([Form],Form,Cost)
removeExpensiveOrAux :: Form -> M ([Form], Form, Cost)
removeExpensiveOrAux (And [Form]
ps) =
  do [([Form], Form, Cost)]
dcs <- [M ([Form], Form, Cost)]
-> ReaderT String NameM [([Form], Form, Cost)]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ Form -> M ([Form], Form, Cost)
removeExpensiveOrAux Form
p | Form
p <- [Form]
ps ]
     let ([[Form]]
defss,[Form]
ps,[Cost]
costs) = [([Form], Form, Cost)] -> ([[Form]], [Form], [Cost])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 [([Form], Form, Cost)]
dcs
     ([Form], Form, Cost) -> M ([Form], Form, Cost)
forall (m :: * -> *) a. Monad m => a -> m a
return ([[Form]] -> [Form]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Form]]
defss, [Form] -> Form
And [Form]
ps, [Cost] -> Cost
andCost [Cost]
costs)

removeExpensiveOrAux (Or [Form]
ps) =
  do [([Form], Form, Cost)]
dcs <- [M ([Form], Form, Cost)]
-> ReaderT String NameM [([Form], Form, Cost)]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ Form -> M ([Form], Form, Cost)
removeExpensiveOrAux Form
p | Form
p <- [Form]
ps ]
     let ([[Form]]
defss,[Form]
ps,[Cost]
costs) = [([Form], Form, Cost)] -> ([[Form]], [Form], [Cost])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 [([Form], Form, Cost)]
dcs
     ([Form]
defs2,Form
p,Cost
c) <- [(Form, Cost)] -> M ([Form], Form, Cost)
makeOr (((Form, Cost) -> (Form, Cost) -> Ordering)
-> [(Form, Cost)] -> [(Form, Cost)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (((Form, Cost) -> Cost) -> (Form, Cost) -> (Form, Cost) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (Form, Cost) -> Cost
forall a b. (a, b) -> b
snd) ([Form] -> [Cost] -> [(Form, Cost)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Form]
ps [Cost]
costs))
     ([Form], Form, Cost) -> M ([Form], Form, Cost)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Form]
defs2 [Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ [[Form]] -> [Form]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Form]]
defss,Form
p,Cost
c)

removeExpensiveOrAux (ForAll (Bind Set Variable
xs Form
p)) =
  do ([Form]
defs,Form
p',Cost
cost) <- Form -> M ([Form], Form, Cost)
removeExpensiveOrAux Form
p
     ([Form], Form, Cost) -> M ([Form], Form, Cost)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Form -> Form) -> [Form] -> [Form]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Bind Form -> Form
ForAll (Bind Form -> Form) -> (Form -> Bind Form) -> Form -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind Set Variable
xs) [Form]
defs, Bind Form -> Form
ForAll (Set Variable -> Form -> Bind Form
forall a. Set Variable -> a -> Bind a
Bind Set Variable
xs Form
p'), Cost
cost)

removeExpensiveOrAux Form
lit =
  do ([Form], Form, Cost) -> M ([Form], Form, Cost)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Form
lit, Cost
unitCost)

-- input is sorted; small costs first
makeOr :: [(Form,Cost)] -> M ([Form],Form,Cost)
makeOr :: [(Form, Cost)] -> M ([Form], Form, Cost)
makeOr [] =
  do ([Form], Form, Cost) -> M ([Form], Form, Cost)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], Form
false, [Cost] -> Cost
orCost [])

makeOr [(Form
f,Cost
c)] =
  do ([Form], Form, Cost) -> M ([Form], Form, Cost)
forall (m :: * -> *) a. Monad m => a -> m a
return ([],Form
f,Cost
c)

makeOr [(Form, Cost)]
fcs
  | [(Form, Cost)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Form, Cost)]
fcs2 =
    do ([Form], Form, Cost) -> M ([Form], Form, Cost)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], [Form] -> Form
Or (((Form, Cost) -> Form) -> [(Form, Cost)] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Form, Cost) -> Form
forall a b. (a, b) -> a
fst [(Form, Cost)]
fcs1), [Cost] -> Cost
orCost (((Form, Cost) -> Cost) -> [(Form, Cost)] -> [Cost]
forall a b. (a -> b) -> [a] -> [b]
map (Form, Cost) -> Cost
forall a b. (a, b) -> b
snd [(Form, Cost)]
fcs1))

  | Bool
otherwise =
    do Atomic
d <- String -> Set Variable -> M Atomic
literal String
"or" ([Form] -> Set Variable
forall a. Symbolic a => a -> Set Variable
free (((Form, Cost) -> Form) -> [(Form, Cost)] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Form, Cost) -> Form
forall a b. (a, b) -> a
fst [(Form, Cost)]
fcs2))
       ([Form]
defs,Form
p,Cost
_) <- [(Form, Cost)] -> M ([Form], Form, Cost)
makeOr ((Literal -> Form
Literal (Atomic -> Literal
forall a. a -> Signed a
Neg Atomic
d),Cost
unitCost)(Form, Cost) -> [(Form, Cost)] -> [(Form, Cost)]
forall a. a -> [a] -> [a]
:[(Form, Cost)]
fcs2)
       ([Form], Form, Cost) -> M ([Form], Form, Cost)
forall (m :: * -> *) a. Monad m => a -> m a
return ( Form
pForm -> [Form] -> [Form]
forall a. a -> [a] -> [a]
:[Form]
defs
              , [Form] -> Form
Or (Literal -> Form
Literal (Atomic -> Literal
forall a. a -> Signed a
Pos Atomic
d) Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: ((Form, Cost) -> Form) -> [(Form, Cost)] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Form, Cost) -> Form
forall a b. (a, b) -> a
fst [(Form, Cost)]
fcs1)
              , [Cost] -> Cost
orCost (Cost
unitCost Cost -> [Cost] -> [Cost]
forall a. a -> [a] -> [a]
: ((Form, Cost) -> Cost) -> [(Form, Cost)] -> [Cost]
forall a b. (a -> b) -> [a] -> [b]
map (Form, Cost) -> Cost
forall a b. (a, b) -> b
snd [(Form, Cost)]
fcs1)
              )
 where
  ([(Form, Cost)]
fcs1,[(Form, Cost)]
fcs2) = [(Form, Cost)]
-> [(Form, Cost)] -> ([(Form, Cost)], [(Form, Cost)])
forall a a b.
(Ord a, Num a) =>
[(a, (a, b))] -> [(a, (a, b))] -> ([(a, (a, b))], [(a, (a, b))])
split [] [(Form, Cost)]
fcs
  
  split :: [(a, (a, b))] -> [(a, (a, b))] -> ([(a, (a, b))], [(a, (a, b))])
split [(a, (a, b))]
fcs1 []                            = ([(a, (a, b))]
fcs1,[])
  split [(a, (a, b))]
fcs1 (fc :: (a, (a, b))
fc@(a
_,(a
cc,b
_)):[(a, (a, b))]
fcs) | a
cc a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
1 = [(a, (a, b))] -> [(a, (a, b))] -> ([(a, (a, b))], [(a, (a, b))])
split ((a, (a, b))
fc(a, (a, b)) -> [(a, (a, b))] -> [(a, (a, b))]
forall a. a -> [a] -> [a]
:[(a, (a, b))]
fcs1) [(a, (a, b))]
fcs
  split [(a, (a, b))]
fcs1 fcs :: [(a, (a, b))]
fcs@((a
_,(a
cc,b
_)):[(a, (a, b))]
_)  | a
cc a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
2 = (Int -> [(a, (a, b))] -> [(a, (a, b))]
forall a. Int -> [a] -> [a]
take Int
2 [(a, (a, b))]
fcs [(a, (a, b))] -> [(a, (a, b))] -> [(a, (a, b))]
forall a. [a] -> [a] -> [a]
++ [(a, (a, b))]
fcs1, Int -> [(a, (a, b))] -> [(a, (a, b))]
forall a. Int -> [a] -> [a]
drop Int
2 [(a, (a, b))]
fcs)
  split [(a, (a, b))]
fcs1 [(a, (a, b))]
fcs                           = (Int -> [(a, (a, b))] -> [(a, (a, b))]
forall a. Int -> [a] -> [a]
take Int
1 [(a, (a, b))]
fcs [(a, (a, b))] -> [(a, (a, b))] -> [(a, (a, b))]
forall a. [a] -> [a] -> [a]
++ [(a, (a, b))]
fcs1, Int -> [(a, (a, b))] -> [(a, (a, b))]
forall a. Int -> [a] -> [a]
drop Int
1 [(a, (a, b))]
fcs)

----------------------------------------------------------------------
-- clausification

-- cnf p = cs
--   PRE: p has no Equiv, no Exists, and no Not,
--        and each variable is only bound once
--   POST: And (map Or cs) is equivalent to p
cnf :: Form -> [[Literal]]
cnf :: Form -> [[Literal]]
cnf (ForAll (Bind Set Variable
_ Form
p)) = Form -> [[Literal]]
cnf Form
p
cnf (And [Form]
ps)            = (Form -> [[Literal]]) -> [Form] -> [[Literal]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Form -> [[Literal]]
cnf [Form]
ps
cnf (Or [Form]
ps)             = [[[Literal]]] -> [[Literal]]
cross ((Form -> [[Literal]]) -> [Form] -> [[[Literal]]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Form -> [[Literal]]
cnf [Form]
ps)
cnf (Literal Literal
x)         = [[Literal
x]]

cross :: [[[Literal]]] -> [[Literal]]
cross :: [[[Literal]]] -> [[Literal]]
cross [] = [[]]
cross ([[Literal]]
cs:[[[Literal]]]
css) = ([Literal] -> [Literal] -> [Literal])
-> [[Literal]] -> [[Literal]] -> [[Literal]]
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 [Literal] -> [Literal] -> [Literal]
forall a. [a] -> [a] -> [a]
(++) [[Literal]]
cs ([[[Literal]]] -> [[Literal]]
cross [[[Literal]]]
css)

----------------------------------------------------------------------
-- simplification of CNF

simplifyCNF :: [[Literal]] -> [[Literal]]
simplifyCNF :: [[Literal]] -> [[Literal]]
simplifyCNF =
  -- usort: don't generate multiple copies of identical clauses
  [[Literal]] -> [[Literal]]
forall a. Ord a => [a] -> [a]
usort ([[Literal]] -> [[Literal]])
-> ([[Literal]] -> [[Literal]]) -> [[Literal]] -> [[Literal]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Literal] -> [[Literal]]) -> [[Literal]] -> [[Literal]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ([Literal] -> [[Literal]]
tautElim ([Literal] -> [[Literal]])
-> ([Literal] -> [Literal]) -> [Literal] -> [[Literal]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Literal] -> [Literal] -> [Literal]
unify [])
  where -- remove negative variable equalities X != Y by substitution
        unify :: [Literal] -> [Literal] -> [Literal]
unify [Literal]
xs [] = [Literal]
xs
        unify [Literal]
xs (Neg (Var Variable
v :=: t :: Term
t@Var{}):[Literal]
ys) =
          [Literal] -> [Literal] -> [Literal]
unify (Subst -> [Literal] -> [Literal]
forall a. Symbolic a => Subst -> a -> a
subst (Variable
v Variable -> Term -> Subst
|=> Term
t) [Literal]
xs) (Subst -> [Literal] -> [Literal]
forall a. Symbolic a => Subst -> a -> a
subst (Variable
v Variable -> Term -> Subst
|=> Term
t) [Literal]
ys)
        unify [Literal]
xs (Literal
l:[Literal]
ys) = [Literal] -> [Literal] -> [Literal]
unify (Literal
lLiteral -> [Literal] -> [Literal]
forall a. a -> [a] -> [a]
:[Literal]
xs) [Literal]
ys
        -- simplify p | ~p or t = t to true.
        tautElim :: [Literal] -> [[Literal]]
tautElim [Literal]
ls
          | Set Atomic -> Bool
forall a. Set a -> Bool
Set.null (Set Atomic
pos Set Atomic -> Set Atomic -> Set Atomic
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` Set Atomic
neg) Bool -> Bool -> Bool
&& Bool -> Bool
not ((Literal -> Bool) -> [Literal] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Literal -> Bool
tauto [Literal]
ls)
            -- reorder the order of the literals in the clause
            -- so that more clauses become equal;
            -- also, remove duplicate literals from the clause
            = [(Atomic -> Literal) -> [Atomic] -> [Literal]
forall a b. (a -> b) -> [a] -> [b]
map Atomic -> Literal
forall a. a -> Signed a
Neg (Set Atomic -> [Atomic]
forall a. Set a -> [a]
Set.toList Set Atomic
neg) [Literal] -> [Literal] -> [Literal]
forall a. [a] -> [a] -> [a]
++ (Atomic -> Literal) -> [Atomic] -> [Literal]
forall a b. (a -> b) -> [a] -> [b]
map Atomic -> Literal
forall a. a -> Signed a
Pos (Set Atomic -> [Atomic]
forall a. Set a -> [a]
Set.toList Set Atomic
pos)]
          | Bool
otherwise = []
          where pos :: Set Atomic
pos = [Atomic] -> Set Atomic
forall a. Ord a => [a] -> Set a
Set.fromList [ Atomic
l | Pos Atomic
l <- [Literal]
ls ]
                neg :: Set Atomic
neg = [Atomic] -> Set Atomic
forall a. Ord a => [a] -> Set a
Set.fromList [ Atomic
l | Neg Atomic
l <- [Literal]
ls ]
                tauto :: Literal -> Bool
tauto (Pos (Term
t :=: Term
u)) = Term
t Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
u
                tauto Literal
_ = Bool
False

----------------------------------------------------------------------
-- monad

type M = ReaderT Tag NameM

run :: M a -> NameM a
run :: M a -> NameM a
run M a
x = M a -> String -> NameM a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT M a
x String
""

skolemName :: Named a => String -> a -> M Name
skolemName :: String -> a -> M Name
skolemName String
prefix a
v = do
  String
s <- M String
getName
  Name
name <- NameM Name -> M Name
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (a -> NameM Name
forall a. Named a => a -> NameM Name
newName a
v)
  Name -> M Name
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> M Name) -> Name -> M Name
forall a b. (a -> b) -> a -> b
$ String -> Name -> Name
withLabel String
"skolem" (Name -> Name) -> Name -> Name
forall a b. (a -> b) -> a -> b
$ Name -> Renamer -> Name
withRenamer Name
name (Renamer -> Name) -> Renamer -> Name
forall a b. (a -> b) -> a -> b
$ \String
str Int
i ->
    [String] -> String -> Renaming
Renaming [String
prefix String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)] (String -> Renaming) -> String -> Renaming
forall a b. (a -> b) -> a -> b
$
      String
prefix String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ String
"_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
t | String
t <- [String
s, String
str], Bool -> Bool
not (String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
t) ]

withName :: Tag -> M a -> M a
withName :: String -> M a -> M a
withName String
s M a
m = NameM a -> M a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (M a -> String -> NameM a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT M a
m String
s)

getName :: M Tag
getName :: M String
getName = M String
forall (m :: * -> *) r. Monad m => ReaderT r m r
ask

skolem :: Variable -> Set Variable -> M Term
skolem :: Variable -> Set Variable -> ReaderT String NameM Term
skolem (Name
v ::: Type
t) Set Variable
vs =
  do Name
n <- String -> Name -> M Name
forall a. Named a => String -> a -> M Name
skolemName String
"sK" Name
v
     let f :: Name ::: FunType
f = Name
n Name -> FunType -> Name ::: FunType
forall a b. a -> b -> a ::: b
::: [Type] -> Type -> FunType
FunType ((Variable -> Type) -> [Variable] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Variable -> Type
forall a. Typed a => a -> Type
typ [Variable]
args) Type
t
     Term -> ReaderT String NameM Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Name ::: FunType
f (Name ::: FunType) -> [Term] -> Term
:@: (Variable -> Term) -> [Variable] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Variable -> Term
Var [Variable]
args)
 where
  args :: [Variable]
args = Set Variable -> [Variable]
forall a. Set a -> [a]
Set.toList Set Variable
vs

literal :: String -> Set Variable -> M Atomic
literal :: String -> Set Variable -> M Atomic
literal String
w Set Variable
vs =
  do Name
n <- String -> String -> M Name
forall a. Named a => String -> a -> M Name
skolemName String
"sP" String
w
     let p :: Name ::: FunType
p = Name
n Name -> FunType -> Name ::: FunType
forall a b. a -> b -> a ::: b
::: [Type] -> Type -> FunType
FunType ((Variable -> Type) -> [Variable] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Variable -> Type
forall a. Typed a => a -> Type
typ [Variable]
args) Type
O
     Atomic -> M Atomic
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Atomic
Tru (Name ::: FunType
p (Name ::: FunType) -> [Term] -> Term
:@: (Variable -> Term) -> [Variable] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Variable -> Term
Var [Variable]
args))
 where
  args :: [Variable]
args = Set Variable -> [Variable]
forall a. Set a -> [a]
Set.toList Set Variable
vs

----------------------------------------------------------------------
-- the end.