<commit_before>module Formula
    ( Formula(..)
    , and, or
    , mapFormula,foldrFormula
    , maxVar
    , fromCNF, toCNF, tseitin
    ) where

import Control.Monad.Trans.State
import Prelude hiding (and,or)
import Text.Read (readPrec,parens)
import Text.ParserCombinators.ReadP (string,choice)
import Text.ParserCombinators.ReadPrec ((<++), lift)

import MiniSat

-----------------------------------------------------------------------

data Formula = And [Formula]
             | Or  [Formula]
             | Not Formula
             | Lit Literal
             deriving (Eq)

and :: Formula -> Formula -> Formula
and x             (Lit (Neg 0)) = x
and x             (Lit (Pos 0)) = Lit (Pos 0)
and (Lit (Neg 0)) y             = y
and (Lit (Pos 0)) y             = Lit (Pos 0)
and (And xs)      (And ys)      = And (xs ++ ys)
and x             (And ys)      = And (x:ys)
and (And xs)      y             = And (y:xs)
and x             y             = And [x,y]

or :: Formula -> Formula -> Formula
or x             (Lit (Neg 0)) = Lit (Neg 0)
or x             (Lit (Pos 0)) = x
or (Lit (Neg 0)) y             = Lit (Neg 0)
or (Lit (Pos 0)) y             = y
or (Or xs)       (Or ys)       = Or (xs ++ ys)
or x             (Or ys)       = Or (x:ys)
or (Or xs)       y             = Or (y:xs)
or x             y             = Or [x,y]

mapFormula :: (Literal -> Literal) -> Formula -> Formula
mapFormula f (And xs) = And $ map (mapFormula f) xs
mapFormula f (Or  xs) = Or  $ map (mapFormula f) xs
mapFormula f (Not x)  = Not $ mapFormula f x
mapFormula f (Lit x)  = Lit $ f x

foldrFormula :: (Literal -> b -> b) -> b -> Formula -> b
foldrFormula f z (Lit x)  = f x z
foldrFormula f z (Not x)  = foldrFormula f z x
foldrFormula f z (Or  xs) = foldr (flip $ foldrFormula f) z xs
foldrFormula f z (And xs) = foldr (flip $ foldrFormula f) z xs

maxVar :: Formula -> Var
maxVar = foldrFormula max' 0
    where
        max' (Pos a) b = max a b
        max' (Neg a) b = max a b

fromCNF :: [Clause] -> Formula
fromCNF = And . map (Or . map Lit)

-- | Given a formula and the next free variable (i.e. the lowest variable
-- not occuring in the formula that can be used as an auxiliary variable
-- in the Tseitin encoding) returns the formula in CNF and the new next
-- free variable.
toCNF :: Formula -> Var -> ([Clause], Var)
toCNF f n = ([x]:xs, n')
    where ((x, xs), n') = runState (tseitin f) n
<commit_msg>check if formula already CNF before tseitinizing<commit_after>{-# LANGUAGE LambdaCase #-}

module Formula
    ( Formula(..)
    , and, or
    , mapFormula,foldrFormula
    , maxVar
    , fromCNF, toCNF, tseitin
    ) where

import Control.Monad.Trans.State
import Prelude hiding (and,or)
import Text.Read (readPrec,parens)
import Text.ParserCombinators.ReadP (string,choice)
import Text.ParserCombinators.ReadPrec ((<++), lift)

import MiniSat

-----------------------------------------------------------------------

data Formula = And [Formula]
             | Or  [Formula]
             | Not Formula
             | Lit Literal
             deriving (Eq)

and :: Formula -> Formula -> Formula
and x             (Lit (Neg 0)) = x
and x             (Lit (Pos 0)) = Lit (Pos 0)
and (Lit (Neg 0)) y             = y
and (Lit (Pos 0)) y             = Lit (Pos 0)
and (And xs)      (And ys)      = And (xs ++ ys)
and x             (And ys)      = And (x:ys)
and (And xs)      y             = And (y:xs)
and x             y             = And [x,y]

or :: Formula -> Formula -> Formula
or x             (Lit (Neg 0)) = Lit (Neg 0)
or x             (Lit (Pos 0)) = x
or (Lit (Neg 0)) y             = Lit (Neg 0)
or (Lit (Pos 0)) y             = y
or (Or xs)       (Or ys)       = Or (xs ++ ys)
or x             (Or ys)       = Or (x:ys)
or (Or xs)       y             = Or (y:xs)
or x             y             = Or [x,y]

mapFormula :: (Literal -> Literal) -> Formula -> Formula
mapFormula f (And xs) = And $ map (mapFormula f) xs
mapFormula f (Or  xs) = Or  $ map (mapFormula f) xs
mapFormula f (Not x)  = Not $ mapFormula f x
mapFormula f (Lit x)  = Lit $ f x

foldrFormula :: (Literal -> b -> b) -> b -> Formula -> b
foldrFormula f z (Lit x)  = f x z
foldrFormula f z (Not x)  = foldrFormula f z x
foldrFormula f z (Or  xs) = foldr (flip $ foldrFormula f) z xs
foldrFormula f z (And xs) = foldr (flip $ foldrFormula f) z xs

maxVar :: Formula -> Var
maxVar = foldrFormula max' 0
    where
        max' (Pos a) b = max a b
        max' (Neg a) b = max a b

fromCNF :: [Clause] -> Formula
fromCNF = And . map (Or . map Lit)

-- | Given a formula and the next free variable (i.e. the lowest variable
-- not occuring in the formula that can be used as an auxiliary variable
-- in the Tseitin encoding) returns the formula in CNF and the new next
-- free variable.
toCNF :: Formula -> Var -> ([Clause], Var)
toCNF f n | isCNF f   = (easy f, n)
          | otherwise = ([x]:xs, n')
    where
        easy (And xs) = [[y | Lit y <- ys] | Or ys <- xs]
        ((x, xs), n') = runState (tseitin f) n

isCNF :: Formula -> Bool
isCNF (And xs) = all (\case { Or ys -> all isLit ys; _ -> False }) xs
isCNF _        = False

isLit :: Formula -> Bool
isLit (Lit _) = True
isLit _       = False

{'fraction_non_alphanumeric': 0.14988425925925927, 'fraction_numerical': 0.005015432098765432, 'mean_word_length': 1.7682861719167111, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 39, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5229398', 'n_tokens_mistral': 1872, 'n_tokens_neox': 1766, 'n_words': 704}