Browse files

Simplified Bit. Since we no longer use data-reify, we do not need Cir…

…cuit.
  • Loading branch information...
1 parent 221b20b commit 152078fc2cb176c3f4ea1b47054e7e834cfc1c68 @ekmett committed Mar 19, 2013
Showing with 51 additions and 102 deletions.
  1. +0 −1 ersatz.cabal
  2. +51 −45 src/Ersatz/Bit.hs
  3. +0 −56 src/Ersatz/Internal/Circuit.hs
View
1 ersatz.cabal
@@ -191,7 +191,6 @@ library
Ersatz.Decoding
Ersatz.Equatable
Ersatz.Encoding
- Ersatz.Internal.Circuit
Ersatz.Internal.Formula
Ersatz.Internal.Literal
Ersatz.Problem
View
96 src/Ersatz/Bit.hs
@@ -7,7 +7,6 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE UndecidableInstances #-}
-
{-# OPTIONS_HADDOCK not-home #-}
--------------------------------------------------------------------
-- |
@@ -31,12 +30,11 @@ import Control.Applicative
import Control.Monad.State
import Data.Foldable (Foldable, toList)
import qualified Data.Foldable as Foldable
-import Data.Sequence ((<|), (|>), (><))
+import Data.Sequence (Seq, (<|), (|>), (><))
import qualified Data.Sequence as Seq
import Data.Typeable
import Ersatz.Decoding
import Ersatz.Encoding
-import Ersatz.Internal.Circuit
import Ersatz.Internal.Formula
import Ersatz.Internal.Literal
import Ersatz.Internal.StableName
@@ -54,68 +52,76 @@ infixr 0 ==>
-- | A 'Bit' provides a reference to a possibly indeterminate boolean
-- value that can be determined by an external SAT solver.
-newtype Bit = Bit (Circuit Bit)
+data Bit
+ = And (Seq Bit)
+ | Or (Seq Bit)
+ | Xor Bit Bit
+ | Mux Bit Bit Bit
+ | Not Bit
+ | Var !Literal
deriving (Show, Typeable)
instance Boolean Bit where
-- improve the stablemap this way
bool True = true
bool False = false
- true = Bit (Var literalTrue)
- false = Bit (Var literalFalse)
-
- a@(Bit (Var (Literal (-1)))) && _ = a
- _ && b@(Bit (Var (Literal (-1)))) = b
- a && Bit (Var (Literal 1)) = a
- Bit (Var (Literal 1)) && b = b
- Bit (And as) && Bit (And bs) = Bit (And (as >< bs))
- Bit (And as) && b = Bit (And (as |> b))
- a && Bit (And bs) = Bit (And (a <| bs))
- a && b = Bit (And (a <| b <| Seq.empty))
-
- a || Bit (Var (Literal (-1))) = a
- Bit (Var (Literal (-1))) || b = b
- a@(Bit (Var (Literal 1))) || _ = a
- _ || b@(Bit (Var (Literal 1))) = b
- Bit (Or as) || Bit (Or bs) = Bit (Or (as >< bs))
- Bit (Or as) || b = Bit (Or (as |> b))
- a || Bit (Or bs) = Bit (Or (a <| bs))
- a || b = Bit (Or (a <| b <| Seq.empty))
-
- not (Bit (Not c)) = c
- not (Bit (Var l)) = Bit (Var (negateLiteral l))
- not c = Bit (Not c)
-
- a `xor` Bit (Var (Literal (-1))) = a
- Bit (Var (Literal (-1))) `xor` b = b
- a `xor` Bit (Var (Literal 1)) = not a
- Bit (Var (Literal 1)) `xor` b = not b
- a `xor` b = Bit (Xor a b)
+ true = Var literalTrue
+ false = Var literalFalse
+
+ a@(Var (Literal (-1))) && _ = a
+ _ && b@(Var (Literal (-1))) = b
+ a && Var (Literal 1) = a
+ Var (Literal 1) && b = b
+ And as && And bs = And (as >< bs)
+ And as && b = And (as |> b)
+ a && And bs = And (a <| bs)
+ a && b = And (a <| b <| Seq.empty)
+
+ a || Var (Literal (-1)) = a
+ Var (Literal (-1)) || b = b
+
+ a@(Var (Literal 1)) || _ = a
+ _ || b@(Var (Literal 1)) = b
+
+ Or as || Or bs = Or (as >< bs)
+ Or as || b = Or (as |> b)
+ a || Or bs = Or (a <| bs)
+ a || b = Or (a <| b <| Seq.empty)
+
+ not (Not c) = c
+ not (Var l) = Var (negateLiteral l)
+ not c = Not c
+
+ a `xor` Var (Literal (-1)) = a
+ Var (Literal (-1)) `xor` b = b
+ a `xor` Var (Literal 1) = not a
+ Var (Literal 1) `xor` b = not b
+ a `xor` b = Xor a b
and = Foldable.foldl' (&&) true
or = Foldable.foldl' (||) false
all p = Foldable.foldl' (\res b -> res && p b) true
any p = Foldable.foldl' (\res b -> res || p b) false
- choose f _ (Bit (Var (Literal (-1)))) = f
- choose _ t (Bit (Var (Literal 1))) = t
- choose f t s = Bit (Mux f t s)
+ choose f _ (Var (Literal (-1))) = f
+ choose _ t (Var (Literal 1)) = t
+ choose f t s = Mux f t s
instance Variable Bit where
- exists = liftM (Bit . Var) exists
+ exists = liftM Var exists
#ifndef HLINT
- forall = liftM (Bit . Var) forall
+ forall = liftM Var forall
#endif
-- a Bit you don't assert is actually a boolean function that you can evaluate later after compilation
instance Decoding Bit where
type Decoded Bit = Bool
- decode sol b@(Bit c)
+ decode sol b
= solutionStableName sol (unsafePerformIO (makeStableName' b))
-- The StableName didn’t have an associated literal with a solution,
-- recurse to compute the value.
- <|> case c of
+ <|> case b of
And cs -> andMaybeBools . toList $ decode sol <$> cs
Or cs -> orMaybeBools . toList $ decode sol <$> cs
Xor x y -> xor <$> decode sol x <*> decode sol y
@@ -160,10 +166,10 @@ assert b = do
-- | Convert a 'Bit' to a 'Literal'.
runBit :: (MonadState s m, HasSAT s) => Bit -> m Literal
-runBit (Bit (Not c)) = negateLiteral `liftM` runBit c
-runBit (Bit (Var l)) = return l
-runBit b@(Bit c) = generateLiteral b $ \out ->
- assertFormula =<< case c of
+runBit (Not c) = negateLiteral `liftM` runBit c
+runBit (Var l) = return l
+runBit b = generateLiteral b $ \out ->
+ assertFormula =<< case b of
And bs -> formulaAnd out `liftM` mapM runBit (toList bs)
Or bs -> formulaOr out `liftM` mapM runBit (toList bs)
Xor x y -> liftM2 (formulaXor out) (runBit x) (runBit y)
View
56 src/Ersatz/Internal/Circuit.hs
@@ -1,56 +0,0 @@
-{-# LANGUAGE DeriveDataTypeable #-}
---------------------------------------------------------------------
--- |
--- Copyright : © Edward Kmett 2010-2013, Johan Kiviniemi 2013
--- License : BSD3
--- Maintainer: Edward Kmett <ekmett@gmail.com>
--- Stability : experimental
--- Portability: non-portable
---
---------------------------------------------------------------------
-module Ersatz.Internal.Circuit
- ( Circuit(..)
- ) where
-
-import Control.Applicative
-import Data.Foldable (Foldable, foldMap)
-import Data.Monoid
-import Data.Sequence (Seq)
-import Data.Traversable (Traversable, traverse)
-import Data.Typeable
-import Ersatz.Internal.Literal
-
--- | This is used to observe the directed graph with sharing of how multiple
--- 'Ersatz.Bit.Bit' values are related.
-data Circuit c
- = And (Seq c)
- | Or (Seq c)
- | Xor c c
- | Mux c c c -- ^ False branch, true branch, predicate/selector branch
- | Not c
- | Var !Literal
- deriving (Show, Typeable)
-
-instance Functor Circuit where
- fmap f (And as) = And (fmap f as)
- fmap f (Or as) = Or (fmap f as)
- fmap f (Xor a b) = Xor (f a) (f b)
- fmap f (Mux a b c) = Mux (f a) (f b) (f c)
- fmap f (Not a) = Not (f a)
- fmap _ (Var l) = Var l
-
-instance Foldable Circuit where
- foldMap f (And as) = foldMap f as
- foldMap f (Or as) = foldMap f as
- foldMap f (Xor a b) = f a <> f b
- foldMap f (Mux a b c) = f a <> f b <> f c
- foldMap f (Not a) = f a
- foldMap _ Var{} = mempty
-
-instance Traversable Circuit where
- traverse f (And as) = And <$> traverse f as
- traverse f (Or as) = Or <$> traverse f as
- traverse f (Xor a b) = Xor <$> f a <*> f b
- traverse f (Mux a b c) = Mux <$> f a <*> f b <*> f c
- traverse f (Not a) = Not <$> f a
- traverse _ (Var l) = pure (Var l)

0 comments on commit 152078f

Please sign in to comment.