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.List( intercalate )
import Data.Map ( Map )
import Data.Set ( Set )
import Data.STRef
import Funsat.Monad
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.Graph.Inductive.Graph as Graph
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)
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
inLit :: (Int -> Int) -> Lit -> Lit
inLit f = L . f . unLit
litSign :: Lit -> Bool
litSign (L x) | x < 0 = False
| x > 0 = True
| otherwise = error "litSign of 0"
instance Show Lit where show = show . unLit
instance Read Lit where
readsPrec i s = map (\(i,s) -> (L i, s)) (readsPrec i s)
var :: Lit -> Var
var = V . abs . unLit
lit :: Var -> Lit
lit = L . unVar
type Clause = [Lit]
data CNF = CNF
{ numVars :: Int
, numClauses :: Int
, clauses :: Set Clause } deriving (Show, Read, Eq)
data Solution = Sat IAssignment | Unsat IAssignment deriving (Eq)
instance Show Solution where
show (Sat a) = "satisfiable: " ++ showAssignment a
show (Unsat _) = "unsatisfiable"
finalAssignment :: Solution -> IAssignment
finalAssignment (Sat a) = a
finalAssignment (Unsat a) = a
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
showAssignment :: IAssignment -> String
showAssignment a = intercalate " " ([show (a!i) | i <- range . bounds $ a,
(a!i) /= 0])
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)
data Cut f gr a b =
Cut { reasonSide :: f Graph.Node
, conflictSide :: f Graph.Node
, cutUIP :: Graph.Node
, cutGraph :: gr a b }
instance (Show (f Graph.Node), Show (gr a b)) => Show (Cut f gr a b) where
show (Cut { conflictSide = c, cutUIP = uip }) =
"Cut (uip=" ++ show uip ++ ", cSide=" ++ show c ++ ")"
data CGNodeAnnot = CGNA Lit Int
instance Show CGNodeAnnot where
show (CGNA (L 0) _) = "lambda"
show (CGNA l lev) = show l ++ " (" ++ show lev ++ ")"
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 ()
where
isFalseUnder x m = isFalse $ x `statusUnder` m
where isFalse (Right False) = True
isFalse _ = False
type Level = Int
type LevelArray s = STUArray s Var Level
type FrozenLevelArray = UArray Var Level
newtype VarOrder s = VarOrder { varOrderArr :: STUArray s Var Double }
deriving Show
newtype FrozenVarOrder = FrozenVarOrder (UArray Var Double)
deriving Show
type WatchedPair s = (STRef s (Lit, Lit), Clause, ClauseId)
type WatchArray s = STArray s Lit [WatchedPair s]
data PartialResolutionTrace = PartialResolutionTrace
{ resTraceIdCount :: !Int
, resTrace :: ![Int]
, resTraceOriginalSingles :: ![(Clause, ClauseId)]
, resSourceMap :: Map ClauseId [ClauseId] } deriving (Show)
type ReasonMap = Map Var (Clause, ClauseId)
type ClauseId = Int
instance Show (STRef s a) where show = const "<STRef>"
instance Show (STUArray s Var Int) where show = const "<STUArray Var Int>"
instance Show (STUArray s Var Double) where show = const "<STUArray Var Double>"
instance Show (STArray s a b) where show = const "<STArray>"