diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2018 
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,93 @@
+# RSolve
+
+A general solver for type checkers of programming languages and real world puzzles with complex constraints. 
+
+
+## Preview
+
+Here are 2 special cases presented in the following sections to show how powerful `RSolve` is.
+
+### The Most Graceful Hindley-Milner Unification
+
+Check `RSolve.HM.Core` and `RSolve.HM.Example`.  
+
+Uncomment the code in `Main.hs` could reproduce following program:
+
+```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)
+
+    let arrow_match = Op Arrow (Var u4) (Var u4)
+
+    _ <- solve $ Unify arrow arrow_var
+    _ <- solve $ Unify arrow_inst1 arrow_match
+    _ <- solve $ Unify arrow_generic arrow_inst1
+    _ <- solve $ Unify arrow_generic arrow_inst2
+    _ <- solveNeg
+
+    mapM require [Var u1, Var u2, arrow_inst1, arrow_inst2, arrow_generic, arrow_match]
+  
+```
+
+output:
+
+```
+u1 : Int
+u2 : Float
+arrow_inst1 : (Int -> Int)
+arrow_inst2 : (Float -> Float)
+arrow_generic : forall  a2.(a2 -> a2)
+arrow_match : (Int -> Int)
+```
+
+### N-Option Puzzles
+
+This implememtation is presented at `RSolve.Options`,  which provides the abstractions to solve all kinds of puzzles described with options.
+
+A Hello World program could be found at `src/Main.hs` which solves a complex problem described with following link:
+
+https://www.zhihu.com/question/68411978/answer/558913247.
+
+
+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:
+
+```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
+```
+
+output:
+
+```
+λ stack exec RSolve
+====
+"a" : Sol (fromList [B])
+"b" : Sol (fromList [B])
+"c" : Sol (fromList [C])
+```
diff --git a/RSolve.cabal b/RSolve.cabal
new file mode 100644
--- /dev/null
+++ b/RSolve.cabal
@@ -0,0 +1,41 @@
+name:                RSolve
+version:             0.1.0.0
+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
+
+source-repository head
+  type:     git
+  location: https://github.com/thautwarm/Rsolver.git
+
+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
+
+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
+
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/src/Main.hs b/src/Main.hs
new file mode 100644
--- /dev/null
+++ b/src/Main.hs
@@ -0,0 +1,26 @@
+module Main where
+import RSolve.Options.Example
+import RSolve.HM.Example
+
+
+main =
+    putStrLn "HM unification"   >>
+    hmUnificationExample        >>
+    putStrLn "4-option puzzles" >>
+    optionExample
+
+
+
+-- 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
diff --git a/src/RSolve/BrMonad.hs b/src/RSolve/BrMonad.hs
new file mode 100644
--- /dev/null
+++ b/src/RSolve/BrMonad.hs
@@ -0,0 +1,26 @@
+module RSolve.BrMonad where
+import Control.Monad
+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 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/Core.hs b/src/RSolve/HM/Core.hs
new file mode 100644
--- /dev/null
+++ b/src/RSolve/HM/Core.hs
@@ -0,0 +1,115 @@
+{-# 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/HM/Example.hs b/src/RSolve/HM/Example.hs
new file mode 100644
--- /dev/null
+++ b/src/RSolve/HM/Example.hs
@@ -0,0 +1,54 @@
+module RSolve.HM.Example where
+import RSolve.HM.Core
+import RSolve.BrMonad
+import RSolve.Infr
+import RSolve.Logic
+import Control.Monad
+
+test = 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
+
+
+    let arrow_match = Op Arrow (Var u4) (Var u4)
+
+    -- a generic function
+    let arrow_generic = Forall [u3] $ Op Arrow (Var u3) (Var u3)
+
+    _ <- solve $ Unify arrow arrow_var
+    _ <- solve $ Unify arrow_inst1 arrow_match
+    _ <- solve $ Unify arrow_generic arrow_inst1
+    _ <- solve $ Unify arrow_generic arrow_inst2
+    _ <- solveNeg
+
+    mapM require [Var u1, Var u2, arrow_inst1, arrow_inst2, arrow_generic, arrow_match]
+
+format :: [(String, Core)] -> IO ()
+format [] = do
+    putStrLn "================="
+format ((a, b):xs) = do
+    _ <- putStrLn $ a ++ " : " ++ show b
+    format xs
+formayMany fields lst =
+    forM_ [zip fields items | items <- lst] format
+
+
+hmUnificationExample = do
+    let fields = ["u1", "u2", "arrow_inst1", "arrow_inst2", "arrow_generic", "arrow_match"]
+    formayMany fields . map fst $ runBr test emptyLState
diff --git a/src/RSolve/Infr.hs b/src/RSolve/Infr.hs
new file mode 100644
--- /dev/null
+++ b/src/RSolve/Infr.hs
@@ -0,0 +1,99 @@
+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
new file mode 100644
--- /dev/null
+++ b/src/RSolve/Logic.hs
@@ -0,0 +1,89 @@
+{-# 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
+
+
diff --git a/src/RSolve/Options/Core.hs b/src/RSolve/Options/Core.hs
new file mode 100644
--- /dev/null
+++ b/src/RSolve/Options/Core.hs
@@ -0,0 +1,102 @@
+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/Options/Example.hs b/src/RSolve/Options/Example.hs
new file mode 100644
--- /dev/null
+++ b/src/RSolve/Options/Example.hs
@@ -0,0 +1,186 @@
+module RSolve.Options.Example where
+import RSolve.Options.Core
+import RSolve.BrMonad
+import RSolve.Infr
+import RSolve.Logic
+import Control.Monad
+import Prelude hiding (not, or, and)
+import qualified Data.Set  as S
+import qualified Data.Map  as M
+import qualified Data.List as L
+
+nub = L.nub
+sol = Sol . S.fromList
+total = [A, B, C, D]
+toSol a = do
+  (_, Just b) <- pruneSol a
+  if S.size b /= 1 then error $ show b
+  else return $ S.elemAt 0 b
+eq a b  = Unify a b
+neq a b = Not $ a `eq` b
+not = Not
+and = And
+or  = Or
+(|-) a b = Imply a b
+
+(==>) :: Option -> (Cond Term) -> Term -> (Cond Term)
+(==>) a b c = c `eq` sol [a] `and` b
+
+(|||)   :: (Term -> (Cond Term)) -> (Term -> Cond Term) -> (Term -> Cond Term)
+a ||| b = \t -> a t `or` b t
+
+for :: Term -> (Term -> Cond Term) -> Br (LState Term) ()
+for a f = solve $ f a
+
+infixr 7 `eq`, `neq`
+infixr 5 `or`
+infixr 6 `and`, |-
+infixr 4 ==>
+infixr 3 |||
+
+test = do
+  _1 <- store $ sol total
+  _2 <- store $ sol total
+  _3 <- store $ sol total
+  _4 <- store $ sol total
+  _5 <- store $ sol total
+  _6 <- store $ sol total
+  _7 <- store $ sol total
+  _8 <- store $ sol total
+  _9 <- store $ sol total
+  _10 <- store $ sol total
+  _ <- for _2 $
+    A ==> _5 `eq` sol [C] |||
+    B ==> _5 `eq` sol [D] |||
+    C ==> _5 `eq` sol [A] |||
+    D ==> _5 `eq` sol [B]
+  _  <- for _3 $
+    let
+       diff3 :: [Term] -> Term -> Cond Term
+       diff3 lst a =
+         let conds = [a `neq` e | e <- L.delete a lst]
+         in case conds of
+                []   -> error "emmm"
+                x:xs -> L.foldl and x xs
+       f = diff3 [_3, _6, _2, _4]
+    in A ==> f _3 |||
+       B ==> f _6 |||
+       C ==> f _2 |||
+       D ==> f _4
+  _ <- for _4 $
+     A ==> _1 `eq` _5 |||
+     B ==> _2 `eq` _7 |||
+     C ==> _1 `eq` _9 |||
+     D ==> _6 `eq` _10
+  _ <- for _5 $
+     A ==> _5 `eq` _8 |||
+     B ==> _5 `eq` _4 |||
+     C ==> _5 `eq` _9 |||
+     D ==> _5 `eq` _7
+  _ <- for _6 $
+     A ==> _2 `eq` _8 `and` _4 `eq` _8   |||
+     B ==> _1 `eq` _8 `and`  _6 `eq` _8  |||
+     C ==> _3 `eq` _8 `and`  _10 `eq` _8 |||
+     D ==> _5 `eq` _8 `and` _9 `eq` _8
+  let
+    solution = do
+      mapM toSol [_1, _2, _3, _4, _5, _6, _7, _8, _9, _10]
+    count :: Br (LState Term) (M.Map Option Int)
+    count = do
+      solution <- solution
+      return . countImpl $ solution
+      where
+        countImpl :: [Option] -> M.Map Option Int
+        countImpl [] = M.empty
+        countImpl (x:xs) = M.alter f x $ countImpl xs
+        f Nothing = Just 1
+        f (Just a) = Just $ a + 1
+    msearch cond = do
+      count <- count
+      return $ M.foldlWithKey f [] count
+      where
+        f [] k v = [(k, v)]
+        f r@((k', v'):_) k v =
+         case compare v v' of
+           a | a == cond  -> [(k, v)]
+           EQ -> (k, v) : r
+           _ -> r
+    msearchNSuite :: (Int -> Int -> Bool) -> Option -> Br (LState Term) (Maybe Int)
+    msearchNSuite cond opt = do
+      count <- count
+      case M.lookup opt count of
+        Nothing -> do
+
+          return (Just 0)
+        Just n  ->
+          let
+            f Nothing k v = Nothing
+            f r@(Just a) k v =
+              if cond v n then Nothing
+              else r
+          in return $ M.foldlWithKey f (Just n) count
+  _ <- for _7 $
+     let minIs a =
+           let m = do
+                 lst <- msearch LT
+                 return $ L.all (\(k, v) -> k == a) lst
+           in Pred m
+     in A ==> minIs C |||
+        B ==> minIs B |||
+        C ==> minIs A |||
+        D ==> minIs D
+  _ <- for _8 $
+     let
+       notAdjacent a b = do
+         a <- toSol a
+         b <- toSol b
+         let sep = (fromEnum a - fromEnum b)
+         return $ abs(sep) > 1
+     in A ==> Pred (notAdjacent _1 _7)  |||
+        B ==> Pred (notAdjacent _1 _5)  |||
+        C ==> Pred (notAdjacent _1 _2)  |||
+        D ==> Pred (notAdjacent _1 _10)
+  _ <- for _9 $
+     let
+       f x =
+        let a = _1 `eq` _6 in
+        let b = x  `eq` _5 in
+        not a `and` b `or` not b `and` a
+     in A ==> f _6  |||
+        B ==> f _10 |||
+        C ==> f _2  |||
+        D ==> f _9
+  _ <- for _10 $
+    let
+      by a =
+        Pred m
+        where m = do
+               (_, minCount):_ <- msearch LT
+               (_, maxCount):_ <- msearch GT
+               return $ maxCount - minCount == a
+    in A ==> by 3 |||
+       B ==> by 2 |||
+       C ==> by 4 |||
+       D ==> by 1
+  _ <- solveNeg
+  _ <- solvePred
+  mapM require [_1, _2, _3, _4, _5, _6, _7, _8, _9, _10]
+
+format :: [String] -> [[Term]] -> IO ()
+format names xs =
+  let
+    formatCell :: (String, Term) -> IO()
+    formatCell (a, b) = putStrLn $ show a ++ " : " ++ show b
+    formatLine :: [(String, Term)] -> IO()
+    formatLine xs = do
+      _ <- putStrLn "===="
+      forM_ xs formatCell
+    formatLines xs =
+      forM_ xs $ \line -> formatLine $ L.zip names line
+  in formatLines xs
+
+
+
+optionExample = do
+    format [show i | i <- [1..10]] . nub . L.map fst
+    $ runBr test emptyLState