diff --git a/HTab.cabal b/HTab.cabal --- a/HTab.cabal +++ b/HTab.cabal @@ -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 diff --git a/NEWS b/NEWS --- a/NEWS +++ b/NEWS @@ -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 diff --git a/examples/sat/down01.frm b/examples/sat/down01.frm deleted file mode 100644 --- a/examples/sat/down01.frm +++ /dev/null @@ -1,3 +0,0 @@ -begin -N2 & <>( down N3 . ( N1:(N2 & !N3))) -end diff --git a/examples/sat/spy.frm b/examples/sat/spy.frm deleted file mode 100644 --- a/examples/sat/spy.frm +++ /dev/null @@ -1,5 +0,0 @@ -begin -down (N1 []([]( down( N2 (N1:<>(N2)))))); -[]<>true; -[] (down (N1 (!<>N1))) -end diff --git a/examples/unsat/test35.frm b/examples/unsat/test35.frm deleted file mode 100644 --- a/examples/unsat/test35.frm +++ /dev/null @@ -1,3 +0,0 @@ -begin -down(N1 !N1) -end diff --git a/examples/unsat/test36.frm b/examples/unsat/test36.frm deleted file mode 100644 --- a/examples/unsat/test36.frm +++ /dev/null @@ -1,3 +0,0 @@ -begin -!((down (N1 dia (N1 ^ p1) )) --> p1) -end diff --git a/examples/unsat/test37.frm b/examples/unsat/test37.frm deleted file mode 100644 --- a/examples/unsat/test37.frm +++ /dev/null @@ -1,9 +0,0 @@ -begin -n3:[R3](down (N1 [R1]([R1]( down( N2 (N1:N2)))))) ; -n3:n1; -n3:n2; -n3:n3; -n1:n2; -n2:n3; -n1:!n3 -end diff --git a/examples/unsat/test38.frm b/examples/unsat/test38.frm deleted file mode 100644 --- a/examples/unsat/test38.frm +++ /dev/null @@ -1,4 +0,0 @@ -begin -p1 v <><><><>p1 v down(N1 <>(N1:[]p1)); -A !p1 -end diff --git a/rc/br_infinite.frm b/rc/br_infinite.frm deleted file mode 100644 --- a/rc/br_infinite.frm +++ /dev/null @@ -1,18 +0,0 @@ -signature { -propositions { s } -nominals { } -relations { br, gbr } -} - -theory - -{ - s; - [] false; - [br](s --> [br]!s); - [br](!s --> [] !s); -

true; - [br]<> true; - [br][br](s --> [](!s --> [][]!s)); - [br][][][br](s --> <>( !s & <><>s )); -} diff --git a/rc/br_no_tree.frm b/rc/br_no_tree.frm deleted file mode 100644 --- a/rc/br_no_tree.frm +++ /dev/null @@ -1,12 +0,0 @@ -signature { -propositions { p } -nominals { } -relations { br } -} - -theory - -{ - [] false; -
[] false; -} diff --git a/rc/br_unsat_bad_infinite.frm b/rc/br_unsat_bad_infinite.frm deleted file mode 100644 --- a/rc/br_unsat_bad_infinite.frm +++ /dev/null @@ -1,14 +0,0 @@ -signature { -propositions { s } -nominals { } -relations { br, gbr } -} - -theory - -{ - s; - [] false; - [br](s --> [br]!s); - [br][]!s; -} diff --git a/rc/gbr_no_tree.frm b/rc/gbr_no_tree.frm deleted file mode 100644 --- a/rc/gbr_no_tree.frm +++ /dev/null @@ -1,12 +0,0 @@ -signature { -propositions { p } -nominals { } -relations { sw } -} - -theory - -{ - [] false; - [] false; -} diff --git a/rc/gsab_confluence.frm b/rc/gsab_confluence.frm deleted file mode 100644 --- a/rc/gsab_confluence.frm +++ /dev/null @@ -1,14 +0,0 @@ -signature { -propositions { a, b, c } -nominals { } -relations { gsb } -} - -theory - -{ - <>(a & !b & <><>a ); - <>(b & !a & <><>b ); - [][](c & []!c); - [][][] false; -} diff --git a/rc/gsab_count.frm b/rc/gsab_count.frm deleted file mode 100644 --- a/rc/gsab_count.frm +++ /dev/null @@ -1,13 +0,0 @@ -signature { -propositions { } -nominals { } -relations { gsb } -} - -theory - -{ - true; - [gsb][gsb][gsb][gsb]false; -} - diff --git a/rc/gsab_infinite.frm b/rc/gsab_infinite.frm deleted file mode 100644 --- a/rc/gsab_infinite.frm +++ /dev/null @@ -1,20 +0,0 @@ -signature { -propositions { s } -nominals { } -relations { sb, gsb } -} - -theory - -{ - s; - []!s; - <> true; - []( <>s & !<>s ); - []<>!s; - [][]( !s --> ( <>s & !<>s) ); - [gsb]( (<>(<>s & <>(!s & !<>s)) ) --> <>!<>s); - [gsb][]( (!<>s) --> []<>s ); - [gsb](!<>( (!<>s) & <><>( !s & (<>s) & <>!<>s))); - [gsb][gsb]( (<>((!<>s) & <><>(!s & !<>s))) --> <>(!<>s & <>!<>s)); -} diff --git a/rc/gsab_no_tree.frm b/rc/gsab_no_tree.frm deleted file mode 100644 --- a/rc/gsab_no_tree.frm +++ /dev/null @@ -1,12 +0,0 @@ -signature { -propositions { } -nominals { } -relations { gsb } -} - -theory - -{ - <><> true; - [gsb][] false; -} diff --git a/rc/gswap_infinite.frm b/rc/gswap_infinite.frm deleted file mode 100644 --- a/rc/gswap_infinite.frm +++ /dev/null @@ -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)); -} diff --git a/rc/gswap_no_tree.frm b/rc/gswap_no_tree.frm deleted file mode 100644 --- a/rc/gswap_no_tree.frm +++ /dev/null @@ -1,12 +0,0 @@ -signature { -propositions { } -nominals { } -relations { gsw } -} - -theory - -{ - []false; - <> true; -} diff --git a/rc/mem_br_struct.frm b/rc/mem_br_struct.frm deleted file mode 100644 --- a/rc/mem_br_struct.frm +++ /dev/null @@ -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); - -
(!s & t &
( !s & !t & - a & !b & !c & !d & - <>(!s & !a & b & !c & !d & - <>(!s & !a & !b & c & !d & - <>(!s & !a & !b & !c & d - ))))); - -} diff --git a/rc/mem_br_struct_refl.frm b/rc/mem_br_struct_refl.frm deleted file mode 100644 --- a/rc/mem_br_struct_refl.frm +++ /dev/null @@ -1,18 +0,0 @@ -signature { -propositions { s, t } -nominals { } -relations { br } -} - -theory - -{ - s; - []false; - [br](s --> [br]!s); - [br](!s --> []!s); - -
(!s & t &
( !s & !t & -
(s &
( (<>s) & <>(!s & <>s))) - )); -} diff --git a/rc/mem_sab_struct.frm b/rc/mem_sab_struct.frm deleted file mode 100644 --- a/rc/mem_sab_struct.frm +++ /dev/null @@ -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 ))); -} diff --git a/rc/mem_sab_struct2.frm b/rc/mem_sab_struct2.frm deleted file mode 100644 --- a/rc/mem_sab_struct2.frm +++ /dev/null @@ -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)))); -} diff --git a/rc/mem_sab_struct3.frm b/rc/mem_sab_struct3.frm deleted file mode 100644 --- a/rc/mem_sab_struct3.frm +++ /dev/null @@ -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) )))); -} diff --git a/rc/mem_sab_struct_refl.frm b/rc/mem_sab_struct_refl.frm deleted file mode 100644 --- a/rc/mem_sab_struct_refl.frm +++ /dev/null @@ -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))); - - - <>( (s & ( (!<>s) & <>( (!<>s ) ) ) ) ); -} diff --git a/rc/mem_sw_struct.frm b/rc/mem_sw_struct.frm deleted file mode 100644 --- a/rc/mem_sw_struct.frm +++ /dev/null @@ -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 --> (s & <><>(s & <>!<>s))); - - - <>(!s & a & !b & !c & !d & - <>(!s & !a & b & !c & !d & - <>(!s & !a & !b & c & !d & - <>(!s & !a & !b & !c & d - )))); -} diff --git a/rc/mem_sw_struct_refl.frm b/rc/mem_sw_struct_refl.frm deleted file mode 100644 --- a/rc/mem_sw_struct_refl.frm +++ /dev/null @@ -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 --> (s & <><>(s & <>!<>s))); - - - <>( a & (s & <><>(!s & !<>s))); -} diff --git a/rc/sab_loop.frm b/rc/sab_loop.frm deleted file mode 100644 --- a/rc/sab_loop.frm +++ /dev/null @@ -1,14 +0,0 @@ -signature { -propositions { a, b } -nominals { } -relations { sb } -} - -theory - -{ - <>(a & !b & <><>a); - <>(b & !a & <><>b); - [sb](a --> [][]!a); - [sb](b --> [][]!b); -} diff --git a/rc/sab_loop_diamond.frm b/rc/sab_loop_diamond.frm deleted file mode 100644 --- a/rc/sab_loop_diamond.frm +++ /dev/null @@ -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; -} diff --git a/rc/sab_no_tree.frm b/rc/sab_no_tree.frm deleted file mode 100644 --- a/rc/sab_no_tree.frm +++ /dev/null @@ -1,12 +0,0 @@ -signature { -propositions { } -nominals { } -relations { sb, gsb } -} - -theory - -{ - <><>true; - [sb][]false; -} diff --git a/rc/sab_sat_01.frm b/rc/sab_sat_01.frm deleted file mode 100644 --- a/rc/sab_sat_01.frm +++ /dev/null @@ -1,13 +0,0 @@ -signature { -propositions { p, q } -nominals { } -relations { sb, gsb } -} - -theory - -{ - p; - q; - ( <><> true) ; -} diff --git a/rc/swap_diamond.frm b/rc/swap_diamond.frm deleted file mode 100644 --- a/rc/swap_diamond.frm +++ /dev/null @@ -1,15 +0,0 @@ -signature { -propositions { a, b } -nominals { } -relations { sw } -} - -theory - -{ - <>(a & !b & <>a); - <>(b & !a & <>b); - [sw][][sw][][] false; - [][sw][][] false; - <><><><><> true; -} diff --git a/rc/swap_infinite.frm b/rc/swap_infinite.frm deleted file mode 100644 --- a/rc/swap_infinite.frm +++ /dev/null @@ -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)); -} diff --git a/rc/swap_no_tree.frm b/rc/swap_no_tree.frm deleted file mode 100644 --- a/rc/swap_no_tree.frm +++ /dev/null @@ -1,15 +0,0 @@ -signature { -propositions { p } -nominals { } -relations { sw } -} - -theory - -{ - p; - []!p; - [][]!p; - [][][]!p; - <><>p; -} diff --git a/src/HTab/Branch.hs b/src/HTab/Branch.hs --- a/src/HTab/Branch.hs +++ b/src/HTab/Branch.hs @@ -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 diff --git a/src/HTab/CommandLine.hs b/src/HTab/CommandLine.hs --- a/src/HTab/CommandLine.hs +++ b/src/HTab/CommandLine.hs @@ -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 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 diff --git a/src/HTab/Formula.hs b/src/HTab/Formula.hs --- a/src/HTab/Formula.hs +++ b/src/HTab/Formula.hs @@ -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 diff --git a/src/HTab/Literals.hs b/src/HTab/Literals.hs --- a/src/HTab/Literals.hs +++ b/src/HTab/Literals.hs @@ -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 diff --git a/src/HTab/Main.hs b/src/HTab/Main.hs --- a/src/HTab/Main.hs +++ b/src/HTab/Main.hs @@ -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 -- diff --git a/src/HTab/Memory.hs b/src/HTab/Memory.hs deleted file mode 100644 --- a/src/HTab/Memory.hs +++ /dev/null @@ -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" - diff --git a/src/HTab/RuleId.hs b/src/HTab/RuleId.hs --- a/src/HTab/RuleId.hs +++ b/src/HTab/RuleId.hs @@ -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 diff --git a/src/HTab/Rules.hs b/src/HTab/Rules.hs --- a/src/HTab/Rules.hs +++ b/src/HTab/Rules.hs @@ -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') - diff --git a/src/HTab/Statistics.hs b/src/HTab/Statistics.hs --- a/src/HTab/Statistics.hs +++ b/src/HTab/Statistics.hs @@ -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} diff --git a/src/HTab/Tableau.hs b/src/HTab/Tableau.hs --- a/src/HTab/Tableau.hs +++ b/src/HTab/Tableau.hs @@ -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 diff --git a/src/htab.hs b/src/htab.hs --- a/src/htab.hs +++ b/src/htab.hs @@ -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/"]