module Types where import Data.List (sortOn) import qualified Data.HashMap.Lazy as HM import qualified Data.IntMap.Lazy as IM -- type definitions -- don't change the unmarked types type EName = String type Name = EName -- change as you like data Polarity = Pos | Neg deriving Eq data ELiteral = Literal Polarity EName deriving Eq type Literal = ELiteral -- change as you like type EClause = [ELiteral] type Clause = EClause -- change as you like type EConjForm = [EClause] type ConjForm = EConjForm -- change as you like type Key = Int type EKeyClause = (Key, EClause) type KeyClause = EKeyClause -- change as you like type EKeyConjForm = [EKeyClause] type KeyConjForm = IM.IntMap Clause -- change as you like EKeyConjForm data EResolve = Resolve EName Key Key deriving (Eq, Show) type Resolve = EResolve -- change as you like type EValuation = [EName] type Valuation = EValuation -- change as you like data EProof = Refutation [EResolve] | Model EValuation deriving (Eq, Show) type Proof = EProof -- change as you like type ScoreTab = HM.HashMap Name [(Int,Int)] -- Key = Variable name, Value = [(# of unique vars in Clause, Clause's idx)] -- 2 tables: 1 for pos vars, 1 for neg vars -- [# of Lit /= key in Clause, Clause's length, Clause's idx] type SelClauseStrategy = KeyConjForm -> ScoreTab -> ScoreTab -> EKeyConjForm -> (Name, Int, Int) -- change as you like --KeyConjForm -> Maybe KeyClause -- adapt the following if you changed the internal data types above toEName :: Name -> EName toEName = id toName :: EName -> Name toName = id toELiteral :: Literal -> ELiteral toELiteral = id toLiteral :: ELiteral -> Literal toLiteral = id toEClause :: Clause -> EClause toEClause = id toClause :: EClause -> Clause toClause = id toEConjForm :: ConjForm -> EConjForm toEConjForm = id toConjForm :: EConjForm -> ConjForm toConjForm = id toEKeyClause :: KeyClause -> EKeyClause toEKeyClause = id toKeyClause :: EKeyClause -> KeyClause toKeyClause = id toEKeyConjForm :: KeyConjForm -> EKeyConjForm toEKeyConjForm = IM.toList toKeyConjForm :: EKeyConjForm -> KeyConjForm toKeyConjForm kCj = IM.fromDistinctAscList (sortOn fst kCj) toEResolve :: Resolve -> EResolve toEResolve = id toResolve :: EResolve -> Resolve toResolve = id toEValuation :: Valuation -> EValuation toEValuation = id toValuation :: EValuation -> Valuation toValuation = id toEProof :: Proof -> EProof toEProof = id toProof :: EProof -> Proof toProof = id