module Funsat.Types where
import Control.Monad.MonadST( MonadST(..) )
import Control.Monad.ST.Strict
import Data.Array.ST
import Data.Array.Unboxed
import Data.BitSet (BitSet)
import Data.Foldable hiding (sequence_)
import Data.Map (Map)
import Data.Set (Set)
import Funsat.Monad
import Funsat.Utils
import Prelude hiding (sum, concatMap, elem, foldr, foldl, any, maximum)
import qualified Data.BitSet as BitSet
import qualified Data.Foldable as Fl
import qualified Data.List as List
import qualified Data.Map as Map
import qualified Data.Set as Set
newtype Var = V {unVar :: Int} deriving (Eq, Ord, Enum, Ix)
instance Show Var where
show (V i) = show i ++ "v"
instance Num Var where
_ + _ = error "+ doesn't make sense for variables"
_ _ = error "- doesn't make sense for variables"
_ * _ = error "* doesn't make sense for variables"
signum _ = error "signum doesn't make sense for variables"
negate = error "negate doesn't make sense for variables"
abs = id
fromInteger l | l <= 0 = error $ show l ++ " is not a variable"
| otherwise = V $ fromInteger l
newtype Lit = L {unLit :: Int} deriving (Eq, Ord, Enum, Ix)
inLit f = L . f . unLit
litSign :: Lit -> Bool
litSign (L x) | x < 0 = False
| x > 0 = True
instance Show Lit where
show l = show ul
where ul = unLit l
instance Read Lit where
readsPrec i s = map (\(i,s) -> (L i, s)) (readsPrec i s :: [(Int, String)])
var :: Lit -> Var
var = V . abs . unLit
instance Num Lit where
_ + _ = error "+ doesn't make sense for literals"
_ _ = error "- doesn't make sense for literals"
_ * _ = error "* doesn't make sense for literals"
signum _ = error "signum doesn't make sense for literals"
negate = inLit negate
abs = inLit abs
fromInteger l | l == 0 = error "0 is not a literal"
| otherwise = L $ fromInteger l
type Clause = [Lit]
data GenCNF a = CNF {
numVars :: Int,
numClauses :: Int,
clauses :: Set a
}
deriving (Show, Read, Eq)
type CNF = GenCNF Clause
instance Foldable GenCNF where
foldMap toM cnf = foldMap toM (clauses cnf)
class Ord a => Setlike t a where
without :: t -> a -> t
with :: t -> a -> t
contains :: t -> a -> Bool
instance Ord a => Setlike (Set a) a where
without = flip Set.delete
with = flip Set.insert
contains = flip Set.member
instance Ord a => Setlike [a] a where
without = flip List.delete
with = flip (:)
contains = flip List.elem
instance Setlike IAssignment Lit where
without a l = a // [(var l, 0)]
with a l = a // [(var l, unLit l)]
contains a l = unLit l == a ! (var l)
instance (Ord k, Ord a) => Setlike (Map k a) (k, a) where
with m (k,v) = Map.insert k v m
without m (k,_) = Map.delete k m
contains = error "no contains for Setlike (Map k a) (k, a)"
instance (Ord a, BitSet.Hash a) => Setlike (BitSet a) a where
with = flip BitSet.insert
without = flip BitSet.delete
contains = flip BitSet.member
instance (BitSet.Hash Lit) where
hash l = if li > 0 then 2 * vi else (2 * vi) + 1
where li = unLit l
vi = abs li
instance (BitSet.Hash Var) where
hash = unVar
type IAssignment = UArray Var Int
type MAssignment s = STUArray s Var Int
freezeAss :: MAssignment s -> ST s IAssignment
freezeAss = freeze
unsafeFreezeAss :: (MonadST s m) => MAssignment s -> m IAssignment
unsafeFreezeAss = liftST . unsafeFreeze
thawAss :: IAssignment -> ST s (MAssignment s)
thawAss = thaw
unsafeThawAss :: IAssignment -> ST s (MAssignment s)
unsafeThawAss = unsafeThaw
assign :: MAssignment s -> Lit -> ST s (MAssignment s)
assign a l = writeArray a (var l) (unLit l) >> return a
unassign :: MAssignment s -> Lit -> ST s (MAssignment s)
unassign a l = writeArray a (var l) 0 >> return a
litAssignment :: IAssignment -> [Lit]
litAssignment mFr = foldr (\i ass -> if mFr!i == 0 then ass
else (L . (mFr!) $ i) : ass)
[]
(range . bounds $ mFr)
class Model a m where
statusUnder :: a -> m -> Either () Bool
instance Model Lit IAssignment where
statusUnder l a | a `contains` l = Right True
| a `contains` negate l = Right False
| otherwise = Left ()
instance Model Var IAssignment where
statusUnder v a | a `contains` pos = Right True
| a `contains` neg = Right False
| otherwise = Left ()
where pos = L (unVar v)
neg = negate pos
instance Model Clause IAssignment where
statusUnder c m
| Fl.any (\e -> m `contains` e) c = Right True
| Fl.all (`isFalseUnder` m) c = Right False
| otherwise = Left ()
isUndefUnder :: Model a m => a -> m -> Bool
isUndefUnder x m = isUndef $ x `statusUnder` m
where isUndef (Left ()) = True
isUndef _ = False
isTrueUnder :: Model a m => a -> m -> Bool
isTrueUnder x m = isTrue $ x `statusUnder` m
where isTrue (Right True) = True
isTrue _ = False
isFalseUnder :: Model a m => a -> m -> Bool
isFalseUnder x m = isFalse $ x `statusUnder` m
where isFalse (Right False) = True
isFalse _ = False
isUnitUnder :: (Model a m) => [a] -> m -> Bool
isUnitUnder c m = isSingle (filter (not . (`isFalseUnder` m)) c)
&& not (Fl.any (`isTrueUnder` m) c)
getUnit :: (Model a m, Show a) => [a] -> m -> a
getUnit c m = case filter (not . (`isFalseUnder` m)) c of
[u] -> u
xs -> error $ "getUnit: not unit: " ++ show xs