HTab 1.6.2 → 1.6.3
raw patch · 13 files changed
+556/−533 lines, 13 filesdep ~containersdep ~deepseqdep ~strict
Dependency ranges changed: containers, deepseq, strict
Files
- HTab.cabal +4/−4
- src/HTab/Branch.hs +130/−122
- src/HTab/CommandLine.hs +2/−0
- src/HTab/DMap.hs +40/−22
- src/HTab/DisjSet.hs +3/−3
- src/HTab/Formula.hs +215/−243
- src/HTab/Literals.hs +20/−19
- src/HTab/Main.hs +76/−57
- src/HTab/ModelGen.hs +18/−18
- src/HTab/Relations.hs +14/−13
- src/HTab/RuleId.hs +1/−0
- src/HTab/Rules.hs +33/−31
- src/htab.hs +0/−1
HTab.cabal view
@@ -1,5 +1,5 @@ Name: HTab-Version: 1.6.2+Version: 1.6.3 Synopsis: Tableau based theorem prover for hybrid logics Description: Tableau based theorem prover for hybrid logics Homepage: http://www.glyc.dc.uba.ar/intohylo/htab.php@@ -42,9 +42,9 @@ HTab.Tableau Build-Depends: base >= 4, base < 5, mtl >= 2, mtl < 3,- containers < 0.4.2,- deepseq < 1.2,- strict < 1,+ containers,+ deepseq,+ strict, cmdargs >= 0.10.1, hylolib == 1.4.* Extensions: GADTs
src/HTab/Branch.hs view
@@ -27,7 +27,6 @@ import Data.IntMap ( IntMap) import qualified Data.IntMap as I -import HTab.DMap ( DMap ) import qualified HTab.DMap as D import qualified HTab.DisjSet as DS import HTab.CommandLine(Params(..))@@ -41,8 +40,8 @@ data BranchInfo = BranchOK Branch | BranchClash Branch Prefix DependencySet Formula -type BoxConstraints = DMap {- Prefix Rel -} [(Formula,DependencySet)]-type BranchingWitnesses = DMap {- Prefix Literal -} [PrFormula]+type BoxConstraints = IntMap {- Prefix -} (Map Rel [(Formula,Depth,DependencySet)])+type BranchingWitnesses = IntMap {- Prefix -} (Map Literal [PrFormula]) type EquivClasses = DS.DisjSet DS.Pointer data Branch =@@ -52,7 +51,7 @@ accStr :: OutRels, -- local and global constraints boxFwd :: BoxConstraints,- univCons :: [(DependencySet,Formula)],+ univCons :: [(DependencySet,Formula,Depth)], -- pending formulas / todo lists todoList :: TodoList, -- saturation of rules@@ -68,14 +67,14 @@ nomPrefClasses :: EquivClasses, -- book keeping lastPref :: Prefix,- nextNom :: Nom,+ nextNom :: Int, -- lazy branching brWitnesses :: BranchingWitnesses, -- information about language of input formula and blocking mode inputLanguage :: LanguageInfo, blockedDias :: IntMap {- Prefix -} [PrFormula], relInfo :: RelInfo,- encoding :: Encoding}+ generators :: [Generator]} -- @@ -97,17 +96,19 @@ "\nPrefix to dependency set: ", showIMap dsShow "\n " (prToDepSet br), "\nPrefix-Nominal classes : ", showMap ", " (nomPrefClasses br), "\nlastPref : ", show (lastPref br),- " nextnom : ", showLit (nextNom br)+ " nextnom : ", show (nextNom br),+ "\ngenerators :", show (generators br),+ "\nRel info:", show (relInfo br), "\n" ] where showIMap :: (a -> String) -> String -> IntMap a -> String- showIMap vShow sep- = I.foldWithKey (\k v -> (++ sep ++ show k ++ " -> " ++ vShow v )) ""+ showIMap vShow sep im+ = I.foldWithKey (\k v -> (++ sep ++ show k ++ " -> " ++ vShow v )) "" im showMap sep = Map.foldrWithKey (\k v -> (++ sep ++ show k ++ " -> " ++ show v )) ""- showMap_lits = I.foldWithKey (\l d -> (++ showLit l ++ " " ++ dsShow d ++ ", ")) ""- showMap_lits2 = I.foldWithKey (\l fs -> (++ showLit l ++ " :" ++ show fs ++ ", ")) ""+ showMap_lits ml = Map.foldrWithKey (\l d -> (++ show l ++ " " ++ dsShow d ++ ", ")) "" ml+ showMap_lits2 = Map.foldrWithKey (\l fs -> (++ show l ++ " :" ++ show fs ++ ", ")) "" showMap_rel- = I.foldWithKey (\r dxs -> (++ "-" ++ showRel r ++ "-> " ++ show dxs ++ ", ")) ""+ = Map.foldrWithKey (\r dxs -> (++ "-" ++ r ++ "-> " ++ show dxs ++ ", ")) "" data TodoList= TodoList{disjTodo :: Set PrFormula, diaTodo :: Set PrFormula,@@ -145,34 +146,34 @@ $ bookKeepFormula p pf br bookKeepFormula :: Params -> PrFormula -> Branch -> Branch-bookKeepFormula p pf_@(PrFormula pr ds f) br+bookKeepFormula p pf_@(PrFormula pr ds md f) br = rescheduleLazyBranching p pf $ rescheduleBlockedDias ur br where (ur,ds2,_) = getUrfatherAndDeps br (DS.Prefix pr) pf = if ur == pr then pf_- else PrFormula ur (dsUnion ds ds2) f+ else PrFormula ur (dsUnion ds ds2) md f rescheduleLazyBranching :: Params -> PrFormula -> Branch -> Branch-rescheduleLazyBranching p (PrFormula pr ds (Lit l)) br -- pr already urfather+rescheduleLazyBranching p (PrFormula pr ds _ (Lit l)) br -- pr already urfather | lazyBranching p && isProp l =- let (Just innerMap) = D.lookup1 pr (brWitnesses br)+ let (Just innerMap) = I.lookup pr (brWitnesses br) in case D.lookup pr l (brWitnesses br) of Just _- -> let innerMap2 = I.delete l innerMap- newBrW = D.insert1 pr innerMap2 (brWitnesses br)- newBr = br{brWitnesses = newBrW}+ -> let innerMap2 = Map.delete l innerMap+ newBrW = I.insert pr innerMap2 (brWitnesses br)+ newBr = br{brWitnesses = newBrW} in newBr -- forget the disjunctions, they are really satisfied Nothing -> case D.lookup pr (negLit l) (brWitnesses br) of Just fs- -> let innerMap2 = I.delete (negLit l) innerMap- newBrW = D.insert1 pr innerMap2 (brWitnesses br)- newBr = br{brWitnesses = newBrW}+ -> let innerMap2 = Map.delete (negLit l) innerMap+ newBrW = I.insert pr innerMap2 (brWitnesses br)+ newBr = br{brWitnesses = newBrW} in foldr addToTodo newBr (map (addDeps ds) fs) --reschedule Nothing@@ -182,13 +183,13 @@ putAwayFormula :: Params -> PrFormula -> Branch -> BranchInfo-putAwayFormula p pf@(PrFormula pr ds f2) br =+putAwayFormula p pf@(PrFormula pr ds md f2) br = case f2 of- Con fs -> addFormulas p (prefix pr ds fs) br+ Con fs -> addFormulas p (prefix pr ds md fs) br Dis _ -> putAwayDisjunction p pf br Dia _ _ -> BranchOK $ addToTodo pf br- Box r f -> addBoxConstraint pr r f ds p br- A f -> addUnivConstraint f ds p br+ Box r f -> addBoxConstraint pr r md f ds p br+ A f -> addUnivConstraint md f ds p br E _ -> BranchOK $ addToTodo pf br At _ _ -> BranchOK $ addToTodo pf br Down _ _ -> BranchOK $ addToTodo pf br@@ -196,13 +197,13 @@ Lit l -> addToLiterals pr ds l br putAwayDisjunction :: Params -> PrFormula -> Branch -> BranchInfo-putAwayDisjunction p pf@(PrFormula pr ds f@(Dis fs)) br+putAwayDisjunction p pf@(PrFormula pr ds md f@(Dis fs)) br | lazyBranching p = case reduceDisjunctionProposeLazy br pr fs of Contradiction dsClash -> BranchClash br pr (dsUnion ds dsClash) f Triviality -> BranchOK br Reduced new_ds disjuncts mProposed- -> let fNew = PrFormula pr (dsUnion ds new_ds) (Dis disjuncts)+ -> let fNew = PrFormula pr (dsUnion ds new_ds) md (Dis disjuncts) -- TODO if there was no reduction, leave ds in case mProposed of@@ -218,18 +219,18 @@ -- assume the tests have been done beforehand, always returns BranchOK doLazyBranching :: Prefix -> Literal -> [PrFormula] -> Branch -> BranchInfo doLazyBranching pr lit pfs br- = case D.lookup1 pr (brWitnesses br) of+ = case I.lookup pr (brWitnesses br) of Nothing -> let newBrW = D.insert pr lit pfs (brWitnesses br) in BranchOK br{brWitnesses = newBrW} Just innerMap- -> case I.lookup lit innerMap of+ -> case Map.lookup lit innerMap of -- assume this is the only place where l or (negLit l) occur- Nothing -> let newInner = I.insert lit pfs innerMap- newBrW = D.insert1 pr newInner (brWitnesses br)+ Nothing -> let newInner = Map.insert lit pfs innerMap+ newBrW = I.insert pr newInner (brWitnesses br) in BranchOK br{brWitnesses = newBrW} Just fs -- assume the test was already done- -> let newInner = I.insert lit (pfs++fs) innerMap- newBrW = D.insert1 pr newInner (brWitnesses br)+ -> let newInner = Map.insert lit (pfs++fs) innerMap+ newBrW = I.insert pr newInner (brWitnesses br) in BranchOK br{brWitnesses = newBrW} @@ -240,7 +241,7 @@ {- todo list functions -} addToTodo :: PrFormula -> Branch -> Branch-addToTodo pf@(PrFormula p ds f2) br =+addToTodo pf@(PrFormula p ds _ f2) br = if alreadyDone then br else brWithSaturation{todoList = newTodoList}@@ -254,8 +255,9 @@ 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,l)+ | isPositiveNom l -> utodo{mergeTodo = Set.insert (ds,p,s) (mergeTodo utodo)}+ where (PosLit (N s)) = l _ -> error $ "addToTodo: " ++ show f2 alreadyDone = case f2 of@@ -265,7 +267,8 @@ Dia _ _ -> False -- test happens when the todo list is processed Dis _ -> False -- test happens when the todo list is processed Lit l- | isPositiveNom l -> inSameClass br p l+ | isPositiveNom l -> inSameClass br p s+ where (PosLit (N s)) = l _ -> error $ "alreadyDone: " ++ show f2 brWithSaturation = case f2 of@@ -276,11 +279,11 @@ rescheduleBlockedDias :: Prefix -> Branch -> Branch rescheduleBlockedDias pr br = foldr addToTodo br2 toAdd- where toAdd = get [] pr (blockedDias br)+ where toAdd = iget [] pr (blockedDias br) br2 = br{blockedDias = I.delete pr $ blockedDias br} addToBlockedDias :: PrFormula -> Branch -> BranchInfo-addToBlockedDias f@(PrFormula pr _ _) br+addToBlockedDias f@(PrFormula pr _ _ _) br = BranchOK br{blockedDias = I.insertWith (++) ur [f] (blockedDias br)} where ur = getUrfather br (DS.Prefix pr) @@ -303,7 +306,7 @@ let oldUr = max ur1 ur2 newUr = min ur1 ur2- literalSlots = mapMaybe (\ur -> D.lookup1 ur (literals br)) [ur1,ur2]+ literalSlots = mapMaybe (\ur -> I.lookup ur (literals br)) [ur1,ur2] currentDeps = dsUnions $ fDs:(map (findDeps br) [ur1,ur2]) newPrToDepSet = I.insert newUr currentDeps (prToDepSet br) newUrfatherSlot = lsAddDeps currentDeps $ lsUnions literalSlots@@ -318,14 +321,14 @@ newLiterals = I.delete oldUr $ I.insert newUr slot $ literals br -- structures that merge- newBoxFwd = D.moveInnerDataDMapPlusDeps fDs (boxFwd br) oldUr newUr+ newBoxFwd = D.moveInnerPlusDeps3 fDs (boxFwd br) oldUr newUr newAccStr = mergePrefixes (accStr br) oldUr newUr fDs newDiaRlCh = moveInMap (diaRlCh br) oldUr newUr Set.union newBlockedDias = moveInMap (blockedDias br) oldUr newUr (++) (newBrWit,unwitnessed) = mergeWitnesses oldUr newUr slot (brWitnesses br) -- structures that combine- mapBoxFwd = map (\idx -> get I.empty idx (boxFwd br) ) [ur1,ur2]+ mapBoxFwd = map (\idx -> iget Map.empty idx (boxFwd br) ) [ur1,ur2] mapAccFwd = map (successors (accStr br)) [ur1,ur2] forms1 = concatMap (boxRule currentDeps) $ combine mapBoxFwd mapAccFwd @@ -345,35 +348,35 @@ mergeWitnesses :: Prefix -> Prefix -> LiteralSlot -> BranchingWitnesses -> (BranchingWitnesses, [PrFormula]) mergeWitnesses oldUr newUr urfatherSlot brWits- =( D.insert1 newUr newDest2 ( D.delete oldUr brWits ), toAdd1 ++ toAdd2 )+ =( I.insert newUr newDest2 ( I.delete oldUr brWits ), toAdd1 ++ toAdd2 ) where- srcInnerMap = get I.empty oldUr brWits- destInnerMap = get I.empty newUr brWits+ srcInnerMap = iget Map.empty oldUr brWits+ destInnerMap = iget Map.empty newUr brWits (newDest1,toAdd1) = mergeWitnessesWitnessesMap srcInnerMap destInnerMap (newDest2,toAdd2) = mergeWitnessesAgainstLiterals newDest1 urfatherSlot -mergeWitnessesWitnessesMap :: IntMap [PrFormula] -> IntMap [PrFormula]- -> (IntMap [PrFormula], [PrFormula])+mergeWitnessesWitnessesMap :: Map Literal [PrFormula] -> Map Literal [PrFormula]+ -> (Map Literal [PrFormula], [PrFormula]) mergeWitnessesWitnessesMap srcWitMap destWitMap- = foldr go (destWitMap,[]) $ I.assocs srcWitMap+ = foldr go (destWitMap,[]) $ Map.assocs srcWitMap where go (l,fs) (destMap,toAddAgain)- = case I.lookup l destMap of- Just fs2 -> (I.insert l (fs2++fs) destMap, toAddAgain)+ = case Map.lookup l destMap of+ Just fs2 -> (Map.insert l (fs2++fs) destMap, toAddAgain) Nothing- -> case I.lookup (negLit l) destMap of+ -> case Map.lookup (negLit l) destMap of -- (negLit l) is just one bit away from l in the map, but we don't use it- Just fs2 -> (I.delete (negLit l) destMap, fs++fs2++toAddAgain)- Nothing -> (I.insert l fs destMap, toAddAgain)+ Just fs2 -> (Map.delete (negLit l) destMap, fs++fs2++toAddAgain)+ Nothing -> (Map.insert l fs destMap, toAddAgain) -mergeWitnessesAgainstLiterals :: IntMap [PrFormula] -> LiteralSlot- -> (IntMap [PrFormula],[PrFormula])+mergeWitnessesAgainstLiterals :: Map Literal [PrFormula] -> LiteralSlot+ -> (Map Literal [PrFormula],[PrFormula]) mergeWitnessesAgainstLiterals witMap ls- = foldr go (witMap,[]) $ I.assocs witMap+ = foldr go (witMap,[]) $ Map.assocs witMap where go (lit,fs) (destMap,toAddAgain)- | lit `I.member` ls = (I.delete lit destMap,toAddAgain)- | negLit lit `I.member` ls = (I.delete lit destMap,fs++toAddAgain)+ | lit `Map.member` ls = (Map.delete lit destMap,toAddAgain)+ | negLit lit `Map.member` ls = (Map.delete lit destMap,fs++toAddAgain) -- same remark as above | otherwise = (destMap,toAddAgain) @@ -382,13 +385,13 @@ -- to a branch as several prefixed formulas with different branching dependencies. -- This functions takes a list of prefixed formulas, looks which inner formulas -- are the same and merge their branching dependencies.-nubAndMergeDeps prfs = namd prfs (Map.empty::Map (Prefix,Formula) DependencySet)+nubAndMergeDeps prfs = namd prfs (Map.empty::Map (Prefix,Formula,Depth) DependencySet) -namd :: [PrFormula] -> Map (Prefix,Formula) DependencySet -> [PrFormula]-namd ((PrFormula p ds f):prfs) theMap =- namd prfs (Map.insertWith dsUnion (p,f) ds theMap)+namd :: [PrFormula] -> Map (Prefix,Formula,Depth) DependencySet -> [PrFormula]+namd ((PrFormula p ds md f):prfs) theMap =+ namd prfs (Map.insertWith dsUnion (p,f,md) ds theMap) -namd [] theMap = map (\((p,f),ds) -> PrFormula p ds f) (Map.assocs theMap)+namd [] theMap = map (\((p,f,md),ds) -> PrFormula p ds md f) (Map.assocs theMap) {- handling nominal urfathers, equivalence classes and dependencies -} @@ -417,89 +420,84 @@ deps = findDeps br ur findDeps :: Branch -> Prefix -> DependencySet-findDeps br pr = get dsEmpty pr (prToDepSet br)+findDeps br pr = iget dsEmpty pr (prToDepSet br) addClassDeps :: Prefix -> DependencySet -> Branch -> Branch addClassDeps pr ds br = br { prToDepSet = I.insertWith dsUnion pr ds (prToDepSet br) } -inSameClass :: Branch -> Prefix -> Int -> Bool+inSameClass :: Branch -> Prefix -> String -> Bool inSameClass br p n- = case fst $ DS.find (DS.Nominal (atom n)) (nomPrefClasses br) of+ = case fst $ DS.find (DS.Nominal n) (nomPrefClasses br) of DS.Nominal _ -> False DS.Prefix p2 -> getUrfather br (DS.Prefix p) == p2 {- box-related constraints -} boxRule :: DependencySet- -> (IntMap {- Rel -} [(Formula,DependencySet)],- IntMap {- Rel -} [(Prefix,DependencySet)] )+ -> (Map Rel [(Formula,Depth,DependencySet)],+ Map Rel [(Prefix,DependencySet)] ) -> [PrFormula] boxRule deps (mapBox, mapAcc)- = [PrFormula p (dsUnions [deps,ds1,ds2]) f |- r1 <- I.keys mapBox,- r2 <- I.keys mapAcc,+ = [PrFormula p (dsUnions [deps,ds1,ds2]) md f |+ r1 <- Map.keys mapBox,+ r2 <- Map.keys mapAcc, r1 == r2,- (f,ds1) <- (I.!) mapBox r1,- (p,ds2) <- (I.!) mapAcc r2 ]+ (f,md,ds1) <- (Map.!) mapBox r1,+ (p,ds2) <- (Map.!) mapAcc r2 ] -addBoxConstraint :: Prefix -> Rel -> Formula -> DependencySet -> Params -> Branch+addBoxConstraint :: Prefix -> Rel -> Depth -> Formula -> DependencySet -> Params -> Branch -> BranchInfo-addBoxConstraint pr_ r f ds p br+addBoxConstraint pr_ r md f ds p br | boxAlreadyDone br pr (r,f) = BranchOK br- | isForward r- = let newBr = br{boxFwd = updateBoxConstr pr r f ds (boxFwd br)}+ | otherwise+ = let newBr = br{boxFwd = updateBoxConstr pr r (md+1) f ds (boxFwd br)} succs = get [] r $ successors (accStr br) pr toAdd = fromTrans ++ fromBox fromTrans = if isTransitive (relInfo br) r- then map (\(pr2,ds2) -> PrFormula pr2 (dsUnion ds ds2) (Box r f)) succs+ then map (\(pr2,ds2) -> PrFormula pr2 (dsUnion ds ds2) md (Box r f)) succs else []- fromBox = map (\(pr2,ds2) -> PrFormula pr2 (dsUnion ds ds2) f) succs+ fromBox = map (\(pr2,ds2) -> PrFormula pr2 (dsUnion ds ds2) (md+1) f) succs -- todo check again with new pattern, create successor if new pattern not realized in addFormulas p toAdd newBr-- | otherwise = error "backwards relation" where pr = getUrfather br (DS.Prefix pr_) -updateBoxConstr :: Prefix -> Rel -> Formula -> DependencySet -> BoxConstraints+updateBoxConstr :: Prefix -> Rel -> Depth -> Formula -> DependencySet -> BoxConstraints -> BoxConstraints-updateBoxConstr p1_ r_ f_ ds_ boxConstr_ =+updateBoxConstr p1_ r_ md_ f_ ds_ boxConstr_ = case I.lookup p1_ boxConstr_ of- Nothing -> I.insert p1_ (I.singleton r_ [(f_,ds_)]) boxConstr_+ Nothing -> I.insert p1_ (Map.singleton r_ [(f_,md_,ds_)]) boxConstr_ Just innerMap ->- case I.lookup r_ innerMap of+ case Map.lookup r_ innerMap of Nothing- -> I.insert p1_ (I.insert r_ [(f_,ds_)] innerMap) boxConstr_+ -> I.insert p1_ (Map.insert r_ [(f_,md_,ds_)] innerMap) boxConstr_ Just innerInnerList- -> I.insert p1_ (I.insert r_ ((f_,ds_):innerInnerList) innerMap) boxConstr_+ -> I.insert p1_ (Map.insert r_ ((f_,md_,ds_):innerInnerList) innerMap) boxConstr_ boxAlreadyDone :: Branch -> Prefix -> (Rel,Formula) -> Bool boxAlreadyDone br ur (r,f)- | isForward r = case ( do inner <- I.lookup ur (boxFwd br)- boxes <- map fst <$> I.lookup r inner- return (f `elem` boxes) ) of- Just True -> True- _ -> False- | otherwise = error "backwards relation"+ = case ( do inner <- I.lookup ur (boxFwd br)+ boxes <- map (\(e,_,_) -> e) <$> Map.lookup r inner+ return (f `elem` boxes) ) of+ Just True -> True+ _ -> False -- accessibility Formulas addAccFormula :: Params -> (DependencySet,Rel,Prefix,Prefix) -> Branch -> BranchInfo addAccFormula p (ds, r, p1_, p2_) br- | isBackwards r = error "backwards relation"- | otherwise -- forward = addFormulas p toAdd newBr where toAdd = transApplications ++ boxApplications transApplications = if isTransitive (relInfo br) r- then map (\(f,ds2) -> PrFormula p2 (dsUnion ds ds2) (Box r f)) toSendFwd+ then map (\(f,md,ds2) -> PrFormula p2 (dsUnion ds ds2) (md+1) (Box r f)) toSendFwd else []- boxApplications = map (\(f,ds2) -> PrFormula p2 (dsUnion ds ds2) f) toSendFwd+ boxApplications = map (\(f,md,ds2) -> PrFormula p2 (dsUnion ds ds2) md f) toSendFwd p1 = getUrfather br (DS.Prefix p1_) p2 = getUrfather br (DS.Prefix p2_)- toSendFwd = get [] r $ get I.empty p1 (boxFwd br)+ toSendFwd = get [] r $ iget Map.empty p1 (boxFwd br) newBr = scheduleInclusionRule p1 p2 r ds $ insertRelationBranch br p1 r p2 ds @@ -542,7 +540,7 @@ -- { f } U { f' | p:[r]f' in branch } -- r has to be forward patternOf :: Branch -> PrFormula -> Set Formula-patternOf br (PrFormula pr _ (Dia r f))+patternOf br (PrFormula pr _ _ (Dia r f)) = Set.insert f boxes where ur = getUrfather br (DS.Prefix pr) boxes = if isTransitive (relInfo br) r@@ -554,7 +552,7 @@ boxesOf :: Branch -> Prefix -> Rel -> Set Formula boxesOf br p r- = set $ map fst $ get [] r $ get I.empty p (boxFwd br)+ = set $ map (\(e,_,_) -> e) $ get [] r $ iget Map.empty p (boxFwd br) findByPattern :: Branch -> Set Formula -> Prefix findByPattern br pattern =@@ -563,30 +561,34 @@ {- modifications done by rule application -} +-- add checks for+-- 1. pattern blocking+-- 2. prefix-level diamond rule saturation addDiaRuleCheck :: Prefix -> (Rel,Formula) -> Prefix -> Branch -> BranchInfo addDiaRuleCheck pr (r,f) newPr br = BranchOK br2- where pattern = patternOf br (PrFormula ur dsEmpty (Dia r f))+ where pattern = patternOf br (PrFormula ur dsEmpty 0 (Dia r f)) br1 = br{patterns = I.insert newPr pattern (patterns br)} br2 = br1{diaRlCh=I.insertWith Set.union ur (Set.singleton (r,f)) (diaRlCh br1)} ur = getUrfather br (DS.Prefix pr) diaAlreadyDone :: Branch -> PrFormula -> Bool-diaAlreadyDone b (PrFormula p _ (Dia r f)) =- case I.lookup ur (diaRlCh b) of- Nothing -> False- Just fset -> Set.member (r,f) fset+diaAlreadyDone b (PrFormula p _ _ (Dia r f)) =+ case I.lookup ur (diaRlCh b) of+ Nothing -> False+ Just fset -> Set.member (r,f) fset where ur = getUrfather b (DS.Prefix p) 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 _ _)) =+downAlreadyDone b (PrFormula p _ _ f@(Down _ _)) = case I.lookup ur (downRlCh b) of Nothing -> False Just fset -> Set.member f fset@@ -594,17 +596,17 @@ downAlreadyDone _ _ = error "down already done : wrong formula kind" -addUnivConstraint :: Formula -> DependencySet -> Params -> Branch -> BranchInfo-addUnivConstraint f ds p br- = addFormulas p [PrFormula pr ds f | pr <- urfathers] newBr- where newBr = br{univCons = (ds,f):(univCons br)}+addUnivConstraint :: Depth -> Formula -> DependencySet -> Params -> Branch -> BranchInfo+addUnivConstraint md f ds p br+ = addFormulas p [PrFormula pr ds (md+1) f | pr <- urfathers] newBr+ where newBr = br{univCons = (ds,f,md+1):(univCons br)} prefs = [0..(lastPref br)] urfathers = filter (isNominalUrfather br) prefs createNewNode :: Params -> Branch -> BranchInfo createNewNode p br = addFormulas p- ( map (\(ds,f) -> PrFormula newPr ds f) univConstraints )+ ( map (\(ds,f,md) -> PrFormula newPr ds md f) univConstraints ) newBrWithRefl where newPr = lastPref br + 1 newBr = br{lastPref = newPr}@@ -618,16 +620,16 @@ createNewNom :: Branch -> BranchInfo createNewNom br- = BranchOK br{nextNom = nextNom br + 4}+ = BranchOK br{nextNom = nextNom br + 1} -- preparation of the branch at the beginning of the calculus: -- - add the input formula at prefix 0 -- - add a nominal formula at a fresh prefix for each nominal of the input language -- (even if the nominal was filtered out during lexical normalisation) -- - add reflexive links for prefixes 0 and nominal witnesses-initialBranch :: Params -> LanguageInfo -> RelInfo -> Encoding -> Formula+initialBranch :: Params -> LanguageInfo -> RelInfo -> [Generator] -> Formula -> BranchInfo-initialBranch p fLang relInfo_ encoding_ f+initialBranch p fLang relInfo_ gs f = addFormulas p [pf] br where pf = firstPrefixedFormula f@@ -638,8 +640,8 @@ initClasses = foldr (\(pr,n) -> DS.union (DS.Prefix pr) (DS.Nominal n)) DS.mkDSet (zip [1..] ns)- initLiterals = foldr (\(pr,n) -> D.insert pr n dsEmpty)- D.empty+ initLiterals = foldr (\(pr,n) -> D.insert pr (PosLit (N n)) dsEmpty)+ I.empty (zip [1..] ns) emptyBr = Branch{ literals = initLiterals,@@ -653,14 +655,14 @@ patterns = I.empty, univCons = [], lastPref = nbNs,- nextNom = maxNom encoding_ + 4,+ nextNom = 0, prToDepSet = I.empty,- brWitnesses = D.empty,+ brWitnesses = I.empty, nomPrefClasses = initClasses, inputLanguage = fLang, blockedDias = I.empty, relInfo = relInfo_,- encoding = encoding_+ generators = gs } addToLiterals :: Prefix -> DependencySet -> Literal -> Branch -> BranchInfo@@ -676,7 +678,8 @@ data ReducedDisjunct = Triviality | Contradiction DependencySet- | Reduced DependencySet (Set Formula) (Maybe Prop) -- proposable witness for lazy branching+ | Reduced DependencySet (Set Formula) (Maybe Literal)+ -- proposable witness for lazy branching deriving Show reduceDisjunctionProposeLazy :: Branch -> Prefix -> Set Formula -> ReducedDisjunct@@ -742,5 +745,10 @@ set :: Ord a => [a] -> Set.Set a set = Set.fromList -get :: a -> Int -> IntMap a -> a-get = I.findWithDefault+iget :: a -> Int -> IntMap a -> a+iget = I.findWithDefault++get :: (Ord k) => a -> k -> Map k a -> a+get = Map.findWithDefault++
src/HTab/CommandLine.hs view
@@ -10,6 +10,7 @@ data Params = Params { filename :: FilePath,+ symfile :: Maybe FilePath, genModel :: Maybe FilePath, dotModel :: Bool, timeout :: Int,@@ -30,6 +31,7 @@ defaultParams = record Params{} [ filename := "" += name "f" += typFile += help "input file",+ symfile := Nothing += name "s" += typFile += help "input symmetries file (not used yet)", genModel := Nothing += name "m" += typFile += help "output model file", dotModel := False += help "output model in dot format (otherwise: hylolib format)", timeout := 0 += name "t" += help "timeout (in seconds, default=none)",
src/HTab/DMap.hs view
@@ -2,12 +2,14 @@ (DMap, empty, flatten, delete, insert, insertWith, (!), insert1, lookup, lookup1, lookupInter,- moveInnerDataDMapPlusDeps )+ moveInnerPlusDeps, moveInnerPlusDeps3 ) where import Data.IntMap ( IntMap ) import qualified Data.IntMap as I+import Data.Map ( Map )+import qualified Data.Map as M import HTab.Formula(DependencySet, dsUnion) @@ -15,68 +17,84 @@ {- a DMap , or double map, is a nesting of two Maps -} -type DMap c = IntMap (IntMap c)+type DMap c = IntMap (Map String c) empty :: DMap c empty = I.empty -insert1 :: Int -> IntMap c -> DMap c -> DMap c+insert1 :: Int -> Map String c -> DMap c -> DMap c insert1 k1 v m = I.insert k1 v m -insert :: Int -> Int -> c -> DMap c -> DMap c+insert :: (Ord k) => Int -> k -> c -> IntMap (Map k c) -> IntMap (Map k c) insert k1 k2 v m = case I.lookup k1 m of- Nothing -> I.insert k1 (I.singleton k2 v) m- Just innerM -> I.insert k1 (I.insert k2 v innerM) m+ Nothing -> I.insert k1 (M.singleton k2 v) m+ Just innerM -> I.insert k1 (M.insert k2 v innerM) m -insertWith :: (c -> c -> c) -> Int -> Int -> c -> DMap c -> DMap c+insertWith :: (c -> c -> c) -> Int -> String -> c -> DMap c -> DMap c insertWith f k1 k2 v m = case I.lookup k1 m of- Nothing -> I.insert k1 (I.singleton k2 v) m- Just innerM -> I.insert k1 (I.insertWith f k2 v innerM) m+ Nothing -> I.insert k1 (M.singleton k2 v) m+ Just innerM -> I.insert k1 (M.insertWith f k2 v innerM) m -flatten :: DMap c -> [((Int,Int),c)]+flatten :: IntMap (Map b c) -> [(Int,b,c)] flatten m = let ambcs = I.assocs m in -- [(a,IntMap c)]- concatMap (\(a_,innerM_) -> map (\(b_,c_) -> ((a_,b_),c_)) (I.assocs innerM_ )) ambcs+ concatMap (\(a_,innerM_) -> map (\(b_,c_) -> (a_,b_,c_)) (M.assocs innerM_ )) ambcs infixl 9 ! -(!) :: DMap c -> Int -> Int -> c-(!) m k1 k2 = (I.!) ( (I.!) m k1 ) k2+(!) :: DMap c -> Int -> String -> c+(!) m k1 k2 = (M.!) ( (I.!) m k1 ) k2 -lookup :: Int -> Int -> DMap c -> Maybe c+lookup :: (Ord k) => Int -> k -> IntMap (Map k c) -> Maybe c lookup k1 k2 m = do innerMap <- I.lookup k1 m- I.lookup k2 innerMap+ M.lookup k2 innerMap -lookup1 :: Int -> DMap c -> Maybe (IntMap c)+lookup1 :: Int -> DMap c -> Maybe (Map String c) lookup1 k1 m = I.lookup k1 m delete :: Int -> DMap c -> DMap c delete k1 m = I.delete k1 m -lookupInter :: Int -> DMap c -> [Int]+lookupInter :: Int -> DMap c -> [String] lookupInter k1 m = case I.lookup k1 m of Nothing -> []- Just innerMap -> I.keys innerMap+ Just innerMap -> M.keys innerMap -- provided two keys of the DMap and a merge function, merge the inner maps of -- both keys using the merge function when needed for inner values -- delete the first inner map -- and add the given dependencies-moveInnerDataDMapPlusDeps :: DependencySet -> DMap [(c,DependencySet)] -> Int -> Int -> DMap [(c,DependencySet)]-moveInnerDataDMapPlusDeps newDeps m origKey destKey+moveInnerPlusDeps :: DependencySet -> DMap [(c,DependencySet)] -> Int -> Int+ -> DMap [(c,DependencySet)]+moveInnerPlusDeps newDeps m origKey destKey = case I.lookup origKey m of Nothing -> m Just origInnerMap- -> let origInnerMapPlusDeps = I.map (addDeps newDeps) origInnerMap+ -> let origInnerMapPlusDeps = M.map (addDeps newDeps) origInnerMap prunedM = I.delete origKey m addDeps newBps = map (\(el,oldBps) -> (el,dsUnion newBps oldBps)) in case I.lookup destKey m of Nothing -> I.insert destKey origInnerMapPlusDeps prunedM Just destInnerMap- -> let mergedInnerMap = I.unionWith (++) origInnerMapPlusDeps destInnerMap+ -> let mergedInnerMap = M.unionWith (++) origInnerMapPlusDeps destInnerMap+ in I.insert destKey mergedInnerMap prunedM++moveInnerPlusDeps3 :: DependencySet -> DMap [(c1,c2,DependencySet)] -> Int -> Int+ -> DMap [(c1,c2,DependencySet)]+moveInnerPlusDeps3 newDeps m origKey destKey+ = case I.lookup origKey m of+ Nothing -> m+ Just origInnerMap+ -> let origInnerMapPlusDeps = M.map (addDeps newDeps) origInnerMap+ prunedM = I.delete origKey m+ addDeps newBps = map (\(el1,el2,oldBps) -> (el1,el2,dsUnion newBps oldBps))+ in case I.lookup destKey m of+ Nothing -> I.insert destKey origInnerMapPlusDeps prunedM+ Just destInnerMap+ -> let mergedInnerMap = M.unionWith (++) origInnerMapPlusDeps destInnerMap in I.insert destKey mergedInnerMap prunedM
src/HTab/DisjSet.hs view
@@ -3,7 +3,7 @@ where import qualified Data.Map as Map-import HTab.Formula ( showLit, Nom )+import HTab.Formula ( Nom ) -- a disjoint-set forest type DisjSet x = Map.Map x x@@ -53,8 +53,8 @@ deriving (Eq) instance Show Pointer where- show (Prefix p) = 'P' : show p- show (Nominal n) = showLit n+ show (Prefix p) = '#' : show p+ show (Nominal n) = n instance Ord Pointer where compare (Prefix i1) (Prefix i2) = compare i1 i2
src/HTab/Formula.hs view
@@ -1,132 +1,94 @@ module HTab.Formula -(Atom, Prop, Nom, Literal,-Rel, Prefix, Formula(..),-DependencySet, Dependency,+(Nom, Prop, Rel, Prefix, Formula(..), Literal(..), Atom(..),+DependencySet, Dependency, Depth, dsUnion, dsUnions, dsInsert, dsMember, dsEmpty, dsMin, dsShow, addDeps, PrFormula(..),showLess, LanguageInfo(..), neg, conj, disj, taut,-prop, nom, formulaLanguageInfo, prefix, negPr,+prop, nom, prefix, negPr, replaceVar, firstPrefixedFormula, parse, simpleParse, Theory, RelInfo, Task,-showRelInfo, showRel, showLit, negLit, isForward, isBackwards,+showRelInfo, negLit, encodeValidityTest, encodeSatTest, encodeRetrieveTask,-HyLoFormula, RelProperty(..), Encoding(..), maxNom, maxProp,-toPropSymbol, toNomSymbol, toRelSymbol,-isTop, isBottom, isPositiveNom, isPositiveProp, isPositive, isNegative,-isNominal, isProp, atom,-invRel, int+HyLoFormula, RelProperty(..),+isPositiveNom, isPositiveProp, isProp+,parseGenerators,Generator,applyGenerators ) where--import Data.Bits (complementBit, testBit, clearBit, (.|.) )+import Debug.Trace import qualified Data.Set as Set-import Data.Set ( Set, unions )+import Data.Set ( Set ) import qualified Data.Map as Map import Data.Map ( Map ) import qualified Data.IntSet as IntSet-import Data.List ( delete, nub, sort )+import Data.List ( delete, nub, intercalate, isPrefixOf ) +import Data.Char ( toUpper )+ import qualified HyLo.Signature.String as S -import HyLo.Signature( HasSignature(..), relSymbols, nomSymbols, propSymbols )+import HyLo.Signature( HasSignature(..), nomSymbols, relSymbols ) import qualified HyLo.InputFile as InputFile import qualified HyLo.InputFile.Parser as P import qualified HyLo.Formula as F import HTab.CommandLine ( Params(..) ) -type Prefix = Int+type Prefix = Int+type Rel = String+type Nom = String+type Prop = String+data Atom = Taut | N String | P String deriving(Eq, Ord)+data Literal = PosLit Atom | NegLit Atom deriving(Eq, Ord) -type Rel = Int+negLit :: Literal -> Literal+negLit (PosLit a) = NegLit a+negLit (NegLit a) = PosLit a -showRel :: Int -> String-showRel x = sign ++ name- where sign = if testBit x 0 then "-" else ""- name = show $ x `div` 2+isPositiveNom, isPositiveProp, isProp :: Literal -> Bool+isPositiveNom (PosLit (N _)) = True+isPositiveNom _ = False+isPositiveProp (PosLit (P _)) = True+isPositiveProp _ = False+isProp (PosLit (P _)) = True+isProp (NegLit (P _)) = True+isProp _ = False +instance Show Atom where+ show (Taut) = "T"+ show (N n) = n+ show (P p) = p -isBackwards, isForward :: Int -> Bool-isBackwards x = testBit x 0-isForward = not . isBackwards+instance Show Literal where+ show (PosLit a) = show a+ show (NegLit a) = '!' : show a data Formula- = Lit Atom+ = Lit Literal | Con (Set Formula) | Dis (Set Formula) | At Nom Formula+ | Down Nom Formula | Box Rel Formula | Dia Rel Formula- | Down Nom Formula | A Formula | E Formula deriving (Eq, Ord) --- convention : bit0 = OFF -> positive literal, negative otherwise--- O : top--- 1 : bottom---- 2 : p0--- 3 : !p0--- 4 : n0--- 5 : !n0---- 6 : p1--- 7 : !p1--- 8 : n1--- 9 : !n1--- ...--type Atom = Int-type Prop = Int-type Nom = Int-type Literal = Int--isTop, isBottom, isPositiveNom, isNominal, isPositiveProp,- isProp, isNegative, isPositive :: Int -> Bool-isTop = (==0)-isBottom = (==1)-isPositiveNom a = ((a `mod` 4) == 0) && (a > 1)-isNominal a = ((a `mod` 4) < 2) && (a > 1)-isPositiveProp a = (a `mod` 4) == 2-isProp a = (a `mod` 4) >= 2-isNegative a = testBit a 0-isPositive = not . isNegative--atom :: Int -> Int-atom x = clearBit x 0--negLit :: Int -> Int-negLit x = complementBit x 0--invRel :: Int -> Int-invRel = negLit--showLit :: Int -> String-showLit n- | isTop n = "True"- | isBottom n = "False"- | otherwise = case n `mod` 4 of- 0 -> "N" ++ show ((n `div` 4) - 1)- 1 -> "!N" ++ show ((n `div` 4) - 1)- 2 -> "P" ++ show (n `div` 4)- 3 -> "!P" ++ show (n `div` 4)- _ -> error "Impossible"- instance Show Formula where- show (Lit a) = showLit a+ show (Lit a) = show a show (Con fs) = "^" ++ show (list fs) show (Dis fs) = "v" ++ show (list fs)- show (At n f) = showLit n ++ ":(" ++ show f ++ ")"- show (Box r f) = "[" ++ showRel r ++ "]" ++ show f- show (Dia r f) = "<" ++ showRel r ++ ">" ++ show f+ show (At n f) = n ++ ":(" ++ show f ++ ")"+ show (Box r f) = "[" ++ r ++ "]" ++ show f+ show (Dia r f) = "<" ++ r ++ ">" ++ show f show (A f) = "A" ++ show f show (E f) = "E" ++ show f- show (Down n f) = "down " ++ showLit n ++ "." ++ show f+ show (Down n f) = "down " ++ n ++ "." ++ show f -- parsing of the input file @@ -134,7 +96,7 @@ type Task = P.InferenceTask type PRelInfo = [P.RelInfo] -type RelInfo = Map Rel [RelProperty]+type RelInfo = Map String [RelProperty] data RelProperty = Reflexive | Transitive | Universal@@ -143,194 +105,138 @@ deriving (Eq, Show, Ord) showRelInfo :: RelInfo -> String-showRelInfo = Map.foldrWithKey (\r v -> (++ " " ++ showRel r ++ " -> " ++ show v )) ""+showRelInfo = Map.foldrWithKey (\r v -> (++ " " ++ show r ++ " -> " ++ show v )) "" -parse :: Params -> String -> (Theory,RelInfo,Encoding,[Task])+parse :: Params -> String -> (Theory,RelInfo,LanguageInfo,[Task]) parse p s- = (theory, relInfo, encoding, tasks)+ = (theory, relInfo, fLang, tasks) where parseOutput = InputFile.myparse s -- direct parse from hylolib- encoding = getEncoding parseOutput pRelInfo = P.relations parseOutput- relInfo = forceProperties p encoding $ convertToOurType pRelInfo encoding- theory = convert relInfo encoding $ P.theory parseOutput+ relInfo = forceProperties p parseOutput $ convertToOurType pRelInfo+ theory = convert relInfo $ P.theory parseOutput tasks = P.tasks parseOutput---data Encoding = Encoding { nomMap :: Map String Int,- propMap :: Map String Int,- relMap :: Map String Int }- deriving Show--maxNom, maxProp :: Encoding -> Int-maxNom e = case Map.elems $ nomMap e of- [] -> 0 -- hackish- els -> maximum els--maxProp e = case Map.elems $ propMap e of- [] -> -2 -- hackish- els -> maximum els--toPropSymbol :: Encoding -> Int -> S.PropSymbol-toPropSymbol e i =- S.PropSymbol $ case Map.lookup (atom i) (invertMap $ propMap e) of- Nothing -> {- new prop symbol -} "new_prop_" ++ show i- Just x -> x--toNomSymbol :: Encoding -> Int -> S.NomSymbol-toNomSymbol e i =- S.NomSymbol $ case Map.lookup (atom i) (invertMap $ nomMap e) of- Nothing -> error $ show e ++ " nom symbol " ++ show i- Just x -> x--toRelSymbol :: Encoding -> Int -> S.RelSymbol-toRelSymbol e i =- case Map.lookup (atom i) (invertMap $ relMap e) of- Nothing -> error $ show e ++ " rel symbol " ++ show i- Just x -> if isForward i then S.RelSymbol x- else error "backwards relations not supported"--invertMap :: (Ord a, Ord b) => Map.Map a b -> Map.Map b a-invertMap = Map.fromList . map (\(a,b) -> (b,a)) . Map.assocs--getEncoding :: P.ParseOutput -> Encoding-getEncoding parseOutput =- Encoding { nomMap = Map.fromList $ zip noms $ map (\n -> 4 + n*4) [0..],- propMap = Map.fromList $ zip props $ map (\p -> 2 + p*4) [0..],- relMap = Map.fromList $ zip rels $ map (\r -> r*2) [0..] } - where- theory = P.theory parseOutput- noms =- map (\(S.NomSymbol n) -> n) $ list $ unions $ map (nomSymbols . getSignature) theory- props =- map (\(S.PropSymbol p) -> p) $ list $ unions $ map (propSymbols . getSignature) theory- rels1 = map fst $ P.relations parseOutput- rels2 =- map (\(S.RelSymbol r) -> r) $ list $ unions $ map (relSymbols . getSignature) theory- rels = nub $ rels1 ++ rels2--nomsOfEncoding :: Encoding -> [Nom]-nomsOfEncoding e = Map.elems (nomMap e)+ fLang = langInfo parseOutput -- add properties specified by the --all-PROP parameters--- in order to work in case of automatic signature, requires--- the list of RelSymbol present in the formula+-- in order to work in case of automatic signature -forceProperties :: Params -> Encoding -> RelInfo -> RelInfo-forceProperties p encoding relI- = foldr addToAll relI rels- where rels = Map.elems $ relMap encoding+forceProperties :: Params -> P.ParseOutput -> RelInfo -> RelInfo+forceProperties p po relI+ = foldr addToAll relI (list rels)+ where+ rels = Set.map (\(S.RelSymbol r) -> up r) $ Set.unions $ map (relSymbols . getSignature) theory addToAll r = Map.insertWith (\c1 c2 -> nub $ c1 ++ c2) r conds conds = map snd $ filter fst [(allTransitive p, Transitive), (allReflexive p, Reflexive )]+ theory = P.theory po -convertToOurType :: PRelInfo -> Encoding -> RelInfo++convertToOurType :: PRelInfo -> RelInfo -- and add for each relation in the formula, the relevant key-convertToOurType prelI e = foldr insertRelProp Map.empty (concatMap convertOne prelI)+convertToOurType prelI = foldr insertRelProp Map.empty (concatMap convertOne prelI) where insertRelProp (rs,pr) = Map.insertWith (++) rs [pr] convertOne (r,props) = concatMap (c r) props- c r P.Reflexive = [(int e r,Reflexive )]+ c r P.Reflexive = [(up r,Reflexive )] c _ P.Symmetric = error "Symmetric not handled"- c r P.Transitive = [(int e r,Transitive )]- c r P.Universal = [(int e r,Universal )]+ c r P.Transitive = [(up r,Transitive )]+ c r P.Universal = [(up r,Universal )] c _ (P.InverseOf _) = error "InverseOf not handled" - c r (P.SubsetOf ss) = [(int e r,SubsetOf [ int e s | s <- ss])]- c r (P.Equals ss) = [(int e r,SubsetOf [ int e s | s <- ss])]- ++ [(int e s,SubsetOf [int e r]) | s <- ss]+ c r (P.SubsetOf ss) = [(up r,SubsetOf [ up s | s <- ss])]+ c r (P.Equals ss) = [(up r,SubsetOf [ up s | s <- ss])]+ ++ [(up s,SubsetOf [up r]) | s <- ss] c _ (P.TClosureOf _) = error "TClosureOf not handled" c _ (P.TRClosureOf _) = error "TRClosureOf not handled" c _ P.Functional = error "Functional not handled" c _ P.Injective = error "Injective not handled" c _ P.Difference = error "Difference not handled" -simpleParse :: Params -> String -> (Theory,RelInfo,Encoding,[Task])+simpleParse :: Params -> String -> (Theory,RelInfo,LanguageInfo) simpleParse p s =- parse p $ "signature { automatic } theory { " ++ removeBeginEnd s ++ "}"+ let (t,r,i,_) = parse p $ "signature { automatic } theory { " ++ removeBeginEnd s ++ "}"+ in (t,r,i) where removeBeginEnd = unwords . delete "begin" . delete "end" . words -convert :: RelInfo -> Encoding -> [F.Formula S.NomSymbol S.PropSymbol S.RelSymbol]+convert :: RelInfo -> [F.Formula S.NomSymbol S.PropSymbol S.RelSymbol] -> Formula-convert relI e = conv_ relI e . foldr (F.:&:) F.Top+convert relI = conv_ relI . foldr (F.:&:) F.Top -conv_ :: RelInfo -> Encoding -> F.Formula S.NomSymbol S.PropSymbol S.RelSymbol+conv_ :: RelInfo -> F.Formula S.NomSymbol S.PropSymbol S.RelSymbol -> Formula-conv_ _ _ F.Top = taut-conv_ _ _ F.Bot = neg taut-conv_ _ e (F.Prop p) = prop e p-conv_ _ e (F.Nom n) = nom e n-conv_ relI e (F.Neg f) = neg $ conv_ relI e f-conv_ relI e (f1 F.:&: f2) = conv_ relI e f1 `conj` conv_ relI e f2-conv_ relI e (f1 F.:|: f2) = conv_ relI e f1 `disj` conv_ relI e f2-conv_ relI e (f1 F.:-->: f2) = conv_ relI e f1 `imp` conv_ relI e f2-conv_ relI e (f1 F.:<-->: f2) = conv_ relI e f1 `dimp` conv_ relI e f2-conv_ relI e (F.Diam r f) = specialiseDia r relI e (conv_ relI e f)-conv_ relI e (F.Box r f) = specialiseBox r relI e (conv_ relI e f)-conv_ relI e (F.At n f) = at e n (conv_ relI e f)-conv_ relI e (F.Down v f) = downArrow e v (conv_ relI e f)-conv_ relI e (F.A f) = univMod (conv_ relI e f)-conv_ relI e (F.E f) = existMod (conv_ relI e f)-conv_ _ _ f = error (show f ++ "not supported")+conv_ _ F.Top = taut+conv_ _ F.Bot = neg taut+conv_ _ (F.Prop p) = prop p+conv_ _ (F.Nom n) = nom n+conv_ relI (F.Neg f) = neg $ conv_ relI f+conv_ relI (f1 F.:&: f2) = conv_ relI f1 `conj` conv_ relI f2+conv_ relI (f1 F.:|: f2) = conv_ relI f1 `disj` conv_ relI f2+conv_ relI (f1 F.:-->: f2) = conv_ relI f1 `imp` conv_ relI f2+conv_ relI (f1 F.:<-->: f2) = conv_ relI f1 `dimp` conv_ relI f2+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") type Connector = Formula -> Formula -specialiseDia :: S.RelSymbol -> RelInfo -> Encoding -> Connector-specialiseDia r relI e = specialise r relI (diamond e, existMod) e+specialiseDia :: String -> RelInfo -> Connector+specialiseDia r relI = specialise r relI (diamond, existMod) -specialiseBox :: S.RelSymbol -> RelInfo -> Encoding -> Connector-specialiseBox r relI e = specialise r relI (box e, univMod) e+specialiseBox :: String -> RelInfo -> Connector+specialiseBox r relI = specialise r relI (box, univMod) -specialise :: S.RelSymbol -> RelInfo -> (S.RelSymbol -> Connector, Connector)- -> Encoding -> Connector-specialise (S.RelSymbol r) relI (relational, global) e+specialise :: String -> RelInfo -> (String -> Connector, Connector)+ -> Connector+specialise r relI (relational, global) | Universal `elem` props = global- | otherwise = relational $ S.RelSymbol r- where props = Map.findWithDefault [] (int e r) relI+ | otherwise = relational r+ where props = Map.findWithDefault [] r relI type HyLoFormula = F.Formula S.NomSymbol S.PropSymbol S.RelSymbol -encodeValidityTest :: RelInfo -> Encoding -> Formula -> [HyLoFormula] -> Formula-encodeValidityTest relI e th fs- = neg $ conj th (convert relI e fs)+encodeValidityTest :: RelInfo -> Formula -> [HyLoFormula] -> Formula+encodeValidityTest relI th fs+ = neg $ conj th (convert relI fs) -encodeSatTest :: RelInfo -> Encoding -> Formula -> [HyLoFormula] -> Formula-encodeSatTest relI e th fs- = conj th (convert relI e fs)+encodeSatTest :: RelInfo -> Formula -> [HyLoFormula] -> Formula+encodeSatTest relI th fs+ = conj th (convert relI fs) -encodeRetrieveTask :: RelInfo -> Encoding -> LanguageInfo -> Formula -> [HyLoFormula]- -> ([Int],[Formula])-encodeRetrieveTask relI e fLang theory fs- = (noms , map (\n -> conj theory (At n (neg $ convert relI e fs))) noms)+encodeRetrieveTask :: RelInfo -> LanguageInfo -> Formula -> [HyLoFormula]+ -> ([String],[Formula])+encodeRetrieveTask relI fLang theory fs+ = (noms , map (\n -> conj theory (At n (neg $ convert relI fs))) noms) where noms = languageNoms fLang -- CONSTRUCTORS {- Atoms -} taut :: Formula-nom :: Encoding -> S.NomSymbol -> Formula-prop :: Encoding -> S.PropSymbol -> Formula+nom :: S.NomSymbol -> Formula+prop :: S.PropSymbol -> Formula -taut = Lit 0-nom e (S.NomSymbol n) = Lit ( nomMap e Map.! n )-prop e (S.PropSymbol p) = Lit ( propMap e Map.! p )+taut = Lit $ PosLit Taut+nom (S.NomSymbol n) = Lit $ PosLit $ N $ up n+prop (S.PropSymbol p) = Lit $ PosLit $ P $ up p {- Modalities -}-box, diamond :: Encoding -> S.RelSymbol -> Formula -> Formula+box, diamond :: String -> Formula -> Formula univMod, existMod :: Formula -> Formula-box e (S.RelSymbol r) = Box $ int e r-diamond e (S.RelSymbol r) = Dia $ int e r+box r = Box r+diamond r = Dia r univMod = A existMod = E -int :: Encoding -> String -> Int-int e s = relMap e Map.! s- {- binder -}-downArrow :: Encoding -> S.NomSymbol -> Formula -> Formula-downArrow e (S.NomSymbol n) = Down (nomMap e Map.! n)+downArrow :: S.NomSymbol -> Formula -> Formula+downArrow (S.NomSymbol n) = Down (up n) {- Hybrid operators -}-at :: Encoding -> S.NomSymbol -> Formula -> Formula-at e (S.NomSymbol n) = At (nomMap e Map.! n)+at :: S.NomSymbol -> Formula -> Formula+at (S.NomSymbol n) = At (up n) {- Conjunction and disjunction -} @@ -381,10 +287,10 @@ | otherwise = c xs isTrue, isFalse :: Formula -> Bool-isTrue (Lit 0) = True-isTrue _ = False-isFalse (Lit 1) = True-isFalse _ = False+isTrue (Lit (PosLit Taut)) = True+isTrue _ = False+isFalse (Lit (NegLit Taut)) = True+isFalse _ = False -- invariant : neg is only called on literals during -- the run of the algorithm@@ -397,43 +303,46 @@ neg (Dia r f) = Box r (neg f) neg (A f) = E (neg f) neg (E f) = A (neg f)-neg (Lit n) = Lit $ negLit n+neg (Lit (PosLit a)) = Lit (NegLit a)+neg (Lit (NegLit a)) = Lit (PosLit a) -- prefixed formula -data PrFormula = PrFormula Prefix DependencySet Formula+type Depth = Int -- modal depth of current formula wrt input formula++data PrFormula = PrFormula Prefix DependencySet Depth Formula deriving Eq instance Show PrFormula where- show (PrFormula pr ds f) = show pr ++ ":" ++ dsShow ds ++ ":" ++ show f+ show (PrFormula pr ds md f) = show pr ++ ":" ++ dsShow ds ++ ":" ++ show md ++ ":" ++ show f showLess :: PrFormula -> String-showLess (PrFormula pr _ f) = show pr ++ ":" ++ show f+showLess (PrFormula pr _ md f) = show pr ++ ":" ++ show (md,f) -prefix :: Prefix -> DependencySet -> Set Formula -> [PrFormula]-prefix p bps fs = [PrFormula p bps formula|formula <- list fs]+prefix :: Prefix -> DependencySet -> Depth -> Set Formula -> [PrFormula]+prefix p bps md fs = [PrFormula p bps md formula|formula <- list fs] firstPrefixedFormula :: Formula -> PrFormula-firstPrefixedFormula = PrFormula 0 dsEmpty+firstPrefixedFormula = PrFormula 0 dsEmpty 0 negPr :: PrFormula -> PrFormula-negPr (PrFormula p ds f) = PrFormula p ds (neg f)+negPr (PrFormula p ds md f) = PrFormula p ds md (neg f) -- formula language -data LanguageInfo = LanguageInfo { languageNoms :: [Int] } -- ascending+data LanguageInfo = LanguageInfo { languageNoms :: [String] } -- ascending instance Show LanguageInfo where- show li = "Input Language:"- ++ "\n|" ++ yesnol "Noms" ( languageNoms li )+ show li = "Input Language:\n|" ++ yesnol "Noms " ( languageNoms li ) where yesnol s l | null l = "no " ++ s- yesnol s l = s ++ concatMap (\l_ -> ", " ++ showLit l_) l+ yesnol s l = s ++ intercalate ", " l -formulaLanguageInfo :: Encoding -> LanguageInfo-formulaLanguageInfo e+langInfo :: P.ParseOutput -> LanguageInfo+langInfo po = LanguageInfo { languageNoms = noms }- where noms = sort $ nomsOfEncoding e+ 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.@@ -451,16 +360,13 @@ Down x f -> Down x (g f) f -> baseCase f -replaceVar :: Int -> Int -> Formula -> Formula-replaceVar v n a@(Lit v2)- | isNominal v2 = if atom v /= atom v2 then a- else Lit $ atom n .|. sign v2- where sign x = if isNegative x then 1 else 0-+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 (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@@ -469,7 +375,7 @@ type DependencySet = IntSet.IntSet instance Ord PrFormula where- compare (PrFormula pr1 ds1 f1) (PrFormula pr2 ds2 f2) =+ compare (PrFormula pr1 ds1 _ f1) (PrFormula pr2 ds2 _ f2) = case dsMin ds1 `compare` dsMin ds2 of LT -> LT GT -> GT@@ -497,10 +403,76 @@ dsShow = show . IntSet.toList addDeps :: DependencySet -> PrFormula -> PrFormula-addDeps ds1 (PrFormula p ds2 f) = PrFormula p (dsUnion ds1 ds2) f+addDeps ds1 (PrFormula p ds2 md f) = PrFormula p (dsUnion ds1 ds2) md f list :: Ord a => Set.Set a -> [a] list = Set.toList set :: Ord a => [a] -> Set.Set a set = Set.fromList++-- symmetries+-- substitution of literals inside of formulas++type Generator = [(Depth,Literal,Literal)]++applyGenerators :: [Generator] -> PrFormula -> [PrFormula]+applyGenerators gens f+ = if null res+ then res+ else trace ("SYM on " ++ showLess f ++ ":" ++ intercalate "," (map showLess res))+ res+ where res = delete f $ nub $ map (\gen -> subst gen f) gens++subst :: Generator -> PrFormula -> PrFormula+subst gen (PrFormula pr ds md f) = PrFormula pr ds md $ substNorm (normGen gen md) f++normGen :: Generator -> Depth -> Generator+normGen g md = [(md1-md,a1,a2) | (md1,a1,a2) <- g, md1 - md >= 0]++substNorm :: Generator -> Formula -> Formula+-- act as if we were at modal depth 0 and generator has been adjusted+substNorm gen (Lit a) = Lit $ genOnLit gen a+substNorm gen (At n f) = At n $ substNorm (normGen gen 1) f+substNorm gen (Box r f) = Box r $ substNorm (normGen gen 1) f+substNorm gen (Dia r f) = Dia r $ substNorm (normGen gen 1) f+substNorm gen (Down n f) = Down n $ substNorm (normGen gen 1) f+substNorm gen (A f) = A $ substNorm (normGen gen 1) f+substNorm gen (E f) = E $ substNorm (normGen gen 1) f+substNorm gen f = composeMap id (substNorm gen) f++genOnLit :: Generator -> Literal -> Literal+genOnLit [] l = l+genOnLit ((d,x,y):g) l+ | d == 0 && x == l = y+ | d == 0 && x == negLit l = negLit y+ | d == 0 && y == l = x+ | d == 0 && y == negLit l = negLit x+ | otherwise = genOnLit g l++parseGenerators :: String -> [Generator]+parseGenerators genString+ = [lineToGen l [] | l <- lines genString,+ not ("%" `isPrefixOf` l),+ not (null l) ]++-- turn such a line into a generator:+-- 4 -2 5, 5 3 5, 0 -6 -3+lineToGen :: String -> Generator -> Generator+lineToGen "" g = g+lineToGen (',':l) g = lineToGen l g+lineToGen l g = let triple = takeWhile (/= ',') l+ remainder = dropWhile (/= ',') l+ [md,l1,l2] = map read $ words triple+ -- we read X for PX or -Y for -PY,+ -- now we need to convert it in atom+ a1 = if l1 < 0+ then NegLit $ P $ "P" ++ show (negate l1)+ else PosLit $ P $ "P" ++ show l1+ a2 = if l2 < 0+ then NegLit $ P $ "P" ++ show (negate l2)+ else PosLit $ P $ "P" ++ show l2+ in lineToGen remainder (g ++ [(md,a1,a2)])++up :: String -> String+up = map toUpper
src/HTab/Literals.hs view
@@ -6,16 +6,15 @@ import Data.IntMap ( IntMap) import qualified Data.IntMap as I--import HTab.DMap ( DMap )-import qualified HTab.DMap as D+import Data.Map ( Map)+import qualified Data.Map as M import Data.List(minimumBy) import Data.Ord ( comparing ) import HTab.Formula -type Literals = DMap {- Prefix Literal -} DependencySet+type Literals = IntMap {- Prefix -} (Map Literal DependencySet) {- functions for literals associated to prefixes -} @@ -24,25 +23,25 @@ -- Insert a literal into a literal slot updateMap :: Literals -> Prefix -> DependencySet -> Literal -> UpdateResult-updateMap ls _ ds l | isTop l = UpdateSuccess ls- | isBottom l = UpdateFailure ds+updateMap ls _ _ (PosLit Taut) = UpdateSuccess ls+updateMap _ _ ds (NegLit Taut) = UpdateFailure ds updateMap ls pre ds l = case I.lookup pre ls of- Nothing -> UpdateSuccess $ I.insert pre (I.singleton l ds) ls+ Nothing -> UpdateSuccess $ I.insert pre (M.singleton l ds) ls Just slot -> case lsUpdate slot l ds of SlotUpdateSuccess updatedSlot -> UpdateSuccess $ I.insert pre updatedSlot ls SlotUpdateFailure failureDeps -> UpdateFailure failureDeps -type LiteralSlot = IntMap {- Literal -} DependencySet+type LiteralSlot = Map Literal DependencySet data SlotUpdateResult = SlotUpdateSuccess LiteralSlot | SlotUpdateFailure DependencySet -- Union a list of literals slots lsUnions :: [LiteralSlot] -> SlotUpdateResult-lsUnions [] = SlotUpdateSuccess I.empty+lsUnions [] = SlotUpdateSuccess M.empty lsUnions [ls] = SlotUpdateSuccess ls lsUnions (ls1:ls2:tl) = case lsUnion ls1 ls2 of@@ -55,7 +54,7 @@ -- earliest dependency is the earliest among all dep. sets that caused the clash lsUnion :: LiteralSlot -> LiteralSlot -> SlotUpdateResult lsUnion ls1 ls2- = uls_helper ls1 (I.assocs ls2)+ = uls_helper ls1 (M.assocs ls2) where uls_helper :: LiteralSlot -> [(Literal,DependencySet)] -> SlotUpdateResult uls_helper ls l_ds_s =@@ -79,12 +78,12 @@ -- Insert a piece of information in a literal slot lsUpdate :: LiteralSlot -> Literal -> DependencySet -> SlotUpdateResult-lsUpdate ls l ds | isTop l = SlotUpdateSuccess ls- | isBottom l = SlotUpdateFailure ds+lsUpdate ls (PosLit Taut) _ = SlotUpdateSuccess ls+lsUpdate _ (NegLit Taut) ds = SlotUpdateFailure ds lsUpdate ls l ds -- nominals, propositional symbols- = case I.lookup (negLit l) ls of+ = case M.lookup (negLit l) ls of Just ds2 -> SlotUpdateFailure $ dsUnion ds ds2- Nothing -> SlotUpdateSuccess $ I.insertWith mergeDeps l ds ls+ Nothing -> SlotUpdateSuccess $ M.insertWith mergeDeps l ds ls where mergeDeps d1 d2 = if dsMin d1 < dsMin d2 then d1 else d2 -- if the same information is caused by an earlier -- branching, only keep the information of the earliest@@ -95,20 +94,22 @@ lsAddDeps :: DependencySet -> SlotUpdateResult -> SlotUpdateResult lsAddDeps ds res_ls = case res_ls of- SlotUpdateSuccess ls -> SlotUpdateSuccess $ I.map (dsUnion ds) ls+ SlotUpdateSuccess ls -> SlotUpdateSuccess $ M.map (dsUnion ds) ls failure -> failure lsQuery :: Literals -> Prefix -> Literal -> Maybe (Bool,DependencySet) -- Output : Nothing = nevermind -- Just True = already there -- Just False = contrary there-lsQuery _ _ l | isTop l = Just (True,dsEmpty)- | isBottom l = Just (False,dsEmpty)+lsQuery _ _ (PosLit Taut) = Just (True,dsEmpty)+lsQuery _ _ (NegLit Taut) = Just (False,dsEmpty) lsQuery lits pr l- = case D.lookup pr l lits of+ = case dlookup pr l lits of Just ds -> Just (True,ds)- Nothing -> case D.lookup pr (negLit l) lits of+ Nothing -> case dlookup pr (negLit l) lits of Just ds -> Just (False,ds) Nothing -> Nothing + where dlookup pr_ l_ lits_ = do slot <- I.lookup pr_ lits_+ M.lookup l_ slot
src/HTab/Main.hs view
@@ -16,46 +16,72 @@ import HyLo.InputFile.Parser ( QueryType(..) ) -import HTab.CommandLine( filename, timeout, Params, genModel, dotModel, showFormula )+import HTab.CommandLine( filename, symfile,+ timeout, Params, genModel, dotModel, showFormula ) import HTab.Branch( BranchInfo(..), initialBranch) import HTab.Statistics( Statistics, initialStatisticsStateFor, printOutMetricsFinal ) import HTab.Tableau( OpenFlag(..), tableauStart )-import HTab.Formula( formulaLanguageInfo, Theory, RelInfo, Encoding, Task,+import HTab.Formula( Theory, RelInfo, LanguageInfo, Task, Formula, encodeValidityTest, encodeSatTest, encodeRetrieveTask,- toNomSymbol, showRelInfo )+ showRelInfo, parseGenerators ) import qualified HTab.Formula as F+import qualified HyLo.Signature.String as S import HTab.ModelGen ( Model, toDot ) data TaskRunFlag = SUCCESS | FAILURE runWithParams :: Params -> IO (Maybe TaskRunFlag) runWithParams p =- time "Total time: "- $ do- let parse i = if head (words i) == "begin"- then F.simpleParse p i else F.parse p i- allTasks <- parse <$> readFile (filename p)- --- result <- if timeout p == 0- then Just <$> runTasks allTasks p- else T.timeout (timeout p * (10::Int)^(6::Int))- (runTasks allTasks p)- --- case result of- Nothing -> myPutStrLn "\nTimeout.\n"- Just SUCCESS -> myPutStrLn "\nAll tasks successful.\n"- Just FAILURE -> myPutStrLn "\nOne task failed.\n"- --- return result+ time "Total time: " $ do+ i <- readFile (filename p)+ if head (words i) == "begin"+ then do+ let (f,relInfo,fLang) = F.simpleParse p i+ when (showFormula p) $+ myPutStrLn $+ unlines ["Input for SAT test:",+ "{ " ++ show f ++ " }",+ "End of input",+ "Relations properties :" ++ showRelInfo relInfo ]+ --+ gs <- parseGenerators <$> maybe (return "") readFile (symfile p) -- read symmetries+ --+ tResult <- inTimeout (timeout p) $+ do (result,s) <- tableauInit p $+ initialBranch p fLang relInfo gs f+ whenNormal $ printOutMetricsFinal s+ return result+ --+ case tResult of+ Nothing -> do myPutStrLn "\nTimeout.\n" >> return Nothing+ Just (OPEN m) -> do myPutStrLn "The formula is satisfiable."+ saveGenModel (genModel p) p m+ return (Just SUCCESS)+ Just (CLOSED _) -> do myPutStrLn "The formula is unsatisfiable."+ return (Just FAILURE)+ else do+ let allTasks = F.parse p i+ result <- inTimeout (timeout p) (runTasks allTasks p)+ --+ case result of+ Nothing -> myPutStrLn "\nTimeout.\n"+ Just SUCCESS -> myPutStrLn "\nAll tasks successful.\n"+ Just FAILURE -> myPutStrLn "\nOne task failed.\n"+ --+ return result +inTimeout :: Int -> IO a -> IO (Maybe a)+inTimeout 0 action = Just <$> action+inTimeout t action = T.timeout (t * (10::Int)^(6::Int)) action+ -- -runTasks :: (Theory,RelInfo,Encoding,[Task]) -> Params -> IO TaskRunFlag-runTasks allTasks@(theory,relInfo,encoding,tasks) p =+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 encoding theory p+ res <- time "Task time:" $+ runTask (Satisfiable, genModel p, []) relInfo fLang theory p case res of SUCCESS | null tasks -> return SUCCESS | otherwise -> do myPutStrLn "\n== Starting tasks =="@@ -66,48 +92,44 @@ -- -runTasks2 :: (Theory,RelInfo,Encoding,[Task]) -> Params -> IO TaskRunFlag+runTasks2 :: (Theory,RelInfo,LanguageInfo,[Task]) -> Params -> IO TaskRunFlag runTasks2 (_,_,_,[]) _ = error "runTasks2 empty list error"-runTasks2 (theory,relInfo,encoding,(hd:tl)) p =- do res <- time "Task time:" $ runTask hd relInfo encoding theory p+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,encoding,tl) p- FAILURE -> do _ <- runTasks2 (theory,relInfo,encoding,tl) p+ | otherwise -> runTasks2 (theory,relInfo,fLang,tl) p+ FAILURE -> do _ <- runTasks2 (theory,relInfo,fLang,tl) p return FAILURE -- -runTask :: Task -> RelInfo -> Encoding -> Formula -> Params -> IO TaskRunFlag-runTask (Retrieve,mOutFile,fs) relInfo encoding theory p =+runTask :: Task -> RelInfo -> LanguageInfo -> Formula -> Params -> IO TaskRunFlag+runTask (Retrieve,mOutFile,fs) relInfo fLang theory p = do myPutStrLn "\n* Instance retrieval task"- let fLang = formulaLanguageInfo encoding- let (noms,encfs) = encodeRetrieveTask relInfo encoding fLang theory fs+ let (noms,encfs) = encodeRetrieveTask relInfo fLang theory fs -- myPutStrLn $ "Instances making true: " ++ show fs --- results <- mapM (tableauInit p . initialBranch p fLang relInfo encoding) encfs- let goods = [ toNomSymbol encoding n | (n,(CLOSED _ ,_)) <- zip noms results]+ results <- mapM (tableauInit p . initialBranch p fLang relInfo []) encfs+ let goods = [ S.NomSymbol n | (n,(CLOSED _ ,_)) <- zip noms results] myPutStrLn $ show goods let doWrite f = do writeFile f (show goods ++ "\n") myPutStrLn ("Nominals saved as " ++ f) maybe (return ()) doWrite mOutFile return SUCCESS -runTask (Satisfiable,mOutFile,fs) relInfo encoding theory p =+runTask (Satisfiable,mOutFile,fs) relInfo fLang theory p = do myPutStrLn "\n* Satisfiability task"- let f = encodeSatTest relInfo encoding theory fs- --- when (showFormula p)- $ myPutStrLn- $ unlines ["Input for SAT test:",- "{ " ++ show f ++ " }",- "End of input",- "Relations properties :" ++ showRelInfo relInfo ]+ let f = encodeSatTest relInfo theory fs --- let fLang = formulaLanguageInfo encoding+ when (showFormula p) $+ myPutStrLn $ unlines ["Input for SAT test:",+ "{ " ++ show f ++ " }",+ "End of input",+ "Relations properties :" ++ showRelInfo relInfo ] --- (result,stats) <- tableauInit p $ initialBranch p fLang relInfo encoding f+ (result,stats) <- tableauInit p $ initialBranch p fLang relInfo [] f -- whenNormal $ printOutMetricsFinal stats --@@ -118,20 +140,17 @@ CLOSED _ -> do myPutStrLn "The formula is unsatisfiable." return FAILURE -runTask (Valid,mOutFile,fs) relInfo encoding theory p =+runTask (Valid,mOutFile,fs) relInfo fLang theory p = do myPutStrLn "\n* Validity task"- let f = encodeValidityTest relInfo encoding theory fs- --- when (showFormula p)- $ myPutStrLn- $ unlines ["Input for SAT test:",- "{ " ++ show f ++ " }",- "End of input",- "Relations properties :" ++ showRelInfo relInfo ]+ let f = encodeValidityTest relInfo theory fs --- let fLang = formulaLanguageInfo encoding+ when (showFormula p) $+ myPutStrLn $ unlines ["Input for SAT test:",+ "{ " ++ show f ++ " }",+ "End of input",+ "Relations properties :" ++ showRelInfo relInfo ] --- (result,stats) <- tableauInit p $ initialBranch p fLang relInfo encoding f+ (result,stats) <- tableauInit p $ initialBranch p fLang relInfo [] f -- whenNormal $ printOutMetricsFinal stats --
src/HTab/ModelGen.hs view
@@ -12,9 +12,9 @@ import qualified HyLo.Signature.String as S -import HTab.Formula( PrFormula(..), Formula(..),- Prefix, Rel, LanguageInfo(..), Encoding, int,- RelInfo, toPropSymbol, toNomSymbol, toRelSymbol, isPositiveProp )+import HTab.Formula( PrFormula(..), Formula(..), Literal(..), Atom(..),+ Prefix, Rel, LanguageInfo(..),+ RelInfo, isPositiveProp ) import HTab.Branch( Branch(..), prefixes, getUrfather, patternOf, findByPattern, isInTheModel, getModelRepresentative,@@ -27,14 +27,13 @@ buildModel :: Branch -> Model buildModel br =- completeTrans e (relInfo br) $ inducedModel $ H.herbrand es ps rs+ completeTrans (relInfo br) $ inducedModel $ H.herbrand es ps rs where- e = encoding br bias = if null $ languageNoms $ inputLanguage br then 0 else 1 + length ( languageNoms $ inputLanguage br ) es = Set.fromList $- [(S.NomSymbol $ show (getUrfather br (DS.Nominal n) + bias), toNomSymbol e n)+ [(S.NomSymbol $ show (getUrfather br (DS.Nominal n) + bias), S.NomSymbol n) | n <- languageNoms $ inputLanguage br] ++ [(S.NomSymbol $ show (p + bias), S.NomSymbol $ show (p + bias)) | p <- prefixes br, isInTheModel br p]@@ -44,36 +43,37 @@ [ (pr, r, pr2) | pr <- prefixes br, isInTheModel br pr,- blockedDia@(PrFormula _ _ (Dia r _)) <- get [] pr (blockedDias br),+ blockedDia@(PrFormula _ _ _ (Dia r _)) <- get [] pr (blockedDias br), let pat = patternOf br blockedDia, let pr2 = findByPattern br pat ] rels = (allRels $ accStr br) ++ pbBlocked inModel = flip getModelRepresentative rs = Set.fromList- $ map (toSimpSig e)+ $ map toSimpSig $ map (\(p1,r,p2) -> ((p1 `inModel` br) + bias , r,(p2 `inModel` br) + bias)) rels -toSimpSig :: Encoding -> (Prefix,Rel,Prefix) -> (S.NomSymbol,S.RelSymbol,S.NomSymbol)-toSimpSig e (p1,r,p2) = (S.NomSymbol (show p1), toRelSymbol e r, S.NomSymbol (show p2))+toSimpSig :: (Prefix,Rel,Prefix) -> (S.NomSymbol,S.RelSymbol,S.NomSymbol)+toSimpSig (p1,r,p2) = (S.NomSymbol (show p1), S.RelSymbol r, S.NomSymbol (show p2)) prefixAndProps :: Branch -> [(Prefix,S.PropSymbol)] prefixAndProps br =- [(pr, toPropSymbol e p_) | (pr , p_) <- prPosLitProp ++ prefWitPositive]+ [(pr, S.PropSymbol s) | (pr , p_) <- prPosLitProp ++ prefWitPositive,+ let (PosLit (P s)) = p_ ] where litsRelevant = I.filterWithKey (\k _ -> isInTheModel br k) (literals br)- prPosLitProp = filter (isPositiveProp . snd) $ map fst $ flatten $ litsRelevant+ prPosLitProp = [ (a,b) | (a,b,_) <- flatten litsRelevant, + isPositiveProp b ] -- witMap = brWitnesses br witMapRelevant = I.filterWithKey (\k _ -> isInTheModel br k) witMap- prefWitPositive = filter (isPositiveProp . snd) $ map fst $ flatten $ witMapRelevant- --- e = encoding br+ prefWitPositive = [ (a,b) | (a,b,_) <- flatten witMapRelevant,+ isPositiveProp b ] -completeTrans :: Encoding -> RelInfo -> Model -> Model-completeTrans e relI m+completeTrans :: RelInfo -> Model -> Model+completeTrans relI m = m{M.succs = \rs@(S.RelSymbol r) w- -> if isTransitive relI (int e r)+ -> if isTransitive relI r then getTransClos (M.succs m) rs w else M.succs m rs w}
src/HTab/Relations.hs view
@@ -8,6 +8,8 @@ import qualified Data.IntMap as I import Data.IntMap ( IntMap )+import qualified Data.Map as M+import Data.Map ( Map ) import qualified Data.List as List @@ -26,43 +28,42 @@ null = I.null allRels :: OutRels -> [(Prefix,Rel,Prefix)]-allRels rels = [ (p1,r,p2) | ((p1,r),ds_out_s) <- D.flatten rels,+allRels rels = [ (p1,r,p2) | (p1,r,ds_out_s) <- D.flatten rels, (p2,_) <- ds_out_s ] linksFromTo :: OutRels -> Prefix -> Prefix -> [Rel] linksFromTo rels p1 p2 = List.nub [ r | (pa,r,pb) <- allRels rels, pa == p1, pb == p2] -successors :: OutRels -> Prefix -> IntMap {- Rel -} [(Prefix,DependencySet)]-successors rels p = I.findWithDefault I.empty p rels+successors :: OutRels -> Prefix -> Map Rel [(Prefix,DependencySet)]+successors rels p = I.findWithDefault M.empty p rels -- assumes you never add twice the same relation insertRelation :: OutRels -> Prefix -> Rel -> Prefix -> DependencySet -> OutRels insertRelation rels p1 r p2 ds = case I.lookup p1 rels of- Nothing -> I.insert p1 (I.singleton r [(p2,ds)]) rels+ Nothing -> I.insert p1 (M.singleton r [(p2,ds)]) rels Just inner- -> case I.lookup r inner of- Nothing -> I.insert p1 (I.insert r [(p2,ds)] inner) rels- Just innerList -> I.insert p1 (I.insert r ((p2,ds):innerList) inner) rels+ -> case M.lookup r inner of+ Nothing -> I.insert p1 (M.insert r [(p2,ds)] inner) rels+ Just innerList -> I.insert p1 (M.insert r ((p2,ds):innerList) inner) rels mergePrefixes :: OutRels -> Prefix -> Prefix -> DependencySet -> OutRels mergePrefixes r pr ur _ | pr == ur = r-mergePrefixes r pr ur ds = D.moveInnerDataDMapPlusDeps ds r pr ur+mergePrefixes r pr ur ds = D.moveInnerPlusDeps ds r pr ur showRels :: OutRels -> String-showRels r = "\nRelations: " ++- prettyShowMap_ r (\v -> "(" ++ prettyShowMap_rel_bps_x v ++ ")") "\n "+showRels r = prettyShowMap_ r (\v -> "(" ++ prettyShowMap_rel_bps_x v ++ ")") "\n " prettyShowMap_ :: (Show y) => IntMap y -> (y -> String) -> String -> String prettyShowMap_ m valueShow separator = List.intercalate separator $ map (\(k,v) -> show k ++ " -> " ++ valueShow v) $ I.toList m -prettyShowMap_rel_bps_x :: (Show a) => IntMap {- Rel -} [(a,DependencySet)] -> String+prettyShowMap_rel_bps_x :: (Show a) => Map Rel [(a,DependencySet)] -> String prettyShowMap_rel_bps_x m = List.intercalate ", "- $ map (\(r,x_bp_s) -> (++) ("-" ++ show r ++ "-> ") $ List.intercalate ", "+ $ map (\(r,x_bp_s) -> (++) ("-" ++ r ++ "-> ") $ List.intercalate ", " $ map (\(x,bp) -> show x ++ " " ++ dsShow bp) x_bp_s )- $ I.toList m+ $ M.toList m
src/HTab/RuleId.hs view
@@ -47,6 +47,7 @@ | R_DiscardDown | R_DiscardDiaDone | R_DiscardDiaBlocked+ | R_DiscardDiaSymBlocked | R_DiscardDiaX | R_DiscardDisjTrivial | R_ClashDisj -- Branch clash
src/HTab/Rules.hs view
@@ -10,8 +10,8 @@ import HTab.Formula( Formula(..), PrFormula(..), showLess, Dependency, DependencySet, dsUnion, dsInsert, prefix, Rel, negPr,- Prefix, Nom, showLit,- replaceVar, Literal )+ Prefix, Nom, Atom(..),+ replaceVar, Literal(..)) import HTab.Branch( Branch(..), BranchInfo(..), TodoList(..), -- for rules createNewNode, createNewNom,@@ -28,7 +28,8 @@ ReducedDisjunct(..) ) import HTab.CommandLine(Params, UnitProp(..),- lazyBranching, semBranch, unitProp, strategy)+ lazyBranching, semBranch, unitProp,+ strategy) import HTab.RuleId(RuleId(..)) import qualified HTab.DisjSet as DS @@ -51,7 +52,7 @@ instance Show Rule where- show (MergeRule pr n _) = "merge: " ++ show (pr, showLit n)+ 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@@ -112,9 +113,10 @@ = do (f,new) <- Set.minView $ diaTodo todos if diaAlreadyDone br f then return ( DiscardDiaDoneRule f, todos{diaTodo = new})- else if patternBlocked br f- then return ( DiscardDiaBlockedRule f, todos{diaTodo = new})- else return ( DiaRule f, todos{diaTodo = new})+ else+ if patternBlocked br f+ then return ( DiscardDiaBlockedRule f, todos{diaTodo = new})+ else return ( DiaRule f, todos{diaTodo = new}) applicableAtRule = do (f,new) <- Set.minView $ atTodo todos return (AtRule f, todos{atTodo = new}) applicableDownRule = do (f,new) <- Set.minView $ downTodo todos@@ -143,18 +145,18 @@ 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))+makeInteresting p br d df@(PrFormula pr ds md (Dis fs)) = case reduceDisjunctionProposeLazy br pr fs of Triviality -> Just (DiscardDisjTrivialRule df,df) Contradiction ds_clash -> Just (ClashDisjRule (dsUnion ds ds_clash) df,df) Reduced new_ds disjuncts mProposed | Set.size disjuncts == 1- -> Just (DisjRule df ( prefix ur newDeps disjuncts ), df)+ -> Just (DisjRule df ( prefix ur newDeps md disjuncts ), df) | lazyBranching p -> case mProposed of Nothing -> Nothing Just lit- -> Just (LazyBrRule df ur lit [PrFormula ur newDeps (Dis disjuncts)],+ -> Just (LazyBrRule df ur lit [PrFormula ur newDeps md (Dis disjuncts)], df) | otherwise -> Nothing where newDeps = dsInsert d $ dsUnion ds new_ds@@ -173,57 +175,57 @@ applyRule :: Params -> Rule -> Branch -> [BranchInfo] applyRule p rule br = case rule of- DiaRule (PrFormula pr ds (Dia r f))- -> [ addAccFormula p (dsUnion ds ds2, r, ur, newPr) br >>?- addFormulas p [PrFormula newPr ds f] >>?- addDiaRuleCheck pr (r,f) newPr >>?- createNewNode p ]+ DiaRule (PrFormula pr ds md (Dia r f))+ -> [ createNewNode p br >>?+ addAccFormula p (dsUnion ds ds2, r, ur, newPr) >>?+ addFormulas p [PrFormula newPr ds (md+1) f] >>?+ addDiaRuleCheck pr (r,f) newPr ] where newPr = lastPref br + 1 (ur,ds2,_) = getUrfatherAndDeps br (DS.Prefix pr) DisjRule _ prFormulas -> [ addFormulas p [toadd] br | toadd <- prFormulas ] SemBrRule _ prFormulas -> [ addFormulas p toadds br | toadds <- go prFormulas [] ]- where go (hd:tl) negs = (hd:negs):(go tl (negPr hd:negs))- go [] _ = []+ where+ go (hd:tl) negs = (hd:negs):(go tl (negPr hd:negs))+ go [] _ = [] LazyBrRule _ pr lit prFormulas -> [ doLazyBranching pr lit prFormulas br ]- AtRule (PrFormula _ ds (At n f)) ->+ AtRule (PrFormula _ ds md (At n f)) -> [ addFormulas p [toadd] br{ nomPrefClasses = equiv }] where (ur,ds2,equiv) = getUrfatherAndDeps br (DS.Nominal n)- toadd = PrFormula ur (dsUnion ds ds2) f- DownRule (PrFormula pr ds f@(Down v f2)) ->+ toadd = PrFormula ur (dsUnion ds ds2) (md+1) f+ DownRule (PrFormula pr ds md f@(Down v f2)) -> [ createNewNom br >>? addFormulas p [toadd1, toadd2] >>? addDownRuleCheck pr f ]- where toadd1 = PrFormula pr ds (replaceVar v newNom f2)- toadd2 = PrFormula pr ds $ Lit newNom- newNom = nextNom br- ExistRule (PrFormula _ ds (E f2)) ->- [addFormulas p [toadd] br >>? createNewNode p]- where toadd = PrFormula newPr ds f2+ where toadd1 = PrFormula pr ds (md+1) (replaceVar v newNom f2)+ toadd2 = PrFormula pr ds (md+1) $ Lit $ PosLit $ N newNom+ newNom = '_':(show $ nextNom br)+ ExistRule (PrFormula _ ds md (E f2)) ->+ [createNewNode p br >>? addFormulas p [toadd]]+ where toadd = PrFormula newPr ds (md+1) f2 newPr = lastPref br + 1 DiscardDownRule _ -> [BranchOK br] DiscardDiaDoneRule _ -> [BranchOK br] DiscardDisjTrivialRule _ -> [BranchOK br] DiscardDiaBlockedRule f -> [addToBlockedDias f br] - ClashDisjRule ds (PrFormula pr ds2 f) -> [BranchClash br pr (dsUnion ds ds2) f]+ 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] _ -> error $ "applyRule with bad argument: " ++ show rule disjRule :: Params -> PrFormula -> Branch -> Dependency -> Rule-disjRule p df@(PrFormula pr ds (Dis fs)) br d+disjRule p df@(PrFormula pr ds md (Dis fs)) br d = if unitProp p == UPNo- then rule df $ prefix pr (dsInsert d ds) fs+ then rule df $ prefix pr (dsInsert d ds) md fs else case reduceDisjunctionProposeLazy br pr fs of Triviality -> DiscardDisjTrivialRule df Contradiction ds_clash -> ClashDisjRule (dsUnion ds ds_clash) df Reduced new_ds disjuncts _- -> rule df (prefix pr (dsInsert d $ dsUnion ds new_ds) disjuncts)+ -> rule df (prefix pr (dsInsert d $ dsUnion ds new_ds) md disjuncts) where rule = if semBranch p then SemBrRule else DisjRule -- todo: if only one conjunct remaining, do not add d , but still create a DisjRule disjRule _ _ _ _ = error "disjRule"-
src/htab.hs view
@@ -10,7 +10,6 @@ import System.IO ( hPrint, stderr ) import System.Exit ( exitWith, ExitCode(ExitFailure) ) -import Prelude hiding ( catch ) import Control.Exception ( catch, SomeException ) import HTab.Main ( runWithParams, TaskRunFlag(..) )