{-# 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