module WeakBasis where
import Logic
import Heuristics
import Preprocessing ( dimacs
, formulas)
import Saturation ( forgetVarKB
, saturateKB)
import System.Environment
import Data.List (nub,delete)
import qualified Data.Set as S
decided :: S.Set FProp -> Bool
decided kb = kb == (S.singleton T) || S.member F kb
notDecided = not . decided
forgetVarsKB :: S.Set FProp -> [VarProp] -> S.Set FProp
forgetVarsKB ps [] = ps
forgetVarsKB ps vs' = (forgetVarsKB aux vs)
where (v:vs) = frequency ps vs'
aux = forgetVarKB v ps
subsequencesN :: [a] -> [[a]]
subsequencesN [v] = [[]]
subsequencesN (v:vs) = [vs] ++ map (v:) (subsequencesN vs)
isWeakBasis :: S.Set FProp -> [VarProp] -> Bool
isWeakBasis kb vs = ((decided . forgetVarsKB kb) vs) &&
all notDecided [forgetVarsKB kb vs' | vs' <- subsequencesN vs]
algorithm :: (Eq a) => ([a] -> Bool) -> [a] -> [[a]]
algorithm p [] = []
algorithm p xs | (p xs) && (null aux) = [xs]
| otherwise = nub $ concatMap (algorithm p) aux
where aux = filter p (subsequencesN xs)
algorithm' :: (Eq a) => ([a] -> Bool) -> ([a],[a]) -> [[a]]
algorithm' _ (xs,[]) = [xs]
algorithm' p (xs,ys) | p xs = algorithm'Aux p xs aux
| otherwise = []
where aux = filter (p . fst) (subsequencesAux (xs,ys))
algorithm'Aux :: (Eq a) => ([a] -> Bool) -> [a] -> [([a],[a])] -> [[a]]
algorithm'Aux _ xs [] = [xs]
algorithm'Aux p _ aux = concatMap (algorithm' p) aux
subsequencesAux (_,[]) = []
subsequencesAux ([],_) = []
subsequencesAux (xs,(y:ys)) = ((delete y xs,ys):subsequencesAux (xs,ys))
weakBasis' kb vs = algorithm' property (vs,vs)
where property = (decided . forgetVarsKB kb)
weakBasis kb vs = algorithm property vs
where property = (decided . forgetVarsKB kb)
weakBasisCNF f = do
putStrLn ("Weak Basis of instance " ++ f ++
" are:")
(f',vs) <- dimacs f
let sol = weakBasis f' vs
return sol
weakBasisFORMULAS f = do
putStrLn ("Weak Basis of instance " ++ f ++
" are:")
(f',vs) <- formulas f
let sol = weakBasis f' vs
return sol