diff --git a/HTab.cabal b/HTab.cabal --- a/HTab.cabal +++ b/HTab.cabal @@ -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 diff --git a/src/HTab/Branch.hs b/src/HTab/Branch.hs --- a/src/HTab/Branch.hs +++ b/src/HTab/Branch.hs @@ -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 + + diff --git a/src/HTab/CommandLine.hs b/src/HTab/CommandLine.hs --- a/src/HTab/CommandLine.hs +++ b/src/HTab/CommandLine.hs @@ -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)", diff --git a/src/HTab/DMap.hs b/src/HTab/DMap.hs --- a/src/HTab/DMap.hs +++ b/src/HTab/DMap.hs @@ -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 diff --git a/src/HTab/DisjSet.hs b/src/HTab/DisjSet.hs --- a/src/HTab/DisjSet.hs +++ b/src/HTab/DisjSet.hs @@ -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 diff --git a/src/HTab/Formula.hs b/src/HTab/Formula.hs --- a/src/HTab/Formula.hs +++ b/src/HTab/Formula.hs @@ -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 diff --git a/src/HTab/Literals.hs b/src/HTab/Literals.hs --- a/src/HTab/Literals.hs +++ b/src/HTab/Literals.hs @@ -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 diff --git a/src/HTab/Main.hs b/src/HTab/Main.hs --- a/src/HTab/Main.hs +++ b/src/HTab/Main.hs @@ -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 -- diff --git a/src/HTab/ModelGen.hs b/src/HTab/ModelGen.hs --- a/src/HTab/ModelGen.hs +++ b/src/HTab/ModelGen.hs @@ -12,9 +12,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} diff --git a/src/HTab/Relations.hs b/src/HTab/Relations.hs --- a/src/HTab/Relations.hs +++ b/src/HTab/Relations.hs @@ -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 diff --git a/src/HTab/RuleId.hs b/src/HTab/RuleId.hs --- a/src/HTab/RuleId.hs +++ b/src/HTab/RuleId.hs @@ -47,6 +47,7 @@ | R_DiscardDown | R_DiscardDiaDone | R_DiscardDiaBlocked + | R_DiscardDiaSymBlocked | R_DiscardDiaX | R_DiscardDisjTrivial | R_ClashDisj -- Branch clash diff --git a/src/HTab/Rules.hs b/src/HTab/Rules.hs --- a/src/HTab/Rules.hs +++ b/src/HTab/Rules.hs @@ -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" - diff --git a/src/htab.hs b/src/htab.hs --- a/src/htab.hs +++ b/src/htab.hs @@ -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(..) )