Satyros.DPLL.StorageUtil
assignDecisionVariable :: Functor f => Literal -> DPLL s f () Source #
assignImplicationVariable :: Functor f => Literal -> Clause -> DPLL s f () Source #
assignFailureDrivenVariable :: Functor f => Literal -> Clause -> DPLL s f () Source #
eraseCurrentImplicationVariables :: Functor f => DPLL s f () Source #
learnClause :: Functor f => Clause -> DPLL s f () Source #
dropLevel :: Functor f => DPLL s f (Maybe (Maybe Variable, Set Variable)) Source #
dropIrrelevantLevels :: Functor f => Clause -> DPLL s f () Source #
deriveConflictClauseRelSAT :: Functor f => Clause -> DPLL s f Clause Source #
levelToSet :: (Maybe Variable, Set Variable) -> Set Variable Source #