diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..1d0658a --- /dev/null +++ b/.gitignore @@ -0,0 +1,19 @@ +# binaries +* + +# compilation intermediate files +*.hi +*.ho + +# vim generates these +*.swp +*.swo + +# include directories +!*/ + +# include files with an extension +!*.* + +# special cases +!Makefile diff --git a/Logic/Parse.hs b/Logic/Parse.hs new file mode 100644 index 0000000..4956bee --- /dev/null +++ b/Logic/Parse.hs @@ -0,0 +1,77 @@ +module Logic.Parse where + +import Control.Applicative (Applicative, Alternative(..)) +import Data.Functor (Functor) + +newtype Parser output = Parser + { runParser :: Input -> Either ParseError (output, Input) + } + +data Input = Input + { inputPos :: Int + , inputSeq :: [Char] + } deriving (Eq, Show) + +mkInput :: [Char] -> Input +mkInput = Input 0 + +data ParseError = + ParseError Int String + deriving (Show) + +expected :: String -> Input -> ParseError +expected thing input = ParseError (inputPos input) $ + "expected " <> thing <> ", found " <> show (take 20 $ inputSeq input) + +eof :: Parser a -> Input -> Either ParseError a +eof p input = do + (result, rest) <- runParser p input + case inputSeq rest of + [] -> Right result + _ -> Left $ expected "end of input" rest + +instance Functor Parser where + fmap :: (a -> b) -> Parser a -> Parser b + fmap f (Parser p) = Parser $ \input -> do + (result, rest) <- p input + return (f result, rest) + +instance Applicative Parser where + pure :: a -> Parser a + pure result = Parser $ \input -> Right (result, input) + + (Parser p1) <*> (Parser p2) = + Parser $ \input -> do + (f, rest) <- p1 input + (result, rest') <- p2 rest + return (f result, rest') + +instance Alternative Parser where + empty :: Parser a + empty = Parser $ const empty + + (Parser p1) <|> (Parser p2) = + Parser $ \input -> p1 input <|> p2 input + +instance Alternative (Either ParseError) where + empty :: Either ParseError a + empty = Left $ ParseError 0 "this parser always fails" + + (Right x) <|> _ = Right x + (Left _) <|> e = e + +parseToken :: String -> Parser String +parseToken token = Parser parse + where + n = length token + parse input@(Input pos xs) + | token == take n xs = Right $ (token,) $ Input (pos + n) (drop n xs) + | otherwise = Left $ expected (show token) input + +parseIf :: String -> (Char -> Bool) -> Parser Char +parseIf description check = Parser $ \input -> + case inputSeq input of + [] -> Left $ ParseError (inputPos input) "unexpected end of input" + (char:chars) + | check char -> Right $ (char,) $ Input (inputPos input + 1) chars + | otherwise -> Left $ expected description input diff --git a/Logic/Statement.hs b/Logic/Statement.hs new file mode 100644 index 0000000..6902140 --- /dev/null +++ b/Logic/Statement.hs @@ -0,0 +1,22 @@ +module Logic.Statement where + +import Data.Set (singleton, union, toAscList) + +data Statement + = Atom String + | Not Statement + | And Statement Statement + | Or Statement Statement + | Implies Statement Statement + | Iff Statement Statement + deriving (Show, Eq) + +atoms :: Statement -> [String] +atoms = toAscList . mkSet + where + mkSet (Atom key) = singleton key + mkSet (Not s) = mkSet s + mkSet (And s1 s2) = union (mkSet s1) (mkSet s2) + mkSet (Or s1 s2) = union (mkSet s1) (mkSet s2) + mkSet (Implies s1 s2) = union (mkSet s1) (mkSet s2) + mkSet (Iff s1 s2) = union (mkSet s1) (mkSet s2) diff --git a/Logic/Statement/Eval.hs b/Logic/Statement/Eval.hs new file mode 100644 index 0000000..83d716c --- /dev/null +++ b/Logic/Statement/Eval.hs @@ -0,0 +1,47 @@ +module Logic.Statement.Eval where + +import Logic.Statement (Statement(..), atoms) + +import Data.List (intercalate) +import Data.Either (fromRight) + +data Bucket + = Tautology + | Contradiction + | Contingent + deriving (Eq, Show) + +bucket :: Statement -> Bucket +bucket s + | and values = Tautology + | all not values = Contradiction + | otherwise = Contingent + where + values = [fromRight undefined $ eval assignments s | assignments <- enumerate $ atoms s] + +eval :: [(String, Bool)] -> Statement -> Either String Bool +eval assignments = aux + where + aux (Atom key) = maybe (Left key) Right $ lookup key assignments + aux (Not s) = not <$> aux s + aux (And s1 s2) = (&&) <$> aux s1 <*> aux s2 + aux (Or s1 s2) = (||) <$> aux s1 <*> aux s2 + aux (Implies s1 s2) = not <$> ((&&) <$> aux s1 <*> (not <$> aux s2)) + aux (Iff s1 s2) = (==) <$> aux s1 <*> aux s2 + +enumerate :: [a] -> [[(a, Bool)]] +enumerate keys = map reverse $ aux start + where + aux assignments = (assignments:) $ + case next assignments of + Nothing -> [] + Just (assignments') -> aux assignments' + + start = map (, False) keys + + next [] = Nothing + next ((key, False):rest) = Just $ (key, True):rest + next ((key, True):rest) = ((key, False):) <$> (next rest) + +implies :: Bool -> Bool -> Bool +implies b1 b2 = not b1 || b2 diff --git a/Logic/Statement/Parse.hs b/Logic/Statement/Parse.hs new file mode 100644 index 0000000..d256a43 --- /dev/null +++ b/Logic/Statement/Parse.hs @@ -0,0 +1,49 @@ +module Logic.Statement.Parse where + +import Logic.Parse + ( Parser(..) + , Input(..) + , ParseError + , expected + , parseToken + , parseIf + ) +import Logic.Statement (Statement(..)) + +import Control.Applicative (Alternative((<|>), some)) +import Data.Char (isAlphaNum) + +stmtAtom :: Parser Statement +stmtAtom = Atom <$> parse + where + parse = some $ parseIf "statement variable" $ \char -> isAlphaNum char || char == '_' + +stmtNot :: Parser Statement +stmtNot = Not <$> (parseToken "!" *> stmt) + +stmtBinary :: Parser Statement +stmtBinary = parseToken "(" *> body <* parseToken ")" + where + body = (\s1 f s2 -> f s1 s2) <$> stmt <*> parseConnective <*> stmt + + parseConnective = + fmap (const And) (parseToken "&") + <|> fmap (const Or) (parseToken "|") + <|> fmap (const Implies) (parseToken "->") + <|> fmap (const Iff) (parseToken "<->") + <|> fail + + fail = Parser $ \input -> Left $ expected "connective" input + +stmt :: Parser Statement +stmt = Parser $ \input -> + let + parser = + case inputSeq input of + [] -> fail + ('!':_) -> stmtNot + ('(':_) -> stmtBinary + _ -> stmtAtom <|> fail + in runParser parser input + where + fail = Parser $ \input -> Left $ expected "statement" input diff --git a/Logic/Statement/Serialize.hs b/Logic/Statement/Serialize.hs new file mode 100644 index 0000000..fa76f5b --- /dev/null +++ b/Logic/Statement/Serialize.hs @@ -0,0 +1,173 @@ +module Logic.Statement.Serialize where + +import Logic.Statement (Statement(..), atoms) +import Logic.Statement.Eval (enumerate, eval, implies) + +import Data.List (intercalate) +import Data.Either (fromRight) + +data TokenString = TokenString + { tsCanEval :: CanEval + , tsLevel :: Int + , tsString :: String + } deriving (Show, Eq) + +data CanEval + = Filler + | CanEval + deriving (Show, Eq) + +data TokenValue = TokenValue + { tvLevel :: Int + , tvValue :: Value + } deriving (Show, Eq) + +data Value + = NoValue + | Value Bool + deriving (Show, Eq) + +data SerializeFormat + = Plain + | Latex +-- | PrefixPlain + deriving (Show, Eq) + +serialize :: SerializeFormat -> Statement -> String +serialize fmt s = concat $ map tsString $ serializeStrings fmt s + +serializeStrings :: SerializeFormat -> Statement -> [TokenString] +serializeStrings fmt = aux 0 + where + aux :: Int -> Statement -> [TokenString] + aux = + case fmt of + Plain -> serializeStringsPlain + Latex -> serializeStringsLatex + +-- Internal function +serializeStringsPlain :: Int -> Statement -> [TokenString] +serializeStringsPlain level = aux + where + f = serializeStringsPlain + level' = level + 1 + + aux (Atom key) = [TokenString CanEval level key] + aux (Not s) = [TokenString CanEval level "!"] ++ f level' s + aux (And s1 s2) = connective level "&" (f level' s1) (f level' s2) + aux (Or s1 s2) = connective level "|" (f level' s1) (f level' s2) + aux (Implies s1 s2) = connective level "->" (f level' s1) (f level' s2) + aux (Iff s1 s2) = connective level "<->" (f level' s1) (f level' s2) + +-- Internal function +serializeStringsLatex :: Int -> Statement -> [TokenString] +serializeStringsLatex level = aux + where + f = serializeStringsLatex + level' = level + 1 + + aux (Atom key) = [TokenString CanEval level key] + aux (Not s) = [TokenString CanEval level "\\neg "] ++ f level' s + aux (And s1 s2) = connective level "\\land " (f level' s1) (f level' s2) + aux (Or s1 s2) = connective level "\\lor " (f level' s1) (f level' s2) + aux (Implies s1 s2) = connective level "\\to " (f level' s1) (f level' s2) + aux (Iff s1 s2) = connective level "\\leftrightarrow " (f level' s1) (f level' s2) + +-- Internal function +connective :: Int -> String -> [TokenString] -> [TokenString] -> [TokenString] +connective level middle tokens1 tokens2 = + [TokenString Filler level "("] + ++ tokens1 + ++ [TokenString CanEval level middle] + ++ tokens2 + ++ [TokenString Filler level ")"] + +-- Using infix convention with brackets +serializeValues :: [(String, Bool)] -> Statement -> Either String [TokenValue] +serializeValues ass = fmap snd . aux 0 + where + aux :: Int -> Statement -> Either String (Bool, [TokenValue]) + aux level s@(Atom key) = do + bool <- eval ass s + return (bool, [TokenValue level $ Value bool]) + aux level (Not s) = do + (bool, tokens) <- aux (level + 1) s + return (not bool, [TokenValue level $ Value $ not bool] ++ tokens) + aux level (And s1 s2) = connective level (&&) s1 s2 + aux level (Or s1 s2) = connective level (||) s1 s2 + aux level (Implies s1 s2) = connective level implies s1 s2 + aux level (Iff s1 s2) = connective level (==) s1 s2 + + connective + :: Int + -> (Bool -> Bool -> Bool) + -> Statement + -> Statement + -> Either String (Bool, [TokenValue]) + connective level f s1 s2 = do + (bool1, tokens1) <- aux (level + 1) s1 + (bool2, tokens2) <- aux (level + 1) s2 + let bracket = [TokenValue level NoValue] + let bool = f bool1 bool2 + return (bool, bracket ++ tokens1 ++ [TokenValue level $ Value bool] ++ tokens2 ++ bracket) + +serializeLatexTruthTable :: Statement -> String +serializeLatexTruthTable s = open <> header <> "\\hline\n" <> body <> close + where + open :: String + open = "\\begin{tabular}{" <> replicate (length $ atoms s) 'c' <> "||" <> spec <> "}\n" + + close :: String + close = "\\end{tabular}\n" + + spec :: String + spec + | length serial == 0 = undefined + | length serial == 1 = "c" + | isMain (head serial) = "c|" <> replicate (length serial - 1) 'c' + | isMain (serial !! (length serial - 1)) = replicate (length serial - 1) 'c' <> "|c" + | otherwise = concat $ map (\token -> if isMain token then "|c|" else "c") serial + + isMain :: TokenString -> Bool + isMain (TokenString CanEval level string) = level == 0 + isMain _ = False + + serial :: [TokenString] + serial = serializeStrings Latex s + + header :: String + header = + intercalate " & " (map dollars $ atoms s) <> + " & " <> + intercalate " & " (map dollars $ map tsString serial) <> + " \\\\\n" + + dollars :: String -> String + dollars string = "$" <> string <> "$" + + body :: String + body = concat $ map line $ enumerate $ atoms s + + line :: [(String, Bool)] -> String + line ass = + intercalate " & " (bools ass) <> + " & " <> + intercalate " & " (cells ass) <> + "\\\\\n" + + bools :: [(String, Bool)] -> [String] + bools ass = [if bool then "1" else "0" | (key, bool) <- ass] + + cells :: [(String, Bool)] -> [String] + cells ass = map cell $ fromRight undefined $ serializeValues ass s + + cell :: TokenValue -> String + cell (TokenValue level value) = + case value of + NoValue -> "" + Value bool -> mkBold level $ if bool then "1" else "0" + + mkBold :: Int -> String -> String + mkBold level string + | level == 0 = "\\textbf " <> string + | otherwise = string diff --git a/Main.hs b/Main.hs index 2ff6318..f3effef 100644 --- a/Main.hs +++ b/Main.hs @@ -1,274 +1,23 @@ -import Control.Applicative (Applicative, Alternative(..)) -import Data.Char (isAlphaNum) -import Data.Functor (Functor) -import Data.List (intercalate) -import Data.Maybe (fromJust) -import qualified Data.Set as S +module Main where -newtype Parser symbol output = Parser - { runParser :: [symbol] -> Maybe (output, [symbol]) - } +import Logic.Parse (eof, mkInput, ParseError(..)) +import Logic.Statement.Parse (stmt) +import Logic.Statement.Eval (bucket) +import Logic.Statement.Serialize (serializeLatexTruthTable) -instance Functor (Parser s) where - fmap :: (a -> b) -> Parser s a -> Parser s b - fmap f (Parser p) = Parser - { runParser = \xs -> do - (result, xs') <- p xs - return (f result, xs') - } - -instance Applicative (Parser s) where - pure :: a -> Parser s a - pure result = Parser $ \xs -> Just (result, xs) - - (Parser p1) <*> (Parser p2) = - Parser $ \xs -> do - (f, xs') <- p1 xs - (result, xs'') <- p2 xs' - return (f result, xs'') - -instance Alternative (Parser s) where - empty :: Parser s a - empty = Parser $ const Nothing - - (Parser p1) <|> (Parser p2) = - Parser $ \xs -> p1 xs <|> p2 xs - -data Statement - = Atom String - | Not Statement - | And Statement Statement - | Or Statement Statement - | Implies Statement Statement - | Iff Statement Statement - deriving (Show, Eq) - -parseToken :: String -> Parser Char String -parseToken token = Parser parse +main :: IO () +main = do + line <- getLine + case eof stmt $ mkInput line of + Left err -> fail err + Right statement -> do + putStrLn $ show statement + putStrLn $ show $ bucket statement + putStr $ serializeLatexTruthTable statement where - n = length token - parse xs - | token == take n xs = Just (token, drop n xs) - | otherwise = Nothing - -parseWhile :: (Char -> Bool) -> Parser Char String -parseWhile check = Parser parse - where - parse [] = Nothing - parse (token:rest) - | check token = - case parse rest of - Nothing -> Just ([token], rest) - Just (tokens, rest') -> Just (token:tokens, rest') - | otherwise = Nothing - -parseBrackets :: Parser Char a -> Parser Char a -parseBrackets p = parseToken "(" *> p <* parseToken ")" - -parseInfix :: String -> Parser Char a -> Parser Char a -> Parser Char (a, a) -parseInfix token p1 p2 = (,) <$> (p1 <* parseToken token) <*> p2 - -parseConnective :: String -> Parser Char a -> Parser Char a -> Parser Char (a, a) -parseConnective token p1 p2 = parseBrackets $ parseInfix token p1 p2 - -stmtAtom :: Parser Char Statement -stmtAtom = Atom <$> parse - where - parse = parseWhile $ \char -> isAlphaNum char || char == '_' - -stmtNot :: Parser Char Statement -stmtNot = Not <$> (parseToken "!" *> stmt) - -stmtAnd :: Parser Char Statement -stmtAnd = uncurry And <$> parseConnective "&" stmt stmt - -stmtOr :: Parser Char Statement -stmtOr = uncurry Or <$> parseConnective "|" stmt stmt - -stmtImplies :: Parser Char Statement -stmtImplies = uncurry Implies <$> parseConnective "->" stmt stmt - -stmtIff :: Parser Char Statement -stmtIff = uncurry Iff <$> parseConnective "<->" stmt stmt - -stmt :: Parser Char Statement -stmt = stmtAtom <|> stmtNot <|> stmtAnd <|> stmtOr <|> stmtImplies <|> stmtIff - -{- -ghci> runParser stmt "(!a<->((!(p->q)&x)|y))" -Just (Iff (Not (Atom "a")) (Or (And (Not (Implies (Atom "p") (Atom "q"))) (Atom "x")) (Atom "y")),"") --} - -p :: Statement -p = fromJust $ fst <$> runParser stmt "((a->b)<->!c)" - -q :: Statement -q = fromJust $ fst <$> runParser stmt "(!a<->((!(p->q)&x)|y))" - -atoms :: Statement -> S.Set String -atoms (Atom key) = S.singleton key -atoms (Not s) = atoms s -atoms (And s1 s2) = S.union (atoms s1) (atoms s2) -atoms (Or s1 s2) = S.union (atoms s1) (atoms s2) -atoms (Implies s1 s2) = S.union (atoms s1) (atoms s2) -atoms (Iff s1 s2) = S.union (atoms s1) (atoms s2) - -eval :: [(String, Bool)] -> Statement -> Maybe Bool -eval assignments = aux - where - aux (Atom key) = lookup key assignments - aux (Not s) = not <$> aux s - aux (And s1 s2) = (&&) <$> aux s1 <*> aux s2 - aux (Or s1 s2) = (||) <$> aux s1 <*> aux s2 - aux (Implies s1 s2) = not <$> ((&&) <$> aux s1 <*> (not <$> aux s2)) - aux (Iff s1 s2) = (==) <$> aux s1 <*> aux s2 - -data Bucket - = Tautology - | Contradiction - | Contingent - deriving (Eq, Show) - -bucket :: Statement -> Bucket -bucket s - | and values = Tautology - | all not values = Contradiction - | otherwise = Contingent - where - atomsList = S.toList $ atoms s - values = [fromJust $ eval assignments s | assignments <- enumerate $ atomsList] - -enumerate :: [a] -> [[(a, Bool)]] -enumerate keys = aux start - where - aux assignments = (assignments:) $ - case next assignments of - Nothing -> [] - Just (assignments') -> aux assignments' - - start = [(key, False) | key <- keys] - - next [] = Nothing - next ((k, False):rest) = Just $ (k, True):rest - next ((k, True):rest) = ((k, False):) <$> (next rest) - -{- - ghci> bucket $ fromJust $ fst <$> runParser stmt "(p<->p)" -Tautology -ghci> bucket p -Contingent -ghci> bucket q -Contingent -ghci> bucket $ fromJust $ fst <$> runParser stmt "(p<->!p)" -Contradiction -ghci> bucket $ fromJust $ fst <$> runParser stmt "(p|!p)" -Tautology -ghci> bucket $ fromJust $ fst <$> runParser stmt "(p->p)" -Tautology -ghci> bucket $ fromJust $ fst <$> runParser stmt "(p&!p)" -Contradiction -ghci> bucket $ fromJust $ fst <$> runParser stmt "(!(p->q)&!p)" -Contradiction -ghci> bucket $ fromJust $ fst <$> runParser stmt "(p|(p->q))" -Tautology -ghci> bucket $ fromJust $ fst <$> runParser stmt "((p->q)->(!p->r))" -Contingent -ghci> bucket $ fromJust $ fst <$> runParser stmt "(!(a&b)<->(!a|!b))" -Tautology -ghci> bucket $ fromJust $ fst <$> runParser stmt "(!(a|b)<->(!a&!b))" -Tautology --} - -data SerializeFormat - = Ascii - | Latex - deriving (Show, Eq) - -serializeParts :: SerializeFormat -> Statement -> [String] -serializeParts = aux - where - aux Ascii = ascii - aux Latex = latex - - ascii (Atom key) = [key] - ascii (Not s) = ["!"] ++ ascii s - ascii (And s1 s2) = connective "&" (ascii s1) (ascii s2) - ascii (Or s1 s2) = connective "|" (ascii s1) (ascii s2) - ascii (Implies s1 s2) = connective "->" (ascii s1) (ascii s2) - ascii (Iff s1 s2) = connective "<->" (ascii s1) (ascii s2) - - latex (Atom key) = [key] - latex (Not s) = ["\\neg "] ++ latex s - latex (And s1 s2) = connective "\\cap " (latex s1) (latex s2) - latex (Or s1 s2) = connective "\\cup " (latex s1) (latex s2) - latex (Implies s1 s2) = connective "\\to " (latex s1) (latex s2) - latex (Iff s1 s2) = connective "\\leftrightarrow " (latex s1) (latex s2) - - connective token s1 s2 = ["("] ++ s1 ++ [token] ++ s2 ++ [")"] - -serialize :: SerializeFormat -> Statement -> String -serialize fmt s = concat $ serializeParts fmt s - -serializeLatexTruthTableRow :: [(String, Bool)] -> Statement -> Maybe String -serializeLatexTruthTableRow = latexRow - where - latexRow ass (Atom key) = toInt <$> eval ass (Atom key) - latexRow ass (Not s) = (toInt <$> not <$> eval ass s) <> latexRow ass s - latexRow ass (And s1 s2) = latexRowBinaryConnective (&&) ass s1 s2 - latexRow ass (Or s1 s2) = latexRowBinaryConnective (||) ass s1 s2 - latexRow ass (Implies s1 s2) = latexRowBinaryConnective implies ass s1 s2 - latexRow ass (Iff s1 s2) = latexRowBinaryConnective (==) ass s1 s2 - - latexRowBinaryConnective op ass s1 s2 = - (\subrow1 subrow2 subeval1 subeval2 -> " " <> subrow1 <> (toInt $ op subeval1 subeval2) <> subrow2 <> " ") <$> - latexRow ass s1 <*> latexRow ass s2 <*> - eval ass s1 <*> eval ass s2 - - toInt :: Bool -> String - toInt False = "0" - toInt True = "1" - - implies :: Bool -> Bool -> Bool - implies b1 b2 = not b1 || b2 - -truthtable :: Statement -> String -truthtable s = open <> header <> "\\hline\n" <> body <> close - where - open = - "\\begin{tabular}{" <> - replicate (length atomsList) 'c' <> - "|" <> - replicate (length serial) 'c' <> - "}\n" - - close = "\\end{tabular}\n\n" - - serial = serialize Latex s - - atomsList :: [String] - atomsList = S.toAscList $ atoms s - - header :: String - header = - intercalate " & " (map dollars atomsList) <> - " & " <> - intercalate " & " (map dollars $ serializeParts Latex s) <> - " \\\\\n" - - dollars :: String -> String - dollars string = "$" <> string <> "$" - - body :: String - body = concat $ map line $ enumerate atomsList - - line assignments = - intercalate " & " (bools assignments) <> - " & " <> - intercalate " & " (parts assignments) <> - " \\\\\n" - - bools assignments = [if bool then "1" else "0" | (key, bool) <- assignments] - - parts assignments = - (\xs -> [" " <> [x] <> " " | x <- xs]) $ - fromJust $ serializeLatexTruthTableRow assignments s + fail err@(ParseError pos message) = + putStrLn $ + "parse error at position " + <> show pos + <> ": " + <> message diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..47f8988 --- /dev/null +++ b/Makefile @@ -0,0 +1,7 @@ +main: dirty clean + +dirty: + ghc Main.hs -o logic + +clean: + find | grep -E '\.(hi|o)' | xargs rm -- diff --git a/readme.md b/readme.md new file mode 100644 index 0000000..d841c09 --- /dev/null +++ b/readme.md @@ -0,0 +1,28 @@ +Statement logic !!! + +# Compile it + +```sh +make +``` + +# Usage + +```sh +echo '((p->q)<->(!q->!p))' | ./logic +``` + +## Output + +``` +Iff (Implies (Atom "p") (Atom "q")) (Implies (Not (Atom "q")) (Not (Atom "p"))) +Tautology +\begin{tabular}{cc||cccccc|c|cccccccc} +$p$ & $q$ & $($ & $($ & $p$ & $\to $ & $q$ & $)$ & $\leftrightarrow $ & $($ & $\neg $ & $q$ & $\to $ & $\neg $ & $p$ & $)$ & $)$ \\ +\hline +0 & 0 & & & 0 & 1 & 0 & & \textbf 1 & & 1 & 0 & 1 & 1 & 0 & & \\ +0 & 1 & & & 1 & 0 & 0 & & \textbf 1 & & 1 & 0 & 0 & 0 & 1 & & \\ +1 & 0 & & & 0 & 1 & 1 & & \textbf 1 & & 0 & 1 & 1 & 1 & 0 & & \\ +1 & 1 & & & 1 & 1 & 1 & & \textbf 1 & & 0 & 1 & 1 & 0 & 1 & & \\ +\end{tabular} +```