module Algorithm where

    import System.Random
    import Data.Maybe
    import Data.List

    type Atom = String
    type Literal = (Bool,Atom)
    type Clause = [Literal]
    type Formula = [Clause]
    type Model = [(Atom, Bool)]
    type Node = (Formula, ([Atom], Model))

    -- This function  takess a Clause and return the set of Atoms of that Clause.
    atomsClause :: Clause -> [Atom]


    -- This function  takes a Formula returns the set of Atoms of a Formula
    atoms :: Formula -> [Atom]


    -- This function returns True if the given Literal can be found within
    -- the Clause.
    isLiteral :: Literal -> Clause -> Bool


    -- this function takes a Model and an Atom and flip the truthvalue of
    -- the atom in the model
    flipSymbol :: Model -> Atom -> Model -- is this ok?

    Additional functions :
    remove :: (Eq a) )a ->[a] ->[a]
    -This function removes an item from a list.

     neg :: Literal->Literal
    -This function flips a literal (ie. from P to :P and from :P to P).
    falseClause :: Model -> Clause -> Bool
    -This function takes a Model and a Clause and returns True
    if the clause is unsatisfied by the model or False otherwise.
    falseClauses :: Formula -> Model -> [Clause]
    -This function takes a Formula and a Model and returns the list of clauses of the  formula that are not satisfied.
     assignModel :: Model -> Formula -> Formula
     -This function applies the assign function for all the assignments of a given model.
     checkFormula :: Formula -> Maybe Bool This function checks whether a formula can be  decided to be satisfiable or unsatisfiable based on the effects of the assign function.
     satisfies :: Model -> Formula -. Bool This function checks whether a model satisfies a formula. This is done with the combination of the assignModel and checkFormula functions.