{- |
Module      :  ./Propositional/Conversions.hs
Description :  Helper functions for proofs in 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

Helper functions for printing of Theories in DIMACS-CNF Format
-}

module Propositional.Conversions
    ( showDIMACSProblem
    , goalDIMACSProblem
    , createSignMap
    , mapClause
    ) where

import qualified Common.AS_Annotation as AS_Anno
import qualified Common.Id as Id
import Common.DocUtils

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

import qualified Propositional.AS_BASIC_Propositional as AS
import qualified Propositional.ProverState as PState
import qualified Propositional.Sign as Sig

import Propositional.Fold

-- | make a DIMACS Problem for SAT-Solvers
goalDIMACSProblem :: String                   -- ^ name of the theory
                  -> PState.PropProverState   -- ^ initial Prover state
                  -> AS_Anno.Named AS.FORMULA -- ^ goal to prove
                  -> [String]                 -- ^ Options (ignored)
                  -> IO String
goalDIMACSProblem :: String -> PropProverState -> Named FORMULA -> [String] -> IO String
goalDIMACSProblem thName :: String
thName pState :: PropProverState
pState conjec :: Named FORMULA
conjec _ = do
    let sign :: Sign
sign = PropProverState -> Sign
PState.initialSignature PropProverState
pState
        axs :: [Named FORMULA]
axs = PropProverState -> [Named FORMULA]
PState.initialAxioms PropProverState
pState
    String
-> Sign -> [Named FORMULA] -> Maybe (Named FORMULA) -> IO String
showDIMACSProblem String
thName Sign
sign [Named FORMULA]
axs (Maybe (Named FORMULA) -> IO String)
-> Maybe (Named FORMULA) -> IO String
forall a b. (a -> b) -> a -> b
$ Named FORMULA -> Maybe (Named FORMULA)
forall a. a -> Maybe a
Just Named FORMULA
conjec

-- | Translation of a Propositional Formula to a String in DIMACS Format
showDIMACSProblem :: String                     -- ^ name of the theory
                  -> Sig.Sign                   -- ^ Signature
                  -> [AS_Anno.Named AS.FORMULA] -- ^ Axioms
                  -> Maybe (AS_Anno.Named AS.FORMULA) -- ^ Conjectures
                  -> IO String                  -- ^ Output
showDIMACSProblem :: String
-> Sign -> [Named FORMULA] -> Maybe (Named FORMULA) -> IO String
showDIMACSProblem name :: String
name fSig :: Sign
fSig axs :: [Named FORMULA]
axs mcons :: Maybe (Named FORMULA)
mcons = do
    let negatedCons :: [Named FORMULA]
negatedCons = case Maybe (Named FORMULA)
mcons of
          Nothing -> []
          Just cons :: Named FORMULA
cons -> [(FORMULA -> FORMULA) -> Named FORMULA -> Named FORMULA
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
AS_Anno.mapNamed (Range -> FORMULA -> FORMULA
negForm Range
Id.nullRange) Named FORMULA
cons]
        tAxs :: [Named FORMULA]
tAxs = (Named FORMULA -> Named FORMULA)
-> [Named FORMULA] -> [Named FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map ((FORMULA -> FORMULA) -> Named FORMULA -> Named FORMULA
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
AS_Anno.mapNamed FORMULA -> FORMULA
cnf) [Named FORMULA]
axs
        tCon :: [Named FORMULA]
tCon = (Named FORMULA -> Named FORMULA)
-> [Named FORMULA] -> [Named FORMULA]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((FORMULA -> FORMULA) -> Named FORMULA -> Named FORMULA
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
AS_Anno.mapNamed FORMULA -> FORMULA
cnf) [Named FORMULA]
negatedCons
        flatSens :: [SenAttr FORMULA a] -> [FORMULA]
flatSens = FORMULA -> [FORMULA]
getConj (FORMULA -> [FORMULA])
-> ([SenAttr FORMULA a] -> FORMULA)
-> [SenAttr FORMULA a]
-> [FORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([FORMULA] -> Range -> FORMULA) -> Range -> [FORMULA] -> FORMULA
forall a b c. (a -> b -> c) -> b -> a -> c
flip [FORMULA] -> Range -> FORMULA
mkConj Range
Id.nullRange ([FORMULA] -> FORMULA)
-> ([SenAttr FORMULA a] -> [FORMULA])
-> [SenAttr FORMULA a]
-> FORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SenAttr FORMULA a -> FORMULA) -> [SenAttr FORMULA a] -> [FORMULA]
forall a b. (a -> b) -> [a] -> [b]
map SenAttr FORMULA a -> FORMULA
forall s a. SenAttr s a -> s
AS_Anno.sentence
        tfAxs :: [FORMULA]
tfAxs = [Named FORMULA] -> [FORMULA]
forall a. [SenAttr FORMULA a] -> [FORMULA]
flatSens [Named FORMULA]
tAxs
        tfCon :: [FORMULA]
tfCon = [Named FORMULA] -> [FORMULA]
forall a. [SenAttr FORMULA a] -> [FORMULA]
flatSens [Named FORMULA]
tCon
        numVars :: Int
numVars = Set Id -> Int
forall a. Set a -> Int
Set.size (Set Id -> Int) -> Set Id -> Int
forall a b. (a -> b) -> a -> b
$ Sign -> Set Id
Sig.items Sign
fSig
        numClauses :: Int
numClauses = [FORMULA] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FORMULA]
tfAxs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [FORMULA] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FORMULA]
tfCon
        sigMap :: Map Token Integer
sigMap = Sign -> Integer -> Map Token Integer -> Map Token Integer
createSignMap Sign
fSig 1 Map Token Integer
forall k a. Map k a
Map.empty
        fct :: [FORMULA] -> [String]
fct = (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String -> String
forall a. [a] -> [a] -> [a]
++ " 0") ([String] -> [String])
-> ([FORMULA] -> [String]) -> [FORMULA] -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FORMULA -> [String]) -> [FORMULA] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (FORMULA -> Map Token Integer -> [String]
`mapClauseAux` Map Token Integer
sigMap)
    String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> IO String) -> String -> IO String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
       [ "c " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name, "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 Int
numClauses]
       [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (if [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FORMULA]
tfAxs then [] else "c Axioms" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [FORMULA] -> [String]
fct [FORMULA]
tfAxs)
       [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ if [FORMULA] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FORMULA]
tfCon Bool -> Bool -> Bool
|| Maybe (Named FORMULA) -> Bool
forall a. Maybe a -> Bool
isNothing Maybe (Named FORMULA)
mcons then []
          else "c Conjectures" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [FORMULA] -> [String]
fct [FORMULA]
tfCon

-- | Create signature map
createSignMap :: Sig.Sign
              -> Integer -- ^ Starting number of the variables
              -> Map.Map Id.Token Integer
              -> Map.Map Id.Token Integer
createSignMap :: Sign -> Integer -> Map Token Integer -> Map Token Integer
createSignMap sig :: Sign
sig inNum :: Integer
inNum inMap :: Map Token Integer
inMap =
    let it :: Set Id
it = Sign -> Set Id
Sig.items Sign
sig
        minL :: Id
minL = Set Id -> Id
forall a. Set a -> a
Set.findMin Set Id
it
        nSig :: Sign
nSig = Sign :: Set Id -> Sign
Sig.Sign {items :: Set Id
Sig.items = Set Id -> Set Id
forall a. Set a -> Set a
Set.deleteMin Set Id
it}
    in if Set Id -> Bool
forall a. Set a -> Bool
Set.null Set Id
it then Map Token Integer
inMap else
       Sign -> Integer -> Map Token Integer -> Map Token Integer
createSignMap Sign
nSig (Integer
inNum Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ 1)
                 (Token -> Integer -> Map Token Integer -> Map Token Integer
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id -> Token
Sig.id2SimpleId Id
minL) Integer
inNum Map Token Integer
inMap)

-- | Mapping of a single Clause
mapClause :: AS.FORMULA
          -> Map.Map Id.Token Integer
          -> String
mapClause :: FORMULA -> Map Token Integer -> String
mapClause form :: FORMULA
form = [String] -> String
unlines ([String] -> String)
-> (Map Token Integer -> [String]) -> Map Token Integer -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String -> String
forall a. [a] -> [a] -> [a]
++ " 0") ([String] -> [String])
-> (Map Token Integer -> [String]) -> Map Token Integer -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FORMULA -> Map Token Integer -> [String]
mapClauseAux FORMULA
form

-- | Mapping of a single Clause
mapClauseAux :: AS.FORMULA
          -> Map.Map Id.Token Integer
          -> [String]
mapClauseAux :: FORMULA -> Map Token Integer -> [String]
mapClauseAux form :: FORMULA
form mapL :: Map Token Integer
mapL = case FORMULA
form of
      -- unused case: AS.Conjunction ts _ -> map (`mapLiteral` mapL) ts
      AS.True_atom _ -> []
      AS.False_atom _ -> ["-1", "1"]
      _ -> [FORMULA -> Map Token Integer -> String
mapLiteral FORMULA
form Map Token Integer
mapL]

-- | Mapping of a single literal
mapLiteral :: AS.FORMULA
           -> Map.Map Id.Token Integer
           -> String
mapLiteral :: FORMULA -> Map Token Integer -> String
mapLiteral f :: FORMULA
f mapL :: Map Token Integer
mapL = case FORMULA
f of
      AS.Disjunction ts :: [FORMULA]
ts _ -> [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (FORMULA -> String) -> [FORMULA] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (FORMULA -> Map Token Integer -> String
`mapLiteral` Map Token Integer
mapL) [FORMULA]
ts
      AS.Negation n :: FORMULA
n _ ->
        '-' Char -> String -> String
forall a. a -> [a] -> [a]
: FORMULA -> Map Token Integer -> String
mapLiteral FORMULA
n Map Token Integer
mapL
      AS.Predication tok :: Token
tok -> 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 Token
tok Map Token Integer
mapL)
      _ -> String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "Impossible clause case: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ FORMULA -> String -> String
forall a. Pretty a => a -> String -> String
showDoc FORMULA
f ""