QBF.Tools

Description

Synopsis

• data FoldRecord a = FoldRecord {
  • foldNegation :: a -> Range -> a
  • foldConjunction :: [a] -> Range -> a
  • foldDisjunction :: [a] -> Range -> a
  • foldImplication :: a -> a -> Range -> a
  • foldEquivalence :: a -> a -> Range -> a
  • foldTrueAtom :: Range -> a
  • foldFalseAtom :: Range -> a
  • foldPredication :: Token -> a
  • foldForAll :: [Token] -> a -> Range -> a
  • foldExists :: [Token] -> a -> Range -> a
  }
• foldFormula :: FoldRecord a -> FORMULA -> a
• mapRecord :: FoldRecord FORMULA
• isNeg :: FORMULA -> Bool
• isQuantified :: FORMULA -> Bool
• getLits :: Set FORMULA -> Set FORMULA
• bothLits :: Set FORMULA -> Bool
• getConj :: FORMULA -> [FORMULA]
• getDisj :: FORMULA -> [FORMULA]
• flatConj :: [FORMULA] -> Set FORMULA
• mkConj :: [FORMULA] -> Range -> FORMULA
• flatDisj :: [FORMULA] -> Set FORMULA
• mkDisj :: [FORMULA] -> Range -> FORMULA
• simplify :: FORMULA -> FORMULA
• elimEquiv :: FORMULA -> FORMULA
• elimImpl :: FORMULA -> FORMULA
• negForm :: Range -> FORMULA -> FORMULA
• moveNegIn :: FORMULA -> FORMULA
• distributeAndOverOr :: FORMULA -> FORMULA
• cnf :: FORMULA -> FORMULA
• distributeOrOverAnd :: FORMULA -> FORMULA
• dnf :: FORMULA -> FORMULA
• combine :: [[a]] -> [[a]]
• containsAtoms :: FORMULA -> (Bool, Bool)
• getVars :: FORMULA -> [Token]
• uniqueQuantifiedVars :: Int -> String -> FORMULA -> (Int, FORMULA)
• uniqueQuantifiedVars' :: Int -> Map Token Token -> String -> FORMULA -> (Int, FORMULA)
• removeQuantifiers :: FORMULA -> FORMULA
• data QuantifiedVars = QuantifiedVars {
  • universallyQ :: [Token]
  • existentiallyQ :: [Token]
  • notQ :: [Token]
  }
• quantifiedVars :: QuantifiedVars
• joinQuantifiedVars :: QuantifiedVars -> QuantifiedVars -> QuantifiedVars
• getQuantifiedVars :: FORMULA -> QuantifiedVars
• flatten :: FORMULA -> [FORMULA]
• flattenDis :: FORMULA -> [FORMULA]
• negateFormula :: FORMULA -> FORMULA

Documentation