BoolBasic.hs revision e9458b1a7a19a63aa4c179f9ab20f4d50681c168
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederDescription : Some basic types for simple boolean representations
cd7372fc7e6e43c389619f63daa6eb872d9d5b16Christian MaederCopyright : (c) Ewaryst Schulz, DFKI Bremen 2010
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederMaintainer : ewaryst.schulz@dfki.de
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederStability : experimental
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederPortability : portable
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederThis module defines some basic types for a simple boolean representation and
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedera printer which outputs this representation into an s-expression like format.
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederThis is mainly for communication with the smt-solver yices.
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder{- ----------------------------------------------------------------------
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederGeneral Datatypes for Extended Parameters
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder---------------------------------------------------------------------- -}
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinidata BoolRep = Not BoolRep | Impl BoolRep BoolRep | And [BoolRep]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini | Or [BoolRep] | Pred String [String]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitrueBool :: BoolRep
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitrueBool = Pred "true" []
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinifalseBool :: BoolRep
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinifalseBool = Pred "false" []
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermapPred :: (String -> [String] -> BoolRep) -> BoolRep -> BoolRep
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimapPred f br =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Not x -> Not $ mapPred f x
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Impl x y -> Impl (mapPred f x) $ mapPred f y
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini And l -> And $ map (mapPred f) l
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Or l -> Or $ map (mapPred f) l
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Pred s l -> f s l
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini{- ----------------------------------------------------------------------
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniOutput for SMT
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini---------------------------------------------------------------------- -}
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinismtBoolExp :: BoolRep -> String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinismtBoolExp br = let f s = g s smtBoolExp
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini g s h l = concat ["(", unwords $ s : map h l, ")"]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini in case br of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Not b -> f "not" [b]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Impl b1 b2 -> f "=>" [b1, b2]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini And l -> f "and" l
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Or l -> f "or" l
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Pred s l -> g s id l