{-# 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 :: 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))
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)
| 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
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
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) ->
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
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
(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
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
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)))
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 :: 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 :: 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 =
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
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
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)) =
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)
removeExists Form
lit =
do Form -> M Form
forall (m :: * -> *) a. Monad m => a -> m a
return Form
lit
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)
type Cost = (Integer,Integer)
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)
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)
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)
simplifyCNF :: [[Literal]] -> [[Literal]]
simplifyCNF :: [[Literal]] -> [[Literal]]
simplifyCNF =
[[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
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
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)
= [(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
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