HTab 1.5.6 → 1.6.0
raw patch · 20 files changed
+495/−969 lines, 20 filesdep −directorydep −filepathdep ~cmdargssetup-changed
Dependencies removed: directory, filepath
Dependency ranges changed: cmdargs
Files
- HTab.cabal +2/−4
- NEWS +7/−0
- Setup.hs +2/−0
- Setup.lhs +0/−4
- examples/unsat/fun_inj1.frm +0/−13
- examples/unsat/fun_inj2.frm +0/−14
- examples/unsat/symmetry1.frm +3/−3
- examples/unsat/test39.frm +0/−15
- examples/unsat/test40.frm +0/−14
- src/HTab/Branch.hs +235/−318
- src/HTab/CommandLine.hs +45/−52
- src/HTab/Formula.hs +32/−221
- src/HTab/Main.hs +5/−6
- src/HTab/ModelGen.hs +21/−7
- src/HTab/Relations.hs +3/−4
- src/HTab/RuleId.hs +0/−1
- src/HTab/Rules.hs +127/−270
- src/HTab/Statistics.hs +1/−9
- src/HTab/Tableau.hs +8/−10
- src/htab.hs +4/−4
HTab.cabal view
@@ -1,5 +1,5 @@ Name: HTab-Version: 1.5.6+Version: 1.6.0 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@@ -42,11 +42,9 @@ Build-Depends: base >= 4, base < 5, mtl >= 2, mtl < 3, containers < 1,- filepath > 1, filepath <= 2,- directory > 1, directory <= 2, deepseq >= 1, deepseq <2, strict < 1,- cmdargs >= 0.6, cmdargs < 0.7,+ cmdargs >= 0.9, cmdargs < 1.0, hylolib >= 1.3.2, hylolib < 1.4 Extensions: GADTs DeriveDataTypeable
NEWS view
@@ -1,3 +1,10 @@+* 2011.12.02 : 1.6.0+ o pattern based blocking by default+ o lazy branching on all nodes except with chain blocking+ o cumulative model building with pattern or inclusion blocking+ o remove support for transitive closure modalities+ o remove support for injective and functional modalities+ o remove noloopcheck flag * 2010.09.27 : 1.5.4 o lazy branching by default o fix memory leak
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
− Setup.lhs
@@ -1,4 +0,0 @@-#! /usr/bin/env runhaskell--> import Distribution.Simple-> main = defaultMain
− examples/unsat/fun_inj1.frm
@@ -1,13 +0,0 @@-signature {-propositions { p }-nominals { n,m }-relations { r : { functional } }-}--theory--{- n:<r><r><r><r><r>p;- m:<r><r><r><r><r>!p;- n:m-}
− examples/unsat/fun_inj2.frm
@@ -1,14 +0,0 @@-signature {-propositions { p }-nominals { n,a,b }-relations { r,- s : { inverseof r, functional } }-}--theory--{- a:<r><r><r><r><r><r><r><r><r><r><r>n;- b:<r><r><r><r><r><r><r><r><r><r><r>n;- a:!b-}
examples/unsat/symmetry1.frm view
@@ -1,14 +1,14 @@ signature { propositions { p } nominals { n,m }-relations { s : {symmetric}, t : {trclosureof s} }+relations { s : {symmetric} } } theory {- n:<s><s><s><s>m;+ n:<s><s><s>m; n:p;- m:[t]!p+ m:[s][s][s]!p }
− examples/unsat/test39.frm
@@ -1,15 +0,0 @@-signature {--propositions { p }-nominals { n}-relations { r : {functional},- s : {inverseof r} }--}--theory-{--E (p & <s><s>n) & E (!p & <s><s>n)--}
− examples/unsat/test40.frm
@@ -1,14 +0,0 @@-signature {--propositions { p }-nominals { n}-relations { r : {functional} }--}--theory-{--n:<r><r><r>( p & n:<r><r><r>!p)--}
src/HTab/Branch.hs view
@@ -1,31 +1,26 @@-------------------------------------------------------- ----- Branch.hs ----- --------------------------------------------------------- module HTab.Branch (-Branch(..), createNewProp, createNewPref, createNewNomTestRelevance, BranchInfo(..),-addFormulas, addFormula, addAccFormula,-addDiaRuleCheck, addDiaXRuleCheck, addDownRuleCheck, addDiffRuleCheck,+Branch(..), BranchInfo(..), TodoList(..), BlockingMode(..),+createNewPref, createNewProp, createNewNomTestRelevance,+addFormulas, addAccFormula,+addToBlockedDias,+addDiaRuleCheck, addDownRuleCheck, addDiffRuleCheck, addParentPrefix, addFirstFormulas,-TodoList(..),-emptyBranch,prefixes,+emptyBranch, reduceDisjunctionProposeLazy, doLazyBranching, merge,-getUrfather, getUrfatherAndDeps, isInTheModel, relationIsInTheModel,+getUrfather, getUrfatherAndDeps, getModelRepresentative, isNotBlocked,-BlockingMode(..), diaAlreadyDone, diaXAlreadyDone,-downAlreadyDone,-unfulfilledEventualities, ReducedDisjunct(..),-isSymmetric, isTransitive,-deleteUEV, insertUEV_addFormula+diaAlreadyDone, downAlreadyDone,+ReducedDisjunct(..),+patternOf, findByPattern,+prefixes, isInTheModel, relationIsInTheModel,+isSymmetric, isTransitive ) where +import Control.Applicative ( (<$>) ) import Data.List(minimumBy)-import Data.Maybe( mapMaybe )+import Data.Maybe( mapMaybe, fromMaybe ) import Data.Ord ( comparing ) import Data.Map ( Map )@@ -46,49 +41,47 @@ import HTab.Relations ( Relations(..), emptyRels, insertRelation, mergePrefixes, successors, predecessors, linksFromTo )-import qualified HTab.Relations as Relations data BranchInfo = BranchOK Branch | BranchClash Branch Prefix DependencySet Formula -type Clashable_info = DMap {- Prefix Literal -} DependencySet-type Box_constraints = DMap {- Prefix Rel -} [(Formula,DependencySet)]-type Branching_witnesses = DMap {- Prefix Literal -} [PrFormula]+type ClashableInfo = DMap {- Prefix Literal -} DependencySet+type BoxConstraints = DMap {- Prefix Rel -} [(Formula,DependencySet)]+type BranchingWitnesses = DMap {- Prefix Literal -} [PrFormula] type EquivClasses = DS.DisjSet DS.Pointer-data BlockingMode = AnywhereBlocking | ChainTwinBlocking deriving (Eq,Show)+data BlockingMode = PatternBlocking | AnywhereBlocking | ChainTwinBlocking deriving (Eq,Show) data Branch =- Branch {clashStr :: Clashable_info,+ Branch {+ -- the premodel+ clashStr :: ClashableInfo,+ accStr :: Relations, -- pending formulas / todo lists todoList :: TodoList, -- immediate rules constraints- boxConstrFwd :: Box_constraints,- boxConstrBwd :: Box_constraints,+ boxConstrFwd :: BoxConstraints,+ boxConstrBwd :: BoxConstraints, univCons :: [(DependencySet,Formula)], -- saturation of rules diaRlCh :: IntMap {- Prefix -} (Set (Rel,Formula)),- diaXRlCh :: IntMap {- Prefix -} (Set (Rel,Formula)),- boxRlCh :: IntMap {- Prefix -} (Set (Rel,Formula)),- boxXRlCh :: IntMap {- Prefix -} (Set (Rel,Formula)), downRlCh :: IntMap {- Prefix -} (Set Formula), atRlCh :: Set Formula, existRlCh :: Set Formula, dDiaRlCh :: Map Formula (Maybe Prop),- -- formulas true in an equivalence class+ -- pattern blocking+ individualPattern :: IntMap (Set Formula),+ -- set of formulas true at each point of the premodel prefToForms :: IntMap {- Prefix -} (Set Formula), -- backjumping data attached to equivalence classes prToDepSet :: IntMap {- Prefix -} DependencySet,- -- other data- accStr :: Relations,- -- equivalence classes+ -- prefix/nominal equivalence classes nomPrefClasses :: EquivClasses, -- book keeping lastPref :: Prefix, nextNom :: Nom, nextProp :: Prop,- eventualities :: IntMap DependencySet, -- lazy branching- brWitnesses :: Branching_witnesses,+ brWitnesses :: BranchingWitnesses, -- caching / memoisation data downVarRelevantCh :: Map Formula Bool, -- information about language of input formula and blocking mode@@ -103,30 +96,27 @@ -- -emptyBranch :: LanguageInfo -> RelInfo -> Encoding -> Branch-emptyBranch fLang relInfo_ encoding_ =+emptyBranch :: LanguageInfo -> RelInfo -> Encoding -> Params -> Branch+emptyBranch fLang relInfo_ encoding_ p = Branch { clashStr = DMap.empty,- todoList = emptyTodoList, accStr = emptyRels,+ todoList = emptyTodoList, boxConstrBwd = DMap.empty, boxConstrFwd = DMap.empty, diaRlCh = IntMap.empty,- diaXRlCh = IntMap.empty,- boxRlCh = IntMap.empty,- boxXRlCh = IntMap.empty, downRlCh = IntMap.empty, atRlCh = Set.empty, existRlCh = Set.empty, dDiaRlCh = Map.empty, downVarRelevantCh = Map.empty,+ individualPattern = IntMap.empty, univCons = [], lastPref = 0, nextNom = maxNom encoding_ + 4, nextProp = maxProp encoding_ + 4, prefToForms = IntMap.empty, prToDepSet = IntMap.empty,- eventualities = IntMap.empty, brWitnesses = DMap.empty, nomPrefClasses = DS.mkDSet, inputLanguage = fLang,@@ -138,104 +128,60 @@ relInfo = relInfo_, encoding = encoding_ }- where blockingMode =- if languagePast fLang- || languageTrans fLang- || relInfo_ `oneIs` Symmetric- || relInfo_ `oneIs` Functional- || relInfo_ `oneIs` Injective- then ChainTwinBlocking- else AnywhereBlocking+ where blockingMode+ | languagePast fLang || relInfo_ `oneIs` Symmetric = ChainTwinBlocking+ | patternBlocking p = PatternBlocking+ | otherwise = AnywhereBlocking instance Show Branch where show br = concat [ show (inputLanguage br), "\nClashable formulas:", showIMap (\v -> "(" ++ showMap_lits v ++ ")") "\n " (toMap $ clashStr br), "\n", show (todoList br),- showl "\nRelations: " (accStr br),- ifNotEmpty (boxConstrFwd br)- (\c -> "\nBox fwd: " ++ showIMap (\v -> "(" ++ showMap_rel v ++ ")") "\n " (toMap c)),- ifNotEmpty (boxConstrBwd br)- (\c -> "\nBox bwd: " ++ showIMap (\v -> "(" ++ showMap_rel v ++ ")") "\n " (toMap c)),- ifNotEmpty (brWitnesses br)- (\c -> "\nWitnesses: " ++ showIMap (\v -> "(" ++ showMap_lits2 v ++ ")") "\n " (toMap c)),- showl "\nDia rule chart: " (diaRlCh br),- showl "\nDown rule chart: " (downRlCh br),- showl "\n@ rule chart: " (list $ atRlCh br),- showl "\nExist rule chart: " (list $ existRlCh br),- showl "\nDiff dia rule chart: " (dDiaRlCh br),- showl "\nDown var relevant chart: " (downVarRelevantCh br),- showl "\nUniv constraints: " (univCons br),- ifNotEmpty (prToDepSet br) (\m -> "\nPrefix to dependency set:" ++ showIMap dsShow "\n " m),- ifNotEmpty (prefToForms br) (\m -> "\nPrefix to formulas:" ++ showIMap (show . Set.toList) "\n " m),- showl "\nEventualities: " (eventualities br),- showl "\nParent: " (prefParent br),+ "\nRelations: ", show (accStr br),+ "\nBox fwd: ", showIMap (\v -> "(" ++ showMap_rel v ++ ")") "\n " (toMap $ boxConstrFwd br),+ "\nBox bwd: ", showIMap (\v -> "(" ++ showMap_rel v ++ ")") "\n " (toMap $ boxConstrBwd br),+ "\nWitnesses: ", showIMap (\v -> "(" ++ showMap_lits2 v ++ ")") "\n " (toMap $ brWitnesses br),+ "\nDia rule chart: ", show (diaRlCh br),+ "\nIndividual patterns: ", show (individualPattern br),+ "\nDown rule chart: ", show (downRlCh br),+ "\n@ rule chart: ", show (list $ atRlCh br),+ "\nExist rule chart: ", show (list $ existRlCh br),+ "\nDiff dia rule chart: ", show (dDiaRlCh br),+ "\nDown var relevant chart: ", show (downVarRelevantCh br),+ "\nUniv constraints: ", show (univCons br),+ "\nPrefix to dependency set: ", showIMap dsShow "\n " (prToDepSet br),+ "\nPrefix to formulas: ", showIMap (show . Set.toList) "\n " (prefToForms br),+ "\nParent: ", show (prefParent br), "\nBlocking mode: ", show (blockMode br),- "\nPrefix-Nominal classes : ", showMap show ", " (nomPrefClasses br),- "\nModel-relevant nominals : " ++ (unwords $ map showLit $ list $ relevantNominals br),- "\nlastPref : " ++ show (lastPref br) ++- " nextnom : " ++ showLit (nextNom br) ++- " nextprop : " ++ showLit (nextProp br)+ "\nPrefix-Nominal classes : ", showMap ", " (nomPrefClasses br),+ "\nModel-relevant nominals : ", unwords $ map showLit $ list $ relevantNominals br,+ "\nlastPref : ", show (lastPref br),+ " nextnom : ", showLit (nextNom br),+ " 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.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 ++ ", ")) ""--class Emptyable a where- empty :: a -> Bool--instance Emptyable [a] where- empty [] = True- empty _ = False--instance Emptyable (Map a b) where- empty = Map.null--instance Emptyable (IntMap b) where- empty = IntMap.null--instance Emptyable (DMap c) where- empty (DMap m) = IntMap.null m--instance Emptyable Relations where- empty = Relations.null--instance Emptyable (Set a) where- empty = Set.null-+ showIMap :: (a -> String) -> String -> IntMap a -> String+ showIMap vShow sep = IntMap.foldWithKey (\k v -> (++ sep ++ show k ++ " -> " ++ vShow v )) ""+ showMap sep = Map.foldrWithKey (\k v -> (++ sep ++ show k ++ " -> " ++ show 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 ++ ", ")) "" data TodoList= TodoList{disjTodo :: Set PrFormula, diaTodo :: Set PrFormula,- diaXTodo :: Set PrFormula, existTodo :: Set PrFormula, atTodo :: Set PrFormula, downTodo :: Set PrFormula, diffTodo :: Set PrFormula, mergeTodo :: Set (DependencySet, Prefix, DS.Pointer), roleIncTodo :: Set (DependencySet, Prefix, Prefix, [Rel]) }--instance Show TodoList where- 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)+ deriving Show emptyTodoList :: TodoList emptyTodoList = TodoList { disjTodo = Set.empty, diaTodo = Set.empty,- diaXTodo = Set.empty, existTodo = Set.empty, atTodo = Set.empty, downTodo = Set.empty,@@ -249,8 +195,8 @@ prefixes and nominals -} -addFormulas :: Params -> Branch -> [PrFormula] -> BranchInfo-addFormulas p br fs =+addFormulas :: Params -> [PrFormula] -> Branch -> BranchInfo+addFormulas p fs br = foldr (\f bi -> case bi of BranchOK br2 -> addFormula p br2 f@@ -303,14 +249,12 @@ putAwayFormula :: Params -> PrFormula -> Branch -> BranchInfo putAwayFormula p pf@(PrFormula pr ds f2) br = case f2 of- Con fs -> addFormulas p br (prefix pr ds fs)+ Con fs -> addFormulas p (prefix pr ds fs) br Dis _ -> putAwayDisjunction p pf br Dia _ _ -> BranchOK $ addToTodo pf br- DiaX _ _ _ -> BranchOK $ addToTodo pf 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+ B f -> bRule pr f ds p br E _ -> BranchOK $ addToTodo pf br D _ -> BranchOK $ addToTodo pf br At _ _ -> BranchOK $ addToTodo pf br@@ -320,7 +264,7 @@ putAwayDisjunction :: Params -> PrFormula -> Branch -> BranchInfo putAwayDisjunction p pf@(PrFormula pr ds f@(Dis fs)) br- | lazyBranching p && ur <= unblockedPrefsLim br+ | lazyBranching p && blockMode br /= ChainTwinBlocking = case reduceDisjunctionProposeLazy br pr fs of Contradiction dsClash -> BranchClash br pr (dsUnion ds dsClash) f Triviality -> BranchOK br@@ -330,27 +274,28 @@ case mProposed of Nothing -> BranchOK $ addToTodo fNew br Just lit -- add pr, lit, ((++) disjuncts) aux witnesses- -> BranchOK $ doLazyBranching ur lit [fNew] br+ -> doLazyBranching ur lit [fNew] br | otherwise = BranchOK $ addToTodo pf br where ur = getUrfather br (DS.Prefix pr) putAwayDisjunction _ pf _ = error ("putAwayDisjunction " ++ show pf) -doLazyBranching :: Prefix -> Literal -> [PrFormula] -> Branch -> Branch-doLazyBranching pr lit pfs br -- assume the tests have been done beforehand+-- assume the tests have been done beforehand, always returns BranchOK+doLazyBranching :: Prefix -> Literal -> [PrFormula] -> Branch -> BranchInfo+doLazyBranching pr lit pfs br = case DMap.lookup1 pr (brWitnesses br) of Nothing -> let newBrW = DMap.insert pr lit pfs (brWitnesses br)- in br{brWitnesses = newBrW}+ in BranchOK br{brWitnesses = newBrW} Just innerMap -> case IntMap.lookup lit innerMap of -- assume this is the only place where l or (negLit l) occur Nothing -> let newInner = IntMap.insert lit pfs innerMap newBrW = DMap.insert1 pr newInner (brWitnesses br)- in br{brWitnesses = newBrW}+ in BranchOK br{brWitnesses = newBrW} Just fs -- assume the test was already done -> let newInner = IntMap.insert lit (pfs++fs) innerMap newBrW = DMap.insert1 pr newInner (brWitnesses br)- in br{brWitnesses = newBrW}+ in BranchOK br{brWitnesses = newBrW} -- TODO@@ -370,7 +315,6 @@ case f2 of Dis _ -> utodo{ disjTodo = Set.insert pf ( disjTodo utodo)} Dia _ _ -> utodo{ diaTodo = Set.insert pf ( diaTodo utodo)}- DiaX _ _ _ -> utodo{ diaXTodo = Set.insert pf ( diaXTodo utodo)} E _ -> utodo{existTodo = Set.insert pf (existTodo utodo)} D _ -> utodo{ diffTodo = Set.insert pf ( diffTodo utodo)} At _ _ -> utodo{ atTodo = Set.insert pf ( atTodo utodo)}@@ -385,7 +329,6 @@ At _ _ -> atAlreadyDone br f2 Down _ _ -> downAlreadyDone br pf Dia _ _ -> False -- the test happens later, when the todo list is processed- DiaX _ r ev -> diaXAlreadyDone br p (r,ev) Dis _ -> False -- the test happens later, when the todo list is processed Lit l | isPositiveNom l -> inSameClass br p l@@ -402,10 +345,15 @@ where toAdd = IntMap.findWithDefault [] pr (blockedDias br) br2 = br{blockedDias = IntMap.delete pr $ blockedDias br} +addToBlockedDias :: PrFormula -> Branch -> BranchInfo+addToBlockedDias f@(PrFormula pr _ _) br+ = BranchOK br{blockedDias = IntMap.insertWith (++) ur [f] (blockedDias br)}+ where ur = getUrfather br (DS.Prefix pr)+ {- helper functions for equivalence class merge -} -merge :: Params -> Branch -> Prefix -> DependencySet -> DS.Pointer -> BranchInfo-merge p br pr fDs pointer -- pointer is a nominal or a prefix+merge :: Params -> Prefix -> DependencySet -> DS.Pointer -> Branch -> BranchInfo+merge p pr fDs pointer br -- 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@@ -427,11 +375,11 @@ newClashableSlotUrfather = cisAddDeps currentDeps $ cisUnions clashableInfoSlots in case newClashableSlotUrfather of- Slot_UpdateFailure clashingDeps ->+ SlotUpdateFailure clashingDeps -> let newBr = br{nomPrefClasses = classes3} in BranchClash newBr pr (dsUnion clashingDeps currentDeps) (neg taut) - Slot_UpdateSuccess urfatherSlot ->+ SlotUpdateSuccess urfatherSlot -> let newClashStr = DMap $ IntMap.delete oldUr $ IntMap.insert newUr urfatherSlot (toMap $ clashStr br) -- structures that merge@@ -440,9 +388,6 @@ newBoxConstrBwd = DMap.moveInnerDataDMapPlusDeps fDs (boxConstrBwd br) oldUr newUr newAccStr = mergePrefixes (accStr br) oldUr newUr fDs newDiaRlCh = moveInMap (diaRlCh br) oldUr newUr Set.union- newDiaXRlCh = moveInMap (diaXRlCh br) oldUr newUr Set.union- newBoxRlCh = moveInMap (boxRlCh br) oldUr newUr Set.union- newBoxXRlCh = moveInMap (boxXRlCh br) oldUr newUr Set.union newBlockedDias = moveInMap (blockedDias br) oldUr newUr (++) (newBrWitnesses,unwitnessedToAdd) = mergeWitnesses oldUr newUr urfatherSlot (brWitnesses br) @@ -466,26 +411,23 @@ prToDepSet = newPrToDepSet, prefToForms = newPrefToForms, diaRlCh = newDiaRlCh,- diaXRlCh = newDiaXRlCh,- boxRlCh = newBoxRlCh,- boxXRlCh = newBoxXRlCh, blockedDias = newBlockedDias, clashStr = newClashStr, brWitnesses = newBrWitnesses} in- addFormulas p newBr formulasToAdd+ addFormulas p formulasToAdd newBr -mergeWitnesses :: Prefix -> Prefix -> Clashable_info_slot -> Branching_witnesses -> (Branching_witnesses, [PrFormula])+mergeWitnesses :: Prefix -> Prefix -> ClashableInfoSlot -> BranchingWitnesses -> (BranchingWitnesses, [PrFormula]) mergeWitnesses oldUr newUr urfatherSlot dbrWits@(DMap brWits) =( DMap.insert1 newUr newDest2 ( DMap.delete oldUr dbrWits ), toAdd1 ++ toAdd2 ) where- srcInnerMap = maybe IntMap.empty id (IntMap.lookup oldUr brWits)- destInnerMap = maybe IntMap.empty id (IntMap.lookup newUr brWits)- (newDest1,toAdd1) = mergeWitnesses_WitnessesMap srcInnerMap destInnerMap- (newDest2,toAdd2) = mergeWitnesses_AgainstClashable newDest1 urfatherSlot+ srcInnerMap = IntMap.findWithDefault IntMap.empty oldUr brWits+ destInnerMap = IntMap.findWithDefault IntMap.empty newUr brWits+ (newDest1,toAdd1) = mergeWitnessesWitnessesMap srcInnerMap destInnerMap+ (newDest2,toAdd2) = mergeWitnessesAgainstClashable newDest1 urfatherSlot -mergeWitnesses_WitnessesMap :: IntMap [PrFormula] -> IntMap [PrFormula] -> (IntMap [PrFormula], [PrFormula])-mergeWitnesses_WitnessesMap srcWitMap destWitMap+mergeWitnessesWitnessesMap :: IntMap [PrFormula] -> IntMap [PrFormula] -> (IntMap [PrFormula], [PrFormula])+mergeWitnessesWitnessesMap srcWitMap destWitMap = foldr go (destWitMap,[]) $ IntMap.assocs srcWitMap where go (l,fs) (destMap,toAddAgain)@@ -496,8 +438,8 @@ Just fs2 -> (IntMap.delete (negLit l) destMap, fs++fs2++toAddAgain) Nothing -> (IntMap.insert l fs destMap, toAddAgain) -mergeWitnesses_AgainstClashable :: IntMap [PrFormula] -> Clashable_info_slot -> (IntMap [PrFormula],[PrFormula])-mergeWitnesses_AgainstClashable witMap cis+mergeWitnessesAgainstClashable :: IntMap [PrFormula] -> ClashableInfoSlot -> (IntMap [PrFormula],[PrFormula])+mergeWitnessesAgainstClashable witMap cis = foldr go (witMap,[]) $ IntMap.assocs witMap where go (lit,fs) (destMap,toAddAgain)@@ -531,11 +473,12 @@ then f else PrFormula urfather (dsUnion ds ds2) f2 addToPrefToForms :: PrFormula -> Branch -> Branch-addToPrefToForms (PrFormula pr _ f) br | forInclusion br f =- br{prefToForms = newMap}+addToPrefToForms (PrFormula pr _ f) br+ | blockMode br == PatternBlocking = br+ | forInclusion br f = br{prefToForms = newMap}+ | otherwise = br where currentPtf = prefToForms br newMap = IntMap.insertWith Set.union pr (Set.singleton f) currentPtf-addToPrefToForms _ br = br {- handling nominal urfathers, equivalence classes and dependencies -} @@ -575,23 +518,6 @@ DS.Nominal _ -> False DS.Prefix p2 -> getUrfather br (DS.Prefix p) == p2 --- <*>-related functions--deleteUEV :: Branch -> Int -> Branch-deleteUEV br idx = br{eventualities = IntMap.delete idx (eventualities br)}--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- Just ((i,_),_) -> i+1- Just idx -> idx- newEvs = IntMap.insertWith dsUnion idxToUse ds $ eventualities br- br2 = br{eventualities= newEvs}- f = ff idxToUse- {- box-related constraints -} boxRule :: DependencySet -> (IntMap {- Rel -} [(Formula,DependencySet)], IntMap {- Rel -} [(Prefix,DependencySet)]) -> [PrFormula]@@ -604,8 +530,8 @@ (p,ds2) <- (IntMap.!) mapAcc r2 ] addBoxConstraint :: Prefix -> Rel -> Formula -> DependencySet -> Params -> Branch -> BranchInfo-addBoxConstraint pr_ r f ds p br_- | boxAlreadyDone br_ pr (r,f) = BranchOK br_+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@@ -615,8 +541,9 @@ else [] symApplications = [PrFormula pr ds $ Box (invRel r) f | isSymmetric (relInfo br) r] boxApplications = map (\(pr2,ds2) -> PrFormula pr2 (dsUnion ds ds2) f) accessiblePrDs+ -- todo check again with new pattern, create successor if new pattern not realized in- addFormulas p newBr toAdd+ addFormulas p toAdd newBr | otherwise = let newBr = br{boxConstrBwd = updateBoxConstr pr (atom r) f ds (boxConstrBwd br)}@@ -627,11 +554,10 @@ else [] boxApplications = map (\(pr2,ds2) -> PrFormula pr2 (dsUnion ds ds2) f) accessiblePrDs in- addFormulas p newBr toAdd- where pr = getUrfather br_ (DS.Prefix pr_)- br = addBoxRuleCheck br_ pr (r,f)+ addFormulas p toAdd newBr+ where pr = getUrfather br (DS.Prefix pr_) -updateBoxConstr :: Prefix -> Rel -> Formula -> DependencySet -> Box_constraints -> Box_constraints+updateBoxConstr :: Prefix -> Rel -> Formula -> DependencySet -> BoxConstraints -> BoxConstraints updateBoxConstr p1_ r_ f_ ds_ (DMap boxConstr_) = case IntMap.lookup p1_ boxConstr_ of Nothing -> DMap $ IntMap.insert p1_ (IntMap.singleton r_ [(f_,ds_)]) boxConstr_@@ -640,40 +566,26 @@ Nothing -> DMap $ IntMap.insert p1_ (IntMap.insert r_ [(f_,ds_)] innerMap) boxConstr_ Just innerInnerList -> DMap $ IntMap.insert p1_ (IntMap.insert r_ ((f_,ds_):innerInnerList) innerMap) boxConstr_ -addBoxRuleCheck :: Branch -> Prefix -> (Rel,Formula) -> Branch-addBoxRuleCheck br ur (r,f) =- br{boxRlCh=IntMap.insertWith Set.union ur (Set.singleton (r,f)) (boxRlCh br)}- boxAlreadyDone :: Branch -> Prefix -> (Rel,Formula) -> Bool-boxAlreadyDone b ur (r,f) =- case IntMap.lookup ur (boxRlCh b) of- Nothing -> False- Just fset -> Set.member (r,f) fset---- [*]phi --> phi & [][*]phi--- need not to do all that addBoxConstraint does-addBoxXConstraint :: Prefix -> Rel -> Formula -> DependencySet -> Params -> Branch -> BranchInfo-addBoxXConstraint pr r f ds p br- | boxXAlreadyDone br ur (r,f) = BranchOK br- | 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)--addBoxXRuleCheck :: Branch -> Prefix -> (Rel,Formula) -> Branch-addBoxXRuleCheck br ur (r,f) =- br{boxXRlCh=IntMap.insertWith Set.union ur (Set.singleton (r,f)) (boxXRlCh br)}+boxAlreadyDone br ur (r,f)+ | isForward r = case ( do inner <- IntMap.lookup ur (toMap $ boxConstrFwd br)+ boxes <- map fst <$> IntMap.lookup r inner+ return (f `elem` boxes) ) of+ Just True -> True+ _ -> False+ | otherwise = case ( do inner <- IntMap.lookup ur (toMap $ boxConstrBwd br)+ boxes <- map fst <$> IntMap.lookup (atom r) inner+ return (f `elem` boxes) ) of+ Just True -> True+ _ -> False -boxXAlreadyDone :: Branch -> Prefix -> (Rel,Formula) -> Bool-boxXAlreadyDone b ur (r,f) =- case IntMap.lookup ur (boxXRlCh b) of- Nothing -> False- Just fset -> Set.member (r,f) fset+-- accessibility Formulas -addAccFormula :: Params -> Branch -> AccFormula -> BranchInfo-addAccFormula p br (AccFormula ds r p1_ p2_)- | isBackwards r = addAccFormula p br (AccFormula ds (invRel r) p2_ p1_)+addAccFormula :: Params -> (DependencySet,Rel,Prefix,Prefix) -> Branch -> BranchInfo+addAccFormula p (ds, r, p1_, p2_) br+ | isBackwards r = addAccFormula p (ds, invRel r, p2_, p1_) br | otherwise -- forward- = addFormulas p newBr toAdd+ = addFormulas p toAdd newBr where toAdd = transApplications ++ boxApplications transApplications = if isTransitive (relInfo br) r then@@ -700,7 +612,7 @@ toschedule = map (\parents -> (ds,p1,p2,parents)) $ filter (not . alreadyDone) parentss alreadyDone = any (`elem` linksFromTo (accStr br) p1 p2) utodo = todoList br- newTodoList = utodo{roleIncTodo = Set.union (Set.fromList toschedule) (roleIncTodo utodo)}+ newTodoList = utodo{roleIncTodo = Set.fromList toschedule `Set.union` roleIncTodo utodo} insertRelationBranch :: Branch -> Prefix -> Rel -> Prefix -> DependencySet -> Branch insertRelationBranch br p1 r p2 ds@@ -709,12 +621,13 @@ {- blocking conditions -} -isNotBlocked :: Branch -> Prefix -> Bool-isNotBlocked br pr+isNotBlocked :: Branch -> PrFormula -> Bool+isNotBlocked br pf@(PrFormula pr _ _) | pr <= unblockedPrefsLim br = True | otherwise = case blockMode br of- AnywhereBlocking -> null $ filter isSubsumer labels+ PatternBlocking -> not $ patternBlocked br pf+ AnywhereBlocking -> not $ any isSubsumer labels where ur = getUrfather br (DS.Prefix pr) fs = formulasOf br ur isSubsumer fs_ = fs `Set.isSubsetOf` fs_@@ -726,7 +639,7 @@ getAllParents :: Branch -> Prefix -> [Prefix] -- getAllParents up to one that has an input nominal-getAllParents br pr = (getUrfather br (DS.Prefix pr)):rest+getAllParents br pr = getUrfather br (DS.Prefix pr):rest where rest = case IntMap.lookup pr (prefParent br) of Nothing -> [] Just parent -> if isNominalUrfather br parent@@ -744,7 +657,8 @@ isInTheModel :: Branch -> Prefix -> Bool isInTheModel br pr | isNominalUrfather br pr = case blockMode br of- AnywhereBlocking -> getModelRepresentative br pr == pr+ PatternBlocking -> True+ AnywhereBlocking -> True ChainTwinBlocking -> case findModelRepresentativeChainTwinBlocking br pr of Nothing -> False Just repr -> repr == pr@@ -753,23 +667,20 @@ relationIsInTheModel :: Branch -> (Prefix,Rel,Prefix) -> Bool relationIsInTheModel br (p1,_,p2) = case blockMode br of+ PatternBlocking -> True+ AnywhereBlocking -> True ChainTwinBlocking -> hasIdentityUrfather br p1 && hasIdentityUrfather br p2- AnywhereBlocking -> isInTheModel br p1 where hasIdentityUrfather br_ pr_ = case findModelRepresentativeChainTwinBlocking br_ pr_ of {Nothing -> False ; _ -> True } -getModelRepresentative :: Branch -> Prefix -> Prefix -- which is also an inclusion representative+getModelRepresentative :: Branch -> Prefix -> Prefix getModelRepresentative br pr = case blockMode br of- AnywhereBlocking-> case map fst $ filter (Set.isSubsetOf fs . snd) $ ascPrefToForm br of- [] -> pr- (hd:_) -> hd- where ur = getUrfather br (DS.Prefix pr)- fs = formulasOf br ur- ChainTwinBlocking -> case findModelRepresentativeChainTwinBlocking br pr of- Nothing -> error ("found an interesting counter example " ++ show pr)- Just repr -> repr-+ PatternBlocking -> ur+ AnywhereBlocking-> ur+ ChainTwinBlocking -> fromMaybe ( error $ "interesting counter example " ++ show pr)+ $ findModelRepresentativeChainTwinBlocking br pr+ where ur = getUrfather br (DS.Prefix pr) findModelRepresentativeChainTwinBlocking :: Branch -> Prefix -> Maybe Prefix findModelRepresentativeChainTwinBlocking br pr@@ -791,6 +702,42 @@ ascPrefToForm :: Branch -> [(Prefix,Set Formula)] ascPrefToForm br = [ (pr,formulasOf br pr) | pr <- prefixes br ] ++-- <r>f is pattern blocked if its pattern is a subset+-- of one pattern of the branch's pattern store+patternBlocked :: Branch -> PrFormula -> Bool+patternBlocked br f = not $ IntMap.null $ IntMap.filter lookForSuperset (individualPattern br) + where lookForSuperset = Set.isSubsetOf (patternOf br f)++-- given a p:<r>f formula, return the pattern:+-- { f } U { f' | p:[r]f' in branch }+-- r has to be forward+patternOf :: Branch -> PrFormula -> Set Formula+patternOf br (PrFormula pr _ (Dia r f))+ = Set.insert f boxes+ where ur = getUrfather br (DS.Prefix pr)+ boxes = if isTransitive (relInfo br) r+ then boxesOf br ur r `Set.union` (Set.map (Box r) $ boxesOf br ur r)+ else boxesOf br ur r++patternOf _ _ = error "patternOf called with a non diamond formula"++boxesOf :: Branch -> Prefix -> Rel -> Set Formula+boxesOf br p r+ = set $ map fst $ IntMap.findWithDefault [] r $ IntMap.findWithDefault IntMap.empty p (toMap $ boxConstrFwd br)++findByPattern :: Branch -> Set Formula -> Prefix+findByPattern br pattern+ | blockMode br == PatternBlocking =+ head $ map fst+ $ filter (\(_,pat2) -> pattern `Set.isSubsetOf` pat2)+ $ IntMap.toList $ individualPattern br+ | blockMode br == AnywhereBlocking =+ head $ map fst+ $ filter (\(_,pat2) -> pattern `Set.isSubsetOf` pat2)+ $ IntMap.toList $ prefToForms br+ | otherwise = error "findByPattern called with ChainTwinBlocking"+ -- maybe should get the urfather of given prefix, so that the caller functions won't have to do it formulasOf :: Branch -> Prefix -> Set Formula formulasOf br p = IntMap.findWithDefault Set.empty p (prefToForms br)@@ -807,22 +754,25 @@ forInclusion _ (Down _ _) = False forInclusion _ (Box _ _) = True forInclusion _ (Dia _ _) = True-forInclusion _ (BoxX _ _) = False-forInclusion _ (DiaX _ _ _) = False forInclusion _ (A _) = False forInclusion _ (E _) = False forInclusion _ (D _) = False forInclusion _ (B _) = False -addParentPrefix :: Branch -> Prefix -> Prefix -> Branch-addParentPrefix br son father = br{prefParent = IntMap.insert son father (prefParent br)}+addParentPrefix :: Prefix -> Prefix -> Branch -> BranchInfo+addParentPrefix son father br = BranchOK br{prefParent = IntMap.insert son father (prefParent br)} {- modifications done by rule application -} -addDiaRuleCheck :: Branch -> Prefix -> (Rel,Formula) -> Branch-addDiaRuleCheck br pr (r,f) =- br{diaRlCh=IntMap.insertWith Set.union ur (Set.singleton (r,f)) (diaRlCh br)}- where ur = getUrfather br (DS.Prefix pr)+addDiaRuleCheck :: Prefix -> (Rel,Formula) -> Prefix -> Branch -> BranchInfo+addDiaRuleCheck pr (r,f) newPr br =+ BranchOK br2+ where pattern = patternOf br (PrFormula ur dsEmpty (Dia r f))+ br1 = case blockMode br of+ PatternBlocking -> br{individualPattern = IntMap.insert newPr pattern (individualPattern br)}+ _ -> br+ br2 = br1{diaRlCh=IntMap.insertWith Set.union ur (Set.singleton (r,f)) (diaRlCh br1)}+ ur = getUrfather br (DS.Prefix pr) diaAlreadyDone :: Branch -> PrFormula -> Bool diaAlreadyDone b (PrFormula p _ (Dia r f)) =@@ -834,31 +784,9 @@ diaAlreadyDone _ _ = error "dia already done : wrong formula kind" -- -addDiaXRuleCheck :: Branch -> Prefix -> (Rel, Formula) -> Branch-addDiaXRuleCheck br pr f =- br{diaXRlCh=IntMap.insertWith Set.union ur (Set.singleton f) (diaXRlCh br)}- where ur = getUrfather br (DS.Prefix pr)--diaXAlreadyDone :: Branch -> Prefix -> (Rel,Formula) -> Bool-diaXAlreadyDone b p f =- case IntMap.lookup ur (diaXRlCh b) of- Nothing -> False- Just fset -> Set.member f fset- where ur = getUrfather b (DS.Prefix p)----unfulfilledEventualities :: Branch -> Maybe DependencySet-unfulfilledEventualities br- = if IntMap.null $ eventualities br- then Nothing- else Just $ dsUnions $ IntMap.elems $ eventualities br------addDownRuleCheck :: Branch -> Prefix -> Formula -> Branch-addDownRuleCheck br pr f =- br{downRlCh=IntMap.insertWith Set.union ur (Set.singleton f) (downRlCh br)}+addDownRuleCheck :: Prefix -> Formula -> Branch -> BranchInfo+addDownRuleCheck pr f br =+ BranchOK br{downRlCh=IntMap.insertWith Set.union ur (Set.singleton f) (downRlCh br)} where ur = getUrfather br (DS.Prefix pr) downAlreadyDone :: Branch -> PrFormula -> Bool@@ -886,30 +814,32 @@ addUnivConstraint :: Formula -> DependencySet -> Params -> Branch -> BranchInfo addUnivConstraint f ds p br- = addFormulas p newBr+ = addFormulas p ( map (\pr -> PrFormula pr ds f) urfathers )+ newBr where newBr = br{univCons = (ds,f):(univCons br)} prefs = [0..(lastPref br)] urfathers = filter (isNominalUrfather br) prefs -- -b_rule :: Prefix -> Formula -> DependencySet -> Params -> Branch -> BranchInfo-b_rule pr f ds p br+bRule :: Prefix -> Formula -> DependencySet -> Params -> Branch -> BranchInfo+bRule 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} -- -addDiffRuleCheck :: Branch -> Formula -> Maybe Prop -> Branch-addDiffRuleCheck br f mp = br{dDiaRlCh=Map.insert f mp (dDiaRlCh br)}+addDiffRuleCheck :: Formula -> Maybe Prop -> Branch -> BranchInfo+addDiffRuleCheck f mp br = BranchOK br{dDiaRlCh=Map.insert f mp (dDiaRlCh br)} -- createNewPref :: Params -> Branch -> BranchInfo createNewPref p br- = addFormulas p newBrWithRefl- ( map (\(ds,f) -> PrFormula newPr ds f) univConstraints )+ = addFormulas p+ ( map (\(ds,f) -> PrFormula newPr ds f) univConstraints )+ newBrWithRefl where newPr = lastPref br + 1 newBr = br{lastPref = newPr} univConstraints = univCons br@@ -923,15 +853,16 @@ -- -createNewProp :: Branch -> Branch-createNewProp br = br{nextProp = nextProp br + 4}+createNewProp :: Branch -> BranchInfo+createNewProp br = BranchOK br{nextProp = nextProp br + 4} -createNewNomTestRelevance :: Branch -> Formula -> Branch-createNewNomTestRelevance br f- = br{nextNom = nextNom br + 4,- relevantNominals = if relevant then Set.insert newNom (relevantNominals br) else relevantNominals br,- downVarRelevantCh = newDVRC- }+createNewNomTestRelevance :: Formula -> Branch -> BranchInfo+createNewNomTestRelevance f br+ = BranchOK+ br{nextNom = nextNom br + 4,+ relevantNominals = if relevant then Set.insert newNom (relevantNominals br) else relevantNominals br,+ downVarRelevantCh = newDVRC+ } where (relevant, newDVRC) = doMemoize checkIfVariableNegatedOnce f (downVarRelevantCh br) newNom = nextNom br @@ -942,10 +873,9 @@ -- - add a nominal formula at a fresh prefix for each nominal of the input language -- (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 :: Params -> Branch -> LanguageInfo -> Formula -> BranchInfo addFirstFormulas p br_ fLang f- = addFormulas p br5 ([pf]++funUniv++injUniv)+ = addFormulas p [pf] br4 where ns = languageNoms fLang nbNs = length ns nomWitnesses = [1..nbNs]@@ -962,19 +892,11 @@ br3 = foldr (\(pr,n) -> bookKeepFormula p (PrFormula pr dsEmpty (Lit n))) br2 (zip [1..] ns)- funUniv = map (\r -> PrFormula 0 dsEmpty- $ A $ Down newNom $ Box (inv r (relInfo br)) $ Box r (Lit newNom)) funRels- where funRels = Map.keys $ Map.filter (elem Functional) (relInfo br)- injUniv = map (\r -> PrFormula 0 dsEmpty- $ A $ Down newNom $ Box r $ Box (inv r (relInfo br)) (Lit newNom)) injRels- where injRels = Map.keys $ Map.filter (elem Injective) (relInfo br)- newNom = nextNom br3- br4 = br3{nextNom = nextNom br3 + 4}- br5 = br4{unblockedPrefsLim = nbNs}+ br4 = br3{unblockedPrefsLim = nbNs} {- functions to handle the "clashable information", ie literals associated to prefixes -} -data UpdateResult = UpdateSuccess Clashable_info | UpdateFailure DependencySet+data UpdateResult = UpdateSuccess ClashableInfo | UpdateFailure DependencySet addToClashable :: Prefix -> DependencySet -> Literal -> Branch -> BranchInfo addToClashable pr_ ds1 l br@@ -987,51 +909,51 @@ -- Insert a piece of clashable information into all the clashable information of a branch -updateMap :: Clashable_info -> Prefix -> DependencySet -> Literal -> UpdateResult+updateMap :: ClashableInfo -> Prefix -> DependencySet -> Literal -> UpdateResult updateMap cs _ ds l | isTop l = UpdateSuccess cs | isBottom l = UpdateFailure ds updateMap (DMap cs) pre ds l = case IntMap.lookup pre cs of- Nothing -> UpdateSuccess $ DMap $ IntMap.insert pre (IntMap.singleton l ds) cs- Just slot -> case cisUpdate slot l ds of- Slot_UpdateSuccess updatedSlot -> UpdateSuccess $ DMap $ IntMap.insert pre updatedSlot cs- Slot_UpdateFailure failureDeps -> UpdateFailure failureDeps+ Nothing -> UpdateSuccess $ DMap $ IntMap.insert pre (IntMap.singleton l ds) cs+ Just slot -> case cisUpdate slot l ds of+ SlotUpdateSuccess updatedSlot -> UpdateSuccess $ DMap $ IntMap.insert pre updatedSlot cs+ SlotUpdateFailure failureDeps -> UpdateFailure failureDeps -type Clashable_info_slot = IntMap {- Literal -} DependencySet-data Slot_UpdateResult = Slot_UpdateSuccess Clashable_info_slot- | Slot_UpdateFailure DependencySet+type ClashableInfoSlot = IntMap {- Literal -} DependencySet+data SlotUpdateResult = SlotUpdateSuccess ClashableInfoSlot+ | SlotUpdateFailure DependencySet -- Union a list of clashable info slots-cisUnions :: [Clashable_info_slot] -> Slot_UpdateResult-cisUnions [] = Slot_UpdateSuccess IntMap.empty-cisUnions [cis] = Slot_UpdateSuccess cis+cisUnions :: [ClashableInfoSlot] -> SlotUpdateResult+cisUnions [] = SlotUpdateSuccess IntMap.empty+cisUnions [cis] = SlotUpdateSuccess cis cisUnions (cis1:cis2:tl) = case cisUnion cis1 cis2 of- failure@(Slot_UpdateFailure _) -> failure- Slot_UpdateSuccess newCis -> cisUnions (newCis:tl)+ failure@(SlotUpdateFailure _) -> failure+ SlotUpdateSuccess newCis -> cisUnions (newCis:tl) -- Union two clashable info slots -- if there is a clash, the result reports the set of dependencies whose earliest dependency is the earliest -- among all dependencies sets that caused the clash-cisUnion :: Clashable_info_slot -> Clashable_info_slot -> Slot_UpdateResult+cisUnion :: ClashableInfoSlot -> ClashableInfoSlot -> SlotUpdateResult cisUnion cis1 cis2 = ucis_helper cis1 (IntMap.assocs cis2)- where ucis_helper :: Clashable_info_slot -> [(Literal,DependencySet)] -> Slot_UpdateResult+ where ucis_helper :: ClashableInfoSlot -> [(Literal,DependencySet)] -> SlotUpdateResult ucis_helper cis l_ds_s = let (updateStatus,clashing_ds_s) = foldr (\(l,ds) (upResult,clashingBps_s) -> case upResult of- Slot_UpdateSuccess cis_ -> (cisUpdate cis_ l ds, clashingBps_s)- Slot_UpdateFailure ds_s -> (cisUpdate cis l ds, ds_s:clashingBps_s)+ SlotUpdateSuccess cis_ -> (cisUpdate cis_ l ds, clashingBps_s)+ SlotUpdateFailure ds_s -> (cisUpdate cis l ds, ds_s:clashingBps_s) -- we reuse the input Clashabe Info Slot )- (Slot_UpdateSuccess cis,[]) l_ds_s+ (SlotUpdateSuccess cis,[]) l_ds_s result = case clashing_ds_s of [] -> updateStatus -- is 'success'- ds_s -> Slot_UpdateFailure $ findEarliestSet ds_s+ ds_s -> SlotUpdateFailure $ findEarliestSet ds_s where findEarliestSet = minimumBy compareBPSets compareBPSets ds1 ds2 = comparing dsMin ds1 ds2 in@@ -1040,23 +962,23 @@ -- Insert a piece of information in a clashable info slot -cisUpdate :: Clashable_info_slot -> Literal -> DependencySet -> Slot_UpdateResult-cisUpdate cis l ds | isTop l = Slot_UpdateSuccess cis- | isBottom l = Slot_UpdateFailure ds+cisUpdate :: ClashableInfoSlot -> Literal -> DependencySet -> SlotUpdateResult+cisUpdate cis l ds | isTop l = SlotUpdateSuccess cis+ | isBottom l = SlotUpdateFailure ds cisUpdate cis l ds -- nominals, propositional symbols = case IntMap.lookup (negLit l) cis of- Just ds2 -> Slot_UpdateFailure $ dsUnion ds ds2- Nothing -> Slot_UpdateSuccess $ IntMap.insertWith mergeDeps l ds cis+ Just ds2 -> SlotUpdateFailure $ dsUnion ds ds2+ Nothing -> SlotUpdateSuccess $ IntMap.insertWith mergeDeps l ds cis where mergeDeps d1 d2 = if dsMin d1 < dsMin d2 then d1 else d2 -- if the same information is caused by an earlier -- branching, only keep the information of the earliest set of dependencies -- Other functions related to clashable information -cisAddDeps :: DependencySet -> Slot_UpdateResult -> Slot_UpdateResult+cisAddDeps :: DependencySet -> SlotUpdateResult -> SlotUpdateResult cisAddDeps ds res_cis = case res_cis of- Slot_UpdateSuccess cis -> Slot_UpdateSuccess $ IntMap.map (dsUnion ds) cis+ SlotUpdateSuccess cis -> SlotUpdateSuccess $ IntMap.map (dsUnion ds) cis failure -> failure @@ -1074,7 +996,6 @@ {- function used for unit propagation -} - data ReducedDisjunct = Triviality | Contradiction DependencySet@@ -1126,10 +1047,6 @@ isTransitive = hasProperty Transitive 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,
src/HTab/CommandLine.hs view
@@ -1,11 +1,4 @@-------------------------------------------------------- ----- CommandLine.hs: ----- Functions that handle command line processing ----- and presentation--- --------------------------------------------------------+{-# OPTIONS_GHC -fno-warn-missing-fields #-} module HTab.CommandLine ( Params(..), UnitProp(..), defaultParams, configureStats, checkParams@@ -13,11 +6,12 @@ import System.Console.CmdArgs import Data.List ( sort )-+import Data.Maybe ( isNothing ) import HTab.Statistics( StatisticsState, setPrintOutInterval ) data Params = Params { filename :: Maybe FilePath,+ stdin :: Bool, genModel :: Maybe FilePath, dotModel :: Bool, timeout :: Int,@@ -26,63 +20,62 @@ semBranch :: Bool, backjumping :: Bool, lazyBranching :: Bool,+ patternBlocking :: Bool, unitProp :: UnitProp,- noLoopCheck :: Bool, showFormula :: Bool, allTransitive :: Bool, allReflexive :: Bool,- allSymmetric :: Bool,- allFunctional :: Bool,- allInjective :: Bool+ allSymmetric :: Bool } deriving (Show, Data, Typeable) data UnitProp = Eager | UPYes | UPNo deriving (Data, Typeable, Eq, Show) -defaultParams :: Params+defaultParams :: Annotate Ann defaultParams- = 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",- semBranch = True &= help "enable semantic branching (default)",- backjumping = True &= help "enable backjumping (default)",- lazyBranching = True &= help "enable lazy branching (default)" ,- unitProp = enum [Eager &= explicit &= name "eager" &= help "unit propagation: eager (default)",- UPYes &= explicit &= name "unit-prop" &= help "unit propagation: enabled",- UPNo &= explicit &= name "no-unit-prop" &= help "unit propagation: disabled"] ,- noLoopCheck = False &= help "disable all loop check",- showFormula = False &= help "display formula",- allTransitive = False &= help "make all relations transitive",- allReflexive = False &= help "make all relations reflexive",- allSymmetric = False &= help "make all relations symmetric",- allFunctional = False &= help "make all relations functional",- allInjective = False &= help "make all relations injective"- } &= verbosity+ = record Params{}+ [ filename := Nothing += name "f" += typFile += help "input file",+ stdin := False += help "use standard input instead of file",+ genModel := Nothing += name "m" += typFile += help "output model file",+ dotModel := False += 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",+ semBranch := True += help "enable semantic branching (default)",+ backjumping := True += help "enable backjumping (default)",+ lazyBranching := True += help "enable lazy branching (default)" ,+ patternBlocking := True += help "use pattern blocking instead of anywhere blocking (default)" ,+ unitProp `enum_` [atom Eager += explicit += name "eager" += help "unit propagation: eager (default)",+ atom UPYes += explicit += name "unit-prop" += help "unit propagation: enabled",+ atom UPNo += explicit += name "no-unit-prop" += help "unit propagation: disabled"] ,+ showFormula := False += help "display formula",+ allTransitive := False += help "make all relations transitive",+ allReflexive := False += help "make all relations reflexive",+ allSymmetric := False += help "make all relations symmetric"+ ] += verbosity strategyVal :: String-strategyVal = "n@E<Db|*r"+strategyVal = "n@E<Db|r" checkParams :: Params -> IO Bool checkParams p- = if strategy p `permutationOf` strategyVal- then return True- else do putStrLn- $ unlines ["ERROR",- "strategy should contain all of the following characters: ",- " n = nominals @ = satisfaction operator",- " E = existential modality < = diamond",- " D = difference modality b = down-arrow binder",- " | = or * = transitive closure diamond",- " r = role inclusion",- "",- "The default is `" ++ strategyVal ++ "'",- "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+ | strategy p `notPermutationOf` strategyVal =+ do putStrLn+ $ unlines ["ERROR",+ "strategy should contain all of the following characters: ",+ " n = nominals @ = satisfaction operator",+ " E = existential modality < = diamond",+ " D = difference modality b = down-arrow binder",+ " | = or r = role inclusion",+ "",+ "The default is `" ++ strategyVal ++ "'",+ "The rules conjunction, box, universal modality and converse difference",+ "modality are immediate, thus do not belong to the strategy."]+ return False+ | not (stdin p) && isNothing (filename p) =+ do putStrLn $ unlines ["ERROR: No input specified.","Run with --help for usage options"]+ return False+ | otherwise = return True+ where notPermutationOf l1 l2 = sort l1 /= sort l2 configureStats :: Params -> StatisticsState () configureStats p = setPrintOutInterval $ stats p
src/HTab/Formula.hs view
@@ -1,12 +1,3 @@-------------------------------------------------------- ----- Formula.hs: ----- Formula data type, normal ----- form and show functions. ----- --------------------------------------------------------- module HTab.Formula (Atom, Prop, Nom, Literal,@@ -14,10 +5,10 @@ DependencySet, Dependency, dsUnion, dsUnions, dsInsert, dsMember, dsEmpty, dsMin, dsShow, addDeps,-PrFormula(..),showLess, AccFormula(..),+PrFormula(..),showLess, LanguageInfo(..), neg, conj, disj, taut,-prop, nom, formulaLanguageInfo, prefix,+prop, nom, formulaLanguageInfo, prefix, negPr, checkIfVariableNegatedOnce, replaceVar, firstPrefixedFormula, parse, simpleParse, Theory, RelInfo, Task,@@ -25,7 +16,7 @@ encodeValidityTest, encodeSatTest, encodeRetrieveTask, HyLoFormula, RelProperty(..), Encoding(..), maxNom, maxProp, toPropSymbol, toNomSymbol, toRelSymbol, isTop, isBottom, isPositiveNom, isPositiveProp, isPositive, isNegative, isNominal, isProp, atom,-inv, invRel, int+invRel, int ) where@@ -69,8 +60,6 @@ | Box Rel Formula | Dia Rel Formula | Down Nom Formula- | BoxX Rel Formula- | DiaX (Maybe Int) Rel Formula | A Formula | E Formula | D Formula@@ -135,8 +124,6 @@ show (At n f) = showLit n ++ ":(" ++ show f ++ ")" show (Box r f) = "[" ++ showRel r ++ "]" ++ show f show (Dia r f) = "<" ++ showRel r ++ ">" ++ show f- show (BoxX r f) = "[" ++ showRel r ++ "*]" ++ show f- show (DiaX i r f) = "<" ++ showRel r ++ "*>(" ++ show i ++ ")" ++ show f show (A f) = "A" ++ show f show (E f) = "E" ++ show f show (D f) = "D" ++ show f@@ -153,8 +140,6 @@ data RelProperty = Reflexive | Symmetric | Transitive- | Functional- | Injective | Universal | Difference --@@ -172,7 +157,7 @@ where parseOutput = InputFile.myparse s -- direct parse from hylolib encoding = getEncoding parseOutput pRelInfo = P.relations parseOutput- relInfo = handleFunInj $ saturate $ forceProperties p encoding $ convertToOurType pRelInfo encoding -- TODO+ relInfo = forceProperties p encoding $ convertToOurType pRelInfo encoding -- TODO theory = convert relInfo encoding $ P.theory parseOutput tasks = P.tasks parseOutput @@ -235,11 +220,9 @@ where rels = Map.elems $ relMap encoding addToAll r = Map.insertWith (\c1 c2 -> nub $ c1 ++ c2) r conds conds = map snd $- filter fst $ [(allTransitive p, Transitive),+ filter fst [(allTransitive p, Transitive), (allReflexive p, Reflexive ),- (allSymmetric p, Symmetric ),- (allFunctional p, Functional),- (allInjective p, Injective )]+ (allSymmetric p, Symmetric )] 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)@@ -248,14 +231,14 @@ c r P.Reflexive = [(int e r,Reflexive )] c r P.Symmetric = [(int e r,Symmetric )] c r P.Transitive = [(int e r,Transitive )]- c r P.Functional = [(int e r,Functional )] c r P.Universal = [(int e r,Universal )] c r P.Difference = [(int e r,Difference )] c r (P.InverseOf s) = [(int e r,InverseOf (int e s))]- c r (P.TRClosureOf s) = [(int e r,TRClosureOf (int e s))] c r (P.SubsetOf ss) = [(int e r,SubsetOf [ int e s | s <- ss])] 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"+ c _ (P.TRClosureOf _) = error "TRClosureOf not handled"+ c _ P.Functional = error "Functional not handled" simpleParse :: Params -> String -> (Theory,RelInfo,Encoding,[Task]) simpleParse p s = parse p $ "signature { automatic } theory { " ++ removeBeginEnd s ++ "}"@@ -286,176 +269,29 @@ type Connector = Formula -> Formula specialiseDia :: S.RelSymbol -> RelInfo -> Encoding -> Connector-specialiseDia r relI e = specialise r relI (diamond e, diamondX e, dExistMod, existMod) e+specialiseDia r relI e = specialise r relI (diamond e, dExistMod, existMod) e specialiseBox :: S.RelSymbol -> RelInfo -> Encoding -> Connector-specialiseBox r relI e = specialise r relI (box e, boxX e, dUnivMod, univMod) e+specialiseBox r relI e = specialise r relI (box e, dUnivMod, univMod) e -specialise :: S.RelSymbol -> RelInfo -> (S.RelSymbol -> Connector, S.RelSymbol -> Connector, Connector, Connector) -> Encoding -> Connector-specialise (S.InvRelSymbol r) _ (relational, _ , _ , _) _ -- happens only with simple input+specialise :: S.RelSymbol -> RelInfo -> (S.RelSymbol -> Connector, Connector, Connector) -> Encoding -> Connector+specialise (S.InvRelSymbol r) _ (relational, _ , _) _ -- happens only with simple input = relational $ S.InvRelSymbol r -specialise (S.RelSymbol r) relI (relational, rtclosure, difference, global) e- = case filter interesting props of- (Difference:_) -> difference- (Universal:_) -> global- [] -> relational $ S.RelSymbol r- _ -> case specialise2 (int e r) relI of- Just_ r2 -> relational $ toRelSymbol e r2- Inverse r2 -> relational $ invRS $ toRelSymbol e r2- RTClosure r2 -> rtclosure $ toRelSymbol e r2- RTClosureInv r2 -> rtclosure $ invRS $ toRelSymbol e r2- where- interesting Difference = True- interesting Universal = True- interesting (InverseOf _) = True- interesting (TRClosureOf _) = True- interesting _ = False- props = Map.findWithDefault [] (int e r) relI- invRS (S.RelSymbol s) = S.InvRelSymbol s- invRS (S.InvRelSymbol s) = S.RelSymbol s--data ModType = Just_ Rel | Inverse Rel | RTClosure Rel | RTClosureInv Rel--specialise2 :: Rel -> RelInfo -> ModType-specialise2 r_ relI- = go (Just_ r_)- where- go j@(Just_ r) =- case filter interesting (propsOf r) of- (InverseOf r2:_) -> go (Inverse r2)- (TRClosureOf r2:_) -> go (RTClosure r2)- _ -> j-- go io@(Inverse r) =- case filter interesting (propsOf r) of- (InverseOf r2:_) -> go (Just_ r2)- (TRClosureOf r2:_) -> RTClosureInv r2- _ -> io-- go rtc@(RTClosure r) =- case filter interesting (propsOf r) of- (InverseOf r2:_) -> RTClosureInv r2- (TRClosureOf r2:_) -> go (RTClosure r2)- _ -> rtc-- go rtci@(RTClosureInv r) =- case filter interesting (propsOf r) of- (InverseOf r2:_) -> RTClosure r2- _ -> rtci-- interesting (InverseOf _) = True- interesting (TRClosureOf _) = True- interesting _ = False- propsOf r__ = Map.findWithDefault [] r__ relI---inv :: Rel -> RelInfo -> Rel-inv r relI- = case Map.lookup r relI of- Nothing -> r- Just properties -> if Symmetric `elem` properties then r else invRel r+-- below we don't attempt checking if r is an inverse of an inverse+specialise (S.RelSymbol r) relI (relational, difference, global) e+ | Difference `elem` props = difference+ | Universal `elem` props = global+ | otherwise = case [ r2 | InverseOf r2 <- props] of+ [] -> relational $ S.RelSymbol r+ (r2:_) -> relational $ invRS $ toRelSymbol e r2+ where+ invRS (S.RelSymbol s) = S.InvRelSymbol s+ invRS (S.InvRelSymbol s) = S.RelSymbol s+ where props = Map.findWithDefault [] (int e r) relI type HyLoFormula = F.Formula S.NomSymbol S.PropSymbol S.RelSymbol --- saturate RelInfo with hierarchy information : Reflexive, Symmetric, Transitive, Universal, Difference--saturate :: RelInfo -> RelInfo-saturate relI = Map.mapWithKey saturateOne relI- where saturateOne r props = let ancestorProps = concatMap (getProperties relI) $ getAncestors r relI- newProps = list $ Set.union (set ancestorProps) (set props)- in- newProps--getProperties :: RelInfo -> Rel -> [RelProperty]-getProperties ri r- = getOnlyProps $ filter isProp_ props- where props = Map.findWithDefault [] r ri- getOnlyProps = filter isProp_- isProp_ Reflexive = True- isProp_ Symmetric = True- isProp_ Transitive = True- isProp_ Universal = True- isProp_ Difference = True- isProp_ _ = False--getAncestors :: Rel -> RelInfo -> [Rel]-getAncestors r_ relI =- list $ go (Set.singleton r_) r_- where- go seen r =- let props = Map.findWithDefault [] r relI- parents = concatMap extractParent props- extractParent (InverseOf rp) = [rp]- extractParent (TRClosureOf rp) = [rp]- extractParent _ = [ ]- todo = list ( (set parents) Set.\\ seen )- newSeen = Set.union seen $ set parents- in- case todo of- [] -> Set.singleton r- _ -> Set.insert r $ Set.unions $ map (go newSeen) todo---- ==========================================================================------ saturate relInfo with the properties Functional and Injective--- rationale : being able to enforce Injectivity even though the--- input format does not have an Injective label.--- the solution to do so is:--- R_injective , Inv_R { inverseof R_injective, Functional }------ ==========================================================================--data FunInj = Not | Fun | Inj | FunInj--handleFunInj :: RelInfo -> RelInfo-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.foldrWithKey startFromLeaf relI relI- where startFromLeaf rs props currentRelI = follow rs props currentRelI Not-- follow rs props currentRelI currentStatus- = case parentsWithInv props status of- Just (parent,newStatus) -> let parentProps = Map.findWithDefault [] parent currentRelI in- follow parent parentProps currentRelI newStatus- Nothing- -> case currentStatus of- Not -> currentRelI- _ -> Map.insertWith (++) rs (toProps status) currentRelI- where- status = if Functional `elem` props- then case currentStatus of- FunInj -> FunInj- Inj -> FunInj- Fun -> Fun- Not -> Fun- else currentStatus- toProps Not = []- toProps FunInj = [Functional, Injective]- toProps Fun = [Functional]- toProps Inj = [Injective]-- parentsWithInv props status- = case concatZip $ map extractParent props of- ([],[]) -> Nothing- ((par:_),_) -> Just (par, invert status)- where invert Not = Not- invert FunInj = FunInj- invert Fun = Inj- invert Inj = Fun- (_,(par:_)) -> Just (par, status)- where extractParent (InverseOf rp) = ([rp],[])- extractParent (TRClosureOf rp) = ([] ,[rp])- extractParent _ = ([] ,[])---concatZip :: [([a],[b])] -> ([a],[b])-concatZip [] = ([],[])-concatZip ((as,bs):tl) = (as++as2,bs++bs2) where (as2,bs2) = concatZip tl---- ==========================================================================- encodeValidityTest :: RelInfo -> Encoding -> Formula -> [HyLoFormula] -> Formula encodeValidityTest relI e th fs = neg $ conj th (convert relI e fs)@@ -481,31 +317,27 @@ prop e (S.PropSymbol p) = Lit ( propMap e Map.! p ) {- Modalities -}-box, diamond, boxX, diamondX :: Encoding -> S.RelSymbol -> Formula -> Formula+box, diamond :: Encoding -> S.RelSymbol -> Formula -> Formula univMod, existMod, dUnivMod, dExistMod :: Formula -> Formula box e (S.RelSymbol r) = Box $ int e r box e (S.InvRelSymbol r) = Box $ invRel $ int e r diamond e (S.RelSymbol r) = Dia $ int e r diamond e (S.InvRelSymbol r) = Dia $ invRel $ int e r-boxX e (S.RelSymbol r) = BoxX $ int e r-boxX e (S.InvRelSymbol r) = BoxX $ invRel $ int e r-diamondX e (S.RelSymbol r) = DiaX Nothing $ int e r-diamondX e (S.InvRelSymbol r) = DiaX Nothing $ invRel $ int e r univMod = A existMod = E dUnivMod = B dExistMod = D int :: Encoding -> String -> Int-int e s = (relMap e) Map.! s+int e s = relMap e Map.! s {- binder -} downArrow :: Encoding -> S.NomSymbol -> Formula -> Formula-downArrow e (S.NomSymbol n) = Down ((nomMap e) Map.! n)+downArrow e (S.NomSymbol n) = Down (nomMap e Map.! n) {- Hybrid operators -} at :: Encoding -> S.NomSymbol -> Formula -> Formula-at e (S.NomSymbol n) = At ((nomMap e) Map.! n)+at e (S.NomSymbol n) = At (nomMap e Map.! n) {- Conjunction and disjunction -} @@ -570,8 +402,6 @@ neg (Down v f) = Down v (neg f) neg (Box r f) = Dia r (neg f) neg (Dia r f) = Box r (neg f)-neg (BoxX r f) = DiaX Nothing r (neg f)-neg (DiaX _ r f) = BoxX r (neg f) neg (A f) = E (neg f) neg (E f) = A (neg f) neg (D f) = B (neg f)@@ -585,7 +415,7 @@ deriving Eq instance Show PrFormula where- show (PrFormula pr ds f) = show pr ++ ":" ++ (dsShow ds) ++ ":" ++ show f+ show (PrFormula pr ds f) = show pr ++ ":" ++ dsShow ds ++ ":" ++ show f showLess :: PrFormula -> String showLess (PrFormula pr _ f) = show pr ++ ":" ++ show f@@ -596,27 +426,20 @@ firstPrefixedFormula :: Formula -> PrFormula firstPrefixedFormula = PrFormula 0 dsEmpty --- accessibility Formulas--data AccFormula = AccFormula DependencySet Rel Prefix Prefix- deriving (Eq, Ord)--instance Show AccFormula where- show (AccFormula bprs r p1 p2) = show bprs ++ ":" ++ show p1 ++ "<" ++ showRel r ++ ">" ++ show p2+negPr :: PrFormula -> PrFormula+negPr (PrFormula p ds f) = PrFormula p ds (neg f) -- formula language data LanguageInfo = LanguageInfo { languageNoms :: [Int], -- ascending list relevantNoms :: [Int],- languagePast :: Bool,- languageTrans :: Bool }+ languagePast :: Bool} instance Show LanguageInfo where show li = "Input Language:" ++ "\n|" ++ yesnol "Noms" ( languageNoms li ) ++ "\n|" ++ yesnol "Relevant Noms" ( relevantNoms li ) ++ "\n" ++ yesno "Past, " ( languagePast li )- ++ yesno "Trans, " ( languageTrans li) where yesno :: String -> Bool -> String yesno s b = ( if b then "" else "no " ) ++ s yesnol s l | null l = "no " ++ s@@ -626,8 +449,7 @@ formulaLanguageInfo f e = LanguageInfo { languageNoms = noms, relevantNoms = relNoms,- languagePast = hasPast f,- languageTrans = hasTransClosure f}+ languagePast = hasPast f} where allNoms_ = nomsOfEncoding e relNoms_ = extractRelevantNominals f@@ -645,8 +467,6 @@ Dis fs -> foldr1 combine $ map g $ list fs Dia _ f -> g f Box _ f -> g f- DiaX _ _ f -> g f- BoxX _ f -> g f At _ f -> g f Down _ f -> g f A f -> g f@@ -663,8 +483,6 @@ Dis fs -> Dis $ Set.map g fs Dia r f -> Dia r (g f) Box r f -> Box r (g f)- DiaX i r f -> DiaX i r (g f)- BoxX r f -> BoxX r (g f) At i f -> At i (g f) A f -> A (g f) E f -> E (g f)@@ -682,14 +500,7 @@ hasPast :: Formula -> Bool hasPast (Dia r _) = testBit r 0 hasPast (Box r _) = testBit r 0-hasPast (BoxX r _) = testBit r 0-hasPast (DiaX _ r _) = testBit r 0 hasPast f = composeFold False (||) hasPast f--hasTransClosure :: Formula -> Bool-hasTransClosure (BoxX _ _) = True-hasTransClosure (DiaX _ _ _) = True-hasTransClosure f = composeFold False (||) hasTransClosure f replaceVar :: Int -> Int -> Formula -> Formula replaceVar v n a@(Lit v2)
src/HTab/Main.hs view
@@ -33,12 +33,11 @@ runWithParams p = time "Total time: " $ do- let fromStdIn = do myPutStrLn $ "Reading from stdin (run again with" ++- "`--help' for usage options)"+ let fromStdIn = do myPutStrLn "Reading from stdin." hSetBuffering stdin LineBuffering getContents - let parse = \i -> if head (words i) == "begin"+ let parse i = if head (words i) == "begin" then F.simpleParse p i else F.parse p i allTasks <- parse <$> maybe fromStdIn readFile (filename p) --@@ -96,7 +95,7 @@ Retrieve -> do let fLang = formulaLanguageInfo theory encoding- let initialBranch = emptyBranch fLang relInfo encoding+ let initialBranch = emptyBranch fLang relInfo encoding p let (noms,encfs) = encodeRetrieveTask relInfo encoding fLang theory fs -- myPutStrLn $ "Instances making true: " ++ show fs@@ -124,7 +123,7 @@ "Relations properties :" ++ showRelInfo relInfo ] -- let fLang = formulaLanguageInfo f encoding- let initialBranch = emptyBranch fLang relInfo encoding+ let initialBranch = emptyBranch fLang relInfo encoding p let branchInfo = addFirstFormulas p initialBranch fLang f -- result <- tableauInit p branchInfo@@ -181,5 +180,5 @@ myPutStrLn :: String -> IO ()-myPutStrLn str = do whenNormal $ putStrLn str+myPutStrLn str = whenNormal $ putStrLn str
src/HTab/ModelGen.hs view
@@ -12,9 +12,11 @@ import qualified HyLo.Signature.String as S -import HTab.Formula( Prefix, Rel, LanguageInfo(..), Encoding, int,+import HTab.Formula( PrFormula(..), Formula(..),+ Prefix, Rel, LanguageInfo(..), Encoding, int, RelInfo, toPropSymbol, toNomSymbol, toRelSymbol, isPositiveProp )-import HTab.Branch( Branch(..), prefixes, getUrfather,+import HTab.Branch( Branch(..), prefixes, getUrfather, BlockingMode(..),+ patternOf, findByPattern, isInTheModel, relationIsInTheModel, getModelRepresentative, isTransitive, isSymmetric ) import qualified HTab.DisjSet as DS@@ -43,9 +45,21 @@ ps = Set.fromList [(S.NomSymbol $ show (pre + bias), pro) | (pre,pro) <- prefixAndProps branch]- rs = Set.fromList $ map (toSimpSig e)- $ map (\(p1,r,p2) -> (getModelRepresentative branch p1 + bias, r, getModelRepresentative branch p2 + bias))- $ filter (relationIsInTheModel branch) $ allRels $ accStr branch+ pbBlocked =+ if blockMode branch `elem` [PatternBlocking,AnywhereBlocking]+ then+ [ (pr, r, pr2) |+ pr <- prefixes branch,+ isInTheModel branch pr,+ blockedDia@(PrFormula _ _ (Dia r _)) <- IntMap.findWithDefault [] pr (blockedDias branch),+ let pat = patternOf branch blockedDia,+ let pr2 = findByPattern branch pat ]+ else []+ rels = (filter (relationIsInTheModel branch) $ allRels $ accStr branch) ++ pbBlocked+ inModel = flip getModelRepresentative+ rs = Set.fromList $ map (toSimpSig e)+ $ map (\(p1,r,p2) -> ((p1 `inModel` branch) + bias , r,(p2 `inModel` branch) + bias))+ rels toSimpSig :: Encoding -> (Prefix,Rel,Prefix) -> (S.NomSymbol,S.RelSymbol,S.NomSymbol) toSimpSig e (p1,r,p2) = (S.NomSymbol (show p1), toRelSymbol e r, S.NomSymbol (show p2))@@ -85,11 +99,11 @@ = case Set.minView todo1 of Nothing -> seen Just (nextWorld,todo2) -> go (Set.insert nextWorld seen) todo2 succs r nextWorld- where todo1 = ((succs r w) `Set.union` todo) `Set.difference` seen+ where todo1 = (succs r w `Set.union` todo) `Set.difference` seen getSymClos :: (Ord w) => Set w -> (r -> w -> Set w) -> r -> w -> Set w getSymClos worlds succs_ r_ w_- = Set.union (succs_ r_ w_) syms+ = succs_ r_ w_ `Set.union` syms where syms = Set.filter (hasAsSuccessor r_ w_) worlds hasAsSuccessor rel world2 world1 = Set.member world2 $ succs_ rel world1
src/HTab/Relations.hs view
@@ -79,12 +79,11 @@ prettyShowMap_ :: (Show y) => IntMap y -> (y -> String) -> String -> String prettyShowMap_ dasMap valueShow separator- = concat $ List.intersperse separator $ map (\(k,v) -> show k ++ " -> " ++ valueShow v)+ = List.intercalate separator $ map (\(k,v) -> show k ++ " -> " ++ valueShow v) $ IntMap.toList dasMap prettyShowMap_rel_bps_x :: (Show a) => IntMap {- Rel -} [(a,DependencySet)] -> String prettyShowMap_rel_bps_x dasMap- = concat $ List.intersperse ", " $ map (\(r,x_bp_s) -> (++) ("-" ++ show r ++ "-> ") $ concat $ List.intersperse ", "- $ map (\(x,bp) -> show x ++ " " ++ dsShow bp) x_bp_s- )+ = List.intercalate ", " $ map (\(r,x_bp_s) -> (++) ("-" ++ show r ++ "-> ") $ List.intercalate ", "+ $ map (\(x,bp) -> show x ++ " " ++ dsShow bp) x_bp_s ) $ IntMap.toList dasMap
src/HTab/RuleId.hs view
@@ -47,7 +47,6 @@ | R_Discard -- Discarding a formula | R_DiscardDown | R_DiscardDiaDone- | R_DiscardDiaDone2 | R_DiscardDiaBlocked | R_DiscardDiaX | R_DiscardDisjTrivial
src/HTab/Rules.hs view
@@ -1,191 +1,59 @@ module HTab.Rules (-Rule(..),BranchModification(..),-applicableRule, applyRule, ruleToId,-applyMod+Rule(..),+applicableRule, applyRule, ruleToId ) where import qualified Data.Set as Set import qualified Data.Map as Map-import qualified Data.IntMap as IntMap-import Data.Maybe ( listToMaybe, mapMaybe )+import Data.Maybe ( mapMaybe ) import HTab.Formula( Formula(..), PrFormula(..), showLess, neg, Dependency, DependencySet, dsUnion, dsInsert,- prefix, AccFormula(..), Rel,+ prefix, Rel, negPr, Prefix,- conj, replaceVar, Prop, Literal )-import HTab.Branch( Branch(..), createNewPref, createNewProp, createNewNomTestRelevance,- BranchInfo(..),+ replaceVar, Literal )+import HTab.Branch( Branch(..), BranchInfo(..), TodoList(..), BlockingMode(..),+ -- for rules+ createNewPref, createNewProp, createNewNomTestRelevance, addFormulas, addAccFormula,- addDiaRuleCheck, addDiaXRuleCheck,+ addDiaRuleCheck, addToBlockedDias, addDownRuleCheck, addDiffRuleCheck,- addParentPrefix,- reduceDisjunctionProposeLazy, doLazyBranching,- getUrfatherAndDeps, isNotBlocked, merge,- diaAlreadyDone, diaXAlreadyDone, downAlreadyDone,- ReducedDisjunct(..), getUrfather,- TodoList(..),- deleteUEV, insertUEV_addFormula )-import HTab.CommandLine(Params, UnitProp(..), lazyBranching, semBranch, unitProp, strategy, noLoopCheck)+ addParentPrefix, doLazyBranching,+ getUrfatherAndDeps, merge,+ -- for choosing rule in todo list+ isNotBlocked,+ diaAlreadyDone, downAlreadyDone,+ -- for rules and choosing rule in todo list+ reduceDisjunctionProposeLazy, getUrfather,+ ReducedDisjunct(..)+ )+import HTab.CommandLine(Params, UnitProp(..), lazyBranching, semBranch, unitProp, strategy) import HTab.RuleId(RuleId(..)) import qualified HTab.DisjSet as DS --- a "rule" is basically a list of modifications of the structures--data BranchModification = BM_AddFormulas [PrFormula]- | BM_AddAccFormula AccFormula- | BM_AddDiaRuleCheck Prefix (Rel,Formula)- | BM_AddDiaXRuleCheck Prefix (Rel,Formula)- | BM_AddDownRuleCheck Prefix Formula- | BM_AddDiffRuleCheck Formula (Maybe Prop)- | BM_CreateNewPref- | BM_CreateNewProp- | BM_CreateNewNomTestRelevance Formula- | BM_AddParentPrefix Prefix Prefix- | BM_Clash DependencySet PrFormula- | BM_DeleteUEV Int- | BM_InsertUEV_addFormula (Maybe Int) DependencySet (Int -> PrFormula)- | BM_Merge Prefix DS.Pointer DependencySet- | BM_DoLazyBranch Prefix Literal [PrFormula]+-- rule constructors contain the data needed to modify a branch --- each rule constructor contains exactly the needed data to know the effect of the rule-data Rule = DiaRule PrFormula -- creates a prefix- | DiaXRule PrFormula Dependency+data Rule = DiaRule PrFormula -- creates a prefix | DisjRule PrFormula [PrFormula]- | SemBrRule PrFormula [[PrFormula]]+ | SemBrRule PrFormula [PrFormula] | LazyBranchRule PrFormula Prefix Literal [PrFormula] | AtRule PrFormula | DownRule PrFormula- | DiffRule PrFormula Dependency+ | DiffRule PrFormula Dependency -- creates a prefix | ExistRule PrFormula -- creates a prefix | 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 --- from the description of a rule application, creates the list of lists of modifications to the branch--- for certain rules, we need to look in the branch to see what modifications we do -getMods :: Branch -> Rule -> [[BranchModification]]-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 (DiscardDiaDone2Rule df)- else [[BM_AddParentPrefix newPr ur,- BM_AddAccFormula acctoadd,- BM_AddFormulas [toadd],- BM_AddDiaRuleCheck pr (r,f),- BM_CreateNewPref]]- where acctoadd = AccFormula (dsUnion ds ds2) r ur newPr- toadd = PrFormula newPr ds f- newPr = getNewPref br- (ur,ds2,_) = getUrfatherAndDeps br (DS.Prefix pr)--getMods _ (DiaRule _) = error "getMods DiaRule"--getMods _ (DiaXRule (PrFormula pr ds (DiaX mi r ev)) dep)=- [[BM_AddFormulas [PrFormula pr ds2 ev],- BM_AddDiaXRuleCheck pr (r,ev)]- ++ case mi of { Nothing -> [] ;- Just idx -> [BM_DeleteUEV idx]- }- ,- [BM_AddDiaXRuleCheck pr (r,ev),- BM_InsertUEV_addFormula mi ds2- (\i -> PrFormula pr ds2 ((neg ev) `conj` (Dia r $ DiaX (Just i) r ev)))]- ]- where ds2 = dsInsert dep ds--getMods _ (DiaXRule _ _)= error "getMods DiaXRule"--getMods br (ExistRule (PrFormula _ ds (E f2))) =- [[BM_AddFormulas [toadd],- BM_CreateNewPref]]- where toadd = PrFormula newPr ds f2- newPr = getNewPref br--getMods _ (ExistRule _) = error "getMods ExistRule"--getMods _ (DisjRule _ toadds) =- [[BM_AddFormulas [toadd]] | toadd <- toadds]--getMods _ (SemBrRule _ toaddss) =- [[BM_AddFormulas toadds] | toadds <- toaddss]--getMods _ (LazyBranchRule _ pr lit pfs) =- [[BM_DoLazyBranch pr lit pfs]]--getMods br (AtRule (PrFormula _ ds (At n f))) =- [[BM_AddFormulas [toadd]]]- where toadd = PrFormula earliestPrefix (dsUnion ds ds2) f- (earliestPrefix,ds2,_) = getUrfatherAndDeps br (DS.Nominal n)--getMods _ (AtRule _) = error "getMods AtRules"---getMods br (DownRule df@(PrFormula pr ds f@(Down v f2)))- = if downAlreadyDone br 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- ]]- where toadd1 = PrFormula pr ds (replaceVar v newNom f2)- toadd2 = PrFormula pr ds $ Lit newNom- newNom = nextNom br--getMods _ (DownRule _) = error "getMods DownRule"--getMods br (DiffRule (PrFormula pr ds_ (D f2)) d) =- case Map.lookup f2 (dDiaRlCh br) of- Nothing -> [[BM_AddDiffRuleCheck f2 Nothing,- BM_CreateNewPref, BM_CreateNewPref,- BM_CreateNewProp,- BM_AddFormulas [PrFormula newPref1 ds f2,- PrFormula newPref2 ds f2,- PrFormula newPref1 ds ( Lit newProp),- PrFormula newPref2 ds (neg $ Lit newProp),- PrFormula pr ds (neg $ Lit newProp)]- ],- [BM_AddDiffRuleCheck f2 (Just newProp),- BM_CreateNewPref,- BM_CreateNewProp,- BM_AddFormulas [PrFormula newPref1 ds f2,- PrFormula newPref1 ds ( Lit newProp),- PrFormula pr ds (neg $ Lit newProp)]- ]- ]- where newPref1 = getNewPref br- newPref2 = newPref1 + 1- newProp = nextProp br- Just Nothing -> [[]]- Just (Just diffProp) -> [[BM_AddFormulas [PrFormula pr ds (neg $ Lit diffProp)]]]- where ds = d `dsInsert` ds_--getMods _ (DiffRule _ _) = error "getMods DiffRule"--getMods _ (DiscardDownRule _) = [[]]-getMods _ (DiscardDiaDoneRule _) = [[]]-getMods _ (DiscardDiaDone2Rule _) = [[]]-getMods _ (DiscardDiaBlockedRule _) = [[]]-getMods _ (DiscardDiaXRule _) = [[]]-getMods _ (DiscardDisjTrivialRule _) = [[]]-- 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@@ -195,9 +63,7 @@ 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 show (ClashDisjRule bprs f) = "Clash: " ++ show bprs ++ " " ++ show f@@ -210,7 +76,6 @@ ruleToId r = case r of (MergeRule _ _ _) -> R_Merge (DiaRule _ ) -> R_Dia- (DiaXRule _ _) -> R_DiaX (DisjRule _ _) -> R_Disj (SemBrRule _ _) -> R_SemBr (AtRule _ ) -> R_At@@ -219,9 +84,7 @@ (DiffRule _ _) -> R_Diff (DiscardDownRule _) -> R_DiscardDown (DiscardDiaDoneRule _) -> R_DiscardDiaDone- (DiscardDiaDone2Rule _) -> R_DiscardDiaDone2 (DiscardDiaBlockedRule _) -> R_DiscardDiaBlocked- (DiscardDiaXRule _) -> R_DiscardDiaX (DiscardDisjTrivialRule _) -> R_DiscardDisjTrivial (ClashDisjRule _ _) -> R_ClashDisj (RoleIncRule _ _ _ _) -> R_RoleInc@@ -229,16 +92,18 @@ -- the rules application strategy is defined here: -- the first rule is the one that will be applied at the next tableau step-applicableRule :: Branch -> Params -> Dependency -> Maybe (Rule,TodoList,Branch)-applicableRule br p d = listToMaybe $ mapMaybe (ruleByChar br p d) (strategy p)+applicableRule :: Branch -> Params -> Dependency -> Maybe (Rule,Branch)+applicableRule br p d =+ case mapMaybe (ruleByChar br p d) (strategy p) of+ [] -> Nothing+ ((rule,newtodo):_) -> Just (rule,br{todoList = newtodo}) -ruleByChar :: Branch -> Params -> Dependency -> Char -> Maybe (Rule,TodoList,Branch)+ruleByChar :: Branch -> Params -> Dependency -> Char -> Maybe (Rule,TodoList) ruleByChar br p d char = case char of 'n' -> applicableMergeRule '|' -> applicableDisjRule '<' -> applicableDiaRule- '*' -> applicableDiaXRule '@' -> applicableAtRule 'E' -> applicableExistRule 'D' -> applicableDiffRule@@ -249,57 +114,38 @@ todos = todoList br applicableDiaRule- = do (f@(PrFormula pr _ _),new) <- Set.minView $ diaTodo todos- if noLoopCheck p- then return (DiaRule f, todos{diaTodo = new},br)- else if diaAlreadyDone br f- 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)- brBlocked = br{blockedDias = IntMap.insertWith (++) ur [f] (blockedDias br)}- -- blocked formulas are added one by one to the blockedDias list.- -- a better way would be to put every formula of a given blocked prefix- -- to that list, but as we do not index todo formulas by prefix we can- -- not do it.- in- return ( DiscardDiaBlockedRule f, todos{diaTodo = new}, brBlocked)-- applicableDiaXRule = do (f,new) <- Set.minView $ diaXTodo todos- return (diaXRule f br d, todos{diaXTodo = new},br)-+ = do (f,new) <- Set.minView $ diaTodo todos+ if diaAlreadyDone br f+ then return ( DiscardDiaDoneRule f, todos{diaTodo = new})+ else if isNotBlocked br f+ then return ( DiaRule f, todos{diaTodo = new})+ else return ( DiscardDiaBlockedRule f, todos{diaTodo = new}) applicableAtRule = do (f,new) <- Set.minView $ atTodo todos- return (AtRule f, todos{atTodo = new},br)-+ return (AtRule f, todos{atTodo = new}) applicableDownRule = do (f,new) <- Set.minView $ downTodo todos- return (DownRule f, todos{downTodo = new},br)-+ if downAlreadyDone br f+ then return (DiscardDownRule f, todos{downTodo = new})+ else return (DownRule f, todos{downTodo = new}) applicableExistRule = do (f,new) <- Set.minView $ existTodo todos- return (ExistRule f, todos{existTodo = new},br)-+ return (ExistRule f, todos{existTodo = new}) applicableDiffRule = do (f,new) <- Set.minView $ diffTodo todos- return (DiffRule f d, todos{diffTodo = new},br)-+ return (DiffRule f d, todos{diffTodo = new}) applicableRoleIncRule = do ((ds, p1, p2, rs),new) <- Set.minView $ roleIncTodo todos- return (RoleIncRule p1 rs p2 (dsInsert d ds), todos{roleIncTodo = new},br)-+ return (RoleIncRule p1 rs p2 (dsInsert d ds), todos{roleIncTodo = new}) applicableMergeRule = do ((ds,pr,po),new) <- Set.minView $ mergeTodo todos- return (MergeRule pr po ds, todos{mergeTodo = new},br)-+ return (MergeRule pr po ds, todos{mergeTodo = new}) applicableDisjRule = case unitProp p of Eager -> {- scan all disjuncts until one can be discarded, reduced to one disjunct or clashes -}- 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+ case mapMaybe (makeInteresting p br d) $ Set.toList $ disjTodo todos of+ ((r,pf):_) -> return (r, todos{disjTodo = Set.delete pf $ disjTodo todos})+ [] -> regularApplicableDisjRule+ -- todo: update counter (CurCount, MaxCount) step 10+ -- to space out unit propagation lookup _ -> regularApplicableDisjRule- regularApplicableDisjRule- = if semBranch p- then do (f,new) <- Set.minView $ disjTodo todos- return (semBrRule p f br d, todos{disjTodo = new},br)- else do (f,new) <- Set.minView $ disjTodo todos- return (disjRule p f br d, todos{disjTodo = new},br)+ = do (f,new) <- Set.minView $ disjTodo todos+ return (disjRule p f br d, todos{disjTodo = new}) makeInteresting :: Params -> Branch -> Dependency -> PrFormula -> Maybe (Rule,PrFormula) makeInteresting p br d df@(PrFormula pr ds (Dis fs))@@ -308,10 +154,10 @@ 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 p && ur <= unblockedPrefsLim br- -> case mProposed of- Nothing -> Nothing- Just lit -> Just (LazyBranchRule df ur lit [PrFormula ur newDeps (Dis disjuncts)], df)+ | lazyBranching p && blockMode br /= ChainTwinBlocking+ -> case mProposed of+ Nothing -> Nothing+ Just lit -> Just (LazyBranchRule df ur lit [PrFormula ur newDeps (Dis disjuncts)], df) | otherwise -> Nothing where newDeps = dsInsert d $ dsUnion ds new_ds ur = getUrfather br (DS.Prefix pr)@@ -321,83 +167,94 @@ makeInteresting _ _ _ _ = error "makeInteresting on a non disjunction" -applyRule :: Params -> Rule -> Branch -> TodoList -> [BranchInfo]-applyRule p rule br_ todo- = map (applyMods p br) (getMods br rule)- where br = br_{todoList = todo} -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+(>>?) :: BranchInfo -> (Branch -> BranchInfo) -> BranchInfo+clash@(BranchClash _ _ _ _) >>? _ = clash+(BranchOK br) >>? f = f br +applyRule :: Params -> Rule -> Branch -> [BranchInfo]+applyRule p rule br+ = case rule of+ DiaRule (PrFormula pr ds (Dia r f))+ -> [ addParentPrefix newPr ur br >>?+ addAccFormula p (dsUnion ds ds2, r, ur, newPr) >>?+ addFormulas p [PrFormula newPr ds f] >>?+ addDiaRuleCheck pr (r,f) newPr >>?+ createNewPref p ]+ where newPr = getNewPref br+ (ur,ds2,_) = getUrfatherAndDeps br (DS.Prefix pr)+ DisjRule _ prFormulas ->+ [ addFormulas p [toadd] br | toadd <- prFormulas ]+ SemBrRule _ prFormulas ->+ [ addFormulas p toadds br | toadds <- go prFormulas [] ]+ where go (hd:tl) negs = (hd:negs):(go tl (negPr hd:negs))+ go [] _ = []+ LazyBranchRule _ pr lit prFormulas ->+ [ doLazyBranching pr lit prFormulas br ]+ AtRule (PrFormula _ ds (At n f)) ->+ [ addFormulas p [toadd] br{ nomPrefClasses = equiv }]+ where (ur,ds2,equiv) = getUrfatherAndDeps br (DS.Nominal n)+ toadd = PrFormula ur (dsUnion ds ds2) f+ DownRule (PrFormula pr ds f@(Down v f2)) ->+ [ createNewNomTestRelevance f br >>?+ addFormulas p [toadd1, toadd2] >>?+ addDownRuleCheck pr f ]+ where toadd1 = PrFormula pr ds (replaceVar v newNom f2)+ toadd2 = PrFormula pr ds $ Lit newNom+ newNom = nextNom br+ DiffRule (PrFormula pr ds_ (D f2)) d ->+ case Map.lookup f2 (dDiaRlCh br) of+ Nothing -> [ addDiffRuleCheck f2 Nothing br >>?+ createNewPref p >>?+ createNewPref p >>?+ createNewProp >>?+ addFormulas p [ PrFormula newPref1 ds f2,+ PrFormula newPref2 ds f2,+ PrFormula newPref1 ds ( Lit newProp),+ PrFormula newPref2 ds (neg $ Lit newProp) ]+ ,+ addDiffRuleCheck f2 (Just newProp) br >>?+ createNewPref p >>?+ createNewProp >>?+ addFormulas p [ PrFormula newPref1 ds f2,+ PrFormula newPref1 ds ( Lit newProp),+ PrFormula pr ds (neg $ Lit newProp) ]+ ]+ where newPref1 = getNewPref br+ newPref2 = newPref1 + 1+ newProp = nextProp br+ Just (Just diffProp) -> [addFormulas p [PrFormula pr ds (neg $ Lit diffProp)] br]+ Just Nothing -> [BranchOK br]+ where ds = d `dsInsert` ds_+ ExistRule (PrFormula _ ds (E f2)) ->+ [addFormulas p [toadd] br >>? createNewPref p] -- this createNewPref / getNewPref thing needs to stop+ where toadd = PrFormula newPr ds f2+ newPr = getNewPref br+ DiscardDownRule _ -> [BranchOK br]+ DiscardDiaDoneRule _ -> [BranchOK br]+ DiscardDisjTrivialRule _ -> [BranchOK br]+ DiscardDiaBlockedRule f -> [addToBlockedDias f 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+ ClashDisjRule ds (PrFormula pr ds2 f) -> [BranchClash br pr (dsUnion ds ds2) f]+ MergeRule pr po ds -> [merge p pr ds po br]+ RoleIncRule p1 rs p2 ds ->+ [addAccFormula p (ds, r, p1, p2) br | r <- rs]+ _ -> error $ "applyRule with bad argument: " ++ show rule --- 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 DiscardDiaXRule f- else DiaXRule f d -diaXRule _ _ _ = error "diaXRule"----- getNewPref :: Branch -> Prefix getNewPref br = lastPref br + 1 --- disjunction 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+ then rule df $ prefix pr (dsInsert d ds) fs else case reduceDisjunctionProposeLazy br pr fs of 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)+ -> rule df (prefix pr (dsInsert d $ dsUnion ds new_ds) disjuncts)+ where rule = if semBranch p then SemBrRule else DisjRule -- todo: if only one conjunct remaining, do not add d , but still create a DisjRule disjRule _ _ _ _ = error "disjRule"---- semantic branching-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 -> 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-semBrRule _ _ _ _ = error "sembrRule"---sbModList :: [PrFormula] -> [[PrFormula]]-sbModList fs = go fs []- where go :: [PrFormula] -> [PrFormula] -> [[PrFormula]]- go (hd:tl) negated = - (hd:negated):(go tl ((neg_ hd):negated))- where neg_ (PrFormula pr ds f) = PrFormula pr ds (neg f)- go [] _ = []
src/HTab/Statistics.hs view
@@ -1,11 +1,3 @@-------------------------------------------------------- ----- Statistics.hs: ----- Functions that collect and print out ----- statistics ----- -------------------------------------------------------- {- Copyright (C) HyLoRes 2002-2006 Carlos Areces - areces@loria.fr - http://www.loria.fr/~areces@@ -66,7 +58,7 @@ updateMetrics :: (Metric -> Metric) -> Statistics -> Statistics updateMetrics f stat = let s = stat{metrics = map (f $!) (metrics stat)} in- (rnf s) `seq` s+ rnf s `seq` s updateStep :: Statistics -> Statistics updateStep s@(Stat _ _ 0) = s
src/HTab/Tableau.hs view
@@ -6,7 +6,7 @@ import Control.Monad.State(StateT,lift,modify) import HTab.Statistics(Statistics,updateStep,printOutMetrics,recordClosedBranch, recordFiredRule)-import HTab.Branch(BranchInfo(..), unfulfilledEventualities)+import HTab.Branch(BranchInfo(..)) import HTab.CommandLine(backjumping,Params,configureStats) import HTab.Rules(applyRule,applicableRule,ruleToId) import HTab.Formula(DependencySet,dsEmpty,dsMember,dsUnion)@@ -24,24 +24,22 @@ do let verbose = lift . whenLoud . putStrLn printOutMetrics modify updateStep- verbose (">> Depth " ++ show depth)+ verbose $ ">> Depth " ++ show depth case branchInfo of BranchClash br pr bprs f ->- do verbose (show br ++ "Clasher : " ++ show (pr,bprs,depth,f))+ do verbose $ show br ++ "Clasher : " ++ show (pr,bprs,depth,f) recordClosedBranch return $ CLOSED bprs BranchOK br -> do verbose (show br) case applicableRule br p (depth + 1) of Nothing ->- 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 verbose (">> Rule : " ++ show rule)+ do verbose ">> Saturated open branch"+ return $ OPEN $ buildModel br+ Just (rule,newBranch) ->+ do verbose $ ">> Rule : " ++ show rule recordFiredRule $ ruleToId rule- case applyRule p rule newBranch newTodo of+ case applyRule p rule newBranch of [newBi] -> tableauDown p (depth + 1) newBi bis -> tableauRight p (depth + 1) bis dsEmpty
src/htab.hs view
@@ -40,19 +40,19 @@ runCmdLineVersion :: IO (Maybe (Maybe TaskRunFlag)) runCmdLineVersion =- do clp <- cmdArgs $ defaultParams &= summary header &= details gpl_tag+ do clp <- cmdArgs_ $ defaultParams += summary header += details gplTag clpOK <- checkParams clp if clpOK then Just <$> runWithParams clp else return Nothing header :: String-header = unlines ["HTab 1.5.6",+header = unlines ["HTab 1.6.0", "G. Hoffmann, C. Areces, D.Gorin and J. Heguiabehere. (c) 2002-2011.", "http://code.google.com/p/intohylo/"] -gpl_tag :: [String]-gpl_tag = [+gplTag :: [String]+gplTag = [ "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",