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