diff --git a/HTab.cabal b/HTab.cabal --- a/HTab.cabal +++ b/HTab.cabal @@ -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 diff --git a/NEWS b/NEWS --- a/NEWS +++ b/NEWS @@ -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 diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/Setup.lhs b/Setup.lhs deleted file mode 100644 --- a/Setup.lhs +++ /dev/null @@ -1,4 +0,0 @@ -#! /usr/bin/env runhaskell - -> import Distribution.Simple -> main = defaultMain diff --git a/examples/unsat/fun_inj1.frm b/examples/unsat/fun_inj1.frm deleted file mode 100644 --- a/examples/unsat/fun_inj1.frm +++ /dev/null @@ -1,13 +0,0 @@ -signature { -propositions { p } -nominals { n,m } -relations { r : { functional } } -} - -theory - -{ - n:p; - m:!p; - n:m -} diff --git a/examples/unsat/fun_inj2.frm b/examples/unsat/fun_inj2.frm deleted file mode 100644 --- a/examples/unsat/fun_inj2.frm +++ /dev/null @@ -1,14 +0,0 @@ -signature { -propositions { p } -nominals { n,a,b } -relations { r, - s : { inverseof r, functional } } -} - -theory - -{ - a:n; - b:n; - a:!b -} diff --git a/examples/unsat/symmetry1.frm b/examples/unsat/symmetry1.frm --- a/examples/unsat/symmetry1.frm +++ b/examples/unsat/symmetry1.frm @@ -1,14 +1,14 @@ signature { propositions { p } nominals { n,m } -relations { s : {symmetric}, t : {trclosureof s} } +relations { s : {symmetric} } } theory { - n:m; + n:m; n:p; - m:[t]!p + m:[s][s][s]!p } diff --git a/examples/unsat/test39.frm b/examples/unsat/test39.frm deleted file mode 100644 --- a/examples/unsat/test39.frm +++ /dev/null @@ -1,15 +0,0 @@ -signature { - -propositions { p } -nominals { n} -relations { r : {functional}, - s : {inverseof r} } - -} - -theory -{ - -E (p & n) & E (!p & n) - -} diff --git a/examples/unsat/test40.frm b/examples/unsat/test40.frm deleted file mode 100644 --- a/examples/unsat/test40.frm +++ /dev/null @@ -1,14 +0,0 @@ -signature { - -propositions { p } -nominals { n} -relations { r : {functional} } - -} - -theory -{ - -n:( p & n:!p) - -} diff --git a/src/HTab/Branch.hs b/src/HTab/Branch.hs --- a/src/HTab/Branch.hs +++ b/src/HTab/Branch.hs @@ -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 ] + +-- 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: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, diff --git a/src/HTab/CommandLine.hs b/src/HTab/CommandLine.hs --- a/src/HTab/CommandLine.hs +++ b/src/HTab/CommandLine.hs @@ -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 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 diff --git a/src/HTab/Formula.hs b/src/HTab/Formula.hs --- a/src/HTab/Formula.hs +++ b/src/HTab/Formula.hs @@ -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) diff --git a/src/HTab/Main.hs b/src/HTab/Main.hs --- a/src/HTab/Main.hs +++ b/src/HTab/Main.hs @@ -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 diff --git a/src/HTab/ModelGen.hs b/src/HTab/ModelGen.hs --- a/src/HTab/ModelGen.hs +++ b/src/HTab/ModelGen.hs @@ -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 diff --git a/src/HTab/Relations.hs b/src/HTab/Relations.hs --- a/src/HTab/Relations.hs +++ b/src/HTab/Relations.hs @@ -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 diff --git a/src/HTab/RuleId.hs b/src/HTab/RuleId.hs --- a/src/HTab/RuleId.hs +++ b/src/HTab/RuleId.hs @@ -47,7 +47,6 @@ | R_Discard -- Discarding a formula | R_DiscardDown | R_DiscardDiaDone - | R_DiscardDiaDone2 | R_DiscardDiaBlocked | R_DiscardDiaX | R_DiscardDisjTrivial diff --git a/src/HTab/Rules.hs b/src/HTab/Rules.hs --- a/src/HTab/Rules.hs +++ b/src/HTab/Rules.hs @@ -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 [] _ = [] diff --git a/src/HTab/Statistics.hs b/src/HTab/Statistics.hs --- a/src/HTab/Statistics.hs +++ b/src/HTab/Statistics.hs @@ -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 diff --git a/src/HTab/Tableau.hs b/src/HTab/Tableau.hs --- a/src/HTab/Tableau.hs +++ b/src/HTab/Tableau.hs @@ -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 diff --git a/src/htab.hs b/src/htab.hs --- a/src/htab.hs +++ b/src/htab.hs @@ -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",