-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | A monad for expressing SAT or QSAT problems using observable sharing.
--   
--   A monad for expressing SAT or QSAT problems using observable sharing.
--   
--   For example, we can express a full-adder with:
--   
--   <pre>
--   full_adder :: Bit -&gt; Bit -&gt; Bit -&gt; (Bit, Bit)
--   full_adder a b cin = (s2, c1 || c2)
--     where (s1,c1) = half_adder a b
--           (s2,c2) = half_adder s1 cin
--   </pre>
--   
--   <pre>
--   half_adder :: Bit -&gt; Bit -&gt; (Bit, Bit)
--   half_adder a b = (a `xor` b, a &amp;&amp; b)
--   </pre>
--   
--   <i>Longer Examples</i>
--   
--   Included are a couple of examples included with the distribution.
--   Neither are as fast as a dedicated solver for their respective
--   domains, but they showcase how you can solve real world problems
--   involving 10s or 100s of thousands of variables and constraints with
--   <a>ersatz</a>.
--   
--   <pre>
--   ersatz-sudoku
--   </pre>
--   
--   <pre>
--   % time ersatz-sudoku
--   Problem:
--   ┌───────┬───────┬───────┐
--   │ 5 3   │   7   │       │
--   │ 6     │ 1 9 5 │       │
--   │   9 8 │       │   6   │
--   ├───────┼───────┼───────┤
--   │ 8     │   6   │     3 │
--   │ 4     │ 8   3 │     1 │
--   │ 7     │   2   │     6 │
--   ├───────┼───────┼───────┤
--   │   6   │       │ 2 8   │
--   │       │ 4 1 9 │     5 │
--   │       │   8   │   7 9 │
--   └───────┴───────┴───────┘
--   Solution:
--   ┌───────┬───────┬───────┐
--   │ 5 3 4 │ 6 7 8 │ 9 1 2 │
--   │ 6 7 2 │ 1 9 5 │ 3 4 8 │
--   │ 1 9 8 │ 3 4 2 │ 5 6 7 │
--   ├───────┼───────┼───────┤
--   │ 8 5 9 │ 7 6 1 │ 4 2 3 │
--   │ 4 2 6 │ 8 5 3 │ 7 9 1 │
--   │ 7 1 3 │ 9 2 4 │ 8 5 6 │
--   ├───────┼───────┼───────┤
--   │ 9 6 1 │ 5 3 7 │ 2 8 4 │
--   │ 2 8 7 │ 4 1 9 │ 6 3 5 │
--   │ 3 4 5 │ 2 8 6 │ 1 7 9 │
--   └───────┴───────┴───────┘
--   ersatz-sudoku  1,13s user 0,04s system 99% cpu 1,179 total
--   </pre>
--   
--   <pre>
--   ersatz-regexp-grid
--   </pre>
--   
--   This solves the "regular crossword puzzle" (<a>grid.pdf</a>) from the
--   2013 MIT mystery hunt.
--   
--   <pre>
--   % time ersatz-regexp-grid
--   </pre>
--   
--   <a>SPOILER</a>
--   
--   <pre>
--   ersatz-regexp-grid  2,45s user 0,05s system 99% cpu 2,502 total
--   </pre>
@package ersatz
@version 0.4.4


module Ersatz.Internal.Literal

-- | A naked possibly-negated Atom, present in the target <a>Solver</a>.
--   
--   The literals <tt>-1</tt> and <tt>1</tt> are dedicated for the constant
--   <a>False</a> and the constant <a>True</a> respectively.
newtype Literal
Literal :: Int -> Literal
[literalId] :: Literal -> Int
negateLiteral :: Literal -> Literal

-- | The <a>False</a> constant. The literal <tt>-1</tt> is dedicated for
--   it.
literalFalse :: Literal

-- | The <a>True</a> constant. The literal <tt>1</tt> is dedicated for it.
literalTrue :: Literal
instance GHC.Classes.Ord Ersatz.Internal.Literal.Literal
instance GHC.Classes.Eq Ersatz.Internal.Literal.Literal
instance GHC.Show.Show Ersatz.Internal.Literal.Literal


module Ersatz.Internal.Formula

-- | A disjunction of possibly negated atoms. Negated atoms are represented
--   by negating the identifier.
newtype Clause
Clause :: IntSet -> Clause
[clauseSet] :: Clause -> IntSet

-- | Extract the (possibly negated) atoms referenced by a <a>Clause</a>.
clauseLiterals :: Clause -> [Literal]
fromLiteral :: Literal -> Clause

-- | A conjunction of clauses
newtype Formula
Formula :: Seq Clause -> Formula
[formulaSet] :: Formula -> Seq Clause

-- | A formula with no clauses
formulaEmpty :: Formula

-- | Assert a literal
formulaLiteral :: Literal -> Formula
fromClause :: Clause -> Formula

-- | The boolean <i>not</i> operation
--   
--   Derivation of the Tseitin transformation:
--   
--   <pre>
--   O ≡ ¬A
--   (O → ¬A) &amp; (¬O → A)
--   (¬O | ¬A) &amp; (O | A)
--   </pre>
formulaNot :: Literal -> Literal -> Formula

-- | The boolean <i>and</i> operation
--   
--   Derivation of the Tseitin transformation:
--   
--   <pre>
--   O ≡ (A &amp; B &amp; C)
--   (O → (A &amp; B &amp; C)) &amp; (¬O → ¬(A &amp; B &amp; C))
--   (¬O | (A &amp; B &amp; C)) &amp; (O | ¬(A &amp; B &amp; C))
--   (¬O | A) &amp; (¬O | B) &amp; (¬O | C) &amp; (O | ¬A | ¬B | ¬C)
--   </pre>
formulaAnd :: Literal -> [Literal] -> Formula

-- | The boolean <i>or</i> operation
--   
--   Derivation of the Tseitin transformation:
--   
--   <pre>
--   O ≡ (A | B | C)
--   (O → (A | B | C)) &amp; (¬O → ¬(A | B | C))
--   (¬O | (A | B | C)) &amp; (O | ¬(A | B | C))
--   (¬O | A | B | C) &amp; (O | (¬A &amp; ¬B &amp; ¬C))
--   (¬O | A | B | C) &amp; (O | ¬A) &amp; (O | ¬B) &amp; (O | ¬C)
--   </pre>
formulaOr :: Literal -> [Literal] -> Formula

-- | The boolean <i>xor</i> operation
--   
--   Derivation of the Tseitin transformation:
--   
--   <pre>
--   O ≡ A ⊕ B
--   O ≡ ((¬A &amp; B) | (A &amp; ¬B))
--   (O → ((¬A &amp; B) | (A &amp; ¬B))) &amp; (¬O → ¬((¬A &amp; B) | (A &amp; ¬B)))
--   </pre>
--   
--   Left hand side:
--   
--   <pre>
--   O → ((¬A &amp; B) | (A &amp; ¬B))
--   ¬O | ((¬A &amp; B) | (A &amp; ¬B))
--   ¬O | ((¬A | A) &amp; (¬A | ¬B) &amp; (A | B) &amp; (¬B | B))
--   ¬O | ((¬A | ¬B) &amp; (A | B))
--   (¬O | ¬A | ¬B) &amp; (¬O | A | B)
--   </pre>
--   
--   Right hand side:
--   
--   <pre>
--   ¬O → ¬((¬A &amp; B) | (A &amp; ¬B))
--   O | ¬((¬A &amp; B) | (A &amp; ¬B))
--   O | (¬(¬A &amp; B) &amp; ¬(A &amp; ¬B))
--   O | ((A | ¬B) &amp; (¬A | B))
--   (O | ¬A | B) &amp; (O | A | ¬B)
--   </pre>
--   
--   Result:
--   
--   <pre>
--   (¬O | ¬A | ¬B) &amp; (¬O | A | B) &amp; (O | ¬A | B) &amp; (O | A | ¬B)
--   </pre>
formulaXor :: Literal -> Literal -> Literal -> Formula

-- | with redundant clauses, cf. discussion in Een and Sorensen,
--   Translating Pseudo Boolean Constraints ..., p. 7
--   <a>http://minisat.se/Papers.html</a>
--   
--   The boolean <i>else-then-if</i> or <i>mux</i> operation
--   
--   Derivation of the Tseitin transformation:
--   
--   <pre>
--   O ≡ (F &amp; ¬P) | (T &amp; P)
--   (O → ((F &amp; ¬P) | (T &amp; P))) &amp; (¬O → ¬((F &amp; ¬P) | (T &amp; P)))
--   </pre>
--   
--   Left hand side:
--   
--   <pre>
--   O → ((F &amp; ¬P) | (T &amp; P))
--   ¬O | ((F &amp; ¬P) | (T &amp; P))
--   ¬O | ((F | T) &amp; (F | P) &amp; (T | ¬P) &amp; (¬P | P))
--   ¬O | ((F | T) &amp; (F | P) &amp; (T | ¬P))
--   (¬O | F | T) &amp; (¬O | F | P) &amp; (¬O | T | ¬P)
--   </pre>
--   
--   Right hand side:
--   
--   <pre>
--   ¬O → ¬((F &amp; ¬P) | (T &amp; P))
--   O | ¬((F &amp; ¬P) | (T &amp; P))
--   O | (¬(F &amp; ¬P) &amp; ¬(T &amp; P))
--   O | ((¬F | P) &amp; (¬T | ¬P))
--   (O | ¬F | P) &amp; (O | ¬T | ¬P)
--   </pre>
--   
--   Result:
--   
--   <pre>
--   (¬O | F | T) &amp; (¬O | F | P) &amp; (¬O | T | ¬P) &amp; (O | ¬F | P) &amp; (O | ¬T | ¬P)
--   </pre>
formulaMux :: Literal -> Literal -> Literal -> Literal -> Formula
formulaFAS :: Literal -> Literal -> Literal -> Literal -> Formula
formulaFAC :: Literal -> Literal -> Literal -> Literal -> Formula
instance GHC.Classes.Ord Ersatz.Internal.Formula.Formula
instance GHC.Classes.Eq Ersatz.Internal.Formula.Formula
instance GHC.Classes.Ord Ersatz.Internal.Formula.Clause
instance GHC.Classes.Eq Ersatz.Internal.Formula.Clause
instance GHC.Base.Semigroup Ersatz.Internal.Formula.Formula
instance GHC.Base.Monoid Ersatz.Internal.Formula.Formula
instance GHC.Show.Show Ersatz.Internal.Formula.Formula
instance GHC.Base.Semigroup Ersatz.Internal.Formula.Clause
instance GHC.Base.Monoid Ersatz.Internal.Formula.Clause
instance GHC.Show.Show Ersatz.Internal.Formula.Clause


module Ersatz.Problem
data SAT
SAT :: {-# UNPACK #-} !Int -> !Formula -> !(HashMap (StableName ()) Literal) -> SAT
class HasSAT s
sat :: HasSAT s => Lens' s SAT
lastAtom :: HasSAT s => Lens' s Int
formula :: HasSAT s => Lens' s Formula
stableMap :: HasSAT s => Lens' s (HashMap (StableName ()) Literal)

-- | Run a <a>SAT</a>-generating state computation. Useful e.g. in ghci for
--   disambiguating the type of a <a>MonadState</a>, <a>HasSAT</a> value.
runSAT :: StateT SAT m a -> m (a, SAT)

-- | Run a <a>SAT</a>-generating state computation in the <a>Identity</a>
--   monad. Useful e.g. in ghci for disambiguating the type of a
--   <a>MonadState</a>, <a>HasSAT</a> value.
runSAT' :: StateT SAT Identity a -> (a, SAT)

-- | Run a <a>SAT</a>-generating state computation and return the
--   respective <a>DIMACS</a> output. Useful for testing and debugging.
dimacsSAT :: StateT SAT Identity a -> ByteString
literalExists :: (MonadState s m, HasSAT s) => m Literal
assertFormula :: (MonadState s m, HasSAT s) => Formula -> m ()
generateLiteral :: (MonadState s m, HasSAT s) => a -> (Literal -> m ()) -> m Literal

-- | A (quantified) boolean formula.
data QSAT
QSAT :: !IntSet -> SAT -> QSAT
class HasSAT t => HasQSAT t
qsat :: HasQSAT t => Lens' t QSAT
universals :: HasQSAT t => Lens' t IntSet

-- | Run a <a>QSAT</a>-generating state computation. Useful e.g. in ghci
--   for disambiguating the type of a <a>MonadState</a>, <a>HasQSAT</a>
--   value.
runQSAT :: StateT QSAT m a -> m (a, QSAT)

-- | Run a <a>QSAT</a>-generating state computation in the <a>Identity</a>
--   monad. Useful e.g. in ghci for disambiguating the type of a
--   <a>MonadState</a>, <a>HasQSAT</a> value.
runQSAT' :: StateT QSAT Identity a -> (a, QSAT)

-- | Run a <a>QSAT</a>-generating state computation and return the
--   respective <a>QDIMACS</a> output. Useful for testing and debugging.
qdimacsQSAT :: StateT QSAT Identity a -> ByteString
literalForall :: (MonadState s m, HasQSAT s) => m Literal

-- | DIMACS file format pretty printer
--   
--   This is used to generate the problem statement for a given <a>SAT</a>
--   <a>Solver</a>.
class DIMACS t
dimacsComments :: DIMACS t => t -> [ByteString]
dimacsNumVariables :: DIMACS t => t -> Int
dimacsClauses :: DIMACS t => t -> Seq IntSet

-- | QDIMACS file format pretty printer
--   
--   This is used to generate the problem statement for a given <a>QSAT</a>
--   <a>Solver</a>.
class QDIMACS t
qdimacsComments :: QDIMACS t => t -> [ByteString]
qdimacsNumVariables :: QDIMACS t => t -> Int
qdimacsQuantified :: QDIMACS t => t -> [Quant]
qdimacsClauses :: QDIMACS t => t -> Seq IntSet

-- | WDIMACS file format pretty printer
--   
--   This is used to generate the problem statement for a given
--   <tt>MaxSAT</tt> <a>Solver</a> (TODO).
class WDIMACS t
wdimacsComments :: WDIMACS t => t -> [ByteString]
wdimacsNumVariables :: WDIMACS t => t -> Int
wdimacsTopWeight :: WDIMACS t => t -> Int64
wdimacsClauses :: WDIMACS t => t -> Seq (Int64, IntSet)

-- | Generate a <a>Builder</a> out of a <a>DIMACS</a> problem.
dimacs :: DIMACS t => t -> Builder

-- | Generate a <a>Builder</a> out of a <a>QDIMACS</a> problem.
qdimacs :: QDIMACS t => t -> Builder

-- | Generate a <a>Builder</a> out of a <a>WDIMACS</a> problem.
wdimacs :: WDIMACS t => t -> Builder
instance GHC.Show.Show Ersatz.Problem.QSAT
instance Ersatz.Problem.QDIMACS Ersatz.Problem.QSAT
instance Ersatz.Problem.DIMACS Ersatz.Problem.SAT
instance Ersatz.Problem.HasQSAT Ersatz.Problem.QSAT
instance Ersatz.Problem.HasSAT Ersatz.Problem.QSAT
instance Data.Default.Class.Default Ersatz.Problem.QSAT
instance Ersatz.Problem.HasSAT Ersatz.Problem.SAT
instance GHC.Show.Show Ersatz.Problem.SAT
instance Data.Default.Class.Default Ersatz.Problem.SAT


module Ersatz.Solution
data Solution
Solution :: Literal -> Maybe Bool -> StableName () -> Maybe Bool -> Solution
[solutionLiteral] :: Solution -> Literal -> Maybe Bool
[solutionStableName] :: Solution -> StableName () -> Maybe Bool
solutionFrom :: HasSAT s => IntMap Bool -> s -> Solution
data Result
Unsolved :: Result
Unsatisfied :: Result
Satisfied :: Result

-- | A <tt><a>Solver</a> s m</tt> is responsible for invoking a solver and
--   returning a <a>Result</a> and a map of determined results.
--   
--   <ul>
--   <li><tt>s</tt> is typically <a>SAT</a> or <a>QSAT</a></li>
--   <li><tt>m</tt> is typically <a>IO</a></li>
--   </ul>
type Solver s m = s -> m (Result, IntMap Bool)
instance GHC.Read.Read Ersatz.Solution.Result
instance GHC.Show.Show Ersatz.Solution.Result
instance GHC.Arr.Ix Ersatz.Solution.Result
instance GHC.Classes.Ord Ersatz.Solution.Result
instance GHC.Classes.Eq Ersatz.Solution.Result
instance GHC.Enum.Enum Ersatz.Solution.Result
instance GHC.Enum.Bounded Ersatz.Solution.Result


module Ersatz.Codec

-- | This class describes data types that can be marshaled to or from a SAT
--   solver.
class Codec a where {
    type family Decoded a :: *;
}

-- | Return a value based on the solution if one can be determined.
decode :: (Codec a, MonadPlus f) => Solution -> a -> f (Decoded a)
encode :: Codec a => Decoded a -> a
instance Ersatz.Codec.Codec Ersatz.Internal.Literal.Literal
instance Ersatz.Codec.Codec ()
instance (Ersatz.Codec.Codec a, Ersatz.Codec.Codec b) => Ersatz.Codec.Codec (a, b)
instance (Ersatz.Codec.Codec a, Ersatz.Codec.Codec b, Ersatz.Codec.Codec c) => Ersatz.Codec.Codec (a, b, c)
instance (Ersatz.Codec.Codec a, Ersatz.Codec.Codec b, Ersatz.Codec.Codec c, Ersatz.Codec.Codec d) => Ersatz.Codec.Codec (a, b, c, d)
instance (Ersatz.Codec.Codec a, Ersatz.Codec.Codec b, Ersatz.Codec.Codec c, Ersatz.Codec.Codec d, Ersatz.Codec.Codec e) => Ersatz.Codec.Codec (a, b, c, d, e)
instance (Ersatz.Codec.Codec a, Ersatz.Codec.Codec b, Ersatz.Codec.Codec c, Ersatz.Codec.Codec d, Ersatz.Codec.Codec e, Ersatz.Codec.Codec f) => Ersatz.Codec.Codec (a, b, c, d, e, f)
instance (Ersatz.Codec.Codec a, Ersatz.Codec.Codec b, Ersatz.Codec.Codec c, Ersatz.Codec.Codec d, Ersatz.Codec.Codec e, Ersatz.Codec.Codec f, Ersatz.Codec.Codec g) => Ersatz.Codec.Codec (a, b, c, d, e, f, g)
instance (Ersatz.Codec.Codec a, Ersatz.Codec.Codec b, Ersatz.Codec.Codec c, Ersatz.Codec.Codec d, Ersatz.Codec.Codec e, Ersatz.Codec.Codec f, Ersatz.Codec.Codec g, Ersatz.Codec.Codec h) => Ersatz.Codec.Codec (a, b, c, d, e, f, g, h)
instance Ersatz.Codec.Codec a => Ersatz.Codec.Codec [a]
instance (GHC.Arr.Ix i, Ersatz.Codec.Codec e) => Ersatz.Codec.Codec (GHC.Arr.Array i e)
instance (Ersatz.Codec.Codec a, Ersatz.Codec.Codec b) => Ersatz.Codec.Codec (Data.Either.Either a b)
instance Ersatz.Codec.Codec a => Ersatz.Codec.Codec (Data.HashMap.Base.HashMap k a)
instance Ersatz.Codec.Codec a => Ersatz.Codec.Codec (Data.IntMap.Internal.IntMap a)
instance Ersatz.Codec.Codec a => Ersatz.Codec.Codec (Data.Map.Internal.Map k a)
instance Ersatz.Codec.Codec a => Ersatz.Codec.Codec (GHC.Base.Maybe a)
instance Ersatz.Codec.Codec a => Ersatz.Codec.Codec (Data.Sequence.Internal.Seq a)
instance Ersatz.Codec.Codec a => Ersatz.Codec.Codec (Data.Tree.Tree a)


-- | <a>DepQBF</a> is a solver capable of solving quantified boolean
--   formulae (<tt>QBF</tt>).
module Ersatz.Solver.DepQBF

-- | This is a <a>Solver</a> for <a>QSAT</a> problems that runs the
--   <tt>depqbf</tt> solver using the current <tt>PATH</tt>, it tries to
--   run an executable named <tt>depqbf</tt>.
depqbf :: MonadIO m => Solver QSAT m

-- | This is a <a>Solver</a> for <a>QSAT</a> problems that lets you specify
--   the path to the <tt>depqbf</tt> executable.
depqbfPath :: MonadIO m => FilePath -> Solver QSAT m


module Ersatz.Solver.Minisat

-- | <a>Solver</a> for <a>SAT</a> problems that tries to invoke the
--   <tt>minisat</tt> executable from the <tt>PATH</tt>
minisat :: MonadIO m => Solver SAT m

-- | <a>Solver</a> for <a>SAT</a> problems that tries to invoke the
--   <tt>cryptominisat</tt> executable from the <tt>PATH</tt>
cryptominisat :: MonadIO m => Solver SAT m

-- | <a>Solver</a> for <a>SAT</a> problems that tries to invoke a program
--   that takes <tt>minisat</tt> compatible arguments.
--   
--   The <a>FilePath</a> refers to the path to the executable.
minisatPath :: MonadIO m => FilePath -> Solver SAT m


module Ersatz.Solver
solveWith :: (Monad m, MonadPlus n, HasSAT s, Default s, Codec a) => Solver s m -> StateT s m a -> m (Result, n (Decoded a))


module Ersatz.Variable

-- | Instances for this class for product-like types can be automatically
--   derived for any type that is an instance of <a>Generic</a>.
class Variable t
literally :: (Variable t, HasSAT s, MonadState s m) => m Literal -> m t
literally :: (Variable t, HasSAT s, MonadState s m, Generic t, GVariable (Rep t)) => m Literal -> m t
forall :: (Variable a, MonadState s m, HasQSAT s) => m a
exists :: (Variable a, MonadState s m, HasSAT s) => m a
class GVariable f
gliterally :: (GVariable f, MonadState s m, HasSAT s) => m Literal -> m (f a)
genericLiterally :: (HasSAT s, MonadState s m, Generic t, GVariable (Rep t)) => m Literal -> m t
instance Ersatz.Variable.Variable a => Ersatz.Variable.GVariable (GHC.Generics.K1 i a)
instance Ersatz.Variable.Variable Ersatz.Internal.Literal.Literal
instance (Ersatz.Variable.Variable a, Ersatz.Variable.Variable b) => Ersatz.Variable.Variable (a, b)
instance (Ersatz.Variable.Variable a, Ersatz.Variable.Variable b, Ersatz.Variable.Variable c) => Ersatz.Variable.Variable (a, b, c)
instance (Ersatz.Variable.Variable a, Ersatz.Variable.Variable b, Ersatz.Variable.Variable c, Ersatz.Variable.Variable d) => Ersatz.Variable.Variable (a, b, c, d)
instance (Ersatz.Variable.Variable a, Ersatz.Variable.Variable b, Ersatz.Variable.Variable c, Ersatz.Variable.Variable d, Ersatz.Variable.Variable e) => Ersatz.Variable.Variable (a, b, c, d, e)
instance (Ersatz.Variable.Variable a, Ersatz.Variable.Variable b, Ersatz.Variable.Variable c, Ersatz.Variable.Variable d, Ersatz.Variable.Variable e, Ersatz.Variable.Variable f) => Ersatz.Variable.Variable (a, b, c, d, e, f)
instance (Ersatz.Variable.Variable a, Ersatz.Variable.Variable b, Ersatz.Variable.Variable c, Ersatz.Variable.Variable d, Ersatz.Variable.Variable e, Ersatz.Variable.Variable f, Ersatz.Variable.Variable g) => Ersatz.Variable.Variable (a, b, c, d, e, f, g)
instance Ersatz.Variable.GVariable GHC.Generics.U1
instance (Ersatz.Variable.GVariable f, Ersatz.Variable.GVariable g) => Ersatz.Variable.GVariable (f GHC.Generics.:*: g)
instance Ersatz.Variable.GVariable f => Ersatz.Variable.GVariable (GHC.Generics.M1 i c f)


module Ersatz.Bit

-- | A <a>Bit</a> provides a reference to a possibly indeterminate boolean
--   value that can be determined by an external SAT solver.
data Bit
And :: !(Seq Bit) -> Bit
Xor :: !Bit -> !Bit -> Bit
Mux :: !Bit -> !Bit -> !Bit -> Bit
Not :: !Bit -> Bit
Var :: !Literal -> Bit
Run :: (forall m s. (MonadState s m, HasSAT s) => m Bit) -> Bit

-- | Assert claims that <a>Bit</a> must be <a>true</a> in any satisfying
--   interpretation of the current problem.
assert :: (MonadState s m, HasSAT s) => Bit -> m ()

-- | The normal <a>Bool</a> operators in Haskell are not overloaded. This
--   provides a richer set that are.
--   
--   Instances for this class for product-like types can be automatically
--   derived for any type that is an instance of <a>Generic</a>
class Boolean b

-- | Lift a <a>Bool</a>
bool :: Boolean b => Bool -> b

-- | <pre>
--   <a>true</a> = <a>bool</a> <a>True</a>
--   </pre>
true :: Boolean b => b

-- | <pre>
--   <a>false</a> = <a>bool</a> <a>False</a>
--   </pre>
false :: Boolean b => b

-- | Logical conjunction.
(&&) :: Boolean b => b -> b -> b

-- | Logical disjunction (inclusive or).
(||) :: Boolean b => b -> b -> b

-- | Logical implication.
(==>) :: Boolean b => b -> b -> b

-- | Logical negation
not :: Boolean b => b -> b

-- | The logical conjunction of several values.
and :: (Boolean b, Foldable t) => t b -> b

-- | The logical disjunction of several values.
or :: (Boolean b, Foldable t) => t b -> b

-- | The negated logical conjunction of several values.
--   
--   <pre>
--   <a>nand</a> = <a>not</a> . <a>and</a>
--   </pre>
nand :: (Boolean b, Foldable t) => t b -> b

-- | The negated logical disjunction of several values.
--   
--   <pre>
--   <a>nor</a> = <a>not</a> . <a>or</a>
--   </pre>
nor :: (Boolean b, Foldable t) => t b -> b

-- | The logical conjunction of the mapping of a function over several
--   values.
all :: (Boolean b, Foldable t) => (a -> b) -> t a -> b

-- | The logical disjunction of the mapping of a function over several
--   values.
any :: (Boolean b, Foldable t) => (a -> b) -> t a -> b

-- | Exclusive-or
xor :: Boolean b => b -> b -> b

-- | Choose between two alternatives based on a selector bit.
choose :: Boolean b => b -> b -> b -> b

-- | Lift a <a>Bool</a>
bool :: (Boolean b, Generic b, GBoolean (Rep b)) => Bool -> b

-- | Logical conjunction.
(&&) :: (Boolean b, Generic b, GBoolean (Rep b)) => b -> b -> b

-- | Logical disjunction (inclusive or).
(||) :: (Boolean b, Generic b, GBoolean (Rep b)) => b -> b -> b

-- | Logical negation
not :: (Boolean b, Generic b, GBoolean (Rep b)) => b -> b

-- | The logical conjunction of the mapping of a function over several
--   values.
all :: (Boolean b, Foldable t, Generic b, GBoolean (Rep b)) => (a -> b) -> t a -> b

-- | The logical disjunction of the mapping of a function over several
--   values.
any :: (Boolean b, Foldable t, Generic b, GBoolean (Rep b)) => (a -> b) -> t a -> b

-- | Exclusive-or
xor :: (Boolean b, Generic b, GBoolean (Rep b)) => b -> b -> b
instance Ersatz.Bit.Boolean Ersatz.Bit.Bit
instance Ersatz.Codec.Codec Ersatz.Bit.Bit
instance Ersatz.Bit.Boolean a => Ersatz.Bit.GBoolean (GHC.Generics.K1 i a)
instance Ersatz.Bit.Boolean GHC.Types.Bool
instance Ersatz.Bit.GBoolean GHC.Generics.V1
instance Ersatz.Bit.GBoolean GHC.Generics.U1
instance (Ersatz.Bit.GBoolean f, Ersatz.Bit.GBoolean g) => Ersatz.Bit.GBoolean (f GHC.Generics.:*: g)
instance Ersatz.Bit.GBoolean a => Ersatz.Bit.GBoolean (GHC.Generics.M1 i c a)
instance GHC.Show.Show Ersatz.Bit.Bit
instance Ersatz.Variable.Variable Ersatz.Bit.Bit


module Ersatz.Equatable

-- | Instances for this class for arbitrary types can be automatically
--   derived from <a>Generic</a>.
class Equatable t

-- | Compare for equality within the SAT problem.
(===) :: Equatable t => t -> t -> Bit

-- | Compare for equality within the SAT problem.
(===) :: (Equatable t, Generic t, GEquatable (Rep t)) => t -> t -> Bit

-- | Compare for inequality within the SAT problem.
(/==) :: Equatable t => t -> t -> Bit
class GEquatable f
(===#) :: GEquatable f => f a -> f a -> Bit
instance Ersatz.Equatable.Equatable Ersatz.Bit.Bit
instance (GHC.Classes.Eq k, Ersatz.Equatable.Equatable v) => Ersatz.Equatable.Equatable (Data.Map.Internal.Map k v)
instance Ersatz.Equatable.Equatable v => Ersatz.Equatable.Equatable (Data.IntMap.Internal.IntMap v)
instance (Ersatz.Equatable.Equatable a, Ersatz.Equatable.Equatable b) => Ersatz.Equatable.Equatable (a, b)
instance (Ersatz.Equatable.Equatable a, Ersatz.Equatable.Equatable b, Ersatz.Equatable.Equatable c) => Ersatz.Equatable.Equatable (a, b, c)
instance (Ersatz.Equatable.Equatable a, Ersatz.Equatable.Equatable b, Ersatz.Equatable.Equatable c, Ersatz.Equatable.Equatable d) => Ersatz.Equatable.Equatable (a, b, c, d)
instance (Ersatz.Equatable.Equatable a, Ersatz.Equatable.Equatable b, Ersatz.Equatable.Equatable c, Ersatz.Equatable.Equatable d, Ersatz.Equatable.Equatable e) => Ersatz.Equatable.Equatable (a, b, c, d, e)
instance (Ersatz.Equatable.Equatable a, Ersatz.Equatable.Equatable b, Ersatz.Equatable.Equatable c, Ersatz.Equatable.Equatable d, Ersatz.Equatable.Equatable e, Ersatz.Equatable.Equatable f) => Ersatz.Equatable.Equatable (a, b, c, d, e, f)
instance (Ersatz.Equatable.Equatable a, Ersatz.Equatable.Equatable b, Ersatz.Equatable.Equatable c, Ersatz.Equatable.Equatable d, Ersatz.Equatable.Equatable e, Ersatz.Equatable.Equatable f, Ersatz.Equatable.Equatable g) => Ersatz.Equatable.Equatable (a, b, c, d, e, f, g)
instance Ersatz.Equatable.Equatable a => Ersatz.Equatable.Equatable (GHC.Base.Maybe a)
instance Ersatz.Equatable.Equatable a => Ersatz.Equatable.Equatable [a]
instance (Ersatz.Equatable.Equatable a, Ersatz.Equatable.Equatable b) => Ersatz.Equatable.Equatable (Data.Either.Either a b)
instance Ersatz.Equatable.Equatable a => Ersatz.Equatable.GEquatable (GHC.Generics.K1 i a)
instance Ersatz.Equatable.GEquatable GHC.Generics.U1
instance Ersatz.Equatable.GEquatable GHC.Generics.V1
instance (Ersatz.Equatable.GEquatable f, Ersatz.Equatable.GEquatable g) => Ersatz.Equatable.GEquatable (f GHC.Generics.:*: g)
instance (Ersatz.Equatable.GEquatable f, Ersatz.Equatable.GEquatable g) => Ersatz.Equatable.GEquatable (f GHC.Generics.:+: g)
instance Ersatz.Equatable.GEquatable f => Ersatz.Equatable.GEquatable (GHC.Generics.M1 i c f)


module Ersatz.Orderable

-- | Instances for this class for arbitrary types can be automatically
--   derived from <a>Generic</a>.
class Equatable t => Orderable t

-- | Compare for less-than within the SAT problem.
(<?) :: Orderable t => t -> t -> Bit

-- | Compare for less-than or equal-to within the SAT problem.
(<=?) :: Orderable t => t -> t -> Bit

-- | Compare for less-than within the SAT problem.
(<?) :: (Orderable t, Generic t, GOrderable (Rep t)) => t -> t -> Bit

-- | Compare for greater-than or equal-to within the SAT problem.
(>=?) :: Orderable t => t -> t -> Bit

-- | Compare for greater-than within the SAT problem.
(>?) :: Orderable t => t -> t -> Bit
class GEquatable f => GOrderable f
(<?#) :: GOrderable f => f a -> f a -> Bit
(<=?#) :: GOrderable f => f a -> f a -> Bit
instance Ersatz.Orderable.Orderable Ersatz.Bit.Bit
instance (Ersatz.Orderable.Orderable a, Ersatz.Orderable.Orderable b) => Ersatz.Orderable.Orderable (a, b)
instance (Ersatz.Orderable.Orderable a, Ersatz.Orderable.Orderable b, Ersatz.Orderable.Orderable c) => Ersatz.Orderable.Orderable (a, b, c)
instance (Ersatz.Orderable.Orderable a, Ersatz.Orderable.Orderable b, Ersatz.Orderable.Orderable c, Ersatz.Orderable.Orderable d) => Ersatz.Orderable.Orderable (a, b, c, d)
instance (Ersatz.Orderable.Orderable a, Ersatz.Orderable.Orderable b, Ersatz.Orderable.Orderable c, Ersatz.Orderable.Orderable d, Ersatz.Orderable.Orderable e) => Ersatz.Orderable.Orderable (a, b, c, d, e)
instance (Ersatz.Orderable.Orderable a, Ersatz.Orderable.Orderable b, Ersatz.Orderable.Orderable c, Ersatz.Orderable.Orderable d, Ersatz.Orderable.Orderable e, Ersatz.Orderable.Orderable f) => Ersatz.Orderable.Orderable (a, b, c, d, e, f)
instance (Ersatz.Orderable.Orderable a, Ersatz.Orderable.Orderable b, Ersatz.Orderable.Orderable c, Ersatz.Orderable.Orderable d, Ersatz.Orderable.Orderable e, Ersatz.Orderable.Orderable f, Ersatz.Orderable.Orderable g) => Ersatz.Orderable.Orderable (a, b, c, d, e, f, g)
instance Ersatz.Orderable.Orderable a => Ersatz.Orderable.Orderable (GHC.Base.Maybe a)
instance (Ersatz.Orderable.Orderable a, Ersatz.Orderable.Orderable b) => Ersatz.Orderable.Orderable (Data.Either.Either a b)
instance Ersatz.Orderable.Orderable a => Ersatz.Orderable.Orderable [a]
instance Ersatz.Orderable.Orderable a => Ersatz.Orderable.GOrderable (GHC.Generics.K1 i a)
instance Ersatz.Orderable.GOrderable GHC.Generics.U1
instance Ersatz.Orderable.GOrderable GHC.Generics.V1
instance (Ersatz.Orderable.GOrderable f, Ersatz.Orderable.GOrderable g) => Ersatz.Orderable.GOrderable (f GHC.Generics.:*: g)
instance (Ersatz.Orderable.GOrderable f, Ersatz.Orderable.GOrderable g) => Ersatz.Orderable.GOrderable (f GHC.Generics.:+: g)
instance Ersatz.Orderable.GOrderable f => Ersatz.Orderable.GOrderable (GHC.Generics.M1 i c f)


-- | <a>Bits</a> is an arbitrary length natural number type
module Ersatz.Bits

-- | A container of 1 <a>Bit</a> that <a>encode</a>s from and
--   <a>decode</a>s to <a>Word8</a>
newtype Bit1
Bit1 :: Bit -> Bit1

-- | A container of 2 <a>Bit</a>s that <a>encode</a>s from and
--   <a>decode</a>s to <a>Word8</a>
data Bit2
Bit2 :: !Bit -> !Bit -> Bit2

-- | A container of 3 <a>Bit</a>s that <a>encode</a>s from and
--   <a>decode</a>s to <a>Word8</a>
data Bit3
Bit3 :: !Bit -> !Bit -> !Bit -> Bit3

-- | A container of 4 <a>Bit</a>s that <a>encode</a>s from and
--   <a>decode</a>s to <a>Word8</a>
data Bit4
Bit4 :: !Bit -> !Bit -> !Bit -> !Bit -> Bit4

-- | A container of 5 <a>Bit</a>s that <a>encode</a>s from and
--   <a>decode</a>s to <a>Word8</a>
data Bit5
Bit5 :: !Bit -> !Bit -> !Bit -> !Bit -> !Bit -> Bit5

-- | A container of 6 <a>Bit</a>s that <a>encode</a>s from and
--   <a>decode</a>s to <a>Word8</a>
data Bit6
Bit6 :: !Bit -> !Bit -> !Bit -> !Bit -> !Bit -> !Bit -> Bit6

-- | A container of 7 <a>Bit</a>s that <a>encode</a>s from and
--   <a>decode</a>s to <a>Word8</a>
data Bit7
Bit7 :: !Bit -> !Bit -> !Bit -> !Bit -> !Bit -> !Bit -> !Bit -> Bit7

-- | A container of 8 <a>Bit</a>s that <a>encode</a>s from and
--   <a>decode</a>s to <a>Word8</a>
data Bit8
Bit8 :: !Bit -> !Bit -> !Bit -> !Bit -> !Bit -> !Bit -> !Bit -> !Bit -> Bit8
newtype Bits
Bits :: [Bit] -> Bits

-- | <a>HasBits</a> provides the <a>bits</a> method for embedding fixed
--   with numeric encoding types into the arbitrary width <a>Bits</a> type.
class HasBits a
bits :: HasBits a => a -> Bits

-- | Predicate for even-valued <a>Bits</a>s.
isEven :: HasBits b => b -> Bit

-- | Predicate for odd-valued <a>Bits</a>s.
isOdd :: HasBits b => b -> Bit

-- | Optimization of <a>sumBits</a> enabled when summing individual
--   <a>Bit</a>s.
sumBit :: Foldable t => t Bit -> Bits

-- | Compute the sum of a source of <a>Bits</a> values.
sumBits :: (Foldable t, HasBits a) => t a -> Bits

-- | Compute the sum and carry bit from adding three bits.
fullAdder :: Bit -> Bit -> Bit -> (Bit, Bit)

-- | Compute the sum and carry bit from adding two bits.
halfAdder :: Bit -> Bit -> (Bit, Bit)
instance GHC.Generics.Generic Ersatz.Bits.Bit8
instance GHC.Show.Show Ersatz.Bits.Bit8
instance GHC.Generics.Generic Ersatz.Bits.Bit7
instance GHC.Show.Show Ersatz.Bits.Bit7
instance GHC.Generics.Generic Ersatz.Bits.Bit6
instance GHC.Show.Show Ersatz.Bits.Bit6
instance GHC.Generics.Generic Ersatz.Bits.Bit5
instance GHC.Show.Show Ersatz.Bits.Bit5
instance GHC.Generics.Generic Ersatz.Bits.Bit4
instance GHC.Show.Show Ersatz.Bits.Bit4
instance GHC.Generics.Generic Ersatz.Bits.Bit3
instance GHC.Show.Show Ersatz.Bits.Bit3
instance GHC.Generics.Generic Ersatz.Bits.Bit2
instance GHC.Show.Show Ersatz.Bits.Bit2
instance GHC.Generics.Generic Ersatz.Bits.Bit1
instance GHC.Show.Show Ersatz.Bits.Bit1
instance Ersatz.Bits.HasBits Ersatz.Bit.Bit
instance Ersatz.Bits.HasBits Ersatz.Bits.Bit1
instance Ersatz.Bits.HasBits Ersatz.Bits.Bit2
instance Ersatz.Bits.HasBits Ersatz.Bits.Bit3
instance Ersatz.Bits.HasBits Ersatz.Bits.Bit4
instance Ersatz.Bits.HasBits Ersatz.Bits.Bit5
instance Ersatz.Bits.HasBits Ersatz.Bits.Bit6
instance Ersatz.Bits.HasBits Ersatz.Bits.Bit7
instance Ersatz.Bits.HasBits Ersatz.Bits.Bit8
instance Ersatz.Bits.HasBits Ersatz.Bits.Bits
instance GHC.Show.Show Ersatz.Bits.Bits
instance Ersatz.Equatable.Equatable Ersatz.Bits.Bits
instance Ersatz.Orderable.Orderable Ersatz.Bits.Bits
instance Ersatz.Codec.Codec Ersatz.Bits.Bits
instance GHC.Num.Num Ersatz.Bits.Bits
instance Ersatz.Bit.Boolean Ersatz.Bits.Bit8
instance Ersatz.Equatable.Equatable Ersatz.Bits.Bit8
instance Ersatz.Orderable.Orderable Ersatz.Bits.Bit8
instance Ersatz.Variable.Variable Ersatz.Bits.Bit8
instance Ersatz.Codec.Codec Ersatz.Bits.Bit8
instance Ersatz.Bit.Boolean Ersatz.Bits.Bit7
instance Ersatz.Equatable.Equatable Ersatz.Bits.Bit7
instance Ersatz.Orderable.Orderable Ersatz.Bits.Bit7
instance Ersatz.Variable.Variable Ersatz.Bits.Bit7
instance Ersatz.Codec.Codec Ersatz.Bits.Bit7
instance Ersatz.Bit.Boolean Ersatz.Bits.Bit6
instance Ersatz.Equatable.Equatable Ersatz.Bits.Bit6
instance Ersatz.Orderable.Orderable Ersatz.Bits.Bit6
instance Ersatz.Variable.Variable Ersatz.Bits.Bit6
instance Ersatz.Codec.Codec Ersatz.Bits.Bit6
instance Ersatz.Bit.Boolean Ersatz.Bits.Bit5
instance Ersatz.Equatable.Equatable Ersatz.Bits.Bit5
instance Ersatz.Orderable.Orderable Ersatz.Bits.Bit5
instance Ersatz.Variable.Variable Ersatz.Bits.Bit5
instance Ersatz.Codec.Codec Ersatz.Bits.Bit5
instance Ersatz.Bit.Boolean Ersatz.Bits.Bit4
instance Ersatz.Equatable.Equatable Ersatz.Bits.Bit4
instance Ersatz.Orderable.Orderable Ersatz.Bits.Bit4
instance Ersatz.Variable.Variable Ersatz.Bits.Bit4
instance Ersatz.Codec.Codec Ersatz.Bits.Bit4
instance Ersatz.Bit.Boolean Ersatz.Bits.Bit3
instance Ersatz.Equatable.Equatable Ersatz.Bits.Bit3
instance Ersatz.Orderable.Orderable Ersatz.Bits.Bit3
instance Ersatz.Variable.Variable Ersatz.Bits.Bit3
instance Ersatz.Codec.Codec Ersatz.Bits.Bit3
instance Ersatz.Bit.Boolean Ersatz.Bits.Bit2
instance Ersatz.Equatable.Equatable Ersatz.Bits.Bit2
instance Ersatz.Orderable.Orderable Ersatz.Bits.Bit2
instance Ersatz.Variable.Variable Ersatz.Bits.Bit2
instance Ersatz.Codec.Codec Ersatz.Bits.Bit2
instance GHC.Num.Num Ersatz.Bits.Bit2
instance Ersatz.Bit.Boolean Ersatz.Bits.Bit1
instance Ersatz.Equatable.Equatable Ersatz.Bits.Bit1
instance Ersatz.Orderable.Orderable Ersatz.Bits.Bit1
instance Ersatz.Variable.Variable Ersatz.Bits.Bit1
instance Ersatz.Codec.Codec Ersatz.Bits.Bit1
instance GHC.Num.Num Ersatz.Bits.Bit1

module Ersatz.Counting
exactly :: Int -> [Bit] -> Bit
atmost :: Int -> [Bit] -> Bit
atleast :: Int -> [Bit] -> Bit

module Ersatz.Relation
data Relation a b
relation :: (Ix a, Ix b, MonadState s m, HasSAT s) => ((a, b), (a, b)) -> m (Relation a b)
symmetric_relation :: (HasSAT s, MonadState s m, Ix b) => ((b, b), (b, b)) -> m (Relation b b)
build :: (Ix a, Ix b) => ((a, b), (a, b)) -> [((a, b), Bit)] -> Relation a b
buildFrom :: (Ix a, Ix b) => (a -> b -> Bit) -> ((a, b), (a, b)) -> Relation a b
identity :: (Ix a) => ((a, a), (a, a)) -> Relation a a
bounds :: (Ix a, Ix b) => Relation a b -> ((a, b), (a, b))
(!) :: (Ix a, Ix b) => Relation a b -> (a, b) -> Bit
indices :: (Ix a, Ix b) => Relation a b -> [(a, b)]
assocs :: (Ix a, Ix b) => Relation a b -> [((a, b), Bit)]
elems :: (Ix a, Ix b) => Relation a b -> [Bit]
table :: (Enum a, Ix a, Enum b, Ix b) => Array (a, b) Bool -> String
mirror :: (Ix a, Ix b) => Relation a b -> Relation b a
union :: (Ix a, Ix b) => Relation a b -> Relation a b -> Relation a b
complement :: (Ix a, Ix b) => Relation a b -> Relation a b
difference :: (Ix a, Ix b) => Relation a b -> Relation a b -> Relation a b
product :: (Ix a, Ix b, Ix c) => Relation a b -> Relation b c -> Relation a c
power :: (Ix a) => Int -> Relation a a -> Relation a a
intersection :: (Ix a, Ix b) => Relation a b -> Relation a b -> Relation a b
reflexive_closure :: Ix a => Relation a a -> Relation a a
symmetric_closure :: Ix a => Relation a a -> Relation a a
implies :: (Ix a, Ix b) => Relation a b -> Relation a b -> Bit
symmetric :: (Ix a) => Relation a a -> Bit
anti_symmetric :: (Ix a) => Relation a a -> Bit
transitive :: (Ix a) => Relation a a -> Bit
irreflexive :: (Ix a) => Relation a a -> Bit
reflexive :: (Ix a) => Relation a a -> Bit
regular :: (Ix a, Ix b) => Int -> Relation a b -> Bit
regular_in_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit
regular_out_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit
max_in_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit
min_in_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit
max_out_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit
min_out_degree :: (Ix a, Ix b) => Int -> Relation a b -> Bit
empty :: (Ix a, Ix b) => Relation a b -> Bit
complete :: (Ix a, Ix b) => Relation a b -> Bit
total :: (Ix a) => Relation a a -> Bit
disjoint :: (Ix a, Ix b) => Relation a b -> Relation a b -> Bit
equals :: (Ix a, Ix b) => Relation a b -> Relation a b -> Bit


module Ersatz.BitChar

-- | List of <a>BitChar</a> intended to be used as the representation for
--   <a>String</a>.
type BitString = [BitChar]

-- | Encoding of the full range of <a>Char</a> values.
newtype BitChar
BitChar :: Bits -> BitChar
instance GHC.Show.Show Ersatz.BitChar.BitChar
instance Ersatz.Codec.Codec Ersatz.BitChar.BitChar
instance Ersatz.Equatable.Equatable Ersatz.BitChar.BitChar
instance Ersatz.Orderable.Orderable Ersatz.BitChar.BitChar
instance Ersatz.Variable.Variable Ersatz.BitChar.BitChar


module Ersatz
