diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,6 @@
+## 1.0.0.0
+- 2019-08-04
+    - Removed the general solver tentatively(for maintainability and good design).
+    - Separated the logic formulas from the problem domains.
+    - Removed the solver for `Options`.
+    - Re-implemented the solver for `HM`.
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,93 +1,153 @@
 # RSolve
 
-[![](https://img.shields.io/hackage/v/RSolve.svg)](hackage.haskell.org/package/RSolve)
+[![](https://img.shields.io/hackage/v/RSolve.svg)](https://hackage.haskell.org/package/RSolve)
 
-A general solver for type checkers of programming languages and real world puzzles with complex constraints.
+NOTE: NO LONGER for general logic programming, this package is now dedicated for the simple propositional logic.
 
-## Preview
+The README is going to get updated.
 
-Here are 2 special cases presented in the following sections to show how powerful `RSolve` is.
+## Propositional Logic
 
-### The Most Graceful Hindley-Milner Unification
+RSolve uses [disjunctive normal form](https://en.wikipedia.org/wiki/Disjunctive_normal_form) to solve logic problems.
 
-Check `RSolve.HM.Core` and `RSolve.HM.Example`.
+This disjunctive normal form works naturally with the logic problems where the atom formulas can be generalized to an arbitrary equation in the problem domain by introducing a problem domain specific solver. A vivid
+example can be found at `RSolve.HM`, where
+I implemented an extended algo-W for [HM unification](https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system).
 
-Uncomment the code in `Main.hs` could reproduce following program:
 
+To take advantage of RSolve, we should implement 2 classes:
+
+- `AtomF`, which stands for the atom formula.
+
+- `CtxSolver`, which stands for the way to solve a bunch of atom formulas.
+
+However we might not need to a solver sometimes:
+
 ```haskell
-check = do
-    let i = Prim Int
-    let f = Prim Float
-    let arrow = Op Arrow i f
-    -- u means undecided
-    u1 <- new
-    u2 <- new
-    u3 <- new
-    u4 <- new
-    -- u1 -> u2 where u1, u2 is not generic
-    let arrow_var = Op Arrow (Var u1) (Var u2)
-    -- int -> int
-    let arrow_inst1 = Op Arrow i i
-    -- float -> float
-    let arrow_inst2 = Op Arrow f f
-    -- a generic function
-    let arrow_generic = Forall [u3] $ Op Arrow (Var u3) (Var u3)
+data Value = A | B | C | D
+    deriving (Show, Eq, Ord, Enum)
 
-    let arrow_match = Op Arrow (Var u4) (Var u4)
+data At = At {at_l :: String, at_r :: Value}
+    deriving (Show, Eq, Ord)
 
-    _ <- solve $ Unify arrow arrow_var
-    _ <- solve $ Unify arrow_inst1 arrow_match
-    _ <- solve $ Unify arrow_generic arrow_inst1
-    _ <- solve $ Unify arrow_generic arrow_inst2
-    _ <- solveNeg
+instance AtomF At where
+    notA At {at_l = lhs, at_r = rhs} =
+        let wholeSet  = enumFrom (toEnum 0) :: [Value]
+            contrasts = delete rhs wholeSet
+        in [At {at_l = lhs, at_r = rhs'} | rhs' <- contrasts]
 
-    mapM require [Var u1, Var u2, arrow_inst1, arrow_inst2, arrow_generic, arrow_match]
-```
+infix 6 <==>
+s <==> v = Atom $ At s v
 
-output:
+equations = do
+    assert $ "a" <==> A :||: "a" <==> B
+    assert $ Not ("a" <==> A)
 
+main =
+  let equationGroups = unionEquations equations
+  in forM equationGroups print
 ```
-u1 : Int
-u2 : Float
-arrow_inst1 : (Int -> Int)
-arrow_inst2 : (Float -> Float)
-arrow_generic : forall  a2.(a2 -> a2)
-arrow_match : (Int -> Int)
+produces
+```haskell
+[At {at_l = "a", at_r = A},At {at_l = "a", at_r = B}]
+[At {at_l = "a", at_r = A},At {at_l = "a", at_r = C}]
+[At {at_l = "a", at_r = A},At {at_l = "a", at_r = D}]
+[At {at_l = "a", at_r = B}]
+[At {at_l = "a", at_r = B},At {at_l = "a", at_r = C}]
+[At {at_l = "a", at_r = B},At {at_l = "a", at_r = C},At {at_l = "a", at_r = D}]
+[At {at_l = "a", at_r = B},At {at_l = "a", at_r = D}]
 ```
 
-### N-Option Puzzles
+According to the property of the problem domain, we can figure out that
+only the 4-th(1-based indexing) equation group
+`[At {at_l = "a", at_r = B}]`
+will produce a feasible solution because symbol `a` can
+only hold one value.
 
-This implementation is presented at `RSolve.Options`,  which provides the abstractions to solve all kinds of puzzles described with options.
+When do we need a solver? For instance, type checking&inference.
 
-A Hello World program could be found at `src/Main.hs` which solves a complex problem described with following link:
+In this case, we need type checking environments to represent the checking states:
 
-https://www.zhihu.com/question/68411978/answer/558913247.
+```haskell
+data TCEnv = TCEnv {
+          _noms  :: M.Map Int T  -- nominal type ids
+        , _tvars :: M.Map Int T  -- type variables
+        , _neqs  :: S.Set (T, T) -- negation constraints
+    }
+    deriving (Show)
 
+emptyTCEnv = TCEnv M.empty M.empty S.empty
+```
 
-However, the much easier cases taking the same background as above problem (logic constraints described with four options `A, B, C, D`) could be enjoyale:
+For sure we also need to represent the type:
 
 ```haskell
-test2 = do
-  a <- store $ sol [A, B, C]
-  b <- store $ sol [B, C, D]
-  c <- store $ sol [C]
-  _ <- solve $ a `eq`  b
-  _ <- solve $ b `neq` c
-  _ <- solveNeg  -- `Not` condition requires this
-  _ <- solvePred -- unnecessary
-  mapM require [a, b, c]
-
-main = do
-    format ["a", "b", "c"] . nub . L.map fst
-    $ runBr test2 emptyLState
+data T
+    = TVar Int
+    | TFresh String
+    | T :-> T
+    | T :*  T -- tuple
+    | TForall (S.Set String) T
+    | TApp T T -- type application
+    | TNom Int -- nominal type index
+    deriving (Eq, Ord)
 ```
 
-output:
+Then the atom formula of HM unification is:
 
+```haskell
+data Unif
+    = Unif {
+          lhs :: T
+        , rhs :: T
+        , neq :: Bool -- lhs /= rhs or  lhs == rhs?
+      }
+  deriving (Eq, Ord)
 ```
-λ stack exec RSolve
-====
-"a" : Sol (fromList [B])
-"b" : Sol (fromList [B])
-"c" : Sol (fromList [C])
+
+We then need to implement this:
+
+```haskell
+-- class AtomF a => CtxSolver s a where
+--     solve :: a -> MS s ()
+prune :: T -> MS TCEnv T -- MS: MultiState
+instance CtxSolver TCEnv Unif where
+  solver = ...
+````
+
+Finally we got this:
+
+```haskell
+infixl 6 <=>
+a <=> b = Atom $ Unif {lhs=a, rhs=b, neq=False}
+solu = do
+    a <- newTVar
+    b <- newTVar
+    c <- newTVar
+    d <- newTVar
+    let [eqs] = unionEquations $
+                do
+                assert $ TVar a <=> TForall (S.fromList ["s"]) ((TFresh "s") :-> (TFresh "s" :* TFresh "s"))
+                assert $ TVar a <=> (TVar b :-> (TVar c :* TVar d))
+                assert $ TVar d <=> TNom 1
+    -- return eqs
+    forM_ eqs solve
+    return eqs
+    a <- prune $ TVar a
+    b <- prune $ TVar b
+    c <- prune $ TVar c
+    return (a, b, c)
+
+test :: Eq a => String -> a -> a -> IO ()
+test msg a b
+    | a == b = return ()
+    | otherwise = print msg
+
+main = do
+    forM (unionEquations equations) print
+
+    let (a, b, c):_ = map fst $ runMS solu emptyTCEnv
+    test "1 failed" (show a) "@t1 -> @t1 * @t1"
+    test "2 failed" (show b) "@t1"
+    test "3 failed" (show c) "@t1"
 ```
diff --git a/RSolve.cabal b/RSolve.cabal
--- a/RSolve.cabal
+++ b/RSolve.cabal
@@ -1,41 +1,77 @@
-name:                RSolve
-version:             0.1.0.1
-synopsis:            A general solver for equations
-description:         A general solver for type checkers of programming languages
-                     and real world puzzles with complex constraints.
-homepage:            https://github.com/thautwarm/Rsolver#readme
-license:             MIT
-license-file:        LICENSE
-author:              thautwarm
-maintainer:          twshere@outlook.com
-copyright:           2018 thautwarm
-category:            Language
-build-type:          Simple
-cabal-version:       >=1.10
-extra-source-files:  README.md
+cabal-version: 1.12
 
+-- This file has been generated from package.yaml by hpack version 0.31.2.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: e5b30745fe99238706cc93bcd6a0c1fe3d35090d5dc5cabf244120d6d382d56c
+
+name:           RSolve
+version:        2.0.0.0
+description:    A general solver for equations
+category:       Logic,Unification
+homepage:       https://github.com/thautwarm/RSolve#readme
+bug-reports:    https://github.com/thautwarm/RSolve/issues
+author:         thautwarm
+maintainer:     twshere@outlook.com
+copyright:      2018, 2019 thautwarm
+license:        MIT
+license-file:   LICENSE
+build-type:     Simple
+extra-source-files:
+    README.md
+    ChangeLog.md
+
 source-repository head
-  type:     git
-  location: https://github.com/thautwarm/Rsolver.git
+  type: git
+  location: https://github.com/thautwarm/RSolve
 
 library
-  hs-source-dirs:      src
-  default-language:    Haskell2010
-  build-depends:       base >= 4 && < 5
-                     , containers
-  exposed-modules:     RSolve.BrMonad
-                     , RSolve.Infr
-                     , RSolve.Logic
-                     , RSolve.HM.Core
-                     , RSolve.Options.Core
+  exposed-modules:
+      RSolve.HM
+      RSolve.Logic
+      RSolve.MapLike
+      RSolve.MultiState
+      RSolve.PropLogic
+      RSolve.Solver
+  other-modules:
+      Paths_RSolve
+  hs-source-dirs:
+      src
+  build-depends:
+      base >=4.7 && <5
+    , containers
+    , lens
+    , mtl
+  default-language: Haskell2010
 
--- executable RSolveExample
---   hs-source-dirs:      src
---   main-is:             Main.hs
---   build-depends:       base >= 4 && < 5
---                      , RSolve
---                      , containers
---   default-language:    Haskell2010
---   other-modules:       RSolve.HM.Example
---                      , RSolve.Options.Example
+executable RSolve-exe
+  main-is: Main.hs
+  other-modules:
+      Paths_RSolve
+  hs-source-dirs:
+      app
+  ghc-options: -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      RSolve
+    , base >=4.7 && <5
+    , containers
+    , lens
+    , mtl
+  default-language: Haskell2010
 
+test-suite RSolve-test
+  type: exitcode-stdio-1.0
+  main-is: Spec.hs
+  other-modules:
+      Paths_RSolve
+  hs-source-dirs:
+      test
+  ghc-options: -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      RSolve
+    , base >=4.7 && <5
+    , containers
+    , lens
+    , mtl
+  default-language: Haskell2010
diff --git a/app/Main.hs b/app/Main.hs
new file mode 100644
--- /dev/null
+++ b/app/Main.hs
@@ -0,0 +1,2 @@
+module Main where
+main = putStrLn "No CLI support yet"
diff --git a/src/RSolve/BrMonad.hs b/src/RSolve/BrMonad.hs
deleted file mode 100644
--- a/src/RSolve/BrMonad.hs
+++ /dev/null
@@ -1,30 +0,0 @@
-module RSolve.BrMonad where
-import Control.Monad
-import Control.Monad.Fail
-import Control.Applicative
-
-newtype Br s a = Br {runBr :: s -> [(a, s)]}
-
-instance Functor (Br s) where
-  fmap = liftM
-
-instance Applicative (Br s) where
-  pure = return
-  (<*>)  = ap
-
-instance MonadFail (Br s) where
-  fail _ = empty
-
-instance Monad (Br s) where
-  m >>= k =
-    Br $ \s ->
-       let xs = runBr m s
-       in join [ runBr (k a) s | (a, s) <- xs]
-  return a = Br $ \s -> [(a, s)]
-
-instance Alternative (Br s) where
-  empty = Br $ const []
-  ma <|> mb = Br $ \s -> runBr ma s ++ runBr mb s
-
-getBy f = Br $ \s -> [(f s, s)]
-putBy f = Br $ \s -> [((), f s)]
diff --git a/src/RSolve/HM.hs b/src/RSolve/HM.hs
new file mode 100644
--- /dev/null
+++ b/src/RSolve/HM.hs
@@ -0,0 +1,208 @@
+-- | HM unification implementations based on propositional logics,
+--   based on nominal type system.
+-- Author: Taine Zhao(thautwarm)
+-- Date: 2019-08-04
+-- License: MIT
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+module RSolve.HM
+where
+import RSolve.Logic
+import RSolve.Solver
+import RSolve.MultiState
+import Control.Lens (Lens', view, over, makeLenses)
+import Control.Applicative
+import Control.Monad
+import Debug.Trace
+
+import qualified Data.List as L
+import qualified Data.Map  as M
+import qualified Data.Set  as S
+
+type Fix a = a -> a
+
+infixl 6 :->, :*
+
+data T
+    = TVar Int
+    | TFresh String
+    | T :-> T
+    | T :*  T -- tuple
+    | TForall (S.Set String) T
+    | TApp T T -- type application
+    | TNom Int -- nominal type index
+    deriving (Eq, Ord)
+
+deConsTOp :: T -> Maybe (T -> T -> T, T, T)
+deConsTOp = \case
+    a :-> b  -> Just ((:->), a, b)
+    a :*  b  -> Just ((:*),  a, b)
+    TApp a b -> Just (TApp,  a, b)
+    _ -> Nothing
+
+instance Show T where
+    show = \case
+        TVar idx    -> "@" ++ show idx
+        TFresh s    -> s
+        a :-> b     -> showNest a ++ " -> " ++ show b
+        a :*  b     -> showNest a ++ " * " ++ show b
+        TForall l t -> "forall " ++ (unwords $ S.toList l) ++ ". " ++ show t
+        TApp t1 t2  -> show t1 ++ " " ++ showNest t2
+        TNom i       -> "@t" ++ show i
+        where
+            showNest s
+                | isNest s  = "(" ++ show s ++ ")"
+                | otherwise = show s
+            isNest s = case s of
+                TApp _ _    -> True
+                TForall _ s -> isNest s
+                _ :-> _     -> True
+                _ :* _      -> True
+                _           -> False
+
+data Unif
+    = Unif {
+          lhs :: T
+        , rhs :: T
+        , neq :: Bool
+      }
+    deriving (Eq, Ord)
+
+instance Show Unif where
+    show Unif {lhs, rhs, neq} =
+        let op = if neq then " /= " else " == "
+        in  show lhs ++ op ++ show rhs
+
+instance AtomF Unif where
+    notA a@Unif {neq} = [a {neq = not neq}]
+
+data TCEnv = TCEnv {
+          _noms  :: M.Map Int T  -- nominal type ids
+        , _tvars :: M.Map Int T  -- type variables
+        , _neqs  :: S.Set (T, T) -- negation constraints
+    }
+    deriving (Show)
+
+emptyTCEnv = TCEnv M.empty M.empty S.empty
+
+makeLenses ''TCEnv
+
+newTVar :: MS TCEnv Int
+newTVar = do
+    i <- getsMS $ M.size . view tvars
+    modifyMS $ over tvars $ M.insert i (TVar i)
+    return i
+
+newTNom :: MS TCEnv Int
+newTNom = do
+    i <- getsMS $ M.size . view noms
+    modifyMS $ over noms $ M.insert i (TNom i)
+    return i
+
+loadTVar :: Int -> MS TCEnv T
+loadTVar i = getsMS $ (M.! i) . view tvars
+
+occurIn :: Int -> T -> MS TCEnv Bool
+occurIn l = contains
+    where
+        contains (deConsTOp -> Just (_, a, b)) = (||) <$> contains a <*> contains b
+        contains (TNom _)      = return False
+        contains (TForall _ a) = contains a
+        contains (TFresh _)    = return False
+        contains (TVar a)
+            | a == l           = return True
+            | otherwise        = do
+                tvar <- loadTVar a
+                case tvar of
+                    TVar a' | a' == a -> return False
+                    _                 -> contains tvar
+
+free :: M.Map String T -> T -> T
+free m = mkFree
+    where
+        mkFree (deConsTOp -> Just (op, a, b)) = op (mkFree a) (mkFree b)
+        mkFree a@(TNom i)       = a
+        mkFree (TForall n t)    = TForall n $ flip free t $ M.withoutKeys m n
+        mkFree a@(TVar _)       = a
+        mkFree a@(TFresh id)    = M.findWithDefault a id m
+
+prune :: T -> MS TCEnv T
+prune = \case
+        (deConsTOp   -> Just (op, a, b)) -> op <$> prune a <*> prune b
+        a@(TNom i)   -> return a
+        TVar i       ->
+            loadTVar i >>= \case
+                a@(TVar  i') | i' == i -> return a
+                a                      -> do
+                    t <- prune a
+                    update i t
+                    return t
+
+        a@(TFresh _) -> return a
+        TForall a b  -> TForall a <$> prune b
+
+update :: Int -> T -> MS TCEnv ()
+update i t = modifyMS $ over tvars $ M.insert i t
+
+addNEq :: (T, T) -> MS TCEnv ()
+addNEq t = modifyMS $ over neqs (S.insert t)
+
+unify :: Fix (Unif -> MS TCEnv ())
+unify self Unif {lhs, rhs, neq=True} = addNEq (lhs, rhs)
+
+unify self Unif {lhs=TNom a, rhs=TNom b}
+    | a == b      = return ()
+    | otherwise   = empty
+
+unify self Unif {lhs=TVar a, rhs = TVar b} = do
+    recursive <- occurIn a (TVar b)
+    if recursive
+    then error "ill formed definition like a = a -> b"
+    else update a (TVar b)
+
+unify self Unif {lhs=TVar id, rhs, neq} = update id rhs
+
+unify self a@Unif {lhs, rhs=rhs@(TVar _)} = self a {lhs=rhs, rhs=lhs}
+
+-- type operators are not frist class
+unify self Unif {lhs=l1 :-> l2, rhs= r1 :-> r2} =
+    self Unif {lhs=l1, rhs=r1, neq=False} >>
+    self Unif {lhs=l2, rhs=r2, neq=False}
+
+unify self Unif {lhs=l1 :* l2, rhs= r1 :* r2} =
+    self Unif {lhs=l1, rhs=r1, neq=False} >>
+    self Unif {lhs=l2, rhs=r2, neq=False}
+
+-- TODO: type aliases?
+unify self Unif {lhs=TApp l1 l2, rhs= TApp r1 r2} =
+    self Unif {lhs=l1, rhs=r1, neq=False} >>
+    self Unif {lhs=l2, rhs=r2, neq=False}
+
+unify self Unif {lhs=TForall freevars poly, rhs} = do
+    pairs <- mapM freepair $ S.toList freevars
+    let freemap = M.fromList pairs
+    let l = free freemap poly
+    self Unif {lhs=l, rhs=rhs, neq=False}
+    where freepair freevar = (freevar,) . TVar <$> newTVar
+
+unify self a@Unif {lhs, rhs=rhs@(TForall _ _)} =
+    self a {lhs=rhs, rhs=lhs}
+
+instance CtxSolver TCEnv Unif where
+    solve =
+        let frec = unify (pruneUnif >=> frec)
+        in  pruneUnif >=> frec
+        where
+            pruneUnif a@Unif {neq=True} = return a
+            pruneUnif a@Unif {lhs, rhs} = do
+                lhs <- prune lhs
+                rhs <- prune rhs
+                return $ a {lhs=lhs , rhs=rhs}
+
+
+
diff --git a/src/RSolve/HM/Core.hs b/src/RSolve/HM/Core.hs
deleted file mode 100644
--- a/src/RSolve/HM/Core.hs
+++ /dev/null
@@ -1,115 +0,0 @@
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE TupleSections #-}
--- https://github.com/thautwarm/reFining/blob/master/DotNet/reFining/reFining
-
-module RSolve.HM.Core where
-import RSolve.BrMonad
-import RSolve.Infr
-import RSolve.Logic
-import Control.Applicative
-import qualified Data.Map as M
-
-type Id = Int
-
-data TypeOp = Arrow | Join | Stmt
-    deriving (Show, Eq, Ord)
-
-data Prim = Int | Float | Char
-    deriving (Show, Eq, Ord)
-
-
-data Core where
-    Prim   :: Prim -> Core
-
-    Op     :: TypeOp -> Core -> Core -> Core
-
-    Forall :: [Id] -> Core -> Core
-
-    Var    :: Id -> Core
-    deriving (Eq)
-
-instance Show Core where
-    show (Prim a) = show a
-    show (Op Arrow a b) =
-        "(" ++ show a ++ " -> " ++ show b ++ ")"
-    show (Op Join a b) = show a ++ ", " ++ show b
-    show (Op Stmt a b) = show a ++ ";\n" ++ show b
-    show (Forall xs b)  =
-        let f a b = a ++ " a" ++ show b
-        in foldl f "forall " xs ++ "." ++ show b
-    show (Var a) = "a" ++ show a
-
-free :: M.Map Id Core -> Core -> Core
-free m = mkFree
-    where
-        mkFree a@(Prim _) = a
-        mkFree (Op op a b) = Op op (mkFree a) (mkFree b)
-        mkFree (Forall a b) = Forall a (mkFree b)
-        mkFree a@(Var id) =
-            M.findWithDefault a id m
-
-occurIn :: Addr -> Addr -> Br (LState Core) Bool
-occurIn l = contains . Var
-    where
-        contains (Prim _) = return False
-
-        contains (Var a) =
-            if a == l then return True
-            else tryLoad a >>= \case
-                Just a -> contains a
-                _ -> return False
-
-        contains (Op _ a b) = (||) <$> contains a <*> contains b
-        contains (Forall _ a) = contains a
-
-instance Reference Core where
-    mkRef = Var
-    isRef (Var a) = Just a
-    isRef  _      = Nothing
-
-
-instance Unify Core where
-    prune v@(Var a) = tryLoad a >>= \case
-        Just var -> prune var
-        _        -> return v
-
-    prune a@(Prim _) = return a
-
-    prune (Forall a b) = Forall a <$> prune b
-    prune (Op op a b) = Op op <$> prune a <*> prune b
-
-    unify (Prim a) (Prim b) =
-            if a == b then return ()
-            else empty
-
-    unify l@(Var a) r@(Var b)
-        | a == b    = return ()
-        | otherwise = do
-            recursive <- occurIn a b
-            if recursive
-            then error "ill formed definition like a = a -> b"
-            else update a r
-
-    unify l r@(Var _) = unify r l
-
-    unify (Var id)  r = update id r
-
-    -- type operators are not frist class
-    unify (Op opl l1 l2) (Op opr r1 r2) =
-        if opl /= opr then empty
-        else
-            unify l1 r1 >> unify l2 r2
-
-    unify (Forall freevars poly) r = do
-        pairs <- mapM freepair freevars
-        let freemap = M.fromList pairs
-        let l = free freemap poly
-        unify l r
-        where
-            freepair freevar = (freevar,) <$> mkRef <$> new
-
-    unify l r@(Forall _ _) = unify r l
-
-
diff --git a/src/RSolve/Infr.hs b/src/RSolve/Infr.hs
deleted file mode 100644
--- a/src/RSolve/Infr.hs
+++ /dev/null
@@ -1,99 +0,0 @@
-module RSolve.Infr where
-import RSolve.BrMonad
-import Control.Applicative
-import qualified Data.Set  as S
-import qualified Data.Map  as M
-import qualified Data.List as L
-
-type Addr = Int
-class Eq a => Reference a where
-  -- reference can be stored in Map
-  isRef :: a  -> Maybe Addr
-  mkRef :: Addr -> a
-
-class Reference a => Unify a where
-  prune  :: a -> Br (LState a) a
-  unify  :: a -> a -> Br (LState a) ()
-  complement :: a -> a -> Br (LState a) ()
-  complement a b =
-        if a == b then return ()
-        else empty
-
-class EnumSet a where
-  toEnumerable :: Br (LState a) ()
-
-
-data Allocator a =
-  Allocator { storage :: M.Map Addr a
-            , addr    :: Addr }
-  deriving (Show)
-
-
-data LState a =
-   LState { allocator  :: Allocator a
-          , negPairs   :: [(a, a)]
-          , constrains :: [Br (LState a) Bool] }
-
-allocator'  st   (LState _ negs cs) = LState st negs cs
-negPairs'   negs (LState st _   cs) = LState st negs cs
-constrains' cs   (LState st negs _) = LState st negs cs
-
-
-inc :: Reference a => Allocator a -> (Addr, Allocator a)
-inc (Allocator s c) = (c, Allocator s $ c + 1)
-
-alloc :: Reference a => a -> Allocator a -> (Addr, Allocator a)
-alloc a (Allocator s c) = (c, Allocator (M.insert c a s) (c + 1))
-
-renew :: Reference a => Addr -> a -> Allocator a -> Allocator a
-renew addr obj r@(Allocator s c) =
-  case isRef obj of
-    Just addr' | addr' == addr -> r -- avoid recursive definition
-    _ ->  Allocator (M.insert addr obj s) c
-
-store :: (Reference a, Eq a) => a -> Br (LState a) a
-store a = do
-  st <- getBy allocator
-  let (n, st') = alloc a st
-  _ <- putBy $ allocator' st'
-  return $ mkRef n
-
-
--- update state
-update  :: Reference a => Addr -> a -> Br (LState a) ()
-update addr obj = getBy allocator >>= putBy . allocator' . renew addr obj
-
-
-load :: Addr -> Br (LState a) a
-load addr =
-  ((M.! addr) . storage) <$> getBy allocator
-
-
-tryLoad :: Addr -> Br (LState a) (Maybe a)
-tryLoad addr =
-  (M.lookup addr . storage) <$> getBy allocator
-
-
--- for the system which take leverage of generics
-new :: Reference a => Br (LState a) Addr
-new = do
-  st <- getBy allocator
-  let (addr', st') = inc st
-  _ <- putBy $ allocator' st'
-  return addr'
-
-negUnify :: Reference a => a -> a -> Br (LState a) ()
-negUnify a b = do
-  negs <- getBy negPairs
-  if check negs then
-     putBy $ negPairs' ((a, b) : negs)
-  else return ()
-  where
-    check [] = True
-    check ((a', b'):xs)
-      | (a', b') == (a, b) || (a', b') == (b, a) = False
-      | otherwise = check xs
-
-
-emptyAllocator = Allocator M.empty 0
-emptyLState    = LState emptyAllocator [] []
diff --git a/src/RSolve/Logic.hs b/src/RSolve/Logic.hs
--- a/src/RSolve/Logic.hs
+++ b/src/RSolve/Logic.hs
@@ -1,89 +1,8 @@
-{-# LANGUAGE GADTs #-}
 module RSolve.Logic where
-import RSolve.BrMonad
-import RSolve.Infr
-import Data.List (nub)
-import Control.Applicative
 
-data Cond a where
-   Unify :: Unify a => a -> a -> Cond a
-   Not   :: Cond a -> Cond a
-   Pred  :: Br (LState a) Bool -> Cond a
-
-   Or    :: Cond a -> Cond a -> Cond a
-   And   :: Cond a -> Cond a -> Cond a
-   Imply :: Cond a -> Cond a -> Cond a
-
-solve :: Cond a -> Br (LState a) ()
-solve (Unify l r) = do
-  l <- prune l
-  r <- prune r
-  unify l r
-
-solve (Or l r)    =
-  solve l <|> solve (And (Not l) r)
-
-solve (And l r)   =
-  solve l >> solve r
-
-solve (Imply l r) =
-  solve (Not l) <|> solve r
-
-solve (Pred c)    = do
-  cs <- getBy constrains
-  putBy $ constrains' (c:cs)
-
-solve (Not emmm)  =
-  case emmm of
-    Pred  c    -> solve $ Pred (not <$> c)
-    Not emmm   -> solve emmm
-    Or     l r -> solve $ And (Not l)(Not r)
-    And    l r -> solve $ Or  (Not l)(Not r)
-    Imply  l r -> solve $ And  l (Not r)
-    Unify  l r -> do
-     l <- prune l
-     r <- prune r
-     negUnify l r
-
-solveNeg :: Unify a => Br (LState a) ()
-solveNeg = do
-  negs <- getBy negPairs
-  negs <- pruneTuples negs
-  solveNeg' $ nub (negs)
-  where
-    pruneTuples [] = return []
-    pruneTuples ((a, b):xs) = do
-      a <- prune a
-      b <- prune b
-      xs' <- pruneTuples xs
-      let
-        process (Just a) (Just b) = x:xs
-          where
-            mkRef2 a b = (mkRef a, mkRef b)
-            x = if a > b then mkRef2 a b else mkRef2 b a
-        process _ _ = (a, b):xs'
-      return $ process (isRef a) (isRef b)
-    solveNeg' [] = return ()
-    solveNeg' ((a,b):xs) =
-      (a `complement` b) >> solveNeg' xs
-
-solvePred :: EnumSet a => Br (LState a) ()
-solvePred = do
-  _ <- toEnumerable
-  cs <- getBy constrains
-  checkPredicate cs
-  where
-    checkPredicate [] = return ()
-    checkPredicate (x:xs) = do
-      x <- x
-      if x then checkPredicate xs
-      else empty
-
-require :: Unify a => a -> Br (LState a) a
-require a = do
-  a <- prune a
-  case isRef a of
-      Just a -> load a
-      _      -> return a
-
-
+-- atom formula
+class (Show a, Ord a) => AtomF a where
+    -- | Specifies how to handle the negations.
+    --   For the finite and enumerable solutions,
+    --   we can return its supplmentary set.
+    notA :: a -> [a]
diff --git a/src/RSolve/MapLike.hs b/src/RSolve/MapLike.hs
new file mode 100644
--- /dev/null
+++ b/src/RSolve/MapLike.hs
@@ -0,0 +1,51 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE LambdaCase #-}
+
+module RSolve.MapLike where
+import Data.Maybe
+import Data.Kind
+import Prelude hiding (lookup, insert)
+import qualified Data.Map  as M
+import qualified Data.List as L
+import qualified Data.Set  as S
+
+class MapLike m k v | m -> k, m -> v where
+    lookup :: k -> m -> Maybe v
+    (!)    :: m -> k -> v
+    m ! k  = fromJust (lookup k m)
+    insert :: k -> v -> m -> m
+    adjust :: (v -> v) -> k -> m -> m
+    member :: k -> m -> Bool
+    update :: (v -> Maybe v) -> k -> m -> m
+
+
+instance Ord k => MapLike (M.Map k v) k v where
+    lookup = M.lookup
+    (!) = (M.!)
+    insert = M.insert
+    adjust = M.adjust
+    member = M.member
+    update = M.update
+
+instance Eq k => MapLike [(k, v)] k v where
+    lookup = L.lookup
+    insert k v = \case
+        []   -> [(k, v)]
+        (k', v'):xs | k' == k -> (k, v):xs
+        x:xs -> x:insert k v xs
+    adjust f k = \case
+        []   -> []
+        (k', v):xs | k' == k -> (k', f v):xs
+        x:xs -> x:adjust f k xs
+    k `member` m = case lookup k m of
+            Just  _ -> True
+            Nothing -> False
+    update f k = \case
+        [] -> []
+        hd@(k', v):xs | k == k' ->
+            case f v of
+                Just v'  -> (k, v'):tl
+                Nothing  -> hd:tl
+            where tl = update f k xs
diff --git a/src/RSolve/MultiState.hs b/src/RSolve/MultiState.hs
new file mode 100644
--- /dev/null
+++ b/src/RSolve/MultiState.hs
@@ -0,0 +1,43 @@
+-- | state monads extended to have branches
+-- Author: Taine Zhao(thautwarm)
+-- Date: 2018-12
+-- License: MIT
+module RSolve.MultiState where
+import Control.Monad
+import Control.Monad.Fail
+import Control.Applicative
+
+newtype MS s a = MS {runMS :: s -> [(a, s)]}
+
+instance Functor (MS s) where
+  fmap = liftM
+
+instance Applicative (MS s) where
+  pure = return
+  (<*>)  = ap
+
+instance MonadFail (MS s) where
+  fail _ = empty
+
+instance Monad (MS s) where
+  m >>= k =
+    MS $ \s ->
+       let xs = runMS m s
+       in join [runMS (k a) s' | (a, s') <- xs]
+  return a = MS $ \s -> [(a, s)]
+
+instance Alternative (MS s) where
+  empty = MS $ const []
+  ma <|> mb = MS $ \s -> runMS ma s ++ runMS mb s
+
+getMS  :: MS s s
+getMS = MS $ \s -> [(s, s)]
+
+putMS  :: s -> MS s ()
+putMS s = MS $ const [((), s)]
+
+getsMS :: (s -> a) -> MS s a
+getsMS f = MS $ \s -> [(f s, s)]
+
+modifyMS :: (s -> s) -> MS s ()
+modifyMS f = MS $ \s -> [((), f s)]
diff --git a/src/RSolve/Options/Core.hs b/src/RSolve/Options/Core.hs
deleted file mode 100644
--- a/src/RSolve/Options/Core.hs
+++ /dev/null
@@ -1,102 +0,0 @@
-module RSolve.Options.Core where
-import RSolve.BrMonad
-import RSolve.Infr
-import RSolve.Logic
-import Control.Monad
-import Control.Applicative
-import Prelude hiding (not, or, and)
-import qualified Data.Set  as S
-import qualified Data.Map  as M
-import qualified Data.List as L
-
-data Option  = A | B | C | D
- deriving (Eq, Show, Ord, Enum)
-
-data Term    = Var Int | Sol (S.Set Option)
- deriving (Eq, Show)
-
-pruneSol :: Term -> Br (LState Term) (Int, Maybe (S.Set Option))
-pruneSol (Var addr) = do
-  t <- load addr
-  case t of
-    Var addr' -> do
-      r @ (addrLast, _) <- pruneSol t
-      update addr (Var addrLast) >> return r
-    Sol lxs    ->
-      return (addr, Just lxs)
-      -- if S.null lxs then error "emmm"
-      -- else return (addr, Just lxs)
-
-pruneSol r @ (Sol xs) =
-  store r >>= \(Var addr) ->
-  return (addr, Just xs)
-
-instance Reference Term where
-  isRef (Var addr) = Just addr
-  isRef _ = Nothing
-  mkRef a = Var a
-
-
-
-instance Unify Term where
-  prune a = pruneSol a >>= return . Var . fst
-  unify l r =
-    pruneSol l >>= \(lFrom, lxsm) ->
-    pruneSol r >>= \(rFrom, rxsm) ->
-    case (lxsm, rxsm) of
-       (Nothing,   _)   -> update lFrom (Var rFrom)
-       (Just lxs,  _) | S.null lxs -> empty
-       (_, Just rxs)  | S.null rxs -> empty
-       (Just _,    Nothing )   -> unify r l
-       (Just lxs,  Just rxs)   ->
-        let xs = S.intersection lxs rxs in
-        if S.null xs
-        then empty
-        else do
-        new <- store $ Sol xs
-        update lFrom new >> update rFrom new
-
-  complement l r = do
-    (l, Just lxs) <- pruneSol l
-    (r, Just rxs) <- pruneSol r
-    case (S.size lxs, S.size rxs) of
-      (1, 1)   | lxs == rxs -> empty
-      (1, 1)   | lxs /= rxs -> return ()
-      (nl, nr) | nl < nr    -> complement (Var r) (Var l)
-      (nl, nr) | nl >= nr   -> do
-         let
-           x:xs = L.map f . S.toList $ rxs
-           f :: Option -> Br (LState Term) ()
-           f re =
-            let lnew_set = S.delete re lxs
-            in
-            if S.null lnew_set
-            then empty
-            else do
-              lnew <- store . Sol $ lnew_set
-              rnew <- store . Sol . S.singleton $ re
-              update l lnew >> update r rnew
-         L.foldl (<|>) x xs
-
-instance EnumSet Term where
-  toEnumerable = do
-    st <- getBy $ storage . allocator
-    M.foldlWithKey f (return ()) st
-    where
-      f :: Br (LState Term) () -> Addr -> Term -> Br (LState Term) ()
-      f a k b =
-        case b of
-          Var _ -> a
-          Sol set ->
-            let
-              lst = S.toList set
-              g :: [Option] -> Br (LState Term) ()
-              g [] = error "unexpected"
-              g (x:xs) = do
-                x <- store . Sol . S.singleton $ x
-                let s = update k x
-                case xs of
-                  [] -> s
-                  _  -> s <|> g xs
-            in a >> g lst
-
diff --git a/src/RSolve/PropLogic.hs b/src/RSolve/PropLogic.hs
new file mode 100644
--- /dev/null
+++ b/src/RSolve/PropLogic.hs
@@ -0,0 +1,72 @@
+-- | Propositional logic infrastructures
+-- Author: Taine Zhao(thautwarm)
+-- Date: 2019-08-03
+-- License: MIT
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE DeriveFunctor #-}
+
+module RSolve.PropLogic
+    (AtomF(..), WFF(..), NF(..), assertNF, normal, assert, unionEquations)
+where
+
+import RSolve.Logic
+import RSolve.MultiState
+import Control.Applicative ((<|>))
+import qualified Data.Set as S
+
+infixl 5 :&&, :&&:
+infixl 3 :||, :||:, :=>:
+
+data WFF a
+    -- | Atom formula, should be specified by the problem
+    = Atom a
+    | Not  (WFF a)
+    -- | And
+    | WFF a :&&: WFF a
+    -- | Or
+    | WFF a :||: WFF a
+    -- | Implication
+    | WFF a :=>:  WFF a
+    deriving (Functor, Eq, Ord)
+
+-- | normalized WWF, where '[NF a]' the disjunctive normal form.
+data NF a
+    = AtomN a
+    | NF a :&& NF a
+    | NF a :|| NF a
+    deriving (Functor, Eq, Ord)
+
+normal :: AtomF a => WFF a -> NF a
+normal = \case
+    Atom a -> AtomN a
+    p1 :&&: p2  -> normal p1 :&& normal p2
+    p1 :||: p2  -> normal p1 :|| normal (Not p1 :&&: p2)
+    Not (Atom a) ->
+        case map AtomN $ notA a of
+            hd:tl -> foldl (:||) hd tl
+            []    -> error $ "Supplementary set of " ++ show a ++ " is empty!"
+    Not (Not p)  -> normal p
+    Not (p1 :&&: p2) -> normal (Not p1) :|| normal (Not p2)
+    Not (p1 :||: p2) -> normal (Not p1) :&& normal (Not p2)
+    Not (p1 :=>: p2) -> normal (Not p1 :||: p2)
+
+assertNF :: AtomF a => NF a -> MS (S.Set a) ()
+assertNF = \case
+    AtomN a   -> modifyMS (S.insert a)
+    p1 :&& p2 -> assertNF p1 >> assertNF p2
+    p1 :|| p2 -> assertNF p1 <|> assertNF p2
+
+
+-- | Use a propositinal logic formula to build logic equations
+--   incrementally.
+assert :: AtomF a => WFF a -> MS (S.Set a) ()
+assert = assertNF . normal
+
+-- | Produced a list of disjunctions of conjunctive clauses.
+unionEquations :: AtomF a  => MS (S.Set a) () -> [[a]]
+unionEquations m =
+    -- get states
+    let sts = map snd $ runMS m S.empty
+    -- unique states
+    in map S.toList . S.toList . S.fromList $ sts
+
diff --git a/src/RSolve/Solver.hs b/src/RSolve/Solver.hs
new file mode 100644
--- /dev/null
+++ b/src/RSolve/Solver.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+module RSolve.Solver where
+import RSolve.Logic
+import RSolve.MultiState
+
+class AtomF a => CtxSolver s a where
+    -- | Give a atom formula and solve it
+    solve :: a -> MS s ()
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,92 @@
+-- import RSolve.Options.Example
+-- import RSolve.HM.Example
+
+
+-- test1 =
+--     putStrLn "HM unification"   >>
+--     hmUnificationExample        >>
+--     putStrLn "4-option puzzles" >>
+--     optionExample
+
+-- main = print 233
+
+
+-- test2 = do
+--   a <- store $ sol [A, B, C]
+--   b <- store $ sol [B, C, D]
+--   c <- store $ sol [C]
+--   _ <- solve $ a `eq`  b
+--   _ <- solve $ b `neq` c
+--   _ <- solveNeg  -- `Not` condition requires this
+--   _ <- solvePred -- unnecessary
+--   mapM require [a, b, c]
+
+-- main = do
+--     format ["a", "b", "c"] . nub . L.map fst
+--     $ runBr test2 emptyLState
+
+import RSolve.HM
+import RSolve.PropLogic
+import RSolve.MultiState
+import RSolve.Solver
+import Control.Monad
+
+import qualified Data.Set as S
+
+import Data.List (delete)
+import Control.Monad
+
+data Value = A | B | C | D
+    deriving (Show, Eq, Ord, Enum)
+
+data At = At {at_l :: String, at_r :: Value}
+    deriving (Show, Eq, Ord)
+
+instance AtomF At where
+    notA At {at_l = lhs, at_r = rhs} =
+        let wholeSet  = enumFrom (toEnum 0) :: [Value]
+            contrasts = delete rhs wholeSet
+        in [At {at_l = lhs, at_r = rhs'} | rhs' <- contrasts]
+
+infix 6 <==>
+s <==> v = Atom $ At s v
+equations = do
+    assert $ "a" <==> A :||: "a" <==> B
+    assert $ "b" <==> C :||: "b" <==> D
+    assert $ Not ("a" <==> A)
+    assert $ Not ("a" <==> B :=>: "b" <==> C)
+
+
+infixl 6 <=>
+a <=> b = Atom $ Unif {lhs=a, rhs=b, neq=False}
+solu = do
+    a <- newTVar
+    b <- newTVar
+    c <- newTVar
+    d <- newTVar
+    let [eqs] = unionEquations $
+                do
+                assert $ TVar a <=> TForall (S.fromList ["s"]) ((TFresh "s") :-> (TFresh "s" :* TFresh "s"))
+                assert $ TVar a <=> (TVar b :-> (TVar c :* TVar d))
+                assert $ TVar d <=> TNom 1
+    forM_ eqs solve
+    a <- prune $ TVar a
+    b <- prune $ TVar b
+    c <- prune $ TVar c
+    return (a, b, c)
+
+test :: Eq a => String -> a -> a -> IO ()
+test msg a b
+    | a == b = return ()
+    | otherwise = print msg
+
+main = do
+    forM (unionEquations equations) $ \xs ->
+        case xs of
+            [a, b] -> print xs
+            _      -> return ()
+
+    let (a, b, c):_ = map fst $ runMS solu emptyTCEnv
+    test "1 failed" (show a) "@t1 -> @t1 * @t1"
+    test "2 failed" (show b) "@t1"
+    test "3 failed" (show c) "@t1"