HTab 1.5.4 → 1.5.5
raw patch · 17 files changed
+339/−472 lines, 17 filesdep ~cmdargsdep ~hylolibdep ~mtl
Dependency ranges changed: cmdargs, hylolib, mtl
Files
- HTab.cabal +5/−6
- examples/sat/blockable1.frm +4/−0
- examples/sat/trclos1.frm +0/−18
- examples/unsat/trans01.frm +6/−0
- examples/unsat/trans02.frm +7/−0
- src/HTab/Base.hs +0/−75
- src/HTab/Branch.hs +101/−105
- src/HTab/CommandLine.hs +13/−12
- src/HTab/DMap.hs +1/−9
- src/HTab/Formula.hs +23/−36
- src/HTab/Main.hs +38/−42
- src/HTab/ModelGen.hs +5/−1
- src/HTab/RuleId.hs +7/−1
- src/HTab/Rules.hs +96/−94
- src/HTab/Tableau.hs +31/−68
- src/htab.hs +2/−2
- tests/coverage.sh +0/−3
HTab.cabal view
@@ -1,5 +1,5 @@ Name: HTab-Version: 1.5.4+Version: 1.5.5 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@@ -27,8 +27,7 @@ Executable htab Main-is: htab.hs- Other-modules: HTab.Base- HTab.Branch+ Other-modules: HTab.Branch HTab.CommandLine HTab.DisjSet HTab.DMap@@ -41,14 +40,14 @@ HTab.Statistics HTab.Tableau Build-Depends: base >= 4, base < 5,- mtl >= 1, mtl < 2,+ mtl >= 2, mtl < 3, containers < 1, filepath > 1, filepath <= 2, directory > 1, directory <= 2, deepseq >= 1, deepseq <2, strict < 1,- cmdargs == 0.5,- hylolib >= 1.3, hylolib < 1.4+ cmdargs >= 0.6, cmdargs < 0.7,+ hylolib >= 1.3.2, hylolib < 1.4 Extensions: GADTs DeriveDataTypeable FlexibleContexts
+ examples/sat/blockable1.frm view
@@ -0,0 +1,4 @@+begin+@ N1 <> true;+@ N1 []<> (down (X1 @ N1 <> X1))+end
− examples/sat/trclos1.frm
@@ -1,18 +0,0 @@-signature {--propositions { P1, P2, P3, P4 }-nominals { N1, N2 }-relations { R1 , RX : {trclosureof R1} }--}--theory {--!P4 v [R1](!P2 v ))));-!N1 v [RX](!P4 v ))));-P2 v N2:(!P1 v [R1](N1 v [RX](!N1 v !N1:(N2 v ))));-N1 v [R1](P3 v !N2:(!P4 v N2:(N1 v ))));-!N1 v [RX](!P3 v !N2:(N1 v !N1:(!N2 v ))));-!N1 v ))))--}
+ examples/unsat/trans01.frm view
@@ -0,0 +1,6 @@+{unsat}+begin+N1 & P1;+<*>(N1 & [*](-P1 v -N1));+[](N1 v Etrue)+end
+ examples/unsat/trans02.frm view
@@ -0,0 +1,7 @@+begin+<>(P1 & P2 & N1);+<*>(N1 & -P1);+<*>(-N1 & -[*](-N1 v P2))+end++
− src/HTab/Base.hs
@@ -1,75 +0,0 @@-------------------------------------------------------- ----- Base.hs ----- General use functions ----- ---------------------------------------------------------{--Copyright (C) HyLoRes 2002-2005-Carlos Areces - areces@loria.fr - http://www.loria.fr/~areces-Daniel Gorin - dgorin@dc.uba.ar-Juan Heguiabehere - juanh@inf.unibz.it - http://www.inf.unibz.it/~juanh/--This program is free software; you can redistribute it and/or-modify it under the terms of the GNU General Public License-as published by the Free Software Foundation; either version 2-of the License, or (at your option) any later version.--This program is distributed in the hope that it will be useful,-but WITHOUT ANY WARRANTY; without even the implied warranty of-MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the-GNU General Public License for more details.--You should have received a copy of the GNU General Public License-along with this program; if not, write to the Free Software-Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307,-USA.--}--module HTab.Base--where-import qualified Data.Map as Map-import Data.IntMap ( IntMap )-import qualified Data.IntMap as IntMap-import Data.List ( sort )-import qualified Data.Set as Set--almostCartesianProduct :: [a] -> [b] -> [(a,b)]--- example:--- acp [a1,a2,a3] [b1,b2,b3] = [(a1,b2),(a1,b3),(a2,b1),(a2,b3),(a3,b1),(a3,b2)]------ require : as and bs must be of the same size-almostCartesianProduct [] _ = error "almostCartesianProduct: first list empty"-almostCartesianProduct _ [] = error "almostCartesianProduct: second list empty"-almostCartesianProduct as bs = [(a,b) | (idxA,a) <- zip [(0::Int)..] as,- (idxB,b) <- zip [(0::Int)..] bs,- idxA /= idxB]---moveInMap :: IntMap b -> Int -> Int -> (b -> b -> b) -> IntMap b-moveInMap m origKey destKey mergeF- = result- where mOrigValue = IntMap.lookup origKey m- prunedM = IntMap.delete origKey m- result = case mOrigValue of- Nothing -> m- Just origValue -> IntMap.insertWith mergeF destKey origValue prunedM--doMemoize :: Ord a => (a -> b) -> a -> Map.Map a b -> (b, Map.Map a b)-doMemoize f e m = case Map.lookup e m of- Nothing -> let result = f e in (result, Map.insert e result m)- Just result -> (result, m)--permutationOf :: Ord a => [a] -> [a] -> Bool-permutationOf l1 l2 = sort l1 == sort l2--set :: Ord a => [a] -> Set.Set a-set = Set.fromList--list :: Ord a => Set.Set a -> [a]-list = Set.toList--invertMap :: (Ord a, Ord b) => Map.Map a b -> Map.Map b a-invertMap = Map.fromList . map (\(a,b) -> (b,a)) . Map.assocs
src/HTab/Branch.hs view
@@ -9,13 +9,12 @@ module HTab.Branch (-Branch(..), BranchMonad, createNewProp, createNewPref, createNewNomTestRelevance, BranchInfo(..),+Branch(..), createNewProp, createNewPref, createNewNomTestRelevance, BranchInfo(..), addFormulas, addFormula, addAccFormula, addDiaRuleCheck, addDiaXRuleCheck, addDownRuleCheck, addDiffRuleCheck, addParentPrefix, addFirstFormulas,-ScheduledRule(..), TodoList(..),-BranchData(..),-emptyBranch,initialBranchStateFor,prefixes,+TodoList(..),+emptyBranch,prefixes, reduceDisjunctionProposeLazy, doLazyBranching, merge, getUrfather, getUrfatherAndDeps, isInTheModel, relationIsInTheModel,@@ -27,8 +26,6 @@ deleteUEV, insertUEV_addFormula ) where -import Control.Monad.Reader(ReaderT, MonadReader)-import Control.Monad.State(StateT) import Data.List(minimumBy) import Data.Maybe( mapMaybe ) import Data.Ord ( comparing )@@ -42,14 +39,12 @@ import qualified HTab.DisjSet as DS -import HTab.Statistics(Statistics)-import HTab.CommandLine(CmdLineParams(..))+import HTab.CommandLine(Params(..)) import HTab.Formula import HTab.DMap ( DMap(..), toMap ) import qualified HTab.DMap as DMap-import HTab.Base(moveInMap, almostCartesianProduct, doMemoize, set, list) import HTab.Relations ( Relations(..), emptyRels, insertRelation, mergePrefixes, successors, predecessors, linksFromTo )@@ -110,11 +105,11 @@ -- -emptyBranch :: CmdLineParams -> LanguageInfo -> RelInfo -> Encoding -> Branch-emptyBranch clp fLang relInfo_ encoding_ =+emptyBranch :: LanguageInfo -> RelInfo -> Encoding -> Branch+emptyBranch fLang relInfo_ encoding_ = Branch { clashStr = DMap.empty,- todoList = emptyTodoList clp,+ todoList = emptyTodoList, accStr = emptyRels, boxConstrBwd = DMap.empty, boxConstrFwd = DMap.empty,@@ -156,7 +151,7 @@ instance Show Branch where show br- = concat [ "Input language: ", show (inputLanguage br),+ = concat [ show (inputLanguage br), "\nClashable formulas:", showIMap (\v -> "(" ++ showMap_lits v ++ ")") "\n " (toMap $ clashStr br), "\n", show (todoList br), showl "\nRelations: " (accStr br),@@ -217,7 +212,7 @@ empty = Set.null -data TodoList = Unfair{disjTodo :: Set PrFormula,+data TodoList= TodoList{disjTodo :: Set PrFormula, diaTodo :: Set PrFormula, diaXTodo :: Set PrFormula, existTodo :: Set PrFormula,@@ -226,29 +221,16 @@ diffTodo :: Set PrFormula, mergeTodo :: Set (DependencySet, Prefix, DS.Pointer), roleIncTodo :: Set (DependencySet, Prefix, Prefix, [Rel]) }- | Fair [ScheduledRule] instance Show TodoList where- show (Fair srs) = "Todo list: " ++ show srs- show (Unfair disjs dias diaxs es ars downs diffs merges rolein)+ show (TodoList disjs dias diaxs es ars downs diffs merges rolein) = "Todo lists:" ++ concatMap (\el -> "\n" ++ show (list el)) [disjs, dias, diaxs, es, ars, downs, diffs] ++ "\n" ++ show (list merges) ++ "\n" ++ show (list rolein) -data ScheduledRule = SR_Formula PrFormula- | SR_Merge Prefix DS.Pointer DependencySet- | SR_Inclusion Prefix [Rel] Prefix DependencySet--instance Show ScheduledRule where- show (SR_Formula pf) = show pf- show (SR_Merge pr po _) = "Merge " ++ show (pr,po)- show (SR_Inclusion p1 ss p2 _) = "Role inclusion " ++ show p1 ++ "<" ++ show ss ++ ">" ++ show p2--emptyTodoList :: CmdLineParams -> TodoList-emptyTodoList clp =- if fairStrategy clp- then Fair []- else Unfair { disjTodo = Set.empty,+emptyTodoList :: TodoList+emptyTodoList =+ TodoList { disjTodo = Set.empty, diaTodo = Set.empty, diaXTodo = Set.empty, existTodo = Set.empty,@@ -264,32 +246,32 @@ prefixes and nominals -} -addFormulas :: CmdLineParams -> Branch -> [PrFormula] -> BranchInfo-addFormulas clp br fs =+addFormulas :: Params -> Branch -> [PrFormula] -> BranchInfo+addFormulas p br fs = foldr (\f bi -> case bi of- BranchOK br2 -> addFormula clp br2 f+ BranchOK br2 -> addFormula p br2 f clash -> clash ) (BranchOK br) fs -addFormula :: CmdLineParams -> Branch -> PrFormula -> BranchInfo-addFormula clp br pf- = putAwayFormula clp pf- $ bookKeepFormula clp pf br+addFormula :: Params -> Branch -> PrFormula -> BranchInfo+addFormula p br pf+ = putAwayFormula p pf+ $ bookKeepFormula p pf br -bookKeepFormula :: CmdLineParams -> PrFormula -> Branch -> Branch-bookKeepFormula clp pf_ br+bookKeepFormula :: Params -> PrFormula -> Branch -> Branch+bookKeepFormula p pf_ br = addToPrefToForms pf- $ rescheduleLazyBranching clp pf+ $ rescheduleLazyBranching p pf $ rescheduleBlockedDias ur br where (ur,pf) = toUrfather br pf_ -rescheduleLazyBranching :: CmdLineParams -> PrFormula -> Branch -> Branch-rescheduleLazyBranching clp (PrFormula pr ds (Lit l)) br -- pr already urfather- | lazyBranching clp && isProp l+rescheduleLazyBranching :: Params -> PrFormula -> Branch -> Branch+rescheduleLazyBranching p (PrFormula pr ds (Lit l)) br -- pr already urfather+ | lazyBranching p && isProp l = let (Just innerMap) = DMap.lookup1 pr (brWitnesses br) in@@ -315,17 +297,17 @@ rescheduleLazyBranching _ _ br = br -putAwayFormula :: CmdLineParams -> PrFormula -> Branch -> BranchInfo-putAwayFormula clp pf@(PrFormula pr ds f2) br =+putAwayFormula :: Params -> PrFormula -> Branch -> BranchInfo+putAwayFormula p pf@(PrFormula pr ds f2) br = case f2 of- Con fs -> addFormulas clp br (prefix pr ds fs)- Dis _ -> putAwayDisjunction clp pf br+ Con fs -> addFormulas p br (prefix pr ds fs)+ Dis _ -> putAwayDisjunction p pf br Dia _ _ -> BranchOK $ addToTodo pf br DiaX _ _ _ -> BranchOK $ addToTodo pf br- Box r f -> addBoxConstraint pr r f ds clp br- BoxX r f -> addBoxXConstraint pr r f ds clp br- A f -> addUnivConstraint f ds clp br- B f -> b_rule pr f ds clp br+ Box r f -> addBoxConstraint pr r f ds p br+ BoxX r f -> addBoxXConstraint pr r f ds p br+ A f -> addUnivConstraint f ds p br+ B f -> b_rule pr f ds p br E _ -> BranchOK $ addToTodo pf br D _ -> BranchOK $ addToTodo pf br At _ _ -> BranchOK $ addToTodo pf br@@ -333,9 +315,9 @@ Lit l | isPositiveNom l -> addToClashable pr ds l $ addToTodo pf br Lit l -> addToClashable pr ds l br -putAwayDisjunction :: CmdLineParams -> PrFormula -> Branch -> BranchInfo-putAwayDisjunction clp pf@(PrFormula pr ds f@(Dis fs)) br- | lazyBranching clp && ur <= unblockedPrefsLim br+putAwayDisjunction :: Params -> PrFormula -> Branch -> BranchInfo+putAwayDisjunction p pf@(PrFormula pr ds f@(Dis fs)) br+ | lazyBranching p && ur <= unblockedPrefsLim br = case reduceDisjunctionProposeLazy br pr fs of Contradiction dsClash -> BranchClash br pr (dsUnion ds dsClash) f Triviality -> BranchOK br@@ -380,13 +362,8 @@ then br else brWithSaturation{todoList = newTodoList} where+ utodo = todoList br newTodoList =- case todoList br of- Fair srs -> case f2 of- Lit l | isPositiveNom l- -> Fair ( srs ++ [SR_Merge p (DS.Nominal l) ds] )- _ -> Fair ( srs ++ [SR_Formula pf])- utodo -> case f2 of Dis _ -> utodo{ disjTodo = Set.insert pf ( disjTodo utodo)} Dia _ _ -> utodo{ diaTodo = Set.insert pf ( diaTodo utodo)}@@ -424,8 +401,8 @@ {- helper functions for equivalence class merge -} -merge :: CmdLineParams -> Branch -> Prefix -> DependencySet -> DS.Pointer -> BranchInfo-merge clp br pr fDs pointer -- pointer is a nominal or a prefix+merge :: Params -> Branch -> Prefix -> DependencySet -> DS.Pointer -> BranchInfo+merge p br pr fDs pointer -- pointer is a nominal or a prefix = let (DS.Prefix ur1,classes1) = DS.find (DS.Prefix pr) (nomPrefClasses br) (poAncestor ,classes2) = DS.find pointer classes1@@ -493,7 +470,7 @@ clashStr = newClashStr, brWitnesses = newBrWitnesses} in- addFormulas clp newBr formulasToAdd+ addFormulas p newBr formulasToAdd mergeWitnesses :: Prefix -> Prefix -> Clashable_info_slot -> Branching_witnesses -> (Branching_witnesses, [PrFormula]) mergeWitnesses oldUr newUr urfatherSlot dbrWits@(DMap brWits)@@ -600,9 +577,9 @@ deleteUEV :: Branch -> Int -> Branch deleteUEV br idx = br{eventualities = IntMap.delete idx (eventualities br)} -insertUEV_addFormula :: Branch -> CmdLineParams -> Maybe Int -> DependencySet -> (Int -> PrFormula) -> BranchInfo-insertUEV_addFormula br clp mi ds ff- = addFormula clp br2 f+insertUEV_addFormula :: Branch -> Params -> Maybe Int -> DependencySet -> (Int -> PrFormula) -> BranchInfo+insertUEV_addFormula br p mi ds ff+ = addFormula p br2 f where idxToUse = case mi of Nothing -> case IntMap.maxViewWithKey $ eventualities br of Nothing -> 0@@ -623,31 +600,31 @@ (f,ds1) <- (IntMap.!) mapBox r1, (p,ds2) <- (IntMap.!) mapAcc r2 ] -addBoxConstraint :: Prefix -> Rel -> Formula -> DependencySet -> CmdLineParams -> Branch -> BranchInfo-addBoxConstraint pr_ r f ds clp br_+addBoxConstraint :: Prefix -> Rel -> Formula -> DependencySet -> Params -> Branch -> BranchInfo+addBoxConstraint pr_ r f ds p br_ | boxAlreadyDone br_ pr (r,f) = BranchOK br_ | isForward r = let newBr = br{boxConstrFwd = updateBoxConstr pr r f ds (boxConstrFwd br)} accessiblePrDs = IntMap.findWithDefault [] r $ successors (accStr br) pr toAdd = symApplications ++ transApplications ++ boxApplications transApplications = if isTransitive (relInfo br) r- then map (\(p,ds2) -> PrFormula p (dsUnion ds ds2) (Box r f)) accessiblePrDs+ then map (\(pr2,ds2) -> PrFormula pr2 (dsUnion ds ds2) (Box r f)) accessiblePrDs else [] symApplications = [PrFormula pr ds $ Box (invRel r) f | isSymmetric (relInfo br) r]- boxApplications = map (\(p,ds2) -> PrFormula p (dsUnion ds ds2) f) accessiblePrDs+ boxApplications = map (\(pr2,ds2) -> PrFormula pr2 (dsUnion ds ds2) f) accessiblePrDs in- addFormulas clp newBr toAdd+ addFormulas p newBr toAdd | otherwise = let newBr = br{boxConstrBwd = updateBoxConstr pr (atom r) f ds (boxConstrBwd br)} accessiblePrDs = IntMap.findWithDefault [] (atom r) $ predecessors (accStr br) pr toAdd = transApplications ++ boxApplications -- no symApplications cause inv rewritten as forward during parsing transApplications = if isTransitive (relInfo br) (atom r)- then map (\(p,ds2) -> PrFormula p (dsUnion ds ds2) (Box r f)) accessiblePrDs+ then map (\(pr2,ds2) -> PrFormula pr2 (dsUnion ds ds2) (Box r f)) accessiblePrDs else []- boxApplications = map (\(p,ds2) -> PrFormula p (dsUnion ds ds2) f) accessiblePrDs+ boxApplications = map (\(pr2,ds2) -> PrFormula pr2 (dsUnion ds ds2) f) accessiblePrDs in- addFormulas clp newBr toAdd+ addFormulas p newBr toAdd where pr = getUrfather br_ (DS.Prefix pr_) br = addBoxRuleCheck br_ pr (r,f) @@ -672,10 +649,10 @@ -- [*]phi --> phi & [][*]phi -- need not to do all that addBoxConstraint does-addBoxXConstraint :: Prefix -> Rel -> Formula -> DependencySet -> CmdLineParams -> Branch -> BranchInfo-addBoxXConstraint pr r f ds clp br+addBoxXConstraint :: Prefix -> Rel -> Formula -> DependencySet -> Params -> Branch -> BranchInfo+addBoxXConstraint pr r f ds p br | boxXAlreadyDone br ur (r,f) = BranchOK br- | otherwise = addFormulas clp br2 [PrFormula pr ds f, PrFormula pr ds (Box r (BoxX r f))]+ | otherwise = addFormulas p br2 [PrFormula pr ds f, PrFormula pr ds (Box r (BoxX r f))] where ur = getUrfather br (DS.Prefix pr) br2 = addBoxXRuleCheck br ur (r,f) @@ -689,11 +666,11 @@ Nothing -> False Just fset -> Set.member (r,f) fset -addAccFormula :: CmdLineParams -> Branch -> AccFormula -> BranchInfo-addAccFormula clp br (AccFormula ds r p1_ p2_)- | isBackwards r = addAccFormula clp br (AccFormula ds (invRel r) p2_ p1_)+addAccFormula :: Params -> Branch -> AccFormula -> BranchInfo+addAccFormula p br (AccFormula ds r p1_ p2_)+ | isBackwards r = addAccFormula p br (AccFormula ds (invRel r) p2_ p1_) | otherwise -- forward- = addFormulas clp newBr toAdd+ = addFormulas p newBr toAdd where toAdd = transApplications ++ boxApplications transApplications = if isTransitive (relInfo br) r then@@ -719,10 +696,8 @@ Just props -> [ rs | SubsetOf rs <- props] toschedule = map (\parents -> (ds,p1,p2,parents)) $ filter (not . alreadyDone) parentss alreadyDone = any (`elem` linksFromTo (accStr br) p1 p2)- newTodoList =- case todoList br of- Fair srs -> Fair (srs ++ map (\(ds_,p1_,p2_,parents_) -> SR_Inclusion p1_ parents_ p2_ ds_) toschedule )- utodo -> utodo{roleIncTodo = Set.union (Set.fromList toschedule) (roleIncTodo utodo)}+ utodo = todoList br+ newTodoList = utodo{roleIncTodo = Set.union (Set.fromList toschedule) (roleIncTodo utodo)} insertRelationBranch :: Branch -> Prefix -> Rel -> Prefix -> DependencySet -> Branch insertRelationBranch br p1 r p2 ds@@ -906,19 +881,19 @@ -- -addUnivConstraint :: Formula -> DependencySet -> CmdLineParams -> Branch -> BranchInfo-addUnivConstraint f ds clp br- = addFormulas clp newBr- ( map (\p -> PrFormula p ds f) urfathers )+addUnivConstraint :: Formula -> DependencySet -> Params -> Branch -> BranchInfo+addUnivConstraint f ds p br+ = addFormulas p newBr+ ( map (\pr -> PrFormula pr ds f) urfathers ) where newBr = br{univCons = (ds,f):(univCons br)} prefs = [0..(lastPref br)] urfathers = filter (isNominalUrfather br) prefs -- -b_rule :: Prefix -> Formula -> DependencySet -> CmdLineParams -> Branch -> BranchInfo-b_rule pr f ds clp br- = addFormula clp br2 (PrFormula pr ds $ Down newNom $ A (Lit newNom `disj` f))+b_rule :: Prefix -> Formula -> DependencySet -> Params -> Branch -> BranchInfo+b_rule pr f ds p br+ = addFormula p br2 (PrFormula pr ds $ Down newNom $ A (Lit newNom `disj` f)) where newNom = nextNom br br2 = br{nextNom = nextNom br + 4} --@@ -928,9 +903,9 @@ -- -createNewPref :: CmdLineParams -> Branch -> BranchInfo-createNewPref clp br- = addFormulas clp newBrWithRefl+createNewPref :: Params -> Branch -> BranchInfo+createNewPref p br+ = addFormulas p newBrWithRefl ( map (\(ds,f) -> PrFormula newPr ds f) univConstraints ) where newPr = lastPref br + 1 newBr = br{lastPref = newPr}@@ -965,9 +940,9 @@ -- (even if the nominal was filtered out during lexical normalisation) -- <= TODO currently not the case. Get the nominals from the encoding -- - add reflexive links for prefixes 0 and nominal witnesses -- - add functionality and injectivitty down-arrow formulas-addFirstFormulas :: CmdLineParams -> Branch -> LanguageInfo -> Formula -> BranchInfo-addFirstFormulas clp br_ fLang f- = addFormulas clp br5 ([pf]++funUniv++injUniv)+addFirstFormulas :: Params -> Branch -> LanguageInfo -> Formula -> BranchInfo+addFirstFormulas p br_ fLang f+ = addFormulas p br5 ([pf]++funUniv++injUniv) where ns = languageNoms fLang nbNs = length ns nomWitnesses = [1..nbNs]@@ -981,7 +956,7 @@ (zip [1..] ns) br2 = br{nomPrefClasses = newClasses, clashStr = newClashStr}- br3 = foldr (\(pr,n) -> bookKeepFormula clp (PrFormula pr dsEmpty (Lit n)))+ br3 = foldr (\(pr,n) -> bookKeepFormula p (PrFormula pr dsEmpty (Lit n))) br2 (zip [1..] ns) funUniv = map (\r -> PrFormula 0 dsEmpty@@ -1147,12 +1122,33 @@ isTransitive :: RelInfo -> Rel -> Bool isTransitive = hasProperty Transitive -{- Monad related stuff -}+almostCartesianProduct :: [a] -> [b] -> [(a,b)]+-- example:+-- acp [a1,a2,a3] [b1,b2,b3] = [(a1,b2),(a1,b3),(a2,b1),(a2,b3),(a3,b1),(a3,b2)]+--+-- require : as and bs must be of the same size+almostCartesianProduct [] _ = error "almostCartesianProduct: first list empty"+almostCartesianProduct _ [] = error "almostCartesianProduct: second list empty"+almostCartesianProduct as bs = [(a,b) | (idxA,a) <- zip [(0::Int)..] as,+ (idxB,b) <- zip [(0::Int)..] bs,+ idxA /= idxB] -data BranchData = BranchData { branch_clp :: CmdLineParams }+moveInMap :: IntMap b -> Int -> Int -> (b -> b -> b) -> IntMap b+moveInMap m origKey destKey mergeF+ = result+ where mOrigValue = IntMap.lookup origKey m+ prunedM = IntMap.delete origKey m+ result = case mOrigValue of+ Nothing -> m+ Just origValue -> IntMap.insertWith mergeF destKey origValue prunedM -type BranchMonad a = ReaderT BranchData (StateT Statistics IO) a+doMemoize :: Ord a => (a -> b) -> a -> Map.Map a b -> (b, Map.Map a b)+doMemoize f e m = case Map.lookup e m of+ Nothing -> let result = f e in (result, Map.insert e result m)+ Just result -> (result, m) -initialBranchStateFor :: (MonadReader BranchData m) => (m a -> BranchData -> b) -> BranchData -> m a -> b-initialBranchStateFor f bd = flip f bd+list :: Ord a => Set.Set a -> [a]+list = Set.toList +set :: Ord a => [a] -> Set.Set a+set = Set.fromList
src/HTab/CommandLine.hs view
@@ -7,22 +7,22 @@ ---------------------------------------------------- module HTab.CommandLine (- CmdLineParams(..), UnitProp(..),+ Params(..), UnitProp(..), defaultParams, configureStats, checkParams ) where import System.Console.CmdArgs+import Data.List ( sort ) -import HTab.Base( permutationOf ) import HTab.Statistics( StatisticsState, setPrintOutInterval ) -data CmdLineParams = CLP {+data Params = Params { filename :: Maybe FilePath, genModel :: Maybe FilePath,+ dotModel :: Bool, timeout :: Int, stats :: Int, strategy :: String,- fairStrategy :: Bool, semBranch :: Bool, backjumping :: Bool, lazyBranching :: Bool,@@ -38,15 +38,15 @@ data UnitProp = Eager | UPYes | UPNo deriving (Data, Typeable, Eq, Show) -defaultParams :: CmdLineParams+defaultParams :: Params defaultParams- = CLP{+ = Params{ filename = Nothing &= name "f" &= typFile &= help "input file", genModel = Nothing &= name "m" &= typFile &= help "output model file",+ dotModel = False &= typFile &= help "output model in dot format (otherwise: hylolib format)", timeout = 0 &= name "t" &= help "timeout (in seconds, default=none)", stats = 0 &= help "display statistics every n steps (default=none)", strategy = strategyVal &= help "specify rule order",- fairStrategy = False &= help "enable fair strategy", semBranch = True &= help "enable semantic branching (default)", backjumping = True &= help "enable backjumping (default)", lazyBranching = True &= help "enable lazy branching (default)" ,@@ -65,9 +65,9 @@ strategyVal :: String strategyVal = "n@E<Db|*r" -checkParams :: CmdLineParams -> IO Bool-checkParams clp- = if (strategy clp) `permutationOf` strategyVal+checkParams :: Params -> IO Bool+checkParams p+ = if strategy p `permutationOf` strategyVal then return True else do putStrLn $ unlines ["ERROR",@@ -82,6 +82,7 @@ "The rules conjunction, box, universal modality and converse difference", "modality are immediate, thus do not belong to the strategy."] return False+ where permutationOf l1 l2 = sort l1 == sort l2 -configureStats :: CmdLineParams -> StatisticsState ()-configureStats clp = setPrintOutInterval $ stats clp+configureStats :: Params -> StatisticsState ()+configureStats p = setPrintOutInterval $ stats p
src/HTab/DMap.hs view
@@ -6,11 +6,6 @@ where --- import Test.QuickCheck ( Arbitrary(..), Gen, Property,--- forAll, oneof, variant, sized, resize )--- import HyLo.Test ( UnitTest, runTest )--- import Control.Monad ( liftM )- import Data.IntMap ( IntMap ) import qualified Data.IntMap as IM @@ -20,10 +15,7 @@ {- a DMap , or double map, is a nesting of two Maps -} -data DMap c = DMap (IntMap (IntMap c))--instance (Show c) => Show (DMap c) where- show (DMap m) = show m+newtype DMap c = DMap (IntMap (IntMap c)) toMap :: DMap c -> IntMap (IntMap c) toMap (DMap m) = m
src/HTab/Formula.hs view
@@ -44,9 +44,8 @@ import qualified HyLo.InputFile as InputFile import qualified HyLo.InputFile.Parser as P-import HTab.Base (set, list, invertMap) import qualified HyLo.Formula as F-import HTab.CommandLine ( CmdLineParams(..) )+import HTab.CommandLine ( Params(..) ) type Prefix = Int @@ -167,13 +166,13 @@ showRelInfo :: RelInfo -> String showRelInfo = Map.foldWithKey (\r v -> (++ " " ++ showRel r ++ " -> " ++ show v )) "" -parse :: CmdLineParams -> String -> (Theory,RelInfo,Encoding,[Task])-parse clp s+parse :: Params -> String -> (Theory,RelInfo,Encoding,[Task])+parse p s = (theory, relInfo, encoding, tasks) where parseOutput = InputFile.myparse s -- direct parse from hylolib encoding = getEncoding parseOutput pRelInfo = P.relations parseOutput- relInfo = handleFunInj $ saturate $ forceProperties clp encoding $ convertToOurType pRelInfo encoding -- TODO+ relInfo = handleFunInj $ saturate $ forceProperties p encoding $ convertToOurType pRelInfo encoding -- TODO theory = convert relInfo encoding $ P.theory parseOutput tasks = P.tasks parseOutput @@ -207,6 +206,8 @@ Nothing -> error $ show e ++ " rel symbol " ++ show i Just x -> if isForward i then S.RelSymbol x else S.InvRelSymbol x +invertMap :: (Ord a, Ord b) => Map.Map a b -> Map.Map b a+invertMap = Map.fromList . map (\(a,b) -> (b,a)) . Map.assocs getEncoding :: P.ParseOutput -> Encoding getEncoding parseOutput =@@ -228,17 +229,17 @@ -- in order to work in case of automatic signature, requires -- the list of RelSymbol present in the formula -forceProperties :: CmdLineParams -> Encoding -> RelInfo -> RelInfo-forceProperties clp encoding relI+forceProperties :: Params -> Encoding -> RelInfo -> RelInfo+forceProperties p encoding relI = foldr addToAll relI rels where rels = Map.elems $ relMap encoding addToAll r = Map.insertWith (\c1 c2 -> nub $ c1 ++ c2) r conds conds = map snd $- filter fst $ [(allTransitive clp, Transitive),- (allReflexive clp, Reflexive ),- (allSymmetric clp, Symmetric ),- (allFunctional clp, Functional),- (allInjective clp, Injective )]+ filter fst $ [(allTransitive p, Transitive),+ (allReflexive p, Reflexive ),+ (allSymmetric p, Symmetric ),+ (allFunctional p, Functional),+ (allInjective p, Injective )] convertToOurType :: PRelInfo -> Encoding -> RelInfo -- and add for each relation in the formula, the relevant key convertToOurType prelI e = foldr insertRelProp Map.empty (concatMap convertOne prelI)@@ -256,8 +257,8 @@ c r (P.Equals ss) = [(int e r,SubsetOf [ int e s | s <- ss])] ++ [(int e s,SubsetOf [int e r]) | s <- ss] c _ (P.TClosureOf _) = error "TClosureOf not handled" -simpleParse :: CmdLineParams -> String -> (Theory,RelInfo,Encoding,[Task])-simpleParse clp s = parse clp $ "signature { automatic } theory { " ++ removeBeginEnd s ++ "}"+simpleParse :: Params -> String -> (Theory,RelInfo,Encoding,[Task])+simpleParse p s = parse p $ "signature { automatic } theory { " ++ removeBeginEnd s ++ "}" where removeBeginEnd = unwords . delete "begin" . delete "end" . words convert :: RelInfo -> Encoding -> [F.Formula S.NomSymbol S.PropSymbol S.RelSymbol] -> Formula@@ -607,20 +608,15 @@ data LanguageInfo = LanguageInfo { languageNoms :: [Int], -- ascending list relevantNoms :: [Int],- languageUniv :: Bool, languagePast :: Bool,- languageDiff :: Bool,- languageTrans :: Bool,- languageDown :: Bool }+ languageTrans :: Bool } instance Show LanguageInfo where show li = "Input Language:" ++ "\n|" ++ yesnol "Noms" ( languageNoms li ) ++ "\n|" ++ yesnol "Relevant Noms" ( relevantNoms li ) ++ "\n"- ++ yesno "Univ, " ( languageUniv li ) ++ yesno "Past, " ( languagePast li ) ++ yesno "Trans, " ( languageTrans li)- ++ yesno "Down." ( languageDown li ) where yesno :: String -> Bool -> String yesno s b = ( if b then "" else "no " ) ++ s yesnol s l | null l = "no " ++ s@@ -630,11 +626,8 @@ formulaLanguageInfo f e = LanguageInfo { languageNoms = noms, relevantNoms = relNoms,- languageUniv = hasUnivModality f, languagePast = hasPast f,- languageDiff = hasDiffModality f,- languageTrans = hasTransClosure f,- languageDown = hasDownArrow f }+ languageTrans = hasTransClosure f} where allNoms_ = nomsOfEncoding e relNoms_ = extractRelevantNominals f@@ -686,10 +679,6 @@ extractRelevantNominals (At _ f) = extractRelevantNominals f extractRelevantNominals f = composeFold Set.empty Set.union extractRelevantNominals f -hasUnivModality :: Formula -> Bool-hasUnivModality (A _) = True-hasUnivModality f = composeFold False (||) hasUnivModality f- hasPast :: Formula -> Bool hasPast (Dia r _) = testBit r 0 hasPast (Box r _) = testBit r 0@@ -697,19 +686,11 @@ hasPast (DiaX _ r _) = testBit r 0 hasPast f = composeFold False (||) hasPast f -hasDiffModality :: Formula -> Bool-hasDiffModality (B _) = True-hasDiffModality f = composeFold False (||) hasDiffModality f- hasTransClosure :: Formula -> Bool hasTransClosure (BoxX _ _) = True hasTransClosure (DiaX _ _ _) = True hasTransClosure f = composeFold False (||) hasTransClosure f -hasDownArrow :: Formula -> Bool-hasDownArrow (Down _ _ ) = True-hasDownArrow f = composeFold False (||) hasDownArrow f- replaceVar :: Int -> Int -> Formula -> Formula replaceVar v n a@(Lit v2) | isNominal v2 = if atom v /= atom v2 then a@@ -768,3 +749,9 @@ addDeps :: DependencySet -> PrFormula -> PrFormula addDeps ds1 (PrFormula p ds2 f) = PrFormula p (dsUnion ds1 ds2) f++list :: Ord a => Set.Set a -> [a]+list = Set.toList++set :: Ord a => [a] -> Set.Set a+set = Set.fromList
src/HTab/Main.hs view
@@ -6,7 +6,6 @@ import Control.Applicative ( (<$>) ) import Control.Monad ( when ) import Control.Monad.State( runStateT )-import Control.Monad.Reader( runReaderT ) import System.Console.CmdArgs ( whenNormal, whenLoud ) @@ -18,22 +17,20 @@ import HyLo.InputFile.Parser ( QueryType(..) ) -import HTab.CommandLine( filename, timeout, CmdLineParams, genModel, backjumping,- showFormula )-import HTab.Branch( BranchInfo(..),initialBranchStateFor, BranchData(..),- emptyBranch, addFirstFormulas)+import HTab.CommandLine( filename, timeout, Params, genModel, dotModel, showFormula )+import HTab.Branch( BranchInfo(..), emptyBranch, addFirstFormulas) import HTab.Statistics( Statistics, initialStatisticsStateFor, printOutMetricsFinal ) import HTab.Tableau( OpenFlag(..), tableauStart )-import HTab.Formula( formulaLanguageInfo, languageTrans, Theory, RelInfo, Encoding, Task,+import HTab.Formula( formulaLanguageInfo, Theory, RelInfo, Encoding, Task, Formula, encodeValidityTest, encodeSatTest, encodeRetrieveTask, toNomSymbol, showRelInfo ) import qualified HTab.Formula as F-import HTab.ModelGen ( Model )+import HTab.ModelGen ( Model, toDot ) data TaskRunFlag = SUCCESS | FAILURE -runWithParams :: CmdLineParams -> IO (Maybe TaskRunFlag)-runWithParams clp =+runWithParams :: Params -> IO (Maybe TaskRunFlag)+runWithParams p = time "Total time: " $ do let fromStdIn = do myPutStrLn $ "Reading from stdin (run again with" ++@@ -42,13 +39,13 @@ getContents let parse = \i -> if head (words i) == "begin"- then F.simpleParse clp i else F.parse clp i- allTasks <- parse <$> maybe fromStdIn readFile (filename clp)+ then F.simpleParse p i else F.parse p i+ allTasks <- parse <$> maybe fromStdIn readFile (filename p) --- result <- if timeout clp == 0- then Just <$> runTasks allTasks clp- else T.timeout (timeout clp * (10::Int)^(6::Int))- (runTasks allTasks clp)+ result <- if timeout p == 0+ then Just <$> runTasks allTasks p+ else T.timeout (timeout p * (10::Int)^(6::Int))+ (runTasks allTasks p) -- case result of Nothing -> myPutStrLn "\nTimeout.\n"@@ -59,35 +56,35 @@ -- -runTasks :: (Theory,RelInfo,Encoding,[Task]) -> CmdLineParams -> IO TaskRunFlag-runTasks allTasks@(theory,relInfo,encoding,tasks) clp =+runTasks :: (Theory,RelInfo,Encoding,[Task]) -> Params -> IO TaskRunFlag+runTasks allTasks@(theory,relInfo,encoding,tasks) p = do myPutStrLn "== Checking theory satisfiability =="- res <- runOneTask (Satisfiable, genModel clp,[]) relInfo encoding theory clp+ res <- runOneTask (Satisfiable, genModel p,[]) relInfo encoding theory p case res of SUCCESS | null tasks -> return SUCCESS | otherwise -> do myPutStrLn "\n== Starting tasks =="- res2 <- runTasks2 allTasks clp+ res2 <- runTasks2 allTasks p myPutStrLn "\n== End of tasks ==" return res2 FAILURE -> return FAILURE -- -runTasks2 :: (Theory,RelInfo,Encoding,[Task]) -> CmdLineParams -> IO TaskRunFlag+runTasks2 :: (Theory,RelInfo,Encoding,[Task]) -> Params -> IO TaskRunFlag runTasks2 (_,_,_,[]) _ = error "runTasks2 empty list error"-runTasks2 (theory,relInfo,encoding,(hd:tl)) clp =- do res <- runOneTask hd relInfo encoding theory clp+runTasks2 (theory,relInfo,encoding,(hd:tl)) p =+ do res <- runOneTask hd relInfo encoding theory p case res of SUCCESS | null tl -> return SUCCESS- | otherwise -> runTasks2 (theory,relInfo,encoding,tl) clp- FAILURE -> do _ <- runTasks2 (theory,relInfo,encoding,tl) clp+ | otherwise -> runTasks2 (theory,relInfo,encoding,tl) p+ FAILURE -> do _ <- runTasks2 (theory,relInfo,encoding,tl) p return FAILURE -- -runOneTask :: Task -> RelInfo -> Encoding -> Formula -> CmdLineParams -> IO TaskRunFlag-runOneTask (query,mOutFile,fs) relInfo encoding theory clp =+runOneTask :: Task -> RelInfo -> Encoding -> Formula -> Params -> IO TaskRunFlag+runOneTask (query,mOutFile,fs) relInfo encoding theory p = time "Task time:" $ do myPutStrLn $ "\n* " ++ case query of {Valid -> "Validity task";@@ -99,12 +96,12 @@ Retrieve -> do let fLang = formulaLanguageInfo theory encoding- let initialBranch = emptyBranch clp fLang relInfo encoding+ let initialBranch = emptyBranch fLang relInfo encoding let (noms,encfs) = encodeRetrieveTask relInfo encoding fLang theory fs -- myPutStrLn $ "Instances making true: " ++ show fs --- results <- mapM (tableauInit clp . addFirstFormulas clp initialBranch fLang) encfs+ results <- mapM (tableauInit p . addFirstFormulas p initialBranch fLang) encfs let goodnoms = [ toNomSymbol encoding n | (n,(CLOSED _ ,_)) <- zip noms results] myPutStrLn $ show goodnoms let doWrite f = do writeFile f (show goodnoms ++ "\n")@@ -119,7 +116,7 @@ Satisfiable -> encodeSatTest relInfo encoding theory fs _ -> error "never happens" --- when (showFormula clp)+ when (showFormula p) $ myPutStrLn $ unlines ["Input for SAT test:", "{ " ++ show f ++ " }",@@ -127,11 +124,10 @@ "Relations properties :" ++ showRelInfo relInfo ] -- let fLang = formulaLanguageInfo f encoding- let initialBranch = emptyBranch clp fLang relInfo encoding- let branchInfo = addFirstFormulas clp initialBranch fLang f- let clp2 = if languageTrans fLang then clp{backjumping=False} else clp+ let initialBranch = emptyBranch fLang relInfo encoding+ let branchInfo = addFirstFormulas p initialBranch fLang f --- result <- tableauInit clp2 branchInfo+ result <- tableauInit p branchInfo -- case result of (OPEN m, stats) -> do myPutStrLn $@@ -139,7 +135,7 @@ Valid -> "The formula is not valid." Satisfiable -> "The formula is satisfiable." _ -> error "never happens"- saveGenModel mOutFile m+ saveGenModel mOutFile p m whenNormal $ printOutMetricsFinal stats return SUCCESS (CLOSED _, stats) -> do myPutStrLn $@@ -159,18 +155,18 @@ -- -saveGenModel :: Maybe FilePath -> Model -> IO ()-saveGenModel mOutFile m = maybe (return ()) doWrite mOutFile- where doWrite f = do writeFile f (show m)+saveGenModel :: Maybe FilePath -> Params -> Model -> IO ()+saveGenModel mOutFile p m = maybe (return ()) doWrite mOutFile+ where doWrite f = do writeFile f output myPutStrLn ("Model saved as " ++ f)+ output | dotModel p = toDot m+ | otherwise = show m -tableauInit :: CmdLineParams -> BranchInfo -> IO (OpenFlag,Statistics)-tableauInit clp bi =+tableauInit :: Params -> BranchInfo -> IO (OpenFlag,Statistics)+tableauInit p bi = do whenLoud $ putStrLn ">> Starting rules application"- initStatsState $ initBranchState bd $ tableauStart clp bi+ initStatsState $ tableauStart p bi where initStatsState = initialStatisticsStateFor runStateT- initBranchState = initialBranchStateFor runReaderT- bd = BranchData { branch_clp = clp } --
src/HTab/ModelGen.hs view
@@ -1,4 +1,4 @@-module HTab.ModelGen (Model, buildModel )+module HTab.ModelGen (Model, buildModel, toDot ) where @@ -6,6 +6,7 @@ import Data.Set (Set) import qualified Data.IntMap as IntMap import HyLo.Model.Herbrand ( inducedModel )+import HyLo.Model.PrettyPrint ( toDotStr ) import qualified HyLo.Model.Herbrand as H import qualified HyLo.Model as M @@ -91,3 +92,6 @@ = Set.union (succs_ r_ w_) syms where syms = Set.filter (hasAsSuccessor r_ w_) worlds hasAsSuccessor rel world2 world1 = Set.member world2 $ succs_ rel world1++toDot :: Model -> String+toDot = toDotStr
src/HTab/RuleId.hs view
@@ -45,7 +45,13 @@ | R_Exist -- Existential modality | R_Diff -- Difference modality | R_Discard -- Discarding a formula- | R_Clash -- Branch clash+ | R_DiscardDown+ | R_DiscardDiaDone+ | R_DiscardDiaDone2+ | R_DiscardDiaBlocked+ | R_DiscardDiaX+ | R_DiscardDisjTrivial+ | R_ClashDisj -- Branch clash | R_UBlocking -- Unrestricted Blocking | R_Merge -- Equivalence classes merge | R_RoleInc -- Role inclusion
src/HTab/Rules.hs view
@@ -25,9 +25,9 @@ getUrfatherAndDeps, isNotBlocked, merge, diaAlreadyDone, diaXAlreadyDone, downAlreadyDone, ReducedDisjunct(..), getUrfather,- ScheduledRule(..), TodoList(..),+ TodoList(..), deleteUEV, insertUEV_addFormula )-import HTab.CommandLine(CmdLineParams, UnitProp(..), lazyBranching, semBranch, unitProp, strategy, noLoopCheck)+import HTab.CommandLine(Params, UnitProp(..), lazyBranching, semBranch, unitProp, strategy, noLoopCheck) import HTab.RuleId(RuleId(..)) import qualified HTab.DisjSet as DS @@ -59,8 +59,13 @@ | DownRule PrFormula | DiffRule PrFormula Dependency | ExistRule PrFormula -- creates a prefix- | DiscardRule PrFormula- | ClashRule DependencySet PrFormula+ | DiscardDownRule PrFormula+ | DiscardDiaDoneRule PrFormula+ | DiscardDiaDone2Rule PrFormula+ | DiscardDiaBlockedRule PrFormula+ | DiscardDiaXRule PrFormula+ | DiscardDisjTrivialRule PrFormula+ | ClashDisjRule DependencySet PrFormula | MergeRule Prefix DS.Pointer DependencySet | RoleIncRule Prefix [Rel] Prefix DependencySet @@ -68,14 +73,14 @@ -- for certain rules, we need to look in the branch to see what modifications we do getMods :: Branch -> Rule -> [[BranchModification]]-getMods _ (ClashRule ds f) = [[BM_Clash ds f]]+getMods _ (ClashDisjRule ds f) = [[BM_Clash ds f]] getMods _ (MergeRule p n ds)= [[BM_Merge p n ds]] getMods _ (RoleIncRule p1 rs p2 ds) = [[BM_AddAccFormula (AccFormula ds r p1 p2)] | r <- rs] getMods br (DiaRule df@(PrFormula pr ds (Dia r f))) = if diaAlreadyDone br df- then getMods br (DiscardRule df)+ then getMods br (DiscardDiaDone2Rule df) else [[BM_AddParentPrefix newPr ur, BM_AddAccFormula acctoadd, BM_AddFormulas [toadd],@@ -130,7 +135,7 @@ getMods br (DownRule df@(PrFormula pr ds f@(Down v f2))) = if downAlreadyDone br df- then getMods br (DiscardRule df)+ then getMods br (DiscardDownRule df) else [[BM_CreateNewNomTestRelevance f, -- order -- what about using a monadic BM_AddFormulas [toadd1, toadd2], -- matters -- writing for the getMods functions ? BM_AddDownRuleCheck pr f@@ -169,23 +174,33 @@ getMods _ (DiffRule _ _) = error "getMods DiffRule" +getMods _ (DiscardDownRule _) = [[]]+getMods _ (DiscardDiaDoneRule _) = [[]]+getMods _ (DiscardDiaDone2Rule _) = [[]]+getMods _ (DiscardDiaBlockedRule _) = [[]]+getMods _ (DiscardDiaXRule _) = [[]]+getMods _ (DiscardDisjTrivialRule _) = [[]] -getMods _ (DiscardRule _) = [[]]+instance Show Rule where+ show (MergeRule pr po _) = "merge: " ++ show (pr,po)+ show (DiaRule todelete) = "diamond: " ++ showLess todelete+ show (DiaXRule todelete _) = "diamondX: " ++ showLess todelete+ show (DisjRule todelete _ ) = "disjunction: " ++ showLess todelete+ show (SemBrRule todelete _ ) = "semantic branching: " ++ showLess todelete+ show (AtRule todelete ) = "at: " ++ showLess todelete+ show (DownRule todelete ) = "down: " ++ showLess todelete+ show (ExistRule todelete ) = "E: " ++ showLess todelete+ show (DiffRule todelete _) = "D: " ++ showLess todelete + show (DiscardDownRule todelete) = "Discard: " ++ showLess todelete+ show (DiscardDiaDoneRule todelete) = "Discard done: " ++ showLess todelete+ show (DiscardDiaDone2Rule todelete) = "Discard done 2: " ++ showLess todelete+ show (DiscardDiaBlockedRule todelete) = "Discard blocked: " ++ showLess todelete+ show (DiscardDiaXRule todelete) = "Discard: " ++ showLess todelete+ show (DiscardDisjTrivialRule todelete) = "Discard trivial: " ++ showLess todelete -instance Show Rule where- show (MergeRule pr po _) = "merge: " ++ show (pr,po)- show (DiaRule todelete) = "diamond: " ++ showLess todelete- show (DiaXRule todelete _) = "diamondX: " ++ showLess todelete- show (DisjRule todelete _ ) = "disjunction: " ++ showLess todelete- show (SemBrRule todelete _ ) = "semantic branching: " ++ showLess todelete- show (AtRule todelete ) = "at: " ++ showLess todelete- show (DownRule todelete ) = "down: " ++ showLess todelete- show (ExistRule todelete ) = "E: " ++ showLess todelete- show (DiffRule todelete _) = "D: " ++ showLess todelete- show (DiscardRule todelete) = "Discard: " ++ showLess todelete- show (ClashRule bprs f) = "Clash: " ++ show bprs ++ " " ++ show f+ show (ClashDisjRule bprs f) = "Clash: " ++ show bprs ++ " " ++ show f show (RoleIncRule p1 rs p2 _) = "Role inclusion " ++ show (p1,rs,p2) show (LazyBranchRule todelete _ _ _) = "Lazy Branch " ++ showLess todelete@@ -202,36 +217,23 @@ (DownRule _) -> R_Down (ExistRule _) -> R_Exist (DiffRule _ _) -> R_Diff- (DiscardRule _) -> R_Discard- (ClashRule _ _) -> R_Clash- (RoleIncRule _ _ _ _) -> R_RoleInc+ (DiscardDownRule _) -> R_DiscardDown+ (DiscardDiaDoneRule _) -> R_DiscardDiaDone+ (DiscardDiaDone2Rule _) -> R_DiscardDiaDone2+ (DiscardDiaBlockedRule _) -> R_DiscardDiaBlocked+ (DiscardDiaXRule _) -> R_DiscardDiaX+ (DiscardDisjTrivialRule _) -> R_DiscardDisjTrivial+ (ClashDisjRule _ _) -> R_ClashDisj+ (RoleIncRule _ _ _ _) -> R_RoleInc (LazyBranchRule _ _ _ _) -> R_LazyBranch -- the rules application strategy is defined here: -- the first rule is the one that will be applied at the next tableau step-applicableRule :: Branch -> CmdLineParams -> Dependency -> Maybe (Rule,TodoList,Branch)-applicableRule br clp d =- case todoList br of- Fair [] -> Nothing- Fair (sr:tl) -> Just (scheduledRuleToRule br clp d sr, Fair tl, br)- _ -> listToMaybe $ mapMaybe (ruleByChar br clp d) (strategy clp)--scheduledRuleToRule :: Branch -> CmdLineParams -> Dependency -> ScheduledRule -> Rule-scheduledRuleToRule _ _ d (SR_Inclusion p1 rs p2 ds) = RoleIncRule p1 rs p2 (dsInsert d ds)-scheduledRuleToRule _ _ _ (SR_Merge pr po ds) = MergeRule pr po ds-scheduledRuleToRule br clp d (SR_Formula pf@(PrFormula _ _ f2)) =- case f2 of- Dis _ -> if semBranch clp then semBrRule clp pf br d else disjRule clp pf br d- Dia _ _ -> DiaRule pf- DiaX _ _ _-> diaXRule pf br d- At _ _ -> AtRule pf- Down _ _ -> DownRule pf- E _ -> ExistRule pf- D _ -> DiffRule pf d- _ -> error "scheduledRuleToRule, incorrect formula kind"+applicableRule :: Branch -> Params -> Dependency -> Maybe (Rule,TodoList,Branch)+applicableRule br p d = listToMaybe $ mapMaybe (ruleByChar br p d) (strategy p) -ruleByChar :: Branch -> CmdLineParams -> Dependency -> Char -> Maybe (Rule,TodoList,Branch)-ruleByChar br clp d char =+ruleByChar :: Branch -> Params -> Dependency -> Char -> Maybe (Rule,TodoList,Branch)+ruleByChar br p d char = case char of 'n' -> applicableMergeRule '|' -> applicableDisjRule@@ -248,10 +250,10 @@ applicableDiaRule = do (f@(PrFormula pr _ _),new) <- Set.minView $ diaTodo todos- if noLoopCheck clp+ if noLoopCheck p then return (DiaRule f, todos{diaTodo = new},br) else if diaAlreadyDone br f- then return (DiscardRule f, todos{diaTodo = new} , br )+ then return (DiscardDiaDoneRule f, todos{diaTodo = new} , br ) else if isNotBlocked br pr then return ( DiaRule f, todos{diaTodo = new}, br ) else let ur = getUrfather br (DS.Prefix pr)@@ -261,7 +263,7 @@ -- to that list, but as we do not index todo formulas by prefix we can -- not do it. in- return ( DiscardRule f, todos{diaTodo = new}, brBlocked)+ return ( DiscardDiaBlockedRule f, todos{diaTodo = new}, brBlocked) applicableDiaXRule = do (f,new) <- Set.minView $ diaXTodo todos return (diaXRule f br d, todos{diaXTodo = new},br)@@ -281,32 +283,32 @@ applicableRoleIncRule = do ((ds, p1, p2, rs),new) <- Set.minView $ roleIncTodo todos return (RoleIncRule p1 rs p2 (dsInsert d ds), todos{roleIncTodo = new},br) - applicableMergeRule = do ((ds,p,po),new) <- Set.minView $ mergeTodo todos- return (MergeRule p po ds, todos{mergeTodo = new},br)+ applicableMergeRule = do ((ds,pr,po),new) <- Set.minView $ mergeTodo todos+ return (MergeRule pr po ds, todos{mergeTodo = new},br) applicableDisjRule- = case unitProp clp of+ = case unitProp p of Eager -> {- scan all disjuncts until one can be discarded, reduced to one disjunct or clashes -}- case mapMaybe (makeInteresting clp br d) $ Set.toList $ disjTodo todos of+ case mapMaybe (makeInteresting p br d) $ Set.toList $ disjTodo todos of ((r,pf):_) -> return (r, todos{disjTodo = Set.delete pf $ disjTodo todos},br) [] -> regularApplicableDisjRule --todo: update counter (CurCount, MaxCount) step 10 until which space out unit propagation _ -> regularApplicableDisjRule regularApplicableDisjRule- = if semBranch clp+ = if semBranch p then do (f,new) <- Set.minView $ disjTodo todos- return (semBrRule clp f br d, todos{disjTodo = new},br)+ return (semBrRule p f br d, todos{disjTodo = new},br) else do (f,new) <- Set.minView $ disjTodo todos- return (disjRule clp f br d, todos{disjTodo = new},br)+ return (disjRule p f br d, todos{disjTodo = new},br) -makeInteresting :: CmdLineParams -> Branch -> Dependency -> PrFormula -> Maybe (Rule,PrFormula)-makeInteresting clp br d df@(PrFormula pr ds (Dis fs))+makeInteresting :: Params -> Branch -> Dependency -> PrFormula -> Maybe (Rule,PrFormula)+makeInteresting p br d df@(PrFormula pr ds (Dis fs)) = case reduceDisjunctionProposeLazy br pr fs of- Triviality -> Just (DiscardRule df,df)- Contradiction ds_clash -> Just (ClashRule (dsUnion ds ds_clash) df,df)+ Triviality -> Just (DiscardDisjTrivialRule df,df)+ Contradiction ds_clash -> Just (ClashDisjRule (dsUnion ds ds_clash) df,df) Reduced new_ds disjuncts mProposed | Set.size disjuncts == 1 -> Just (DisjRule df ( prefix ur newDeps disjuncts ), df)- | lazyBranching clp && ur <= unblockedPrefsLim br+ | lazyBranching p && ur <= unblockedPrefsLim br -> case mProposed of Nothing -> Nothing Just lit -> Just (LazyBranchRule df ur lit [PrFormula ur newDeps (Dis disjuncts)], df)@@ -319,42 +321,42 @@ makeInteresting _ _ _ _ = error "makeInteresting on a non disjunction" -applyRule :: CmdLineParams -> Rule -> Branch -> TodoList -> [BranchInfo]-applyRule clp rule br_ todo- = map (applyMods clp br) (getMods br rule)+applyRule :: Params -> Rule -> Branch -> TodoList -> [BranchInfo]+applyRule p rule br_ todo+ = map (applyMods p br) (getMods br rule) where br = br_{todoList = todo} -applyMods :: CmdLineParams -> Branch -> [BranchModification] -> BranchInfo-applyMods clp br (hd:tl)- = case (applyMod clp br hd) of- BranchOK br2 -> applyMods clp br2 tl+applyMods :: Params -> Branch -> [BranchModification] -> BranchInfo+applyMods p br (hd:tl)+ = case (applyMod p br hd) of+ BranchOK br2 -> applyMods p br2 tl si@(BranchClash _ _ _ _) -> si applyMods _ br [] = BranchOK br -applyMod :: CmdLineParams -> Branch -> BranchModification -> BranchInfo-applyMod clp br (BM_AddFormulas li) = addFormulas clp br li-applyMod clp br (BM_AddAccFormula accFor) = addAccFormula clp br accFor-applyMod _ br (BM_AddDiaRuleCheck pr (r,f)) = BranchOK $ addDiaRuleCheck br pr (r,f)-applyMod _ br (BM_AddDiaXRuleCheck pr (r,f)) = BranchOK $ addDiaXRuleCheck br pr (r,f)-applyMod _ br (BM_AddDownRuleCheck pr f) = BranchOK $ addDownRuleCheck br pr f-applyMod clp br (BM_CreateNewPref) = createNewPref clp br-applyMod _ br (BM_CreateNewProp) = BranchOK $ createNewProp br-applyMod _ br (BM_CreateNewNomTestRelevance f) = BranchOK $ createNewNomTestRelevance br f-applyMod _ br (BM_AddDiffRuleCheck f mp) = BranchOK $ addDiffRuleCheck br f mp-applyMod _ br (BM_AddParentPrefix son father) = BranchOK $ addParentPrefix br son father-applyMod _ br (BM_Clash ds (PrFormula pr ds2 f)) = BranchClash br pr (dsUnion ds ds2) f-applyMod _ br (BM_DeleteUEV i) = BranchOK $ deleteUEV br i-applyMod clp br (BM_InsertUEV_addFormula mi ds ff) = insertUEV_addFormula br clp mi ds ff-applyMod clp br (BM_Merge pr p ds) = merge clp br pr ds p-applyMod _ br (BM_DoLazyBranch pr l pfs) = BranchOK $ doLazyBranching pr l pfs br+applyMod :: Params -> Branch -> BranchModification -> BranchInfo+applyMod p br (BM_AddFormulas li) = addFormulas p br li+applyMod p br (BM_AddAccFormula accFor) = addAccFormula p br accFor+applyMod _ br (BM_AddDiaRuleCheck pr (r,f)) = BranchOK $ addDiaRuleCheck br pr (r,f)+applyMod _ br (BM_AddDiaXRuleCheck pr (r,f)) = BranchOK $ addDiaXRuleCheck br pr (r,f)+applyMod _ br (BM_AddDownRuleCheck pr f) = BranchOK $ addDownRuleCheck br pr f+applyMod p br (BM_CreateNewPref) = createNewPref p br+applyMod _ br (BM_CreateNewProp) = BranchOK $ createNewProp br+applyMod _ br (BM_CreateNewNomTestRelevance f) = BranchOK $ createNewNomTestRelevance br f+applyMod _ br (BM_AddDiffRuleCheck f mp) = BranchOK $ addDiffRuleCheck br f mp+applyMod _ br (BM_AddParentPrefix son father) = BranchOK $ addParentPrefix br son father+applyMod _ br (BM_Clash ds (PrFormula pr ds2 f)) = BranchClash br pr (dsUnion ds ds2) f+applyMod _ br (BM_DeleteUEV i) = BranchOK $ deleteUEV br i+applyMod p br (BM_InsertUEV_addFormula mi ds ff) = insertUEV_addFormula br p mi ds ff+applyMod p br (BM_Merge pr po ds) = merge p br pr ds po+applyMod _ br (BM_DoLazyBranch pr l pfs) = BranchOK $ doLazyBranching pr l pfs br -- the actual rules and their helper functions -- diaX (may create a discard rule) diaXRule :: PrFormula -> Branch -> Dependency -> Rule diaXRule f@(PrFormula pr _ (DiaX _ r f2)) br d = if diaXAlreadyDone br pr (r,f2)- then DiscardRule f+ then DiscardDiaXRule f else DiaXRule f d diaXRule _ _ _ = error "diaXRule"@@ -365,26 +367,26 @@ getNewPref br = lastPref br + 1 -- disjunction-disjRule :: CmdLineParams -> PrFormula -> Branch -> Dependency -> Rule-disjRule clp df@(PrFormula pr ds (Dis fs)) br d- = if unitProp clp == UPNo+disjRule :: Params -> PrFormula -> Branch -> Dependency -> Rule+disjRule p df@(PrFormula pr ds (Dis fs)) br d+ = if unitProp p == UPNo then DisjRule df $ prefix pr (dsInsert d ds) fs else case reduceDisjunctionProposeLazy br pr fs of- Triviality -> DiscardRule df- Contradiction ds_clash -> ClashRule (dsUnion ds ds_clash) df+ Triviality -> DiscardDisjTrivialRule df+ Contradiction ds_clash -> ClashDisjRule (dsUnion ds ds_clash) df Reduced new_ds disjuncts _ -> DisjRule df (prefix pr (dsInsert d $ dsUnion ds new_ds) disjuncts) -- todo: if only one conjunct remaining, do not add d , but still create a DisjRule disjRule _ _ _ _ = error "disjRule" -- semantic branching-semBrRule :: CmdLineParams -> PrFormula -> Branch -> Dependency -> Rule -- todo : unit propagation, part 2 (b)-semBrRule clp df@(PrFormula pr ds (Dis fs)) br d- = if unitProp clp == UPNo+semBrRule :: Params -> PrFormula -> Branch -> Dependency -> Rule -- todo : unit propagation, part 2 (b)+semBrRule p df@(PrFormula pr ds (Dis fs)) br d+ = if unitProp p == UPNo then SemBrRule df $ sbModList $ prefix pr (dsInsert d ds) fs else case reduceDisjunctionProposeLazy br pr fs of- Triviality -> DiscardRule df- Contradiction ds_clash -> ClashRule (dsUnion ds ds_clash) df+ Triviality -> DiscardDisjTrivialRule df+ Contradiction ds_clash -> ClashDisjRule (dsUnion ds ds_clash) df Reduced new_ds disjuncts _ -> SemBrRule df (sbModList $ prefix pr (dsInsert d $ dsUnion ds new_ds) disjuncts) -- todo same remark as above
src/HTab/Tableau.hs view
@@ -4,92 +4,55 @@ import System.Console.CmdArgs ( whenLoud ) -import Control.Monad.Reader(ask) import Control.Monad.State(StateT,lift,modify)-import HTab.Statistics(updateStep,printOutMetrics,- recordClosedBranch, recordFiredRule, Statistics)-import HTab.Branch(BranchInfo(..),Branch(..),BranchMonad, BranchData(..),- unfulfilledEventualities)-import HTab.CommandLine(backjumping,CmdLineParams,configureStats)-import HTab.Rules(Rule,applyRule,applicableRule,ruleToId)-import HTab.Formula(Prefix,DependencySet,Formula,dsEmpty,dsMember,dsUnion)+import HTab.Statistics(Statistics,updateStep,printOutMetrics,recordClosedBranch, recordFiredRule)+import HTab.Branch(BranchInfo(..), unfulfilledEventualities)+import HTab.CommandLine(backjumping,Params,configureStats)+import HTab.Rules(applyRule,applicableRule,ruleToId)+import HTab.Formula(DependencySet,dsEmpty,dsMember,dsUnion) import HTab.ModelGen ( Model, buildModel ) type Depth = Int data OpenFlag = OPEN Model | CLOSED DependencySet+type TableauMonad a = StateT Statistics IO a -tableauStart :: CmdLineParams -> BranchInfo -> BranchMonad OpenFlag-tableauStart clp bi = liftStats (configureStats clp) >> tableau 0 bi+tableauStart :: Params -> BranchInfo -> TableauMonad OpenFlag+tableauStart p bi = configureStats p >> tableauDown p 0 bi -tableau :: Depth -> BranchInfo -> BranchMonad OpenFlag-tableau depth branchInfo =- do logMe- bd <- ask- debugMsg_NewSection depth+tableauDown :: Params -> Depth -> BranchInfo -> TableauMonad OpenFlag+tableauDown p depth branchInfo =+ do let verbose = lift . whenLoud . putStrLn+ printOutMetrics+ modify updateStep+ verbose (">> Depth " ++ show depth) case branchInfo of BranchClash br pr bprs f ->- do debugMsg_BranchClash br pr bprs f depth- liftStats recordClosedBranch- return (CLOSED bprs)+ do verbose (show br ++ "Clasher : " ++ show (pr,bprs,depth,f))+ recordClosedBranch+ return $ CLOSED bprs BranchOK br ->- do debugMsg_BranchOK br- let clp = branch_clp bd- case applicableRule br clp (depth + 1) of+ do verbose (show br)+ case applicableRule br p (depth + 1) of Nothing ->- do debugMsg_BranchOK_saturated+ do verbose (">> Saturated open branch") return $ case unfulfilledEventualities br of Just ds -> CLOSED ds Nothing -> OPEN $ buildModel br Just (rule,newTodo,newBranch) -> -- of course then merge newBranch and newTodo- do debugMsg_BranchOK_applicableRule rule- liftStats $ recordFiredRule $ ruleToId rule- case applyRule clp rule newBranch newTodo of- [newBi] -> tableau (depth + 1) newBi- bis -> chooseBranch dsEmpty bis (depth + 1)-+ do verbose (">> Rule : " ++ show rule)+ recordFiredRule $ ruleToId rule+ case applyRule p rule newBranch newTodo of+ [newBi] -> tableauDown p (depth + 1) newBi+ bis -> tableauRight p (depth + 1) bis dsEmpty -chooseBranch :: DependencySet -> [BranchInfo] -> Depth -> BranchMonad OpenFlag-chooseBranch currentDepSet (hd:tl) depth =- do res <- tableau depth hd+tableauRight :: Params -> Depth -> [BranchInfo] -> DependencySet -> TableauMonad OpenFlag+tableauRight p depth (hd:tl) currentDepSet =+ do res <- tableauDown p depth hd case res of o@(OPEN _) -> return o CLOSED depSet ->- do bd <- ask- if (backjumping $ branch_clp bd) && (not $ dsMember depth depSet)+ if backjumping p && not (dsMember depth depSet) then return $ CLOSED depSet- else chooseBranch (dsUnion currentDepSet depSet) tl depth--chooseBranch currentDepSet [] _ = return $ CLOSED currentDepSet------logMe :: BranchMonad ()-logMe = do liftStats printOutMetrics- liftStats $ modify updateStep--debugMsg_NewSection :: Depth -> BranchMonad ()-debugMsg_NewSection depth- = liftIO $ whenLoud $ putStrLn ("\n>> Depth " ++ show depth)--debugMsg_BranchClash :: Branch -> Prefix -> DependencySet -> Formula -> Depth -> BranchMonad ()-debugMsg_BranchClash br pr bprs f depth- = liftIO $ whenLoud $ putStrLn (show br ++ "\nClasher : " ++ show (pr,bprs,depth,f))--debugMsg_BranchOK :: Branch -> BranchMonad ()-debugMsg_BranchOK br- = liftIO $ whenLoud $ putStrLn (show br)--debugMsg_BranchOK_applicableRule :: Rule -> BranchMonad ()-debugMsg_BranchOK_applicableRule rule- = liftIO $ whenLoud $ putStrLn ("\n>> Rule : " ++ show rule)--debugMsg_BranchOK_saturated :: BranchMonad ()-debugMsg_BranchOK_saturated- = liftIO $ whenLoud $ putStrLn ("\n>> Saturated open branch")--liftStats :: StateT Statistics IO a -> BranchMonad a-liftStats = lift--liftIO :: IO a -> BranchMonad a-liftIO = lift . lift+ else tableauRight p depth tl (dsUnion currentDepSet depSet) +tableauRight _ _ [] currentDepSet = return $ CLOSED currentDepSet
src/htab.hs view
@@ -47,8 +47,8 @@ else return Nothing header :: String-header = unlines ["HTab 1.5.4",- "G. Hoffmann, C. Areces, D.Gorin and J. Heguiabehere. (c) 2002-2010.",+header = unlines ["HTab 1.5.5",+ "G. Hoffmann, C. Areces, D.Gorin and J. Heguiabehere. (c) 2002-2011.", "http://code.google.com/p/intohylo/"] gpl_tag :: [String]
tests/coverage.sh view
@@ -11,7 +11,6 @@ for i in $DATA/*; do $HTAB --showformula -f $i- $HTAB -t 2 --fairstrategy -u -f $i $HTAB -v --stats=10 -f $i $HTAB -t 2 -f $i $HTAB -t 2 --lazybranching=False -f $i@@ -30,7 +29,6 @@ for i in $DATA/*; do $HTAB --showformula -f $i- $HTAB -t 2 --fairstrategy -u -f $i $HTAB -v --stats=10 -f $i $HTAB -t 2 -f $i $HTAB -t 2 --lazybranching=False -f $i@@ -49,7 +47,6 @@ for i in $DATA/*; do $HTAB --showformula -f $i- $HTAB -t 2 --fairstrategy -u -f $i $HTAB -v --stats=10 -f $i $HTAB -t 2 -f $i $HTAB -t 2 --lazybranching=False -f $i