!QR      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQ 7(c) Iago Abal, 2012 (c) David Castro, 2012BSD3WIago Abal <iago.abal@gmail.com>, David Castro <david.castro.dcp@gmail.com> Safe-Inferred +24RAn alternative to S to fake type parameters. Example: TY :: TY Integer instead of undefined :: IntegerRTRTRT A(c) Iago Abal, 2012-2013 (c) David Castro, 2012-2013BSD3WIago Abal <iago.abal@gmail.com>, David Castro <david.castro.dcp@gmail.com>None 24<UZ3 error codesVZ3 pretty-printing modesWZ3 String typeXZ3 custom error handlerY*Boolean type. It is just an alias for int.Z,Lifted Boolean type: false, undefined, true.[A parameter set for Z3.\|A solver for Z3, that is, an engine for collecting and solving constraints using a specific algorithm or set of algorithms.]>A model for the constraints asserted into the logical context.^cA kind of AST used to represent pattern and multi-patterns used to guide quantifier instantiation._CA kind of AST used to represent constant and function declarations.`1A kind of AST used to represent function symbols.a&A kind of AST used to represent types.bjAbstract syntax tree node. That is, the data-structure used in Z3 to represent terms, formulas and types.czA Lisp-link symbol. It is used to name types, constants, and functions. A symbol can be created using string or integers.d4Logical context. This is the main Z3 data-structure.e;A configuration object used to initialize logical contexts.f0Return a string describing the given error code. Reference : nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae0aba52b5738b2ea78e0d6ad67ef1f92g0Return a string describing the given error code. Reference : nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf06357c49299efb8a0bdaeb3bc96c6d6h Set an error. Reference : nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga41cf70319c4802ab7301dd168d6f5e45iRegister a Z3 error handler. Reference : nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gadaa12e9990f37b0c1e2bf1dd502dbf39j,Return the error code for the last API call. Reference : nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8ac771e68b28d2c86f40aa84889b3807k?Convert a func_decl into a string using the current print mode. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga15243dcad77f5571e28e8aa1da465675l:Convert a sort into a string using the current print mode. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf90c72f63eab298e1dd750f6a26fb945m=Convert a pattern into a string using the current print mode. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga51b048ddbbcd88708e7aa4fe1c2462d6n:Convert an AST into a string using the current print mode. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab1aa4b78298fe00b3167bf7bfd88aea3odSet the pretty-printing mode for converting ASTs to strings. The mode can be one of the following:?z3_print_smtlib_full: Print AST nodes in SMTLIB verbose format.=z3_print_low_level: Print AST nodes using a low-level format.Kz3_print_smtlib_compliant: Print AST nodes in SMTLIB 1.x compliant format.Lz3_print_smtlib2_compliant: Print AST nodes in SMTLIB 2.x compliant format. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga20d66dac19b6d6a06537843d0e25f761pReturn a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for the last call to Z3_solver_check or Z3_solver_check_assumptions on the given solver. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaed5d19000004b43dd75e487682e91b55qlRetrieve the model for the last call to Z3_solver_check or Z3_solver_check_assumptions on the given solver. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf14a54d904a7e45eecc00c5fb8a9d5c9r>Check whether the assertions in a given solver are consistent. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga000e369de7b71caa4ee701089709c526s`Add a constraint to a solver and track it using a Boolean constant, given as the last argument. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf46fb6f3aa3ef451d6be01a737697810tAdd a constraint to a solver. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga72afadf5e8b216f2c6ae675e872b8be4u$Remove all assertions from a solver. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4a4a215b9130d7980e3c393fe857335fv4Backtrack to the nth-most recent backtracking point. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga40aa98e15aceffa5be3afad2e065478aw(Create a backtracking point in a solver. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae41bebe15b1b1105f9abb8690188d1e2x4Decrement the reference counter of the given solver. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2362dcef4e9b8ede41298a50428902ffy4Increment the reference counter of the given solver. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga388e25a8b477abbd49f08c6c29dfa12dz Set the parameters for a solver. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga887441b3468a1bc605bbf564ddebf2ae{NCreate a solver for a particular logic, as given by the SMTLIB standard here: &http://smtlib.cs.uiowa.edu/logics.html Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga54244cfc9d9cd2ca8f08c3909d700628|Create a simple solver. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5735499ef0b46846c5d45982eaa0e74c}8Create an SMT solver that uses a set of builtin tactics. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5735499ef0b46846c5d45982eaa0e74c~rConvert a parameter set into a string. This function is mainly used for printing the contents of a parameter set. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga624e692e180a8b2f617156b1e1ae9722=Add a symbol parameter k with value v to the parameter set p. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac2e899a4906b6133a23fdb60ef992ec9=Add a double parameter k with value v to the parameter set p. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga11498ce4b25d294f5f89ab7ac1b74c62@Add an unsigned parameter k with value v to the parameter set p. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4974397cb652c7f7f479012eb465e250>Add a Boolean parameter k with value v to the parameter set p. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga39e3df967eaad45b343256d56c54e91c;Decrement the reference counter of the given parameter set. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae4df28ba713b81ee99abd929e32484ea;Increment the reference counter of the given parameter set. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3a91c9f749b89e1dcf1493177d395d0cCreate a Z3 (empty) parameter set. Starting at Z3 4.0, parameter sets are used to configure many components such as: simplifiers, tactics, solvers, etc. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac7f883536538ab0ad234fde58988e673Delete a model object. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0cc98d3ce68047f873e119bccaabdbee=Check whether the given logical context is consistent or not. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga72055cfbae81bd174abed32a83e50b03=Check whether the given logical context is consistent or not. Reference : nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaff310fef80ac8a82d0a51417e073ec0a-Assert a constraing into the logical context. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1a05ff73a564ae7256a2257048a4680adEvaluate the AST node t in the given model. Return Z3_TRUE if succeeded, and store the result in v. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga47d3655283564918c85bda0b423b7f67=Return numeral value, as a string of a numeric constant term. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94617ef18fa7157e1a3f85db625d2f4bTReturn Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF otherwise. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga133aaa1ec31af9b570ed7627a3c8c5a4Return the sort of an AST node. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0a4dac7e9397ff067136354cd33cb933-Return the size of the given bit-vector sort. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8fc3550edace7bc046e16d1f96ddb419Create an exists formula. Referece: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4ffce34ff9117e6243283f11d87c1407Create a forall formula. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7e975b7d7ac96de1db73d8f71166c663Create a bound variable. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1d4da8849fca699b345322f8ee1fa31e.Create a pattern for quantifier instantiation. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf15c95b66dc3b0af735774ee401a6f85!Create a numeral of a given sort. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga88a165138162a8bac401672f0a1b7891!Create a numeral of a given sort. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga42cc319787d485d9cb665d80e02d206f!Create a numeral of a given sort. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7201b6231b61421c005457206760a121!Create a numeral of a given sort. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8779204998136569c3e166c34cfd3e2cCreate a real from a fraction. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabe0bbc1e01a084a75506a62e5e6900b3!Create a numeral of a given sort. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8aca397e32ca33618d8024bff32948cAccess the array default value. Produces the default range value, for arrays that can be represented as finite maps with a default range value. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga78e89cca82f0ab4d5f4e662e5e5fba7d!map f on the the argument arrays. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9150242d9430a8c3d55d2ca3b9a4362dCreate the constant array. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga84ea6f0c32b99c70033feaa8f00e8f2dArray update.  Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae305a4f54b4a64f7e5973ae6ccb13593XArray read. The argument a is the array and i is the index of the array that gets read. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga38f423f3683379e7f597a7fe59eccb67KCreate a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflow. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga501ccc01d737aad3ede5699741717fdaCCreate a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga86f4415719d295a2f6845c70b3aaa1df4Check that bit-wise negation does not overflow when t1( is interpreted as a signed bit-vector. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae9c5d72605ddcd0e76657341eaccb6c7DCreate a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa17e7b2c33dfe2abbd74d390927ae83e@Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6480850f9fa01e14aea936c88ff184c4GCreate a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga785f8127b87e0b42130e6d8f52167d7cDCreate a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1e2b1927cf4e50000c1600d47a152947=Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga88f6b5ec876f05e0d7ba51e96c4b077f/Create an integer from the bit-vector argument t1. If  is_signed is false, then the bit-vector t1O is treated as unsigned. So the result is non-negative and in the range [0..2^N -1], where N are the number of bits in t1. If  is_signed is true, t1# is treated as a signed bit-vector. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac87b227dc3821d57258d7f53a28323d4 Create an n* bit bit-vector from the integer argument t1. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga35f89eb05df43fbd9cce7200cc1f30b5Rotate bits of t1 to the right t2 times. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabb227526c592b523879083f12aab281fRotate bits of t1 to the left t2 times. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf46f1cb80e5a56044591a76e7c89e5e7Rotate bits of t1 to the right i times. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3b94e1bf87ecd1a1858af8ebc1da4a1cRotate bits of t1 to the left i times. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4932b7d08fea079dd903cd857a52dcdaArithmetic shift right. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga674b580ad605ba1c2c9f9d3748be87c4Logical shift right. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac59645a6edadad79a201f417e4e0c512 Shift left. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8d5e776c786c1172fa0d7dfede454e1&Repeat the given bit-vector up length i. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga03e81721502ea225c264d1f556c9119dWExtend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where m% is the size of the given bit-vector. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac9322fae11365a78640baf9078c428b3RSign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m% is the size of the given bit-vector. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad29099270b36d0680bb54b560353c10e_Extract the bits high down to low from a bitvector of size m to yield a new bitvector of size n, where n = high - low + 1. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga32d2fe7563f3e6b114c1b97b205d4317"Concatenate the given bit-vectors. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae774128fa5e9ff7458a36bd10e6ca0fa%Two's complement signed greater than. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e93a985aa2a7812c7c11a2c65d7c5f0Unsigned greater than. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga063ab9f16246c99e5c1c893613927ee31Two's complement signed greater than or equal to. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeec3414c0e8a90a6aa5a23af36bf6dc5"Unsigned greater than or equal to. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gade58fbfcf61b67bf8c4a441490d3c4df.Two's complement signed less than or equal to. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab7c026feb93e7d2eab180e96f1e6255dUnsigned less than or equal to. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab738b89de0410e70c089d3ac9e696e87"Two's complement signed less than. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8ce08af4ed1fbdf08d4d6e63d171663aUnsigned less than. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5774b22e93abcaf9b594672af6c7c3c49Two's complement signed remainder (sign follows divisor). Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95dac8e6eecb50f63cb82038560e0879:Two's complement signed remainder (sign follows dividend). Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46c18a3042fca174fe659d3185693db1Unsigned remainder. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5df4298ec835e43ddc9e3e0bae690c8d!Two's complement signed division. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad240fedb2fda1c1005b8e9d3c7f3d5a0Unsigned division. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga56ce0cd61666c6f8cf5777286f590544)Standard two's complement multiplication. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6abd3dde2a1ceff1704cf7221a72258c&Standard two's complement subtraction. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga688c9aa1347888c7a51be4e46c19178e#Standard two's complement addition. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga819814e33573f3f9948b32fdc5311158&Standard two's complement unary minus. Reference: < nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0c78be00c03eda4ed6a983224ed5c7b7 Bitwise xnor. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga784f5ca36a4b03b93c67242cc94b21d6 Bitwise nor. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabf15059e9e8a2eafe4929fdfd259aadb Bitwise nand. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga96dc37d36efd658fff5b2b4df49b0e61Bitwise exclusive-or. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0a3821ea00b1c762205f73e4bc29e7d8 Bitwise or. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga77a6ae233fb3371d187c6d559b2843f5 Bitwise and. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab96e0ea55334cbcd5a0e79323b57615d>Take disjunction of bits in vector, return vector of length 1. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafd18e127c0586abf47ad9cd96895f7d2>Take conjunction of bits in vector, return vector of length 1. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaccc04f2b58903279b1b3be589b00a7d8Bitwise negation. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga36cf75c92c54c1ca633a230344f23080%Check if a real number is an integer. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaac2ad0fb04e4900fdb4add438d137ad3Coerce a real to an integer. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga759b6563ba1204aae55289009a3fdc6dCoerce an integer to a real. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7130641e614c7ebafd28ae16a7681a21 Create greater than or equal to. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad9245cbadb80b192323d01a8360fb942Create greater than. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46167b86067586bb742c0557d7babfd3Create less than or equal to. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa9a33d11096841f4e8c407f1578bc0bfCreate less than. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga58a3dc67c5de52cf599c346803ba1534.Create an AST node representing arg1 rem arg2. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2fcdb17f9039bbdaddf8a30d037bd9ff.Create an AST node representing arg1 mod arg2. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8e350ac77e6b8fe805f57efe196e7713.Create an AST node representing arg1 div arg2. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1ac60ee8307af8d0b900375914194ff3%Create an AST node representing -arg. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gadcd2929ad732937e25f34277ce4988eaCCreate an AST node representing args[0] - ... - args[num_args - 1]. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4f5fea9b683f9e674fd8f14d676cc9a9ACreate an AST node representing args[0] * ... * args[num_args-1]. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab9affbf8401a18eea474b59ad4adc890ACreate an AST node representing args[0] + ... + args[num_args-1]. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e4ac0a4e53eee0b4b0ef159ed7d0cd5CCreate an AST node representing args[0] or ... or args[num_args-1]. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga00866d16331d505620a6c515302021f9ECreate an AST node representing args[0] and ... and args[num_args-1]. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacde98ce4a8ed1dde50b9669db4838c61*Create an AST node representing t1 xor t2. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacc6d1b848032dec0c4617b594d4229ec.Create an AST node representing t1 implies t2. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac829c0e25bbbd30343bf073f7b524517*Create an AST node representing t1 iff t2. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga930a8e844d345fbebc498ac43a696042ACreate an AST node representing an if-then-else: ite(t1, t2, t3). Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94417eed5c36e1ad48bcfc8ad6e83547'Create an AST node representing not(a). Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3329538091996eb7b3dc677760a61072&Create an AST node representing l = r. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95a19ce675b70e22bb0401f7137af37c Create an AST node representing false. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5952ac17671117a02001fed6575c778d Create an AST node representing true. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae898e7380409bbc57b56cc5205ef1db7Declare and create a constant. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga093c9703393f33ae282ec5e8729354ef*Create a constant or function application. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga33a202d86bf628bfab9b6f437536cebeDeclare a constant or function. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa5c5e2602a44d5f1373f077434859ca2Create an array type Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafe617994cce1b516f46128e448c84445+Create a bit-vector type of the given size.0This type can also be seen as a machine integer. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeed000a1bbb84b6ca6fdaac6cf0c1688Create a real type. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga40ef93b9738485caed6dc84631c3c1a0Create an integer type. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6cd426ab5748653b77d389fd3eac1015Create the Boolean type. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacdc73510b69a010b71793d429015f342$Create a Z3 symbol using a C string. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafebb0d3c212927cf7834c3a20a84ecae!Delete the given logical context. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga556eae80ed43ab13e1e7dc3b38c35200/Create a context using the given configuration. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0bd93cfab4d749dd3e2f2a4416820a46Set a configuration parameter. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga001ade87a1671fe77d7e53ed0f4f1ec3&Delete the given configuration object. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5e620acf5d55d0271097c9bb97219774Values of lifted boolean typeValues of lifted boolean typeValues of lifted boolean typeZ3_bool valuesZ3_bool valuesCreate a configuration. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7d6c40d9b79fe8a8851cc8540970787fUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~     UVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~     UVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~     A(c) Iago Abal, 2012-2013 (c) David Castro, 2012-2013BSD3WIago Abal <iago.abal@gmail.com>, David Castro <david.castro.dcp@gmail.com>None +24BEF\Pretty-printing mode for converting ASTs to strings. The mode can be one of the following:?Z3_PRINT_SMTLIB_FULL: Print AST nodes in SMTLIB verbose format.=Z3_PRINT_LOW_LEVEL: Print AST nodes using a low-level format.KZ3_PRINT_SMTLIB_COMPLIANT: Print AST nodes in SMTLIB 1.x compliant format.LZ3_PRINT_SMTLIB2_COMPLIANT: Print AST nodes in SMTLIB 2.x compliant format.Solvers available in Z3.These are described at &http://smtlib.cs.uiowa.edu/logics.htmlWARNINGJ: Support for solvers is fragile, you may experience segmentation faults!LNon-linear integer arithmetic with uninterpreted sort and function symbols.ELinear real arithmetic with uninterpreted sort and function symbols. VUnquantified non-linear real arithmetic with uninterpreted sort and function symbols. RUnquantified linear real arithmetic with uninterpreted sort and function symbols. UUnquantified linear integer arithmetic with uninterpreted sort and function symbols. bDifference Logic over the integers (in essence) but with uninterpreted sort and function symbols. TUnquantified formulas over bitvectors with uninterpreted sort function and symbols.fUnquantified formulas built over a signature of uninterpreted (i.e., free) sort and function symbols.Difference Logic over the reals. In essence, Boolean combinations of inequations of the form x - y < b where x and y are real variables and b is a rational constant. Quantifier-free real arithmetic.#Quantifier-free integer arithmetic.Unquantified linear real arithmetic. In essence, Boolean combinations of inequations between linear polynomials over real variables.Unquantified linear integer arithmetic. In essence, Boolean combinations of inequations between linear polynomials over integer variables.Difference Logic over the integers. In essence, Boolean combinations of inequations of the form x - y < b where x and y are integer variables and b is an integer constant.JClosed quantifier-free formulas over the theory of fixed-size bitvectors.OClosed quantifier-free formulas over the theory of arrays with extensionality.wClosed quantifier-free linear formulas over the theory of integer arrays extended with free sort and function symbols.Closed quantifier-free formulas over the theory of bitvectors and bitvector arrays extended with free sort and function symbols.TClosed quantifier-free formulas over the theory of bitvectors and bitvector arrays.1Closed linear formulas in linear real arithmetic.|Closed formulas with free function and predicate symbols over a theory of arrays of arrays of integer index and real value.Closed linear formulas with free sort and function symbols over one- and two-dimentional arrays of integer index and real value.Closed formulas over the theory of linear integer arithmetic and arrays extended with free sort and function symbols but restricted to arrays with integer indices and values.+Z3 exceptions./!Result of a satisfiability check.3A Z3 solver engine4A Z3 parameter set. Starting at Z3 4.0, parameter sets are used to configure many components such as: simplifiers, tactics, solvers, etc.5>A model for the constraints asserted into the logical context.6eA kind of AST used to represent pattern and multi-patterns used to guide quantifier instantiation.7FA kind of Z3 AST used to represent constant and function declarations.8/Kind of AST used to represent function symbols.9Kind of Z3 AST representing types.:A Z3 AST node.;A Z3 Lisp-link symbol.<A Z3 logical context.=A Z3 configuration object.Convert Z from Z3.Base.C to /Convert Y to . * should be OK but this is more convenient.Convert  to Y.Throws a z3 error)Throw an exception if a Z3 error happened>Create a configuration. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7d6c40d9b79fe8a8851cc8540970787f?Delete a configuration. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5e620acf5d55d0271097c9bb97219774@;Run a computation using a temporally created configuration.ASet a configuration parameter. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga001ade87a1671fe77d7e53ed0f4f1ec3See: Fhttp://research.microsoft.com/en-us/um/redmond/projects/z3/config.htmlB/Create a context using the given configuration. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0bd93cfab4d749dd3e2f2a4416820a46C!Delete the given logical context. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga556eae80ed43ab13e1e7dc3b38c35200D5Run a computation using a temporally created context.E"Create a Z3 symbol using a string. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafebb0d3c212927cf7834c3a20a84ecaeF Create the Boolean type. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacdc73510b69a010b71793d429015f342G Create an integer type. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6cd426ab5748653b77d389fd3eac1015H Create a real type. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga40ef93b9738485caed6dc84631c3c1a0I+Create a bit-vector type of the given size.0This type can also be seen as a machine integer. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeed000a1bbb84b6ca6fdaac6cf0c1688JCreate an array type Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafe617994cce1b516f46128e448c84445K A Z3 functionL*Create a constant or function application. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga33a202d86bf628bfab9b6f437536cebeMDeclare and create a constant. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga093c9703393f33ae282ec5e8729354efN Create an AST node representing true. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae898e7380409bbc57b56cc5205ef1db7O Create an AST node representing false. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5952ac17671117a02001fed6575c778dP Create an AST node representing l = r. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95a19ce675b70e22bb0401f7137af37cQNThe distinct construct is used for declaring the arguments pairwise distinct. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa076d3a668e0ec97d61744403153ecf7R Create an AST node representing not(a). Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3329538091996eb7b3dc677760a61072S1Create an AST node representing an if-then-else: ite(t1, t2, t3). Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94417eed5c36e1ad48bcfc8ad6e83547T Create an AST node representing  t1 iff t2. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga930a8e844d345fbebc498ac43a696042U Create an AST node representing  t1 implies t2. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac829c0e25bbbd30343bf073f7b524517V Create an AST node representing  t1 xor t2. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacc6d1b848032dec0c4617b594d4229ecWECreate an AST node representing args[0] and ... and args[num_args-1]. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacde98ce4a8ed1dde50b9669db4838c61XCCreate an AST node representing args[0] or ... or args[num_args-1]. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga00866d16331d505620a6c515302021f9YACreate an AST node representing args[0] + ... + args[num_args-1]. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e4ac0a4e53eee0b4b0ef159ed7d0cd5ZACreate an AST node representing args[0] * ... * args[num_args-1]. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab9affbf8401a18eea474b59ad4adc890[CCreate an AST node representing args[0] - ... - args[num_args - 1]. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4f5fea9b683f9e674fd8f14d676cc9a9\%Create an AST node representing -arg. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gadcd2929ad732937e25f34277ce4988ea].Create an AST node representing arg1 div arg2. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1ac60ee8307af8d0b900375914194ff3^.Create an AST node representing arg1 mod arg2. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8e350ac77e6b8fe805f57efe196e7713_.Create an AST node representing arg1 rem arg2. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2fcdb17f9039bbdaddf8a30d037bd9ff`Create less than. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga58a3dc67c5de52cf599c346803ba1534aCreate less than or equal to. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa9a33d11096841f4e8c407f1578bc0bfbCreate greater than. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46167b86067586bb742c0557d7babfd3c Create greater than or equal to. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad9245cbadb80b192323d01a8360fb942dCoerce an integer to a real. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7130641e614c7ebafd28ae16a7681a21eCoerce a real to an integer. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga759b6563ba1204aae55289009a3fdc6df%Check if a real number is an integer. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaac2ad0fb04e4900fdb4add438d137ad3gBitwise negation. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga36cf75c92c54c1ca633a230344f23080h>Take conjunction of bits in vector, return vector of length 1. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaccc04f2b58903279b1b3be589b00a7d8i>Take disjunction of bits in vector, return vector of length 1. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafd18e127c0586abf47ad9cd96895f7d2j Bitwise and. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab96e0ea55334cbcd5a0e79323b57615dk Bitwise or. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga77a6ae233fb3371d187c6d559b2843f5lBitwise exclusive-or. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0a3821ea00b1c762205f73e4bc29e7d8m Bitwise nand. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga96dc37d36efd658fff5b2b4df49b0e61n Bitwise nor. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabf15059e9e8a2eafe4929fdfd259aadbo Bitwise xnor. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga784f5ca36a4b03b93c67242cc94b21d6p&Standard two's complement unary minus. Reference: < nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0c78be00c03eda4ed6a983224ed5c7b7q#Standard two's complement addition. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga819814e33573f3f9948b32fdc5311158r&Standard two's complement subtraction. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga688c9aa1347888c7a51be4e46c19178es)Standard two's complement multiplication. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6abd3dde2a1ceff1704cf7221a72258ctUnsigned division. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga56ce0cd61666c6f8cf5777286f590544u!Two's complement signed division. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad240fedb2fda1c1005b8e9d3c7f3d5a0vUnsigned remainder. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5df4298ec835e43ddc9e3e0bae690c8dw:Two's complement signed remainder (sign follows dividend). Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46c18a3042fca174fe659d3185693db1x9Two's complement signed remainder (sign follows divisor). Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95dac8e6eecb50f63cb82038560e0879yUnsigned less than. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5774b22e93abcaf9b594672af6c7c3c4z"Two's complement signed less than. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8ce08af4ed1fbdf08d4d6e63d171663a{Unsigned less than or equal to. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab738b89de0410e70c089d3ac9e696e87|.Two's complement signed less than or equal to. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab7c026feb93e7d2eab180e96f1e6255d}"Unsigned greater than or equal to. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gade58fbfcf61b67bf8c4a441490d3c4df~1Two's complement signed greater than or equal to. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaeec3414c0e8a90a6aa5a23af36bf6dc5Unsigned greater than. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga063ab9f16246c99e5c1c893613927ee3%Two's complement signed greater than. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e93a985aa2a7812c7c11a2c65d7c5f0"Concatenate the given bit-vectors. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae774128fa5e9ff7458a36bd10e6ca0fa_Extract the bits high down to low from a bitvector of size m to yield a new bitvector of size n, where n = high - low + 1. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga32d2fe7563f3e6b114c1b97b205d4317RSign-extend of the given bit-vector to the (signed) equivalent bitvector of size m+i, where m% is the size of the given bit-vector. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad29099270b36d0680bb54b560353c10eWExtend the given bit-vector with zeros to the (unsigned) equivalent bitvector of size m+i, where m% is the size of the given bit-vector. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac9322fae11365a78640baf9078c428b3&Repeat the given bit-vector up length i. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga03e81721502ea225c264d1f556c9119d Shift left. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8d5e776c786c1172fa0d7dfede454e1Logical shift right. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac59645a6edadad79a201f417e4e0c512Arithmetic shift right. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga674b580ad605ba1c2c9f9d3748be87c4Rotate bits of t1 to the left i times. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4932b7d08fea079dd903cd857a52dcdaRotate bits of t1 to the right i times. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3b94e1bf87ecd1a1858af8ebc1da4a1cRotate bits of t1 to the left t2 times. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf46f1cb80e5a56044591a76e7c89e5e7Rotate bits of t1 to the right t2 times. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gabb227526c592b523879083f12aab281f Create an n* bit bit-vector from the integer argument t1. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga35f89eb05df43fbd9cce7200cc1f30b5/Create an integer from the bit-vector argument t1. If  is_signed is false, then the bit-vector t1O is treated as unsigned. So the result is non-negative and in the range [0..2^N -1], where N are the number of bits in t1. If  is_signed is true, t1# is treated as a signed bit-vector. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac87b227dc3821d57258d7f53a28323d4=Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga88f6b5ec876f05e0d7ba51e96c4b077fDCreate a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1e2b1927cf4e50000c1600d47a152947GCreate a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga785f8127b87e0b42130e6d8f52167d7c@Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6480850f9fa01e14aea936c88ff184c4DCreate a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa17e7b2c33dfe2abbd74d390927ae83e4Check that bit-wise negation does not overflow when t1( is interpreted as a signed bit-vector. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae9c5d72605ddcd0e76657341eaccb6c7CCreate a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga86f4415719d295a2f6845c70b3aaa1dfKCreate a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflow. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga501ccc01d737aad3ede5699741717fdaXArray read. The argument a is the array and i is the index of the array that gets read. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga38f423f3683379e7f597a7fe59eccb67Array update.  Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae305a4f54b4a64f7e5973ae6ccb13593Create the constant array. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga84ea6f0c32b99c70033feaa8f00e8f2d!map f on the the argument arrays. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga9150242d9430a8c3d55d2ca3b9a4362dAccess the array default value. Produces the default range value, for arrays that can be represented as finite maps with a default range value. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga78e89cca82f0ab4d5f4e662e5e5fba7d!Create a numeral of a given sort. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8aca397e32ca33618d8024bff32948cCreate a numeral of sort int.Create a numeral of sort real.-Return the size of the given bit-vector sort. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8fc3550edace7bc046e16d1f96ddb419Return the sort of an AST node. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0a4dac7e9397ff067136354cd33cb933Cast a Z from Z3.Base.C to Bool.TReturn Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF otherwise. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga133aaa1ec31af9b570ed7627a3c8c5a4=Return numeral value, as a string of a numeric constant term. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94617ef18fa7157e1a3f85db625d2f4bReturn Z3Int valueReturn Z3Real value(Evaluate an AST node in the given model.6Evaluate a collection of AST nodes in the given model.Create a backtracking point. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad651ad68c7a060cbb5616349233cb10f Backtrack n backtracking points. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab2b3a542006c86c8d86dc37872f88b61-Assert a constraing into the logical context. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1a05ff73a564ae7256a2257048a4680a)Get model (logical context is consistent) Reference : nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaff310fef80ac8a82d0a51417e073ec0aDelete a model object. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0cc98d3ce68047f873e119bccaabdbee&Convert the given model into a string. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaf36d49862a8c0d20dd5e6508eef5f8af0Convert the given logical context into a string. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga165e38ddfc928f586cb738cdf6c5f216=Check whether the given logical context is consistent or not. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga72055cfbae81bd174abed32a83e50b03<Set the pretty-printing mode for converting ASTs to strings.Convert an AST to a string.Convert a pattern to a string.Convert a sort to a string.Convert a FuncDecl to a string.  !"#$%&'()*+,-./01234567 8!"9#$:%&;'(<)*=+,->?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~./0123456789:;<=  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~=<;:9876543/210>?@ABCDEFGHIJKLMNOPRSTUVWXQYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ +,-.*)('&%$#"!   *)('&%$#"! +,-./21034567 8!"9#$:%&;'(<)*=+,->?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~./0123456789:;<=7(c) Iago Abal, 2013 (c) David Castro, 2013BSD3WIago Abal <iago.abal@gmail.com>, David Castro <david.castro.dcp@gmail.com>None 24Values for Z3 options.>Configuration option.Z3 configuration.Default configuration.Append configurations.Set a configuration option.Set configuration.?Set an option.@>AB?CDEFGH@>AB?CDEFGH7(c) Iago Abal, 2013 (c) David Castro, 2013BSD3WIago Abal <iago.abal@gmail.com>, David Castro <david.castro.dcp@gmail.com>None 24B7Eval a Z3 script.4Eval a Z3 script with default configuration options."Create a Z3 symbol using a string. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gafebb0d3c212927cf7834c3a20a84ecae Create the boolean type. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacdc73510b69a010b71793d429015f342 Create the integer type. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga6cd426ab5748653b77d389fd3eac1015 Create the real type. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga40ef93b9738485caed6dc84631c3c1a0 A Z3 function*Create a constant or function application. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga33a202d86bf628bfab9b6f437536cebeDeclare and create a constant. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga093c9703393f33ae282ec5e8729354ef Create an AST node representing true. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gae898e7380409bbc57b56cc5205ef1db7 Create an AST node representing false. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga5952ac17671117a02001fed6575c778d Create an AST node representing l = r. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga95a19ce675b70e22bb0401f7137af37cNThe distinct construct is used for declaring the arguments pairwise distinct. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa076d3a668e0ec97d61744403153ecf7 Create an AST node representing not(a). Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga3329538091996eb7b3dc677760a610721Create an AST node representing an if-then-else: ite(t1, t2, t3). Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga94417eed5c36e1ad48bcfc8ad6e83547 Create an AST node representing  t1 iff t2. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga930a8e844d345fbebc498ac43a696042 Create an AST node representing  t1 implies t2. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac829c0e25bbbd30343bf073f7b524517 Create an AST node representing  t1 xor t2. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacc6d1b848032dec0c4617b594d4229ecECreate an AST node representing args[0] and ... and args[num_args-1]. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gacde98ce4a8ed1dde50b9669db4838c61CCreate an AST node representing args[0] or ... or args[num_args-1]. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga00866d16331d505620a6c515302021f9ACreate an AST node representing args[0] + ... + args[num_args-1]. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4e4ac0a4e53eee0b4b0ef159ed7d0cd5ACreate an AST node representing args[0] * ... * args[num_args-1]. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gab9affbf8401a18eea474b59ad4adc890CCreate an AST node representing args[0] - ... - args[num_args - 1]. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga4f5fea9b683f9e674fd8f14d676cc9a9%Create an AST node representing -arg. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gadcd2929ad732937e25f34277ce4988ea.Create an AST node representing arg1 div arg2. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1ac60ee8307af8d0b900375914194ff3.Create an AST node representing arg1 mod arg2. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga8e350ac77e6b8fe805f57efe196e7713.Create an AST node representing arg1 rem arg2. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga2fcdb17f9039bbdaddf8a30d037bd9ffCreate less than. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga58a3dc67c5de52cf599c346803ba1534Create less than or equal to. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaa9a33d11096841f4e8c407f1578bc0bfCreate greater than. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga46167b86067586bb742c0557d7babfd3 Create greater than or equal to. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gad9245cbadb80b192323d01a8360fb942Coerce an integer to a real. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga7130641e614c7ebafd28ae16a7681a21Coerce a real to an integer. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga759b6563ba1204aae55289009a3fdc6d%Check if a real number is an integer. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaac2ad0fb04e4900fdb4add438d137ad3!Create a numeral of a given sort. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gac8aca397e32ca33618d8024bff32948cCreate a numeral of sort int.Create a numeral of sort real.Returns  Just True,  Just False, or Nothing for  undefined. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga133aaa1ec31af9b570ed7627a3c8c5a4Return the integer valueReturn rational value(Evaluate an AST node in the given model.6Evaluate a collection of AST nodes in the given model.Create a backtracking point. Backtrack n backtracking points.-Assert a constraing into the logical context. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga1a05ff73a564ae7256a2257048a4680a Get model. Reference : nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#gaff310fef80ac8a82d0a51417e073ec0aDelete a model object. Reference: nhttp://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html#ga0cc98d3ce68047f873e119bccaabdbee&Convert the given model into a string.+Convert Z3's logical context into a string. =Check whether the given logical context is consistent or not. 3Set the mode for converting expressions to strings. Convert an AST to a string. Convert a pattern to a string. Convert a sort to a string.Convert a FuncDecl to a string.NIJKLMNOPQRSTU     Vn /01256789:;     h ;:98765/210     GIJKLMNOPQRSTU     V 7(c) Iago Abal, 2012 (c) David Castro, 2012BSD3WIago Abal <iago.abal@gmail.com>, David Castro <david.castro.dcp@gmail.com> experimentalNone  !"+2346=BKWOrdering comparisons.XEquality testing.YOperations for sort real.ZOperations for sort int.[Commutative ring operations.\Boolean variadic operations.]Boolean binary operations.^ Z3 function_ QuantifiersQuantifier pattern.Convertible types.`Quantifiable expressions. Expressions.aQuantifier layout level.bUnique identifiers.$Typeclass for Haskell Z3 numbers of real sort in Z3.$Typeclass for Haskell Z3 numbers of int sort in Z3.Numeric types.cFunction types.Types for expressions.d5Type invariant. Introduced when creating a variable.eTypecheck an expression.f(Create a sort of the underlying Z3 type.gCreate a value of the .hValue extractori Compilable things.PjklmnWopqrXstYuZvwx[yz{\|}]~^_`abcdefghiMklWopqrXstYuZvwx[yz{\|}]~^_`abcdefghijklmnWrqpoXtsYuZxwv[{zy\}|]~^_`abcdefghi 7(c) Iago Abal, 2012 (c) David Castro, 2012BSD3WIago Abal <iago.abal@gmail.com>, David Castro <david.castro.dcp@gmail.com> experimentalNone 246:BM Z3 monad.Internal state of Z3 monad.the logic to use; see &http://smtlib.cs.uiowa.edu/logics.htmlsoft timeout (in milliseconds) Z3 optionsEval a Z3 script.Eval a Z3 script.Fresh symbol name.< /fghA(c) Iago Abal, 2012-2013 (c) David Castro, 2012-2013BSD3WIago Abal <iago.abal@gmail.com>, David Castro <david.castro.dcp@gmail.com> experimentalNone !"*+2346=BKM2#A computation derived from a model./Compile while introducing TCCs into the script. Declare skolem variables.!4Declare skolem variables with a user specified name."*Declare uninterpreted function of arity 1.#*Declare uninterpreted function of arity 2.$*Declare uninterpreted function of arity 3.%*Declare uninterpreted function of arity 4.&*Declare uninterpreted function of arity 5.Declare uninterpreted function'"Make assertion in current context.(>Introduce an auxiliary declaration to name a given expression.9If you really want sharing use this instead of Haskell's let.)Convert an Expr to a string.*9Check satisfiability and evaluate a model if some exists.+9Check satisfiability and evaluate a model if some exists.,LCheck satisfiability and evaluate a model if some exists, also returning a / to the reason for any failure.-Show Z3's internal model..&Evaluate an expression within a model./4Evaluate a collection of expressions within a model.0literal constructor.1Boolean literals.2Boolean literals.3Boolean negation4Boolean binary xor.5Boolean implication6 An alias for 5.7Boolean if and only if.8 An alias for 7.9Boolean variadic and.:Boolean variadic or.;Boolean variadic distinct.<Boolean binary and.=Boolean binary or.>Universally quantified formula.?!Existentially quantified formula.@Pattern-based instantiation.A Casting between compatible typesBInteger division.CInteger modulo.DInteger remainder.E k E n == n %* k ==* 0FEquals.G Not equals.HLess or equals than.I Less than.JGreater or equals than.K Greater than.LMinimum.MMaximum.N if-then-else.T !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMN^ /  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMN^/  !"#$%&'( )*+,-./01239<:=;45678>?@BCDEFGHIJKLMNAQ !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMN45678<=BCDFGHIJK7(c) Iago Abal, 2012 (c) David Castro, 2012BSD3WIago Abal <iago.abal@gmail.com>, David Castro <david.castro.dcp@gmail.com>None 24MO3Ceiling logarithm base two. Axiomatization of the lg2: function. Most likely Z3 is going to diverge if you use lg2X to specify a satisfiable problem since it cannot construct a recursive definition for lg27, but it should work fine for unsatisfiable instances.OOOO7(c) Iago Abal, 2012 (c) David Castro, 2012BSD3WIago Abal <iago.abal@gmail.com>, David Castro <david.castro.dcp@gmail.com>None 24MP0Raise to the power of 2. Axiomatization of the 2^n: function. Most likely Z3 is going to diverge if you use 2^nY to specify a satisfiable problem, since it cannot construct a recursive definition for 2^n7, but it should work fine for unsatisfiable instances.PPPP7(c) Iago Abal, 2012 (c) David Castro, 2012BSD3WIago Abal <iago.abal@gmail.com>, David Castro <david.castro.dcp@gmail.com>None  +246=BKM QQQ Q7(c) Iago Abal, 2012 (c) David Castro, 2012BSD3WIago Abal <iago.abal@gmail.com>, David Castro <david.castro.dcp@gmail.com> experimentalNone 24_ /  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNQ  !"#$%&'()*+,-./0123456789::;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~STUVYZ[\]^_`abcdefghijklmnopqrst D          C      ! " # $ % & ' ( ) * + , - . / 0 1 2 3 4 5 6 7 8 9 : ; < = > ? @ A B C D E F G H I J K L M N O P Q R S T U V W X Y Z [ \ ] ^ _ ` a b c d e f g h i j k l m n o p q r s t u v w x y z { | } ~                                                                                              ABCDEFGHIJK                  ! " # $ % & ' ( J ) * * + , - . / 0 1 2 3 4 5 6 7 8 9 : ; < = > F ? @ A B C E D E F G H I J K L M N O P Q R S T U V W X Y Z [  Z \ ] ^ _ ` a b c d e f ^ g h i j klmmCnopqrstuvwxyz{|}~~z3-0.3.0Z3.Lang.PreludeZ3.BaseZ3.OptsZ3.Monad Z3.Lang.Lg2 Z3.Lang.Pow2 Z3.Lang.Nat Z3.Lang.TY Z3.Base.CForeigntoBool Z3.Lang.Exprs Z3.Lang.MonadZ3.LangZ3 ASTPrintModeZ3_PRINT_SMTLIB2_COMPLIANTZ3_PRINT_SMTLIB_COMPLIANTZ3_PRINT_LOW_LEVELZ3_PRINT_SMTLIB_FULLLogicUFNIAUFLRAQF_UFNRAQF_UFLRAQF_UFLIAQF_UFIDLQF_UFBVQF_UFQF_RDLQF_NRAQF_NIAQF_LRAQF_LIAQF_IDLQF_BVQF_AX QF_AUFLIAQF_AUFBVQF_ABVLRAAUFNIRAAUFLIRAAUFLIA Z3ErrorCode Z3Exception DecRefError InvalidUsage InternalFatalFileAccessError MemoutFailInvalidPatternNoParser ParserError InvalidArgIOB SortErrorZ3ErrorerrCodeerrMsgResultUndefUnsatSatSolverParamsModelPatternAppFuncDeclSortASTSymbolContextConfigmkConfig delConfig withConfig setParamValue mkContext delContext withContextmkStringSymbol mkBoolSort mkIntSort mkRealSortmkBvSort mkArraySort mkFuncDeclmkAppmkConstmkTruemkFalsemkEq mkDistinctmkNotmkItemkIff mkImpliesmkXormkAndmkOrmkAddmkMulmkSub mkUnaryMinusmkDivmkModmkRemmkLtmkLemkGtmkGe mkInt2Real mkReal2IntmkIsIntmkBvnot mkBvredand mkBvredormkBvandmkBvormkBvxormkBvnandmkBvnormkBvxnormkBvnegmkBvaddmkBvsubmkBvmulmkBvudivmkBvsdivmkBvuremmkBvsremmkBvsmodmkBvultmkBvsltmkBvulemkBvslemkBvugemkBvsgemkBvugtmkBvsgtmkConcat mkExtract mkSignExt mkZeroExtmkRepeatmkBvshlmkBvlshrmkBvashr mkRotateLeft mkRotateRightmkExtRotateLeftmkExtRotateRightmkInt2bvmkBv2intmkBvaddNoOverflowmkBvaddNoUnderflowmkBvsubNoOverflowmkBvsubNoUnderflowmkBvsdivNoOverflowmkBvnegNoOverflowmkBvmulNoOverflowmkBvmulNoUnderflowmkSelectmkStore mkConstArraymkMapmkArrayDefault mkNumeralmkIntmkReal mkPatternmkBoundmkForallmkExists getBvSortSizegetSortgetBoolgetIntgetRealevalevalTpushpop assertCnstrgetModeldelModel showModel showContextcheckmkParams paramsSetBool paramsSetUIntparamsSetDoubleparamsSetSymbolparamsToStringmkSolvermkSimpleSolvermkSolverForLogicsolverSetParams solverPush solverPop solverResetsolverAssertCnstrsolverAssertAndTrack solverChecksolverCheckAndGetModelsolverGetReasonUnknownsetASTPrintMode astToStringpatternToString sortToStringfuncDeclToStringOptValueOptsstdOpts+?optsetOptsMonadZ3 getSolver getContext evalZ3WithevalZ3 withModelPatCastableExprIsRealIsIntIsNumIsTyArgslogic softTimeoutoptionsstdArgsvarnamedVarfun1fun2fun3fun4fun5assertlet_ exprToString checkModelcheckModelWithcheckModelWithResultliteraltruefalsenot_xorimplies==>iff<=>and_or_distinct&&*||*forallexists instanceWhencast//%*%%divides==*/=*<=*<*>=*>*min_max_ite declareLg2 declarePow2NatTYbaseGHC.Err undefined Z3_error_codeZ3_ast_print_mode Z3_stringZ3_error_handlerZ3_boolZ3_lbool Z3_params Z3_solverZ3_model Z3_patternZ3_app Z3_func_declZ3_sortZ3_ast Z3_symbol Z3_context Z3_configz3_get_error_msg_exz3_get_error_msg z3_set_errorz3_set_error_handlerz3_get_error_codez3_func_decl_to_stringz3_sort_to_stringz3_pattern_to_stringz3_ast_to_stringz3_set_ast_print_modez3_solver_get_reason_unknownz3_solver_get_modelz3_solver_checkz3_solver_assert_and_trackz3_solver_assertz3_solver_reset z3_solver_popz3_solver_pushz3_solver_dec_refz3_solver_inc_refz3_solver_set_paramsz3_mk_solver_for_logicz3_mk_simple_solver z3_mk_solverz3_params_to_stringz3_params_set_symbolz3_params_set_doublez3_params_set_uintz3_params_set_boolz3_params_dec_refz3_params_inc_ref z3_mk_params z3_del_modelz3_checkz3_check_and_get_modelz3_assert_cnstrz3_evalz3_get_numeral_stringz3_get_bool_value z3_get_sortz3_get_bv_sort_size z3_mk_exists z3_mk_forall z3_mk_bound z3_mk_patternz3_mk_unsigned_int64 z3_mk_int64z3_mk_unsigned_int z3_mk_int z3_mk_real z3_mk_numeralz3_mk_array_default z3_mk_mapz3_mk_const_array z3_mk_store z3_mk_selectz3_mk_bvmul_no_underflowz3_mk_bvmul_no_overflowz3_mk_bvneg_no_overflowz3_mk_bvsdiv_no_overflowz3_mk_bvsub_no_underflowz3_mk_bvsub_no_overflowz3_mk_bvadd_no_underflowz3_mk_bvadd_no_overflow z3_mk_bv2int z3_mk_int2bvz3_mk_ext_rotate_rightz3_mk_ext_rotate_leftz3_mk_rotate_rightz3_mk_rotate_left z3_mk_bvashr z3_mk_bvlshr z3_mk_bvshl z3_mk_repeatz3_mk_zero_extz3_mk_sign_ext z3_mk_extract z3_mk_concat z3_mk_bvsgt z3_mk_bvugt z3_mk_bvsge z3_mk_bvuge z3_mk_bvsle z3_mk_bvule z3_mk_bvslt z3_mk_bvult z3_mk_bvsmod z3_mk_bvsrem z3_mk_bvurem z3_mk_bvsdiv z3_mk_bvudiv z3_mk_bvmul z3_mk_bvsub z3_mk_bvadd z3_mk_bvneg z3_mk_bvxnor z3_mk_bvnor z3_mk_bvnand z3_mk_bvxor z3_mk_bvor z3_mk_bvand z3_mk_bvredorz3_mk_bvredand z3_mk_bvnot z3_mk_is_intz3_mk_real2intz3_mk_int2realz3_mk_gez3_mk_gtz3_mk_lez3_mk_lt z3_mk_rem z3_mk_mod z3_mk_divz3_mk_unary_minus z3_mk_sub z3_mk_mul z3_mk_addz3_mk_or z3_mk_and z3_mk_xor z3_mk_implies z3_mk_iff z3_mk_ite z3_mk_notz3_mk_eq z3_mk_false z3_mk_true z3_mk_const z3_mk_appz3_mk_func_declz3_mk_array_sort z3_mk_bv_sortz3_mk_real_sortz3_mk_int_sortz3_mk_bool_sortz3_mk_string_symbolz3_del_context z3_mk_contextz3_set_param_value z3_del_config z3_l_true z3_l_false z3_l_undefz3_truez3_falsez3_invalid_usagez3_context_to_stringz3_model_to_stringz3_popz3_pushz3_mk_distinct z3_mk_configz3_print_smtlib_fullz3_print_low_levelz3_print_smtlib_compliantz3_print_smtlib2_compliantz3_ok z3_sort_errorz3_iobz3_invalid_argz3_parser_error z3_no_parserz3_invalid_patternz3_memout_failz3_file_access_errorz3_internal_fatalz3_dec_ref_error z3_exceptiontoResultghc-prim GHC.TypesBoolunBoolz3Error checkError castLBoolgetNumeralStringunSolverunParamsunModel unPattern_unApp unFuncDeclunSortunASTunSymbol unContextunConfig toZ3ErrormkIntZ3mkUnsignedIntZ3 mkInt64Z3mkUnsignedInt64Z3 mkInt_IntZ3mkInt_UnsignedIntZ3 mkInt_Int64Z3mkInt_UnsignedInt64Z3mkRealZ3 mkReal_IntZ3mkReal_UnsignedIntZ3mkReal_Int64Z3mkReal_UnsignedInt64Z3 $fShowLogic$fExceptionZ3Error $fShowZ3ErrorOptsetOptoption $fOptValue[]$fOptValueDouble$fOptValueInteger $fOptValueInt$fOptValueBool $fMonoidOptsZ3Env envSolver envContext_unZ3 liftScalarliftFun1liftFun2liftFun3liftFun4 liftSolver0 liftSolver1 $fMonadZ3Z3CmpOpICmpOpERealOpIntOpCRingOp BoolMultiOp BoolBinOpFunApp QuantifierQExprLayoutUniqIsFuntypeInvtcmkSort mkLiteralgetValue CompilableTCCTCMunTCMGtGeLtLeDistinctEqDivRemModQuotSubMulAddOrAndIffImpliesXorPAppExistsForAll compileCast compileQuantCastIteCmpICmpE RealArithIntArith CRingArithNegQuant BoolMultiBoolBinNotTagConstLitdomainrangecompileokwithHyponewTCCevalTCM typecheckZ3StatefreshuniqValcontextsolverqLayoutsetArgs getQLayout deBruijnIx newQLayout mkBoolBin mkBoolMultimkQuantmkCmp mkCRingArith mkIntArith mkRealArithcompileWithTCCfunDeclQBody createVartcBool compileBoolwithSortedSymbol tcIntegercompileInteger tcRationalcompileRationalapp2AST$fCompilablePattern$fCompilableFunApp $fIsFun(->) $fIsFun(->)0 $fIsRealRatio $fIsNumRatio $fIsTyRatio$fCompilableExpr$fIsIntInteger$fIsNumInteger $fIsTyInteger$fCompilableExpr0 $fQExpr(->) $fQExpr(->)0 $fQExpr(->)1 $fIsTyBool$fCompilableExpr1$fCastableRatioInteger$fCastableIntegerRatio$fFractionalExpr $fNumExprunNattcNat compileNat$fCastableNatInteger $fIsIntNat $fIsNumNat $fIsTyNat $fIntegralNat$fNumNat $fShowNat