h&wl      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                                                                                                                                         . Edward Kmett 2010-2014, Johan Kiviniemi 2013BSD3Edward Kmett  experimental non-portable Safe-Inferred ersatz5A naked possibly-negated Atom, present in the target  . The literals -1 and 1 are dedicated for the constant  and the constant  respectively.ersatzThe  constant. The literal -1 is dedicated for it.ersatzThe  constant. The literal 1 is dedicated for it.. Edward Kmett 2010-2014, Johan Kiviniemi 2013BSD3Edward Kmett  experimental non-portable Safe-Inferred u ersatzA conjunction of clauses ersatzA disjunction of possibly negated atoms. Negated atoms are represented by negating the identifier.ersatz5Extract the (possibly negated) atoms referenced by a  .ersatzA formula with no clausesersatzAssert a literalersatz The boolean not operation)Derivation of the Tseitin transformation: /O D A (O C A) & (O C A) (O | A) & (O | A) ersatz The boolean and operation)Derivation of the Tseitin transformation: O D (A & B & C) (O C (A & B & C)) & (O C (A & B & C)) (O | (A & B & C)) & (O | (A & B & C)) (O | A) & (O | B) & (O | C) & (O | A | B | C) ersatz The boolean or operation)Derivation of the Tseitin transformation: O D (A | B | C) (O C (A | B | C)) & (O C (A | B | C)) (O | (A | B | C)) & (O | (A | B | C)) (O | A | B | C) & (O | (A & B & C)) (O | A | B | C) & (O | A) & (O | B) & (O | C) ersatz The boolean xor operation)Derivation of the Tseitin transformation: O D A E B O D ((A & B) | (A & B)) (O C ((A & B) | (A & B))) & (O C ((A & B) | (A & B))) Left hand side: O C ((A & B) | (A & B)) O | ((A & B) | (A & B)) O | ((A | A) & (A | B) & (A | B) & (B | B)) O | ((A | B) & (A | B)) (O | A | B) & (O | A | B) Right hand side: O C ((A & B) | (A & B)) O | ((A & B) | (A & B)) O | ((A & B) & (A & B)) O | ((A | B) & (A | B)) (O | A | B) & (O | A | B) Result: <(O | A | B) & (O | A | B) & (O | A | B) & (O | A | B) ersatzwith redundant clauses, cf. discussion in Een and Sorensen, Translating Pseudo Boolean Constraints ..., p. 7 http://minisat.se/Papers.html The boolean  else-then-if or mux operation)Derivation of the Tseitin transformation: O D (F & P) | (T & P) (O C ((F & P) | (T & P))) & (O C ((F & P) | (T & P))) Left hand side: O C ((F & P) | (T & P)) O | ((F & P) | (T & P)) O | ((F | T) & (F | P) & (T | P) & (P | P)) O | ((F | T) & (F | P) & (T | P)) (O | F | T) & (O | F | P) & (O | T | P) Right hand side: O C ((F & P) | (T & P)) O | ((F & P) | (T & P)) O | ((F & P) & (T & P)) O | ((F | P) & (T | P)) (O | F | P) & (O | T | P) Result: (O | F | T) & (O | F | P) & (O | T | P) & (O | F | P) & (O | T | P) ersatzOutputersatzInputersatzOutputersatzInputsersatzOutputersatzInputsersatzOutputersatzInputersatzInputersatzOutputersatz False branchersatz True branchersatzPredicate/selector   . Edward Kmett 2010-2014, Johan Kiviniemi 2013BSD3Edward Kmett  experimental non-portable Safe-Inferred/ . Edward Kmett 2010-2014, Johan Kiviniemi 2013BSD3Edward Kmett  experimental non-portable Safe-Inferred. Edward Kmett 2010-2014, Johan Kiviniemi 2013BSD3Edward Kmett  experimental non-portable Trustworthy "/ersatzAn explicit prenex quantifier%ersatz"WDIMACS file format pretty printer;This is used to generate the problem statement for a given MaxSAT   (TODO).*ersatz"QDIMACS file format pretty printer;This is used to generate the problem statement for a given 6  ./ersatz!DIMACS file format pretty printer;This is used to generate the problem statement for a given =  .6ersatzA (quantified) boolean formula.ersatz:a set indicating which literals are universally quantifiedersatz The rest of the information, in =ersatz!The id of the last atom allocatedersatza set of clauses to assertersatza mapping used during Bit expansion?ersatz5Constraint synonym for types that carry a QSAT state.@ersatz4Constraint synonym for types that carry a SAT state.AersatzRun a =-generating state computation. Useful e.g. in ghci for disambiguating the type of a @ value.BersatzRun a =%-generating state computation in the > monad. Useful e.g. in ghci for disambiguating the type of a @ value.CersatzRun a =9-generating state computation and return the respective /* output. Useful for testing and debugging.GersatzRun a 6-generating state computation. Useful e.g. in ghci for disambiguating the type of a , 3 value.HersatzRun a 6%-generating state computation in the > monad. Useful e.g. in ghci for disambiguating the type of a , 3 value.IersatzRun a 69-generating state computation and return the respective ** output. Useful for testing and debugging.Kersatz Generate a  out of a / problem.Lersatz Generate a  out of a * problem.Mersatz Generate a  out of a % problem.ersatzthe name is wrong (Does it return Clauses? No - it returns IntSets.) and it means extra work (traversing, and re-building, the full collection). Or is this fused away (because of Coercible)?(ersatzSpecified to be 1 D n < 2^63)%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLM)=>89:;<@ABCDEF67345?GHIJ/012*+,-.%&'()KLM. Edward Kmett 2010-2014, Johan Kiviniemi 2013BSD3Edward Kmett  experimental non-portable Safe-Inferred!WersatzA W s m7 is responsible for invoking a solver and returning a X! and a map of determined results.s is typically = or 6m is typically  WXYZ[\]^_` \]^_`XYZ[W. Edward Kmett 2010-2014, Johan Kiviniemi 2013BSD3Edward Kmett  experimental non-portable Safe-Inferred"hersatzThis class describes data types that can be marshaled to or from a SAT solver.jersatz>Return a value based on the solution if one can be determined.hikjhikj. Edward Kmett 2010-2014, Johan Kiviniemi 2013BSD3Edward Kmett  experimental non-portable Safe-Inferred% ersatzThis error is thrown by  when no solvers are found.ersatzTry a list of solvers in order. When a solver fails due to a missing executable the next solver will be tried. Throws 7 exception if none of the given solvers were installed.ersatz0Problem file extension including the dot, if anyersatz1Solution file extension including the dot, if any. Edward Kmett 2010-2014, Johan Kiviniemi 2013BSD3Edward Kmett  experimental non-portable Safe-Inferred&~ersatz This is a W for 6 problems that runs the depqbf solver using the current PATH&, it tries to run an executable named depqbf.ersatz This is a W for 60 problems that lets you specify the path to the depqbf executable.~~. Edward Kmett 2010-2014, Johan Kiviniemi 2013BSD3Edward Kmett  experimental non-portable Safe-Inferred"*^ersatzHybrid W that tries to use: , , and ersatzW for =# problems that tries to invoke the minisat executable from the PATHersatzW for =# problems that tries to invoke the  cryptominisat executable from the PATHersatzW for =4 problems that tries to invoke a program that takes minisat compatible arguments.The & refers to the path to the executable.ersatzW for =# problems that tries to invoke the cryptominisat5 executable from the PATHersatzW for =4 problems that tries to invoke a program that takes cryptominisat5 compatible arguments.The & refers to the path to the executable.. Edward Kmett 2010-2014, Johan Kiviniemi 2013BSD3Edward Kmett  experimental non-portable Safe-Inferred,ersatzW for =# problems that tries to invoke the z3 executable from the PATHersatzW for =4 problems that tries to invoke a program that takes z3 compatible arguments.The & refers to the path to the executable. . Edward Kmett 2010-2014, Johan Kiviniemi 2013BSD3Edward Kmett  experimental non-portable Safe-Inferred, ~ . Edward Kmett 2010-2014, Johan Kiviniemi 2013BSD3Edward Kmett  experimental non-portable Safe-Inferred</}ersatzThis class describes all types that can be represented by a collection of literals. The class method  is usually applied to D or J, see implementations of  and .Instances for this class for product-like types can be automatically derived for any type that is an instance of . Example usage {-# language DeriveGeneric, TypeApplications #-} import GHC.Generics data T = C Bit Bit deriving Generic instance Variable T constraint = do t <- exists @T ; ...  . Edward Kmett 2010-2014, Johan Kiviniemi 2013BSD3Edward Kmett  experimental non-portable Trustworthy <5ersatz The normal  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 ersatzLift a ersatz  =  ersatz  =  ersatzLogical conjunction.ersatz#Logical disjunction (inclusive or).ersatzLogical implication.ersatzLogical negationersatz*The logical conjunction of several values.ersatz*The logical disjunction of several values.ersatz2The negated logical conjunction of several values.  =  . ersatz2The negated logical disjunction of several values.  =  . ersatzThe logical conjunction of the mapping of a function over several values.ersatzThe logical disjunction of the mapping of a function over several values.ersatz Exclusive-orersatz8Choose between two alternatives based on a selector bit.ersatzA  provides a reference to a possibly indeterminate boolean value that can be determined by an external SAT solver.ersatzAssert claims that  must be : in any satisfying interpretation of the current problem.ersatz Convert a  to a .ersatz False branchersatz True branchersatzPredicate/selector branch32032 Safe-InferredEs ersatz Relation a b represents a binary relation R \subseteq A \times B , where the domain A is a finite subset of the type a, and the codomain B is a finite subset of the type b.#A relation is stored internally as Array (a,b) Bit, so a and b have to be instances of  , and both A and B are intervals.ersatz"relation ((amin,bmin),(amax,mbax))& constructs an indeterminate relation  R \subseteq A \times B  where A is {amin .. amax} and B is @{bmin .. bmax}$.ersatz%Constructs an indeterminate relation  R \subseteq B \times B  that it is symmetric, i.e., = \forall x, y \in B: ((x,y) \in R) \rightarrow ((y,x) \in R) .A symmetric relation is an undirected graph, possibly with loops.ersatzConstructs a relation R \subseteq A \times B  from a list.Example r = build ((0,a),(1,b)) [((0,a), true), ((0,b)), false), ((1,a), false), ((1,b ), true))] ersatzConstructs a relation R \subseteq A \times B  from a function.ersatz!Constructs the identity relation 4I \subseteq A \times A, I = \{ (x,x) ~|~ x \in A \} .ersatzThe bounds of the array that correspond to the matrix representation of the given relation.Exampler = build ((0,0),(1,1)) [((0,0), false), ((0,1), true), ((1,0), true), ((1,1), false))]bounds r ((0,0),(1,1))ersatz; corresponds to the matrix representation of this relation.ersatzSince a symmetric relation must be homogeneous, the domain must equal the codomain. Therefore, given bounds  ((p,q),(r,s)), it must hold that p=q and r=s.ersatzA list of tuples, where the first element represents an element  (x,y) \in A \times B & and the second element is a positive  if  (x,y) \in R , or a negative  if  (x,y) \notin R .ersatz8A function with the specified signature, that assigns a -value to each element  (x,y) \in A \times B .ersatzSince the identity relation is homogeneous, the domain must equal the codomain. Therefore, given bounds  ((p,q),(r,s)), it must hold that p=q and r=s.  Safe-InferredNe ersatz!Constructs the converse relation  R^{-1} \subseteq B \times A  of a relation  R \subseteq A \times B , which is defined by & R^{-1} = \{ (y,x) ~|~ (x,y) \in R \} .ersatz#Constructs the complement relation  \overline{R}  of a relation  R \subseteq A \times B , which is defined by ? \overline{R} = \{ (x,y) \in A \times B ~|~ (x,y) \notin R \} .ersatzConstructs the difference  R \setminus S  of the relations R and S), that contains all elements that are in R but not in S , i.e., 6 R \setminus S = \{ (x,y) \in R ~|~ (x,y) \notin S \} . Note that if  R \subseteq A \times B  and  S \subseteq C \times D , then  A \times B  must be a subset of  C \times D  and $ R \setminus S \subseteq A \times B .ersatzConstructs the union  R \cup S  of the relations  R  and  S .Note that for  R \subseteq A \times B  and  S \subseteq C \times D , it must hold that ! A \times B \subseteq C \times D .ersatzConstructs the composition  R \cdot S  of the relations  R \subseteq A \times B  and  S \subseteq B \times C , which is defined by ? R \cdot S = \{ (a,c) ~|~ ((a,b) \in R) \land ((b,c) \in S) \} .ersatzConstructs the relation  R^{n}  that results if a relation  R \subseteq A \times A  is composed n times with itself. R^{0}  is the identity relation ! I_{R} = \{ (x,x) ~|~ x \in A \}  of R.ersatzConstructs the intersection  R \cap S  of the relations  R  and  S .Note that for  R \subseteq A \times B  and  S \subseteq C \times D , it must hold that ! A \times B \subseteq C \times D .ersatz!Constructs the reflexive closure  R \cup I_{R}  of the relation  R \subseteq A \times A , where ! I_{R} = \{ (x,x) ~|~ x \in A \}  is the identity relation of R.ersatz!Constructs the symmetric closure  R \cup R^{-1}  of the relation  R \subseteq A \times A , where & R^{-1} = \{ (y,x) ~|~ (x,y) \in R \}  is converse relation of R.ersatzn  . Edward Kmett 2010-2014, Johan Kiviniemi 2013BSD3Edward Kmett  experimental non-portable Safe-Inferred <OersatzInstances for this class for arbitrary types can be automatically derived from .ersatz,Compare for equality within the SAT problem.ersatz.Compare for inequality within the SAT problem.44. Edward Kmett 2010-2014, Johan Kiviniemi 2013BSD3Edward Kmett  experimental non-portable Safe-Inferred <Se ersatzInstances for this class for arbitrary types can be automatically derived from .ersatz-Compare for less-than within the SAT problem.ersatz9Compare for less-than or equal-to within the SAT problem.ersatzCompare by lexicographic order on: root node, list of childrenersatz*Compare by lexicographic order on elementsersatz8Compare by lexicographic order on sorted key-value pairsersatz8Compare by lexicographic order on sorted key-value pairs4444 Edward Kmett 2010-2015,  Eric Mertens 2014, Johan Kiviniemi 2013BSD3Edward Kmett  experimental non-portable Safe-Inferred;]Lersatz provides the  method for embedding fixed with numeric encoding types into the arbitrary width  type.ersatzA container of s that is suitable for comparisons and arithmetic. Bits are stored with least significant bit first to enable phantom  values to be truncated.ersatzA container of 8 s that k s from and js to . MSB is first.ersatzA container of 7 s that k s from and js to . MSB is first.ersatzA container of 6 s that k s from and js to . MSB is first.ersatzA container of 5 s that k s from and js to . MSB is first.ersatzA container of 4 s that k s from and js to . MSB is first.ersatzA container of 3 s that k s from and js to . MSB is first.ersatzA container of 2 s that k s from and js to . MSB is first.ersatzA container of 1  that k s from and js to .ersatz5Compute the sum and carry bit from adding three bits.ersatz3Compute the sum and carry bit from adding two bits.ersatzZip the component bits of a & extending the shorter argument with  values.ersatzAdd two $ values given an incoming carry bit.ersatzCompute the sum of a source of  values.ersatzOptimization of " enabled when summing individual s.ersatzPredicate for odd-valued s.ersatzPredicate for even-valued s.ersatzThis instance provides modular arithmetic (overflow is ignored).ersatzThis instance provides modular arithmetic (overflow is ignored).ersatzThis instance provides full arithmetic. The result has large enough width so that there is no overflow.Subtraction is modified: a - b denotes  max 0 (a - b). Width of a + b is 1 + max (width a) (width b) , width of a * b is (width a) + (width b) , width of a - b is max (width a) (width b). fromInteger will raise  for negative arguments.ersatz (sum, carry)ersatz (sum, carry) Safe-Inferred] Safe-InferrediersatzTests if the first relation R$ is a subset of the second relation S-, i.e., every element that is contained in R is also contained in S. Note that if  R \subseteq A \times B  and  S \subseteq C \times D , then  A \times B  must be a subset of  C \times D .ersatzTests if a relation is empty, i.e., the relation doesn't contain any elements.ersatzTests if a relation  R \subseteq A \times B  is complete, i.e., R = A \times B .ersatzTests if a relation  R \subseteq A \times A  is strongly connected, i.e., 6 \forall x, y \in A: ((x,y) \in R) \lor ((y,x) \in R) .ersatzTests if two relations are disjoint, i.e., there is no element that is contained in both relations.ersatzTests if two relations  R, S \subseteq A \times B 3 are equal, i.e., they contain the same elements.ersatzTests if a relation  R \subseteq A \times A  is symmetric, i.e., = \forall x, y \in A: ((x,y) \in R) \rightarrow ((y,x) \in R) .ersatzTests if a relation  R \subseteq A \times A  is antisymmetric, i.e.,  \forall x, y \in A: ((x,y) \in R) \land ((y,x) \in R)) \rightarrow (x = y) .ersatzTests if a relation  R \subseteq A \times A  is irreflexive, i.e., ! \forall x \in A: (x,x) \notin R .ersatzTests if a relation  R \subseteq A \times A  is reflexive, i.e.,  \forall x \in A: (x,x) \in R .ersatz Given an   n  and a relation  R \subseteq A \times B  , check if , \forall x \in A: | \{ (x,y) \in R \} | = n  and , \forall y \in B: | \{ (x,y) \in R \} | = n  hold.ersatz Given an   n  and a relation  R \subseteq A \times B  , check if , \forall x \in A: | \{ (x,y) \in R \} | = n  holds.ersatz Given an   n  and a relation  R \subseteq A \times B  , check if / \forall x \in A: | \{ (x,y) \in R \} | \leq n  holds.ersatz Given an   n  and a relation  R \subseteq A \times B  , check if / \forall x \in A: | \{ (x,y) \in R \} | \geq n  holds.ersatz Given an   n  and a relation  R \subseteq A \times B  , check if , \forall y \in B: | \{ (x,y) \in R \} | = n  holds.ersatz Given an   n  and a relation  R \subseteq A \times B  , check if / \forall y \in B: | \{ (x,y) \in R \} | \leq n  holds.ersatz Given an   n  and a relation  R \subseteq A \times B  , check if / \forall y \in B: | \{ (x,y) \in R \} | \geq n  holds.ersatzTests if a relation  R \subseteq A \times A  is transitive, i.e.,  \forall x, y \in A: ((x,y) \in R) \land ((y,z) \in R) \rightarrow ((x,z) \in R) . $Johannes Waldmann, Antonia SwiridoffBSD3 Safe-Inferredi'' Eric Mertens 2010-2014BSD3Edward Kmett  experimental non-portable Safe-InferredkAersatzEncoding of the full range of  values.ersatzList of / intended to be used as the representation for .. Edward Kmett 2010-2014, Johan Kiviniemi 2013BSD3Edward Kmett  experimental non-portable Safe-Inferredk%)(&'*.-+,/201345678<;9:=>?@ABCDEFGHIJKLMWX[YZ\_]^`hjiki~ !""#$$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMMNOPQRSSTUVWXYZ[\]^_`abcdefghijklmnoppqrstuvwxyz{|}~                                                                                                     $ersatz-0.4.13-7E7YD0VFgNU8GCjMXSB1mVErsatz.Internal.LiteralErsatz.Internal.FormulaErsatz.ProblemErsatz.Solution Ersatz.CodecErsatz.Solver.DepQBFErsatz.Solver.MinisatErsatz.Solver.Z3 Ersatz.SolverErsatz.Variable Ersatz.BitErsatz.RelationErsatz.EquatableErsatz.Orderable Ersatz.BitsErsatz.CountingErsatz.BitCharSolverErsatz.Internal.ParserErsatz.Internal.StableNameErsatz.Solver.CommonErsatz.Relation.DataErsatz.Relation.OpErsatz.Relation.PropErsatzLiteral literalId negateLiteral literalFalse literalTrue $fShowLiteral $fEqLiteral $fOrdLiteralFormula formulaSetClause clauseSetclauseLiterals fromLiteral formulaEmptyformulaLiteral fromClause formulaNot formulaAnd formulaOr formulaXor formulaMux formulaFAS formulaFAC $fShowClause$fMonoidClause$fSemigroupClause $fShowFormula$fMonoidFormula$fSemigroupFormula $fEqFormula $fOrdFormula $fEqClause $fOrdClauseWDIMACSwdimacsCommentswdimacsNumVariableswdimacsTopWeightwdimacsClausesQDIMACSqdimacsCommentsqdimacsNumVariablesqdimacsQuantifiedqdimacsClausesDIMACSdimacsCommentsdimacsNumVariables dimacsClausesHasQSATqsat universalsQSATHasSATsatlastAtomformula stableMapSAT MonadQSATMonadSATrunSATrunSAT' dimacsSAT literalExists assertFormulagenerateLiteralrunQSATrunQSAT' qdimacsQSAT literalForalldimacsqdimacswdimacs $fDefaultSAT $fShowSAT $fHasSATSAT $fDefaultQSAT $fHasSATQSAT $fHasQSATQSAT $fDIMACSSAT $fQDIMACSQSAT $fShowQSATResultUnsolved Unsatisfied SatisfiedSolutionsolutionLiteralsolutionStableName solutionFrom$fBoundedResult $fEnumResult $fEqResult $fOrdResult $fIxResult $fShowResult $fReadResultCodecDecodeddecodeencode $fCodecTree $fCodecSeq $fCodecMaybe $fCodecMap $fCodecIntMap$fCodecHashMap $fCodecEither $fCodecArray $fCodec[]$fCodec(,,,,,,,)$fCodec(,,,,,,)$fCodec(,,,,,) $fCodec(,,,,) $fCodec(,,,) $fCodec(,,) $fCodec(,) $fCodec()$fCodecLiteraldepqbf depqbfPath anyminisatminisat cryptominisat minisatPathcryptominisat5cryptominisat5Pathz3z3Path solveWithVariable literally GVariable gliterallyexistsforallgenericLiterally $fGVariableM1$fGVariable:*: $fGVariableU1$fVariable(,,,,,,)$fVariable(,,,,,)$fVariable(,,,,)$fVariable(,,,)$fVariable(,,) $fVariable(,)$fVariableLiteral $fGVariableK1Booleanbooltruefalse&&||==>notandornandnorallanyxorchooseBitAndXorMuxNotVarRunassert $fVariableBit $fShowBit $fGBooleanM1 $fGBoolean:*: $fGBooleanU1 $fGBooleanV1 $fBooleanBool $fGBooleanK1 $fCodecBit $fBooleanBitRelationrelationsymmetric_relationbuild buildFromidentityboundsindicesassocselems!tablemirror complement differenceunionproductpower intersectionreflexive_closuresymmetric_closure GEquatable===# Equatable===/==$fGEquatableM1$fGEquatable:+:$fGEquatable:*:$fGEquatableV1$fGEquatableU1$fEquatableBool$fEquatableOrdering$fEquatableDouble$fEquatableFloat$fEquatableChar$fEquatableInt64$fEquatableInt32$fEquatableInt16$fEquatableInt8$fEquatableWord64$fEquatableWord32$fEquatableWord16$fEquatableWord8$fEquatableWord$fEquatableNatural$fEquatableInteger$fEquatableInt$fEquatableVoid $fEquatable()$fGEquatableK1$fEquatableEither$fEquatableNonEmpty $fEquatable[]$fEquatableMaybe$fEquatable(,,,,,,)$fEquatable(,,,,,)$fEquatable(,,,,)$fEquatable(,,,)$fEquatable(,,)$fEquatable(,)$fEquatableTree$fEquatableSeq$fEquatableIntMap$fEquatableMap$fEquatableBit GOrderable=?>?$fGOrderableM1$fGOrderable:+:$fGOrderable:*:$fGOrderableV1$fGOrderableU1$fOrderableBool$fOrderableOrdering$fOrderableDouble$fOrderableFloat$fOrderableChar$fOrderableInt64$fOrderableInt32$fOrderableInt16$fOrderableInt8$fOrderableWord64$fOrderableWord32$fOrderableWord16$fOrderableWord8$fOrderableWord$fOrderableNatural$fOrderableInteger$fOrderableInt$fOrderableVoid $fOrderable()$fGOrderableK1 $fOrderable[]$fOrderableEither$fOrderableMaybe$fOrderable(,,,,,,)$fOrderable(,,,,,)$fOrderable(,,,,)$fOrderable(,,,)$fOrderable(,,)$fOrderable(,)$fOrderableTree$fOrderableSeq$fOrderableIntMap$fOrderableMap$fOrderableBitHasBitsbitsBitsBit8Bit7Bit6Bit5Bit4Bit3Bit2Bit1 fullAdder halfAddersumBitssumBitisOddisEven $fNumBit1 $fCodecBit1$fVariableBit1$fOrderableBit1$fEquatableBit1 $fBooleanBit1 $fNumBit2 $fCodecBit2$fVariableBit2$fOrderableBit2$fEquatableBit2 $fBooleanBit2 $fCodecBit3$fVariableBit3$fOrderableBit3$fEquatableBit3 $fBooleanBit3 $fCodecBit4$fVariableBit4$fOrderableBit4$fEquatableBit4 $fBooleanBit4 $fCodecBit5$fVariableBit5$fOrderableBit5$fEquatableBit5 $fBooleanBit5 $fCodecBit6$fVariableBit6$fOrderableBit6$fEquatableBit6 $fBooleanBit6 $fCodecBit7$fVariableBit7$fOrderableBit7$fEquatableBit7 $fBooleanBit7 $fCodecBit8$fVariableBit8$fOrderableBit8$fEquatableBit8 $fBooleanBit8 $fNumBits $fCodecBits$fOrderableBits$fEquatableBits $fShowBits $fHasBitsBits $fHasBitsBit8 $fHasBitsBit7 $fHasBitsBit6 $fHasBitsBit5 $fHasBitsBit4 $fHasBitsBit3 $fHasBitsBit2 $fHasBitsBit1 $fHasBitsBit $fShowBit8 $fGenericBit8 $fShowBit7 $fGenericBit7 $fShowBit6 $fGenericBit6 $fShowBit5 $fGenericBit5 $fShowBit4 $fGenericBit4 $fShowBit3 $fGenericBit3 $fShowBit2 $fGenericBit2 $fShowBit1 $fGenericBit1exactlyatmostatleastimpliesemptycompletetotaldisjointequals symmetricanti_symmetric irreflexive reflexiveregularregular_out_degreemax_out_degreemin_out_degreeregular_in_degree max_in_degree min_in_degree transitiveBitChar BitString$fVariableBitChar$fOrderableBitChar$fEquatableBitChar$fCodecBitChar $fShowBitCharghc-prim GHC.TypesFalseTrueParser runParsersepBysepBy1tokenstringintegernaturaleofsatisfybaseGHC.StableName StableNamemakeStableName'Quant _universals_qsatSat _lastAtom_formula _stableMapData.Functor.IdentityIdentity mtl-2.2.2Control.Monad.State.Class MonadStatebytestring-0.11.3.1 Data.ByteString.Builder.InternalBuilder satClausesIO NoSolvers trySolvers withTempFilesresultOfparseSolution5GHC.IOFilePath GHC.GenericsGenericBoolrunBit&&#||#GHC.IxIxGHC.WordWord8 zipWithBitsaddBitsGHC.ErrerrorIntCharGHC.BaseString