HTab 1.7.2 → 1.7.3
raw patch · 44 files changed
+96/−1175 lines, 44 files
Files
- HTab.cabal +1/−3
- NEWS +3/−0
- examples/sat/down01.frm +0/−3
- examples/sat/spy.frm +0/−5
- examples/unsat/test35.frm +0/−3
- examples/unsat/test36.frm +0/−3
- examples/unsat/test37.frm +0/−9
- examples/unsat/test38.frm +0/−4
- rc/br_infinite.frm +0/−18
- rc/br_no_tree.frm +0/−12
- rc/br_unsat_bad_infinite.frm +0/−14
- rc/gbr_no_tree.frm +0/−12
- rc/gsab_confluence.frm +0/−14
- rc/gsab_count.frm +0/−13
- rc/gsab_infinite.frm +0/−20
- rc/gsab_no_tree.frm +0/−12
- rc/gswap_infinite.frm +0/−25
- rc/gswap_no_tree.frm +0/−12
- rc/mem_br_struct.frm +0/−22
- rc/mem_br_struct_refl.frm +0/−18
- rc/mem_sab_struct.frm +0/−25
- rc/mem_sab_struct2.frm +0/−25
- rc/mem_sab_struct3.frm +0/−25
- rc/mem_sab_struct_refl.frm +0/−26
- rc/mem_sw_struct.frm +0/−28
- rc/mem_sw_struct_refl.frm +0/−24
- rc/sab_loop.frm +0/−14
- rc/sab_loop_diamond.frm +0/−17
- rc/sab_no_tree.frm +0/−12
- rc/sab_sat_01.frm +0/−13
- rc/swap_diamond.frm +0/−15
- rc/swap_infinite.frm +0/−25
- rc/swap_no_tree.frm +0/−15
- src/HTab/Branch.hs +4/−37
- src/HTab/CommandLine.hs +4/−16
- src/HTab/Formula.hs +3/−211
- src/HTab/Literals.hs +1/−8
- src/HTab/Main.hs +25/−61
- src/HTab/Memory.hs +0/−232
- src/HTab/RuleId.hs +0/−2
- src/HTab/Rules.hs +38/−100
- src/HTab/Statistics.hs +10/−13
- src/HTab/Tableau.hs +6/−8
- src/htab.hs +1/−1
HTab.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.4 Name: HTab-Version: 1.7.2+Version: 1.7.3 Synopsis: Tableau based theorem prover for hybrid logics Description: Tableau based theorem prover for hybrid logics Homepage: http://hub.darcs.net/gh/htab@@ -17,7 +17,6 @@ examples/*.sh examples/sat/*.frm examples/unsat/*.frm- rc/*.frm source-repository head type: darcs location: http://hub.darcs.net/gh/htab@@ -32,7 +31,6 @@ HTab.Formula HTab.Literals HTab.Main- HTab.Memory HTab.ModelGen HTab.Relations HTab.RuleId
NEWS view
@@ -1,3 +1,6 @@+* 2020.05.15 : 1.7.3+ o remove dynamic logics support, these were branched to HTabDyn and HTabDown+ o remove randomization * 2019.04.25 : 1.7.2 o --memory flag to run memory logic testsuite o compile with GHC 8.6
− examples/sat/down01.frm
@@ -1,3 +0,0 @@-begin-N2 & <>( down N3 . ( N1:(N2 & !N3)))-end
− examples/sat/spy.frm
@@ -1,5 +0,0 @@-begin-down (N1 []([]( down( N2 (N1:<>(N2))))));-[]<>true;-[] (down (N1 (!<>N1)))-end
− examples/unsat/test35.frm
@@ -1,3 +0,0 @@-begin-down(N1 !N1)-end
− examples/unsat/test36.frm
@@ -1,3 +0,0 @@-begin-!((down (N1 dia (N1 ^ p1) )) --> p1)-end
− examples/unsat/test37.frm
@@ -1,9 +0,0 @@-begin-n3:[R3](down (N1 [R1]([R1]( down( N2 (N1:<R1>N2)))))) ;-n3:<R3>n1;-n3:<R3>n2;-n3:<R3>n3;-n1:<R1>n2;-n2:<R1>n3;-n1:!<R1>n3-end
− examples/unsat/test38.frm
@@ -1,4 +0,0 @@-begin-p1 v <><><><>p1 v down(N1 <>(N1:[]p1));-A !p1-end
− rc/br_infinite.frm
@@ -1,18 +0,0 @@-signature {-propositions { s }-nominals { }-relations { br, gbr }-}--theory--{- s;- [] false;- [br](s --> [br]!s);- [br](!s --> [] !s);- <br><br> true;- [br]<> true;- [br][br](s --> [](!s --> [][]!s));- [br][][][br](s --> <>( !s & <><>s ));-}
− rc/br_no_tree.frm
@@ -1,12 +0,0 @@-signature {-propositions { p }-nominals { }-relations { br }-}--theory--{- [] false;- <br>[] false;-}
− rc/br_unsat_bad_infinite.frm
@@ -1,14 +0,0 @@-signature {-propositions { s }-nominals { }-relations { br, gbr }-}--theory--{- s;- [] false;- [br](s --> [br]!s);- [br][]!s;-}
− rc/gbr_no_tree.frm
@@ -1,12 +0,0 @@-signature {-propositions { p }-nominals { }-relations { sw }-}--theory--{- [] false;- <gbr>[] false;-}
− rc/gsab_confluence.frm
@@ -1,14 +0,0 @@-signature {-propositions { a, b, c }-nominals { }-relations { gsb }-}--theory--{- <>(a & !b & <><>a );- <>(b & !a & <><>b );- [][](c & []!c);- <gsb>[][][] false;-}
− rc/gsab_count.frm
@@ -1,13 +0,0 @@-signature {-propositions { }-nominals { }-relations { gsb }-}--theory--{- <gsb><gsb><gsb> true;- [gsb][gsb][gsb][gsb]false;-}-
− rc/gsab_infinite.frm
@@ -1,20 +0,0 @@-signature {-propositions { s }-nominals { }-relations { sb, gsb }-}--theory--{- s;- []!s;- <> true;- []( <>s & <gsb>!<>s );- []<>!s;- [][]( !s --> ( <>s & <gsb>!<>s) );- [gsb]( (<>(<>s & <>(!s & !<>s)) ) --> <>!<>s);- [gsb][]( (!<>s) --> []<>s );- [gsb](!<>( (!<>s) & <><>( !s & (<>s) & <>!<>s)));- [gsb][gsb]( (<>((!<>s) & <><>(!s & !<>s))) --> <>(!<>s & <>!<>s));-}
− rc/gsab_no_tree.frm
@@ -1,12 +0,0 @@-signature {-propositions { }-nominals { }-relations { gsb }-}--theory--{- <><> true;- [gsb][] false;-}
− rc/gswap_infinite.frm
@@ -1,25 +0,0 @@-signature {-propositions { s }-nominals { }-relations { gsw }-}--theory--{- s;- []!s;- [][]!s;- [][][]!s;- [][][][]!s;- [][][][][]!s;- [][][][][][]!s;- [][][][][][][]!s;- [][][][][][][][]!s;- [][][][][][][][][]!s;- <> true;- []<> true;- [][][gsw][gsw][][](s --> <><><>s);- [][gsw](<>s -> [][]!s);- [][][][gsw][gsw][gsw]((<><><>s) --> <><><>(!s & <><><>s));-}
− rc/gswap_no_tree.frm
@@ -1,12 +0,0 @@-signature {-propositions { }-nominals { }-relations { gsw }-}--theory--{- []false;- <gsw><> true;-}
− rc/mem_br_struct.frm
@@ -1,22 +0,0 @@-signature {-propositions { s, t, a, b, c, d }-nominals { }-relations { br }-}--theory--{- s;- []false;- [br](s --> [br]!s);- [br](!s --> []!s);-- <br>(!s & t & <br>( !s & !t &- a & !b & !c & !d &- <>(!s & !a & b & !c & !d &- <>(!s & !a & !b & c & !d &- <>(!s & !a & !b & !c & d- )))));--}
− rc/mem_br_struct_refl.frm
@@ -1,18 +0,0 @@-signature {-propositions { s, t }-nominals { }-relations { br }-}--theory--{- s;- []false;- [br](s --> [br]!s);- [br](!s --> []!s);-- <br>(!s & t & <br>( !s & !t &- <br>(s & <br>( (<>s) & <>(!s & <>s)))- ));-}
− rc/mem_sab_struct.frm
@@ -1,25 +0,0 @@-signature {-propositions { s, a, b, c }-nominals { }-relations { sb }-}--theory--{- s;- []!s;-- []<>s;- [sb][sb](s --> []<>s);- [][sb](s --> <>[]!s);-- [][](!s --> <>s);- [][][](s --> []<>s);- [][][sb]( s --> <>[]!s);-- [][sb](s --> [sb]( ([]!s) --> [][](s --> []<>s)));- [][sb](s --> [](([]!s) --> [][](s --> <>[]!s)));-- <>(a & !b & !c & <>(!s & !a & b & !c & <>(!s & !a & !b & c )));-}
− rc/mem_sab_struct2.frm
@@ -1,25 +0,0 @@-signature {-propositions { s, a, b, c, d }-nominals { }-relations { sb }-}--theory--{- s;- []!s;-- []<>s;- [sb][sb](s --> []<>s);- [][sb](s --> <>[]!s);-- [][](!s --> <>s);- [][][](s --> []<>s);- [][][sb]( s --> <>[]!s);-- [][sb](s --> [sb]( ([]!s) --> [][](s --> []<>s)));- [][sb](s --> [](([]!s) --> [][](s --> <>[]!s)));-- <>(a & !b & !c & !d & <>(!s & !a & b & !c & !d & <>(!s & !a & !b & c & !d & <> (!s & !a & !b & !c & d))));-}
− rc/mem_sab_struct3.frm
@@ -1,25 +0,0 @@-signature {-propositions { s, a, b, c, d, e }-nominals { }-relations { sb }-}--theory--{- s;- []!s;-- []<>s;- [sb][sb](s --> []<>s);- [][sb](s --> <>[]!s);-- [][](!s --> <>s);- [][][](s --> []<>s);- [][][sb]( s --> <>[]!s);-- [][sb](s --> [sb]( ([]!s) --> [][](s --> []<>s)));- [][sb](s --> [](([]!s) --> [][](s --> <>[]!s)));-- <>(a & !b & !c & !d & !e & <>(!s & !a & b & !c & !d & !e & <>(!s & !a & !b & c & !d & !e & <> (!s & !a & !b & !c & d & !e & <> (!s & !a & !b & !c & !d & e) ))));-}
− rc/mem_sab_struct_refl.frm
@@ -1,26 +0,0 @@-signature {-propositions { s, a, b, c }-nominals { }-relations { sb }-}--theory--{- s;- []!s;-- []<>s;- [sb][sb](s --> []<>s);- [][sb](s --> <>[]!s);-- [][](!s --> <>s);- [][][](s --> []<>s);- [][][sb]( s --> <>[]!s);-- [][sb](s --> [sb]( ([]!s) --> [][](s --> []<>s)));- [][sb](s --> [](([]!s) --> [][](s --> <>[]!s)));--- <>( <sb>(s & <sb>( (!<>s) & <>( (!<>s ) ) ) ) );-}
− rc/mem_sw_struct.frm
@@ -1,28 +0,0 @@-signature {-propositions { s, a, b, c, d }-nominals { }-relations { sw }-}--theory--{- s;- []!s;- [](!s --> ((<>(s & []false)) & [sw](s --> []!<>s)));- [][](!s --> ((<>(s & []false)) & [sw](s --> []!<>s)));- [][][](!s --> ((<>(s & []false)) & [sw](s --> []!<>s)));-- [][sw](s --> [][][](s --> [] false));- [][][sw](s --> [][][](s --> [] false));--- [sw][sw](!s --> <sw>(s & <><><sw>(s & <>!<>s)));--- <>(!s & a & !b & !c & !d &- <>(!s & !a & b & !c & !d &- <>(!s & !a & !b & c & !d &- <>(!s & !a & !b & !c & d- ))));-}
− rc/mem_sw_struct_refl.frm
@@ -1,24 +0,0 @@-signature {-propositions { s, a, b, c, d }-nominals { }-relations { sw }-}--theory--{- s;- []!s;- [](!s --> ((<>(s & []false)) & [sw](s --> []!<>s)));- [][](!s --> ((<>(s & []false)) & [sw](s --> []!<>s)));- [][][](!s --> ((<>(s & []false)) & [sw](s --> []!<>s)));-- [][sw](s --> [][][](s --> [] false));- [][][sw](s --> [][][](s --> [] false));--- [sw][sw](!s --> <sw>(s & <><><sw>(s & <>!<>s)));--- <>( a & <sw>(s & <><>(!s & !<>s)));-}
− rc/sab_loop.frm
@@ -1,14 +0,0 @@-signature {-propositions { a, b }-nominals { }-relations { sb }-}--theory--{- <>(a & !b & <><>a);- <>(b & !a & <><>b);- [sb](a --> [][]!a);- [sb](b --> [][]!b);-}
− rc/sab_loop_diamond.frm
@@ -1,17 +0,0 @@-signature {-propositions { a, b }-nominals { }-relations { sb }-}--theory--{- <>(a & !b & <><><>a);- <>(b & !a & <><><>b);- [sb](a --> [][][]!a);- [sb](b --> [][][]!b);-- [][][sb][][][] false;- [][][][][]<> true;-}
− rc/sab_no_tree.frm
@@ -1,12 +0,0 @@-signature {-propositions { }-nominals { }-relations { sb, gsb }-}--theory--{- <><>true;- [sb][]false;-}
− rc/sab_sat_01.frm
@@ -1,13 +0,0 @@-signature {-propositions { p, q }-nominals { }-relations { sb, gsb }-}--theory--{- <sb>p;- <sb>q;- <gsb>( <><> true) ;-}
− rc/swap_diamond.frm
@@ -1,15 +0,0 @@-signature {-propositions { a, b }-nominals { }-relations { sw }-}--theory--{- <>(a & !b & <>a);- <>(b & !a & <>b);- [sw][][sw][][] false;- [][sw][][] false;- <sw><sw><><><><><> true;-}
− rc/swap_infinite.frm
@@ -1,25 +0,0 @@-signature {-propositions { s }-nominals { }-relations { sw }-}--theory--{- s;- []!s;- [][]!s;- [][][]!s;- [][][][]!s;- [][][][][]!s;- [][][][][][]!s;- [][][][][][][]!s;- [][][][][][][][]!s;- [][][][][][][][][]!s;- <> true;- []<> true;- [sw][sw](!s --> <><><><><>s);- [sw][][]!s;- [sw][sw][sw](([]!s) --> <><><>(!s & <><><>s));-}
− rc/swap_no_tree.frm
@@ -1,15 +0,0 @@-signature {-propositions { p }-nominals { }-relations { sw }-}--theory--{- p;- []!p;- [][]!p;- [][][]!p;- <sw><><>p;-}
src/HTab/Branch.hs view
@@ -1,20 +1,19 @@ module HTab.Branch ( Branch(..), BranchInfo(..), TodoList(..),-createNewNode, createNewNom,+createNewNode, addFormulas, addAccFormula, addToBlockedDias,-addDiaRuleCheck, addDownRuleCheck,+addDiaRuleCheck, initialBranch, reduceDisjunctionProposeLazy, doLazyBranching, merge, getUrfather, getUrfatherAndDeps, getModelRepresentative, patternBlocked,-diaAlreadyDone, downAlreadyDone,+diaAlreadyDone, ReducedDisjunct(..), patternOf, findByPattern, prefixes, isNominalUrfather, isInTheModel,-positiveNomOf, isTransitive ) where @@ -35,8 +34,7 @@ successors, linksFromTo, showRels ) import HTab.Literals ( UpdateResult(..), Literals, SlotUpdateResult(..), LiteralSlot,- updateMap, lsUnions, lsAddDeps, lsQuery,- positiveNom)+ updateMap, lsUnions, lsAddDeps, lsQuery) data BranchInfo = BranchOK Branch | BranchClash Branch Prefix DependencySet Formula@@ -89,7 +87,6 @@ showIMap (\v -> "(" ++ showMap_lits2 v ++ ")") "\n " (brWitnesses br), "\nDia rule chart: ", show (diaRlCh br), "\nIndividual patterns: ", show (patterns br),- "\nDown rule chart: ", show (downRlCh br), "\n@ rule chart: ", show (list $ atRlCh br), "\nExist rule chart: ", show (list $ existRlCh br), "\nUniv constraints: ", show (univCons br),@@ -113,7 +110,6 @@ diaTodo :: Set PrFormula, existTodo :: Set PrFormula, atTodo :: Set PrFormula,- downTodo :: Set PrFormula, mergeTodo :: Set (DependencySet, Prefix, Nom), roleIncTodo :: Set (DependencySet, Prefix, Prefix, [Rel]) } @@ -123,7 +119,6 @@ , "DiaTodo " ++ show (diaTodo t) , "ExistTodo " ++ show (existTodo t) , "AtTodo " ++ show (atTodo t)- , "DownTodo " ++ show (downTodo t) , "MergeTodo " ++ show (mergeTodo t) , "RoleITodo " ++ show (roleIncTodo t) ]@@ -134,7 +129,6 @@ diaTodo = Set.empty, existTodo = Set.empty, atTodo = Set.empty,- downTodo = Set.empty, mergeTodo = Set.empty, roleIncTodo = Set.empty }@@ -201,7 +195,6 @@ A f -> addUnivConstraint f ds p br E _ -> BranchOK $ addToTodo pf br At _ _ -> BranchOK $ addToTodo pf br- Down _ _ -> BranchOK $ addToTodo pf br Lit l | isPositiveNom l -> addToLiterals pr ds l $ addToTodo pf br Lit l -> addToLiterals pr ds l br @@ -262,7 +255,6 @@ Dia _ _ -> utodo{ diaTodo = Set.insert pf ( diaTodo utodo)} E _ -> utodo{existTodo = Set.insert pf (existTodo utodo)} At _ _ -> utodo{ atTodo = Set.insert pf ( atTodo utodo)}- Down _ _ -> utodo{ downTodo = Set.insert pf ( downTodo utodo)} Lit l | isPositiveNom l -> utodo{mergeTodo = Set.insert (ds,p,s) (mergeTodo utodo)}@@ -272,7 +264,6 @@ case f2 of E f3 -> Set.member f3 (existRlCh br) At n f3 -> Set.member (n,f3) (atRlCh br)- Down _ _ -> downAlreadyDone br pf Dia _ _ -> False -- test happens when the todo list is processed Dis _ -> False -- test happens when the todo list is processed Lit l@@ -590,26 +581,6 @@ diaAlreadyDone _ _ = error "dia already done : wrong formula kind" --addDownRuleCheck :: Prefix -> Formula -> Branch -> BranchInfo-addDownRuleCheck pr f br =- BranchOK br{downRlCh=I.insertWith Set.union ur (Set.singleton f) (downRlCh br)}- where ur = getUrfather br (DS.Prefix pr)--downAlreadyDone :: Branch -> PrFormula -> Bool-downAlreadyDone b (PrFormula p _ f@(Down _ _)) =- case I.lookup ur (downRlCh b) of- Nothing -> False- Just fset -> Set.member f fset- where ur = getUrfather b (DS.Prefix p)--downAlreadyDone _ _ = error "down already done : wrong formula kind"---- | return some nominal that holds at a given prefix-positiveNomOf :: Branch -> Prefix -> Maybe String-positiveNomOf b p = positiveNom (literals b) ur- where ur = getUrfather b (DS.Prefix p)- addUnivConstraint :: Formula -> DependencySet -> Params -> Branch -> BranchInfo addUnivConstraint f ds p br = addFormulas p [PrFormula pr ds f | pr <- urfathers] newBr@@ -631,10 +602,6 @@ addReflexiveLinks pr br = foldr (\rel_ br_ -> insertRelationBranch br_ pr rel_ pr dsEmpty) br reflRels where reflRels = Map.keys $ Map.filter (elem Reflexive) (relInfo br)--createNewNom :: Branch -> BranchInfo-createNewNom br- = BranchOK br{nextNom = nextNom br + 1} -- preparation of the branch at the beginning of the calculus: -- - add the input formula at prefix 0
src/HTab/CommandLine.hs view
@@ -22,11 +22,7 @@ showFormula :: Bool, allTransitive :: Bool, allReflexive :: Bool- , translate :: Bool , minimal :: Bool- , random :: Bool- , seed :: Maybe String- , test_translations :: Bool } deriving (Show, Data, Typeable) data UnitProp = UPYes | Eager | UPNo deriving (Data, Typeable, Eq, Show)@@ -49,15 +45,11 @@ showFormula := False += help "display formula", allTransitive := False += help "make all relations transitive", allReflexive := False += help "make all relations reflexive",- translate := False += help "translate relation-changing formulas to hybrid",- minimal := False += help "look for minimal model (slow)",- random := False += help "randomly select next disjunctive formula, also randomize disjuncts",- seed := Nothing += help "set random seed (integer)",- test_translations := False += help "run the memory-to-relation-changing test suite"+ minimal := False += help "look for minimal model (slow)" ] += verbosity strategyVal :: String-strategyVal = "n@E<b|r"+strategyVal = "n@E<|r" checkParams :: Params -> IO Bool checkParams p@@ -67,18 +59,14 @@ "strategy should contain all of the following characters: ", " n = nominals @ = satisfaction operator", " E = existential modality < = diamond",- " b = down-arrow binder | = or",- " r = role inclusion",+ " | = or r = role inclusion", "", "The default is \"" ++ strategyVal ++ "\"", "The rules conjunction, box, and universal modality", "are applied immediately, thus do not belong to the strategy."] return False- | null (filename p) && not (test_translations p)=+ | null (filename p)= do putStrLn $ unlines ["ERROR: No input specified.","Run with --help for usage options"]- return False- | translate p && (allTransitive p || allReflexive p) = - do putStrLn $ unlines ["ERROR: --translate incompatible with --all-transitive or --all-reflexive."] return False | otherwise = return True where notPermutationOf l1 l2 = sort l1 /= sort l2
src/HTab/Formula.hs view
@@ -8,14 +8,12 @@ LanguageInfo(..), neg, conj, disj, taut, prop, nom, prefix, negPr,-replaceVar, firstPrefixedFormula, parse, simpleParse, Theory, RelInfo, Task, showRelInfo, negLit, encodeValidityTest, encodeSatTest, encodeRetrieveTask, HyLoFormula, RelProperty(..),-isPositiveNom, isPositiveProp, isProp, list, imp,-trSab, trSwap, trBri, emptyset+isPositiveNom, isPositiveProp, isProp, list, imp ) where@@ -71,7 +69,6 @@ | Con (Set Formula) | Dis (Set Formula) | At Nom Formula- | Down Nom Formula | Box Rel Formula | Dia Rel Formula | A Formula@@ -87,7 +84,6 @@ show (Dia r f) = "<" ++ r ++ ">" ++ show f show (A f) = "A " ++ show f show (E f) = "E " ++ show f- show (Down n f) = "down " ++ n ++ "." ++ show f -- parsing of the input file @@ -106,19 +102,13 @@ showRelInfo :: RelInfo -> String showRelInfo = Map.foldrWithKey (\r v -> (++ " " ++ show r ++ " -> " ++ show v )) "" -data RelationChanging = Sabotage | Bridge | Swap- parse :: Params -> String -> (Theory,RelInfo,LanguageInfo,[Task]) parse p s = (theory, relInfo, fLang, tasks) where parseOutput = InputFile.myparse s -- direct parse from hylolib pRelInfo = P.relations parseOutput- relInfo = if translate p- then monomodal $ convertToOurType pRelInfo- else forceProperties p parseOutput $ convertToOurType pRelInfo- theory = if translate p- then doTranslate (detectRCLogic pRelInfo) $ P.theory parseOutput- else convert relInfo $ P.theory parseOutput+ relInfo = forceProperties p parseOutput $ convertToOurType pRelInfo+ theory = convert relInfo $ P.theory parseOutput tasks = P.tasks parseOutput fLang = langInfo parseOutput @@ -136,25 +126,6 @@ (allReflexive p, Reflexive )] theory = P.theory po --- assume input formula is relation-changing--- then it is monomodal, only relation is R-monomodal :: RelInfo -> RelInfo-monomodal _ = Map.fromList [("R", [])]- -- TODO check parameter and fail if relation other than R used in input file---detectRCLogic :: PRelInfo -> RelationChanging-detectRCLogic prelI- | "sb" `elem` rels = Sabotage- | "gsb" `elem` rels = Sabotage- | "sw" `elem` rels = Swap- | "gsw" `elem` rels = Swap- | "br" `elem` rels = Bridge- | "gbr" `elem` rels = Bridge- | otherwise = error "does not seem like a relation-changing formula!"- where rels = map fst prelI-- convertToOurType :: PRelInfo -> RelInfo -- and add for each relation in the formula, the relevant key convertToOurType prelI = foldr insertRelProp Map.empty (concatMap convertOne prelI)@@ -199,7 +170,6 @@ conv_ relI (F.Diam (S.RelSymbol r) f) = specialiseDia (up r) relI (conv_ relI f) conv_ relI (F.Box (S.RelSymbol r) f) = specialiseBox (up r) relI (conv_ relI f) conv_ relI (F.At n f) = at n (conv_ relI f)-conv_ relI (F.Down v f) = downArrow v (conv_ relI f) conv_ relI (F.A f) = univMod (conv_ relI f) conv_ relI (F.E f) = existMod (conv_ relI f) conv_ _ f = error (show f ++ "not supported")@@ -219,153 +189,6 @@ | otherwise = relational r where props = Map.findWithDefault [] r relI ---- COMMON STRUCTURES FOR ALL RELATION-CHANGING TRANSLATIONS ---type S = ( [(String, String)] , Int) -- Int = next nominal number to use-emptyset :: S -- directly nominal strings (uppercase)-emptyset = ([],0)--- generate unused nominal and update S-next :: S -> (String,S)-next (ss,n) = ("N" ++ show n, (ss, n + 1))---- SABOTAGE TRANSLATION ----- not exactly a union but we're mimicking the article-union :: S -> (String, String) -> S-union (ss,n) nm = (ss ++ [nm], n)--- macro for translation-belongs :: String -> S -> Formula-belongs n (ss,_) = foldr disj (neg taut) $ set [ (n' y) `conj` At n (n' x) | (x,y) <- ss ]- where n' = Lit . PosLit . N---- SWAP TRANSLATION ---inverse :: S -> S-inverse (ss,n) = (map (\(a,b) -> (b,a)) ss, n)--- | slightly different from paper: phi must be already translated-isSat :: S -> Formula -> Formula-isSat (ss,_) phi = foldr disj (neg taut) [ n x `conj` At y phi | (x,y) <- ss ]- where n = Lit . PosLit . N---- | swap again some pair in S-again :: S -> (String, String) -> S-again (ss,n) xy@(x,y)- | xy `elem` ss = ( (y,x):(delete xy ss), n)- | otherwise = error "trying to swap again something that is not here"--doTranslate :: RelationChanging -> [F.Formula S.NomSymbol S.PropSymbol S.RelSymbol] -> Formula-doTranslate rc input = -- TODO detect if sabotage, if bridge, if swap- case rc of- Sabotage -> trSab emptyset bigAnd- Swap -> trSwap emptyset bigAnd- Bridge -> trBri emptyset bigAnd- where bigAnd = convert Map.empty input--trSab :: S -> Formula -> Formula-trSab _ l@(Lit _) = l-trSab s (Con fs) = Con (Set.map (trSab s) fs)-trSab s (Dis fs) = Dis (Set.map (trSab s) fs)-trSab s (At n f) = At n (trSab s f)-trSab s (Down v f) = Down v (trSab s f)-trSab s (A f) = A (trSab s f)-trSab s (E f) = E (trSab s f)-trSab s (Box r f) = neg $ trSab s (Dia r (neg f))-trSab s (Dia r f)- | up r `elem` ["R","R1"] =- case s of- ([],_) -> Dia "R" (trSab s1 f)- _ -> Down newNom1 ( Dia "R" ( (neg $ belongs newNom1 s1) `conj` (trSab s1 f)))- | up r == "SB" =- Down newNom1 (Dia "R" ( (neg $ belongs newNom1 s2) `conj` (Down newNom2 (trSab s2u12 f)))) - | up r == "GSB" =- Down newNom1 $ E $ Down newNom2- $ (Dia "R" ( (neg $ belongs newNom2 s2) `conj` (Down newNom3 $ At newNom1 (trSab s4u23 f))))- | otherwise = error ("Relation is not r, r1, sb or gsb: " ++ r)- where (newNom1,s1) = next s- (newNom2,s2) = next s1- s2u12 = s2 `union` (newNom1,newNom2)- (newNom3,s3) = next s2- s4u23 = s3 `union` (newNom2,newNom3)--trBri :: S -> Formula -> Formula-trBri _ l@(Lit _) = l-trBri s (Con fs) = Con (Set.map (trBri s) fs)-trBri s (Dis fs) = Dis (Set.map (trBri s) fs)-trBri s (At n f) = At n (trBri s f)-trBri s (Down v f) = Down v (trBri s f)-trBri s (A f) = A (trBri s f)-trBri s (E f) = E (trBri s f)-trBri s (Box r f) = neg $ trBri s (Dia r (neg f))-trBri s (Dia r f)- | up r `elem` ["R","R1"] =- case s of- ([],_) -> Dia "R" (trBri s1 f)- _ -> Down newNom1 $ E $ Down newNom2- ( (( At newNom1 (Dia "R" (n newNom2))) `disj` (belongs newNom1 s1))- `conj` (trBri s2 f)- )- | up r == "BR" =- Down newNom1 $ E $ Down newNom2- ( ( neg $ At newNom1 (Dia "R" (n newNom2)))- `conj` (neg $ belongs newNom1 s1)- `conj` (trBri s2u12 f)- )- | up r == "GBR" =- Down newNom1 $ E $ Down newNom2 $ E $ Down newNom3- ( ( neg $ At newNom2 (Dia "R" (n newNom3)))- `conj` (neg $ belongs newNom2 s1)- `conj` At newNom1 (trBri s4u23 f)- )- | otherwise = error ("Relation is not r, r1, br or gbr: " ++ r)- where (newNom1,s1) = next s- (newNom2,s2) = next s1- s2u12 = s2 `union` (newNom1,newNom2)- (newNom3,s3) = next s2- s4u23 = s3 `union` (newNom2,newNom3)- n = Lit . PosLit . N--trSwap :: S -> Formula -> Formula-trSwap _ l@(Lit _) = l-trSwap s (Con fs) = Con (Set.map (trSwap s) fs)-trSwap s (Dis fs) = Dis (Set.map (trSwap s) fs)-trSwap s (At n f) = At n (trSwap s f)-trSwap s (Down v f) = Down v (trSwap s f)-trSwap s (A f) = A (trSwap s f)-trSwap s (E f) = E (trSwap s f)-trSwap s (Box r f) = neg $ trSwap s (Dia r (neg f))-trSwap s@(ss,_) (Dia r f)- | up r `elem` ["R","R1"] =- case s of- ([],_) -> Dia "R" (trSwap s1 f)- _ -> (Down newNom1 ( Dia "R" ( (neg $ belongs newNom1 s1) `conj` (trSwap s1 f))))- `disj`- (isSat (inverse s) (trSwap s f))- | up r == "SW" =- ( Down newNom1 (Dia "R" (n newNom1)) `conj` trSwap s f )- `disj`- ( Down newNom1 $ Dia "R" - $ neg (n newNom1)- `conj` neg (belongs newNom1 s)- `conj` neg (belongs newNom1 (inverse s))- `conj` (Down newNom2 $ trSwap s2u12 f))- `disj`- foldr disj (neg taut) [ n y `conj` At x (trSwap (again s (x,y)) f) | (x,y) <- ss ]- | up r == "GSW" =- ( (E $ Down newNom1 $ Dia "R" $ n newNom1) `conj` trSwap s f )- `disj`- ( Down newNom1 $ E $ Down newNom2 $ Dia "R"- $ neg (n newNom2)- `conj` neg (belongs newNom2 s)- `conj` neg (belongs newNom2 (inverse s))- `conj` (Down newNom3 $ At newNom1 $ trSwap s4u23 f))- `disj`- foldr disj (neg taut) [ trSwap (again s (x,y)) f | (x,y) <- ss ]- | otherwise = error ("Relation is not r, r1, sw or gsw: " ++ r)- where (newNom1,s1) = next s- (newNom2,s2) = next s1- s2u12 = s2 `union` (newNom1,newNom2)- (newNom3,s3) = next s2- s4u23 = s3 `union` (newNom2,newNom3)- n = Lit . PosLit . N- type HyLoFormula = F.Formula S.NomSymbol S.PropSymbol S.RelSymbol encodeValidityTest :: RelInfo -> Formula -> [HyLoFormula] -> Formula@@ -401,10 +224,6 @@ univMod = A existMod = E -{- binder -}-downArrow :: S.NomSymbol -> Formula -> Formula-downArrow (S.NomSymbol n) = Down (up n)- {- Hybrid operators -} at :: S.NomSymbol -> Formula -> Formula at (S.NomSymbol n) = At (up n)@@ -469,7 +288,6 @@ neg (Con l) = Dis (Set.map neg l) neg (Dis l) = Con (Set.map neg l) neg (At n f) = At n (neg f)-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 (A f) = E (neg f)@@ -477,7 +295,6 @@ neg (Lit (PosLit a)) = Lit (NegLit a) neg (Lit (NegLit a)) = Lit (PosLit a) - -- prefixed formula data PrFormula = PrFormula Prefix DependencySet Formula@@ -512,31 +329,6 @@ = LanguageInfo { languageNoms = noms } where noms = nub $ map (\(S.NomSymbol n) -> up n) $ concatMap (list . nomSymbols . getSignature) theory theory = P.theory po---- composeXX functions follow the idea from--- "A pattern for almost compositional functions", Bringert and Ranta.-composeMap :: (Formula -> Formula)- -> (Formula -> Formula)- -> (Formula -> Formula)-composeMap baseCase g e = case e of- Con fs -> Con $ Set.map g fs- Dis fs -> Dis $ Set.map g fs- Dia r f -> Dia r (g f)- Box r f -> Box r (g f)- At i f -> At i (g f)- A f -> A (g f)- E f -> E (g f)- Down x f -> Down x (g f)- f -> baseCase f--replaceVar :: String -> String -> Formula -> Formula-replaceVar v n a@(Lit (PosLit (N v2))) = if v == v2 then Lit (PosLit (N n)) else a-replaceVar v n a@(Lit (NegLit (N v2))) = if v == v2 then Lit (NegLit (N n)) else a-replaceVar v n a@(Down v2 f) = if v == v2 then a -- variable capture- else Down v2 (replaceVar v n f)-replaceVar v n (At v2 f) = if v == v2 then At n (replaceVar v n f)- else At v2 (replaceVar v n f)-replaceVar v n f = composeMap id (replaceVar v n) f -- backjumping
src/HTab/Literals.hs view
@@ -1,8 +1,7 @@ module HTab.Literals ( UpdateResult(..), Literals, SlotUpdateResult(..), LiteralSlot,-updateMap, lsUnions, lsAddDeps, lsQuery,-positiveNom+updateMap, lsUnions, lsAddDeps, lsQuery ) where import Data.IntMap ( IntMap)@@ -113,10 +112,4 @@ where dlookup pr_ l_ lits_ = do slot <- I.lookup pr_ lits_ M.lookup l_ slot--positiveNom :: Literals -> Prefix -> Maybe String-positiveNom lits pr = do slot <- I.lookup pr lits- case filter isPositiveNom (M.keys slot) of- (PosLit (N n):_) -> Just n- _ -> Nothing
src/HTab/Main.hs view
@@ -3,21 +3,19 @@ ( runWithParams, TaskRunFlag(..)) where-import Control.Monad ( when, forM_ )+import Control.Monad ( when ) import Control.Monad.State( runStateT ) import Data.List ( intersperse )-import qualified Data.Map as Map import System.Console.CmdArgs ( whenNormal, whenLoud ) import System.CPUTime( getCPUTime ) import qualified System.Timeout as T-import System.Random (StdGen, getStdGen) import System.IO.Strict ( readFile ) import Prelude hiding ( readFile ) import HyLo.InputFile.Parser ( QueryType(..) ) -import HTab.CommandLine( filename, random, seed, test_translations,+import HTab.CommandLine( filename, timeout, Params, genModel, dotModel, showFormula ) import HTab.Branch( BranchInfo(..), initialBranch) import HTab.Statistics( Statistics, initialStatisticsStateFor, printOutMetricsFinal )@@ -25,7 +23,6 @@ import HTab.Formula( Theory, RelInfo, LanguageInfo(..), Task, Formula(Con), encodeValidityTest, encodeSatTest, encodeRetrieveTask, showRelInfo, list )-import HTab.Memory (unsats, sats) import qualified HTab.Formula as F import qualified HyLo.Signature.String as S import HTab.ModelGen ( Model, toDot )@@ -33,41 +30,8 @@ data TaskRunFlag = SUCCESS | FAILURE runWithParams :: Params -> IO (Maybe TaskRunFlag)-runWithParams p | test_translations p =- do putStrLn "Running memory logic to relation-changing logics test suite."- g <- case seed p of- Nothing -> getStdGen- Just s -> do putStrLn "Using given random seed."- return (read s)- putStrLn "=== UNSAT formulas ==="- forM_ (zip [1::Int ..] unsats) $ \(i,(mf,rc,h,name)) ->- do myPutStrLn (show i ++ " " ++ show mf ++ " via " ++ name)- r <- inTimeout (timeout p) $- do (result,_) <- tableauInit p g $ initialBranch p (LanguageInfo []) Map.empty h- return result- case r of- Nothing -> myPutStrLn "Timeout"- Just (CLOSED _) -> myPutStrLn "OK"- Just (OPEN _) -> myPutStrLn ("ERROR: formula is sat\n" ++ show rc)- putStrLn "=== SAT formulas ==="- forM_ (zip [(length unsats + 1)::Int ..] sats) $ \(i,(mf,rc,h,name)) ->- do myPutStrLn (show i ++ " " ++ show mf ++ " via " ++ name)- r <- inTimeout (timeout p) $- do (result,_) <- tableauInit p g $ initialBranch p (LanguageInfo []) Map.empty h- return result- case r of- Nothing -> myPutStrLn "Timeout"- Just (OPEN _) -> myPutStrLn "OK"- Just (CLOSED _) -> myPutStrLn ("ERROR: formula is unsat\n" ++ show rc)- return (Just SUCCESS)- runWithParams p = time "Total time: " $ do- g <- case seed p of- Nothing -> getStdGen- Just s -> do putStrLn "Using given random seed."- return (read s)- when (random p) $ putStrLn ( unlines ["Will use random seed:",show g]) i <- readFile (filename p) if head (words i) == "begin" then do@@ -80,7 +44,7 @@ "Relations properties :" ++ showRelInfo relInfo ] -- tResult <- inTimeout (timeout p) $- do (result,s) <- tableauInit p g $+ do (result,s) <- tableauInit p $ initialBranch p fLang relInfo f whenNormal $ printOutMetricsFinal s return result@@ -94,7 +58,7 @@ return (Just FAILURE) else do let allTasks = F.parse p i- result <- inTimeout (timeout p) (runTasks allTasks p g)+ result <- inTimeout (timeout p) (runTasks allTasks p) -- case result of Nothing -> myPutStrLn "\nTimeout.\n"@@ -109,42 +73,42 @@ -- -runTasks :: (Theory,RelInfo,LanguageInfo,[Task]) -> Params -> StdGen -> IO TaskRunFlag-runTasks allTasks@(theory,relInfo,fLang,tasks) p g =+runTasks :: (Theory,RelInfo,LanguageInfo,[Task]) -> Params -> IO TaskRunFlag+runTasks allTasks@(theory,relInfo,fLang,tasks) p = do myPutStrLn "== Checking theory satisfiability ==" res <- time "Task time:" $- runTask (Satisfiable, genModel p, []) relInfo fLang theory p g+ runTask (Satisfiable, genModel p, []) relInfo fLang theory p case res of SUCCESS | null tasks -> return SUCCESS | otherwise -> do myPutStrLn "\n== Starting tasks =="- res2 <- runTasks2 allTasks p g+ res2 <- runTasks2 allTasks p myPutStrLn "\n== End of tasks ==" return res2 FAILURE -> return FAILURE -- -runTasks2 :: (Theory,RelInfo,LanguageInfo,[Task]) -> Params -> StdGen -> IO TaskRunFlag-runTasks2 (_,_,_,[]) _ _ = error "runTasks2 empty list error"-runTasks2 (theory,relInfo,fLang,(hd:tl)) p g =- do res <- time "Task time:" $ runTask hd relInfo fLang theory p g+runTasks2 :: (Theory,RelInfo,LanguageInfo,[Task]) -> Params -> IO TaskRunFlag+runTasks2 (_,_,_,[]) _ = error "runTasks2 empty list error"+runTasks2 (theory,relInfo,fLang,(hd:tl)) p =+ do res <- time "Task time:" $ runTask hd relInfo fLang theory p case res of SUCCESS | null tl -> return SUCCESS- | otherwise -> runTasks2 (theory,relInfo,fLang,tl) p g- FAILURE -> do _ <- runTasks2 (theory,relInfo,fLang,tl) p g+ | otherwise -> runTasks2 (theory,relInfo,fLang,tl) p+ FAILURE -> do _ <- runTasks2 (theory,relInfo,fLang,tl) p return FAILURE -- -runTask :: Task -> RelInfo -> LanguageInfo -> Formula -> Params -> StdGen -> IO TaskRunFlag-runTask (Retrieve,mOutFile,fs) relInfo fLang theory p g =+runTask :: Task -> RelInfo -> LanguageInfo -> Formula -> Params -> IO TaskRunFlag+runTask (Retrieve,mOutFile,fs) relInfo fLang theory p = do myPutStrLn "\n* Instance retrieval task" let (noms,encfs) = encodeRetrieveTask relInfo fLang theory fs -- myPutStrLn $ "Instances making true: " ++ show fs --- results <- mapM (tableauInit p g . initialBranch p fLang relInfo) encfs -- NOTE: we reuse the same random generator+ results <- mapM (tableauInit p . initialBranch p fLang relInfo) encfs -- NOTE: we reuse the same random generator let goods = [ S.NomSymbol n | (n,(CLOSED _ ,_)) <- zip noms results] myPutStrLn $ show goods let doWrite f = do writeFile f (show goods ++ "\n")@@ -152,7 +116,7 @@ maybe (return ()) doWrite mOutFile return SUCCESS -runTask (Satisfiable,mOutFile,fs) relInfo fLang theory p g =+runTask (Satisfiable,mOutFile,fs) relInfo fLang theory p = do myPutStrLn "\n* Satisfiability task" let f = encodeSatTest relInfo theory fs --@@ -165,7 +129,7 @@ ["}", "End of input", "Relations properties :" ++ showRelInfo relInfo ] --- (result,stats) <- tableauInit p g $ initialBranch p fLang relInfo f+ (result,stats) <- tableauInit p $ initialBranch p fLang relInfo f -- whenNormal $ printOutMetricsFinal stats --@@ -176,7 +140,7 @@ CLOSED _ -> do myPutStrLn "The formula is unsatisfiable." return FAILURE -runTask (Valid,mOutFile,fs) relInfo fLang theory p g =+runTask (Valid,mOutFile,fs) relInfo fLang theory p = do myPutStrLn "\n* Validity task" let f = encodeValidityTest relInfo theory fs --@@ -186,7 +150,7 @@ "End of input", "Relations properties :" ++ showRelInfo relInfo ] --- (result,stats) <- tableauInit p g $ initialBranch p fLang relInfo f+ (result,stats) <- tableauInit p $ initialBranch p fLang relInfo f -- whenNormal $ printOutMetricsFinal stats --@@ -197,7 +161,7 @@ CLOSED _ -> do myPutStrLn "The formula is valid." return SUCCESS -runTask (Counting,_,_) _ _ _ _ _ =+runTask (Counting,_,_) _ _ _ _ = do myPutStrLn "\n* Counting task is NOT supported" return FAILURE @@ -210,11 +174,11 @@ output | dotModel p = toDot m | otherwise = show m -tableauInit :: Params -> StdGen -> BranchInfo -> IO (OpenFlag,Statistics)-tableauInit p g bi =+tableauInit :: Params -> BranchInfo -> IO (OpenFlag,Statistics)+tableauInit p bi = do whenLoud $ putStrLn ">> Starting rules application" initStatsState $ tableauStart p bi- where initStatsState = initialStatisticsStateFor runStateT g+ where initStatsState = initialStatisticsStateFor runStateT --
− src/HTab/Memory.hs
@@ -1,232 +0,0 @@-module HTab.Memory ( sats, unsats )-where--import qualified Data.Set as Set-import HTab.Formula--data MemFormula- = MLit Literal- | MCon MemFormula MemFormula- | MDis MemFormula MemFormula- | MBox MemFormula- | MDia MemFormula- | MNeg MemFormula- | Re MemFormula -- ^ Remember- | Kn -- ^ Known- deriving (Eq, Ord )--instance Show MemFormula where- show (MLit a) = show a- show (MCon f1 f2) = "(" ++ show f1 ++ " & " ++ show f2 ++ ")"- show (MDis f1 f2) = "(" ++ show f1 ++ " v " ++ show f2 ++ ")"- show (MBox f) = "[](" ++ show f ++ ")"- show (MDia f) = "<>(" ++ show f ++ ")"- show (MNeg f) = "¬(" ++ show f ++ ")"- show (Re f) = "Re(" ++ show f ++ ")"- show Kn = "Kn"--mtop, mbot :: MemFormula-mtop = MLit $ PosLit Taut-mbot = MLit $ NegLit Taut---- unsat memory logic formulas-kn, re1, re2, re3 :: MemFormula-kn = Kn-re1 = (MLit (PosLit (P "P"))) `MCon` (Re (MLit (NegLit (P "P")))) -re2 = (MBox mbot) `MCon` (Re (MDia mtop)) -re3 = (MDia mbot) `MCon` (Re (MBox mtop)) --- bury these unsat formulas in sufficiently deep diamonds-unsats_mem :: [MemFormula]-unsats_mem = concat [ nested f | f <- [kn, re1, re2, re3] ]---- (interesting) SAT memory logic formulas-rekn1, rekn2, rekn3, rekn4, chain4 :: MemFormula-rekn1 = Re (MDia Kn `MCon` MBox Kn) -- (r)( <>(k) & [](k) )-rekn2 = MNeg Kn -- !(k)-rekn3 = Re ( MDia (MNeg Kn)) -- (r)<>!(k)-rekn4 = Re (MDia Kn `MCon` MDia (MNeg Kn)) -- (r)( <>(k) & <>!(k) )-chain4 = c [ p "a", q "b", q "c", q "d", MDia- (c [ q "a", p "b", q "c", q "d", MDia- (c [ q "a", q "b", p "c", q "d", MDia- (c [ q "a", q "b", q "c", p "d"])])])]- where p = MLit . PosLit . P- q = MLit . NegLit . P- c = foldr1 MCon--sats_mem :: [MemFormula]-sats_mem = chain4 : concat [ nested f | f <- [rekn1, rekn2, rekn3, rekn4]]--nested :: MemFormula -> [MemFormula]-nested f = [f, MDia f, MDia $ MDia f, MDia $ MDia $ MDia f]---- test suite for translations Memory Logic -> Relation-Changing logics-unsats, sats :: [(MemFormula, Formula,Formula,String)]-unsats = concatMap memToHybrid unsats_mem -- all of them should be found UNSAT-sats = concatMap memToHybrid sats_mem -- all of them should be found SAT---- given a memory logic formula, translate it to the 6 relation-changing logics + translate again to hybrid logic-memToHybrid :: MemFormula -> [(MemFormula,Formula,Formula,String)]-memToHybrid f = map (\(rcTr, hTr,name) -> (f, rcTr f, hTr (rcTr f), name))- [ (memGSb, trSab emptyset, "Global Sabotage")- , (memGSw, trSwap emptyset, "Global Swap")- , (memGBr, trBri emptyset, "Global Bridge")- , (memLBr, trBri emptyset, "Local Bridge")- , (memLSw, trSwap emptyset, "Local Swap")- , (memLSb, trSab emptyset, "Local Sabotage") ]---- ^ translate a memory logic formula into a global sabotage--- formula where modalities are R and GSB-memGSb :: MemFormula -> Formula-memGSb f_ = struct (mmd f_) `conj` go f_- where- struct n = foldr conj neg_s [ nestBox i (neg_s `imp` Dia "R" s) | i <- [0..n]]-- go (Kn) = neg (Dia "R" s)- go (Re f) = Dia "GSB" ( (neg (Dia "R" s)) `conj` go f)- go (MDia f) = Dia "R" (neg_s `conj` go f)- go (MBox f) = Box "R" (neg_s `imp` go f)- go (MCon f g) = (go f) `conj` (go g)- go (MDis f g) = (go f) `disj` (go g)- go (MLit l) = Lit l- go (MNeg f) = neg (go f)--memGSw :: MemFormula -> Formula-memGSw f_ = struct (mmd f_) `conj` go f_- where- struct n = foldr conj neg_s [ nestBox i (neg_s `imp` Dia "R" s) | i <- [0..n]]-- go (Kn) = neg (Dia "R" s)- go (Re f) = Dia "GSW" ( (neg (Dia "R" s)) `conj` go f)- go (MDia f) = Dia "R" (neg_s `conj` go f)- go (MBox f) = Box "R" (neg_s `imp` go f)- go (MCon f g) = (go f) `conj` (go g)- go (MDis f g) = (go f) `disj` (go g)- go (MLit l) = Lit l- go (MNeg f) = neg (go f)--memGBr :: MemFormula -> Formula-memGBr f_ = struct (mmd f_) `conj` go f_- where- struct n = foldr conj taut [ nestBox i neg_s | i <- [0..(n+1)]]-- go (Kn) = Dia "R" s- go (Re f) = Dia "GBR" ( (Dia "R" s) `conj` go f)- go (MDia f) = Dia "R" (neg_s `conj` go f)- go (MBox f) = Box "R" (neg_s `imp` go f)- go (MCon f g) = (go f) `conj` (go g)- go (MDis f g) = (go f) `disj` (go g)- go (MLit l) = Lit l- go (MNeg f) = neg (go f)--memLSw :: MemFormula -> Formula-memLSw f_ = struct `conj` d (go f_)- where- struct = Con $ set- [ s- , b neg_s- , b (neg_s `imp` uniq)- , b $ b (neg_s `imp` uniq)- , b $ b $ b (neg_s `imp` uniq)- , b $ bsw (s `imp` (b $ b $ b (s `imp` b (neg taut))))- , b $ b $ bsw (s `imp` (b $ b $ b (s `imp` b (neg taut))))- , bsw $ bsw ( neg_s `imp` dsw ( s `conj` (d (b neg_s `imp` (d $ d (s `conj` d(b(neg_s))))))))- ]-- go (MDia f) = Dia "R" (neg_s `conj` go f)- go (MBox f) = Box "R" (neg_s `imp` go f)- go (MCon f g) = (go f) `conj` (go g)- go (MDis f g) = (go f) `disj` (go g)- go (MLit l) = Lit l- go (MNeg f) = neg (go f)- go (Kn) = neg (d s)- go (Re f) = dsw (s `conj` d (go f))-- uniq = (d (s `conj` (b (neg taut))))- `conj` bsw (s `imp` b (b neg_s))- bsw = Box "SW"- dsw = Dia "SW"--memLBr :: MemFormula -> Formula-memLBr f_ = struct `conj` dbr(neg_s `conj` t `conj` dbr(neg_s `conj` neg_t `conj` go f_))- where- struct = Con $ set- [ s- , b (neg taut)- , bbr (s `imp` bbr neg_s)- , bbr (neg_s `imp` b neg_s)- ]-- go (MDia f) = Dia "R" (neg_s_and_neg_t `conj` go f)- go (MBox f) = Box "R" (neg_s_and_neg_t `imp` go f)- go (MCon f g) = (go f) `conj` (go g)- go (MDis f g) = (go f) `disj` (go g)- go (MLit l) = Lit l- go (MNeg f) = neg (go f)- go (Kn) = d s- go (Re f) = dbr( s `conj` dbr ( neg_s `conj` (d s) `conj` (go f)))-- t = Lit (PosLit (P "T"))- neg_t = Lit (NegLit (P "T"))- neg_s_and_neg_t = neg_s `conj` neg_t- dbr = Dia "BR"- bbr = Box "BR"--memLSb :: MemFormula -> Formula-memLSb f_ = struct `conj` d (go f_)- where- struct = Con $ set- [ s- , b neg_s- , b $ d s- , bsb ( bsb ( s `imp` b (d s)))- , b ( bsb ( s `imp` d (b neg_s )))- , b ( b ( neg_s `imp` d s))--- , b ( bsb ( s `imp` ( bsb ( (b neg_s) `imp` (b ( b ( s `imp` b (d s))))))))- , b ( bsb ( s `imp` ( b ( (b neg_s) `imp` (b ( b ( s `imp` d (b neg_s))))))))- , b ( b ( neg_s `imp`( s `imp` d ( b neg_s))))-- ]-- go (MDia f) = Dia "R" (neg_s `conj` go f)- go (MBox f) = Box "R" (neg_s `imp` go f)- go (MCon f g) = (go f) `conj` (go g)- go (MDis f g) = (go f) `disj` (go g)- go (MLit l) = Lit l- go (MNeg f) = neg (go f)- go (Kn) = neg (d s)- go (Re f) = dsb( s `conj` dsb ( neg (d s) `conj` go f))-- dsb = Dia "SB"- bsb = Box "SB"----- helper functions---- ^ Modal depth of a memory logic formula-mmd :: MemFormula -> Int-mmd Kn = 0-mmd (MLit _ ) = 0-mmd (MBox f) = 1 + mmd f-mmd (MDia f) = 1 + mmd f-mmd (MDis f g) = max (mmd f) (mmd g)-mmd (MCon f g) = max (mmd f) (mmd g)-mmd (MNeg f) = mmd f-mmd (Re f) = mmd f--nestBox :: Int -> Formula -> Formula-nestBox 0 f = f-nestBox n f = nestBox (n-1) (Box "R" f)--s, neg_s :: Formula-neg_s = Lit (NegLit (P "S"))-s = Lit (PosLit (P "S"))--set :: Ord a => [a] -> Set.Set a-set = Set.fromList--d, b :: Formula -> Formula-d = Dia "R"-b = Box "R"-
src/HTab/RuleId.hs view
@@ -40,11 +40,9 @@ | R_Disj -- Disjunction | R_SemBr -- Semantic Branching | R_At -- Satisfaction operator (@) rule- | R_Down -- Down-arrow rule | R_NegNom -- Negation before nominal rule | R_Exist -- Existential modality | R_Discard -- Discarding a formula- | R_DiscardDown | R_DiscardDiaDone | R_DiscardDiaBlocked | R_DiscardDiaSymBlocked
src/HTab/Rules.hs view
@@ -4,30 +4,24 @@ applicableRule, applyRule, ruleToId ) where -import System.Random--import qualified Data.Map as Map- import qualified Data.Set as Set import Data.Maybe ( mapMaybe ) import HTab.Formula( Formula(..), PrFormula(..), showLess, Dependency, DependencySet, dsUnion, dsInsert, prefix, Rel, negPr,- Prefix, Nom, Atom(..),- replaceVar, Literal(..))+ Prefix, Nom, Literal(..)) import HTab.Branch( Branch(..), BranchInfo(..), TodoList(..), -- for rules- createNewNode, createNewNom,+ createNewNode, addFormulas, addAccFormula, addDiaRuleCheck, addToBlockedDias,- addDownRuleCheck, doLazyBranching, getUrfatherAndDeps, merge,- isNominalUrfather, positiveNomOf,+ isNominalUrfather, -- for choosing rule in todo list patternBlocked,- diaAlreadyDone, downAlreadyDone,+ diaAlreadyDone, -- for rules and choosing rule in todo list reduceDisjunctionProposeLazy, getUrfather, ReducedDisjunct(..)@@ -35,7 +29,6 @@ import HTab.CommandLine(Params, UnitProp(..), lazyBranching, semBranch, unitProp, strategy, minimal)-import qualified HTab.CommandLine as CL ( random ) import HTab.RuleId(RuleId(..)) import qualified HTab.DisjSet as DS @@ -47,8 +40,6 @@ | SemBrRule PrFormula [PrFormula] | LazyBrRule PrFormula Prefix Literal [PrFormula] | AtRule PrFormula- | DownRule PrFormula- | DiscardDownRule PrFormula | DiscardDiaDoneRule PrFormula | DiscardDiaBlockedRule PrFormula | DiscardDisjTrivialRule PrFormula@@ -56,17 +47,14 @@ | MergeRule Prefix Nom DependencySet | RoleIncRule Prefix [Rel] Prefix DependencySet - instance Show Rule where show (MergeRule pr n _) = "merge: " ++ show (pr, show n) show (DiaRule todelete _ ) = "diamond: " ++ 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 (DiscardDownRule todelete) = "Discard: " ++ showLess todelete show (DiscardDiaDoneRule todelete) = "Discard done: " ++ showLess todelete show (DiscardDiaBlockedRule todelete) = "Discard blocked: " ++ showLess todelete show (DiscardDisjTrivialRule todelete) = "Discard trivial: " ++ showLess todelete@@ -83,9 +71,7 @@ (DisjRule _ _) -> R_Disj (SemBrRule _ _) -> R_SemBr (AtRule _ ) -> R_At- (DownRule _) -> R_Down (ExistRule _ _) -> R_Exist- (DiscardDownRule _) -> R_DiscardDown (DiscardDiaDoneRule _) -> R_DiscardDiaDone (DiscardDiaBlockedRule _) -> R_DiscardDiaBlocked (DiscardDisjTrivialRule _) -> R_DiscardDisjTrivial@@ -95,21 +81,20 @@ -- 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 -> StdGen -> Maybe (Rule,Branch, StdGen)-applicableRule br p d g =- case mapMaybe (ruleByChar br p d g) (strategy p) of -- TODO weird to use the same g, but right after we only take the first rule+applicableRule :: Branch -> Params -> Dependency -> Maybe (Rule,Branch)+applicableRule br p d =+ case mapMaybe (ruleByChar br p d) (strategy p) of -- TODO weird to use the same g, but right after we only take the first rule [] -> Nothing- ((rule,newtodo,g'):_) -> Just (rule, br{todoList = newtodo}, g')+ ((rule,newtodo):_) -> Just (rule, br{todoList = newtodo}) -ruleByChar :: Branch -> Params -> Dependency -> StdGen -> Char -> Maybe (Rule,TodoList, StdGen)-ruleByChar br p d g char =+ruleByChar :: Branch -> Params -> Dependency -> Char -> Maybe (Rule,TodoList)+ruleByChar br p d char = case char of 'n' -> applicableMergeRule '|' -> applicableDisjRule '<' -> applicableDiaRule '@' -> applicableAtRule 'E' -> applicableExistRule- 'b' -> applicableDownRule 'r' -> applicableRoleIncRule _ -> error "ruleByChar" where@@ -118,48 +103,35 @@ applicableDiaRule = do (f,new) <- Set.minView $ diaTodo todos if diaAlreadyDone br f- then return ( DiscardDiaDoneRule f, todos{diaTodo = new}, g)+ then return ( DiscardDiaDoneRule f, todos{diaTodo = new}) else if patternBlocked br f- then return ( DiscardDiaBlockedRule f, todos{diaTodo = new}, g)- else return ( DiaRule f d, todos{diaTodo = new}, g)+ then return ( DiscardDiaBlockedRule f, todos{diaTodo = new})+ else return ( DiaRule f d, todos{diaTodo = new}) applicableAtRule = do (f,new) <- Set.minView $ atTodo todos- return (AtRule f, todos{atTodo = new}, g)-- applicableDownRule = do (f,new) <- Set.minView $ downTodo todos- if downAlreadyDone br f- then return (DiscardDownRule f, todos{downTodo = new}, g)- else return (DownRule f, todos{downTodo = new}, g)+ return (AtRule f, todos{atTodo = new}) applicableExistRule = do (f,new) <- Set.minView $ existTodo todos- return (ExistRule f d, todos{existTodo = new}, g)+ return (ExistRule f d, todos{existTodo = new}) applicableRoleIncRule = do ((ds, p1, p2, rs),new) <- Set.minView $ roleIncTodo todos- return (RoleIncRule p1 rs p2 (dsInsert d ds), todos{roleIncTodo = new}, g)+ return (RoleIncRule p1 rs p2 (dsInsert d ds), todos{roleIncTodo = new}) applicableMergeRule = do ((ds,pr,n),new) <- Set.minView $ mergeTodo todos- return (MergeRule pr n ds, todos{mergeTodo = new}, g)+ return (MergeRule pr n 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}, g)+ ((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- | not (CL.random p)- = do (f,new) <- Set.minView $ disjTodo todos- return (disjRule p f br d, todos{disjTodo = new}, g)- | otherwise- = if Set.null s then Nothing- else let (n, g') = randomR (0, Set.size s - 1) g- f = Set.elemAt n s -- pick formula- new = Set.deleteAt n s -- remove from Set- in Just (disjRule p f br d, todos{disjTodo = new}, g')- where s = disjTodo todos+ = 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))@@ -189,12 +161,12 @@ clash@(BranchClash _ _ _ _) >>? _ = clash (BranchOK br) >>? f = f br -applyRule :: Params -> Rule -> Branch -> StdGen -> ([BranchInfo], StdGen)-applyRule p rule br g+applyRule :: Params -> Rule -> Branch -> [BranchInfo]+applyRule p rule br = case rule of DiaRule (PrFormula pr ds (Dia r f)) d -- here, if minimal, branch on all prefixes- | minimal p -> if CL.random p then shuffle g choices else (choices, g)- | otherwise -> (properNewBranch, g)+ | minimal p -> choices+ | otherwise -> properNewBranch where tryAllPrefixes = map reusePrefix $ filter (isNominalUrfather br) [0..lastPref br] reusePrefix pr' =@@ -207,58 +179,43 @@ addFormulas p [PrFormula newPr ds f] >>? addDiaRuleCheck pr (r,f) newPr ]- deps = if CL.random p && minimal p then dsInsert d (dsUnion ds ds2) else dsUnion ds ds2+ deps = dsUnion ds ds2 choices = tryAllPrefixes ++ properNewBranch newPr = lastPref br + 1 (ur,ds2,_) = getUrfatherAndDeps br (DS.Prefix pr) ExistRule (PrFormula _ ds (E f2)) d -- here, if minimal, branch on all prefixes- | minimal p -> if CL.random p then shuffle g choices else (choices, g)- | otherwise -> (properNewBranch, g)+ | minimal p -> choices+ | otherwise -> properNewBranch where tryAllPrefixes = map reusePrefix $ filter (isNominalUrfather br) [0..lastPref br] reusePrefix pr' = addFormulas p [PrFormula pr' (dsInsert d ds) f2] br- properNewBranch = [createNewNode p br >>? addFormulas p [PrFormula newPr deps f2]]- deps = if CL.random p && minimal p then dsInsert d ds else ds+ properNewBranch = [createNewNode p br >>? addFormulas p [PrFormula newPr ds f2]] choices = tryAllPrefixes ++ properNewBranch newPr = lastPref br + 1 DisjRule _ prFormulas- | CL.random p -> shuffle g choices- | otherwise -> (choices, g)+ -> choices where choices = [ addFormulas p [toadd] br | toadd <- prFormulas ] SemBrRule _ prFormulas- | CL.random p -> shuffle g choices- | otherwise -> (choices, g)+ -> choices where choices = [ addFormulas p toadds br | toadds <- go prFormulas [] ] go (hd:tl) negs = (hd:negs):(go tl (negPr hd:negs)) go [] _ = [] LazyBrRule _ pr lit prFormulas ->- ([ doLazyBranching pr lit prFormulas br ], g)+ [ doLazyBranching pr lit prFormulas br ] AtRule (PrFormula _ ds (At n f)) ->- ([ addFormulas p [toadd] br{ nomPrefClasses = equiv }], g)+ [ 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)) ->- case positiveNomOf br pr of -- reuse positive nominal if we can- Nothing -> ( [ createNewNom br >>?- addFormulas p [toadd1, toadd2] >>?- addDownRuleCheck pr f ], g)- where toadd1 = PrFormula pr ds (replaceVar v newNom f2)- toadd2 = PrFormula pr ds $ Lit $ PosLit $ N newNom- newNom = '_':(show $ nextNom br)- Just n' ->- ( [ addFormulas p [PrFormula pr ds (replaceVar v n' f2)] br >>?- addDownRuleCheck pr f ], g)- DiscardDownRule _ -> ([BranchOK br], g)- DiscardDiaDoneRule _ -> ([BranchOK br], g)- DiscardDisjTrivialRule _ -> ([BranchOK br], g)- DiscardDiaBlockedRule f -> ([addToBlockedDias f br], g)+ DiscardDiaDoneRule _ -> [BranchOK br]+ DiscardDisjTrivialRule _ -> [BranchOK br]+ DiscardDiaBlockedRule f -> [addToBlockedDias f br] - ClashDisjRule ds (PrFormula pr ds2 f) -> ([BranchClash br pr (dsUnion ds ds2) f], g)- MergeRule pr n ds -> ([merge p pr ds n br], g)+ ClashDisjRule ds (PrFormula pr ds2 f) -> [BranchClash br pr (dsUnion ds ds2) f]+ MergeRule pr n ds -> [merge p pr ds n br] RoleIncRule p1 rs p2 ds ->- ([addAccFormula p (ds, r, p1, p2) br | r <- rs], g)+ [addAccFormula p (ds, r, p1, p2) br | r <- rs] _ -> error $ "applyRule with bad argument: " ++ show rule disjRule :: Params -> PrFormula -> Branch -> Dependency -> Rule@@ -273,22 +230,3 @@ 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"----- list shuffler--- http://okmij.org/ftp/Haskell/perfect-shuffle.txt --fisherYatesStep :: RandomGen g => (Map.Map Int a, g) -> (Int, a) -> (Map.Map Int a, g)-fisherYatesStep (m, gen) (i, x) = ((Map.insert j x . Map.insert i (m Map.! j)) m, gen')- where- (j, gen') = randomR (0, i) gen--shuffle :: RandomGen g => g -> [a] -> ([a], g)-shuffle gen [] = ([], gen)-shuffle gen l =- toElems $ foldl fisherYatesStep (initial (head l) gen) (numerate (tail l))- where- toElems (x, y) = (Map.elems x, y)- numerate = zip [1..]- initial x gen' = (Map.singleton 0 x, gen')-
src/HTab/Statistics.hs view
@@ -39,8 +39,6 @@ import qualified Control.Monad.State as State(liftIO) import Control.DeepSeq ( NFData, rnf ) -import System.Random- import Data.Map(Map) import qualified Data.Map as Map(insertWith, toList, empty) import Data.List ( intercalate )@@ -49,11 +47,10 @@ data Statistics = Stat{metrics::[Metric], count::Int,- step::Int,- rGen::StdGen}+ step::Int} instance NFData Statistics where- rnf (Stat sM sC sS _) = rnf sM `seq` rnf sC `seq` rnf sS+ rnf (Stat sM sC sS) = rnf sM `seq` rnf sC `seq` rnf sS type StatisticsState a = forall m. (MonadState Statistics m) => m a type StatisticsStateIO a = forall m. (MonadState Statistics m, MonadIO m) => m a@@ -64,23 +61,23 @@ rnf s `seq` s updateStep :: Statistics -> Statistics-updateStep s@(Stat _ _ 0 _) = s+updateStep s@(Stat _ _ 0) = s updateStep stat = stat{count = count stat + 1} needsToPrintOut :: Statistics -> Bool-needsToPrintOut (Stat _ _ 0 _) = False-needsToPrintOut (Stat _ iter toi _) = iter > 0 && iter `mod` toi == 0+needsToPrintOut (Stat _ _ 0) = False+needsToPrintOut (Stat _ iter toi) = iter > 0 && iter `mod` toi == 0 -defaultStats :: StdGen -> Statistics-defaultStats g = Stat{metrics=[closedBranches, ruleApplicationCount],- count=0, step=0, rGen=g}+defaultStats :: Statistics+defaultStats = Stat{metrics=[closedBranches, ruleApplicationCount],+ count=0, step=0} ---------- Monadic Statistics functions follow ------------- -initialStatisticsStateFor :: (MonadState Statistics m) => (m a -> Statistics -> b) -> StdGen+initialStatisticsStateFor :: (MonadState Statistics m) => (m a -> Statistics -> b) -> m a -> b-initialStatisticsStateFor f g = flip f (defaultStats g)+initialStatisticsStateFor f = flip f defaultStats setPrintOutInterval :: Int -> StatisticsState () setPrintOutInterval i = modify $ \s -> s{step = i}
src/HTab/Tableau.hs view
@@ -4,8 +4,8 @@ import System.Console.CmdArgs ( whenLoud ) -import Control.Monad.State(StateT,lift,modify, gets, modify)-import HTab.Statistics(Statistics(rGen),updateStep,printOutMetrics,+import Control.Monad.State(StateT,lift,modify, modify)+import HTab.Statistics(Statistics,updateStep,printOutMetrics, recordClosedBranch,recordFiredRule) import HTab.Branch(BranchInfo(..)) import HTab.CommandLine(backjumping,Params,configureStats)@@ -33,17 +33,15 @@ return $ CLOSED bprs BranchOK br -> do verbose (show br)- g <- gets rGen- case applicableRule br p (depth + 1) g of -- generate new number+ case applicableRule br p (depth + 1) of Nothing -> do verbose ">> Saturated open branch" return $ OPEN $ buildModel br- Just (rule,newBranch, g') ->+ Just (rule,newBranch) -> do verbose $ ">> Rule : " ++ show rule recordFiredRule $ ruleToId rule- let (bis,g'') = applyRule p rule newBranch g'- modify $ \s -> s{rGen = g''}- case bis of -- need to shuffle disjunction order+ let bis = applyRule p rule newBranch+ case bis of [newBi] -> tableauDown p (depth + 1) newBi _ -> tableauRight p (depth + 1) bis dsEmpty
src/htab.hs view
@@ -45,7 +45,7 @@ else return Nothing header :: String-header = unlines ["HTab 1.7.0",+header = unlines ["HTab 1.7.3", "G. Hoffmann, C. Areces, D.Gorin and J. Heguiabehere. (c) 2002-2016.", "http://hub.darcs.net/gh/htab/"]