{- |
Module      :  ./Propositional/Conservativity.hs
Description :  ConservativityChecker for propositional logic
Copyright   :  (c) Dominik Luecke, Uni Bremen 2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  experimental
Portability :  portable

THe QBF solver sKizzo is used for conservativity checking. This is the
code connecting it to Hets
-}

module Propositional.Conservativity (conserCheck) where

import Common.AS_Annotation
import Common.Consistency
import Common.Id
import Common.Result
import Common.Utils

import System.Directory
import System.Exit

import qualified Data.Map as Map
import qualified Data.Set as Set

-- Propositional Stuff
import Propositional.Sign
import Propositional.AS_BASIC_Propositional
import Propositional.Morphism
import Propositional.Conversions
import Propositional.Fold

proverName :: String
proverName :: String
proverName = "sKizzo"

defOptions :: String
defOptions :: String
defOptions = "-timeout 60"

-- | Conservativity Check for Propositional Logic
conserCheck :: (Sign, [Named FORMULA])      -- ^ Initial sign and formulas
           -> Morphism                      -- ^ morhpism between specs
           -> [Named FORMULA]               -- ^ Formulas of extended spec
           -> IO (Result (Conservativity, [FORMULA]))
conserCheck :: (Sign, [Named FORMULA])
-> Morphism
-> [Named FORMULA]
-> IO (Result (Conservativity, [FORMULA]))
conserCheck (_, inSens :: [Named FORMULA]
inSens) mor :: Morphism
mor cForms :: [Named FORMULA]
cForms = do
      let inSig :: Sign
inSig = Morphism -> Sign
source Morphism
mor
          cSig :: Sign
cSig = Morphism -> Sign
target Morphism
mor
      case (FORMULA -> Result FORMULA) -> [FORMULA] -> Result [FORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Morphism -> FORMULA -> Result FORMULA
mapSentence Morphism
mor) ([FORMULA] -> Result [FORMULA]) -> [FORMULA] -> Result [FORMULA]
forall a b. (a -> b) -> a -> b
$ [Named FORMULA] -> [FORMULA]
getFormulas [Named FORMULA]
inSens of
        Result ds :: [Diagnosis]
ds Nothing -> Result (Conservativity, [FORMULA])
-> IO (Result (Conservativity, [FORMULA]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (Conservativity, [FORMULA])
 -> IO (Result (Conservativity, [FORMULA])))
-> Result (Conservativity, [FORMULA])
-> IO (Result (Conservativity, [FORMULA]))
forall a b. (a -> b) -> a -> b
$ [Diagnosis]
-> Maybe (Conservativity, [FORMULA])
-> Result (Conservativity, [FORMULA])
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds Maybe (Conservativity, [FORMULA])
forall a. Maybe a
Nothing
        Result _ (Just inFormsM :: [FORMULA]
inFormsM) -> do
          let checkForm :: FORMULA
checkForm = FORMULA -> FORMULA -> Range -> FORMULA
Implication
                 ([FORMULA] -> Range -> FORMULA
Conjunction [FORMULA]
inFormsM Range
nullRange)
                 ([FORMULA] -> Range -> FORMULA
Conjunction ((Named FORMULA -> FORMULA) -> [Named FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map Named FORMULA -> FORMULA
forall s a. SenAttr s a -> s
sentence [Named FORMULA]
cForms) Range
nullRange)
                 Range
nullRange
          Sign -> Sign -> FORMULA -> IO (Result (Conservativity, [FORMULA]))
doConservCheck Sign
inSig Sign
cSig FORMULA
checkForm

-- | Extraction of needed formulas, removes all Theorems and Annotations
getFormulas :: [Named FORMULA] -> [FORMULA]
getFormulas :: [Named FORMULA] -> [FORMULA]
getFormulas = (Named FORMULA -> FORMULA) -> [Named FORMULA] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map Named FORMULA -> FORMULA
forall s a. SenAttr s a -> s
sentence ([Named FORMULA] -> [FORMULA])
-> ([Named FORMULA] -> [Named FORMULA])
-> [Named FORMULA]
-> [FORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named FORMULA -> Bool) -> [Named FORMULA] -> [Named FORMULA]
forall a. (a -> Bool) -> [a] -> [a]
filter Named FORMULA -> Bool
forall s a. SenAttr s a -> Bool
isAxiom

doConservCheck :: Sign       -- ^ Initial  Sign
               -> Sign       -- ^ Extended Sign
               -> FORMULA    -- ^ QBF Formula to Prove
               -> IO (Result (Conservativity, [FORMULA]))
doConservCheck :: Sign -> Sign -> FORMULA -> IO (Result (Conservativity, [FORMULA]))
doConservCheck inSig :: Sign
inSig oSig :: Sign
oSig form :: FORMULA
form = do
             let iMap :: Map Token Integer
iMap = Sign -> Integer -> Map Token Integer -> Map Token Integer
createSignMap Sign
oSig 1 Map Token Integer
forall k a. Map k a
Map.empty
                 iSym :: Set Id
iSym = Sign -> Set Id
items Sign
inSig
                 eSym :: Set Id
eSym = Sign -> Set Id
items Sign
oSig Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set Id
iSym
                 fs :: [FORMULA]
fs = FORMULA -> [FORMULA]
getConj (FORMULA -> [FORMULA]) -> FORMULA -> [FORMULA]
forall a b. (a -> b) -> a -> b
$ FORMULA -> FORMULA
cnf FORMULA
form
                 qdim :: String
qdim = Set Id -> Set Id -> Map Token Integer -> [FORMULA] -> String
showQDimacs Set Id
iSym Set Id
eSym Map Token Integer
iMap [FORMULA]
fs
             -- exclude the trivial case that makes sKizzo fail
             if [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FORMULA]
fs then Result (Conservativity, [FORMULA])
-> IO (Result (Conservativity, [FORMULA]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (Conservativity, [FORMULA])
 -> IO (Result (Conservativity, [FORMULA])))
-> Result (Conservativity, [FORMULA])
-> IO (Result (Conservativity, [FORMULA]))
forall a b. (a -> b) -> a -> b
$ (Conservativity, [FORMULA]) -> Result (Conservativity, [FORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return (Conservativity
Cons, []) else do
               Conservativity
res <- String -> IO Conservativity
runSKizzo String
qdim
               Result (Conservativity, [FORMULA])
-> IO (Result (Conservativity, [FORMULA]))
forall (m :: * -> *) a. Monad m => a -> m a
return (Result (Conservativity, [FORMULA])
 -> IO (Result (Conservativity, [FORMULA])))
-> Result (Conservativity, [FORMULA])
-> IO (Result (Conservativity, [FORMULA]))
forall a b. (a -> b) -> a -> b
$ (Conservativity, [FORMULA]) -> Result (Conservativity, [FORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return (Conservativity
res, [])

-- | Printer for QDimacs Format
showQDimacs :: Set.Set Id               -- ^ Symbols of initial  Sign
            -> Set.Set Id               -- ^ New symbols of extended Sign
            -> Map.Map Token Integer    -- ^ Map of Symbols
            -> [FORMULA]          -- ^ Formulas to Translate
            -> String
showQDimacs :: Set Id -> Set Id -> Map Token Integer -> [FORMULA] -> String
showQDimacs inSym :: Set Id
inSym exSym :: Set Id
exSym sigMap :: Map Token Integer
sigMap fforms :: [FORMULA]
fforms =
      let numVars :: Int
numVars = Set Id -> Int
forall a. Set a -> Int
Set.size Set Id
inSym Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Set Id -> Int
forall a. Set a -> Int
Set.size Set Id
exSym
          fct :: Id -> String -> String
fct sym :: Id
sym str :: String
str = Integer -> String
forall a. Show a => a -> String
show (Integer -> Token -> Map Token Integer -> Integer
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault 0 (Id -> Token
id2SimpleId Id
sym) Map Token Integer
sigMap)
                        String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
str
      in "c Conservativity Problem Created by Hets \n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
             "p cnf " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
numVars String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++
             Int -> String
forall a. Show a => a -> String
show ([FORMULA] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FORMULA]
fforms) String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
             "a " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Id -> String -> String) -> String -> Set Id -> String
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold Id -> String -> String
fct "" Set Id
inSym String -> String -> String
forall a. [a] -> [a] -> [a]
++ "0\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
             "e " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Id -> String -> String) -> String -> Set Id -> String
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold Id -> String -> String
fct "" Set Id
exSym String -> String -> String
forall a. [a] -> [a] -> [a]
++ "0\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
             case [FORMULA]
fforms of
                    [] -> ""
                    _ -> "c Axioms\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (FORMULA -> String) -> [FORMULA] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (FORMULA -> Map Token Integer -> String
`mapClause` Map Token Integer
sigMap)
                          [FORMULA]
fforms

-- | Runs sKizzo that has to reside in your path
runSKizzo :: String                  -- ^ File in qdimacs syntax
          -> IO Conservativity
runSKizzo :: String -> IO Conservativity
runSKizzo qd :: String
qd = do
              String
path <- String -> String -> IO String
getTempFile String
qd "sKizzoTemp.qdimacs"
              (exCode :: ExitCode
exCode, out :: String
out, err1 :: String
err1) <- String -> [String] -> String -> IO (ExitCode, String, String)
executeProcess String
proverName
                (String -> [String]
words String
defOptions [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
path]) ""
              let err :: String
err = String
out String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
err1
              String -> IO ()
removeFile String
path
              Conservativity -> IO Conservativity
forall (m :: * -> *) a. Monad m => a -> m a
return (Conservativity -> IO Conservativity)
-> Conservativity -> IO Conservativity
forall a b. (a -> b) -> a -> b
$ case ExitCode
exCode of
                ExitFailure n :: Int
n -> case Int
n of
                  10 -> Conservativity
Cons
                  20 -> Conservativity
Inconsistent
                  _ -> String -> Conservativity
Unknown (String -> Conservativity) -> String -> Conservativity
forall a b. (a -> b) -> a -> b
$ case Int
n of
                    30 -> "Timeout"
                    40 -> "unable to decide"
                    127 -> String
err
                    250 -> "Out of memory"
                    251 -> "sKizzo crashed"
                    254 -> "File not found"
                    -1 -> "sKizzo internal error"
                    -2 -> "I/O error or unexisting file"
                    -3 -> "commandline parse error"
                    -4 -> "DIMACS parse error"
                    -5 -> "sKizzo SIGBUS/SIGSEV crash"
                    -6 -> "unmanaged out of memory"
                    _ -> "Unkown, exit was: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
                   String -> String -> String
forall a. [a] -> [a] -> [a]
++ if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
err then "" else ' ' Char -> String -> String
forall a. a -> [a] -> [a]
: String
err
                _ -> String -> Conservativity
Unknown "Unkown, but successful exit."