{- |

Module : $Header$

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 thName pState conjec _ = do

let sign = PState.initialSignature pState

axs = PState.initialAxioms pState

showDIMACSProblem thName sign axs $ Just 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 name fSig axs mcons = do

let negatedCons = case mcons of

Nothing -> []

Just cons -> [AS_Anno.mapNamed (negForm Id.nullRange) cons]

tAxs = map (AS_Anno.mapNamed cnf) axs

tCon = fmap (AS_Anno.mapNamed cnf) negatedCons

flatSens = getConj . flip mkConj Id.nullRange . map AS_Anno.sentence

tfAxs = flatSens tAxs

tfCon = flatSens tCon

numVars = Set.size $ Sig.items fSig

numClauses = length tfAxs + length tfCon

sigMap = createSignMap fSig 1 Map.empty

fct = map (++ " 0") . concatMap (`mapClauseAux` sigMap)

return $ unlines $

[ "c " ++ name, "p cnf " ++ show numVars ++ " " ++ show numClauses]

++ (if null tfAxs then [] else "c Axioms" : fct tfAxs)

++ if null tfCon || isNothing mcons then []

else "c Conjectures" : fct tfCon

-- | Create signature map

createSignMap :: Sig.Sign

-> Integer -- ^ Starting number of the variables

-> Map.Map Id.Token Integer

-> Map.Map Id.Token Integer

createSignMap sig inNum inMap =

let it = Sig.items sig

minL = Set.findMin it

nSig = Sig.Sign {Sig.items = Set.deleteMin it}

in if Set.null it then inMap else

createSignMap nSig (inNum + 1)

(Map.insert (Sig.id2SimpleId minL) inNum inMap)

-- | Mapping of a single Clause

mapClause :: AS.FORMULA

-> Map.Map Id.Token Integer

-> String

mapClause form = unlines . map (++ " 0") . mapClauseAux form

-- | Mapping of a single Clause

mapClauseAux :: AS.FORMULA

-> Map.Map Id.Token Integer

-> [String]

mapClauseAux form mapL = case form of

-- unused case: AS.Conjunction ts _ -> map (`mapLiteral` mapL) ts

AS.True_atom _ -> []

AS.False_atom _ -> ["-1", "1"]

_ -> [mapLiteral form mapL]

-- | Mapping of a single literal

mapLiteral :: AS.FORMULA

-> Map.Map Id.Token Integer

-> String

mapLiteral f mapL = case f of

AS.Disjunction ts _ -> unwords $ map (`mapLiteral` mapL) ts

AS.Negation n _ ->

'-' : mapLiteral n mapL

AS.Predication tok -> show (Map.findWithDefault 0 tok mapL)

_ -> error $ "Impossible clause case: " ++ showDoc f ""