<commit_before>{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances, TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}

module Narradar.Processor.RPO where

import Control.Applicative
import Control.Monad
import Data.List ((\\), groupBy, sortBy, inits)
import qualified Data.Set as Set

import Narradar.Framework.GraphViz

import Narradar.Types
import qualified Narradar.Types.ArgumentFiltering as AF
import Narradar.Framework
import Narradar.Constraints.SAT.Common
import Narradar.Constraints.SAT.RPOAF (rpoAF_NDP, rpoAF_DP, inAF, isUsable, the_symbolR, filtering, OmegaUsable)
import qualified Narradar.Constraints.SAT.RPO as RPO
import qualified Narradar.Constraints.SAT.RPOAF as RPOAF
import Narradar.Utils
import System.IO.Unsafe

import qualified Satchmo.Solver.Yices as Yices
import qualified Satchmo.Solver.Minisat as MiniSat

-- -------------------
-- RPO SAT Processor
-- -------------------
rpo :: (MonadPlus mp, Info info i, Info info o, Processor info RPOProc i o) =>
       i -> Proof info mp o
rpo = apply (RPOProc RPOSAF MiniSat)


data RPOProc = RPOProc Extension Solver
data Extension = RPOSAF | LPOSAF | MPOAF | LPOAF | LPOS | LPO | MPO
data Solver = Yices | MiniSat -- | Funsat

instance (Ord id, Pretty id
         ,Info info (RPOProof id)
         ) =>
    Processor info RPOProc
                  (DPProblem Rewriting  (NarradarTRS (TermF id) Var))
                  (DPProblem Rewriting  (NarradarTRS (TermF id) Var))
   where
    apply (RPOProc RPOSAF Yices) p = procAF p (Yices.solve $ rpoAF_DP True RPOAF.rpos p)
    apply (RPOProc LPOSAF Yices) p = procAF p (Yices.solve $ rpoAF_DP True RPOAF.lpos p)
    apply (RPOProc LPOAF Yices)  p = procAF p (Yices.solve $ rpoAF_DP True RPOAF.lpo  p)
    apply (RPOProc MPOAF Yices)  p = procAF p (Yices.solve $ rpoAF_DP True RPOAF.mpo  p)
    apply (RPOProc LPOS  Yices)  p = proc   p (Yices.solve $ RPO.lposDP p)
    apply (RPOProc LPO   Yices)  p = proc   p (Yices.solve $ RPO.lpoDP p)
    apply (RPOProc MPO   Yices)  p = proc   p (Yices.solve $ RPO.mpoDP p)

    apply (RPOProc RPOSAF MiniSat) p = procAF p (MiniSat.solve $ rpoAF_DP True RPOAF.rpos p)
    apply (RPOProc LPOSAF MiniSat) p = procAF p (MiniSat.solve $ rpoAF_DP True RPOAF.lpos p)
    apply (RPOProc LPOAF MiniSat)  p = procAF p (MiniSat.solve $ rpoAF_DP True RPOAF.lpo  p)
    apply (RPOProc MPOAF MiniSat)  p = procAF p (MiniSat.solve $ rpoAF_DP True RPOAF.mpo  p)
    apply (RPOProc LPOS  MiniSat)  p = proc   p (MiniSat.solve $ RPO.lposDP p)
    apply (RPOProc LPO   MiniSat)  p = proc   p (MiniSat.solve $ RPO.lpoDP p)
    apply (RPOProc MPO   MiniSat)  p = proc   p (MiniSat.solve $ RPO.mpoDP p)

instance (Ord id, Pretty id
         ,Info info (RPOProof id)
         ) => Processor info RPOProc
                             (DPProblem IRewriting (NarradarTRS (TermF id) Var))
                             (DPProblem IRewriting  (NarradarTRS (TermF id) Var))
   where
    apply (RPOProc RPOSAF Yices) p = procAF p (Yices.solve $ rpoAF_DP True RPOAF.rpos p)
    apply (RPOProc LPOSAF Yices) p = procAF p (Yices.solve $ rpoAF_DP True RPOAF.lpos p)
    apply (RPOProc LPOAF  Yices) p = procAF p (Yices.solve $ rpoAF_DP True RPOAF.lpo  p)
    apply (RPOProc MPOAF  Yices) p = procAF p (Yices.solve $ rpoAF_DP True RPOAF.mpo  p)
    apply (RPOProc LPOS  Yices)  p = proc   p (Yices.solve $ RPO.lposDP p)
    apply (RPOProc LPO   Yices)  p = proc   p (Yices.solve $ RPO.lpoDP p)
    apply (RPOProc MPO   Yices)  p = proc   p (Yices.solve $ RPO.mpoDP p)

    apply (RPOProc RPOSAF MiniSat) p = procAF p (MiniSat.solve $ rpoAF_DP True RPOAF.rpos p)
    apply (RPOProc LPOSAF MiniSat) p = procAF p (MiniSat.solve $ rpoAF_DP True RPOAF.lpos p)
    apply (RPOProc LPOAF  MiniSat) p = procAF p (MiniSat.solve $ rpoAF_DP True RPOAF.lpo  p)
    apply (RPOProc MPOAF  MiniSat) p = procAF p (MiniSat.solve $ rpoAF_DP True RPOAF.mpo  p)
    apply (RPOProc LPOS  MiniSat)  p = proc   p (MiniSat.solve $ RPO.lposDP p)
    apply (RPOProc LPO   MiniSat)  p = proc   p (MiniSat.solve $ RPO.lpoDP p)
    apply (RPOProc MPO   MiniSat)  p = proc   p (MiniSat.solve $ RPO.mpoDP p)

-- For Narrowing we need to add the constraint that one of the dps is ground in the rhs
-- TODO And also we do not just remove the strictly decreasing pairs,
--      Instead we need to create two problems, one without the decreasing pairs and one
--      without the ground right hand sides
instance (Ord id, Pretty id
         ,Info info (RPOProof id)
         ) => Processor info RPOProc
                             (DPProblem Narrowing (NarradarTRS (TermF id) Var))
                             (DPProblem Narrowing (NarradarTRS (TermF id) Var))
  where
    apply (RPOProc RPOSAF Yices) p = procNAF p (Yices.solve $ rpoAF_NDP False RPOAF.rpos p)
    apply (RPOProc LPOSAF Yices) p = procNAF p (Yices.solve $ rpoAF_NDP False RPOAF.lpos p)
    apply (RPOProc LPOAF  Yices) p = procNAF p (Yices.solve $ rpoAF_NDP False RPOAF.lpo  p)
    apply (RPOProc MPOAF  Yices) p = procNAF p (Yices.solve $ rpoAF_NDP False RPOAF.mpo  p)

    apply (RPOProc RPOSAF MiniSat) p = procNAF p (MiniSat.solve $ rpoAF_NDP False RPOAF.rpos p)
    apply (RPOProc LPOSAF MiniSat) p = procNAF p (MiniSat.solve $ rpoAF_NDP False RPOAF.lpos p)
    apply (RPOProc LPOAF  MiniSat) p = procNAF p (MiniSat.solve $ rpoAF_NDP False RPOAF.lpo  p)
    apply (RPOProc MPOAF  MiniSat) p = procNAF p (MiniSat.solve $ rpoAF_NDP False RPOAF.mpo  p)

instance (Ord id, Pretty id
         ,Info info (RPOProof id)
         ) => Processor info RPOProc
                        (DPProblem CNarrowing (NarradarTRS (TermF id) Var))
                        (DPProblem CNarrowing (NarradarTRS (TermF id) Var))
  where
    apply (RPOProc RPOSAF Yices) p = procNAF p (Yices.solve $ rpoAF_NDP False RPOAF.rpos p)
    apply (RPOProc LPOSAF Yices) p = procNAF p (Yices.solve $ rpoAF_NDP False RPOAF.lpos p)
    apply (RPOProc LPOAF  Yices) p = procNAF p (Yices.solve $ rpoAF_NDP False RPOAF.lpo  p)
    apply (RPOProc MPOAF  Yices) p = procNAF p (Yices.solve $ rpoAF_NDP False RPOAF.mpo  p)

    apply (RPOProc RPOSAF MiniSat) p = procNAF p (MiniSat.solve $ rpoAF_NDP False RPOAF.rpos p)
    apply (RPOProc LPOSAF MiniSat) p = procNAF p (MiniSat.solve $ rpoAF_NDP False RPOAF.lpos p)
    apply (RPOProc LPOAF  MiniSat) p = procNAF p (MiniSat.solve $ rpoAF_NDP False RPOAF.lpo  p)
    apply (RPOProc MPOAF  MiniSat) p = procNAF p (MiniSat.solve $ rpoAF_NDP False RPOAF.mpo  p)


procAF p m = case unsafePerformIO m of
                  Nothing -> dontKnow (rpoFail p) p
                  Just (dps', symbols) ->
                      let proof = RPOAFProof decreasingDps usableRules symbols
                          decreasingDps = select (rules dps) ([0..length (rules dps)] \\ dps')
                          usableRules   = [ r | r <- rules(getR p), let Just f = rootSymbol (lhs r), f `Set.member` usableSymbols]
                          usableSymbols = Set.fromList [ the_symbolR s | s <- symbols, isUsable s]
                          p'            = setP (restrictDPTRS dps dps') p
                      in singleP proof p p'
       where dps = getP p

procNAF p m = case unsafePerformIO m of
                  Nothing -> dontKnow (rpoFail p) p
                  Just ((non_dec_dps, non_rhsground_dps), symbols) ->
                      let proof = RPOAFProof decreasingDps usableRules symbols
                          decreasingDps = select (rules dps) ([0..length (rules dps)] \\ non_dec_dps)
                          usableRules   = [ r | r <- rules(getR p), let Just f = rootSymbol (lhs r), f `Set.member` usableSymbols]
                          usableSymbols = Set.fromList [ the_symbolR s | s <- symbols, isUsable s]
                          p1            = setP (restrictDPTRS dps non_dec_dps) p
                          p2            = setP (restrictDPTRS dps non_rhsground_dps) p
                      in andP proof p (snub [p1,p2])
       where dps = getP p

proc p m = case unsafePerformIO m of<commit_msg>LPOAF is no longer supported<commit_after>{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances, TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}

module Narradar.Processor.RPO where

import Control.Applicative
import Control.Monad
import Data.List ((\\), groupBy, sortBy, inits)
import qualified Data.Set as Set

import Narradar.Framework.GraphViz

import Narradar.Types
import qualified Narradar.Types.ArgumentFiltering as AF
import Narradar.Framework
import Narradar.Constraints.SAT.Common
import Narradar.Constraints.SAT.RPOAF (rpoAF_NDP, rpoAF_DP, inAF, isUsable, the_symbolR, filtering, OmegaUsable)
import qualified Narradar.Constraints.SAT.RPO as RPO
import qualified Narradar.Constraints.SAT.RPOAF as RPOAF
import Narradar.Utils
import System.IO.Unsafe

import qualified Satchmo.Solver.Yices as Yices
import qualified Satchmo.Solver.Minisat as MiniSat

-- -------------------
-- RPO SAT Processor
-- -------------------
rpo :: (MonadPlus mp, Info info i, Info info o, Processor info RPOProc i o) =>
       i -> Proof info mp o
rpo = apply (RPOProc RPOSAF MiniSat)


data RPOProc = RPOProc Extension Solver
data Extension = RPOSAF | LPOSAF | MPOAF  | LPOS | LPO | MPO
data Solver = Yices | MiniSat -- | Funsat

instance (Ord id, Pretty id
         ,Info info (RPOProof id)
         ) =>
    Processor info RPOProc
                  (DPProblem Rewriting  (NarradarTRS (TermF id) Var))
                  (DPProblem Rewriting  (NarradarTRS (TermF id) Var))
   where
    apply (RPOProc RPOSAF Yices) p = procAF p (Yices.solve $ rpoAF_DP True RPOAF.rpos p)
    apply (RPOProc LPOSAF Yices) p = procAF p (Yices.solve $ rpoAF_DP True RPOAF.lpos p)
    apply (RPOProc MPOAF Yices)  p = procAF p (Yices.solve $ rpoAF_DP True RPOAF.mpo  p)
    apply (RPOProc LPOS  Yices)  p = proc   p (Yices.solve $ RPO.lposDP p)
    apply (RPOProc LPO   Yices)  p = proc   p (Yices.solve $ RPO.lpoDP p)
    apply (RPOProc MPO   Yices)  p = proc   p (Yices.solve $ RPO.mpoDP p)

    apply (RPOProc RPOSAF MiniSat) p = procAF p (MiniSat.solve $ rpoAF_DP True RPOAF.rpos p)
    apply (RPOProc LPOSAF MiniSat) p = procAF p (MiniSat.solve $ rpoAF_DP True RPOAF.lpos p)
    apply (RPOProc MPOAF MiniSat)  p = procAF p (MiniSat.solve $ rpoAF_DP True RPOAF.mpo  p)
    apply (RPOProc LPOS  MiniSat)  p = proc   p (MiniSat.solve $ RPO.lposDP p)
    apply (RPOProc LPO   MiniSat)  p = proc   p (MiniSat.solve $ RPO.lpoDP p)
    apply (RPOProc MPO   MiniSat)  p = proc   p (MiniSat.solve $ RPO.mpoDP p)

instance (Ord id, Pretty id
         ,Info info (RPOProof id)
         ) => Processor info RPOProc
                             (DPProblem IRewriting (NarradarTRS (TermF id) Var))
                             (DPProblem IRewriting  (NarradarTRS (TermF id) Var))
   where
    apply (RPOProc RPOSAF Yices) p = procAF p (Yices.solve $ rpoAF_DP True RPOAF.rpos p)
    apply (RPOProc LPOSAF Yices) p = procAF p (Yices.solve $ rpoAF_DP True RPOAF.lpos p)
    apply (RPOProc MPOAF  Yices) p = procAF p (Yices.solve $ rpoAF_DP True RPOAF.mpo  p)
    apply (RPOProc LPOS  Yices)  p = proc   p (Yices.solve $ RPO.lposDP p)
    apply (RPOProc LPO   Yices)  p = proc   p (Yices.solve $ RPO.lpoDP p)
    apply (RPOProc MPO   Yices)  p = proc   p (Yices.solve $ RPO.mpoDP p)

    apply (RPOProc RPOSAF MiniSat) p = procAF p (MiniSat.solve $ rpoAF_DP True RPOAF.rpos p)
    apply (RPOProc LPOSAF MiniSat) p = procAF p (MiniSat.solve $ rpoAF_DP True RPOAF.lpos p)
    apply (RPOProc MPOAF  MiniSat) p = procAF p (MiniSat.solve $ rpoAF_DP True RPOAF.mpo  p)
    apply (RPOProc LPOS  MiniSat)  p = proc   p (MiniSat.solve $ RPO.lposDP p)
    apply (RPOProc LPO   MiniSat)  p = proc   p (MiniSat.solve $ RPO.lpoDP p)
    apply (RPOProc MPO   MiniSat)  p = proc   p (MiniSat.solve $ RPO.mpoDP p)

-- For Narrowing we need to add the constraint that one of the dps is ground in the rhs
-- TODO And also we do not just remove the strictly decreasing pairs,
--      Instead we need to create two problems, one without the decreasing pairs and one
--      without the ground right hand sides
instance (Ord id, Pretty id
         ,Info info (RPOProof id)
         ) => Processor info RPOProc
                             (DPProblem Narrowing (NarradarTRS (TermF id) Var))
                             (DPProblem Narrowing (NarradarTRS (TermF id) Var))
  where
    apply (RPOProc RPOSAF Yices) p = procNAF p (Yices.solve $ rpoAF_NDP False RPOAF.rpos p)
    apply (RPOProc LPOSAF Yices) p = procNAF p (Yices.solve $ rpoAF_NDP False RPOAF.lpos p)
    apply (RPOProc MPOAF  Yices) p = procNAF p (Yices.solve $ rpoAF_NDP False RPOAF.mpo  p)

    apply (RPOProc RPOSAF MiniSat) p = procNAF p (MiniSat.solve $ rpoAF_NDP False RPOAF.rpos p)
    apply (RPOProc LPOSAF MiniSat) p = procNAF p (MiniSat.solve $ rpoAF_NDP False RPOAF.lpos p)
    apply (RPOProc MPOAF  MiniSat) p = procNAF p (MiniSat.solve $ rpoAF_NDP False RPOAF.mpo  p)

instance (Ord id, Pretty id
         ,Info info (RPOProof id)
         ) => Processor info RPOProc
                        (DPProblem CNarrowing (NarradarTRS (TermF id) Var))
                        (DPProblem CNarrowing (NarradarTRS (TermF id) Var))
  where
    apply (RPOProc RPOSAF Yices) p = procNAF p (Yices.solve $ rpoAF_NDP False RPOAF.rpos p)
    apply (RPOProc LPOSAF Yices) p = procNAF p (Yices.solve $ rpoAF_NDP False RPOAF.lpos p)
    apply (RPOProc MPOAF  Yices) p = procNAF p (Yices.solve $ rpoAF_NDP False RPOAF.mpo  p)

    apply (RPOProc RPOSAF MiniSat) p = procNAF p (MiniSat.solve $ rpoAF_NDP False RPOAF.rpos p)
    apply (RPOProc LPOSAF MiniSat) p = procNAF p (MiniSat.solve $ rpoAF_NDP False RPOAF.lpos p)
    apply (RPOProc MPOAF  MiniSat) p = procNAF p (MiniSat.solve $ rpoAF_NDP False RPOAF.mpo  p)


procAF p m = case unsafePerformIO m of
                  Nothing -> dontKnow (rpoFail p) p
                  Just (dps', symbols) ->
                      let proof = RPOAFProof decreasingDps usableRules symbols
                          decreasingDps = select (rules dps) ([0..length (rules dps)] \\ dps')
                          usableRules   = [ r | r <- rules(getR p), let Just f = rootSymbol (lhs r), f `Set.member` usableSymbols]
                          usableSymbols = Set.fromList [ the_symbolR s | s <- symbols, isUsable s]
                          p'            = setP (restrictDPTRS dps dps') p
                      in singleP proof p p'
       where dps = getP p

procNAF p m = case unsafePerformIO m of
                  Nothing -> dontKnow (rpoFail p) p
                  Just ((non_dec_dps, non_rhsground_dps), symbols) ->
                      let proof = RPOAFProof decreasingDps usableRules symbols
                          decreasingDps = select (rules dps) ([0..length (rules dps)] \\ non_dec_dps)
                          usableRules   = [ r | r <- rules(getR p), let Just f = rootSymbol (lhs r), f `Set.member` usableSymbols]
                          usableSymbols = Set.fromList [ the_symbolR s | s <- symbols, isUsable s]
                          p1            = setP (restrictDPTRS dps non_dec_dps) p
                          p2            = setP (restrictDPTRS dps non_rhsground_dps) p
                      in andP proof p (snub [p1,p2])
       where dps = getP p

proc p m = case unsafePerformIO m of
{'fraction_non_alphanumeric': 0.08874627252690263, 'fraction_numerical': 0.0007779074290159471, 'mean_word_length': 2.4373885918003566, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 23, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3803925', 'n_tokens_mistral': 5936, 'n_tokens_neox': 5692, 'n_words': 1752}