{-# LANGUAGE TypeOperators, CPP #-}
module Jukebox.Tools.AnalyseMonotonicity where

import Prelude hiding (lookup)
import Jukebox.Name
import Jukebox.Form hiding (Form, clause, true, false, And, Or)
import Control.Monad
import qualified Data.Map.Strict as Map
import Data.Map(Map)
#ifndef NO_MINISAT
import Jukebox.Sat.Easy
#endif
import qualified Data.Set as Set
import Data.Set(Set)
import Data.Maybe

data Extension = TrueExtend | FalseExtend | CopyExtend deriving Int -> Extension -> ShowS
[Extension] -> ShowS
Extension -> String
(Int -> Extension -> ShowS)
-> (Extension -> String)
-> ([Extension] -> ShowS)
-> Show Extension
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Extension] -> ShowS
$cshowList :: [Extension] -> ShowS
show :: Extension -> String
$cshow :: Extension -> String
showsPrec :: Int -> Extension -> ShowS
$cshowsPrec :: Int -> Extension -> ShowS
Show

data Var = FalseExtended Function | TrueExtended Function deriving (Var -> Var -> Bool
(Var -> Var -> Bool) -> (Var -> Var -> Bool) -> Eq Var
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Var -> Var -> Bool
$c/= :: Var -> Var -> Bool
== :: Var -> Var -> Bool
$c== :: Var -> Var -> Bool
Eq, Eq Var
Eq Var
-> (Var -> Var -> Ordering)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Bool)
-> (Var -> Var -> Var)
-> (Var -> Var -> Var)
-> Ord Var
Var -> Var -> Bool
Var -> Var -> Ordering
Var -> Var -> Var
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Var -> Var -> Var
$cmin :: Var -> Var -> Var
max :: Var -> Var -> Var
$cmax :: Var -> Var -> Var
>= :: Var -> Var -> Bool
$c>= :: Var -> Var -> Bool
> :: Var -> Var -> Bool
$c> :: Var -> Var -> Bool
<= :: Var -> Var -> Bool
$c<= :: Var -> Var -> Bool
< :: Var -> Var -> Bool
$c< :: Var -> Var -> Bool
compare :: Var -> Var -> Ordering
$ccompare :: Var -> Var -> Ordering
$cp1Ord :: Eq Var
Ord)

analyseMonotonicity :: Problem Clause -> IO (Set Type)
analyseMonotonicity :: Problem Clause -> IO (Set Type)
analyseMonotonicity Problem Clause
prob = do
  Map Type (Maybe (Map Function Extension))
m <- [Clause] -> IO (Map Type (Maybe (Map Function Extension)))
monotone ((Input Clause -> Clause) -> Problem Clause -> [Clause]
forall a b. (a -> b) -> [a] -> [b]
map Input Clause -> Clause
forall a. Input a -> a
what Problem Clause
prob)
  Set Type -> IO (Set Type)
forall (m :: * -> *) a. Monad m => a -> m a
return ([Type] -> Set Type
forall a. Ord a => [a] -> Set a
Set.fromList (Map Type (Maybe (Map Function Extension)) -> [Type]
forall k a. Map k a -> [k]
Map.keys ((Maybe (Map Function Extension) -> Bool)
-> Map Type (Maybe (Map Function Extension))
-> Map Type (Maybe (Map Function Extension))
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter Maybe (Map Function Extension) -> Bool
forall a. Maybe a -> Bool
isJust Map Type (Maybe (Map Function Extension))
m)))

monotone :: [Clause] -> IO (Map Type (Maybe (Map Function Extension)))
#ifdef NO_MINISAT
monotone _ = return Map.empty
#else
monotone :: [Clause] -> IO (Map Type (Maybe (Map Function Extension)))
monotone [Clause]
cs = Watch Var
-> [Type]
-> Sat Var Type (Map Type (Maybe (Map Function Extension)))
-> IO (Map Type (Maybe (Map Function Extension)))
forall b a c. Ord b => Watch a -> [b] -> Sat a b c -> IO c
runSat Watch Var
watch [Type]
tys (Sat Var Type (Map Type (Maybe (Map Function Extension)))
 -> IO (Map Type (Maybe (Map Function Extension))))
-> Sat Var Type (Map Type (Maybe (Map Function Extension)))
-> IO (Map Type (Maybe (Map Function Extension)))
forall a b. (a -> b) -> a -> b
$ do
  let fs :: [Function]
fs = [Clause] -> [Function]
forall a. Symbolic a => a -> [Function]
functions [Clause]
cs
  (Clause -> Sat Var Type ()) -> [Clause] -> Sat Var Type ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Literal] -> Sat Var Type ()
clause ([Literal] -> Sat Var Type ())
-> (Clause -> [Literal]) -> Clause -> Sat Var Type ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> [Literal]
toLiterals) [Clause]
cs
  ([(Type, Maybe (Map Function Extension))]
 -> Map Type (Maybe (Map Function Extension)))
-> Sat Var Type [(Type, Maybe (Map Function Extension))]
-> Sat Var Type (Map Type (Maybe (Map Function Extension)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [(Type, Maybe (Map Function Extension))]
-> Map Type (Maybe (Map Function Extension))
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (Sat Var Type [(Type, Maybe (Map Function Extension))]
 -> Sat Var Type (Map Type (Maybe (Map Function Extension))))
-> ((Type -> Sat Var Type (Type, Maybe (Map Function Extension)))
    -> Sat Var Type [(Type, Maybe (Map Function Extension))])
-> (Type -> Sat Var Type (Type, Maybe (Map Function Extension)))
-> Sat Var Type (Map Type (Maybe (Map Function Extension)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Type]
-> (Type -> Sat Var Type (Type, Maybe (Map Function Extension)))
-> Sat Var Type [(Type, Maybe (Map Function Extension))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Type]
tys ((Type -> Sat Var Type (Type, Maybe (Map Function Extension)))
 -> Sat Var Type (Map Type (Maybe (Map Function Extension))))
-> (Type -> Sat Var Type (Type, Maybe (Map Function Extension)))
-> Sat Var Type (Map Type (Maybe (Map Function Extension)))
forall a b. (a -> b) -> a -> b
$ \Type
ty -> Type
-> Sat1 Var (Type, Maybe (Map Function Extension))
-> Sat Var Type (Type, Maybe (Map Function Extension))
forall a b c. (Ord a, Ord b) => b -> Sat1 a c -> Sat a b c
atIndex Type
ty (Sat1 Var (Type, Maybe (Map Function Extension))
 -> Sat Var Type (Type, Maybe (Map Function Extension)))
-> Sat1 Var (Type, Maybe (Map Function Extension))
-> Sat Var Type (Type, Maybe (Map Function Extension))
forall a b. (a -> b) -> a -> b
$ do
    Bool
r <- [Signed Var] -> Sat1 Var Bool
forall a. Ord a => [Signed a] -> Sat1 a Bool
solve []
    case Bool
r of
      Bool
False -> (Type, Maybe (Map Function Extension))
-> Sat1 Var (Type, Maybe (Map Function Extension))
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty, Maybe (Map Function Extension)
forall a. Maybe a
Nothing)
      Bool
True -> do
        Var -> Bool
m <- Sat1 Var (Var -> Bool)
forall a. Ord a => Sat1 a (a -> Bool)
model
        (Type, Maybe (Map Function Extension))
-> Sat1 Var (Type, Maybe (Map Function Extension))
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty, Map Function Extension -> Maybe (Map Function Extension)
forall a. a -> Maybe a
Just ([Function] -> Type -> (Var -> Bool) -> Map Function Extension
fromModel [Function]
fs Type
ty Var -> Bool
m))
  where watch :: Watch Var
watch (FalseExtended Function
f) =
          Form Var -> Sat1 Var ()
forall a. Ord a => Form a -> Sat1 a ()
addForm ([Form Var] -> Form Var
forall a. [Form a] -> Form a
Or [Signed Var -> Form Var
forall a. Signed a -> Form a
Lit (Var -> Signed Var
forall a. a -> Signed a
Neg (Function -> Var
FalseExtended Function
f)),
                       Signed Var -> Form Var
forall a. Signed a -> Form a
Lit (Var -> Signed Var
forall a. a -> Signed a
Neg (Function -> Var
TrueExtended Function
f))])
        watch Var
_ = () -> Sat1 Var ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        tys :: [Type]
tys = [Clause] -> [Type]
forall a. Symbolic a => a -> [Type]
types' [Clause]
cs

fromModel :: [Function] -> Type -> (Var -> Bool) -> Map Function Extension
fromModel :: [Function] -> Type -> (Var -> Bool) -> Map Function Extension
fromModel [Function]
fs Type
ty Var -> Bool
m = [(Function, Extension)] -> Map Function Extension
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (Function
f, Function -> (Var -> Bool) -> Extension
extension Function
f Var -> Bool
m) | Function
f <- [Function]
fs, Function -> Type
forall a. Typed a => a -> Type
typ Function
f Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
O, Type
ty Type -> [Type] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` FunType -> [Type]
args (Function -> FunType
forall a b. (a ::: b) -> b
rhs Function
f) ]

extension :: Function -> (Var -> Bool) -> Extension
extension :: Function -> (Var -> Bool) -> Extension
extension Function
f Var -> Bool
m =
  case (Var -> Bool
m (Function -> Var
FalseExtended Function
f), Var -> Bool
m (Function -> Var
TrueExtended Function
f)) of
    (Bool
False, Bool
False) -> Extension
CopyExtend
    (Bool
True, Bool
False) -> Extension
FalseExtend
    (Bool
False, Bool
True) -> Extension
TrueExtend

clause :: [Literal] -> Sat Var Type ()
clause :: [Literal] -> Sat Var Type ()
clause [Literal]
ls = (Literal -> Sat Var Type ()) -> [Literal] -> Sat Var Type ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ([Literal] -> Literal -> Sat Var Type ()
literal [Literal]
ls) [Literal]
ls

literal :: [Literal] -> Literal -> Sat Var Type ()
literal :: [Literal] -> Literal -> Sat Var Type ()
literal [Literal]
ls (Pos (Term
t :=: Term
u)) = Type -> Sat1 Var () -> Sat Var Type ()
forall a b c. (Ord a, Ord b) => b -> Sat1 a c -> Sat a b c
atIndex (Term -> Type
forall a. Typed a => a -> Type
typ Term
t) (Sat1 Var () -> Sat Var Type ()) -> Sat1 Var () -> Sat Var Type ()
forall a b. (a -> b) -> a -> b
$ do
  Form Var -> Sat1 Var ()
forall a. Ord a => Form a -> Sat1 a ()
addForm ([Literal] -> Term -> Form Var
safe [Literal]
ls Term
t)
  Form Var -> Sat1 Var ()
forall a. Ord a => Form a -> Sat1 a ()
addForm ([Literal] -> Term -> Form Var
safe [Literal]
ls Term
u)
literal [Literal]
_ls (Neg (Term
_ :=: Term
_)) = () -> Sat Var Type ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
literal [Literal]
ls (Pos (Tru (Function
p :@: [Term]
ts))) =
  [Term] -> (Term -> Sat Var Type ()) -> Sat Var Type ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Term]
ts ((Term -> Sat Var Type ()) -> Sat Var Type ())
-> (Term -> Sat Var Type ()) -> Sat Var Type ()
forall a b. (a -> b) -> a -> b
$ \Term
t -> Type -> Sat1 Var () -> Sat Var Type ()
forall a b c. (Ord a, Ord b) => b -> Sat1 a c -> Sat a b c
atIndex (Term -> Type
forall a. Typed a => a -> Type
typ Term
t) (Sat1 Var () -> Sat Var Type ()) -> Sat1 Var () -> Sat Var Type ()
forall a b. (a -> b) -> a -> b
$ Form Var -> Sat1 Var ()
forall a. Ord a => Form a -> Sat1 a ()
addForm ([Form Var] -> Form Var
forall a. [Form a] -> Form a
Or [[Literal] -> Term -> Form Var
safe [Literal]
ls Term
t, Signed Var -> Form Var
forall a. Signed a -> Form a
Lit (Var -> Signed Var
forall a. a -> Signed a
Neg (Function -> Var
FalseExtended Function
p))])
literal [Literal]
ls (Neg (Tru (Function
p :@: [Term]
ts))) =
  [Term] -> (Term -> Sat Var Type ()) -> Sat Var Type ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Term]
ts ((Term -> Sat Var Type ()) -> Sat Var Type ())
-> (Term -> Sat Var Type ()) -> Sat Var Type ()
forall a b. (a -> b) -> a -> b
$ \Term
t -> Type -> Sat1 Var () -> Sat Var Type ()
forall a b c. (Ord a, Ord b) => b -> Sat1 a c -> Sat a b c
atIndex (Term -> Type
forall a. Typed a => a -> Type
typ Term
t) (Sat1 Var () -> Sat Var Type ()) -> Sat1 Var () -> Sat Var Type ()
forall a b. (a -> b) -> a -> b
$ Form Var -> Sat1 Var ()
forall a. Ord a => Form a -> Sat1 a ()
addForm ([Form Var] -> Form Var
forall a. [Form a] -> Form a
Or [[Literal] -> Term -> Form Var
safe [Literal]
ls Term
t, Signed Var -> Form Var
forall a. Signed a -> Form a
Lit (Var -> Signed Var
forall a. a -> Signed a
Neg (Function -> Var
TrueExtended Function
p))])

safe :: [Literal] -> Term -> Form Var
safe :: [Literal] -> Term -> Form Var
safe [Literal]
ls (Var Variable
x) = [Form Var] -> Form Var
forall a. [Form a] -> Form a
Or [ Literal -> Variable -> Form Var
guards Literal
l Variable
x | Literal
l <- [Literal]
ls ]
safe [Literal]
_ Term
_ = Form Var
forall a. Form a
true

guards :: Literal -> Variable -> Form Var
guards :: Literal -> Variable -> Form Var
guards (Neg (Var Variable
_ :=: Var Variable
_)) Variable
_ = String -> Form Var
forall a. HasCallStack => String -> a
error String
"Monotonicity.guards: found a variable inequality X!=Y after clausification"
guards (Neg (Var Variable
x :=: Term
_)) Variable
y | Variable
x Variable -> Variable -> Bool
forall a. Eq a => a -> a -> Bool
== Variable
y = Form Var
forall a. Form a
true
guards (Neg (Term
_ :=: Var Variable
x)) Variable
y | Variable
x Variable -> Variable -> Bool
forall a. Eq a => a -> a -> Bool
== Variable
y = Form Var
forall a. Form a
true
guards (Pos (Tru (Function
p :@: [Term]
ts))) Variable
x | Variable -> Term
Var Variable
x Term -> [Term] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Term]
ts = Signed Var -> Form Var
forall a. Signed a -> Form a
Lit (Var -> Signed Var
forall a. a -> Signed a
Pos (Function -> Var
TrueExtended Function
p))
guards (Neg (Tru (Function
p :@: [Term]
ts))) Variable
x | Variable -> Term
Var Variable
x Term -> [Term] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Term]
ts = Signed Var -> Form Var
forall a. Signed a -> Form a
Lit (Var -> Signed Var
forall a. a -> Signed a
Pos (Function -> Var
FalseExtended Function
p))
guards Literal
_ Variable
_ = Form Var
forall a. Form a
false
#endif