h$6      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                                                                                                                                                                                                              !!!!!!!!!!!!""""""""""""""""""""""###########################$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%&&&&&&&&&&&&&&&&&& ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ) ) ) ) ) ) * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , - - - - - - - - - - ----------------------------------------------------------........................//////////////////////////////////////////////////////////////////////////////////////////////000000000000000000000001111111111111111222222222222222222222222222222222222222222222222222222222222222222222333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333334444444444444444444444444444444444444444444444444444444444444444445555555555555555555555555555555555555555555555555555555555555555555555555555555555555555555555567777777777777889999::::::::::::::::::::;;;;;;;;;;;;;;;;;;;;;<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<==============================>>>>>>>>>>>>>>>>>?????????????????????????????@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABBBBBBBBBBBBBBCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCDDDDDDDDDDDDEEEEEEEEEEFFFFFFFFFFFFGGGGGGGGGGGGGGGHHHHHHHHHHHHIIIIIITesting abstraction layer(c) Galois Inc, 2020BSD3kquick@galois.comNoneE what4This is the generator monad for the Verification proxy tests. The inner monad will be the actual test implementation's monadic generator, and the a9 return type is the type returned by running this monad.Tests should only use the 'Gen TYPE' as an output; the constructors and internals should be used only by the test concretization.what4This is the reader environment for the surface level proxy testing monad. This environment will be provided by the actual test code to map these proxy operations to the specific testing implementation. what49Internal data structure to store the two elements to the  assumption operator.what4A class specifying things that can be verified by constructing a local Property.what4Local definition of a Property: intended to be a proxy for a QuickCheck Property or a Hedgehog Property. The  implementation function converts from these proxy Properties to the native Property implementation.Tests should only use the  type as an output; the constructors and internals should be used only by the test concretization.what42Used by testing code to assert a boolean property.what4The named form of the  assumption operatorwhat4The assumption operator that performs the property test (second element) only when the first argument is true (the assumption guard for the test). This is the analog to the corresponding QuickCheck ==> operator.what4+A test generator that returns True or Falsewhat4!A test generator that returns an 1 value between the specified (inclusive) bounds.what4!A test generator that returns an 1 value between the specified (inclusive) bounds.what4A test generator that returns the current shrink size of the generator functionality.what4This function should be called by the testing code to convert the proxy tests in this module into the native tests (e.g. QuickCheck or Hedgehog). This function is provided with the mapping environment between the proxy tests here and the native equivalents, and a local Generator monad expression, returning a native Generator equivalent.   09This module exports the types used in solver expressions.(c) Galois, Inc 2014-2020BSD3!Joe Hendrix  provisionalNone'(-./2>?K +what4?A runtime representation of a solver interface type. Parameter bt has kind F.9what4 Floating-point precision aliases:what4This computes the number of bits occupied by a floating-point format.<what4This data kind describes the types of floating-point formats. This consist of the standard IEEE 754-2008 binary floating point formats.Fwhat4This data kind enumerates the Crucible solver interface types, which are types that may be represented symbolically.Kwhat4+A Context where all the argument types are  instancesLwhat41Return the type of the indices for an array type.Mwhat4(Return the result type of an array type. ;what4:: JK -> JK -> <.=what4::  F -> F -> F.>what4::  F -> F.?what4:: F.@what4:: F.Awhat4:: < -> F.Bwhat4::  -> F.Cwhat4:: F.Dwhat4:: F.Ewhat4:: F.Gwhat4:: J.Hwhat4:: J.Iwhat4:: J.%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNO-FEDC@BA?>=JIHG<:;98765+,-./01234)*%&'(LMNOK Declarations for function names.(c) Galois, Inc 2014-2020BSD3!Joe Hendrix  provisionalNoneMurwhat4For our purposes, a function name is just unicode text. Individual languages may want to further restrict names.twhat4(Name of function for starting simulator.rstursutNone'(/M|what4This represents a concrete index value, and is used for creating arrays.|~}|~} TrustworthyOIwhat4 represents an error condition that should only arise due to a programming error. It will exit the program and print a message asking users to open a ticket.what4&Short name of where the error occured what4(More detailed description of the error 8Descriptions of the "features" that can occur in queries(c) Galois, Inc 2016-2020BSD3!Joe Hendrix  provisionalNoneTwhat4Allowed features represents features that the constraint solver will need to support to solve the problem.what45Indicates whether the problem uses linear arithmetic.what49Indicates whether the problem uses non-linear arithmetic.what4=Indicates whether the problem uses computable real functions.what41Indicates the problem contains integer variables.what4.Indicates whether the problem uses bitvectors.what4:Indicates whether the problem needs exists-forall support.what4Has general quantifier support.what43Indicates whether the problem uses symbolic arrays.what4*Indicates whether the problem uses structsStructs are modeled using constructors in CVC4/Z3, and tuples in Yices.what4*Indicates whether the problem uses strings2Strings have some symbolic support in CVC4 and Z3.what41Indicates whether the problem uses floating-point8Floating-point has some symbolic support in CVC4 and Z3.what4Indicates if the solver is able and configured to compute UNSAT cores.what4Indicates if the solver is able and configured to compute UNSAT assumptions.'Datatype for handling program locations(c) Galois, Inc 2014-2020BSD3!Joe Hendrix  provisionalNone567Wrwhat4=A very small type that contains a function and PC identifier.what4*A value with a source position associated.what48A source position containing filename, line, and column.what4>A binary position containing a filename and address in memory.what4Some unstructured position information that doesn't fit into the other categories.what4Parses an SExp. If the input is a string (recognized by the  readString argument), return that as an 5; if the input is a single token, return that as an .what4Parses the body of an SExp after the opening '(' has already been parsed.what4A parser for string literals what4A parser for string literals what4A parser for string literals   None  >awhat4The parsed declarations and definitions returned by "(get-model)"what4A line in the model responsewhat44This denotes an SMTLIB term over a fixed vocabulary.what4 IntTerm v denotes the SMTLIB expression v if v >= 0! and @(- `(negate v)) otherwise.what4 RatTerm r denotes the SMTLIB expression !(/ `(numerator r) `(denomator r)).what4StoreTerm a i v denotes the SMTLIB expression  (store a i v).what4IfEqTerm v c t f denotes the SMTLIB expression (ite (= v c) t f).what4 An SMT sort.what4&A named sort with the given arguments.what4!A bitvector with the given width.what4>floating point with exponent bits followed by significand bit.what4 An SMT symbolwhat4*Result of check-sat and check-sat-assumingwhat4Read the results of a  (check-sat) request.what4;This reads the model response from a "(get-model)" request.$$ None  '(/38what4This is a subtype of the type of the same name in Data.SBV.Control.what47This represents a command to be sent to the SMT solver.what4'Denotes an expression in the SMT solverwhat4Sort for SMTLIB expressionswhat4?Identifies the set of predefined sorts and operators available.what4Use the QF_BV logicwhat4&Set the logic to all supported logics.what4 Create a sort from a symbol namewhat4Booleanswhat4)Bitvectors with the given number of bits.what4Integerswhat4 Real numberswhat4 arraySort a b# denotes the set of functions from a to be b.what4Construct an expression with the given operator and list of arguments.what4Construct an expression with the given operator and single argument.what4Construct an expression with the given operator and two arguments.what4;Append a "name" to a term so that it will be printed when (get-assignment) is called.what4true Boolean termwhat4false Boolean termwhat4Complement a Booleanwhat4 implies c r is equivalent to c1 => c2 => .. cn => r.what4Conjunction of all termswhat4Disjunction of all termswhat4Disjunction of all termswhat4#Return true if all terms are equal.what42Construct a chainable term with the givne relation pairwise_app p [x1, x2, ..., xn]+ is equivalent to forall_{i,j} p x_i x_j@.what4-Asserts that each term in the list is unique.what4"Create an if-then-else expression.what4 forall vars t# denotes a predicate that holds if t* for every valuation of the variables in vars.what4 exists vars t# denotes a predicate that holds if t) for some valuation of the variables in vars.what4Create a let binding. NOTE: SMTLib2 defines this to be a "parallel" let, which means that the bound variables are NOT in scope in the right-hand sides of other bindings, even syntactically-later ones.what4!Negate an integer or real number.what40Create a numeral literal from the given integer.what42Create a literal as a real from the given integer.what4sub x1 [x2, ..., xn] with n >= 1 returns x1 minus  x2 + ... + xn.$The terms are expected to have type Int or Real.what4add [x1, x2, ..., xn] with n >= 2 returns x1 minus  x2 + ... + xn.$The terms are expected to have type Int or Real.what4add [x1, x2, ..., xn] with n >= 2 returns x1 minus  x2 + ... + xn.$The terms are expected to have type Int or Real.what4div x1 [x2, ..., xn] with n >= 1 returns x1 div  x2 * ... * xn.$The terms are expected to have type Int.what4x1 ./ [x2, ..., xn] with n >= 1 returns x1 /  x2 * ... * xn.what4 mod x1 x2 returns x1 - x2 * (x1  [x2])@.$The terms are expected to have type Int.what4abs x1 returns the absolute value of x1."The term is expected to have type Int.what40Less than or equal over a chained list of terms.le [x1, x2, ..., xn] is equivalent to  x1 <= x2  x2 <= x3  ... / x(n-1) <= xn.This is defined in the Reals, Ints, and Reals_Ints theories, and the number of elements must be at least 2.With a strict interpretation of the SMTLIB standard, the terms should be all of the same type (i.e. Int or Real"), but existing solvers appear to implicitly all mixed terms.what4'Less than over a chained list of terms.lt [x1, x2, ..., xn] is equivalent to x1 < x2  x2 < x3  ... / x(n-1) < xn.With a strict interpretation of the SMTLIB standard, the terms should be all of the same type (i.e. Int or Real"), but existing solvers appear to implicitly all mixed terms.what43Greater than or equal over a chained list of terms.ge [x1, x2, ..., xn] is equivalent to  x1 >= x2  x2 >= x3  ... / x(n-1) >= xn.With a strict interpretation of the SMTLIB standard, the terms should be all of the same type (i.e. Int or Real"), but existing solvers appear to implicitly all mixed terms.what4*Greater than over a chained list of terms.gt [x1, x2, ..., xn] is equivalent to x1 > x2  x2 > x3  ... / x(n-1) > xn.With a strict interpretation of the SMTLIB standard, the terms should be all of the same type (i.e. Int or Real"), but existing solvers appear to implicitly all mixed terms.what4Maps a term with type Int to Real.what4Returns the largest integer not larger than the given real term.what4#Returns true if this is an integer.what4arrayConst t1 t2 c$ generates an array with index type t1 and value type t2 that always returns c.+This uses the non-standard SMTLIB2 syntax ((as const (Array t1 t2)) c)9 which is supported by CVC4 and Z3 (and perhaps others).what4 select a i denotes the value of a at i.what4 store a i v& denotes the array whose valuation is v at index i and  select a j at every other index j.what4A 1-bit bitvector representing 0.what4A 1-bit bitvector representing 1.what4 bvbinary w x( constructs a bitvector term with width w equal to x  2^w. The width w must be positive.#The literal uses a binary notation.what4 bvdecimal x w( constructs a bitvector term with width w equal to x  2^w. The width w must be positive.$The literal uses a decimal notation.what4bvhexadecimal x w( constructs a bitvector term with width w equal to x  2^w. The width w" must be a positive multiple of 4.The literal uses hex notation.what4 concat x y( returns the bitvector with the bits of x followed by the bits of y.what4 extract i j x+ returns the bitvector containing the bits [j..i].what4Bitwise negation of term.what4Bitwise and of all arguments.what4$Bitwise include or of all arguments.what4(Bitvector exclusive or of all arguments.what4Negate the bitvectorwhat4Bitvector additionwhat4Bitvector subtractionwhat4Bitvector multiplicationwhat4 bvudiv x y returns floor (to_nat x / to_nat y) when y != 0.When y = 0, this returns not (from_nat 0).what4 bvurem x y returns x - y * bvudiv x y when y != 0.When y = 0, this returns  from_nat 0.what4 bvshl x y shifts the bits in x to the left by to_nat u bits.The new bits are zeros (false)what4 bvlshr x y shifts the bits in x to the right by to_nat u bits.The new bits are zeros (false)what4 bvult x y( returns a Boolean term that is true if to_nat x < to_nat y.what4 bvule x y( returns a Boolean term that is true if to_nat x <= to_nat y.Note. This is in QF_BV, but not the bitvector theory.what4 bvsle x y( returns a Boolean term that is true if to_int x <= to_int y.Note. This is in QF_BV, but not the bitvector theory.what4 bvslt x y( returns a Boolean term that is true if to_int x < to_int y.Note. This is in QF_BV, but not the bitvector theory.what4 bvuge x y( returns a Boolean term that is true if to_nat x <= to_nat y.Note. This is in QF_BV, but not the bitvector theory.what4 bvugt x y( returns a Boolean term that is true if to_nat x < to_nat y.Note. This is in QF_BV, but not the bitvector theory.what4 bvsge x y( returns a Boolean term that is true if to_int x <= to_int y.Note. This is in QF_BV, but not the bitvector theory.what4 bvsgt x y( returns a Boolean term that is true if to_int x < to_int y.Note. This is in QF_BV, but not the bitvector theory.what4 bvashr x y shifts the bits in x to the right by to_nat u bits.9The new bits are the same as the most-significant bit of x.Note. This is in QF_BV, but not the bitvector theory.what4 bvsdiv x y returns #round_to_zero (to_int x / to_int y) when y != 0.When y = 0, this returns not (from_nat 0).Note. This is in QF_BV, but not the bitvector theory.what4 bvsrem x y returns x - y * bvsdiv x y when y != 0.When y = 0, this returns  from_nat 0.Note. This is in QF_BV, but not the bitvector theory.what4bvsignExtend w x adds an additional w' bits to the most significant bits of x by sign extending x.Note. This is in QF_BV, but not the bitvector theory.what4bvzeroExtend w x adds an additional w, zero bits to the most significant bits of x.Note. This is in QF_BV, but not the bitvector theory.what4Set the logic of the SMT solverwhat4Set an option in the SMT solver6The name should not need to be prefixed with a colon."what4Set option to produce modelsThis is a widely used option so, we we have a custom command to make it.what4Request the SMT solver to exitwhat4Declare an uninterpreted sort with the given number of sort parameters.what4%Define a sort in terms of other sortswhat48Declare a constant with the given name and return types.what4Declare a function with the given name, argument types, and return type.what4Declare a function with the given name, argument types, and return type.what42Assert the predicate holds in the current context.what4Assert the predicate holds in the current context, and assign it a name so it can appear in unsatisfiable core results.what42Check the satisfiability of the current assertionswhat4Check the satisfiability of the current assertions and the additional ones in the list.what4Check satisfiability of the given atomic assumptions in the current context.NOTE! The names of variables passed to this function MUST be generated using a `declare-fun` statement, and NOT a `define-fun` statement. Thus, if you want to bind an arbitrary term, you must declare a new term and assert that it is equal to it's definition. Yes, this is quite irritating.what4/Get the model associated with the last call to  check-sat.what4?Get the values associated with the terms from the last call to  check-sat.what4Empties the assertion stack and remove all global assertions and declarations.what48Push the given number of scope frames to the SMT solver.what47Pop the given number of scope frames to the SMT solver.what4A get-info commandwhat4Name of new sortwhat4 Parameters for polymorphic sortswhat4 DefinitionSimple datastructure for capturing the result of a SAT/SMT query(c) Galois, Inc 2015-2020BSD3!Joe Hendrix  provisional Safe-Inferred8  ;Definitions related to semiring structures over base types.(c) Galois Inc, 2019-2020BSD3rdockins@galois.comNone '(/=what4The  family counts how many times a term occurs in a product. For most semirings, this is just a natural number representing the exponent. For the boolean ring of bitvectors, however, it is unit because the lattice operations are idempotent.what4$The constant values in the semiring.what4The subset of semirings that are equipped with an appropriate (order-respecting) total order.what44Data-kind representing the semirings What4 supports.what4Data-kind indicating the two flavors of bitvector semirings. The ordinary arithmetic semiring consists of addition and multiplication, and the "bits" semiring consists of bitwise xor and bitwise and.what4,Compute the base type of the given semiring.what4Compute the semiring corresponding to the given ordered semiring.what4 ::  ->  -> what4 :: what4 :: what4 :: what4 :: %%Datatype for representing names that can be communicated to solvers(c) Galois Inc, 2015-2020BSD3jhendrix@galois.comNonewhat4+This represents a name known to the solver.We have three types of symbols:The empty symbol A user symbolA system symbolA user symbol should consist of a letter followed by any combination of letters, digits, and underscore characters. It also cannot be a reserved word in Yices or SMTLIB.A system symbol should start with a letter followed by any number of letter, digit, underscore or an exclamation mark characters. It must contain at least one exclamation mark to distinguish itself from user symbols.what4This describes why a given text value was not a valid solver symbol.what4Return the empty symbol.what4This returns either a user symbol or the empty symbol if the string is empty.what4Attempts to create a user symbol from the given string. If this fails for some reason, the string is Z-encoded into a system symbol instead with the prefix "zenc!".5A finite map data structure with monoidal annotations(c) Galois Inc, 2019-2020BSD3huffman@galois.com Safe-Inferred567Zwhat4for keys present in both maps what4for subtrees only in first map what4 for subtrees only in second map *Utility functions for computing arithmetic(c) Galois, Inc 2015-2020BSD3!Joe Hendrix  provisional Safe-Inferred what4)Returns true if number is a power of two.what4Returns floor of log base 2.what4)Returns ceil of log base 2. We define  lgCeil 0 = 0what4Count trailing zeroswhat4Count leading zeroswhat4nextMultiple x y computes the next multiple m of x s.t. m >= y. E.g., nextMultiple 4 8 = 8 since 8 is a multiple of 8; nextMultiple 4 7 = 8; nextMultiple 8 6 = 8.what4nextPow2Multiple x n" returns the smallest multiple of 2^n not less than x.what4:This returns the sqrt of an integer if it is well-defined.what4Return the rational sqrt of awhat4;Evaluate a real to an integer with rounding away from zero.what4width what4value to rotate what4amount to rotate what4width what4value to rotate what4amount to rotate  (c) Galois Inc, 2019-2020BSD3huffman@galois.comNone '(/what4A value of type BVDomain w* represents a set of bitvectors of width w. Each BVDomain can represent a single contiguous interval of bitvectors that may wrap around from -1 to 0.what4#The set of all bitvectors of width w. Argument caches 2^w-1.what4;Intervals are represented by a starting value and a size. BVDInterval mask l d+ represents the set of values of the form  x mod 2^w for x such that l <= x <= l + d$. It should satisfy the invariants  0 <= l < 2^w and  0 <= d < 2^w'. The first argument caches the value 2^w-1.what4=Compute how many concrete elements are in the abstract domainwhat4Test if the given integer value is a member of the abstract domainwhat4,Check if the domain satisfies its invariantswhat40Return the bitvector mask value from this domainwhat4"Random generator for domain valueswhat4'Generate a random element from a domainwhat4Generate a random domain and an element contained in that domain.what4$Return value if this is a singleton.what4"Return unsigned bounds for domain.what4 Return signed bounds for domain.what4 Return the (lo,sz), the low bound and size of the given arithmetic interval. A value x0 is in the set defined by this domain iff  (x - lo)  w <= sz holds. Returns Nothing# if the domain contains all values.what40Return true if domains contain a common element.what4Check if all elements in one domain are less than all elements in other.what4Check if all elements in one domain are less than all elements in other.what4Represents all valueswhat43Create a bitvector domain representing the integer.what4 range w l u; returns domain containing all bitvectors formed from the w low order bits of some i in [l,u]. Note that per testBit&, the least significant bit has index 0.what4Unsafe constructor for internal use only. Caller must ensure that mask = maxUnsigned w , and that aw is non-negative.what4Create an abstract domain from an ascending list of elements. The elements are assumed to be distinct.what4Return union of two domains.what4 concat a y& returns domain where each element in a+ has been concatenated with an element in y". The most-significant bits are a%, and the least significant bits are y.what4 select i n a selects n bits starting from index i from a.what4Complement bits in range.what4Return bitwise bounds for domain (i.e. logical AND of all possible values, paired with logical OR of all possible values).what4unknowns lo hi returns a bitmask representing the set of bit positions whose values are not constant throughout the range lo..hi.what4 fillright x rounds up x to the nearest 2^n-1.what4Check that a domain is proper, and that the given value is a member(c) Galois Inc, 2020BSD3huffman@galois.comNone '(/what4A bitwise interval domain, defined via a bitwise upper and lower bound. The ordering used here to construct the interval is the pointwise ordering on bits. In particular x [= y iff x .|. y == y, and a value x# is in the set defined by the pair (lo,hi) just when lo [= x && x [= hi.what4BVDBitInterval mask lo hi. mask caches the value of 2^w - 1what4+Test if the domain satisfies its invariantswhat4Test if the given integer value is a member of the abstract domainwhat4=Compute how many concrete elements are in the abstract domainwhat40Return the bitvector mask value from this domainwhat4Random generator for domain values. We always generate nonempty domain values.what4Generate a random nonempty domain and an element contained in that domain.what4$Unsafe constructor for internal use.what46Construct a domain from bitwise lower and upper boundswhat4Bitwise lower and upper boundswhat4Test if this domain contains a single value, and return it if sowhat4Returns true iff there is at least on element in this bitwise domain.what4/Return a domain containing just the given valuewhat4/Bitwise domain containing every bitvector valuewhat46Returns true iff the domains have some value in commonwhat4 concat a y& returns domain where each element in a+ has been concatenated with an element in y". The most-significant bits are a%, and the least significant bits are y.what4 select i n a selects n bits starting from index i from a.what4Check that a domain is proper, and that the given value is a member::(c) Galois Inc, 2019-2020BSD3huffman@galois.comNone '(/ what4A value of type BVDomain w* represents a set of bitvectors of width w. This is an alternate representation of the bitwise domain values, optimized to compute XOR operations.what4BVDXor mask hi unknown% represents a set of values where hi is a bitwise high bound, and unknown? represents the bits whose values are not known. The value mask caches the value 2^w-1.what4+Test if the domain satisfies its invariantswhat4Test if the given integer value is a member of the abstract domainwhat40Return the bitvector mask value from this domainwhat46Construct a domain from bitwise lower and upper boundswhat4$Unsafe constructor for internal use.what4Bitwise lower and upper boundswhat4Test if this domain contains a single value, and return it if sowhat4Random generator for domain values. We always generate nonempty domain values.what4Generate a random nonempty domain and an element contained in that domain.what4/Return a domain containing just the given valuewhat4Check that a domain is proper, and that the given value is a memberAbstract domains for bitvectors(c) Galois Inc, 2019-2020BSD3huffman@galois.comNone &'(/zwhat4A value of type  w* represents a set of bitvectors of width w. A BVDomain represents either an arithmetic interval, or a bitwise interval.what4+Test if the domain satisfies its invariantswhat4Test if the given integer value is a member of the abstract domainwhat4=Compute how many concrete elements are in the abstract domainwhat4!Generate a random nonempty domainwhat4Generate a random element from a domain, which is assumed to be nonemptywhat4Generate a random nonempty domain and an element contained in that domain.what4$Return value if this is a singleton.what4Precondition:  x <= lomask'. Find the (arithmetically) smallest z above x which is bitwise above lomask%. In other words find the smallest z such that x <= z and lomask .|. z == z.what4Precondition: lomask <= x <= himask and lomask .|. himask == himask&. Find the (arithmetically) smallest z above x which is bitwise between lomask and himask%. In other words, find the smallest z such that x <= z and lomask .|. z = z and z .|. himask == himask.what40Return true if domains contain a common element.what4Check if all elements in one domain are less than all elements in other.what4Check if all elements in one domain are less than all elements in other.what4Return Just if every bitvector in the domain has the same bit at the given index.what4Represents all valueswhat43Create a bitvector domain representing the integer.what4 range w l u; returns domain containing all bitvectors formed from the w low order bits of some i in [l,u]. Note that per testBit&, the least significant bit has index 0.what4Create an abstract domain from an ascending list of elements. The elements are assumed to be distinct.what4Return union of two domains.what4 concat a y& returns domain where each element in a+ has been concatenated with an element in y". The most-significant bits are a%, and the least significant bits are y.what4 select i n a selects n bits starting from index i from a.what4Complement bits in range.what4bvmask3, based on the width of the bitvectors in question what4 xwhat4 lomaskwhat4bvmask3, based on the width of the bitvectors in question what4 xwhat4 lomaskwhat4 himaskwhat41Index of bit (least-significant bit has index 0) Provides a complex representation that is more generic than Data.Complex.(c) Galois, Inc 2014-2020BSD3!Joe Hendrix  provisional Safe-Inferred '(5678ɷwhat4&A complex pair over an arbitrary type.what4Returns square of magnitude.what4 Sqrt functionwhat47Square-root function defined for non-negative values a.6 Safe-Inferred"Provides functions for finding an executable, and expanding a path with referenced to environment variables.(c) Galois, Inc 2013-2020BSD3!Joe Hendrix  provisional Safe-Inferredˆwhat4!Find an executable from a string.what4Path to expandNone '(+89 what46Rounding modes for IEEE-754 floating point operations.what4Round to nearest even.what4Round to nearest away.what4Round toward plus Infinity.what4Round toward minus Infinity.what4Round toward zero.what4=Make LibBF options for the given precision and rounding mode.what4Make a floating point number from an integer, using the given rounding modewhat4Make a floating point number from a rational, using the given rounding modewhat4;Convert a floating point number to a rational, if possible.what4;Convert a floating point number to an integer, if possible.Nonewhat4Wrapper to help with reading from another process's standard out and stderr.We want to be able to read from another process's stderr and stdout without causing the process to stall because stdout or stderr becomes full. This data type will read from either of the handles, and buffer as much data as needed in the queue. It then provides a line-based method for reading that data as strict bytestrings. what48Create a new handle reader for reading the given handle.what42Stop the handle reader; cannot be used afterwards.what4 Safe-Inferred&what4Return the empty mapwhat4Find largest element that is less than or equal to key (if any).what43Find largest element that is at least key (if any).what46Find less than element that is less than key (if any).what46Find less than element that is less than key (if any).what45Create a map from a list of keys in descending order.$Typeclass for monads generalizing ST(c) Galois, Inc 2014-2020BSD3!Joe Hendrix  provisional Safe-Inferred>;(c) Galois, Inc. 2020BSD3!Joe Hendrix None'(what41This provides a GADT instance used to indicate a F must have value D. IO stream utilities(c) Galois, Inc 2013-2020BSD3!Joe Hendrix  provisionalNonewhat4.Write from input stream to a logging function.what4Logging function!None 2;what4This method parses configuration files describing the upper and lower bounds of solver versions we expect to work correctly with What4. See the file "solverBounds.config" for examples of how such bounds are specified.  "-Utility definitions for wide (2-byte) strings(c) Galois, Inc 2019-2020BSD3!Rob Dockins  provisional Safe-Inferredv what4A string of Word16 values, encoded as a bytestring in little endian (LE) order.We maintain the invariant that Word16Strings are represented by an even number of bytes.what4 Generate a  Word16String from a bytestring where the 16bit words are encoded as two bytes in little-endian order.PRECONDITION: the input bytestring must have a length which is a multiple of 2.what4/Return the underlying little endian bytestring.what4Return the empty stringwhat46Compute the string containing just the given characterwhat4!Test if the given string is emptywhat4 Retrive the nth character of the string. Out of bounds accesses will cause an error.what4Find the first index (if it exists) where the first string appears as a substring in the secondwhat4Returns true if the first string appears somewhere in the second string.#Utility definitions for strings(c) Galois, Inc 2019-2020BSD3!Rob Dockins  provisionalNone'(/>what4Index of first occurrence of second string in first one starting at the position specified by the third argument. stringLitIndexOf s t k, with  0 <= k <= |s|/ is the position of the first occurrence of t in s at or after position k, if any. Otherwise, it is -1. Note that the result is k whenever k is within the range [0, |s|] and t is empty.$(Abstract domains for term simplification(c) Galois Inc, 2015-2020BSD3jhendrix@galois.comNone./5>?xwhat4*Take the union of the two abstract values.what4Returns true if the abstract values could contain a common concrete value.what4Check equality on two abstract values. Return true or false if we can definitively determine the equality of the two elements, and nothing otherwise.what47A utility class for values that contain abstract valueswhat45An abstract value represents a disjoint st of values.what4The string abstract domain tracks an interval range for the length of the string.what4,The length of the string falls in this rangewhat45Describes a range of values in a totally ordered set.what4+Indicates that range denotes a single valuewhat4Indicates that the number is somewhere between the given upper and lower bound.what4"A lower or upper bound on a value.what4Compute an abstract range for integer division. We are using the SMTLib division operation, where the division is floor when the divisor is positive and ceiling when the divisor is negative. We compute the ranges assuming that division by 0 doesn't happen, and we are allowed to return nonsense ranges for these cases.what4"Multiply a range by a scalar valuewhat4Multiply two ranges together.what4Return lower bound of range.what4Return upper bound of range.what42Compute the smallest range containing both ranges.what4Return maybe Boolean if range is equal, is not equal, or indeterminant.what4 Defines a unbounded value range.what4 Defines a unbounded value range.what42Defines a value range containing a single element.what4*Define a value range with the given boundswhat4(Check if range is just a single element.what49Range accepting everything between lower and upper bound.what4Add two real abstract values.what4?#what4A product of semiring values.what47Runtime representation of the semiring for this productwhat4A weighted sum of semiring values. Mathematically, this represents an affine operation on the underlying expressions.what44Runtime representation of the semiring for this sum.what41Retrieve the constant addend of the weighted sum.what4.Attempt to parse a weighted sum as a constant.what45Return true if a weighted sum is equal to constant 0.what4Attempt to parse a weighted sum as a single expression with a coefficient and offset. asAffineVar w = Just (c,r,o) when denotation(w) = c*r + o.what4Attempt to parse weighted sum as a single expression with a coefficient. asWeightedVar w = Just (c,r) when denotation(w) = c*r.what4;Attempt to parse a weighted sum as a single expression. asVar w = Just r when denotation(w) = rwhat4/Create a sum from a constant coefficient value.what4+Traverse the expressions in a weighted sum.what4,Traverse the coefficients in a weighted sum.what4&Traverse the expressions in a product.what4)This returns a variable times a constant.what4:Create a weighted sum corresponding to the given variable.what4Add two sums, collecting terms as necessary and deleting terms whose coefficients sum to 0.what4;Create a weighted sum that represents the sum of two terms.what4Add a variable to the sum.what4Add a constant to the sum.what4)Multiply a sum by a constant coefficient.what4:Produce a weighted sum from a list of terms and an offset.what4Apply update functions to the terms and coefficients of a weighted sum.what4Evaluate a sum given interpretations of addition, scalar multiplication, and a constant. This evaluation is threaded through a monad. The addition function is associated to the left, as in foldlM.what4Evaluate a sum given interpretations of addition, scalar multiplication, and a constant rational.what4Reduce a weighted sum of integers modulo a concrete integer. This reduces each of the coefficients modulo the given integer, removing any that are congruent to 0; the offset value is also reduced.what4Given two weighted sums x and y, this returns a triple  (z,x',y') where  x = z + x' and  y = z + y' and z! contains the "common" parts of x and y. We only extract common terms when both terms occur with the same coefficient in each sum.This is primarily used to simplify if-then-else expressions to preserve shared subterms.what4;Returns true if the product is trivial (contains no terms).what46If the product consists of exactly on term, return it.what4Returns true if the product contains at least on occurrence of the given term.what45Produce a product representing the single given term.what4?Multiply two products, collecting terms and adding occurrences.what4Evaluate a product, given a function representing multiplication and a function to evaluate terms.what4Evaluate a product, given a function representing multiplication and a function to evaluate terms, where both functions are threaded through a monad.what4The annotation type used for the annotated map for products. It consists of the hash value and the abstract domain representation of type d for each submap. NOTE! that the multiplication operation on abstract values is not always associative. This, however, is acceptable because all associative groupings lead to sound (but perhaps not best) approximate values.what4Addition function what4Scalar multiply what4Constant evaluation what4Addition function what4Scalar multiply what4Constant evaluation what4The sum to reduce what4The modulus, must not be 0 what4multiplication evalation what4term evaluation what4multiplication evalation what4term evaluation %%&Datastructure for representing a sequence of updates to an SMT array(c) Galois Inc, 2019-2020BSD3rdockins@galois.comNone'(/'Concrete values of base types(c) Galois, Inc 2018-2020BSD3!Rob Dockins  provisionalNone'(-./2:>?n what4?A data type for representing the concrete values of base types. what45Compute the type representative for a concrete value. what4Pretty-print a concrete value  (9Declares attributes for simulator configuration settings.(c) Galois, Inc 2015-2020BSD3!Rob Dockins  provisionalNone '(-./>8A: what4A  ConfigValue? bundles together the name of an option with its current value. what4A utility class for making working with option settings easier. The tp argument is a BaseType , and the a, argument is an associcated Haskell type. what4-Return the current value of the option, as a Maybe value. what4Attempt to set the value of an option. Return any errors or warnings. what4Set the value of an option. Return any generated warnings. Throws an OptSetFailure exception if a validation error occurs. what4Get the current value of an option. Throw an exception if the option is not currently set. what4The main configuration datatype. It consists of an MVar containing the actual configuration data. what4A  ConfigDesc describes a configuration option before it is installed into a Config object. It consists of a  ConfigOption name for the option, an  OptionStyle describing the sort of option it is, and an optional help message describing the semantics of this option. what4 An inclusive or exclusive bound. what4An option defines some metadata about how a configuration option behaves. It contains a base type representation, which defines the runtime type that is expected for setting and querying this option at runtime. what4'base type representation of this option what4An operation for validating new option values. This action may also be used to take actions whenever an option setting is changed. NOTE! the onset action should not attempt to look up the values of other configuration settings, or deadlock may occur.The first argument is the current value of the option (if any). The second argument is the new value that is being set. If the validation fails, the operation should return a result describing why validation failed. Optionally, warnings may also be returned. what4Documentation for the option to be displayed in the event a user asks for information about this option. This message should contain information relevant to all options in this style (e.g., its type and range of expected values), not necessarily information about a specific option. what42This gives a default value for the option, if set. what4An  OptionSetting gives the direct ability to query or set the current value of an option. The  getOption field is an action that, when executed, fetches the current value of the option, if it is set. The  setOption method attempts to set the value of the option. If the associated  opt_onset validation method rejects the option, it will retain its previous value; otherwise it will be set to the given value. In either case, the generated OptionSetResult will be returned. what4When setting the value of an option, a validation function is called (as defined by the associated  OptionStyle3). The result of the validation function is an OptionSetResult. If the option value given is invalid for some reason, an error should be returned. Additionally, warning messages may be returned, which will be passed through to the eventual call site attempting to alter the option setting. what4A Haskell-land wrapper around the name of a configuration option. Developers are encouraged to define and use   values to avoid two classes of errors: typos in configuration option names; and dynamic type-cast failures. Both classes of errors can be lifted to statically-checkable failures (missing symbols and type-checking, respectively) by consistently using   values.3The following example indicates the suggested usage  asdfFrob :: ConfigOption BaseRealType asdfFrob = configOption BaseRealRepr "asdf.frob" asdfMaxBound :: ConfigOption BaseIntegerType asdfMaxBound = configOption BaseIntegerRepr "asdf.max_bound" what4 Construct a   from a string name. Idiomatic usage is to define a single top-level   value in the module where the option is defined to consistently fix its name and type for all subsequent uses. what4>Get the individual dot-separated segments of an option's name. what44Reconstruct the original string name of this option. what44Reconstruct the original string name of this option. what4-Retrieve the run-time type representation of tp. what47Accept the new option value with no errors or warnings. what42Reject the new option value with an error message. what4Standard option style for boolean-valued configuration options what4;Standard option style for real-valued configuration options what4?Standard option style for integral-valued configuration options what4Option style for real-valued options with upper and lower bounds what47Option style for real-valued options with a lower bound what48Option style for real-valued options with an upper bound what4Option style for integer-valued options with upper and lower bounds what4:Option style for integer-valued options with a lower bound what4;Option style for integer-valued options with an upper bound what4A configuration style for options that must be one of a fixed set of text values what4A configuration syle for options that must be one of a fixed set of text values. Associated with each string is a validation/callback action that will be run whenever the named string option is selected. what4Used as a wrapper for an option that has been deprecated. If the option is actually set (as opposed to just using the default value) then this will emit an OptionSetResult warning that time, optionally mentioning the replacement option (if specified).There are three cases of deprecation: 1. Removing an option that no longer applies 2. Changing the name or heirarchical position of an option. 3. #2 and also changing the type. 4. Replacing an option by multiple new options (e.g. split url option into hostname and port options)In the case of #1, the option will presumably be ignored by the code and the warnings are provided to allow the user to clean the option from their configurations.In the case of #2, the old option and the new option will share the same value storage: changes to one can be seen via the other and vice versa. The code can be switched over to reference the new option entirely, and user configurations setting the old option will still work until they have been updated and the definition of the old option is removed entirely.NOTE: in order to support #2, the newer option should be declared (via $) *before* the option it deprecates.In the case of #3, it is not possible to share storage space, so during the deprecation period, the code using the option config value must check both locations and decide which value to utilize.Case 4 is an enhanced form of 3 and #2, and is generally treated as #3, but adds the consideration that deprecation warnings will need to advise about multiple new options. The inverse of #4 (multiple options being combined to a single newer option) is just treated as separate deprecations.NOTE: in order to support #4, the newer options should all be declared (via &) *before* the options they deprecate.Nested deprecations are valid, and replacement warnings are automatically transitive to the newest options.Any user-supplied value for the old option will result in warnings emitted to the OptionSetResult for all four cases. Code should ensure that these warnings are appropriately communicated to the user to allow configuration updates to occur.Note that for 1 and 2, the overhead burden of continuing to define the deprecated option is very small, so actual removal of the older config can be delayed indefinitely. what4A configuration style for options that are expected to be paths to an executable image. Configuration options with this style generate a warning message if set to a value that cannot be resolved to an absolute path to an executable file in the current OS environment. what42The most general method for constructing a normal  . what4Construct an option using a default style with a given initial value what4Construct an option using a default style with a given initial value. Also provide a validation function to check new values as they are set. what4Construct an option using a default style with no initial value. what4Construct an option using a default style with no initial value. Also provide a validation function to check new values as they are set. what4The copyOpt creates a duplicate ConfigDesc under a different name. This is typically used to taking a common operation and modify the prefix to apply it to a more specialized role (e.g. solver.strict_parsing --> solver.z3.strict_parsing). The style and help text of the input ConfigDesc are preserved, but any deprecation is discarded. what4Construct a new configuration from the given configuration descriptions. what4:Extend an existing configuration with new options. An   exception will be raised if any of the given options clash with options that already exists. what4Verbosity of the simulator. This option controls how much informational and debugging output is generated. 0 yields low information output; 5 is extremely chatty. what4Return an operation that will consult the current value of the verbosity option, and will print a string to the given Handle if the provided int is smaller than the current verbosity setting. what4 Throw an exception if the given OptionSetResult indidcates an error. Otherwise, return any generated warnings. what4Given a unicode text value, set the named option to that value or generate an OptSetFailure exception if the option is not a unicode text valued option. what4Given an integer value, set the named option to that value or generate an OptSetFailure exception if the option is not an integer valued option. what4Given a boolean value, set the named option to that value or generate an OptSetFailure exception if the option is not a boolean valued option. what4Given a  ConfigOption name, produce an  OptionSetting> object for accessing and setting the value of that option.An exception is thrown if the named option cannot be found the Config& object, or if a type mismatch occurs. what4Given a text name, produce an  OptionSetting> object for accessing and setting the value of that option.;An exception is thrown if the named option cannot be found. what4Given the name of a subtree, return all the currently-set configurtion values in that subtree.If the subtree name is empty, the entire tree will be traversed. what4Given the name of a subtree, compute help text for all the options available in that subtree.If the subtree name is empty, the entire tree will be traversed. what4*Fixes the name and the type of this optionwhat4Define the style of this optionwhat4 Help textwhat4A default value for this option what4*Fixes the name and the type of this optionwhat4Default value for the optionwhat4/An informational message describing this option what4*Fixes the name and the type of this optionwhat4Default value for the optionwhat4Validation function. Return `Just err` if the value to set is not valid.what4/An informational message describing this option what4*Fixes the name and the type of this optionwhat4/An informational message describing this option what4+Fixes the name and the type of this option what4Validation function. Return `Just err` if the value to set is not valid. what40An informational message describing this option what4Initial value for the   optionwhat4Option descriptions to install )None '(/= what4Utility function that runs a solver specified by the given config setting within a context. Errors can then be attributed to the solver. what4This runs a given external binary, providing the process handle and handles to input and output to the action. It takes care to terminate the process if any exception is thrown by the action. what4Close the connected process pipes and wait for the process to exit what40Start a process connected to this one via pipes. what4 Filtering function for use with  or  that filters out asynch exceptions so they are rethrown instead of captured what4Path to processwhat4Arguments to processwhat4Working directory if any.what4Action to run with process; should wait for process to terminate before returning. what4Path to executable what4Command-line arguments what4Optional working directory what4>process stdin, process stdout, process stderr, process handle   *.Main interface for constructing What4 formulae(c) Galois, Inc 2014-2020BSD3!Joe Hendrix None'(-./8>?7 what4;Statistics gathered on a running expression builder. See  . what4;The number of times an expression node has been allocated. what4The number of non-linear operations, such as multiplications, that have occurred. what4This provides an interface for converting between Haskell values and a solver representation. what4This extends the interface for building expressions with operations for creating new symbolic constants and functions. what40Create a fresh top-level uninterpreted constant. what4Create a fresh latch variable. what4Create a fresh bitvector value with optional lower and upper bounds (which bound the unsigned value of the bitvector). If provided, the bounds are inclusive. If inconsistent or out-of-range bounds are given, an  InvalidRange exception will be thrown. what4Create a fresh bitvector value with optional lower and upper bounds (which bound the signed value of the bitvector). If provided, the bounds are inclusive. If inconsistent or out-of-range bounds are given, an InvalidRange exception will be thrown. what4Create a fresh integer constant with optional lower and upper bounds. If provided, the bounds are inclusive. If inconsistent bounds are given, an InvalidRange exception will be thrown. what4Create a fresh real constant with optional lower and upper bounds. If provided, the bounds are inclusive. If inconsistent bounds are given, an InvalidRange exception will be thrown. what4Creates a bound variable.This will be treated as a free constant when appearing inside asserted expressions. These are intended to be bound using quantifiers or symbolic functions. what48Return an expression that references the bound variable. what4forallPred sym v e' returns an expression that represents  forall v . e. Throws a user error if bound var has already been used in a quantifier. what4existsPred sym v e' returns an expression that represents  exists v . e. Throws a user error if bound var has already been used in a quantifier. what4Return a function defined by an expression over bound variables. The predicate argument allows the user to specify when an application of the function should be unfolded and evaluated, e.g. to perform constant folding. what4Return a function defined by Haskell computation over symbolic expressions. what4$Create a new uninterpreted function. what40Apply a set of arguments to a symbolic function. what4This exception is thrown if the user requests to make a bounded variable, but gives incoherent or out-of-range bounds. what47Describes when we unfold the body of defined functions. what4What4 will not unfold the body of functions when applied to arguments what4The function will be unfolded into its definition whenever it is applied to arguments what4The function will be unfolded into its definition only if all the provided arguments are concrete. what4A class for extracting type representatives from symbolic functions what4%Get the argument types of a function. what4"Get the return type of a function. what45A function that can be applied to symbolic arguments.-This type is used by some methods in classes   and  . what4>This class allows the simulator to build symbolic expressions.-Methods of this class refer to type families   sym and   sym.Note: Some methods in this class represent operations that are partial functions on their domain (e.g., division by 0). Such functions will have documentation strings indicating that they are undefined under some conditions. When partial functions are applied outside their defined domains, they will silently produce an unspecified value of the expected type. The unspecified value returned as the result of an undefined function is _not_ guaranteed to be equivalant to a free constant, and no guarantees are made about what properties such values will satisfy. what4Retrieve the configuration object corresponding to this solver interface. what4Install an action that will be invoked before and after calls to backend solvers. This action is primarily intended to be used for logging/profiling/debugging purposes. Passing & to this function disables logging. what4Get the currently-installed solver log listener, if one has been installed. what4Provide the given event to the currently installed solver log listener, if any. what4Get statistics on execution from the initialization of the symbolic interface to this point. May return zeros if gathering statistics isn't supported. what4;Get current location of program for term creation purposes. what4;Set current location of program for term creation purposes. what4Return true if two expressions are equal. The default implementation dispatches  ,  ,  ,  ,  ,  ,  , or  , depending on the type. what4Take the if-then-else of two expressions. The default implementation dispatches  ,  ,  ,  ,  ,  ,  , or  , depending on the type. what4Given a symbolic expression, annotate it with a unique identifier that can be used to maintain a connection with the given term. The   is intended to be used as the key in a hash table or map to additional data can be maintained alongside the terms. The returned   has the same semantics as the argument, but has embedded in it the  > value so that it can be used later during term traversals.Note, the returned annotation is not necessarily fresh; if an already-annotated term is passed in, the same annotation value will be returned. what4(Project an annotation from an expression!It should be the case that using   on a term returned by  " returns the same annotation that   did. what4Constant true predicate what4Constant false predicate what4Boolean negation what4Boolean conjunction what4Boolean disjunction what4Boolean implication what4Exclusive-or operation what4Equality of boolean values what4If-then-else on a predicate. what4Create an integer literal. what4Negate an integer. what4Add two integers. what4"Subtract one integer from another. what4 Multiply one integer by another. what4)Return the minimum value of two integers. what4)Return the maximum value of two integers. what4!If-then-else applied to integers. what4Integer equality. what4Integer less-than-or-equal. what4Integer less-than. what4)Compute the absolute value of an integer. what4 intDiv x y" computes the integer division of x by y. This division is interpreted the same way as the SMT-Lib integer theory, which states that div and mod are the unique Euclidean division operations satisfying the following for all y /= 0: y * (div x y) + (mod x y) == x  0 <= mod x y < abs y The value of  intDiv x y is undefined when y = 0.Integer division requires nonlinear support whenever the divisor is not a constant.Note: div x y is  floor (x/y) when y' is positive (regardless of sign of x) and  ceiling (x/y) when y is negative. This is neither of the more common "round toward zero" nor "round toward -inf" definitions.Some useful theorems that are true of this division/modulus pair: 'mod x y == mod x (- y) == mod x (abs y) div x (-y) == -(div x y) what4 intMod x y! computes the integer modulus of x by y. See   for more details. The value of  intMod x y is undefined when y = 0.Integer modulus requires nonlinear support whenever the divisor is not a constant. what4intDivisible x k is true whenever x8 is an integer divisible by the known natural number k. In other words `divisible x k` holds if there exists an integer z such that `x = k*z`. what42Create a bitvector with the given width and value. what4Concatenate two bitvectors. what4&Select a subsequence from a bitvector. what42's complement negation. what4Add two bitvectors. what4$Subtract one bitvector from another. what4"Multiply one bitvector by another. what4Unsigned bitvector division.The result of  bvUdiv x y is undefined when y' is zero, but is otherwise equal to floor( x / y ). what4Unsigned bitvector remainder.The result of  bvUrem x y is undefined when y' is zero, but is otherwise equal to x - (bvUdiv x y) * y. what4Returns true if the corresponding bit in the bitvector is set. what4%Return true if bitvector is negative. what4#If-then-else applied to bitvectors. what4$Return true if bitvectors are equal. what4'Return true if bitvectors are distinct. what4Unsigned less-than. what4Unsigned less-than-or-equal. what4Unsigned greater-than-or-equal. what4Unsigned greater-than. what4Signed less-than. what4Signed greater-than. what4Signed less-than-or-equal. what4Signed greater-than-or-equal. what40returns true if the given bitvector is non-zero. what4>Left shift. The shift amount is treated as an unsigned value. what4Logical right shift. The shift amount is treated as an unsigned value. what4Arithmetic right shift. The shift amount is treated as an unsigned value. what4Rotate left. The rotate amount is treated as an unsigned value. what4Rotate right. The rotate amount is treated as an unsigned value. what4Zero-extend a bitvector. what4Sign-extend a bitvector. what4Truncate a bitvector. what4Bitwise logical and. what4Bitwise logical or. what4Bitwise logical exclusive or. what4Bitwise complement. what4bvSet sym v i p returns a bitvector v' where bit i of v' is set to p7, and the bits at the other indices are the same as in v. what4bvFill sym w p returns a bitvector w?-bits long where every bit is given by the boolean value of p. what4Return the bitvector of the desired width with all 0 bits; this is the minimum unsigned integer. what4Return the bitvector of the desired width with all bits set; this is the maximum unsigned integer. what4Return the bitvector representing the largest 2's complement signed integer of the given width. This consists of all bits set except the MSB. what4Return the bitvector representing the smallest 2's complement signed integer of the given width. This consists of all 0 bits except the MSB, which is set. what4)Return the number of 1 bits in the input. what4Return the number of consecutive 0 bits in the input, starting from the most significant bit position. If the input is zero, all bits are counted as leading. what4Return the number of consecutive 0 bits in the input, starting from the least significant bit position. If the input is zero, all bits are counted as leading. what4Unsigned add with overflow bit. what4Signed add with overflow bit. Overflow is true if positive + positive = negative, or if negative + negative = positive. what4?Unsigned subtract with overflow bit. Overflow is true if x < y. what4Signed subtract with overflow bit. Overflow is true if positive - negative = negative, or if negative - positive = positive. what4Compute the carry-less multiply of the two input bitvectors. This operation is essentially the same as a standard multiply, except that the partial addends are simply XOR'd together instead of using a standard adder. This operation is useful for computing on GF(2^n) polynomials. what4unsignedWideMultiplyBV sym x y multiplies two unsigned w bit numbers x and y.%It returns a pair containing the top w+ bits as the first element, and the lower w bits as the second element. what4>Compute the unsigned multiply of two values with overflow bit. what4signedWideMultiplyBV sym x y multiplies two signed w bit numbers x and y.%It returns a pair containing the top w+ bits as the first element, and the lower w bits as the second element. what4= on two real numbers. what4Check > on two real numbers. what4If-then-else on real numbers. what4'Return the minimum of two real numbers. what4(Return the maxmimum of two real numbers. what4Negate a real number. what4Add two real numbers. what4Multiply two real numbers. what4Subtract one real from another. what4 realSq sym x returns x * x. what4realDiv sym x y returns term equivalent to x/y.The result is undefined when y is zero. what4 realMod x y returns the value of x - y * floor(x / y) when y is not zero and x when y is zero. what4 y.This test usually does NOT correspond to the not-equal tests found in programming languages. Instead, one generally takes the logical negation of the   test. what4Check if two floating point numbers are "unordered". This happens precicely when one or both of the inputs is NaN. what4Check IEEE-754 <= on two floating point numbers.1NOTE! This test returns false if either value is NaN; in particular NaN is not less-than-or-equal-to any other value! Moreover, positive and negative 0 are considered equal, despite having different bit patterns. what4Check IEEE-754 < on two floating point numbers.1NOTE! This test returns false if either value is NaN; in particular NaN is not less-than any other value! Moreover, positive and negative 0 are considered equal, despite having different bit patterns. what4Check IEEE-754 >= on two floating point numbers.1NOTE! This test returns false if either value is NaN; in particular NaN is not greater-than-or-equal-to any other value! Moreover, positive and negative 0 are considered equal, despite having different bit patterns. what4Check IEEE-754 > on two floating point numbers.1NOTE! This test returns false if either value is NaN; in particular NaN is not greater-than any other value! Moreover, positive and negative 0 are considered equal, despite having different bit patterns. what4&Test if a floating-point value is NaN. what4Test if a floating-point value is (positive or negative) infinity. what4>Test if a floating-point value is (positive or negative) zero. what4Test if a floating-point value is positive. NOTE! NaN is considered neither positive nor negative. what4Test if a floating-point value is negative. NOTE! NaN is considered neither positive nor negative. what4,Test if a floating-point value is subnormal. what4)Test if a floating-point value is normal. what4'If-then-else on floating point numbers. what40Change the precision of a floating point number. what43Round a floating point number to an integral value. what4Convert from binary representation in IEEE 754-2008 format to floating point. what4Convert from floating point from to the binary representation in IEEE 754-2008 format.NOTE! NaN has multiple representations, i.e. all bit patterns where the exponent is 0b1..1 and the significant is not 0b0..0. This functions returns the representation of positive "quiet" NaN,, i.e. the bit pattern where the sign is 0b0, the exponent is 0b1..1, and the significant is 0b10..0. what48Convert a unsigned bitvector to a floating point number. what46Convert a signed bitvector to a floating point number. what41Convert a real number to a floating point number. what48Convert a floating point number to a unsigned bitvector. what46Convert a floating point number to a signed bitvector. what41Convert a floating point number to a real number. what4,Create a complex from cartesian coordinates. what4 getRealPart x returns the real part of x. what4 getImagPart x returns the imaginary part of x. what4:Convert a complex number into the real and imaginary part. what4"Create a constant complex literal. what4#Create a complex from a real value. what4If-then-else on complex values. what4Negate a complex number. what4!Add two complex numbers together. what4)Subtract one complex number from another. what4&Multiply two complex numbers together. what4*Compute the magnitude of a complex number. what45Return the principal square root of a complex number. what4!Compute sine of a complex number. what4#Compute cosine of a complex number. what4&Compute tangent of a complex number.  cplxTan x is undefined when  cplxCos x is 0, which occurs only along the real line in the same conditions where  realCos x is 0. what4 hypotCplx x y returns sqrt(abs(x)^2 + abs(y)^2). what4 roundCplx x rounds complex number to nearest integer. Numbers with a fractional part of 0.5 are rounded away from 0. Imaginary and real parts are rounded independently. what4 cplxFloor x rounds to nearest integer less than or equal to x. Imaginary and real parts are rounded independently. what4 cplxCeil x rounds to nearest integer greater than or equal to x. Imaginary and real parts are rounded independently. what4 conjReal x, returns the complex conjugate of the input. what4(Returns exponential of a complex number. what4&Check equality of two complex numbers. what4*Check non-equality of two complex numbers. what4Symbolic natural numbers. what4This datatype describes events that involve interacting with solvers. A  SolverEvent1 will be provided to the action installed via setSolverLogListener) whenever an interesting event occurs. what4This class provides operations for recognizing when symbolic expressions represent concrete values, extracting the type from an expression, and for providing pretty-printed representations of an expression. what4"Evaluate if predicate is constant. what4-Return integer if this is a constant integer. what46Return any bounding information we have about the term what4,Return rational if this is a constant value. what41Return floating-point value if this is a constant what46Return any bounding information we have about the term what4+Return complex if this is a constant value. what43Return a bitvector if this is a constant bitvector. what4If we have bounds information about the term, return unsigned upper and lower bounds as integers what4If we have bounds information about the term, return signed upper and lower bounds as integers what4If this expression syntactically represents an "affine" form, return its components. When asAffineVar x = Just (c,r,o), then we have  x == c*r + o. what44Return the string value if this is a constant string what4Return the representation of the string info for a string-typed term. what4Return the unique element value if this is a constant array, such as one made with  . what46Return the struct fields if this is a concrete struct. what4Get type of expression. what4Get the width of a bitvector what40Get the precision of a floating-point expression what49Print a sym expression for debugging or display purposes. what4Type used to uniquely identify expressions that have been annotated. what46Type of bound variable associated with symbolic state.+This type is used by some methods in class  . what4The class for expressions. what4Symbolic strings. what4Symbolic bitvectors. what4Symbolic arrays. what4Symbolic structures. what4Symbolic complex numbers. what4 Symbolic floating point numbers. what4Symbolic real numbers. what4Symbolic integers. what4(Symbolic boolean values, AKA predicates. what4%Perform an ite on a predicate lazily. what40Return nat if this is a constant natural number. what4A natural number literal. what4Add two natural numbers. what4!Subtract one number from another.?The result is 0 if the subtraction would otherwise be negative. what4Multiply one number by another. what4  sym x y performs division on naturals.The result is undefined if y equals 0.  and   satisfy the property that given , d <- natDiv sym x y m <- natMod sym x y and y > 0, we have that  y * d + m = x and m < y. what4  sym x y returns x mod y.See   for a description of the properties the return value is expected to satisfy. what4(If-then-else applied to natural numbers. what4'Equality predicate for natural numbers. what4  sym x y returns true if x <= y. what4  sym x y returns true if x < y. what4'Convert a natural number to an integer. what47Convert the unsigned value of a bitvector to a natural. what4*Convert a natural number to a real number. what4'Convert an integer to a natural number.2For negative integers, the result is clamped to 0. what4*Convert a real number to a natural number.The result is undefined if the given real number does not represent a natural number. what4Create a fresh natural number constant with optional lower and upper bounds. If provided, the bounds are inclusive. If inconsistent bounds are given, an InvalidRange exception will be thrown. what4'Create a fresh natural number constant. what4Join a Vector of smaller bitvectors. The vector is interpreted in big endian order; that is, with most significant bitvector first. what4Split a bitvector to a Vector of smaller bitvectors. The returned vector is in big endian order; that is, with most significant bitvector first. what4"Implement LLVM's "bswap" intrinsicSee < 8https://llvm.org/docs/LangRef.html#llvm-bswap-intrinsics the LLVM bswap documentation.>&This is the implementation in SawCore: llvmBSwap :: (n :: Nat) -> bitvector (mulNat n 8) -> bitvector (mulNat n 8); llvmBSwap n x = join n 8 Bool (reverse n (bitvector 8) (split n 8 Bool x)); what4*Swap the order of the bits in a bitvector. what4Create a literal from an |. what4A utility combinator for combining actions that build terms with ifthenelse. If the given predicate is concretely true or false only the corresponding "then" or "else" action is run; otherwise both actions are run and combined with the given "ite" action. what4An iterated sequence of ifthenelse operations. The list of predicates and "then" results is constructed as-needed. The "default" value represents the result of the expression if none of the predicates in the given list is true. what4 Evaluates an  UnfoldPolicy on a collection of arguments. what4?This returns true if the value corresponds to a concrete value. what4Return some default value for each base type. For numeric types, this is 0; for booleans, false; for strings, the empty string. Structs are filled with default values for every field, default arrays are constant arrays of default values. what4)Return predicate equivalent to a Boolean. what4Create a value from a rational. what4Create a value from an integer. what4/Return 1 if the predicate is true; 0 otherwise. what4Extract the value of a complex expression, which is assumed to be a constant real number. Fail if the number has nonzero imaginary component, or if it is not a constant. what4:Return a complex value as a constant integer if it exists. what40Return value as a constant integer if it exists. what40Return value as a constant integer if it exists. what44Compute the conjunction of a sequence of predicates. what44Compute the disjunction of a sequence of predicates. what41Return predicate that holds if value is non-zero. what4Return predicate that holds if imaginary part of number is zero. what4Divide one number by another. cplxDiv x y is undefined when y is 0. what43Returns the principal logarithm of the input value. cplxLog x is undefined when x is 0>, and has a cut discontinuity along the negative real line. what4+Returns logarithm of input at a given base.cplxLogBase b x is undefined when x is 0. what4Return a concrete representation of a value, if it is concrete. what46Create a literal symbolic value from a concrete value. what4This function is used for selecting a value from among potential values in a range.muxRange p ite f l h returns an expression denoting the value obtained from the value f i where i$ is the smallest value in the range [l..h] such that p i is true. If p i8 is true for no such value, then this returns the value f h.  what4 lower bound what4 upper bound what4 lower bound what4 upper bound what4 lower bound what4 upper bound what4 lower bound what4 upper bound what4Symbolic interfacewhat40The name to give a function (need not be unique)what41Bound variables to use as arguments for function.what4.Operation defining result of defined function.what4$Policy for unfolding on applications what4Symbolic interfacewhat40The name to give a function (need not be unique)what4 Type signature for the argumentswhat4$Policy for unfolding on applicationswhat4.Operation defining result of defined function. what4Symbolic interfacewhat40The name to give a function (need not be unique)what4'Types of arguments expected by functionwhat4Return type of function what4Symbolic interfacewhat4Function to callwhat4Arguments to function what4most significant bitswhat4least significant bits what4/Starting index, from 0 as least significant bitwhat4Number of bits to takewhat4Bitvector to select from what4-Index of bit (0 is the least significant bit) what4 Shift this what4Amount to shift by what4 Shift this what4Amount to shift by what4 Shift this what4Amount to shift by what4bitvector to rotate what4amount to rotate by what4bitvector to rotate what4amount to rotate by what4Symbolic interfacewhat4Bitvector to updatewhat40-based index to setwhat4Predicate to set. what4symbolic interface what4output bitvector width what4%predicate to fill the bitvector with what4 Index typewhat4Constant what4Types for indiceswhat4Value for known indices.what4Value for other entries. what4Value for known indices.what4Value for existing array. what41Predicate that indicates if array should be true. what4string to test what4substring to look for what4prefix string what4string to test what4suffix string what4string to test what4string to search in what4substring to search for what4starting index for search what4"string to select a substring from what4)offset of the beginning of the substring what4length of the substring what4 lower bound what4 upper bound what4Symbolic interfacewhat4Bitvector to swap around what4Base for the logarithm what4Returns predicate that holds if we have found the value we are looking for. It is assumed that the predicate must hold for a unique integer in the range.what4 Ite function what4Function for concrete values what4Lower bound (inclusive) what4Upper bound (inclusive) %(&')*+43210/.,-56789:;<=>?@ABCDEFGHIJKLMNO|}~   |}~ +"Dynamically-sized bitvector valuesGalois, Inc. 2018-2020BSD3rdockins@galois.com experimental"non-portable (language extensions)None'(-./567>?"+ what4A What4 symbolic bitvector where the size does not appear in the type what47Return the signed value if this is a constant bitvector what49Return the unsigned value if this is a constant bitvector what4Convert an integer to an unsigned bitvector. The input value is reduced modulo 2^w. what4/Interpret the bit-vector as an unsigned integer what4,Interpret the bit-vector as a signed integer what4Get the width of a bitvector what41Create a bitvector with the given width and value what4Returns true if the corresponding bit in the bitvector is set. NOTE bits are numbered in big-endian ordering, meaning the most-significant bit is bit 0 what4Returns true if the corresponding bit in the bitvector is set. NOTE bits are numbered in little-endian ordering, meaning the least-significant bit is bit 0 what4Set the numbered bit in the given bitvector to the given bit value. NOTE bits are numbered in big-endian ordering, meaning the most-significant bit is bit 0 what4Set the numbered bit in the given bitvector to the given bit value. NOTE bits are numbered in big-endian ordering, meaning the most-significant bit is bit 0 what4Concatenate two bitvectors. what4Select a subsequence from a bitvector, with bits numbered in Big Endian order (most significant bit is 0). This fails if idx + n is >= w what4Select a subsequence from a bitvector, with bits numbered in Little Endian order (least significant bit is 0). This fails if idx + n is >= w what4#If-then-else applied to bitvectors. what4Explode a bitvector into a vector of booleans in Big Endian order (most significant bit first) what4Explode a bitvector into a vector of booleans in Little Endian order (least significant bit first) what4convert a vector of booleans to a bitvector. The input are used in Big Endian order (most significant bit first) what4convert a vector of booleans to a bitvector. The inputs are used in Little Endian order (least significant bit first) what4Bitwise complement what4Bitwise logical and. what4Bitwise logical or. what4Bitwise logical exclusive or. what42's complement negation. what4Add two bitvectors. what4$Subtract one bitvector from another. what4"Multiply one bitvector by another. what4Unsigned bitvector division.The result is undefined when y' is zero, but is otherwise equal to floor( x / y ). what4Unsigned bitvector remainder.The result is undefined when y' is zero, but is otherwise equal to x - (bvUdiv x y) * y. what4None '(./235678?/ what4A partial value represents a value that may or may not be valid.The   field represents a predicate (optionally with additional provenance information) embodying the value's partiality.what4/Either a partial value, or a straight-up error.what4A monad transformer which enables symbolic partial computations to run by maintaining a predicate on the value.what4A  is a  that provides no information about what went wrong. Its name is historic.what4=Create a part expression from a value that is always defined.what4,Create a part expression from a maybe value.what4 = LM .what4$If-then-else on partial expressions.what4Merge a collection of partial values in an if-then-else tree. For example, if we merge a list like [(xp,x),(yp,y),(zp,z)]6, we get a value that is morally equivalent to: if xp then x else (if yp then y else (if zp then z else undefined)).what4Run a partial computation.what4End the partial computation and just return the unassigned value.what4Lift a  value to a partial expression.what4Return a partial expression.This joins the partial expression with the current constraints on the current computation.what4:Add an extra condition to the current partial computation.what4'Operation to combine inner values. The  3 parameter is the if-then-else condition. what4condition to merge on what4'if' value what4'then' value what40Operation to combine inner values. The  ) parameter is the if-then-else condition.what4values to merge what4Solver interfacewhat4Initial conditionwhat4Computation to run.  ./Predicates with some metadata (a tag or label).(c) Galois, Inc 2019-2020BSD3&Langston Barrett  provisionalNone358what48Information about an assertion that was previously made.what4Predicate that was asserted.what41Message added when assumption/assertion was made.what4Predicate that was asserted.what41Message added when assumption/assertion was made.what4Partition datastructures containing predicates by their possibly concrete values.The output format is (constantly true, constantly false, unknown/symbolic).what4Partition datastructures containing predicates by their possibly concrete values.The output format is (constantly true, constantly false, unknown/symbolic).what4?Partition labeled predicates by their possibly concrete values.The output format is (constantly true, constantly false, unknown/symbolic).what4'avoid "ambiguous type variable" errors what4'avoid "ambiguous type variable" errors what4'avoid "ambiguous type variable" errors  /None'(/>2what4A family of value-level representatives for floating-point types.what4This data kind describes the types of floating-point formats. This consist of the standard IEEE 754-2008 binary floating point formats, as well as the X86 extended 80-bit format and the double-double format.what4Helper interface for creating new symbolic floating-point constants and variables.what4?Create a fresh top-level floating-point uninterpreted constant.what4-Create a fresh floating-point latch variable.what4(Creates a floating-point bound variable.what4"Abstact floating point operations.what4Return floating point number +0.what4Return floating point number -0.what4Return floating point NaN.what4Return floating point  +infinity.what4Return floating point  -infinity.what48Create a floating point literal from a rational literal.what43Create a (single precision) floating point literal.what43Create a (double precision) floating point literal.what4=Create an (extended double precision) floating point literal.what4Negate a floating point number.what45Return the absolute value of a floating point number.what43Compute the square root of a floating point number.what4Add two floating point numbers.what4$Subtract two floating point numbers.what4$Multiply two floating point numbers.what4"Divide two floating point numbers.what4Compute the reminder:  x - y * n, where n in Z is nearest to x / y.what4-Return the min of two floating point numbers.what4-Return the max of two floating point numbers.what4/Compute the fused multiplication and addition:  (x * y) + z.what45Check logical equality of two floating point numbers.what49Check logical non-equality of two floating point numbers.what42Check IEEE equality of two floating point numbers.what43Check IEEE apartness of two floating point numbers.what4Check <= on two floating point numbers.what4Check < on two floating point numbers.what4Check >= on two floating point numbers.what4Check > on two floating point numbers.what4'If-then-else on floating point numbers.what40Change the precision of a floating point number.what43Round a floating point number to an integral value.what4Convert from binary representation in IEEE 754-2008 format to floating point.what4Convert from floating point from to the binary representation in IEEE 754-2008 format.what48Convert a unsigned bitvector to a floating point number.what46Convert a signed bitvector to a floating point number.what41Convert a real number to a floating point number.what48Convert a floating point number to a unsigned bitvector.what46Convert a floating point number to a signed bitvector.what41Convert a floating point number to a real number.what4The associated BaseType representative of the floating point interpretation for each format.what4 Symbolic floating point numbers.what4*Interpretation of the floating point type.what4Representation of 80-bit floating values, since there's no native Haskell type for these.what45Two 64-bit floats fused in the "double-double" style.what4X86 80-bit extended floats.what4128 bit binary IEEE754.what464 bit binary IEEE754.what432 bit binary IEEE754.what416 bit binary IEEE754.0"A "unary" bitvector representation(c) Galois, Inc 2015-2020BSD3!Joe Hendrix None '(/?"Fwhat4A unary bitvector encoding where the map contains predicates such as u^.unaryBVMap^.at i$ holds iff the value represented by u is less than or equal to i.The map stored in the representation should always have a single element, and the largest integer stored in the map should be associated with a predicate representing "true". This means that if the map contains only a single binding, then it represents a constant.what49Returns the number of distinct values that this could be.what4.Create a unary bitvector term from a constant.what4.Create a unary bitvector term from a constant.what4unsignedRanges v returns a set of predicates and ranges where we know that for each entry (p,l,h) and each value i : l <= i & i <= h: p iff. v <= iwhat4Evaluate a unary bitvector as an integer given an evaluation function.what48Evaluate a unary bitvector given an evaluation function.This function is used to convert a unary bitvector into some other representation such as a binary bitvector or vector of bits.'It is polymorphic over the result type r:, and requires functions for manipulating values of type r to construct it.what4This function instantiates the predicates in a unary predicate with new predicates. The mapping f1 should be monotonic, that is for all predicates p and 'q, such that 'p |- q', f1 should satisfy the constraint that 'f p |- f q'.what4,Return potential values for abstract domain.what4 mux sym c x y returns value equal to if c then x else y8. The number of entries in the return value is at most size x + size y.what44Return predicate that holds if bitvectors are equal.what4>Return predicate that holds if first value is less than other.what4>Return predicate that holds if first value is less than other.what4Add two bitvectors.The number of integers in the result will be at most the product of the sizes of the individual bitvectors.what4Negate a bitvector. The size of the result will be equal to the size of the input.what4Perform a unsigned extensionwhat4Perform a signed extensionwhat4Perform a struncation.what4Function for mapping an integer to its bitvector representation.what4Function for performing an ite expression on r.what4Unary bitvector to evaluate.1/Datastructure for sequences of appended strings(c) Galois Inc, 2019-2020BSD3rdockins@galois.comNone '(/#+  28Low-level support for MATLAB-style arithmetic operations(c) Galois, Inc, 2016-2020BSD3!Joe Hendrix None'(/?(what4Builtin functions that can be used to generate symbolic functions.These functions are expected to be total, but the value returned may not be specified. e.g. IntegerToNatFn must return some natural number for every integer, but for negative integers, the particular number is unspecified.what43Compute the clamped negation of a signed bitvector.The only difference between this operation and the usual 2's complement negation function is the handling of MIN_INT. The usual 2's complement negation sends MIN_INT to MIN_INT; however, the clamped version instead sends MIN_INT to MAX_INT.what49Compute the clamped absolute value of a signed bitvector.The only difference between this operation and the usual 2's complement operation is the handling of MIN_INT. The usual 2's complement absolute value function sends MIN_INT to MIN_INT; however, the clamped version instead sends MIN_INT to MAX_INT.what4This class is provides functions needed to implement the symbolic array intrinsic functionswhat43Create a Matlab solver function from its prototype.what4Get arg tpyes of solver fn.what4Get return type of solver fn.what4Test  values for equality.3(c) Galois Inc, 2015-2020BSD3jhendrix@galois.comNone! &'(./8>??'what4This represents a symbolic function in the simulator. Parameter t4 is a phantom type brand used to track nonces. The args and ret parameters define the types of arguments and the return type of the function.Type  t (Expr t) instantiates the type family   ( ExprBuilder t st).what4This describes information about an undefined or defined function. Parameter t4 is a phantom type brand used to track nonces. The args and ret parameters define the types of arguments and the return type of the function.what4Information about the argument type and return type of an uninterpreted function.what4Information about a defined function. Includes bound variables and an expression associated to a defined function, as well as a policy for when to unfold the body.what4This is a function that corresponds to a matlab solver function. It includes the definition as a ExprBuilder expr to enable export to other solvers.what4Type NonceApp t e tp* encodes the top-level application of an . It includes expression forms that bind variables (contrast with ). Parameter t: is a phantom type brand used to track nonces. Parameter e is used everywhere a recursive sub-expression would go. Uses of the ; type will tie the knot through this parameter. Parameter tp& indicates the type of the expression.what4.Information about bound variables. Parameter t. is a phantom type brand used to track nonces.Type  t instantiates the type family   ( ExprBuilder t st).,Selector functions are provided to destruct  values, but the constructor is kept hidden. The preferred way to construct a  is to use  .what4The Kind of a bound variable.what4%A variable appearing in a quantifier.what4&A variable appearing as a latch input.what40A variable appearing in a uninterpreted constantwhat4Type  e tp) encodes the top-level application of an  expression. It includes first-order expression forms that do not bind variables (contrast with ). Parameter e is used everywhere a recursive sub-expression would go. Uses of the ; type will tie the knot through this parameter. Parameter tp& indicates the type of the expression.what4The main ExprBuilder expression datastructure. The non-trivial Expr values constructed by this module are uniquely identified by a nonce value that is used to explicitly represent sub-term sharing. When traversing the structure of an Expr it is usually very important to memoize computations based on the values of these identifiers to avoid exponential blowups due to shared term structure.Type parameter t is a phantom type brand used to relate nonces to a specific nonce generator (similar to the s parameter of the ST monad). The type index tp of kind F indicates the type of the values denoted by the given expression.Type  t instantiates the type family   ( ExprBuilder t st).what4This type represents  values that were built from an . Parameter t. is a phantom type brand used to track nonces.,Selector functions are provided to destruct  values, but the constructor is kept hidden. The preferred way to construct an  from an  is to use  sbMakeExpr.what4This type represents  values that were built from a . Parameter t. is a phantom type brand used to track nonces.,Selector functions are provided to destruct  values, but the constructor is kept hidden. The preferred way to construct an  from a  is to use  sbNonceExpr.what4!Either a argument or text or textwhat4Contains the elements before, the index, doc, and width and the elements after.what4A fixed doc with length.what4A doc that can be let bound.what4 AppPPExpr6 represents a an application, and it may be let bound.what4.Length of AppPPExpr not including parenthesis.what4This privides a view of a semiring expr as a weighted sum of values.what4+Used to implement foldMapFc from traversal.what4$Check if two applications are equal.what4Hash an an application.what4Return true if an app represents a non-linear operation. Controls whether the non-linear counter ticks upward in the  .what4Destructor for the  constructor.what4Destructor for the  constructor.what4+Get abstract value associated with element.what4A slightly more aggressive syntactic equality check than testEquality,  will recurse through a small collection of known syntax formers.what4Pretty print a AppPPExprwhat4$Get length of Expr including parens.what4Pretty print PPExprwhat4Pretty print an ' using let bindings to create the term.what4(Pretty print the top part of an element.what48Return solver function associated with ExprSymFn if any.what4'Return an unconstrained abstract value.what42Return abstract domain associated with a nonce appwhat45Pretty print a code to identify the type of constant.47Main definitions of the What4 expression representation(c) Galois Inc, 2015-2020BSD3jhendrix@galois.comNone &'(./8>?Rwhat41An IdxCache is used to map expressions with type  Expr t tp& to values with a corresponding type f tp . It is a mutable map using an  hash table. Parameter t/ is a phantom type brand used to track nonces.what4(Cache for storing dag terms. Parameter t. is a phantom type brand used to track nonces.what4The maximum number of distinct values a term may have and use the unary representation.what4?The maximum number of distinct ranges in a BVDomain expression.what4+The starting size when building a new cachewhat4Counter to generate new unique identifiers for elements and functions.what40Additional state maintained by the state managerwhat4>Mode flag for how floating-point values should be interpreted.what4This describes what a given SolverSymbol is associated with. Parameter t. is a phantom type brand used to track nonces.what4Solverwhat4A bijective map between vars and their canonical name for printing purposes. Parameter t. is a phantom type brand used to track nonces.what4Empty symbol var bimapwhat4Create a new IdxCachewhat45Return the value associated to the expr in the index.what4.Bind the value to the given expr in the index.what4 Remove a value from the IdxCachewhat4#Remove all values from the IdxCachewhat4Implements a cached evaluated using the given element. Given an element this function returns the value of the element if bound, and otherwise calls the evaluation function, stores the result in the cache, and returns the value.what4Implements a cached evaluated using the given element. Given an element this function returns the value of the element if bound, and otherwise calls the evaluation function, stores the result in the cache, and returns the value.what4#Create an element from a nonce app.what45Maximum number of values in unary bitvector encoding..This option is named "backend.unary_threshold"what47Maximum number of ranges in bitvector abstract domains.3This option is named "backend.bvdomain_range_limit"what48Starting size for element cache when caching is enabled./This option is named "backend.cache_start_size"what4Indicates if we should cache terms. When enabled, hash-consing is used to find and deduplicate common subexpressions. This option is named "use_cache"what4Get current variable bindings.what4%Stop caching applications in backend.what4Restart caching applications in backend (clears cache if it is currently caching).what4This evaluates the term with the given bound variables rebound to the given arguments.The algorithm works by traversing the subterms in the term in a bottom-up fashion while using a hash-table to memoize results for shared subterms. The hash-table is pre-populated so that the bound variables map to the element, so we do not need any extra map lookup when checking to see if a variable is bound.NOTE: This function assumes that variables in the substitution are not themselves bound in the term (e.g. in a function definition or quantifier). If this is not respected, then  will call  with an error message.what4*Evaluate a weighted sum of integer values.what4'Evaluate a weighted sum of real values.what4Float interpretation mode (i.e., how are floats translated for the solver).what4(Initial state for the expression builderwhat4Nonce generator for names|}~  |}~ 5None '(./f!what4Necessary monadic operationswhat4All module inputs, in reverse order. We use Word64 for Nonces to avoid GHC bugs. For more detail:  0https://gitlab.haskell.org/ghc/ghc/-/issues/2595  1https://gitlab.haskell.org/ghc/ghc/-/issues/10856 1https://gitlab.haskell.org/ghc/ghc/-/issues/16501what4All module outputs, in reverse order. Includes the type, signedness, name, and initializer of each.what4All internal wires, in reverse order. Includes the type, signedness, name, and initializer of each.what4A map from the identifier nonces seen so far to their identifier names. These nonces exist for identifiers from the original term, but not intermediate Verilog variables.what4A set of all the identifiers used so far, including intermediate Verilog variables.what4An expression cache to preserve sharing present in the What4 representation.what4A cache of bit vector constants, to avoid duplicating constant declarations.what4A cache of Boolean constants, to avoid duplicating constant declarations.what4'The What4 symbolic backend to use with .what4;A data type for items that may show up in a Verilog module.what4A wrapper around the BV type allowing it to be put into a map or set. We use this to make sure we generate only one instance of each distinct constant.what4A type for Verilog expressions that enforces well-typedness, including bitvector size constraints.what4A type for Verilog expression names that enforces well-typedness. This type exists essentially to pair a name and type to avoid needing to repeat them and ensure that all uses of the name are well-typed.what4A type for Verilog unary operators that enforces well-typedness.what4A type for Verilog binary operators that enforces well-typedness, including bitvector size constraints.what4Create a let binding, associating a name with an expression. In Verilog, this is a new "wire".what4Indicate than an expression name is signed. This causes arithmetic operations involving this name to be interpreted as signed operations.what4Apply a binary operation to two expressions and bind the result to a new, returned name.what4A special binary operation for scalar multiplication. This avoids the need to call  at every call site.what4Return the (possibly-cached) name for a literal bitvector value.what4>Return the (possibly-cached) name for a literal Boolean value.what4Apply a unary operation to an expression and bind the result to a new, returned name.what4Create a conditional, with the given condition, true, and false branches, and bind the result to a new, returned name.what4Extract a single bit from a bit vector and bind the result to a new, returned name.what4Extract a range of bits from a bit vector and bind the result to a new, returned name. The two NatRepr values are the starting index and the number of bits to extract, respectively.what4Concatenate two bit vectors and bind the result to a new, returned name.what4Create a Verilog module in the context of a given What4 symbolic backend and a monadic computation that returns an expression name that corresponds to the module's output.what4Returns and records a fresh input with the given type and with a name constructed from the given base.what4Add an output to the current Verilog module state, given a type, a name, and an initializer expression.what4Add a new wire to the current Verilog module state, given a type, a signedness flag, a name, and an initializer expression.what4Create a fresh identifier by concatenating the given base with the current fresh identifier counter.what4Add a new wire to the current Verilog module state, given a type, a signedness flag, the prefix of a name, and an initializer expression. The name prefix will be freshened by appending current value of the fresh variable counter.6None '(./?hwhat4Convert a What4 expresssion into a Verilog expression and return a name for that expression's result.7None &'(i8what4.Show non-negative Integral numbers in base 16.  8Nonejwhat4Convert the given What4 expressions, representing the outputs of a circuit, into a textual representation of a Verilog module of the given name.what4Convert the given What4 expressions, representing the outputs of a circuit, into a Verilog module of the given name.9?Simplification procedure for distributing operations through ifthenelse(c) Galois, Inc 2016-2020BSD3!Joe Hendrix None &'(.?l5what47Simplify a Boolean expression by distributing over ite.what4Return a map from nonce indices to the number of times an elt with that nonce appears in the subterm.:?Computing ground values for expressions from solver assignments(c) Galois, Inc 2016-2020BSD3!Joe Hendrix  provisionalNone./sQ what4)A representation of a ground-value array.what4%Lookup function for querying by indexwhat42Default value and finite map of particular indiceswhat49A newtype wrapper around ground value for use in a cache.what4Function that calculates upper and lower bounds for real-valued elements. This type is used for solvers (e.g., dReal) that give only approximate solutions.what4A function that calculates ground values for elements. Clients of solvers should use the  groundEval, function for computing values in models.what4$Look up an index in an ground array.what40Construct a default value for a given base type.what4Helper function for evaluating Expr expressions in a model.This function is intended for implementers of symbolic backends.what4Evaluate an element, when given an evaluation function for subelements. Instead of recursing directly,  calls into the given function on sub-elements to allow the caller to cache results if desired.However, sometimes we are unable to compute expressions outside the solver. In these cases, this function will return  in the `MaybeT IO` monad. In these cases, the caller should instead query the solver directly to evaluate the expression, if possible.what4Helper function for evaluating NonceApp expressions.This function is intended for implementers of symbolic backends.what4Helper function for evaluating App expressions.This function is intended for implementers of symbolic backends.;Defines the low-level interface between a particular solver and the SimpleBuilder family of backends.(c) Galois, Inc 2015-2020BSD3!Rob Dockins  provisionalNonezf what4A collection of operations for producing output from solvers. Solvers can produce messages at varying verbosity levels that might be appropriate for user output by using the  operation. If a  is provided, the entire interaction sequence with the solver will be mirrored into that handle.what4&takes a verbosity and a message to logwhat4+the default verbosity; typical default is 2what4'the reason for performing the operationwhat40handle on which to mirror solver input/responseswhat4The main interface for interacting with a solver in an "offline" fashion, which means that a new solver process is started for each query.what45Configuration options relevant to this solver adapterwhat4Operation to check the satisfiability of a formula. The final argument is a callback that calculates the ultimate result from a SatResult and operations for finding model values in the event of a SAT result. Note: the evaluation functions may cease to be avaliable after the callback completes, so any necessary information should be extracted from them before returning.what4Write an SMTLib2 problem instance onto the given handle, incorporating any solver-specific tweaks appropriate to this solverwhat41Default featues to use for writing SMTLIB2 files.what4Test the ability to interact with a solver by peforming a check-sat query on a trivially unsatisfiable problem.<Infrastructure for rendering What4 expressions in the language of SMT solvers(c) Galois, Inc 2014-2020.BSD3!Joe Hendrix None '(./?what48Used when we need two way communication with the solver.what43Get functions for parsing values out of the solver.what4.Parse a set result from the solver's response.what4Parse a list of names of assumptions that form an unsatisfiable core. These correspond to previously-named assertions.what4Parse a list of names of assumptions that form an unsatisfiable core. The boolean indicates the polarity of the atom: true for an ordinary atom, false for a negated atom.what4Given a SMT term for a Boolean value, this should whether the term is assigned true or false.what4Given a bitwidth, and a SMT term for a bitvector with that bitwidth, this should return an unsigned integer with the value of that bitvector.what4Given a SMT term for real value, this should return a rational value for that term.what4Given floating point format, and an SMT term for a floating-point value in that format, this returns an unsigned integer with the bits of the IEEE-754 representation.what4If , a function to read arrays whose domain and codomain are both bitvectors. If , signifies that we should fall back to index-selection representation of arrays.what4Given a SMT term representing as sequence of bytes, return the value as a bytestring.what4=This describes the result that was collected from the solver.what4"Result from sandboxed computation.what4List of bound variables.what4"Constants added during generation.what41List of Boolean predicates asserted by collector.what4+Typeclass need to generate SMTLIB commands.what4Create a forall expressionwhat4Create an exists expressionwhat4Create a constant arrayThis may return Nothing if the solver does not support constant arrays.what4Select an element from an arraywhat49'arrayUpdate a i v' returns an array that contains value v at index i, and the same value as in a at every other index.what4-Create a command that just defines a comment.what4(Create a command that asserts a formula.what4Create a command that asserts a formula and attaches the given name to it (primarily for the purposes of later reporting unsatisfiable cores).what4Push 1 new scopewhat4Pop 1 existing scopewhat4Pop several scopes.what4Reset the solver state, forgetting all pushed frames and assertionswhat4Check if the current set of assumption is satisfiable. May require multiple commands. The intial commands require an ack. The last one does not.what4Check if a collection of assumptions is satisfiable in the current context. The assumptions must be given as the names of literals already in scope.what4Ask the solver to return an unsatisfiable core from among the assumptions passed into the previous "check with assumptions" command.what4Ask the solver to return an unsatisfiable core from among the named assumptions previously asserted using the  after an unsatisfiable  checkCommand.what4Set an option/parameter.what4Declare a new symbol with the given name, arguments types, and result type.what4Define a new symbol with the given name, arguments, result type, and associated expression.The argument contains the variable name and the type of the variable.what4Declare a struct datatype if is has not been already given the number of arguments in the struct.what43Build a struct term with the given types and fieldswhat42Project a field from a struct with the given typeswhat4,Produce a term representing a string literalwhat4Compute the length of a termwhat4stringIndexOf s t i5 computes the first index following or at i where t appears within s1 as a substring, or -1 if no such index existswhat43Test if the first string contains the second stringwhat49Test if the first string is a prefix of the second stringwhat49Test if the first string is a suffix of the second stringwhat4stringSubstring s off len extracts the substring of s starting at index off and having length len0. The result of this operation is undefined if off and len( to not specify a valid substring of s; in particular, we must have off+len <= length(s).what4Append the given stringswhat4,Forget all previously-declared struct types.what4"Write a command to the connection.what4.Strictness level for parsing solver responses.what4:allows other output preceeding recognized solver responseswhat4?parse _only_ recognized solver responses; fail on anything elsewhat4An action for consuming an acknowledgement message from the solver, if it is configured to produce ack messages.what4,Name of writer for error reporting purposes.what4Handle to write towhat4Handle to read responses from. In some contexts, there are no responses expected (e.g., if we are writing a problem directly to a file); in these cases, the input stream might be the trivial stream  nullInput(, which just immediately returns EOF.what4Indicates if the writer can define constants or functions in terms of an expression.If this is not supported, we can only declare free variables, and assert that they are equal.what48Functions may be passed as arguments to other functions.We currently never allow SMT_FnType to appear in structs or array indices.what4;Allow the SMT writer to generate problems with quantifiers.what4Be strict in parsing SMTLib2 responses; no verbosity or variants allowedwhat4+Indicates features supported by the solver.what4$The specific connection information.what4A term in the output language.what45A class of values containing rational and operations.what4"Compare two elements for equality.what4%Compare two elements for in-equality.what4Create a let expression. This is a "sequential" let, which is syntactic sugar for a nested series of single let bindings. As a consequence, bound variables are in scope for the right-hand-sides of subsequent bindings.what4"Create an if-then-else expression.what4Add a list of values together.what4(Convert an integer expression to a real.what4(Convert a real expression to an integer.what4Convert an integer to a term.what4Convert a rational to a term.what4Less-then-or-equalwhat4 Less-thenwhat4 Greater thenwhat4Greater then or equalwhat4Integer theory termswhat4!Create expression from bitvector.what4$Concatenate two bitvectors together.what4bvExtract w i n v extracts bits [i..i+n) from v as a new bitvector. v must contain at least w elements, and i+n must be less than or equal to w. The result has n) elements. The least significant bit of v should have index 0.what4bvTestBit w i x% returns predicate that holds if bit i in x is set to true. w! should be the number of bits in x.what44Predicate that holds if a real number is an integer.what4*Apply the arguments to the given function.what4Update a function value to return a new value at the given point.This may be Nothing if solver has no builtin function for update.what4:Function for creating a lambda term if output supports it.Yices support lambda expressions, but SMTLIB2 does not. The function takes arguments and the expression.what4 defines how a given F maps to an SMTLIB type.It is necessary as there may be several ways in which a base type can be encoded.what4+An acknowledgement action that does nothingwhat42Clear the entry stack, and start with a fresh one.what4Pop all but the topmost stack entry. Return the number of entries on the stack prior to popping.what4Return the number of pushed stack frames. Note, this is one fewer than the number of entries in the stack beacuse the base entry is the top-level context that is not in the scope of any push.what4?Push a new frame to the stack for maintaining the writer cache.what4Given an optional override configuration option, return the SMT response parsing strictness that should be applied based on the override or thedefault strictSMTParsing configuration.what4Write a command to the connection along with position information if it differs from the last position.what4Write a sequence of commands. All but the last should have acknowledgement.what4*Create a new variable with the given name.what4Consider the bound variable as free within the current assumption frame.what4$Assume that the given formula holds.what49Create a variable name eqivalent to the given expression.what40Given a solver connection and a base type repr,  attempts to find the best encoding for a variable of that type supported by teh solver.what46This runs the side collector and collects the results.what4(Convert an element to a base expression.what4Write a expression to SMTwhat4Write a logical expression.what4>Write assume formula predicates for asserting predicate holds.what4The function creates a function for evaluating elts to concrete values given a connection to an SMT solver along with some functions for evaluating different types of terms to concrete values.what4Name of variablewhat4Type for indiceswhat4Type for value.what4Constant to assign all values.what4Stream to write queries ontowhat43Input stream to read responses from (may be the  nullInput% stream if no responses are expected)what45An action to consume solver acknowledgement responseswhat4&Name of solver for reporting purposes.what4Be strict in parsing responses?what44Indicates what features are supported by the solver.what4A bijective mapping between variables and their canonical name (if any).what44State information specific to the type of connectionwhat4/Names of variables in term and associated type.what4Type of expression.what4Connection to SMT solver.32444444=None what41Called to get a response from the SMT connection.what4Gets a limited set of responses, throwing an exception when a response is not matched by the filter. Also throws exceptions for standard error results. The passed command and intent arguments are only used for marking error messages.Callers which do not want exceptions thrown for standard error conditions should feel free to use + and handle all response cases themselves.>;Identifying the solver theory required by a core expression(c) Galois, Inc 2016-2020BSD3!Joe Hendrix  provisionalNone'(hwhat4$The theory that a symbol belongs to.what4Theory attributed to structs (equivalent to records in CVC4/Z3, tuples in Yices)what4(Theory attributed application functions.?=Compute the bound and free variables appearing in expressions(c) Galois, Inc 2015-2020BSD3!Rob Dockins  provisionalNone &'(/W what47Information about bound variables outside this context.what4Contains all information about a bound variable appearing in the expression.what45The outer term containing the binding (e.g., Ax.f(x))what4#The type of quantifier that appearswhat4The variable that is bound Variables may be bound multiple times.what4)The term that appears inside the binding.what4Describes types of functionality required by solver based on the problem.what4Expressions appearing in the problem as existentially quantified when the problem is expressed in negation normal form. This is a map from the existential quantifier element to the info.what4Expressions appearing in the problem as existentially quantified when the problem is expressed in negation normal form. This is a map from the existential quantifier element to the info.what48Return variables needed to define element as a predicatewhat4#Record the variables in an element.N:Commonly-used reexports from the expression representation(c) Galois, Inc 2015-2020BSD3!Rob Dockins None_@Online solver interactions(c) Galois, Inc 2018-2020BSD3!Rob Dockins None '(ɱ#what4.A live connection to a running solver process.This data structure should be used in a single-threaded manner or with external synchronization to ensure that only a single thread has access at a time. Unsynchronized multithreaded use will lead to race conditions and very strange results.what4)Writer for sending commands to the solverwhat4Callback for regular code paths to gracefully close associated pipes and wait for the process to shutdownwhat4Handle to the solver processwhat4;Indicate this solver's behavior following an error responsewhat4%Standard error for the solver processwhat41The functions used to parse values out of models.what4Some solvers will enter an UNSAT state early, if they can easily determine that context is unsatisfiable. If this IORef contains an integer value, it indicates how many "pop" operations need to be performed to return to a potentially satisfiable state. A Just 0 state indicates the special case that the top-level context is unsatisfiable, and must be "reset".what4Some solvers do not have support for the SMTLib2.6 operation (reset-assertions), or an equivalent. For these solvers, we instead make sure to always have at least one assertion frame pushed, and pop all outstanding frames (and push a new top-level one) as a way to mimic the reset behavior.what4The amount of time (in seconds) that a solver should spend trying to satisfy any particular goal before giving up. A value of zero indicates no time limit.what4The amount of time that a solver is allowed to attempt to satisfy any particular goal.)The timeout value may be retrieved with  or .what4This datatype describes how a solver will behave following an error.what4This indicates the solver will immediately exit following an errorwhat4This indicates the solver will remain live and respond to further commmands following an errorwhat4This class provides an API for starting and shutting down connections to various different solvers that support online interaction modes.what41Start a new solver process attached to the given .what4Shut down a solver process. The process will be asked to shut down in a "polite" way, e.g., by sending an (exit)) message, or by closing the process's . Use  killProcess/ instead to shutdown a process via a signal.what4Simple data-type encapsulating some implementation of an online solver.what4Get the SolverGoalTimeout raw numeric value in units of seconds.what4-Standard input stream for the solver process.what45The solver's stdout, for easier parsing of responses.what49An impolite way to shut down a solver. Prefer to use , unless the solver is unresponsive or in some unrecoverable error state.what4Check if the given formula is satisfiable in the current solver state, without requesting a model. This is done in a fresh frame, which is exited after the check call.what4Check if the formula is satisifiable in the current solver state. This is done in a fresh frame, which is exited after the continuation complets. The evaluation function can be used to query the model. The model is valid only in the given continuation.what4Pop all assumption frames and remove all top-level asserts from the global scope. Forget all declarations except those in scope at the top level.what4#Push a new solver assumption frame.what4'Pop a previous solver assumption frame.what4 provisionalNone !&'(/>swhat4Run the solver in a session.what41This is an interactive session with an SMT solverwhat4This class exists so that solvers supporting the SMTLib2 format can support features that go slightly beyond the standard.In particular, there is no standardized syntax for constant arrays (arrays which map every index to the same value). Solvers that support the theory of arrays and have custom syntax for constant arrays should implement . In addition, solvers may override the default representation of complex numbers if necessary. The default is to represent complex numbers as "(Array Bool Real)" and to build instances by updating a constant array.what4Return a representation of the type associated with a (multi-dimensional) symbolic array.By default, we encode symbolic arrays using a nested representation. If the solver, supports tuples/structs it may wish to change this.what4/The sort of structs with the given field types.By default, this uses SMTLIB2 datatypes and are not primitive to the language.what44Construct a struct value from the given field valueswhat4(Construct a struct field projection termwhat4&Set the logic to all supported logics.what4Write check sat commandwhat46Set the produce models option (We typically want this)what4&This function runs a check sat commandwhat4A default method for writing SMTLib2 problems without any solver-specific tweaks.what49Solver version bounds computed from "solverBounds.config"what4!Get the result of a version querywhat4)Query the solver's error behavior settingwhat4!Get the result of a version querywhat4 provisionalNone  '(>owhat4 Path to Z3what41Per-check timeout, in milliseconds (zero is none)what4Run Z3 in a session. Z3 will be configured to produce models, but otherwise left with the default configuration.what4Path to Z3 executablewhat4 Action to run  CSolver adapter code for Yices(c) Galois, Inc 2015-2020BSD3!Rob Dockins  provisionalNone &/>% what4;Exceptions that can occur when reading responses from Yiceswhat4&This is a tag used to indicate that a . is a connection to a specific Yices process.what4Send a check command to Yices.what4 Call eval to get a Boolean term.what4 Path to yiceswhat4Enable the MC-SAT solverwhat49Enable interactive mode (necessary for per-goal timeouts)what4"Set a per-goal timeout in seconds.what4Write a yices file that checks the satisfiability of the given predicate.what4"Run writer and get a yices result.what4+Indicates the problem features to support. what4%Builder for getting current bindings.what4 Path to filewhat4Predicate to checkDSolver adapter code for STP(c) Galois, Inc 2015-2020BSD3!Joe Hendrix  provisionalNone > what4 Path to stpwhat4Run STP in a session. STP will be configured to produce models, buth otherwise left with the default configuration.what4Path to STP executablewhat4 Action to runESolver adapter code for an external ABC process via SMT-LIB2.(c) Galois, Inc 2020BSD3Aaron Tomb  provisionalNone  '(>what4 Path to ABCFInterface for running dReal(c) Galois, Inc 2014-2020BSD3!Rob Dockins  provisionalNone /what4 Path to dRealwhat4propositions to check  GSolver adapter code for CVC4(c) Galois, Inc 2015-2020BSD3!Rob Dockins  provisionalNone  '(>what4 Path to cvc4what41Per-check timeout, in milliseconds (zero is none)what4Run CVC4 in a session. CVC4 will be configured to produce models, but otherwise left with the default configuration.what4Path to CVC4 executablewhat4 Action to run  HInterface for running Boolector(c) Galois, Inc 2014-2020BSD3!Rob Dockins  provisionalNone  '(>ywhat4Path to boolectorwhat4Run Boolector in a session. Boolector will be configured to produce models, but otherwise left with the default configuration.what4Path to Boolector executablewhat4 Action to runO"Reexports for working with solvers(c) Galois, Inc 2015-2020BSD3!Rob Dockins None! I.Datastructure for mapping bitvectors to values(c) Galois, Inc 2014-2020BSD3!Rob Dockins None/what4A WordMap: represents a finite partial map from bitvectors of width w to elements of type tp.what43Create a word map where every element is undefined.what4Compute a pointwise if-then-else operation on the elements of two word maps.what4%Update a word map at the given index.what4+Lookup the value of an index in a word map.what4index what4 new value what4word map to update what4index PQRSTUSVWXYYZ[\Z[]^__`abcdefghijklmnopqrstuvwxyz{|}~                                                                                                                                                                                                              !!!!!!!!!!!!""""""""""""""""""""""###########################$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%&&&&&&&&&&&&&&&&&&'''''''''''''''''''''''(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((( ( ) ) ) ) ) ) * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * ** * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +++++++++ + + + + + + + + , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - . . . . . . . . . . . . . . . . . . . . . . . . / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / / ////////////000000000000000000000001111111111111111222222222222222222222222222222222222222222222222222222222222222222222333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333333334444444444444444444444444444444444444444444444444444444444444444445555555555555555555555555555555555555555555555555555555555555555555555555555555555555555555555567777777777777889999::::::::::::::::::::;;;;;;;;;;;;;;;;;;;;;<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<< <<<<<<<<<<<<<<<<<<< < < < < < <<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<< < < < << < < < <<<<< < < < < < < < < < < < <<<<< < < < < < < < < < < < < < < < < < < < < < < < < < < < < << < < << < < < <<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<==============================>>>>>>>>>>>>>>>>>?????????????????????????????@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAABBBBBBBBBBBBBBCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCCDDDDDDDDDDDDEEEEEEEEEEFFFFFFFFFFFFGGGGGGGGGGGGGGGHHHHHHHHHHHHIIIIIIPZPKSJSJSJSJSSSSZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZZSS(SSSSPSSS what4-1.2-1HZVAtyI2ZZL0e5J47Z1A4What4.Utils.MonadST What4.PanicWhat4.BaseTypesTest.VerificationWhat4.FunctionNameWhat4.IndexLitWhat4.ProblemFeaturesWhat4.ProgramLocWhat4.Protocol.PolyRootWhat4.Protocol.ReadDecimalWhat4.Protocol.SExpWhat4.Protocol.SMTLib2.ParseWhat4.Protocol.SMTLib2.SyntaxWhat4.SatResultWhat4.SemiRing What4.SymbolWhat4.Utils.AnnotatedMapWhat4.Utils.ArithmeticWhat4.Utils.BVDomain.ArithWhat4.Utils.BVDomain.BitwiseWhat4.Utils.BVDomain.XORWhat4.Utils.BVDomainWhat4.Utils.ComplexWhat4.Utils.EndianWhat4.Utils.EnvironmentWhat4.Utils.FloatHelpersWhat4.Utils.HandleReaderWhat4.Utils.IncrHashWhat4.Expr.BoolMapWhat4.Utils.LeqMapWhat4.Utils.OnlyIntReprWhat4.Utils.StreamsWhat4.Utils.VersionsWhat4.Utils.Word16StringWhat4.Utils.StringLiteralWhat4.Utils.AbstractDomainsWhat4.Expr.WeightedSumWhat4.Expr.ArrayUpdateMapWhat4.Concrete What4.ConfigWhat4.Utils.ProcessWhat4.Interface What4.SWord What4.SFloat What4.PartialWhat4.LabeledPredWhat4.InterpretedFloatingPointWhat4.Expr.UnaryBVWhat4.Expr.StringSeqWhat4.Expr.MATLABWhat4.Expr.AppWhat4.Expr.Builder What4.Protocol.VerilogWriter.AST$What4.Protocol.VerilogWriter.Backend'What4.Protocol.VerilogWriter.ABCVerilogWhat4.Protocol.VerilogWriterWhat4.Expr.SimplifyWhat4.Expr.GroundEvalWhat4.Solver.AdapterWhat4.Protocol.SMTWriterWhat4.Protocol.SMTLib2.ResponseWhat4.Expr.AppTheoryWhat4.Expr.VarIdentificationWhat4.Protocol.OnlineWhat4.Protocol.SMTLib2What4.Solver.Z3What4.Solver.YicesWhat4.Solver.STPWhat4.Solver.ExternalABCWhat4.Solver.DRealWhat4.Solver.CVC4What4.Solver.Boolector What4.WordMap GHC.TypeNatsNat Data.Maybe fromMaybe What4.Expr What4.Solverghc-primGHC.Prim RealWorldbaseGHC.STSTGHC.Stack.Types HasCallStack$panic-0.4.0.1-Fo4sCfDqcEkCpAt882LFEyPanic2parameterized-utils-2.1.3.0-7UVJSUXvfwv8DO3zof6bSZData.Parameterized.Classes knownRepr KnownReprGenGenEnv genChooseBool genChooseIntgenChooseInteger genGetSize AssumptionAssuming preCondition assumedProp Verifiable verifyingProperty BoolPropertyAssumptionProppropertyassuming==> chooseBool chooseInt chooseIntegergetSizetoNativeProperty$fVerifiableProperty$fVerifiableBool $fMonadGen$fApplicativeGen $fFunctorGen$fShowAssumption$fShowPropertyStringInfoRepr Char8Repr Char16Repr UnicodeReprFloatPrecisionReprFloatingPointPrecisionRepr BaseTypeRepr BaseBoolRepr BaseBVReprBaseIntegerRepr BaseRealRepr BaseFloatReprBaseStringReprBaseComplexReprBaseStructRepr BaseArrayReprPrec128Prec80Prec64Prec32Prec16FloatPrecisionBitsFloatingPointPrecisionFloatPrecision BaseArrayTypeBaseStructTypeBaseComplexTypeBaseStringType BaseFloatType BaseBVType BaseRealTypeBaseIntegerType BaseBoolTypeBaseTypeUnicodeChar16Char8 StringInfoKnownCtxarrayTypeIndicesarrayTypeResultfloatPrecisionToBVTypelemmaFloatPrecisionIsPos$fKnownReprFloatPrecisionFloatPrecisionReprFloatingPointPrecision*$fKnownReprStringInfoStringInfoReprUnicode)$fKnownReprStringInfoStringInfoReprChar16($fKnownReprStringInfoStringInfoReprChar8,$fKnownReprBaseTypeBaseTypeReprBaseArrayType-$fKnownReprBaseTypeBaseTypeReprBaseStructType.$fKnownReprBaseTypeBaseTypeReprBaseComplexType,$fKnownReprBaseTypeBaseTypeReprBaseFloatType)$fKnownReprBaseTypeBaseTypeReprBaseBVType-$fKnownReprBaseTypeBaseTypeReprBaseStringType+$fKnownReprBaseTypeBaseTypeReprBaseRealType.$fKnownReprBaseTypeBaseTypeReprBaseIntegerType+$fKnownReprBaseTypeBaseTypeReprBaseBoolType$fOrdFStringInfoStringInfoRepr&$fTestEqualityStringInfoStringInfoRepr&$fOrdFFloatPrecisionFloatPrecisionRepr.$fTestEqualityFloatPrecisionFloatPrecisionRepr$fOrdFBaseTypeBaseTypeRepr"$fTestEqualityBaseTypeBaseTypeRepr$fShowFStringInfoStringInfoRepr$fShowStringInfoRepr$fPrettyStringInfoRepr'$fShowFFloatPrecisionFloatPrecisionRepr$fShowFloatPrecisionRepr$fPrettyFloatPrecisionRepr$fShowFBaseTypeBaseTypeRepr$fShowBaseTypeRepr$fPrettyBaseTypeRepr$fHashableStringInfoRepr#$fHashableFStringInfoStringInfoRepr$fHashableFloatPrecisionRepr+$fHashableFFloatPrecisionFloatPrecisionRepr$fHashableBaseTypeRepr$fHashableFBaseTypeBaseTypeRepr FunctionName functionNamestartFunctionNamefunctionNameFromText$fPrettyFunctionName$fShowFunctionName$fIsStringFunctionName$fEqFunctionName$fOrdFunctionName$fHashableFunctionNameIndexLit IntIndexLit BVIndexLit hashIndexLit$fShowFBaseTypeIndexLit$fShowIndexLit$fHashableFBaseTypeIndexLit$fHashableIndexLit$fOrdFBaseTypeIndexLit$fTestEqualityBaseTypeIndexLit $fEqIndexLitWhat4panic$fPanicComponentWhat4ProblemFeatures noFeaturesuseLinearArithmeticuseNonlinearArithmeticuseComputableRealsuseIntegerArithmetic useBitvectorsuseExistForalluseQuantifiersuseSymbolicArrays useStructs useStringsuseFloatingPoint useUnsatCoresuseUnsatAssumptionshasProblemFeature$fEqProblemFeatures$fBitsProblemFeatures HasProgramLoc programLoc ProgramLoc plFunction plSourceLocPosdpospos_valPosition SourcePos BinaryPosOtherPos InternalPos sourcePos startOfFile ppNoFileNameinitializationLoc mkProgramLoc$fPrettyPosition$fNFDataPosition$fShowPosition $fNFDataPosd$fShowProgramLoc$fEqProgramLoc$fOrdProgramLoc $fFunctorPosd$fFoldablePosd$fTraversablePosd $fShowPosd$fEqPosd $fEqPosition $fOrdPositionRoot approximateparseYicesRoot fromYicesText$fPrettySingPoly $fPrettyRoot $fShowRoot$fFunctorSingPoly$fFoldableSingPoly$fTraversableSingPoly$fShowSingPoly readDecimalSExpSAtomSStringSAppskipSpaceOrNewline parseNextWord parseSExp parseSExpBody stringToSExp asNegAtomList asAtomList$fIsStringSExp$fEqSExp $fOrdSExp $fShowSExpGetModelResponse ModelResponseDeclareSortResponseDefineFunResponse DefineFun funSymbolfunArgs funResultSortfunDefTerm SymbolTermAsConstBVTermIntTermRatTerm StoreTermIfEqTermSortBitVec FloatingPointSymbolCheckSatResponse SatResponse UnsatResponseUnknownResponseCheckSatUnsupported CheckSatErrorArray RoundingModeRealIntBoolreadCheckSatResponsereadGetModelResponse$fIsStringParser$fMonadFailParser $fMonadParser$fCanParseInteger$fCanParseCheckSatResponse$fCanParseSymbol$fIsStringSymbol $fShowSymbol$fCanParseSort$fCanParseTerm$fCanParseModelResponse $fEqSymbol$fFunctorParser$fApplicativeParser SMTInfoFlagNameVersion ErrorBehavior InfoKeywordCommandCmdT renderTermunSortLogic builder_listqf_bv allSupportedvarSortboolSortbvSortintSortrealSort arraySortterm_appun_appbin_app namedTermtruefalsenotimpliesandorxoreq pairwise_appdistinctiteforallexists letBindernegatenumeraldecimalsubaddmuldiv./modabsleltgegttoRealtoIntisInt arrayConstselectstorebit0bit1bvbinary bvdecimal bvhexadecimalconcatextractbvnotbvandbvorbvxorbvnegbvaddbvsubbvmulbvudivbvurembvshlbvlshrbvultbvulebvslebvsltbvugebvugtbvsgebvsgtbvashrbvsdivbvsrem bvsignExtend bvzeroExtendsetLogic setOptionsetProduceModelsexit declareSort defineSort declareConst declareFun defineFunassert assertNamedcheckSatcheckSatAssumingcheckSatWithAssumptionsgetModelgetUnsatAssumptions getUnsatCoregetValueresetAssertionspushpopgetInfo getVersiongetNamegetErrorBehavior$fDataSMTInfoFlag$fEqSMTInfoFlag$fOrdSMTInfoFlag$fGenericSMTInfoFlag$fShowSMTInfoFlag$fIsStringTerm $fMonoidTerm$fSemigroupTerm SatResultSatUnsatUnknowntraverseSatResultisSatisUnsat isUnknownforgetModelAndCore$fShowSatResult$fGenericSatResult Occurrence Coefficient SemiRingBaseOrderedSemiRingReprOrderedSemiRingIntegerReprOrderedSemiRingRealRepr SemiRingReprSemiRingIntegerReprSemiRingRealReprSemiRingBVRepr BVFlavorRepr BVArithRepr BVBitsRepr SemiRingBV SemiRingRealSemiRingIntegerBVBitsBVArithSemiRingBVFlavor semiRingBaseorderedSemiRing sr_comparesr_hashWithSaltocc_oneocc_add occ_countocc_eqocc_hashWithSalt occ_comparezeroone$fHashableSemiRingRepr$fHashableFSemiRingSemiRingRepr$fHashableOrderedSemiRingRepr&$fHashableFSemiRingOrderedSemiRingRepr$fHashableBVFlavorRepr$fHashableFBVFlavorBVFlavorRepr$fOrdFSemiRingSemiRingRepr!$fOrdFSemiRingOrderedSemiRingRepr$fOrdFBVFlavorBVFlavorRepr"$fTestEqualitySemiRingSemiRingRepr)$fTestEqualitySemiRingOrderedSemiRingRepr"$fTestEqualityBVFlavorBVFlavorRepr SolverSymbolsolverSymbolAsTextSolverSymbolErrorppSolverSymbolError emptySymbol userSymbol systemSymbol safeSymbol$fShowSolverSymbolError$fShowSolverSymbol$fEqSolverSymbol$fOrdSolverSymbol$fHashableSolverSymbol AnnotatedMap annotationtoList fromAscListeqBynullempty singletonsizeinsertlookupdeletealteralterFunion unionWithunionWithKeyMaybefiltermapMaybetraverseMaybeWithKey difference mergeWithKeymergeA mergeWithKeyM $fMonoidTag$fSemigroupTag$fMeasuredTagEntry$fTraversableAnnotatedMap$fFoldableAnnotatedMap$fFunctorAnnotatedMap$fFunctorEntry$fFoldableEntry$fTraversableEntryisPow2lglgCeilctzclz rotateRight rotateLeft nextMultiplenextPow2Multiple tryIntSqrttryRationalSqrt roundAwayDomainBVDAny BVDIntervalmemberproperbvdMask genDomain genElementgenPair asSingletonuboundssboundsarithDomainDatadomainsOverlapsltultanyrangeintervalfromAscEltListzextsextshllshrashrscaleudivuremsdivsrem bitboundsunknowns fillrightpmember correct_anycorrect_uboundscorrect_sboundscorrect_singletoncorrect_overlap correct_unioncorrect_zero_extcorrect_sign_extcorrect_concatcorrect_shrink correct_trunccorrect_select correct_add correct_neg correct_not correct_mul correct_scalecorrect_scale_eq correct_udiv correct_uremcorrect_sdivRange correct_sdiv correct_srem correct_shl correct_lshr correct_ashr correct_eq correct_ult correct_sltcorrect_unknownscorrect_bitbounds $fShowDomain BVBitIntervalbitlenonempty intersectiontestBitrolrorcorrect_intersection correct_rol correct_ror correct_and correct_or correct_xorcorrect_testBitBVDXor and_scalarcorrect_and_scalarBVDomainBVDArith BVDBitwisebitwiseToXorDomainarithToXorDomainxorToBitwiseDomain asXorDomain fromXorDomain asArithDomainasBitwiseDomainbitwiseRoundAbovebitwiseRoundBetweenpopcntcorrect_arithToBitwisecorrect_bitwiseToArithcorrect_bitwiseToXorDomaincorrect_arithToXorDomaincorrect_xorToBitwiseDomaincorrect_asXorDomaincorrect_fromXorDomain correct_bra1 correct_bra2 correct_brb1 correct_brb2precise_overlapcorrect_popcnt correct_ctz correct_clz$fShowBVDomainComplex:+realPartimagPart complexNegate complexAdd complexSub complexMul complexDiv complexRecip magnitude magnitudeSq tryMagnitudetryComplexSqrtcomplexAsRational$fRealFracComplex$fFloatingComplex$fFractionalComplex $fRealComplex $fNumComplex $fShowComplex$fPolyEqComplexComplex$fHashableComplex$fTraversableComplex $fEqComplex $fOrdComplex$fFoldableComplex$fFunctorComplex$fGenericComplexEndian LittleEndian BigEndian $fEqEndian $fShowEndian $fOrdEndianexpandEnvironmentPathfindExecutableRNERNARTPRTNRTZbfStatusfppOpts toRoundModefpOptsfloatFromIntegerfloatFromRationalfloatToRationalfloatToIntegerfloatRoundToInt$fHashableRoundingMode$fEqRoundingMode$fGenericRoundingMode$fOrdRoundingMode$fShowRoundingMode$fEnumRoundingMode HandleReaderhrChanhrHandle hrThreadIdteeInputStreamteeOutputStreamlineBufferedOutputStreamdemuxProcessHandles streamLinesstartHandleReaderstopHandleReaderwithHandleReader readNextLine readAllLinesIncrHash mkIncrHash toIncrHashtoIncrHashWithSalt$fHashableIncrHash$fMonoidIncrHash$fSemigroupIncrHash $fEqIncrHash $fOrdIncrHash BoolMapView BoolMapUnitBoolMapDualUnit BoolMapTermsBoolMapWrapunWrapPolarityPositiveNegativenegatePolarity traverseVars viewBoolMapisInconsistentisNullvaraddVarfromVarscombinecontainsreversePolarities removeVar$fHashablePolarity$fHashableWrap $fOrdWrap$fEqWrap$fHashableBoolMap $fEqBoolMap $fEqPolarity $fOrdPolarity$fShowPolarityLeqMapfindMaxfindMinmapKeysMonotonicsplitLeq splitEntrylookupLElookupGElookupLTlookupGTfilterGtfilterLt foldlWithKey'keysminViewWithKey deleteFindMin deleteFindMax toDescListfromDistinctAscListfromDistinctDescList$fTraversableLeqMap$fFoldableLeqMap$fFunctorLeqMap $fEqLeqMapMonadSTliftST$fMonadSTsWriterT$fMonadSTsWriterT0$fMonadSTsStateT$fMonadSTsStateT0$fMonadSTsReaderT$fMonadSTsContT $fMonadSTsST$fMonadSTRealWorldIO OnlyIntReprtoBaseTypeRepr$fHashableFBaseTypeOnlyIntRepr$fHashableOnlyIntRepr!$fTestEqualityBaseTypeOnlyIntReprlogErrorStream SolverBoundslowerupper recommendedveremptySolverBoundsparseSolverBoundscomputeDefaultSolverBounds$fLiftLiftedRepSolverBounds$fLiftLiftedRepVersion$fLiftLiftedRepVUnit Word16StringfromLEByteStringtoLEByteStringindexdroptakeappendlengthfoldl' findSubstring isInfixOf isPrefixOf isSuffixOf$fHashableWord16String$fShowWord16String$fOrdWord16String$fEqWord16String$fMonoidWord16String$fSemigroupWord16String StringLiteralUnicodeLiteral Char8Literal Char16LiteralstringLiteralInfofromUnicodeLit fromChar8Lit fromChar16LitstringLitLengthstringLitEmpty stringLitNullstringLitContainsstringLitIsPrefixOfstringLitIsSuffixOfstringLitSubstringstringLitIndexOfstringLitBounds$fIsStringStringLiteral$fSemigroupStringLiteral$fHashableStringLiteral"$fHashableFStringInfoStringLiteral$fShowStringLiteral$fShowFStringInfoStringLiteral$fOrdStringLiteral$fOrdFStringInfoStringLiteral$fEqStringLiteral%$fTestEqualityStringInfoStringLiteral AbstractableavJoin avOverlap avCheckEqConcreteValueWrapperunwrapCV ConcreteValueAbstractValueWrapperunwrapAV HasAbsValue getAbsValue AbstractValueStringAbstractValue StringAbs_stringAbsLengthRealAbstractValueRAVravRange ravIsInteger ValueRange SingleRange MultiRange ValueBound Unbounded Inclusive minValueBound maxValueBound intAbsRange intDivRange intModRangeaddRangerangeScalarMul negateRangemulRange rangeLowBound rangeHiBound joinRange rangeCheckEq rangeCheckLeunboundedRange concreteRange singleRange valueRange asSingleRangemapRange ravUnbounded ravSingleravConcreteRangeravAdd ravScalarMulravMulravJoin ravCheckEq ravCheckLeabsAndabsOrrangeMaxrangeMin stringAbsTopstringAbsEmpty stringAbsJoinstringAbsSinglestringAbsOverlapstringAbsConcatstringAbsSubstringstringAbsContainsstringAbsIsPrefixOfstringAbsIsSuffixOfstringAbsIndexOfstringAbsLengthavTopavSinglewithAbstractable avContains$fMonadValueBound$fApplicativeValueBound$fAbstractableBaseStructType$fAbstractableBaseArrayType$fAbstractableBaseComplexType$fAbstractableBaseFloatType$fAbstractableBaseBVType$fAbstractableBaseRealType$fAbstractableBaseIntegerType$fAbstractableBaseStringType$fAbstractableBaseBoolType$fFunctorValueBound$fShowValueBound$fEqValueBound$fOrdValueBoundSemiRingProductprodRepr WeightedSumsumReprTm sumAbsValue sumOffset asConstantisZero asAffineVar asWeightedVarasVarconstanttraverseCoeffstraverseProdVars scaledVaraddVars addConstant fromTerms transformSumevalMevalreduceIntSumMod extractCommonnullProd asProdVar prodAbsValue prodContainsprodVarprodMulprodEval prodEvalM$fSemigroupSRAbsValue$fHashableWrapF $fEqWrapF $fOrdWrapF$fSemigroupNote$fSemigroupProdNote$fHashableWeightedSum!$fTestEqualitySemiRingWeightedSum$fHashableSemiRingProduct%$fTestEqualitySemiRingSemiRingProductArrayUpdateMaparrayUpdateAbstraverseArrayUpdateMapmergeMkeysSettoMap$fSemigroupArrayUpdateNote$fHashableArrayUpdateMap$fEqArrayUpdateMap ConcreteVal ConcreteBoolConcreteInteger ConcreteRealConcreteStringConcreteComplex ConcreteBVConcreteStruct ConcreteArrayfromConcreteBoolfromConcreteIntegerfromConcreteRealfromConcreteComplexfromConcreteStringfromConcreteBV concreteType$fShowConcreteVal$fShowFBaseTypeConcreteVal ppConcrete$fOrdConcreteVal$fOrdFBaseTypeConcreteVal$fEqConcreteVal!$fTestEqualityBaseTypeConcreteVal ConfigValue OptGetFailure OptSetFailureOpt getMaybeOpt trySetOptsetOptgetOptConfigOptCreateFailure ConfigDescBound Exclusive OptionStyleopt_type opt_onsetopt_helpopt_default_value OptionSettingoptionSettingName getOptionOptionSetResultoptionSetErroroptionSetWarnings ConfigOption configOptionconfigOptionNamePartsconfigOptionNameconfigOptionTextconfigOptionTypeoptOKoptErroptWarn set_opt_onsetset_opt_default boolOptSty realOptSty integerOptSty stringOptStyrealWithRangeOptStyrealWithMinOptStyrealWithMaxOptStyintegerWithRangeOptStyintegerWithMinOptStyintegerWithMaxOptSty enumOptSty listOptSty deprecatedOptexecutablePathOptStymkOptoptoptVoptUoptUVcopyOpt initialConfig extendConfig verbosityverbosityLoggercheckOptSetResult setUnicodeOpt setIntegerOpt setBoolOptgetOptionSettinggetOptionSettingFromTextgetConfigValues configHelp$fShowConfigOption$fMonoidOptionSetResult$fSemigroupOptionSetResult$fShowFBaseTypeOptionSetting$fShowOptionSetting$fShowConfigDesc$fShowOptCreateFailure$fExceptionOptCreateFailure$fShowOptSetFailure$fExceptionOptSetFailure $fShowOptRef$fShowOptGetFailure$fExceptionOptGetFailure$fOptBaseRealTypeRatio$fOptBaseBoolTypeBool$fOptBaseIntegerTypeInteger$fOptBaseStringTypeText$fPrettyConfigValueresolveSolverPathfindSolverPathwithProcessHandlescleanupProcess startProcess filterAsync Statistics statAllocsstatNonLinearOps SymEncodersymEncoderType symFromExpr symToExprIsSymExprBuilder freshConstant freshLatchfreshBoundedBVfreshBoundedSBVfreshBoundedIntfreshBoundedReal freshBoundVarvarExpr forallPred existsPred definedFninlineDefineFunfreshTotalUninterpFn applySymFn InvalidRange UnfoldPolicy NeverUnfold AlwaysUnfoldUnfoldConcreteIsSymFn fnArgTypes fnReturnTypeSymFn IsExprBuildergetConfigurationsetSolverLogListenergetSolverLogListenerlogSolverEvent getStatisticsgetCurrentProgramLocsetCurrentProgramLocisEq baseTypeIte annotateTerm getAnnotationtruePred falsePrednotPredandPredorPred impliesPredxorPredeqPreditePredintLitintNegintAddintSubintMulintMinintMaxintIteintEqintLeintLtintAbsintDivintMod intDivisiblebvLitbvConcatbvSelectbvNegbvAddbvSubbvMulbvUdivbvUrembvSdivbvSrem testBitBVbvIsNegbvItebvEqbvNebvUltbvUlebvUgebvUgtbvSltbvSgtbvSlebvSge bvIsNonzerobvShlbvLshrbvAshrbvRolbvRorbvZextbvSextbvTrunc bvAndBitsbvOrBits bvXorBits bvNotBitsbvSetbvFill minUnsignedBV maxUnsignedBV maxSignedBV minSignedBV bvPopcountbvCountLeadingZerosbvCountTrailingZeros addUnsignedOF addSignedOF subUnsignedOF subSignedOFcarrylessMultiplyunsignedWideMultiplyBV mulUnsignedOFsignedWideMultiplyBV mulSignedOFmkStruct structFieldstructEq structIte constantArray arrayFromFnarrayMap arrayUpdate arrayLookup arrayFromMaparrayUpdateAtIdxLitsarrayItearrayEqallTrueEntriesarrayTrueOnEntries integerToReal bvToInteger sbvToIntegerpredToBV uintToReal sbvToReal realRound realRoundEven realFloorrealCeil realTrunc integerToBV realToIntegerrealToBV realToSBVclampedIntToSBVclampedIntToBV intSetWidth uintSetWidth intToUInt uintToInt stringEmpty stringLitstringEq stringIte stringConcatstringContainsstringIsPrefixOfstringIsSuffixOf stringIndexOf stringLengthstringSubstringrealZerorealLitsciLitrealEqrealNerealLerealLtrealGerealGtrealIterealMinrealMaxrealNegrealAddrealMulrealSubrealSqrealDivrealMod isInteger realIsNonNegrealSqrt realAtan2realPirealLogrealExprealSinrealCosrealTanrealSinhrealCoshrealTanhrealAbs realHypot floatPZero floatNZerofloatNaN floatPInf floatNInffloatLitRationalfloatLitfloatNegfloatAbs floatSqrtfloatAddfloatSubfloatMulfloatDivfloatRemfloatMinfloatMaxfloatFMAfloatEqfloatNe floatFpEq floatFpApartfloatFpUnorderedfloatLefloatLtfloatGefloatGt floatIsNaN floatIsInf floatIsZero floatIsPos floatIsNegfloatIsSubnorm floatIsNormfloatIte floatCast floatRoundfloatFromBinary floatToBinary bvToFloat sbvToFloat realToFloat floatToBV floatToSBV floatToReal mkComplex getRealPart getImagPart cplxGetParts mkComplexLit cplxFromRealcplxItecplxNegcplxAddcplxSubcplxMulcplxMagcplxSqrtcplxSincplxCoscplxTan cplxHypot cplxRound cplxFloorcplxCeilcplxConjcplxExpcplxEqcplxNeSymNatSolverEndSATQuerySolverEndSATQueryRecsatQueryResult satQueryErrorSolverStartSATQuerySolverStartSATQueryRecsatQuerySolverNamesatQueryReason SolverEventArrayResultWrapperunwrapArrayResultIsExprasConstantPred asInteger integerBounds asRationalasFloatrationalBounds asComplexasBVunsignedBVBoundssignedBVBoundsasString stringInfoasConstantArrayasStructexprTypebvWidthfloatPrecision printSymExpr SymAnnotationBoundVarSymExpr SymStringSymBVSymArray SymStructSymCplxSymFloatSymReal SymIntegerPreditePredMasNatnatLitnatAddnatSubnatMulnatDivnatModnatItenatEqnatLenatLt natToIntegerbvToNat natToReal integerToNat realToNatfreshBoundedNatfreshNat printSymNat bvJoinVector bvSplitVectorbvSwap bvBitreverseindexLititeMiteList shouldUnfoldbaseIsConcretebaseDefaultValue backendPred mkRationalmkReal predToRealcplxExprAsRationalcplxExprAsIntegerrationalAsIntegerrealExprAsIntegerandAllOforOneOf isNonZeroisRealcplxDivcplxLog cplxLogBase asConcrete concreteToSymmuxRangezeroStatistics%$fHashableFBaseTypeArrayResultWrapper($fTestEqualityBaseTypeArrayResultWrapper$fHashableSymNat $fOrdSymNat $fEqSymNat$fShowInvalidRange$fExceptionInvalidRange$fShowStatistics$fEqUnfoldPolicy$fOrdUnfoldPolicy$fShowUnfoldPolicy$fShowSolverEvent$fGenericSolverEvent$fShowSolverEndSATQuery$fGenericSolverEndSATQuery$fShowSolverStartSATQuery$fGenericSolverStartSATQuerySWordDBVZBVbvAsSignedIntegerbvAsUnsignedIntegerfreshBVbvAtBEbvAtLEbvSetBEbvSetLEbvJoin bvSliceBE bvSliceLE bvUnpackBE bvUnpackLEbvPackBEbvPackLEbvNotbvAndbvOrbvXorbvForallbvUDivbvURembvSDivbvSRembvLg2 $fShowSWord SFloatRelSFloatBinArith FPTypeError fpExpectedfpActualUnsupportedFloatfpWho exponentBits precisionBitsSFloatfpReprfpReprOffpSizefpAsLitfpFreshfpNaNfpPosInffpNegInf fpFromLitfpFromRationalLit fpFromBinary fpToBinaryfpNegfpAbsfpSqrtfpAddfpSubfpMulfpDivfpMinfpMaxfpFMAfpItefpEqfpEqIEEEfpLtIEEEfpGtIEEEfpRoundfpToReal fpFromReal fpFromIntegerfpFromRational fpToRationalfpIsInffpIsNaNfpIsZerofpIsNeg fpIsSubnormfpIsNorm$fExceptionUnsupportedFloat$fExceptionFPTypeError$fShowFPTypeError$fShowUnsupportedFloatPartial _partialPred _partialValue $fDataPartial $fEqPartial$fFunctorPartial$fGenericPartial$fGeneric1TYPEPartial$fFoldablePartial$fTraversablePartial $fOrdPartial $fShowPartial partialPred partialValue$fBifunctorPartial$fBifoldablePartial$fBitraversablePartial $fEq1Partial $fEq2Partial $fOrd1Partial $fOrd2Partial$fShow1PartialPartialWithErrNoErrErr$fShow2Partial$fDataPartialWithErr$fEqPartialWithErr$fFunctorPartialWithErr$fGenericPartialWithErr$fGeneric1TYPEPartialWithErr$fFoldablePartialWithErr$fTraversablePartialWithErr$fOrdPartialWithErr$fShowPartialWithErr$fBifunctorPartialWithErr$fBifoldablePartialWithErr$fBitraversablePartialWithErr$fEq1PartialWithErr$fEq2PartialWithErr$fOrd1PartialWithErr$fOrd2PartialWithErr$fShow1PartialWithErrPartialT unPartialPartExprPE UnassignedmkPE justPartExpr maybePartExpr joinMaybePE mergePartial mergePartials runPartialTreturnUnassigned returnMaybe returnPartial addCondition$fShow2PartialWithErr$fMonadIOPartialT$fMonadTransPartialT$fMonadFailPartialT$fMonadPartialT$fApplicativePartialT$fFunctorPartialT LabeledPred _labeledPred_labeledPredMsg$fEqLabeledPred$fDataLabeledPred$fFunctorLabeledPred$fGenericLabeledPred$fGeneric1TYPELabeledPred$fOrdLabeledPred$fBifunctorLabeledPred$fBifoldableLabeledPred$fBitraversableLabeledPred$fEq1LabeledPred$fEq2LabeledPred$fOrd1LabeledPred$fOrd2LabeledPred$fShow1LabeledPred labeledPredlabeledPredMsgpartitionByPredsMpartitionByPredspartitionLabeledPreds$fShow2LabeledPred FloatInfoRepr HalfFloatReprSingleFloatReprDoubleFloatRepr QuadFloatReprX86_80FloatReprDoubleDoubleFloatReprDoubleDoubleFloat X86_80Float QuadFloat DoubleFloat SingleFloat HalfFloat FloatInfo2$fKnownReprFloatInfoFloatInfoReprDoubleDoubleFloat,$fKnownReprFloatInfoFloatInfoReprX86_80Float*$fKnownReprFloatInfoFloatInfoReprQuadFloat,$fKnownReprFloatInfoFloatInfoReprDoubleFloat,$fKnownReprFloatInfoFloatInfoReprSingleFloat*$fKnownReprFloatInfoFloatInfoReprHalfFloat IsInterpretedFloatSymExprBuilderfreshFloatConstantfreshFloatLatchfreshFloatBoundVarIsInterpretedFloatExprBuilder iFloatPZero iFloatNZero iFloatNaN iFloatPInf iFloatNInfiFloatLitRationaliFloatLitSingleiFloatLitDoubleiFloatLitLongDouble iFloatNeg iFloatAbs iFloatSqrt iFloatAdd iFloatSub iFloatMul iFloatDiv iFloatRem iFloatMin iFloatMax iFloatFMAiFloatEqiFloatNe iFloatFpEq iFloatFpApartiFloatLeiFloatLtiFloatGeiFloatGt iFloatIsNaN iFloatIsInf iFloatIsZero iFloatIsPos iFloatIsNegiFloatIsSubnorm iFloatIsNorm iFloatIte iFloatCast iFloatRoundiFloatFromBinaryiFloatToBinary iBVToFloat iSBVToFloat iRealToFloat iFloatToBV iFloatToSBV iFloatToRealiFloatBaseTypeReprSymInterpretedFloatSymInterpretedFloatType X86_80ValFloatInfoToBitWidthFloatPrecisionToInfoFloatInfoToPrecisionfloatInfoToPrecisionReprfloatPrecisionToInfoReprfloatInfoToBVTypeRepr fp80ToBitsfp80ToRational$fOrdFFloatInfoFloatInfoRepr$$fTestEqualityFloatInfoFloatInfoRepr$fShowFFloatInfoFloatInfoRepr$fShowFloatInfoRepr$fPrettyFloatInfoRepr$fHashableFloatInfoRepr!$fHashableFFloatInfoFloatInfoRepr$fShowX86_80Val $fEqX86_80Val$fOrdX86_80ValUnaryBVwidth traversePredsunsignedRangesunsignedEntriesevaluate sym_evaluate instantiatedomainmuxneguexttrunc$fHashableUnaryBV$fTestEqualityNatUnaryBV StringSeqStringSeqEntryStringSeqLiteral StringSeqTerm stringSeqAbstraverseStringSeq$fMonoidStringSeqNote$fSemigroupStringSeqNote%$fMeasuredStringSeqNoteStringSeqEntry$fHashableStringSeq$fHashableFStringInfoStringSeq $fEqStringSeq!$fTestEqualityStringInfoStringSeqMatlabSolverFnBoolOrFn IsIntegerFnIntLeFn BVToIntegerFnSBVToIntegerFnIntegerToRealFnRealToIntegerFnPredToIntegerFnIntSeqFn RealSeqFnIndicesInRangeIsEqFn BVIsNonZeroFnClampedIntNegFnClampedIntAbsFnClampedIntAddFnClampedIntSubFnClampedIntMulFnClampedUIntAddFnClampedUIntSubFnClampedUIntMulFn IntSetWidthFnUIntSetWidthFn UIntToIntFn IntToUIntFnRealIsNonZeroFn RealCosFn RealSinFn RealToSBVFn RealToUBVFn PredToBVFnCplxIsNonZeroFn CplxIsRealFnRealToComplexFnRealPartOfCplxFnImagPartOfCplxFn CplxNegFn CplxAddFn CplxSubFn CplxMulFn CplxRoundFn CplxFloorFn CplxCeilFn CplxMagFn CplxSqrtFn CplxExpFn CplxLogFn CplxLogBaseFn CplxSinFn CplxCosFn CplxTanFn clampedIntAdd clampedIntSub clampedIntMul clampedIntNeg clampedIntAbsclampedUIntAddclampedUIntSubclampedUIntMulMatlabSymbolicArrayBuildermkMatlabSolverFntraverseMatlabSolverFnmatlabSolverArgTypesmatlabSolverReturnTypeppMatlabSolverFntestSolverFnEqevalMatlabSolverFn$fHashableMatlabSolverFn ExprSymFnsymFnId symFnName symFnInfosymFnLoc SymFnInfoUninterpFnInfo DefinedFnInfoMatlabSolverFnInfoNonceApp AnnotationForallExists ArrayFromFn MapOverArraysArrayTrueOnEntriesFnApp ExprBoundVarBVarbvarIdbvarLocbvarNamebvarTypebvarKindbvarAbstractValueVarKindQuantifierVarKind LatchVarKindUninterpVarKindAppBaseIteBaseEqNotPredConjPred SemiRingSum SemiRingProd SemiRingLe RealIsIntegerIntDivIntModIntAbs IntDivisibleRealDivRealSqrtPiRealSinRealCos RealATan2RealSinhRealCoshRealExpRealLog BVTestBitBVSltBVUltBVOrBits BVUnaryTermBVConcatBVSelectBVFillBVUdivBVUremBVSdivBVSremBVShlBVLshrBVAshrBVRolBVRorBVZextBVSext BVPopcountBVCountTrailingZerosBVCountLeadingZerosFloatNegFloatAbs FloatSqrtFloatAddFloatSubFloatMulFloatDivFloatRemFloatFMA FloatFpEqFloatLeFloatLt FloatIsNaN FloatIsInf FloatIsZero FloatIsPos FloatIsNegFloatIsSubnorm FloatIsNorm FloatCast FloatRoundFloatFromBinary FloatToBinary BVToFloat SBVToFloat RealToFloat FloatToBV FloatToSBV FloatToRealArrayMap ConstantArray UpdateArray SelectArray IntegerToReal RealToInteger BVToInteger SBVToInteger IntegerToBV RoundReal RoundEvenReal FloorRealCeilRealCplxRealPartImagPartStringContainsStringIsPrefixOfStringIsSuffixOf StringIndexOfStringSubstring StringAppend StringLength StructCtor StructFieldBVOrSetBVOrNoteExprSemiRingLiteralBoolExpr FloatExpr StringExprAppExpr NonceAppExpr BoundVarExpr AppExprCtor appExprId appExprLoc appExprAppappExprAbsValueNonceAppExprCtor nonceExprId nonceExprLoc nonceExprAppnonceExprAbsValue PrettyApp PrettyArg PrettyText PrettyFuncSplitPPExprList PPExprOptsppExpr_maxWidthppExpr_useDecimalPPExpr FixedPPExpr AppPPExprAPEapeIndexapeLocapeNameapeExprs apeLength BoundVarMapOccurrenceTablePPIndex ExprPPIndex RatPPIndex SemiRingView SR_ConstantSR_SumSR_Prod SR_GeneralCplxExprRealExpr IntegerExprBVExprDummy traverseAppappEqFhashAppisNonLinearApptraverseArrayResultWrapper$traverseArrayResultWrapperAssignmentasApp asNonceAppexprLocmkExpriteSize asSemiRingLit asSemiRingSumasSemiRingProd viewSemiRing asWeightedSum asConjunction asDisjunction asPosAtom asNegAtom exprAbsValue compareExprsameTermcountOccurrences incOccurrencecountOccurrences'cache boundVars boundVars'apeDoc textPPExpr stringPPExpr ppExprLengthparenIf ppExprDocdefaultPPExprOptsppExpr ppExprTopfindExprToRemoveppExpr' symFnArgTypessymFnReturnTypeasMatlabSolverFntestExprSymFnEqtraverseBVOrSet bvOrInsert bvOrSingleton bvOrContains bvOrUnion bvOrToListbvOrAbs nonceAppTypeappTypeunconstrainedAbsValue quantAbsEval abstractEval reduceAppppVar ppBoundVar ppVarTypeCode exprPrettyArgexprPrettyIndicesstringPrettyArg showPrettyArg prettyApp ppNonceAppppApp' $fShowApp$fShowFBaseTypeExprBoundVar$fShowExprBoundVar$fHashableBVOrSet $fEqBVOrSet$fSemigroupBVOrNote$fIsSymFnExprSymFn$fHashableExprSymFn$fShowExprSymFn$fHashableFBaseTypeExprBoundVar$fHashableExprBoundVar$fOrdFBaseTypeExprBoundVar$fOrdExprBoundVar"$fTestEqualityBaseTypeExprBoundVar$fEqExprBoundVar$fShowFBaseTypeExpr $fPrettyExpr $fShowExpr$fHashableFBaseTypeExpr$fHashableExpr $fOrdExpr$fEqExpr$fOrdFBaseTypeExpr$fTestEqualityBaseTypeExpr$fOrdNonceAppExpr$fEqNonceAppExpr$fOrdFBaseTypeNonceAppExpr"$fTestEqualityBaseTypeNonceAppExpr$fHasAbsValueExpr $fIsExprExpr$fPolyEqExprExpr'$fTraversableFCBaseTypeBaseTypeNonceApp$$fFoldableFCBaseTypeBaseTypeNonceApp#$fFunctorFCBaseTypeBaseTypeNonceApp$fHashableFBaseTypeNonceApp$fTestEqualityBaseTypeNonceApp $fEqNonceApp$fHashableFBaseTypeApp$fTestEqualityBaseTypeApp$fEqApp$fFoldableFCBaseTypeBaseTypeApp$fHasAbsValueDummy$fHashableFkDummy $fOrdFkDummy $fOrdDummy$fTestEqualitykDummy $fEqFkDummy $fEqDummy$fHashablePPIndex $fPrettyApp $fEqPPIndex $fOrdPPIndex$fGenericPPIndexIdxCache ExprBuildersbUnaryThresholdsbBVDomainRangeLimitsbCacheStartSize exprCounter sbUserState FloatModeRepr FloatIEEEReprFloatUninterpretedRepr FloatRealReprFlags FloatRealFloatUninterpreted FloatIEEE FloatMode SymbolBindingVarSymbolBindingFnSymbolBindingSymbolVarBimapemptySymbolVarBimaplookupBindingOfSymbollookupSymbolOfBinding newIdxCachelookupIdxValue lookupIdxinsertIdxValuedeleteIdxValue clearIdxCache exprMaybeId idxCacheEval idxCacheEval' curProgramLoc sbNonceExpr sbMakeExprunaryThresholdOptionbvdomainRangeLimitOptioncacheStartSizeOption cacheTermsnewExprBuildergetSymbolVarBimap stopCaching startCaching evalBoundVarsintSumrealSumbvSumbvUnary scalarMul$fOrdSymbolBinding$fEqSymbolBinding$fHashableFCtxMatlabFnWrapper $fTestEqualityCtxMatlabFnWrapper$$fTestEqualityFloatModeFloatModeRepr*$fKnownReprFloatModeFloatModeReprFloatReal3$fKnownReprFloatModeFloatModeReprFloatUninterpreted*$fKnownReprFloatModeFloatModeReprFloatIEEE$fShowFFloatModeFloatModeRepr$fShowFloatModeRepr'$fMatlabSymbolicArrayBuilderExprBuilder-$fIsInterpretedFloatSymExprBuilderExprBuilder$fIsSymExprBuilderExprBuilder*$fIsInterpretedFloatExprBuilderExprBuilder+$fIsInterpretedFloatExprBuilderExprBuilder0+$fIsInterpretedFloatExprBuilderExprBuilder1$fIsExprBuilderExprBuilderModuleVerilogM ModuleStatevsInputs vsOutputsvsWires vsSeenNoncesvsUsedIdentifiers vsExpCache vsBVCache vsBoolCachevsSymItemInputOutputWireAssignBVConstExpIExpBinopUnop BVRotateL BVRotateRMuxBit BitSelectConcatBVLitBoolLitLHSLHSBitIdentNotBVNotAndOrXorEqNeLtLeBVAndBVOrBVXorBVAddBVSubBVMulBVDivBVRemBVPowBVShiftLBVShiftR BVShiftRA Identifier binopTypeiexpTypeexpTypemkLetsignedbinopscalMultlitBVlitBoolunopbit bitSelectconcat2mkModuleinitModuleState runVerilogM execVerilogM addBoundInput addFreshInput addOutputaddWirefreshIdentifier addFreshWire $fOrdBVConst$fFunctorVerilogM$fApplicativeVerilogM$fMonadVerilogM$fMonadStateModuleStateVerilogM$fMonadError[]VerilogM$fMonadIOVerilogM $fEqBVConstexprToVerilogExpr moduleDoctypeDocidentDoclhsDocinputDocwireDocunopDocbinopDochexDocdecDociexpDoc rotateDocexpDoc exprsVerilog exprsToModulesimplifycount_subterms$fApplicativeOr $fFunctorOr GroundArray ArrayMapping ArrayConcreteGroundValueWrapperGVWunGVWExprRangeBindings GroundEvalFn groundEval GroundValue lookupArraydefaultValueForTypeevalGroundExprtryEvalGroundExprevalGroundNonceAppgroundEq evalGroundApp$fApplicativeMAnd $fFunctorMAndLogDatalogCallbackVerbose logVerbosity logReason logHandle SolverAdaptersolver_adapter_namesolver_adapter_config_optionssolver_adapter_check_satsolver_adapter_write_smt2 logCallbackdefaultLogDatadefaultWriteSMTLIB2FeaturesdefaultSolverAdaptersolverAdapterOptions smokeTest$fOrdSolverAdapter$fEqSolverAdapter$fShowSolverAdapter SMTReadWriter smtEvalFuns smtSatResultsmtUnsatCoreResultsmtUnsatAssumptionsResultSMTEvalFunctions smtEvalBool smtEvalBV smtEvalReal smtEvalFloatsmtEvalBvArray smtEvalStringSMTEvalBVArrayWrapperunEvalBVArrayWrapperSMTEvalBVArrayFnCollectorResultscrResult crBindingscrFreeConstants crSideConds DefineStyleFunctionDefinitionEqualityDefinition SMTWriter forallExpr existsExpr arrayConstant arraySelectcommentCommand assertCommandassertNamedCommand pushCommand popCommandpopManyCommands resetCommand checkCommandscheckWithAssumptionsCommandsgetUnsatAssumptionsCommandgetUnsatCoreCommand setOptCommanddeclareCommand defineCommanddeclareStructDatatype structCtor structProj stringTerm stringAppendresetDeclaredStructs writeCommandResponseStrictnessLenientStrictAcknowledgementAction AckAction runAckAction WriterConn smtWriterName connHandleconnInputHandlesupportFunctionDefssupportFunctionArgumentssupportQuantifiers strictParsingsupportedFeatures connStateSupportTermOpsboolExprnotExprandAllorAll.&&.||.==./= impliesExprletExprsumExprtermIntegerToRealtermRealToInteger integerTerm rationalTerm.<=.<.>.>=bvTermbvSLebvULebvSLtbvULt bvExtract bvTestBit bvSumExpr floatTerm realIsInteger realATan2smtFnApp smtFnUpdate lambdaTermfromTextArrayConstantFnTypeMap BoolTypeMapIntegerTypeMap RealTypeMap BVTypeMap FloatTypeMap Char8TypeMapComplexToStructTypeMapComplexToArrayTypeMapPrimArrayTypeMapFnArrayTypeMap StructTypeMapappapp_listnullAcknowledgementActionresetEntryStackpopEntryStackToTopentryStackHeightpushEntryStack popEntryStack newWriterConnparserStrictness addCommandaddCommandNoAck addCommands mkFreeVar bindVarAsFree assumeFormulaassumeFormulaWithNameassumeFormulaWithFreshNamefreshBoundVarNametypeMap runInSandbox mkBaseExpr mkSMTTerm mkFormulamkAtomicFormulaassumesmtExprGroundEvalFn$fTestEqualityBaseTypeTypeMap $fEqTypeMap $fShowTypeMap$fShowFBaseTypeTypeMap$fEqDefineStyle$fShowDefineStyle$fEqTermLifetime$fEqResponseStrictness$fShowResponseStrictnessSMTLib2ExceptionSMTLib2Unsupported SMTLib2ErrorSMTLib2ParseErrorSMTLib2ResponseUnrecognizedSMTLib2InvalidResponse SMTResponse AckSuccessAckUnsupportedAckErrorAckSatAckUnsat AckUnknownRspName RspVersionRspErrBehaviorRspOutOfMemoryRspRsnIncomplete RspUnkReasonAckSuccessSExp AckSkippedstrictSMTParsingstrictSMTParseOptsmtParseOptionsgetSolverResponsegetLimitedSolverResponse$fExceptionSMTLib2Exception$fShowSMTLib2Exception$fEqSMTResponse$fShowSMTResponse AppTheory BoolTheoryLinearArithTheoryNonlinearArithTheoryComputableArithTheoryBitvectorTheoryQuantifierTheory StringTheoryFloatingPointTheory ArrayTheory StructTheoryFnTheory quantTheory typeTheory appTheory $fEqAppTheory$fOrdAppTheoryScope ExistsOnly ExistsForall VarRecorderCollectedVarInfoQuantifierInfoMapQuantifierInfoBVI boundTopTerm boundQuantboundVarboundInnerTerm BoundQuant ForallBound ExistBoundproblemFeaturesuninterpConstantsexistQuantifiersforallQuantifierslatches varErrorspredicateVarInfocollectVarInforecordExprVars$fFunctorVarRecorder$fApplicativeVarRecorder$fMonadVarRecorder$fMonadFailVarRecorder$fMonadSTsVarRecorder SolverProcess solverConnsolverCleanupCallback solverHandlesolverErrorBehavior solverStderrsolverEvalFuns solverLogFn solverNamesolverEarlyUnsatsolverSupportsResetAssertionssolverGoalTimeoutSolverGoalTimeoutgetGoalTimeoutInMilliSeconds ImmediateExitContinueOnError OnlineSolverstartSolverProcessshutdownSolverProcessAnOnlineSolvergetGoalTimeoutInSeconds solverStdinsolverResponse killSolvercheckSatisfiablecheckSatisfiableWithModelreset inNewFrameinNewFrameWithVarscheckWithAssumptionscheckWithAssumptionsAndModelcheckcheckAndGetModel getSatResultSMTLib2GenericSolverdefaultSolverPathdefaultSolverArgsdefaultFeaturessupportsResetAssertionssetDefaultLogicAndOptionsnewDefaultWriter withSolverrunSolverInOverrideSession sessionWritersessionResponseWriter SMTLib2Tweaks smtlib2tweakssmtlib2exitCommandsmtlib2arrayTypesmtlib2arrayConstantsmtlib2arraySelectsmtlib2arrayUpdatesmtlib2StringSortsmtlib2StringTermsmtlib2StringLengthsmtlib2StringAppendsmtlib2StringContainssmtlib2StringIndexOfsmtlib2StringIsPrefixOfsmtlib2StringIsSuffixOfsmtlib2StringSubstringsmtlib2StructSortsmtlib2StructCtorsmtlib2StructProjsmtlib2declareStructCmd all_supportedsmtlib2Options arrayStore asSMT2Type newWriter writeCheckSat writeExit writeGetValue runCheckSat smtAckResultsmtLibEvalFunswriteDefaultSMT2 startSolvershutdownSolverdefaultSolverBoundsppSolverVersionCheckErrorppSolverVersionError nameResultqueryErrorBehavior versionResultcheckSolverVersion'checkSolverVersion$fSupportTermOpsTerm $fNumTerm$fSMTLib2Tweaks()$fSMTWriterWriter$fSMTReadWriterWriter$fEqSMTFloatPrecision$fOrdSMTFloatPrecisionZ3z3Path z3Timeout z3Options z3Adapter z3FeatureswriteZ3SMT2FilerunZ3InOverridewithZ3$fOnlineSolverWriter$fSMTLib2GenericSolverZ3$fSMTLib2TweaksZ3$fShowZ3YicesExceptionYicesUnsupported YicesErrorYicesParseError Connection yicesTypeefSolveCommand newConnection sendChecksendCheckExistsForall assertForallsetParamsetYicesParams yicesEvalBoolyicesDefaultFeatures yicesAdapter yicesPathyicesEnableMCSatyicesEnableInteractiveyicesGoalTimeout yicesOptionswriteYicesFilerunYicesInOverride$fOnlineSolverConnection$fSupportTermOpsYicesTerm$fNumYicesTerm$fSMTWriterConnection$fExceptionYicesException$fShowYicesException$fSMTReadWriterConnectionSTPstpPath stpOptions stpAdapter stpFeaturesrunSTPInOverridewithSTP$fSMTLib2GenericSolverSTP$fSMTLib2TweaksSTP $fShowSTP ExternalABCabcPath abcOptionsexternalABCAdapterwriteABCSMT2FilerunExternalABCInOverride!$fSMTLib2GenericSolverExternalABC$fSMTLib2TweaksExternalABC$fShowExternalABC DRealBindingsDReal drealPath drealOptions drealAdapterwriteDRealSMT2FilegetAvgBindingsgetBoundBindingsrunDRealInOverride$fSMTLib2TweaksDReal $fShowDRealCVC4cvc4Path cvc4Timeout cvc4Options cvc4Adapter cvc4FeatureswriteMultiAsmpCVC4SMT2FilewriteCVC4SMT2FilerunCVC4InOverridewithCVC4$fSMTLib2GenericSolverCVC4$fSMTLib2TweaksCVC4 $fShowCVC4 Boolector boolectorPathboolectorOptionsboolectorAdapterrunBoolectorInOverride withBoolectorboolectorFeatures$fSMTLib2GenericSolverBoolector$fSMTLib2TweaksBoolector$fShowBoolectorWordMap SimpleWordMap emptyWordMap muxWordMap insertWordMap lookupWordMap GHC.Typesinteger-wired-inGHC.Integer.TypeIntegerData.Parameterized.CtxCtx+*-<=Data.Type.Equality:~:Refl TestEquality testEquality#Data.Parameterized.NatRepr.InternalNatReprnatValueknownNatData.Parameterized.NatReprlemmaMul mulCancelR natRecBounded natRecStrongnatRec natFromZero natForEach withAddLeqwithAddPrefixLeq addIsLeqLeft1 dblPosIsPosaddPrefixIsLeqaddIsLeqleqSub leqAddPosleqAdd leqMulMono leqMulPos leqMulCongrisPosNat withLeqProofleqProofleqSub2leqAdd2leqTransleqRefltestLeqlessThanAsymmetriclessThanIrreflexive testNatCases testStrictLeq decideLeqwithSubMulDistribRightwithAddMulDistribRightaddMulDistribRightminusPlusCancelplusMinusCancelmul2PlusmulComm plusAssocplusCommmaxNat mkNatReprsomeNat signedClamp unsignedClamptoSigned toUnsigned maxSigned minSigned maxUnsigned minUnsigned natMultiply withDivModNatdivNatsubNataddNathalfNatincNatpredNatdecNat isZeroOrGT1 isZeroNat withKnownNatwidthValintValue IsZeroNatZeroNat NonZeroNatLeqProofNatCases NatCaseGT NatCaseLT NatCaseEQData.Parameterized.SomeSome compareNat NatComparisonNatGTNatLTNatEQGHC.Base.GHC.Real insertOptionControl.Exception.Base catchJusttryJust GHC.MaybeNothingMaybeIOControl.Monad.FailfailJustGHC.IO.Handle.FDstdin