HTab 1.5.5 → 1.5.6

raw patch · 7 files changed

+11/−25 lines, 7 files

Files

• HTab.cabal +2/−2
• examples/sat/blockable1.frm +0/−4
• examples/unsat/trans01.frm +0/−6
• examples/unsat/trans02.frm +0/−7
• src/HTab/Branch.hs +6/−3
• src/HTab/Formula.hs +2/−2
• src/htab.hs +1/−1

@@ -1,5 +1,5 @@ Name:                HTab-Version:             1.5.5+Version:             1.5.6 Synopsis:            Tableau based theorem prover for hybrid logics Description:         Tableau based theorem prover for hybrid logics Homepage:            http://www.glyc.dc.uba.ar/intohylo/htab.php@@ -8,7 +8,7 @@ License:             GPL License-file:        COPYING Author:              Guillaume Hoffmann, Carlos Areces, Daniel Gorín, Juan Heguiabehere-Maintainer:          guillaume.hoffmann@loria.fr+Maintainer:          guillaumh@gmail.com Cabal-version:       >= 1.6.0 Build-type:          Simple 

@@ -1,4 +0,0 @@-begin-@ N1 <> true;-@ N1 []<> (down (X1 @ N1 <> X1))-end

@@ -1,6 +0,0 @@-{unsat}-begin-N1 & P1;-<*>(N1 & [*](-P1 v -N1));-[](N1 v Etrue)-end

@@ -1,7 +0,0 @@-begin-<>(P1 & P2 & N1);-<*>(N1 & -P1);-<*>(-N1 & -[*](-N1 v P2))-end--

@@ -1,5 +1,3 @@-{-# OPTIONS_GHC -fglasgow-exts #-}- ---------------------------------------------------- --                                                -- -- Branch.hs                                      --@@ -180,11 +178,16 @@               " nextprop : " ++ showLit (nextProp br)            ]               where+                  ifNotEmpty :: Emptyable a => a -> (a -> String) -> String                   ifNotEmpty b f = if empty b then "" else f b++                  showl :: (Emptyable a, Show a) => String -> a -> String                   showl intro b  = if empty b then "" else intro ++ show b +                  showIMap :: (a -> String) -> String -> IntMap a -> String                   showIMap vShow sep = IntMap.foldWithKey (\k v -> (++ sep ++ show k ++ " -> " ++ vShow v )) ""-                  showMap vShow sep  = Map.foldWithKey (\k v -> (++ sep ++ show k ++ " -> " ++ vShow v )) ""+                  --+                  showMap vShow sep  = Map.foldrWithKey (\k v -> (++ sep ++ show k ++ " -> " ++ vShow v )) ""                   showMap_lits       = IntMap.foldWithKey (\l d   -> (++ showLit l ++ " " ++ dsShow d  ++ ", ")) ""                   showMap_lits2      = IntMap.foldWithKey (\l fs  -> (++ showLit l ++ " " ++ ":" ++ show fs ++ ", ")) ""                   showMap_rel        = IntMap.foldWithKey (\r dxs -> (++ "-" ++ showRel r ++ "-> " ++ show dxs ++ ", ")) ""

@@ -164,7 +164,7 @@                      deriving (Eq, Show, Ord)  showRelInfo :: RelInfo -> String-showRelInfo = Map.foldWithKey (\r v -> (++ " " ++ showRel r ++ " -> " ++ show v )) ""+showRelInfo = Map.foldrWithKey (\r v -> (++ " " ++ showRel r ++ " -> " ++ show v )) ""  parse :: Params -> String -> (Theory,RelInfo,Encoding,[Task]) parse p s@@ -412,7 +412,7 @@ handleFunInj relI = -- explore the hierarchy of relations starting by the leaves and ending at the top -- taking into account the alternations "inverseof" to enforce functionality and/or injectivity-  Map.foldWithKey startFromLeaf relI relI+  Map.foldrWithKey startFromLeaf relI relI  where startFromLeaf rs props currentRelI = follow rs props currentRelI Not         follow rs props currentRelI currentStatus

@@ -47,7 +47,7 @@       else return Nothing  header :: String-header = unlines ["HTab 1.5.5",+header = unlines ["HTab 1.5.6",                   "G. Hoffmann, C. Areces, D.Gorin and J. Heguiabehere. (c) 2002-2011.",                   "http://code.google.com/p/intohylo/"]