!"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~(c) Galois, Inc. 2014BSD3jhendrix@galois.com experimentalportable Safe-Inferred !"-./68HM5Result of a verification check.Satisfiability check result.BSome graph quantifies over the state phantom variable for a graph. qA network is an and-invertor graph paired with it's outputs, thus representing a complete combinational circuit. BAn And-Inverter-Graph is a data structure storing bit-level nodes.Graphs are and-inverter graphs, which contain a number of input literals and Boolean operations for creating new literals. Every literal is part of a specific graph, and literals from different networks may not be mixed.Both the types for literals and graphs must take a single phantom type for an arugment that is used to ensure that literals from different networks cannot be used in the same operation. ?Create a temporary graph, and use it to compute a result value.6Build a new graph instance, and packge it into the . type that remembers the IsAIG implementation.6Read an AIG from a file, assumed to be in Aiger format7Get unique literal in graph representing constant true.8Get unique literal in graph representing constant false.!Generate a constant literal valueRReturn if the literal is a fixed constant. If the literal is symbolic, return Nothing.Generate a fresh input literal'Compute the logical and of two literals+Build the conjunction of a list of literals&Compute the logical or of two literals,Compute the logical equality of two literals/Compute the logical implication of two literals(Compute the exclusive or of two literals)Perform a mux (if-then-else on the bits).%Return number of inputs in the graph.&Get input at given index in the graph. Write network out to AIGER file.lWrite network out to DIMACS CNF file. Returns vector mapping combinational inputs to CNF Variable numbers. +Check if literal is satisfiable in network.!+Perform combinational equivalence checking."1Evaluate the network on a set of concrete inputs.#1Evaluate the network on a set of concrete inputs.$JExamine the outermost structure of a literal to see how it was constructed%IBuild an evaluation function over an AIG using the provided view function&_A proxy is used to identify a specific AIG instance when calling methods that create new AIGs.)Negate a literal.*Tests whether two lits are identical. This is only a syntactic check, and may return false even if the two literals represent the same predicate..EConcrete datatype representing the ways an AIG can be constructed.5;Evaluate the given literal using the provided view function6DEvaluate the given list of literals using the provided view function78Build an AIG literal by unfolding a constructor function8@Build a list of AIG literals by unfolding a constructor function92Extract a tree representation of the given literal:3Construct an AIG literal from a tree representation;>Extract a forest representation of the given list of literal s<=Construct a list of AIG literals from a forest representation=^Short-cutting mux operator that optimizes the case where the test bit is a concrete literal>5Get number of inputs associated with current network.?,Number of outputs associated with a network.Unpack  SomeGraph7 in a local scope so it can be used to compute a result@7Convert a sat result to a verify result by negating it.A7Convert a verify result to a sat result by negating it.BGenerate an arbitrary . given a generator for aCGenerate an arbitrary +DjGiven a LitTree, calculate the maximum input number in the tree. Returns 0 if no inputs are referenced.E>Given a list of LitTree, construct a corresponding AIG networkF/Generate a random network by building a random +* and using that to construct a network.I A &C value, used for selecting the concrete implementation typeclass The AIG graph computation to run !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFG  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFG()*  !"#$%=&' >?.43210/+,-9:;<5678A@BCDEF    !"#$%&'()*+,-.43210/56789:;<=>?@ABCDEF(c) Galois, Inc. 2014BSD3jhendrix@galois.com experimentalportableNone-./M[GA BitVector consists of a sequence of symbolic bits and can be used for symbolic machine-word arithmetic. Bits are stored in most-significant-bit first order.HEmpty bitvectorINumber of bits in a bit vectorJGenerate a bitvector of length n, using function f0 to specify the bit literals. The indexes to f% are given in LSB-first order, i.e., f 0 is the least significant bit.KGenerate a bitvector of length n, using monadic function f1 to generate the bit literals. The indexes to f% are given in LSB-first order, i.e., f 0 is the least significant bit.LGenerate a bitvector of length n, using function f0 to specify the bit literals. The indexes to f% are given in MSB-first order, i.e., f 0 is the most significant bit.MGenerate a bitvector of length n, using monadic function f1 to generate the bit literals. The indexes to f% are given in MSB-first order, i.e., f 0 is the most significant bit.N Generate a bit vector of length n" where every bit value is literal l.O Generate a bit vector of length n/ where every bit value is generated in turn by m.P=Generate a one-element bitvector containing the given literalQ/Project the individual bits of a BitVector. x Q 0P is the most significant bit. It is an error to request an out-of-bounds bit.RGAppend two bitvectors, with the most significant bitvector given first.SaConcatenate a list of bitvectors, with the most significant bitvector at the head of the list.TProject out the n( most significant bits from a bitvector.U Drop the n( most significant bits from a bitvector.VExtract n bits starting at index i&. The vector must contain at least i+n elementsWExtract n bits starting at index ig, counting from the end of the vector instead of the beginning. The vector must contain at least i+n elements.X.Combine two bitvectors with a bitwise functionY>Combine two bitvectors with a bitwise monadic combiner action.Z:Convert a bitvector to a list, most significant bit first.[=Convert a list to a bitvector, assuming big-endian bit order.\JSelect bits from a bitvector, starting from the least significant bit. x ! 0Q is the least significant bit. It is an error to request an out-of-bounds bit.]pDisplay a bitvector as a string of bits with most significant bits first. Concrete literals are displayed as '0' or '1'-, whereas symbolic literals are displayed as x.^PGenerate a bitvector from an integer value, using 2's complement representation._6Interpret a bitvector as an unsigned integer. Return Nothing% if the bitvector is not concrete.`3Interpret a bitvector as a signed integer. Return Nothing% if the bitvector is not concrete.a1Retrieve the most significant bit of a bitvector.b2Retrieve the least significant bit of a bitvector.c'If-then-else combinator for bitvectors.dIf-then-else combinator for bitvector computations with optimistic shortcutting. If the test bit is concrete, we can avoid generating either the if or the else circuit.eLazy negation of a circuit.gBuild a short-cut OR circuit. If the left argument evaluates to the constant true, the right argument will not be evaluated.ihConstruct a lazy equality test. If both arguments are constants, the output will also be a constant.kBuild a short-cut AND circuit. If the left argument evaluates to the constant false, the right argument will not be evaluated.n^Construct a lazy xor. If both arguments are constants, the output will also be a constant.AA half adder which takes two inputs and returns output and carry.CA full adder which takes three inputs and returns output and carry.VImplements a ripple carry adder. Both addends are assumed to have the same length.LA subtraction circuit which takes three inputs and returns output and carry.:Subtract two bit vectors, returning result and borrow bit.-Compute just the borrow bit of a subtraction.o2Compute the 2's complement negation of a bitvectorp:Add two bitvectors with the same size. Discard carry bit.q1Add two bitvectors with the same size with carry.rKSubtract one bitvector from another with the same size. Discard carry bit.sBSubtract one bitvector from another with the same size with carry.t#Add a constant value to a bitvectoru#Add a constant value to a bitvectorvMultiply two bitvectors with the same size, with result of the same size as the arguments. Overflow is silently discarded.w+Unsigned multiply two bitvectors with size m and size n#, resulting in a vector of size m+n.x)Signed multiply two bitvectors with size m and size n#, resulting in a vector of size m+n.yHCompute the signed quotient of two signed bitvectors with the same size.zRCompute the signed division remainder of two signed bitvectors with the same size.>Cons value to head of a list and shift other elements to left.{*Return absolute value of signed bitvector.Bitblast version of unsigned quotRem.|LCompute the unsigned quotient of two unsigned bitvectors with the same size.}VCompute the unsigned division remainder of two unsigned bitvectors with the same size.~4Test syntactic equalify of two bitvectors using the * operation3Test equality of two bitvectors with the same size.$Test if a bitvector is equal to zero)Test if a bitvector is distinct from zero3Unsigned less-than on bitvector with the same size.<Unsigned less-than-or-equal on bitvector with the same size.1Signed less-than on bitvector with the same size.:Signed less-than-or-equal on bitvector with the same size.sext v n sign extends v to be a vector with length n. This function requires that  n >= length v and  length v > 0. zext g v n zero extends v to be a vector with length n. This function requires that  n >= length v.5Truncate the given bit vector to the specified lengthHTruncate or zero-extend a bitvector to have the specified number of bitsHTruncate or sign-extend a bitvector to have the specified number of bits&muxInteger mergeFn maxValue lv valueFn$ returns a circuit whose result is  valueFn v when lv has value v.1Shift left. The least significant bit becomes 0.Shift left by a constant.Shift right by a constant.8Signed right shift. The most significant bit is copied.:Unsigned right shift. The most significant bit becomes 0.Rotate left by a constant.Rotate right by a constant. Rotate left. Rotate right.Compute the rounded-down base2 logarithm of the input bitvector. For x > 0, this uniquely satisfies 2^(logBase2_down(x)) <= x < 2^(logBase2_down(x)+1). For x = 0, we set logBase2(x) = -1. The output bitvector has the same width as the input bitvector.Compute the rounded-up base2 logarithm of the input bitvector. For x > 1, this uniquely satisfies 2^(logBase2_up(x) - 1) < x <= 2^(logBase2_up(x)). For x = 1, logBase2_up 1 = 0. For x = 0, we get logBase2_up 0 =  inputbitvector length; this just happens to work out from the defining fomula `logBase2_up x = logBase2_down (x-1) + 1` when interpreted in 2's complement. The output bitvector has the same width as the input bitvector.rCount the number of leading zeros in the input vector; that is, the number of more-significant digits set to 0 above the most significant digit that is set. If the input vector is 0, the output of this function is the length of the bitvector (i.e., all digits are counted as leading zeros). The output bitvector has the same width as the input bitvector.vCount the number of trailing zeros in the input vector; that is, the number of less-significant digits set to 0 below the least significant digit which is set. If the input vector is 0, the output of this function is the length of the bitvector (i.e., all digits are counted as trailing zeros). The output bitvector has the same width as the input bitvector.Given positive x, find the unique i such that: 2^i <= x < 2^(i+1) This is the floor of the lg2 function. We extend the function so intLog2_down 0 = -1.Given positive x, find the unique i such that: 2^(i-1) < x <= 2^i This is the ceiling of the lg2 function. Note: intLog2_up 1 = 0Priority encoder. Given a bitvector, calculate the bit position of the most-significant 1 bit, with position 0 corresponding to the least-significant-bit. Return the "valid" bit, which is set iff at least one bit in the input is set; and the calcuated bit position. If no bits are set in the input (i.e. if the valid bit is false), the calculated bit position is zero. The indicated bitwidth must be large enough to hold the answer; in particular, we must have (length bv <= 2^w).Polynomial multiplication. Note that the algorithm works the same no matter which endianness convention is used. Result length is  max 0 (m+n-1), where m and n are the lengths of the inputs.Polynomial mod with symbolic modulus. Return value has length one less than the length of the modulus. This implementation is optimized for the (common) case where the modulus is concrete.LPolynomial division. Return value has length equal to the first argument.kGHIJn#, length of the generated bitvectorf$, function to calculate bit literalsKn#, length of the generated bitvectorf', computation to generate a bit literaln#, length of the generated bitvectorf', computation to generate a bit literalLn#, length of the generated bitvectorf$, function to calculate bit literalsMn#, length of the generated bitvectorf', computation to generate a bit literalNn, length of the bitvectorl, the value to replicateOn, length of the bitvectorm&, the computation to produce a literalPQRSTUVi, 0-based start indexn, bits to take%a vector consisting of the bits from i to i+n-1Wi0, 0-based start index from the end of the vectorn, bits to takeXYZ[\]^)number of bits in the resulting bitvector integer value_`abctest bitthen bitvectorelse bitvectordtest bitthen circuit computationelse circuit computationefghijklmnsum and carry-out bitopqrstuvwxyz{|}~.Maximum value input vector is allowed to take. Input vectorthe value to shifthow many places to shiftthe value to shifthow many places to shiftthe value to shifthow many places to shiftthe value to rotatehow many places to rotatethe value to rotatehow many places to rotateinput bitvectorinput bitvectorinput bitvectorinput bitvectorwidth of the output bitvectorinput bitvector Valid bit and position bitvectorwidth of the output bitvectorinput bitvectorRGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~RGHIQ\RSTUVWXYab~]MLKJNO^[Pklghnmijefcd_`Zopqrstuvwxyz|}{iGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~(c) Galois, Inc. 2014BSD3jhendrix@galois.com experimentalportableNone2468=HM##(c) Galois, Inc. 2014BSD3jhendrix@galois.com experimentalportableNone  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~       !"#$%&'())*+,--./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~H aig-0.2.3Data.AIG.InterfaceData.AIG.OperationsData.AIG.TraceData.AIG VerifyResult VerifyUnknownInvalidValid SatResult SatUnknownSatUnsat SomeGraphNetworkIsAIG withNewGraphnewGraph aigerNetworktrueLitfalseLitconstant asConstantnewInputandandsoreqimpliesxormux inputCountgetInput writeAigerwriteCNFcheckSatcec evaluatorevaluatelitViewabstractEvaluateAIGProxyIsLitnot===LitTree unLitTreeLitViewFalseLitTrueLitNotInputInputNotAndAndfoldAIGfoldAIGs unfoldAIG unfoldAIGs toLitTree fromLitTree toLitForest fromLitForestlazyMuxnetworkInputCountnetworkOutputCounttoVerifyResult toSatResult genLitView genLitTree getMaxInput buildNetwork randomNetworkBVemptylength generate_lsb0generateM_lsb0 generate_msb0generateM_msb0 replicate replicateM singletonat++concattakedropslicesliceRevzipWithzipWithMbvToList bvFromList!bvShow bvFromInteger asUnsignedasSignedmsblsbiteiteMlNotlNot'lOrlOr'lEqlEq'lAndlAnd'lXor'lXornegaddaddCsubsubCaddConstsubConstmulmulFullsmulFullsquotsremsabsuquoturembvSamebvEqisZerononZeroultulesltslesextzexttrunc zeroIntCoerce signIntCoerce muxIntegershlsshrushrrolror logBase2_down logBase2_upcountLeadingZeroscountTrailingZerospriorityEncodepmulpmodpdiv TraceOutput traceOutputTraceOptraceOp TraceGraphtGraphtActiveTraceLit unTraceLit Traceable compareLitshowLitproxyactivateTracingdeactiveTracing withTracingwithNewGraphTracing$fIsAIGTraceLitTraceGraph$fTraceOutputlgLitView$fTraceOutputlgVerifyResult$fTraceOutputlgSatResult$fTraceOutputlg()$fTraceOutputlgInt$fTraceOutputlgTraceLit$fTraceOutputlg[] $fTraceOplgIO$fTraceOplg(->)$fTraceOplg(->)0$fTraceOplg(->)1$fTraceOplg(->)2 $fOrdTraceLit $fEqTraceLit$fIsLitTraceLit withSomeGraph$fArbitraryLitTree halfAdder fullAdder ripple_addfullSub ripple_subripple_sub_borrowshiftL1uquotRemshlCshrCrolCrorC intLog2_down intLog2_upunBVtailgenerateM_scan_lsb0lAnd''splitAtnegWhensquotRemdoPriorityEncodepdivmodpdivmod_helper