cl-z3/ffi

System Information

Dependencies:

cffi-grovel
cffi

Definition Index

Z3-C-TYPES
Low-level Z3 types
- EXTERNAL CLASS
  Z3_APP
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_APPLY_RESULT
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_AST
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_AST_MAP
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_AST_VECTOR
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_CONFIG
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_CONSTRUCTOR
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_CONSTRUCTOR_LIST
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_CONTEXT
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_FIXEDPOINT
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_FUNC_DECL
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_FUNC_ENTRY
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_FUNC_INTERP
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_GOAL
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_MODEL
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_OPTIMIZE
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_PARAMS
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_PARAM_DESCRS
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_PATTERN
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_PROBE
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_RCF_NUM
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_SOLVER
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_SOLVER_CALLBACK
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_SORT
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_STATS
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_SYMBOL
  
  Source
  No documentation provided.
- EXTERNAL CLASS
  Z3_TACTIC
  
  Source
  No documentation provided.
Z3-C
Bound low-level Z3 C API functions.
- EXTERNAL FUNCTION
  Z3-ADD-CONST-INTERP
  
  C
  
  M
  
  F
  
  A
  
  Source
  Add a constant interpretation.
- EXTERNAL FUNCTION
  Z3-ADD-FUNC-INTERP
  
  C
  
  M
  
  F
  
  DEFAULT-VALUE
  
  Source
  Create a fresh func_interp object, add it to a model for a specified function. It has reference count 0.
- EXTERNAL FUNCTION
  Z3-ADD-REC-DEF
  
  C
  
  F
  
  N
  
  ARGS
  
  BODY
  
  Source
  Define the body of a recursive function.
- EXTERNAL FUNCTION
  Z3-ALGEBRAIC-ADD
  
  C
  
  A
  
  B
  
  Source
  Return the value a + b.
- EXTERNAL FUNCTION
  Z3-ALGEBRAIC-DIV
  
  C
  
  A
  
  B
  
  Source
  Return the value a / b.
- EXTERNAL FUNCTION
  Z3-ALGEBRAIC-EQ
  
  C
  
  A
  
  B
  
  Source
  Return true if a == b, and false otherwise.
- EXTERNAL FUNCTION
  Z3-ALGEBRAIC-EVAL
  
  C
  
  P
  
  N
  
  A
  
  Source
  Given a multivariate polynomial p(x_0, ..., x_{n-1}), return the sign of p(a[0], ..., a[n-1]).
- EXTERNAL FUNCTION
  Z3-ALGEBRAIC-GE
  
  C
  
  A
  
  B
  
  Source
  Return true if a >= b, and false otherwise.
- EXTERNAL FUNCTION
  Z3-ALGEBRAIC-GET-I
  
  C
  
  A
  
  Source
  Return which root of the polynomial the algebraic number represents.
- EXTERNAL FUNCTION
  Z3-ALGEBRAIC-GET-POLY
  
  C
  
  A
  
  Source
  Return the coefficients of the defining polynomial.
- EXTERNAL FUNCTION
  Z3-ALGEBRAIC-GT
  
  C
  
  A
  
  B
  
  Source
  Return true if a > b, and false otherwise.
- EXTERNAL FUNCTION
  Z3-ALGEBRAIC-IS-NEG
  
  C
  
  A
  
  Source
  Return true if a is negative, and false otherwise.
- EXTERNAL FUNCTION
  Z3-ALGEBRAIC-IS-POS
  
  C
  
  A
  
  Source
  Return true if a is positive, and false otherwise.
- EXTERNAL FUNCTION
  Z3-ALGEBRAIC-IS-VALUE
  
  C
  
  A
  
  Source
  Return true if a can be used as value in the Z3 real algebraic number package.
- EXTERNAL FUNCTION
  Z3-ALGEBRAIC-IS-ZERO
  
  C
  
  A
  
  Source
  Return true if a is zero, and false otherwise.
- EXTERNAL FUNCTION
  Z3-ALGEBRAIC-LE
  
  C
  
  A
  
  B
  
  Source
  Return true if a <= b, and false otherwise.
- EXTERNAL FUNCTION
  Z3-ALGEBRAIC-LT
  
  C
  
  A
  
  B
  
  Source
  Return true if a < b, and false otherwise.
- EXTERNAL FUNCTION
  Z3-ALGEBRAIC-MUL
  
  C
  
  A
  
  B
  
  Source
  Return the value a * b.
- EXTERNAL FUNCTION
  Z3-ALGEBRAIC-NEQ
  
  C
  
  A
  
  B
  
  Source
  Return true if a != b, and false otherwise.
- EXTERNAL FUNCTION
  Z3-ALGEBRAIC-POWER
  
  C
  
  A
  
  K
  
  Source
  Return the a^k
- EXTERNAL FUNCTION
  Z3-ALGEBRAIC-ROOT
  
  C
  
  A
  
  K
  
  Source
  Return the a^(1/k)
- EXTERNAL FUNCTION
  Z3-ALGEBRAIC-ROOTS
  
  C
  
  P
  
  N
  
  A
  
  Source
  Given a multivariate polynomial p(x_0, ..., x_{n-1}, x_n), returns the roots of the univariate polynomial p(a[0], ..., a[n-1], x_n).
- EXTERNAL FUNCTION
  Z3-ALGEBRAIC-SIGN
  
  C
  
  A
  
  Source
  Return 1 if a is positive, 0 if a is zero, and -1 if a is negative.
- EXTERNAL FUNCTION
  Z3-ALGEBRAIC-SUB
  
  C
  
  A
  
  B
  
  Source
  Return the value a - b.
- EXTERNAL FUNCTION
  Z3-APP-TO-AST
  
  C
  
  A
  
  Source
  Convert a Z3_app into Z3_ast. This is just type casting.
- EXTERNAL FUNCTION
  Z3-APPEND-LOG
  
  STRING
  
  Source
  Append user-defined string to interaction log.
- EXTERNAL FUNCTION
  Z3-APPLY-RESULT-DEC-REF
  
  C
  
  R
  
  Source
  Decrement the reference counter of the given Z3_apply_result object.
- EXTERNAL FUNCTION
  Z3-APPLY-RESULT-GET-NUM-SUBGOALS
  
  C
  
  R
  
  Source
  Return the number of subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
- EXTERNAL FUNCTION
  Z3-APPLY-RESULT-GET-SUBGOAL
  
  C
  
  R
  
  I
  
  Source
  Return one of the subgoals in the Z3_apply_result object returned by Z3_tactic_apply.
- EXTERNAL FUNCTION
  Z3-APPLY-RESULT-INC-REF
  
  C
  
  R
  
  Source
  Increment the reference counter of the given Z3_apply_result object.
- EXTERNAL FUNCTION
  Z3-APPLY-RESULT-TO-STRING
  
  C
  
  R
  
  Source
  Convert the Z3_apply_result object returned by Z3_tactic_apply into a string.
- EXTERNAL FUNCTION
  Z3-AST-MAP-CONTAINS
  
  C
  
  M
  
  K
  
  Source
  Return true if the map m contains the AST key k.
- EXTERNAL FUNCTION
  Z3-AST-MAP-DEC-REF
  
  C
  
  M
  
  Source
  Decrement the reference counter of the given AST map.
- EXTERNAL FUNCTION
  Z3-AST-MAP-ERASE
  
  C
  
  M
  
  K
  
  Source
  Erase a key from the map.
- EXTERNAL FUNCTION
  Z3-AST-MAP-FIND
  
  C
  
  M
  
  K
  
  Source
  Return the value associated with the key k.
- EXTERNAL FUNCTION
  Z3-AST-MAP-INC-REF
  
  C
  
  M
  
  Source
  Increment the reference counter of the given AST map.
- EXTERNAL FUNCTION
  Z3-AST-MAP-INSERT
  
  C
  
  M
  
  K
  
  V
  
  Source
  Store/Replace a new key, value pair in the given map.
- EXTERNAL FUNCTION
  Z3-AST-MAP-KEYS
  
  C
  
  M
  
  Source
  Return the keys stored in the given map.
- EXTERNAL FUNCTION
  Z3-AST-MAP-RESET
  
  C
  
  M
  
  Source
  Remove all keys from the given map.
- EXTERNAL FUNCTION
  Z3-AST-MAP-SIZE
  
  C
  
  M
  
  Source
  Return the size of the given map.
- EXTERNAL FUNCTION
  Z3-AST-MAP-TO-STRING
  
  C
  
  M
  
  Source
  Convert the given map into a string.
- EXTERNAL FUNCTION
  Z3-AST-TO-STRING
  
  C
  
  A
  
  Source
  Convert the given AST node into a string.
- EXTERNAL FUNCTION
  Z3-AST-VECTOR-DEC-REF
  
  C
  
  V
  
  Source
  Decrement the reference counter of the given AST vector.
- EXTERNAL FUNCTION
  Z3-AST-VECTOR-GET
  
  C
  
  V
  
  I
  
  Source
  Return the AST at position i in the AST vector v.
- EXTERNAL FUNCTION
  Z3-AST-VECTOR-INC-REF
  
  C
  
  V
  
  Source
  Increment the reference counter of the given AST vector.
- EXTERNAL FUNCTION
  Z3-AST-VECTOR-PUSH
  
  C
  
  V
  
  A
  
  Source
  Add the AST a in the end of the AST vector v. The size of v is increased by one.
- EXTERNAL FUNCTION
  Z3-AST-VECTOR-RESIZE
  
  C
  
  V
  
  N
  
  Source
  Resize the AST vector v.
- EXTERNAL FUNCTION
  Z3-AST-VECTOR-SET
  
  C
  
  V
  
  I
  
  A
  
  Source
  Update position i of the AST vector v with the AST a.
- EXTERNAL FUNCTION
  Z3-AST-VECTOR-SIZE
  
  C
  
  V
  
  Source
  Return the size of the given AST vector.
- EXTERNAL FUNCTION
  Z3-AST-VECTOR-TO-STRING
  
  C
  
  V
  
  Source
  Convert AST vector into a string.
- EXTERNAL FUNCTION
  Z3-AST-VECTOR-TRANSLATE
  
  S
  
  V
  
  AST
  
  Source
  Translate the AST vector v from context s into an AST vector in context t.
- EXTERNAL FUNCTION
  Z3-BENCHMARK-TO-SMTLIB-STRING
  
  C
  
  NAME
  
  LOGIC
  
  STATUS
  
  ATTRIBUTES
  
  NUM-ASSUMPTIONS
  
  ASSUMPTIONS
  
  FORMULA
  
  Source
  Convert the given benchmark into SMT-LIB formatted string.
- EXTERNAL FUNCTION
  Z3-CLOSE-LOG
  
  Source
  Close interaction log.
- EXTERNAL FUNCTION
  Z3-DATATYPE-UPDATE-FIELD
  
  C
  
  FIELD-ACCESS
  
  AST
  
  VALUE
  
  Source
  Update record field with a value.
- EXTERNAL FUNCTION
  Z3-DEC-REF
  
  C
  
  A
  
  Source
  Decrement the reference counter of the given AST. The context c should have been created using Z3_mk_context_rc. This function is a NOOP if c was created using Z3_mk_context.
- EXTERNAL FUNCTION
  Z3-DEL-CONFIG
  
  C
  
  Source
  Delete the given configuration object.
- EXTERNAL FUNCTION
  Z3-DEL-CONSTRUCTOR
  
  C
  
  CONSTR
  
  Source
  Reclaim memory allocated to constructor.
- EXTERNAL FUNCTION
  Z3-DEL-CONSTRUCTOR-LIST
  
  C
  
  CLIST
  
  Source
  Reclaim memory allocated for constructor list.
- EXTERNAL FUNCTION
  Z3-DEL-CONTEXT
  
  C
  
  Source
  Delete the given logical context.
- EXTERNAL FUNCTION
  Z3-DISABLE-TRACE
  
  TAG
  
  Source
  Disable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise
- EXTERNAL FUNCTION
  Z3-ENABLE-TRACE
  
  TAG
  
  Source
  Enable tracing messages tagged as tag when Z3 is compiled in debug mode. It is a NOOP otherwise
- EXTERNAL FUNCTION
  Z3-EVAL-SMTLIB2-STRING
  
  X
  
  STR
  
  Source
  Parse and evaluate and SMT-LIB2 command sequence. The state from a previous call is saved so the next evaluation builds on top of the previous call.
- EXTERNAL FUNCTION
  Z3-FINALIZE-MEMORY
  
  Source
  Destroy all allocated resources.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-ADD-CALLBACK
  
  CTX
  
  F
  
  STATE
  
  NEW-LEMMA-EH
  
  PREDECESSOR-EH
  
  UNFOLD-EH
  
  Source
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-ADD-CONSTRAINT
  
  C
  
  D
  
  E
  
  LVL
  
  Source
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-ADD-COVER
  
  C
  
  D
  
  LEVEL
  
  PRED
  
  PROPERTY
  
  Source
  Add property about the predicate pred. Add a property of predicate pred at level. It gets pushed forward when possible.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-ADD-FACT
  
  C
  
  D
  
  R
  
  NUM-ARGS
  
  ARGS
  
  Source
  Add a Database fact.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-ADD-INVARIANT
  
  C
  
  D
  
  PRED
  
  PROPERTY
  
  Source
  Add an invariant for the predicate pred. Add an assumed invariant of predicate pred.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-ADD-RULE
  
  C
  
  D
  
  RULE
  
  NAME
  
  Source
  Add a universal Horn clause as a named rule. The horn_rule should be of the form:
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-ASSERT
  
  C
  
  D
  
  AXIOM
  
  Source
  Assert a constraint to the fixedpoint context.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-DEC-REF
  
  C
  
  D
  
  Source
  Decrement the reference counter of the given fixedpoint context.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-FROM-FILE
  
  C
  
  F
  
  S
  
  Source
  Parse an SMT-LIB2 file with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the file.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-FROM-STRING
  
  C
  
  F
  
  S
  
  Source
  Parse an SMT-LIB2 string with fixedpoint rules. Add the rules to the current fixedpoint context. Return the set of queries in the string.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-GET-ANSWER
  
  C
  
  D
  
  Source
  Retrieve a formula that encodes satisfying answers to the query.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-GET-ASSERTIONS
  
  C
  
  F
  
  Source
  Retrieve set of background assertions from fixedpoint context.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-GET-COVER-DELTA
  
  C
  
  D
  
  LEVEL
  
  PRED
  
  Source
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-GET-GROUND-SAT-ANSWER
  
  C
  
  D
  
  Source
  Retrieve a bottom-up (from query) sequence of ground facts
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-GET-HELP
  
  C
  
  F
  
  Source
  Return a string describing all fixedpoint available parameters.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-GET-NUM-LEVELS
  
  C
  
  D
  
  PRED
  
  Source
  Query the PDR engine for the maximal levels properties are known about predicate.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-GET-PARAM-DESCRS
  
  C
  
  F
  
  Source
  Return the parameter description set for the given fixedpoint object.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-GET-REACHABLE
  
  C
  
  D
  
  PRED
  
  Source
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-GET-REASON-UNKNOWN
  
  C
  
  D
  
  Source
  Retrieve a string that describes the last status returned by Z3_fixedpoint_query.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-GET-RULE-NAMES-ALONG-TRACE
  
  C
  
  D
  
  Source
  Obtain the list of rules along the counterexample trace.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-GET-RULES
  
  C
  
  F
  
  Source
  Retrieve set of rules from fixedpoint context.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-GET-RULES-ALONG-TRACE
  
  C
  
  D
  
  Source
  Obtain the list of rules along the counterexample trace.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-GET-STATISTICS
  
  C
  
  D
  
  Source
  Retrieve statistics information from the last call to Z3_fixedpoint_query.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-INC-REF
  
  C
  
  D
  
  Source
  Increment the reference counter of the given fixedpoint context
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-INIT
  
  C
  
  D
  
  STATE
  
  Source
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-QUERY
  
  C
  
  D
  
  QUERY
  
  Source
  Pose a query against the asserted rules.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-QUERY-FROM-LVL
  
  C
  
  D
  
  QUERY
  
  LVL
  
  Source
  Pose a query against the asserted rules at the given level.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-QUERY-RELATIONS
  
  C
  
  D
  
  NUM-RELATIONS
  
  RELATIONS
  
  Source
  Pose multiple queries against the asserted rules.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-REGISTER-RELATION
  
  C
  
  D
  
  F
  
  Source
  Register relation as Fixedpoint defined. Fixedpoint defined relations have least-fixedpoint semantics. For example, the relation is empty if it does not occur in a head or a fact.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-SET-PARAMS
  
  C
  
  F
  
  P
  
  Source
  Set parameters on fixedpoint context.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-SET-PREDICATE-REPRESENTATION
  
  C
  
  D
  
  F
  
  NUM-RELATIONS
  
  RELATION-KINDS
  
  Source
  Configure the predicate representation.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-SET-REDUCE-APP-CALLBACK
  
  C
  
  D
  
  CB
  
  Source
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-SET-REDUCE-ASSIGN-CALLBACK
  
  C
  
  D
  
  CB
  
  Source
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-TO-STRING
  
  C
  
  F
  
  NUM-QUERIES
  
  QUERIES
  
  Source
  Print the current rules and background axioms as a string. param c - context. param f - fixedpoint context. param num_queries - number of additional queries to print. param queries - additional queries.
- EXTERNAL FUNCTION
  Z3-FIXEDPOINT-UPDATE-RULE
  
  C
  
  D
  
  A
  
  NAME
  
  Source
  Update a named rule. A rule with the same name must have been previously created.
- EXTERNAL FUNCTION
  Z3-FPA-GET-EBITS
  
  C
  
  S
  
  Source
  Retrieves the number of bits reserved for the exponent in a FloatingPoint sort.
- EXTERNAL FUNCTION
  Z3-FPA-GET-NUMERAL-EXPONENT-BV
  
  C
  
  AST
  
  BIASED
  
  Source
  Retrieves the exponent of a floating-point literal as a bit-vector expression.
- EXTERNAL FUNCTION
  Z3-FPA-GET-NUMERAL-EXPONENT-INT64
  
  C
  
  AST
  
  N
  
  BIASED
  
  Source
  Return the exponent value of a floating-point numeral as a signed 64-bit integer
- EXTERNAL FUNCTION
  Z3-FPA-GET-NUMERAL-EXPONENT-STRING
  
  C
  
  AST
  
  BIASED
  
  Source
  Return the exponent value of a floating-point numeral as a string.
- EXTERNAL FUNCTION
  Z3-FPA-GET-NUMERAL-SIGN
  
  C
  
  AST
  
  SGN
  
  Source
  Retrieves the sign of a floating-point literal.
- EXTERNAL FUNCTION
  Z3-FPA-GET-NUMERAL-SIGN-BV
  
  C
  
  AST
  
  Source
  Retrieves the sign of a floating-point literal as a bit-vector expression.
- EXTERNAL FUNCTION
  Z3-FPA-GET-NUMERAL-SIGNIFICAND-BV
  
  C
  
  AST
  
  Source
  Retrieves the significand of a floating-point literal as a bit-vector expression.
- EXTERNAL FUNCTION
  Z3-FPA-GET-NUMERAL-SIGNIFICAND-STRING
  
  C
  
  AST
  
  Source
  Return the significand value of a floating-point numeral as a string.
- EXTERNAL FUNCTION
  Z3-FPA-GET-NUMERAL-SIGNIFICAND-UINT64
  
  C
  
  AST
  
  N
  
  Source
  Return the significand value of a floating-point numeral as a uint64.
- EXTERNAL FUNCTION
  Z3-FPA-GET-SBITS
  
  C
  
  S
  
  Source
  Retrieves the number of bits reserved for the significand in a FloatingPoint sort.
- EXTERNAL FUNCTION
  Z3-FPA-IS-NUMERAL-INF
  
  C
  
  AST
  
  Source
  Checks whether a given floating-point numeral is a +oo or -oo.
- EXTERNAL FUNCTION
  Z3-FPA-IS-NUMERAL-NAN
  
  C
  
  AST
  
  Source
  Checks whether a given floating-point numeral is a NaN.
- EXTERNAL FUNCTION
  Z3-FPA-IS-NUMERAL-NEGATIVE
  
  C
  
  AST
  
  Source
  Checks whether a given floating-point numeral is negative.
- EXTERNAL FUNCTION
  Z3-FPA-IS-NUMERAL-NORMAL
  
  C
  
  AST
  
  Source
  Checks whether a given floating-point numeral is normal.
- EXTERNAL FUNCTION
  Z3-FPA-IS-NUMERAL-POSITIVE
  
  C
  
  AST
  
  Source
  Checks whether a given floating-point numeral is positive.
- EXTERNAL FUNCTION
  Z3-FPA-IS-NUMERAL-SUBNORMAL
  
  C
  
  AST
  
  Source
  Checks whether a given floating-point numeral is subnormal.
- EXTERNAL FUNCTION
  Z3-FPA-IS-NUMERAL-ZERO
  
  C
  
  AST
  
  Source
  Checks whether a given floating-point numeral is +zero or -zero.
- EXTERNAL FUNCTION
  Z3-FUNC-DECL-TO-AST
  
  C
  
  F
  
  Source
  Convert a Z3_func_decl into Z3_ast. This is just type casting.
- EXTERNAL FUNCTION
  Z3-FUNC-DECL-TO-STRING
  
  C
  
  D
  
  Source
- EXTERNAL FUNCTION
  Z3-FUNC-ENTRY-DEC-REF
  
  C
  
  E
  
  Source
  Decrement the reference counter of the given Z3_func_entry object.
- EXTERNAL FUNCTION
  Z3-FUNC-ENTRY-GET-ARG
  
  C
  
  E
  
  I
  
  Source
  Return an argument of a Z3_func_entry object.
- EXTERNAL FUNCTION
  Z3-FUNC-ENTRY-GET-NUM-ARGS
  
  C
  
  E
  
  Source
  Return the number of arguments in a Z3_func_entry object.
- EXTERNAL FUNCTION
  Z3-FUNC-ENTRY-GET-VALUE
  
  C
  
  E
  
  Source
  Return the value of this point.
- EXTERNAL FUNCTION
  Z3-FUNC-ENTRY-INC-REF
  
  C
  
  E
  
  Source
  Increment the reference counter of the given Z3_func_entry object.
- EXTERNAL FUNCTION
  Z3-FUNC-INTERP-ADD-ENTRY
  
  C
  
  FI
  
  ARGS
  
  VALUE
  
  Source
  add a function entry to a function interpretation.
- EXTERNAL FUNCTION
  Z3-FUNC-INTERP-DEC-REF
  
  C
  
  F
  
  Source
  Decrement the reference counter of the given Z3_func_interp object.
- EXTERNAL FUNCTION
  Z3-FUNC-INTERP-GET-ARITY
  
  C
  
  F
  
  Source
  Return the arity (number of arguments) of the given function interpretation.
- EXTERNAL FUNCTION
  Z3-FUNC-INTERP-GET-ELSE
  
  C
  
  F
  
  Source
  Return the 'else' value of the given function interpretation.
- EXTERNAL FUNCTION
  Z3-FUNC-INTERP-GET-ENTRY
  
  C
  
  F
  
  I
  
  Source
  Return a "point" of the given function interpretation. It represents the value of f in a particular point.
- EXTERNAL FUNCTION
  Z3-FUNC-INTERP-GET-NUM-ENTRIES
  
  C
  
  F
  
  Source
  Return the number of entries in the given function interpretation.
- EXTERNAL FUNCTION
  Z3-FUNC-INTERP-INC-REF
  
  C
  
  F
  
  Source
  Increment the reference counter of the given Z3_func_interp object.
- EXTERNAL FUNCTION
  Z3-FUNC-INTERP-SET-ELSE
  
  C
  
  F
  
  ELSE-VALUE
  
  Source
  Return the 'else' value of the given function interpretation.
- EXTERNAL FUNCTION
  Z3-GET-ALGEBRAIC-NUMBER-LOWER
  
  C
  
  A
  
  PRECISION
  
  Source
  Return a lower bound for the given real algebraic number. The interval isolating the number is smaller than 1/10^precision. The result is a numeral AST of sort Real.
- EXTERNAL FUNCTION
  Z3-GET-ALGEBRAIC-NUMBER-UPPER
  
  C
  
  A
  
  PRECISION
  
  Source
  Return a upper bound for the given real algebraic number. The interval isolating the number is smaller than 1/10^precision. The result is a numeral AST of sort Real.
- EXTERNAL FUNCTION
  Z3-GET-APP-ARG
  
  C
  
  A
  
  I
  
  Source
  Return the i-th argument of the given application.
- EXTERNAL FUNCTION
  Z3-GET-APP-DECL
  
  C
  
  A
  
  Source
  Return the declaration of a constant or function application.
- EXTERNAL FUNCTION
  Z3-GET-APP-NUM-ARGS
  
  C
  
  A
  
  Source
  Return the number of argument of an application. If t is an constant, then the number of arguments is 0.
- EXTERNAL FUNCTION
  Z3-GET-ARITY
  
  C
  
  D
  
  Source
  Alias for Z3_get_domain_size.
- EXTERNAL FUNCTION
  Z3-GET-ARRAY-SORT-DOMAIN
  
  C
  
  AST
  
  Source
  Return the domain of the given array sort. In the case of a multi-dimensional array, this function returns the sort of the first dimension.
- EXTERNAL FUNCTION
  Z3-GET-ARRAY-SORT-DOMAIN-N
  
  C
  
  AST
  
  IDX
  
  Source
  Return the i'th domain sort of an n-dimensional array.
- EXTERNAL FUNCTION
  Z3-GET-ARRAY-SORT-RANGE
  
  C
  
  AST
  
  Source
  Return the range of the given array sort.
- EXTERNAL FUNCTION
  Z3-GET-AS-ARRAY-FUNC-DECL
  
  C
  
  A
  
  Source
  Return the function declaration f associated with a (_ as_array f) node.
- EXTERNAL FUNCTION
  Z3-GET-AST-HASH
  
  C
  
  A
  
  Source
  Return a hash code for the given AST. The hash code is structural but two different AST objects can map to the same hash. The result of Z3_get_ast_id returns an indentifier that is unique over the set of live AST objects.
- EXTERNAL FUNCTION
  Z3-GET-AST-ID
  
  C
  
  AST
  
  Source
  Return a unique identifier for t. The identifier is unique up to structural equality. Thus, two ast nodes created by the same context and having the same children and same function symbols have the same identifiers. Ast nodes created in the same context, but having different children or different functions have different identifiers. Variables and quantifiers are also assigned different identifiers according to their structure.
- EXTERNAL FUNCTION
  Z3-GET-AST-KIND
  
  C
  
  A
  
  Source
  Return the kind of the given AST.
- EXTERNAL FUNCTION
  Z3-GET-BOOL-VALUE
  
  C
  
  A
  
  Source
  Return Z3_L_TRUE if a is true, Z3_L_FALSE if it is false, and Z3_L_UNDEF otherwise.
- EXTERNAL FUNCTION
  Z3-GET-BV-SORT-SIZE
  
  C
  
  AST
  
  Source
  Return the size of the given bit-vector sort.
- EXTERNAL FUNCTION
  Z3-GET-DATATYPE-SORT-CONSTRUCTOR
  
  C
  
  AST
  
  IDX
  
  Source
  Return idx'th constructor.
- EXTERNAL FUNCTION
  Z3-GET-DATATYPE-SORT-CONSTRUCTOR-ACCESSOR
  
  C
  
  AST
  
  IDX-C
  
  IDX-A
  
  Source
  Return idx_a'th accessor for the idx_c'th constructor.
- EXTERNAL FUNCTION
  Z3-GET-DATATYPE-SORT-NUM-CONSTRUCTORS
  
  C
  
  AST
  
  Source
  Return number of constructors for datatype.
- EXTERNAL FUNCTION
  Z3-GET-DATATYPE-SORT-RECOGNIZER
  
  C
  
  AST
  
  IDX
  
  Source
  Return idx'th recognizer.
- EXTERNAL FUNCTION
  Z3-GET-DECL-AST-PARAMETER
  
  C
  
  D
  
  IDX
  
  Source
  Return the expression value associated with an expression parameter.
- EXTERNAL FUNCTION
  Z3-GET-DECL-DOUBLE-PARAMETER
  
  C
  
  D
  
  IDX
  
  Source
  Return the double value associated with an double parameter.
- EXTERNAL FUNCTION
  Z3-GET-DECL-FUNC-DECL-PARAMETER
  
  C
  
  D
  
  IDX
  
  Source
  Return the expression value associated with an expression parameter.
- EXTERNAL FUNCTION
  Z3-GET-DECL-INT-PARAMETER
  
  C
  
  D
  
  IDX
  
  Source
  Return the integer value associated with an integer parameter.
- EXTERNAL FUNCTION
  Z3-GET-DECL-KIND
  
  C
  
  D
  
  Source
  Return declaration kind corresponding to declaration.
- EXTERNAL FUNCTION
  Z3-GET-DECL-NAME
  
  C
  
  D
  
  Source
  Return the constant declaration name as a symbol.
- EXTERNAL FUNCTION
  Z3-GET-DECL-NUM-PARAMETERS
  
  C
  
  D
  
  Source
  Return the number of parameters associated with a declaration.
- EXTERNAL FUNCTION
  Z3-GET-DECL-PARAMETER-KIND
  
  C
  
  D
  
  IDX
  
  Source
  Return the parameter type associated with a declaration.
- EXTERNAL FUNCTION
  Z3-GET-DECL-RATIONAL-PARAMETER
  
  C
  
  D
  
  IDX
  
  Source
  Return the rational value, as a string, associated with a rational parameter.
- EXTERNAL FUNCTION
  Z3-GET-DECL-SORT-PARAMETER
  
  C
  
  D
  
  IDX
  
  Source
  Return the sort value associated with a sort parameter.
- EXTERNAL FUNCTION
  Z3-GET-DECL-SYMBOL-PARAMETER
  
  C
  
  D
  
  IDX
  
  Source
  Return the double value associated with an double parameter.
- EXTERNAL FUNCTION
  Z3-GET-DENOMINATOR
  
  C
  
  A
  
  Source
  Return the denominator (as a numeral AST) of a numeral AST of sort Real.
- EXTERNAL FUNCTION
  Z3-GET-DOMAIN
  
  C
  
  D
  
  I
  
  Source
  Return the sort of the i-th parameter of the given function declaration.
- EXTERNAL FUNCTION
  Z3-GET-DOMAIN-SIZE
  
  C
  
  D
  
  Source
  Return the number of parameters of the given declaration.
- EXTERNAL FUNCTION
  Z3-GET-ERROR-CODE
  
  C
  
  Source
  Return the error code for the last API call.
- EXTERNAL FUNCTION
  Z3-GET-ERROR-MSG
  
  C
  
  ERR
  
  Source
  Return a string describing the given error code.
- EXTERNAL FUNCTION
  Z3-GET-ESTIMATED-ALLOC-SIZE
  
  Source
  Return the estimated allocated memory in bytes.
- EXTERNAL FUNCTION
  Z3-GET-FINITE-DOMAIN-SORT-SIZE
  
  C
  
  S
  
  R
  
  Source
  Store the size of the sort in r. Return false if the call failed. That is, Z3_get_sort_kind(s) == Z3_FINITE_DOMAIN_SORT
- EXTERNAL FUNCTION
  Z3-GET-FULL-VERSION
  
  Source
  Return a string that fully describes the version of Z3 in use.
- EXTERNAL FUNCTION
  Z3-GET-FUNC-DECL-ID
  
  C
  
  F
  
  Source
  Return a unique identifier for f.
- EXTERNAL FUNCTION
  Z3-GET-IMPLIED-EQUALITIES
  
  C
  
  S
  
  NUM-TERMS
  
  TERMS
  
  CLASS-IDS
  
  Source
  Retrieve congruence class representatives for terms.
- EXTERNAL FUNCTION
  Z3-GET-INDEX-VALUE
  
  C
  
  A
  
  Source
  Return index of de-Bruijn bound variable.
- EXTERNAL FUNCTION
  Z3-GET-LSTRING
  
  C
  
  S
  
  LENGTH
  
  Source
  Retrieve the string constant stored in s. The string can contain escape sequences. Characters in the range 1 to 255 are literal. Characters in the range 0, and 256 above are escaped.
- EXTERNAL FUNCTION
  Z3-GET-NUM-PROBES
  
  C
  
  Source
  Return the number of builtin probes available in Z3.
- EXTERNAL FUNCTION
  Z3-GET-NUM-TACTICS
  
  C
  
  Source
  Return the number of builtin tactics available in Z3.
- EXTERNAL FUNCTION
  Z3-GET-NUMERAL-BINARY-STRING
  
  C
  
  A
  
  Source
  Return numeral value, as a binary string of a numeric constant term
- EXTERNAL FUNCTION
  Z3-GET-NUMERAL-DECIMAL-STRING
  
  C
  
  A
  
  PRECISION
  
  Source
  Return numeral as a string in decimal notation. The result has at most precision decimal places.
- EXTERNAL FUNCTION
  Z3-GET-NUMERAL-DOUBLE
  
  C
  
  A
  
  Source
  Return numeral as a double.
- EXTERNAL FUNCTION
  Z3-GET-NUMERAL-INT
  
  C
  
  V
  
  I
  
  Source
  Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int. Return true if the call succeeded.
- EXTERNAL FUNCTION
  Z3-GET-NUMERAL-INT64
  
  C
  
  V
  
  I
  
  Source
  Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine int64_t int. Return true if the call succeeded.
- EXTERNAL FUNCTION
  Z3-GET-NUMERAL-RATIONAL-INT64
  
  C
  
  V
  
  NUM
  
  DEN
  
  Source
  Similar to Z3_get_numeral_string, but only succeeds if the value can fit as a rational number as machine int64_t int. Return true if the call succeeded.
- EXTERNAL FUNCTION
  Z3-GET-NUMERAL-SMALL
  
  C
  
  A
  
  NUM
  
  DEN
  
  Source
  Return numeral value, as a pair of 64 bit numbers if the representation fits.
- EXTERNAL FUNCTION
  Z3-GET-NUMERAL-STRING
  
  C
  
  A
  
  Source
  Return numeral value, as a decimal string of a numeric constant term
- EXTERNAL FUNCTION
  Z3-GET-NUMERAL-UINT
  
  C
  
  V
  
  U
  
  Source
  Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine unsigned int. Return true if the call succeeded.
- EXTERNAL FUNCTION
  Z3-GET-NUMERAL-UINT64
  
  C
  
  V
  
  U
  
  Source
  Similar to Z3_get_numeral_string, but only succeeds if the value can fit in a machine uint64_t int. Return true if the call succeeded.
- EXTERNAL FUNCTION
  Z3-GET-NUMERATOR
  
  C
  
  A
  
  Source
  Return the numerator (as a numeral AST) of a numeral AST of sort Real.
- EXTERNAL FUNCTION
  Z3-GET-PATTERN
  
  C
  
  P
  
  IDX
  
  Source
  Return i'th ast in pattern.
- EXTERNAL FUNCTION
  Z3-GET-PATTERN-NUM-TERMS
  
  C
  
  P
  
  Source
  Return number of terms in pattern.
- EXTERNAL FUNCTION
  Z3-GET-PROBE-NAME
  
  C
  
  I
  
  Source
  Return the name of the i probe.
- EXTERNAL FUNCTION
  Z3-GET-QUANTIFIER-BODY
  
  C
  
  A
  
  Source
  Return body of quantifier.
- EXTERNAL FUNCTION
  Z3-GET-QUANTIFIER-BOUND-NAME
  
  C
  
  A
  
  I
  
  Source
  Return symbol of the i'th bound variable.
- EXTERNAL FUNCTION
  Z3-GET-QUANTIFIER-BOUND-SORT
  
  C
  
  A
  
  I
  
  Source
  Return sort of the i'th bound variable.
- EXTERNAL FUNCTION
  Z3-GET-QUANTIFIER-NO-PATTERN-AST
  
  C
  
  A
  
  I
  
  Source
  Return i'th no_pattern.
- EXTERNAL FUNCTION
  Z3-GET-QUANTIFIER-NUM-BOUND
  
  C
  
  A
  
  Source
  Return number of bound variables of quantifier.
- EXTERNAL FUNCTION
  Z3-GET-QUANTIFIER-NUM-NO-PATTERNS
  
  C
  
  A
  
  Source
  Return number of no_patterns used in quantifier.
- EXTERNAL FUNCTION
  Z3-GET-QUANTIFIER-NUM-PATTERNS
  
  C
  
  A
  
  Source
  Return number of patterns used in quantifier.
- EXTERNAL FUNCTION
  Z3-GET-QUANTIFIER-PATTERN-AST
  
  C
  
  A
  
  I
  
  Source
  Return i'th pattern.
- EXTERNAL FUNCTION
  Z3-GET-QUANTIFIER-WEIGHT
  
  C
  
  A
  
  Source
  Obtain weight of quantifier.
- EXTERNAL FUNCTION
  Z3-GET-RANGE
  
  C
  
  D
  
  Source
  Return the range of the given declaration.
- EXTERNAL FUNCTION
  Z3-GET-RE-SORT-BASIS
  
  C
  
  S
  
  Source
  Retrieve basis sort for regex sort.
- EXTERNAL FUNCTION
  Z3-GET-RELATION-ARITY
  
  C
  
  S
  
  Source
  Return arity of relation.
- EXTERNAL FUNCTION
  Z3-GET-RELATION-COLUMN
  
  C
  
  S
  
  COL
  
  Source
  Return sort at i'th column of relation sort.
- EXTERNAL FUNCTION
  Z3-GET-SEQ-SORT-BASIS
  
  C
  
  S
  
  Source
  Retrieve basis sort for sequence sort.
- EXTERNAL FUNCTION
  Z3-GET-SORT
  
  C
  
  A
  
  Source
  Return the sort of an AST node.
- EXTERNAL FUNCTION
  Z3-GET-SORT-ID
  
  C
  
  S
  
  Source
  Return a unique identifier for s.
- EXTERNAL FUNCTION
  Z3-GET-SORT-KIND
  
  C
  
  AST
  
  Source
  Return the sort kind (e.g., array, tuple, int, bool, etc).
- EXTERNAL FUNCTION
  Z3-GET-SORT-NAME
  
  C
  
  D
  
  Source
  Return the sort name as a symbol.
- EXTERNAL FUNCTION
  Z3-GET-STRING
  
  C
  
  S
  
  Source
  Retrieve the string constant stored in s. Characters outside the basic printiable ASCII range are escaped.
- EXTERNAL FUNCTION
  Z3-GET-STRING-CONTENTS
  
  C
  
  S
  
  LENGTH
  
  CONTENTS
  
  Source
  Retrieve the unescaped string constant stored in s.
- EXTERNAL FUNCTION
  Z3-GET-STRING-LENGTH
  
  C
  
  S
  
  Source
  Retrieve the length of the unescaped string constant stored in s.
- EXTERNAL FUNCTION
  Z3-GET-SYMBOL-INT
  
  C
  
  S
  
  Source
  Return the symbol int value.
- EXTERNAL FUNCTION
  Z3-GET-SYMBOL-KIND
  
  C
  
  S
  
  Source
  Return Z3_INT_SYMBOL if the symbol was constructed using Z3_mk_int_symbol, and Z3_STRING_SYMBOL if the symbol was constructed using Z3_mk_string_symbol.
- EXTERNAL FUNCTION
  Z3-GET-SYMBOL-STRING
  
  C
  
  S
  
  Source
  Return the symbol name.
- EXTERNAL FUNCTION
  Z3-GET-TACTIC-NAME
  
  C
  
  I
  
  Source
  Return the name of the idx tactic.
- EXTERNAL FUNCTION
  Z3-GET-TUPLE-SORT-FIELD-DECL
  
  C
  
  AST
  
  I
  
  Source
  Return the i-th field declaration (i.e., projection function declaration) of the given tuple sort.
- EXTERNAL FUNCTION
  Z3-GET-TUPLE-SORT-MK-DECL
  
  C
  
  AST
  
  Source
  Return the constructor declaration of the given tuple sort.
- EXTERNAL FUNCTION
  Z3-GET-TUPLE-SORT-NUM-FIELDS
  
  C
  
  AST
  
  Source
  Return the number of fields of the given tuple sort.
- EXTERNAL FUNCTION
  Z3-GET-VERSION
  
  MAJOR
  
  MINOR
  
  BUILD-NUMBER
  
  REVISION-NUMBER
  
  Source
  Return Z3 version number information.
- EXTERNAL FUNCTION
  Z3-GLOBAL-PARAM-GET
  
  PARAM-ID
  
  PARAM-VALUE
  
  Source
  Get a global (or module) parameter.
- EXTERNAL FUNCTION
  Z3-GLOBAL-PARAM-RESET-ALL
  
  Source
  Restore the value of all global (and module) parameters. This command will not affect already created objects (such as tactics and solvers).
- EXTERNAL FUNCTION
  Z3-GLOBAL-PARAM-SET
  
  PARAM-ID
  
  PARAM-VALUE
  
  Source
  Set a global (or module) parameter. This setting is shared by all Z3 contexts.
- EXTERNAL FUNCTION
  Z3-GOAL-ASSERT
  
  C
  
  G
  
  A
  
  Source
  Add a new formula a to the given goal. The formula is split according to the following procedure that is applied until a fixed-point: Conjunctions are split into separate formulas. Negations are distributed over disjunctions, resulting in separate formulas. If the goal is false, adding new formulas is a no-op. If the formula a is true, then nothing is added. If the formula a is false, then the entire goal is replaced by the formula false.
- EXTERNAL FUNCTION
  Z3-GOAL-CONVERT-MODEL
  
  C
  
  G
  
  M
  
  Source
  Convert a model of the formulas of a goal to a model of an original goal. The model may be null, in which case the returned model is valid if the goal was established satisfiable.
- EXTERNAL FUNCTION
  Z3-GOAL-DEC-REF
  
  C
  
  G
  
  Source
  Decrement the reference counter of the given goal.
- EXTERNAL FUNCTION
  Z3-GOAL-DEPTH
  
  C
  
  G
  
  Source
  Return the depth of the given goal. It tracks how many transformations were applied to it.
- EXTERNAL FUNCTION
  Z3-GOAL-FORMULA
  
  C
  
  G
  
  IDX
  
  Source
  Return a formula from the given goal.
- EXTERNAL FUNCTION
  Z3-GOAL-INC-REF
  
  C
  
  G
  
  Source
  Increment the reference counter of the given goal.
- EXTERNAL FUNCTION
  Z3-GOAL-INCONSISTENT
  
  C
  
  G
  
  Source
  Return true if the given goal contains the formula false.
- EXTERNAL FUNCTION
  Z3-GOAL-IS-DECIDED-SAT
  
  C
  
  G
  
  Source
  Return true if the goal is empty, and it is precise or the product of a under approximation.
- EXTERNAL FUNCTION
  Z3-GOAL-IS-DECIDED-UNSAT
  
  C
  
  G
  
  Source
  Return true if the goal contains false, and it is precise or the product of an over approximation.
- EXTERNAL FUNCTION
  Z3-GOAL-NUM-EXPRS
  
  C
  
  G
  
  Source
  Return the number of formulas, subformulas and terms in the given goal.
- EXTERNAL FUNCTION
  Z3-GOAL-PRECISION
  
  C
  
  G
  
  Source
  Return the "precision" of the given goal. Goals can be transformed using over and under approximations. A under approximation is applied when the objective is to find a model for a given goal. An over approximation is applied when the objective is to find a proof for a given goal.
- EXTERNAL FUNCTION
  Z3-GOAL-RESET
  
  C
  
  G
  
  Source
  Erase all formulas from the given goal.
- EXTERNAL FUNCTION
  Z3-GOAL-SIZE
  
  C
  
  G
  
  Source
  Return the number of formulas in the given goal.
- EXTERNAL FUNCTION
  Z3-GOAL-TO-DIMACS-STRING
  
  C
  
  G
  
  INCLUDE-NAMES
  
  Source
  Convert a goal into a DIMACS formatted string. The goal must be in CNF. You can convert a goal to CNF by applying the tseitin-cnf tactic. Bit-vectors are not automatically converted to Booleans either, so if the caller intends to preserve satisfiability, it should apply bit-blasting tactics. Quantifiers and theory atoms will not be encoded.
- EXTERNAL FUNCTION
  Z3-GOAL-TO-STRING
  
  C
  
  G
  
  Source
  Convert a goal into a string.
- EXTERNAL FUNCTION
  Z3-GOAL-TRANSLATE
  
  SOURCE
  
  G
  
  TARGET
  
  Source
  Copy a goal g from the context source to the context target.
- EXTERNAL FUNCTION
  Z3-INC-REF
  
  C
  
  A
  
  Source
  Increment the reference counter of the given AST. The context c should have been created using Z3_mk_context_rc. This function is a NOOP if c was created using Z3_mk_context.
- EXTERNAL FUNCTION
  Z3-INTERRUPT
  
  C
  
  Source
  Interrupt the execution of a Z3 procedure. This procedure can be used to interrupt: solvers, simplifiers and tactics.
- EXTERNAL FUNCTION
  Z3-IS-ALGEBRAIC-NUMBER
  
  C
  
  A
  
  Source
  Return true if the given AST is a real algebraic number.
- EXTERNAL FUNCTION
  Z3-IS-APP
  
  C
  
  A
  
  Source
- EXTERNAL FUNCTION
  Z3-IS-AS-ARRAY
  
  C
  
  A
  
  Source
  The (_ as-array f) AST node is a construct for assigning interpretations for arrays in Z3. It is the array such that forall indices i we have that (select (_ as-array f) i) is equal to (f i). This procedure returns true if the a is an as-array AST node.
- EXTERNAL FUNCTION
  Z3-IS-CHAR-SORT
  
  C
  
  S
  
  Source
  Check if s is a character sort.
- EXTERNAL FUNCTION
  Z3-IS-EQ-AST
  
  C
  
  T1
  
  T2
  
  Source
  Compare terms.
- EXTERNAL FUNCTION
  Z3-IS-EQ-FUNC-DECL
  
  C
  
  F1
  
  F2
  
  Source
  Compare terms.
- EXTERNAL FUNCTION
  Z3-IS-EQ-SORT
  
  C
  
  S1
  
  S2
  
  Source
  compare sorts.
- EXTERNAL FUNCTION
  Z3-IS-LAMBDA
  
  C
  
  A
  
  Source
  Determine if ast is a lambda expression.
- EXTERNAL FUNCTION
  Z3-IS-NUMERAL-AST
  
  C
  
  A
  
  Source
- EXTERNAL FUNCTION
  Z3-IS-QUANTIFIER-EXISTS
  
  C
  
  A
  
  Source
  Determine if ast is an existential quantifier.
- EXTERNAL FUNCTION
  Z3-IS-QUANTIFIER-FORALL
  
  C
  
  A
  
  Source
  Determine if an ast is a universal quantifier.
- EXTERNAL FUNCTION
  Z3-IS-RE-SORT
  
  C
  
  S
  
  Source
  Check if s is a regular expression sort.
- EXTERNAL FUNCTION
  Z3-IS-SEQ-SORT
  
  C
  
  S
  
  Source
  Check if s is a sequence sort.
- EXTERNAL FUNCTION
  Z3-IS-STRING
  
  C
  
  S
  
  Source
  Determine if s is a string constant.
- EXTERNAL FUNCTION
  Z3-IS-STRING-SORT
  
  C
  
  S
  
  Source
  Check if s is a string sort.
- EXTERNAL FUNCTION
  Z3-IS-WELL-SORTED
  
  C
  
  AST
  
  Source
  Return true if the given expression t is well sorted.
- EXTERNAL FUNCTION
  Z3-MK-ADD
  
  C
  
  NUM-ARGS
  
  ARGS
  
  Source
  Create an AST node representing args[0] + ... + args[num_args-1].
- EXTERNAL FUNCTION
  Z3-MK-AND
  
  C
  
  NUM-ARGS
  
  ARGS
  
  Source
  Create an AST node representing args[0] and ... and args[num_args-1].
- EXTERNAL FUNCTION
  Z3-MK-APP
  
  C
  
  D
  
  NUM-ARGS
  
  ARGS
  
  Source
  Create a constant or function application.
- EXTERNAL FUNCTION
  Z3-MK-ARRAY-DEFAULT
  
  C
  
  ARRAY
  
  Source
  Access the array default value. Produces the default range value, for arrays that can be represented as finite maps with a default range value.
- EXTERNAL FUNCTION
  Z3-MK-ARRAY-EXT
  
  C
  
  ARG1
  
  ARG2
  
  Source
  Create array extensionality index given two arrays with the same sort. The meaning is given by the axiom: (=> (= (select A (array-ext A B)) (select B (array-ext A B))) (= A B))
- EXTERNAL FUNCTION
  Z3-MK-ARRAY-SORT
  
  C
  
  DOMAIN
  
  RANGE
  
  Source
  Create an array type.
- EXTERNAL FUNCTION
  Z3-MK-ARRAY-SORT-N
  
  C
  
  N
  
  DOMAIN
  
  RANGE
  
  Source
  Create an array type with N arguments
- EXTERNAL FUNCTION
  Z3-MK-AS-ARRAY
  
  C
  
  F
  
  Source
  Create array with the same interpretation as a function. The array satisfies the property (f x) = (select (_ as-array f) x) for every argument x.
- EXTERNAL FUNCTION
  Z3-MK-AST-MAP
  
  C
  
  Source
  Return an empty mapping from AST to AST
- EXTERNAL FUNCTION
  Z3-MK-AST-VECTOR
  
  C
  
  Source
  Return an empty AST vector.
- EXTERNAL FUNCTION
  Z3-MK-ATLEAST
  
  C
  
  NUM-ARGS
  
  ARGS
  
  K
  
  Source
  Pseudo-Boolean relations.
- EXTERNAL FUNCTION
  Z3-MK-ATMOST
  
  C
  
  NUM-ARGS
  
  ARGS
  
  K
  
  Source
  Pseudo-Boolean relations.
- EXTERNAL FUNCTION
  Z3-MK-BOOL-SORT
  
  C
  
  Source
  Create the Boolean type.
- EXTERNAL FUNCTION
  Z3-MK-BOUND
  
  C
  
  INDEX
  
  TY
  
  Source
  Create a bound variable.
- EXTERNAL FUNCTION
  Z3-MK-BV-NUMERAL
  
  C
  
  SZ
  
  BITS
  
  Source
  create a bit-vector numeral from a vector of Booleans.
- EXTERNAL FUNCTION
  Z3-MK-BV-SORT
  
  C
  
  SZ
  
  Source
  Create a bit-vector type of the given size.
- EXTERNAL FUNCTION
  Z3-MK-BV2INT
  
  C
  
  T1
  
  IS-SIGNED
  
  Source
  Create an integer from the bit-vector argument t1. If is_signed is false, then the bit-vector t1 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.
- EXTERNAL FUNCTION
  Z3-MK-BVADD
  
  C
  
  T1
  
  T2
  
  Source
  Standard two's complement addition.
- EXTERNAL FUNCTION
  Z3-MK-BVADD-NO-OVERFLOW
  
  C
  
  T1
  
  T2
  
  IS-SIGNED
  
  Source
  Create a predicate that checks that the bit-wise addition of t1 and t2 does not overflow.
- EXTERNAL FUNCTION
  Z3-MK-BVADD-NO-UNDERFLOW
  
  C
  
  T1
  
  T2
  
  Source
  Create a predicate that checks that the bit-wise signed addition of t1 and t2 does not underflow.
- EXTERNAL FUNCTION
  Z3-MK-BVAND
  
  C
  
  T1
  
  T2
  
  Source
  Bitwise and.
- EXTERNAL FUNCTION
  Z3-MK-BVASHR
  
  C
  
  T1
  
  T2
  
  Source
  Arithmetic shift right.
- EXTERNAL FUNCTION
  Z3-MK-BVLSHR
  
  C
  
  T1
  
  T2
  
  Source
  Logical shift right.
- EXTERNAL FUNCTION
  Z3-MK-BVMUL
  
  C
  
  T1
  
  T2
  
  Source
  Standard two's complement multiplication.
- EXTERNAL FUNCTION
  Z3-MK-BVMUL-NO-OVERFLOW
  
  C
  
  T1
  
  T2
  
  IS-SIGNED
  
  Source
  Create a predicate that checks that the bit-wise multiplication of t1 and t2 does not overflow.
- EXTERNAL FUNCTION
  Z3-MK-BVMUL-NO-UNDERFLOW
  
  C
  
  T1
  
  T2
  
  Source
  Create a predicate that checks that the bit-wise signed multiplication of t1 and t2 does not underflow.
- EXTERNAL FUNCTION
  Z3-MK-BVNAND
  
  C
  
  T1
  
  T2
  
  Source
  Bitwise nand.
- EXTERNAL FUNCTION
  Z3-MK-BVNEG
  
  C
  
  T1
  
  Source
  Standard two's complement unary minus.
- EXTERNAL FUNCTION
  Z3-MK-BVNEG-NO-OVERFLOW
  
  C
  
  T1
  
  Source
  Check that bit-wise negation does not overflow when t1 is interpreted as a signed bit-vector.
- EXTERNAL FUNCTION
  Z3-MK-BVNOR
  
  C
  
  T1
  
  T2
  
  Source
  Bitwise nor.
- EXTERNAL FUNCTION
  Z3-MK-BVNOT
  
  C
  
  T1
  
  Source
  Bitwise negation.
- EXTERNAL FUNCTION
  Z3-MK-BVOR
  
  C
  
  T1
  
  T2
  
  Source
  Bitwise or.
- EXTERNAL FUNCTION
  Z3-MK-BVREDAND
  
  C
  
  T1
  
  Source
  Take conjunction of bits in vector, return vector of length 1.
- EXTERNAL FUNCTION
  Z3-MK-BVREDOR
  
  C
  
  T1
  
  Source
  Take disjunction of bits in vector, return vector of length 1.
- EXTERNAL FUNCTION
  Z3-MK-BVSDIV
  
  C
  
  T1
  
  T2
  
  Source
  Two's complement signed division.
- EXTERNAL FUNCTION
  Z3-MK-BVSDIV-NO-OVERFLOW
  
  C
  
  T1
  
  T2
  
  Source
  Create a predicate that checks that the bit-wise signed division of t1 and t2 does not overflow.
- EXTERNAL FUNCTION
  Z3-MK-BVSGE
  
  C
  
  T1
  
  T2
  
  Source
  Two's complement signed greater than or equal to.
- EXTERNAL FUNCTION
  Z3-MK-BVSGT
  
  C
  
  T1
  
  T2
  
  Source
  Two's complement signed greater than.
- EXTERNAL FUNCTION
  Z3-MK-BVSHL
  
  C
  
  T1
  
  T2
  
  Source
  Shift left.
- EXTERNAL FUNCTION
  Z3-MK-BVSLE
  
  C
  
  T1
  
  T2
  
  Source
  Two's complement signed less than or equal to.
- EXTERNAL FUNCTION
  Z3-MK-BVSLT
  
  C
  
  T1
  
  T2
  
  Source
  Two's complement signed less than.
- EXTERNAL FUNCTION
  Z3-MK-BVSMOD
  
  C
  
  T1
  
  T2
  
  Source
  Two's complement signed remainder (sign follows divisor).
- EXTERNAL FUNCTION
  Z3-MK-BVSREM
  
  C
  
  T1
  
  T2
  
  Source
  Two's complement signed remainder (sign follows dividend).
- EXTERNAL FUNCTION
  Z3-MK-BVSUB
  
  C
  
  T1
  
  T2
  
  Source
  Standard two's complement subtraction.
- EXTERNAL FUNCTION
  Z3-MK-BVSUB-NO-OVERFLOW
  
  C
  
  T1
  
  T2
  
  Source
  Create a predicate that checks that the bit-wise signed subtraction of t1 and t2 does not overflow.
- EXTERNAL FUNCTION
  Z3-MK-BVSUB-NO-UNDERFLOW
  
  C
  
  T1
  
  T2
  
  IS-SIGNED
  
  Source
  Create a predicate that checks that the bit-wise subtraction of t1 and t2 does not underflow.
- EXTERNAL FUNCTION
  Z3-MK-BVUDIV
  
  C
  
  T1
  
  T2
  
  Source
  Unsigned division.
- EXTERNAL FUNCTION
  Z3-MK-BVUGE
  
  C
  
  T1
  
  T2
  
  Source
  Unsigned greater than or equal to.
- EXTERNAL FUNCTION
  Z3-MK-BVUGT
  
  C
  
  T1
  
  T2
  
  Source
  Unsigned greater than.
- EXTERNAL FUNCTION
  Z3-MK-BVULE
  
  C
  
  T1
  
  T2
  
  Source
  Unsigned less than or equal to.
- EXTERNAL FUNCTION
  Z3-MK-BVULT
  
  C
  
  T1
  
  T2
  
  Source
  Unsigned less than.
- EXTERNAL FUNCTION
  Z3-MK-BVUREM
  
  C
  
  T1
  
  T2
  
  Source
  Unsigned remainder.
- EXTERNAL FUNCTION
  Z3-MK-BVXNOR
  
  C
  
  T1
  
  T2
  
  Source
  Bitwise xnor.
- EXTERNAL FUNCTION
  Z3-MK-BVXOR
  
  C
  
  T1
  
  T2
  
  Source
  Bitwise exclusive-or.
- EXTERNAL FUNCTION
  Z3-MK-CHAR
  
  C
  
  CH
  
  Source
- EXTERNAL FUNCTION
  Z3-MK-CHAR-FROM-BV
  
  C
  
  BV
  
  Source
  Create a character from a bit-vector (code point).
- EXTERNAL FUNCTION
  Z3-MK-CHAR-IS-DIGIT
  
  C
  
  CH
  
  Source
  Create a check if the character is a digit.
- EXTERNAL FUNCTION
  Z3-MK-CHAR-LE
  
  C
  
  CH1
  
  CH2
  
  Source
  Create less than or equal to between two characters.
- EXTERNAL FUNCTION
  Z3-MK-CHAR-SORT
  
  C
  
  Source
  Create a sort for unicode characters.
- EXTERNAL FUNCTION
  Z3-MK-CHAR-TO-BV
  
  C
  
  CH
  
  Source
  Create a bit-vector (code point) from character.
- EXTERNAL FUNCTION
  Z3-MK-CHAR-TO-INT
  
  C
  
  CH
  
  Source
  Create an integer (code point) from character.
- EXTERNAL FUNCTION
  Z3-MK-CONCAT
  
  C
  
  T1
  
  T2
  
  Source
  Concatenate the given bit-vectors.
- EXTERNAL FUNCTION
  Z3-MK-CONFIG
  
  Source
  Create a configuration object for the Z3 context object.
- EXTERNAL FUNCTION
  Z3-MK-CONST
  
  C
  
  S
  
  TY
  
  Source
  Declare and create a constant.
- EXTERNAL FUNCTION
  Z3-MK-CONST-ARRAY
  
  C
  
  DOMAIN
  
  V
  
  Source
  Create the constant array.
- EXTERNAL FUNCTION
  Z3-MK-CONSTRUCTOR
  
  C
  
  NAME
  
  RECOGNIZER
  
  NUM-FIELDS
  
  FIELD-NAMES
  
  SORTS
  
  SORT-REFS
  
  Source
  Create a constructor.
- EXTERNAL FUNCTION
  Z3-MK-CONSTRUCTOR-LIST
  
  C
  
  NUM-CONSTRUCTORS
  
  CONSTRUCTORS
  
  Source
  Create list of constructors.
- EXTERNAL FUNCTION
  Z3-MK-CONTEXT
  
  C
  
  Source
  Create a context using the given configuration.
- EXTERNAL FUNCTION
  Z3-MK-CONTEXT-RC
  
  C
  
  Source
  Create a context using the given configuration. This function is similar to Z3_mk_context. However, in the context returned by this function, the user is responsible for managing Z3_ast reference counters. Managing reference counters is a burden and error-prone, but allows the user to use the memory more efficiently. The user must invoke Z3_inc_ref for any Z3_ast returned by Z3, and Z3_dec_ref whenever the Z3_ast is not needed anymore. This idiom is similar to the one used in BDD (binary decision diagrams) packages such as CUDD.
- EXTERNAL FUNCTION
  Z3-MK-DATATYPE
  
  C
  
  NAME
  
  NUM-CONSTRUCTORS
  
  CONSTRUCTORS
  
  Source
  Create datatype, such as lists, trees, records, enumerations or unions of records. The datatype may be recursive. Return the datatype sort.
- EXTERNAL FUNCTION
  Z3-MK-DATATYPES
  
  C
  
  NUM-SORTS
  
  SORT-NAMES
  
  SORTS
  
  CONSTRUCTOR-LISTS
  
  Source
  Create mutually recursive datatypes.
- EXTERNAL FUNCTION
  Z3-MK-DISTINCT
  
  C
  
  NUM-ARGS
  
  ARGS
  
  Source
  Create an AST node representing distinct(args[0], ..., args[num_args-1]).
- EXTERNAL FUNCTION
  Z3-MK-DIV
  
  C
  
  ARG1
  
  ARG2
  
  Source
  Create an AST node representing arg1 div arg2.
- EXTERNAL FUNCTION
  Z3-MK-DIVIDES
  
  C
  
  T1
  
  T2
  
  Source
  Create division predicate.
- EXTERNAL FUNCTION
  Z3-MK-EMPTY-SET
  
  C
  
  DOMAIN
  
  Source
  Create the empty set.
- EXTERNAL FUNCTION
  Z3-MK-ENUMERATION-SORT
  
  C
  
  NAME
  
  N
  
  ENUM-NAMES
  
  ENUM-CONSTS
  
  ENUM-TESTERS
  
  Source
  Create a enumeration sort.
- EXTERNAL FUNCTION
  Z3-MK-EQ
  
  C
  
  L
  
  R
  
  Source
  Create an AST node representing l = r.
- EXTERNAL FUNCTION
  Z3-MK-EXISTS
  
  C
  
  WEIGHT
  
  NUM-PATTERNS
  
  PATTERNS
  
  NUM-DECLS
  
  SORTS
  
  DECL-NAMES
  
  BODY
  
  Source
  Create an exists formula. Similar to Z3_mk_forall.
- EXTERNAL FUNCTION
  Z3-MK-EXISTS-CONST
  
  C
  
  WEIGHT
  
  NUM-BOUND
  
  BOUND
  
  NUM-PATTERNS
  
  PATTERNS
  
  BODY
  
  Source
  Similar to Z3_mk_forall_const. Create an existential quantifier using a list of constants that will form the set of bound variables.
- EXTERNAL FUNCTION
  Z3-MK-EXT-ROTATE-LEFT
  
  C
  
  T1
  
  T2
  
  Source
  Rotate bits of t1 to the left t2 times.
- EXTERNAL FUNCTION
  Z3-MK-EXT-ROTATE-RIGHT
  
  C
  
  T1
  
  T2
  
  Source
  Rotate bits of t1 to the right t2 times.
- EXTERNAL FUNCTION
  Z3-MK-EXTRACT
  
  C
  
  HIGH
  
  LOW
  
  T1
  
  Source
  Extract the bits high down to low from a bit-vector of size m to yield a new bit-vector of size n, where n = high - low + 1.
- EXTERNAL FUNCTION
  Z3-MK-FALSE
  
  C
  
  Source
  Create an AST node representing false.
- EXTERNAL FUNCTION
  Z3-MK-FINITE-DOMAIN-SORT
  
  C
  
  NAME
  
  SIZE
  
  Source
  Create a named finite domain sort.
- EXTERNAL FUNCTION
  Z3-MK-FIXEDPOINT
  
  C
  
  Source
  Create a new fixedpoint context.
- EXTERNAL FUNCTION
  Z3-MK-FORALL
  
  C
  
  WEIGHT
  
  NUM-PATTERNS
  
  PATTERNS
  
  NUM-DECLS
  
  SORTS
  
  DECL-NAMES
  
  BODY
  
  Source
  Create a forall formula. It takes an expression body that contains bound variables of the same sorts as the sorts listed in the array sorts. The bound variables are de-Bruijn indices created using Z3_mk_bound. The array decl_names contains the names that the quantified formula uses for the bound variables. Z3 applies the convention that the last element in the decl_names and sorts array refers to the variable with index 0, the second to last element of decl_names and sorts refers to the variable with index 1, etc.
- EXTERNAL FUNCTION
  Z3-MK-FORALL-CONST
  
  C
  
  WEIGHT
  
  NUM-BOUND
  
  BOUND
  
  NUM-PATTERNS
  
  PATTERNS
  
  BODY
  
  Source
  Create a universal quantifier using a list of constants that will form the set of bound variables.
- EXTERNAL FUNCTION
  Z3-MK-FPA-ABS
  
  C
  
  AST
  
  Source
  Floating-point absolute value
- EXTERNAL FUNCTION
  Z3-MK-FPA-ADD
  
  C
  
  RM
  
  T1
  
  T2
  
  Source
  Floating-point addition
- EXTERNAL FUNCTION
  Z3-MK-FPA-DIV
  
  C
  
  RM
  
  T1
  
  T2
  
  Source
  Floating-point division
- EXTERNAL FUNCTION
  Z3-MK-FPA-EQ
  
  C
  
  T1
  
  T2
  
  Source
  Floating-point equality.
- EXTERNAL FUNCTION
  Z3-MK-FPA-FMA
  
  C
  
  RM
  
  T1
  
  T2
  
  T3
  
  Source
  Floating-point fused multiply-add.
- EXTERNAL FUNCTION
  Z3-MK-FPA-FP
  
  C
  
  SGN
  
  EXP
  
  SIG
  
  Source
  Create an expression of FloatingPoint sort from three bit-vector expressions.
- EXTERNAL FUNCTION
  Z3-MK-FPA-GEQ
  
  C
  
  T1
  
  T2
  
  Source
  Floating-point greater than or equal.
- EXTERNAL FUNCTION
  Z3-MK-FPA-GT
  
  C
  
  T1
  
  T2
  
  Source
  Floating-point greater than.
- EXTERNAL FUNCTION
  Z3-MK-FPA-INF
  
  C
  
  S
  
  NEGATIVE
  
  Source
  Create a floating-point infinity of sort s.
- EXTERNAL FUNCTION
  Z3-MK-FPA-IS-INFINITE
  
  C
  
  AST
  
  Source
  Predicate indicating whether t is a floating-point number representing +oo or -oo.
- EXTERNAL FUNCTION
  Z3-MK-FPA-IS-NAN
  
  C
  
  AST
  
  Source
  Predicate indicating whether t is a NaN.
- EXTERNAL FUNCTION
  Z3-MK-FPA-IS-NEGATIVE
  
  C
  
  AST
  
  Source
  Predicate indicating whether t is a negative floating-point number.
- EXTERNAL FUNCTION
  Z3-MK-FPA-IS-NORMAL
  
  C
  
  AST
  
  Source
  Predicate indicating whether t is a normal floating-point number.
- EXTERNAL FUNCTION
  Z3-MK-FPA-IS-POSITIVE
  
  C
  
  AST
  
  Source
  Predicate indicating whether t is a positive floating-point number.
- EXTERNAL FUNCTION
  Z3-MK-FPA-IS-SUBNORMAL
  
  C
  
  AST
  
  Source
  Predicate indicating whether t is a subnormal floating-point number.
- EXTERNAL FUNCTION
  Z3-MK-FPA-IS-ZERO
  
  C
  
  AST
  
  Source
  Predicate indicating whether t is a floating-point number with zero value, i.e., +zero or -zero.
- EXTERNAL FUNCTION
  Z3-MK-FPA-LEQ
  
  C
  
  T1
  
  T2
  
  Source
  Floating-point less than or equal.
- EXTERNAL FUNCTION
  Z3-MK-FPA-LT
  
  C
  
  T1
  
  T2
  
  Source
  Floating-point less than.
- EXTERNAL FUNCTION
  Z3-MK-FPA-MAX
  
  C
  
  T1
  
  T2
  
  Source
  Maximum of floating-point numbers.
- EXTERNAL FUNCTION
  Z3-MK-FPA-MIN
  
  C
  
  T1
  
  T2
  
  Source
  Minimum of floating-point numbers.
- EXTERNAL FUNCTION
  Z3-MK-FPA-MUL
  
  C
  
  RM
  
  T1
  
  T2
  
  Source
  Floating-point multiplication
- EXTERNAL FUNCTION
  Z3-MK-FPA-NAN
  
  C
  
  S
  
  Source
  Create a floating-point NaN of sort s.
- EXTERNAL FUNCTION
  Z3-MK-FPA-NEG
  
  C
  
  AST
  
  Source
  Floating-point negation
- EXTERNAL FUNCTION
  Z3-MK-FPA-NUMERAL-DOUBLE
  
  C
  
  V
  
  TY
  
  Source
  Create a numeral of FloatingPoint sort from a double.
- EXTERNAL FUNCTION
  Z3-MK-FPA-NUMERAL-FLOAT
  
  C
  
  V
  
  TY
  
  Source
  Create a numeral of FloatingPoint sort from a float.
- EXTERNAL FUNCTION
  Z3-MK-FPA-NUMERAL-INT
  
  C
  
  V
  
  TY
  
  Source
  Create a numeral of FloatingPoint sort from a signed integer.
- EXTERNAL FUNCTION
  Z3-MK-FPA-NUMERAL-INT-UINT
  
  C
  
  SGN
  
  EXP
  
  SIG
  
  TY
  
  Source
  Create a numeral of FloatingPoint sort from a sign bit and two integers.
- EXTERNAL FUNCTION
  Z3-MK-FPA-NUMERAL-INT64-UINT64
  
  C
  
  SGN
  
  EXP
  
  SIG
  
  TY
  
  Source
  Create a numeral of FloatingPoint sort from a sign bit and two 64-bit integers.
- EXTERNAL FUNCTION
  Z3-MK-FPA-REM
  
  C
  
  T1
  
  T2
  
  Source
  Floating-point remainder
- EXTERNAL FUNCTION
  Z3-MK-FPA-RNA
  
  C
  
  Source
  Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
- EXTERNAL FUNCTION
  Z3-MK-FPA-RNE
  
  C
  
  Source
  Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
- EXTERNAL FUNCTION
  Z3-MK-FPA-ROUND-NEAREST-TIES-TO-AWAY
  
  C
  
  Source
  Create a numeral of RoundingMode sort which represents the NearestTiesToAway rounding mode.
- EXTERNAL FUNCTION
  Z3-MK-FPA-ROUND-NEAREST-TIES-TO-EVEN
  
  C
  
  Source
  Create a numeral of RoundingMode sort which represents the NearestTiesToEven rounding mode.
- EXTERNAL FUNCTION
  Z3-MK-FPA-ROUND-TO-INTEGRAL
  
  C
  
  RM
  
  AST
  
  Source
  Floating-point roundToIntegral. Rounds a floating-point number to the closest integer, again represented as a floating-point number.
- EXTERNAL FUNCTION
  Z3-MK-FPA-ROUND-TOWARD-NEGATIVE
  
  C
  
  Source
  Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
- EXTERNAL FUNCTION
  Z3-MK-FPA-ROUND-TOWARD-POSITIVE
  
  C
  
  Source
  Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
- EXTERNAL FUNCTION
  Z3-MK-FPA-ROUND-TOWARD-ZERO
  
  C
  
  Source
  Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
- EXTERNAL FUNCTION
  Z3-MK-FPA-ROUNDING-MODE-SORT
  
  C
  
  Source
  Create the RoundingMode sort.
- EXTERNAL FUNCTION
  Z3-MK-FPA-RTN
  
  C
  
  Source
  Create a numeral of RoundingMode sort which represents the TowardNegative rounding mode.
- EXTERNAL FUNCTION
  Z3-MK-FPA-RTP
  
  C
  
  Source
  Create a numeral of RoundingMode sort which represents the TowardPositive rounding mode.
- EXTERNAL FUNCTION
  Z3-MK-FPA-RTZ
  
  C
  
  Source
  Create a numeral of RoundingMode sort which represents the TowardZero rounding mode.
- EXTERNAL FUNCTION
  Z3-MK-FPA-SORT
  
  C
  
  EBITS
  
  SBITS
  
  Source
  Create a FloatingPoint sort.
- EXTERNAL FUNCTION
  Z3-MK-FPA-SORT-128
  
  C
  
  Source
  Create the quadruple-precision (128-bit) FloatingPoint sort.
- EXTERNAL FUNCTION
  Z3-MK-FPA-SORT-16
  
  C
  
  Source
  Create the half-precision (16-bit) FloatingPoint sort.
- EXTERNAL FUNCTION
  Z3-MK-FPA-SORT-32
  
  C
  
  Source
  Create the single-precision (32-bit) FloatingPoint sort.
- EXTERNAL FUNCTION
  Z3-MK-FPA-SORT-64
  
  C
  
  Source
  Create the double-precision (64-bit) FloatingPoint sort.
- EXTERNAL FUNCTION
  Z3-MK-FPA-SORT-DOUBLE
  
  C
  
  Source
  Create the double-precision (64-bit) FloatingPoint sort.
- EXTERNAL FUNCTION
  Z3-MK-FPA-SORT-HALF
  
  C
  
  Source
  Create the half-precision (16-bit) FloatingPoint sort.
- EXTERNAL FUNCTION
  Z3-MK-FPA-SORT-QUADRUPLE
  
  C
  
  Source
  Create the quadruple-precision (128-bit) FloatingPoint sort.
- EXTERNAL FUNCTION
  Z3-MK-FPA-SORT-SINGLE
  
  C
  
  Source
  Create the single-precision (32-bit) FloatingPoint sort.
- EXTERNAL FUNCTION
  Z3-MK-FPA-SQRT
  
  C
  
  RM
  
  AST
  
  Source
  Floating-point square root
- EXTERNAL FUNCTION
  Z3-MK-FPA-SUB
  
  C
  
  RM
  
  T1
  
  T2
  
  Source
  Floating-point subtraction
- EXTERNAL FUNCTION
  Z3-MK-FPA-TO-FP-BV
  
  C
  
  BV
  
  S
  
  Source
  Conversion of a single IEEE 754-2008 bit-vector into a floating-point number.
- EXTERNAL FUNCTION
  Z3-MK-FPA-TO-FP-FLOAT
  
  C
  
  RM
  
  AST
  
  S
  
  Source
  Conversion of a FloatingPoint term into another term of different FloatingPoint sort.
- EXTERNAL FUNCTION
  Z3-MK-FPA-TO-FP-INT-REAL
  
  C
  
  RM
  
  EXP
  
  SIG
  
  S
  
  Source
  Conversion of a real-sorted significand and an integer-sorted exponent into a term of FloatingPoint sort.
- EXTERNAL FUNCTION
  Z3-MK-FPA-TO-FP-REAL
  
  C
  
  RM
  
  AST
  
  S
  
  Source
  Conversion of a term of real sort into a term of FloatingPoint sort.
- EXTERNAL FUNCTION
  Z3-MK-FPA-TO-FP-SIGNED
  
  C
  
  RM
  
  AST
  
  S
  
  Source
  Conversion of a 2's complement signed bit-vector term into a term of FloatingPoint sort.
- EXTERNAL FUNCTION
  Z3-MK-FPA-TO-FP-UNSIGNED
  
  C
  
  RM
  
  AST
  
  S
  
  Source
  Conversion of a 2's complement unsigned bit-vector term into a term of FloatingPoint sort.
- EXTERNAL FUNCTION
  Z3-MK-FPA-TO-IEEE-BV
  
  C
  
  AST
  
  Source
  Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
- EXTERNAL FUNCTION
  Z3-MK-FPA-TO-REAL
  
  C
  
  AST
  
  Source
  Conversion of a floating-point term into a real-numbered term.
- EXTERNAL FUNCTION
  Z3-MK-FPA-TO-SBV
  
  C
  
  RM
  
  AST
  
  SZ
  
  Source
  Conversion of a floating-point term into a signed bit-vector.
- EXTERNAL FUNCTION
  Z3-MK-FPA-TO-UBV
  
  C
  
  RM
  
  AST
  
  SZ
  
  Source
  Conversion of a floating-point term into an unsigned bit-vector.
- EXTERNAL FUNCTION
  Z3-MK-FPA-ZERO
  
  C
  
  S
  
  NEGATIVE
  
  Source
  Create a floating-point zero of sort s.
- EXTERNAL FUNCTION
  Z3-MK-FRESH-CONST
  
  C
  
  PREFIX
  
  TY
  
  Source
  Declare and create a fresh constant.
- EXTERNAL FUNCTION
  Z3-MK-FRESH-FUNC-DECL
  
  C
  
  PREFIX
  
  DOMAIN-SIZE
  
  DOMAIN
  
  RANGE
  
  Source
  Declare a fresh constant or function.
- EXTERNAL FUNCTION
  Z3-MK-FULL-SET
  
  C
  
  DOMAIN
  
  Source
  Create the full set.
- EXTERNAL FUNCTION
  Z3-MK-FUNC-DECL
  
  C
  
  S
  
  DOMAIN-SIZE
  
  DOMAIN
  
  RANGE
  
  Source
  Declare a constant or function.
- EXTERNAL FUNCTION
  Z3-MK-GE
  
  C
  
  T1
  
  T2
  
  Source
  Create greater than or equal to.
- EXTERNAL FUNCTION
  Z3-MK-GOAL
  
  C
  
  MODELS
  
  UNSAT-CORES
  
  PROOFS
  
  Source
  Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers.
- EXTERNAL FUNCTION
  Z3-MK-GT
  
  C
  
  T1
  
  T2
  
  Source
  Create greater than.
- EXTERNAL FUNCTION
  Z3-MK-IFF
  
  C
  
  T1
  
  T2
  
  Source
  Create an AST node representing t1 iff t2.
- EXTERNAL FUNCTION
  Z3-MK-IMPLIES
  
  C
  
  T1
  
  T2
  
  Source
  Create an AST node representing t1 implies t2.
- EXTERNAL FUNCTION
  Z3-MK-INT
  
  C
  
  V
  
  TY
  
  Source
  Create a numeral of an int, bit-vector, or finite-domain sort.
- EXTERNAL FUNCTION
  Z3-MK-INT-SORT
  
  C
  
  Source
  Create the integer type.
- EXTERNAL FUNCTION
  Z3-MK-INT-SYMBOL
  
  C
  
  I
  
  Source
  Create a Z3 symbol using an integer.
- EXTERNAL FUNCTION
  Z3-MK-INT-TO-STR
  
  C
  
  S
  
  Source
  Integer to string conversion.
- EXTERNAL FUNCTION
  Z3-MK-INT2BV
  
  C
  
  N
  
  T1
  
  Source
  Create an n bit bit-vector from the integer argument t1.
- EXTERNAL FUNCTION
  Z3-MK-INT2REAL
  
  C
  
  T1
  
  Source
  Coerce an integer to a real.
- EXTERNAL FUNCTION
  Z3-MK-INT64
  
  C
  
  V
  
  TY
  
  Source
  Create a numeral of a int, bit-vector, or finite-domain sort.
- EXTERNAL FUNCTION
  Z3-MK-IS-INT
  
  C
  
  T1
  
  Source
  Check if a real number is an integer.
- EXTERNAL FUNCTION
  Z3-MK-ITE
  
  C
  
  T1
  
  T2
  
  T3
  
  Source
  Create an AST node representing an if-then-else: ite(t1, t2, t3).
- EXTERNAL FUNCTION
  Z3-MK-LAMBDA
  
  C
  
  NUM-DECLS
  
  SORTS
  
  DECL-NAMES
  
  BODY
  
  Source
  Create a lambda expression. It takes an expression body that contains bound variables of the same sorts as the sorts listed in the array sorts. The bound variables are de-Bruijn indices created using Z3_mk_bound. The array decl_names contains the names that the quantified formula uses for the bound variables. Z3 applies the convention that the last element in the decl_names and sorts array refers to the variable with index 0, the second to last element of decl_names and sorts refers to the variable with index 1, etc. The sort of the resulting expression is (Array sorts range) where range is the sort of body. For example, if the lambda binds two variables of sort Int and Bool, and the body has sort Real, the sort of the expression is (Array Int Bool Real).
- EXTERNAL FUNCTION
  Z3-MK-LAMBDA-CONST
  
  C
  
  NUM-BOUND
  
  BOUND
  
  BODY
  
  Source
  Create a lambda expression using a list of constants that form the set of bound variables
- EXTERNAL FUNCTION
  Z3-MK-LE
  
  C
  
  T1
  
  T2
  
  Source
  Create less than or equal to.
- EXTERNAL FUNCTION
  Z3-MK-LINEAR-ORDER
  
  C
  
  A
  
  ID
  
  Source
  create a linear ordering relation over signature a. The relation is identified by the index id.
- EXTERNAL FUNCTION
  Z3-MK-LIST-SORT
  
  C
  
  NAME
  
  ELEM-SORT
  
  NIL-DECL
  
  IS-NIL-DECL
  
  CONS-DECL
  
  IS-CONS-DECL
  
  HEAD-DECL
  
  TAIL-DECL
  
  Source
  Create a list sort
- EXTERNAL FUNCTION
  Z3-MK-LSTRING
  
  C
  
  LEN
  
  S
  
  Source
  Create a string constant out of the string that is passed in It takes the length of the string as well to take into account 0 characters. The string is treated as if it is unescaped so a sequence of characters \u{0} is treated as 5 characters and not the character 0.
- EXTERNAL FUNCTION
  Z3-MK-LT
  
  C
  
  T1
  
  T2
  
  Source
  Create less than.
- EXTERNAL FUNCTION
  Z3-MK-MAP
  
  C
  
  F
  
  N
  
  ARGS
  
  Source
  Map f on the argument arrays.
- EXTERNAL FUNCTION
  Z3-MK-MOD
  
  C
  
  ARG1
  
  ARG2
  
  Source
  Create an AST node representing arg1 mod arg2.
- EXTERNAL FUNCTION
  Z3-MK-MODEL
  
  C
  
  Source
  Create a fresh model object. It has reference count 0.
- EXTERNAL FUNCTION
  Z3-MK-MUL
  
  C
  
  NUM-ARGS
  
  ARGS
  
  Source
  Create an AST node representing args[0] * ... * args[num_args-1].
- EXTERNAL FUNCTION
  Z3-MK-NOT
  
  C
  
  A
  
  Source
  Create an AST node representing not(a).
- EXTERNAL FUNCTION
  Z3-MK-NUMERAL
  
  C
  
  NUMERAL
  
  TY
  
  Source
  Create a numeral of a given sort.
- EXTERNAL FUNCTION
  Z3-MK-OPTIMIZE
  
  C
  
  Source
  Create a new optimize context.
- EXTERNAL FUNCTION
  Z3-MK-OR
  
  C
  
  NUM-ARGS
  
  ARGS
  
  Source
  Create an AST node representing args[0] or ... or args[num_args-1].
- EXTERNAL FUNCTION
  Z3-MK-PARAMS
  
  C
  
  Source
  Create a Z3 (empty) parameter set. Starting at Z3 4.0, parameter sets are used to configure many components such as: simplifiers, tactics, solvers, etc.
- EXTERNAL FUNCTION
  Z3-MK-PARTIAL-ORDER
  
  C
  
  A
  
  ID
  
  Source
  create a partial ordering relation over signature a and index id.
- EXTERNAL FUNCTION
  Z3-MK-PATTERN
  
  C
  
  NUM-PATTERNS
  
  TERMS
  
  Source
  Create a pattern for quantifier instantiation.
- EXTERNAL FUNCTION
  Z3-MK-PBEQ
  
  C
  
  NUM-ARGS
  
  ARGS
  
  COEFFS
  
  K
  
  Source
  Pseudo-Boolean relations.
- EXTERNAL FUNCTION
  Z3-MK-PBGE
  
  C
  
  NUM-ARGS
  
  ARGS
  
  COEFFS
  
  K
  
  Source
  Pseudo-Boolean relations.
- EXTERNAL FUNCTION
  Z3-MK-PBLE
  
  C
  
  NUM-ARGS
  
  ARGS
  
  COEFFS
  
  K
  
  Source
  Pseudo-Boolean relations.
- EXTERNAL FUNCTION
  Z3-MK-PIECEWISE-LINEAR-ORDER
  
  C
  
  A
  
  ID
  
  Source
  create a piecewise linear ordering relation over signature a and index id.
- EXTERNAL FUNCTION
  Z3-MK-POWER
  
  C
  
  ARG1
  
  ARG2
  
  Source
  Create an AST node representing arg1 ^ arg2.
- EXTERNAL FUNCTION
  Z3-MK-PROBE
  
  C
  
  NAME
  
  Source
  Return a probe associated with the given name. The complete list of probes may be obtained using the procedures Z3_get_num_probes and Z3_get_probe_name. It may also be obtained using the command (help-tactic) in the SMT 2.0 front-end.
- EXTERNAL FUNCTION
  Z3-MK-QUANTIFIER
  
  C
  
  IS-FORALL
  
  WEIGHT
  
  NUM-PATTERNS
  
  PATTERNS
  
  NUM-DECLS
  
  SORTS
  
  DECL-NAMES
  
  BODY
  
  Source
  Create a quantifier - universal or existential, with pattern hints. See the documentation for Z3_mk_forall for an explanation of the parameters.
- EXTERNAL FUNCTION
  Z3-MK-QUANTIFIER-CONST
  
  C
  
  IS-FORALL
  
  WEIGHT
  
  NUM-BOUND
  
  BOUND
  
  NUM-PATTERNS
  
  PATTERNS
  
  BODY
  
  Source
  Create a universal or existential quantifier using a list of constants that will form the set of bound variables.
- EXTERNAL FUNCTION
  Z3-MK-QUANTIFIER-CONST-EX
  
  C
  
  IS-FORALL
  
  WEIGHT
  
  QUANTIFIER-ID
  
  SKOLEM-ID
  
  NUM-BOUND
  
  BOUND
  
  NUM-PATTERNS
  
  PATTERNS
  
  NUM-NO-PATTERNS
  
  NO-PATTERNS
  
  BODY
  
  Source
  Create a universal or existential quantifier using a list of constants that will form the set of bound variables.
- EXTERNAL FUNCTION
  Z3-MK-QUANTIFIER-EX
  
  C
  
  IS-FORALL
  
  WEIGHT
  
  QUANTIFIER-ID
  
  SKOLEM-ID
  
  NUM-PATTERNS
  
  PATTERNS
  
  NUM-NO-PATTERNS
  
  NO-PATTERNS
  
  NUM-DECLS
  
  SORTS
  
  DECL-NAMES
  
  BODY
  
  Source
  Create a quantifier - universal or existential, with pattern hints, no patterns, and attributes
- EXTERNAL FUNCTION
  Z3-MK-RE-ALLCHAR
  
  C
  
  REGEX-SORT
  
  Source
  Create a regular expression that accepts all singleton sequences of the regular expression sort
- EXTERNAL FUNCTION
  Z3-MK-RE-COMPLEMENT
  
  C
  
  RE
  
  Source
  Create the complement of the regular language re.
- EXTERNAL FUNCTION
  Z3-MK-RE-CONCAT
  
  C
  
  N
  
  ARGS
  
  Source
  Create the concatenation of the regular languages.
- EXTERNAL FUNCTION
  Z3-MK-RE-DIFF
  
  C
  
  RE1
  
  RE2
  
  Source
  Create the difference of regular expressions.
- EXTERNAL FUNCTION
  Z3-MK-RE-EMPTY
  
  C
  
  RE
  
  Source
  Create an empty regular expression of sort re.
- EXTERNAL FUNCTION
  Z3-MK-RE-FULL
  
  C
  
  RE
  
  Source
  Create an universal regular expression of sort re.
- EXTERNAL FUNCTION
  Z3-MK-RE-INTERSECT
  
  C
  
  N
  
  ARGS
  
  Source
  Create the intersection of the regular languages.
- EXTERNAL FUNCTION
  Z3-MK-RE-LOOP
  
  C
  
  R
  
  LO
  
  HI
  
  Source
  Create a regular expression loop. The supplied regular expression r is repeated between lo and hi times. The lo should be below hi with one exception: when supplying the value hi as 0, the meaning is to repeat the argument r at least lo number of times, and with an unbounded upper bound.
- EXTERNAL FUNCTION
  Z3-MK-RE-OPTION
  
  C
  
  RE
  
  Source
  Create the regular language [re].
- EXTERNAL FUNCTION
  Z3-MK-RE-PLUS
  
  C
  
  RE
  
  Source
  Create the regular language re+.
- EXTERNAL FUNCTION
  Z3-MK-RE-POWER
  
  C
  
  X
  
  N
  
  Source
  Create a power regular expression.
- EXTERNAL FUNCTION
  Z3-MK-RE-RANGE
  
  C
  
  LO
  
  HI
  
  Source
  Create the range regular expression over two sequences of length 1.
- EXTERNAL FUNCTION
  Z3-MK-RE-SORT
  
  C
  
  SEQ
  
  Source
  Create a regular expression sort out of a sequence sort.
- EXTERNAL FUNCTION
  Z3-MK-RE-STAR
  
  C
  
  RE
  
  Source
  Create the regular language re*.
- EXTERNAL FUNCTION
  Z3-MK-RE-UNION
  
  C
  
  N
  
  ARGS
  
  Source
  Create the union of the regular languages.
- EXTERNAL FUNCTION
  Z3-MK-REAL
  
  C
  
  NUM
  
  DEN
  
  Source
  Create a real from a fraction.
- EXTERNAL FUNCTION
  Z3-MK-REAL-SORT
  
  C
  
  Source
  Create the real type.
- EXTERNAL FUNCTION
  Z3-MK-REAL2INT
  
  C
  
  T1
  
  Source
  Coerce a real to an integer.
- EXTERNAL FUNCTION
  Z3-MK-REC-FUNC-DECL
  
  C
  
  S
  
  DOMAIN-SIZE
  
  DOMAIN
  
  RANGE
  
  Source
  Declare a recursive function
- EXTERNAL FUNCTION
  Z3-MK-REM
  
  C
  
  ARG1
  
  ARG2
  
  Source
  Create an AST node representing arg1 rem arg2.
- EXTERNAL FUNCTION
  Z3-MK-REPEAT
  
  C
  
  I
  
  T1
  
  Source
  Repeat the given bit-vector up length i.
- EXTERNAL FUNCTION
  Z3-MK-ROTATE-LEFT
  
  C
  
  I
  
  T1
  
  Source
  Rotate bits of t1 to the left i times.
- EXTERNAL FUNCTION
  Z3-MK-ROTATE-RIGHT
  
  C
  
  I
  
  T1
  
  Source
  Rotate bits of t1 to the right i times.
- EXTERNAL FUNCTION
  Z3-MK-SBV-TO-STR
  
  C
  
  S
  
  Source
  Signed bit-vector to string conversion.
- EXTERNAL FUNCTION
  Z3-MK-SELECT
  
  C
  
  A
  
  I
  
  Source
  Array read. The argument a is the array and i is the index of the array that gets read.
- EXTERNAL FUNCTION
  Z3-MK-SELECT-N
  
  C
  
  A
  
  N
  
  IDXS
  
  Source
  n-ary Array read. The argument a is the array and idxs are the indices of the array that gets read.
- EXTERNAL FUNCTION
  Z3-MK-SEQ-AT
  
  C
  
  S
  
  INDEX
  
  Source
  Retrieve from s the unit sequence positioned at position index. The sequence is empty if the index is out of bounds.
- EXTERNAL FUNCTION
  Z3-MK-SEQ-CONCAT
  
  C
  
  N
  
  ARGS
  
  Source
  Concatenate sequences.
- EXTERNAL FUNCTION
  Z3-MK-SEQ-CONTAINS
  
  C
  
  CONTAINER
  
  CONTAINEE
  
  Source
  Check if container contains containee.
- EXTERNAL FUNCTION
  Z3-MK-SEQ-EMPTY
  
  C
  
  SEQ
  
  Source
  Create an empty sequence of the sequence sort seq.
- EXTERNAL FUNCTION
  Z3-MK-SEQ-EXTRACT
  
  C
  
  S
  
  OFFSET
  
  LENGTH
  
  Source
  Extract subsequence starting at offset of length.
- EXTERNAL FUNCTION
  Z3-MK-SEQ-IN-RE
  
  C
  
  SEQ
  
  RE
  
  Source
  Check if seq is in the language generated by the regular expression re.
- EXTERNAL FUNCTION
  Z3-MK-SEQ-INDEX
  
  C
  
  S
  
  SUBSTR
  
  OFFSET
  
  Source
  Return index of first occurrence of substr in s starting from offset offset. If s does not contain substr, then the value is -1, if offset is the length of s, then the value is -1 as well. The value is -1 if offset is negative or larger than the length of s.
- EXTERNAL FUNCTION
  Z3-MK-SEQ-LAST-INDEX
  
  C
  
  X
  
  SUBSTR
  
  Source
- EXTERNAL FUNCTION
  Z3-MK-SEQ-LENGTH
  
  C
  
  S
  
  Source
  Return the length of the sequence s.
- EXTERNAL FUNCTION
  Z3-MK-SEQ-NTH
  
  C
  
  S
  
  INDEX
  
  Source
  Retrieve from s the element positioned at position index. The function is under-specified if the index is out of bounds.
- EXTERNAL FUNCTION
  Z3-MK-SEQ-PREFIX
  
  C
  
  PREFIX
  
  S
  
  Source
  Check if prefix is a prefix of s.
- EXTERNAL FUNCTION
  Z3-MK-SEQ-REPLACE
  
  C
  
  S
  
  SRC
  
  DST
  
  Source
  Replace the first occurrence of src with dst in s.
- EXTERNAL FUNCTION
  Z3-MK-SEQ-SORT
  
  C
  
  S
  
  Source
  Create a sequence sort out of the sort for the elements.
- EXTERNAL FUNCTION
  Z3-MK-SEQ-SUFFIX
  
  C
  
  SUFFIX
  
  S
  
  Source
  Check if suffix is a suffix of s.
- EXTERNAL FUNCTION
  Z3-MK-SEQ-TO-RE
  
  C
  
  SEQ
  
  Source
  Create a regular expression that accepts the sequence seq.
- EXTERNAL FUNCTION
  Z3-MK-SEQ-UNIT
  
  C
  
  A
  
  Source
  Create a unit sequence of a.
- EXTERNAL FUNCTION
  Z3-MK-SET-ADD
  
  C
  
  SET
  
  ELEM
  
  Source
  Add an element to a set.
- EXTERNAL FUNCTION
  Z3-MK-SET-COMPLEMENT
  
  C
  
  ARG
  
  Source
  Take the complement of a set.
- EXTERNAL FUNCTION
  Z3-MK-SET-DEL
  
  C
  
  SET
  
  ELEM
  
  Source
  Remove an element to a set.
- EXTERNAL FUNCTION
  Z3-MK-SET-DIFFERENCE
  
  C
  
  ARG1
  
  ARG2
  
  Source
  Take the set difference between two sets.
- EXTERNAL FUNCTION
  Z3-MK-SET-HAS-SIZE
  
  C
  
  SET
  
  K
  
  Source
  Create predicate that holds if Boolean array set has k elements set to true.
- EXTERNAL FUNCTION
  Z3-MK-SET-INTERSECT
  
  C
  
  NUM-ARGS
  
  ARGS
  
  Source
  Take the intersection of a list of sets.
- EXTERNAL FUNCTION
  Z3-MK-SET-MEMBER
  
  C
  
  ELEM
  
  SET
  
  Source
  Check for set membership.
- EXTERNAL FUNCTION
  Z3-MK-SET-SORT
  
  C
  
  TY
  
  Source
  Create Set type.
- EXTERNAL FUNCTION
  Z3-MK-SET-SUBSET
  
  C
  
  ARG1
  
  ARG2
  
  Source
  Check for subsetness of sets.
- EXTERNAL FUNCTION
  Z3-MK-SET-UNION
  
  C
  
  NUM-ARGS
  
  ARGS
  
  Source
  Take the union of a list of sets.
- EXTERNAL FUNCTION
  Z3-MK-SIGN-EXT
  
  C
  
  I
  
  T1
  
  Source
  Sign-extend of the given bit-vector to the (signed) equivalent bit-vector of size m+i, where m is the size of the given bit-vector.
- EXTERNAL FUNCTION
  Z3-MK-SIMPLE-SOLVER
  
  C
  
  Source
  Create a new incremental solver.
- EXTERNAL FUNCTION
  Z3-MK-SOLVER
  
  C
  
  Source
  Create a new solver. This solver is a "combined solver" (see combined_solver module) that internally uses a non-incremental (solver1) and an incremental solver (solver2). This combined solver changes its behaviour based on how it is used and how its parameters are set.
- EXTERNAL FUNCTION
  Z3-MK-SOLVER-FOR-LOGIC
  
  C
  
  LOGIC
  
  Source
  Create a new solver customized for the given logic. It behaves like Z3_mk_solver if the logic is unknown or unsupported.
- EXTERNAL FUNCTION
  Z3-MK-SOLVER-FROM-TACTIC
  
  C
  
  AST
  
  Source
  Create a new solver that is implemented using the given tactic. The solver supports the commands Z3_solver_push and Z3_solver_pop, but it will always solve each Z3_solver_check from scratch.
- EXTERNAL FUNCTION
  Z3-MK-STORE
  
  C
  
  A
  
  I
  
  V
  
  Source
  Array update.
- EXTERNAL FUNCTION
  Z3-MK-STORE-N
  
  C
  
  A
  
  N
  
  IDXS
  
  V
  
  Source
  n-ary Array update.
- EXTERNAL FUNCTION
  Z3-MK-STR-LE
  
  C
  
  PREFIX
  
  S
  
  Source
  Check if s1 is equal or lexicographically strictly less than s2.
- EXTERNAL FUNCTION
  Z3-MK-STR-LT
  
  C
  
  PREFIX
  
  S
  
  Source
  Check if s1 is lexicographically strictly less than s2.
- EXTERNAL FUNCTION
  Z3-MK-STR-TO-INT
  
  C
  
  S
  
  Source
  Convert string to integer.
- EXTERNAL FUNCTION
  Z3-MK-STRING
  
  C
  
  S
  
  Source
  Create a string constant out of the string that is passed in The string may contain escape encoding for non-printable characters or characters outside of the basic printable ASCII range. For example, the escape encoding \u{0} represents the character 0 and the encoding \u{100} represents the character 256.
- EXTERNAL FUNCTION
  Z3-MK-STRING-FROM-CODE
  
  C
  
  A
  
  Source
  Code to string conversion.
- EXTERNAL FUNCTION
  Z3-MK-STRING-SORT
  
  C
  
  Source
  Create a sort for unicode strings.
- EXTERNAL FUNCTION
  Z3-MK-STRING-SYMBOL
  
  C
  
  S
  
  Source
  Create a Z3 symbol using a C string.
- EXTERNAL FUNCTION
  Z3-MK-STRING-TO-CODE
  
  C
  
  A
  
  Source
  String to code conversion.
- EXTERNAL FUNCTION
  Z3-MK-SUB
  
  C
  
  NUM-ARGS
  
  ARGS
  
  Source
  Create an AST node representing args[0] - ... - args[num_args - 1].
- EXTERNAL FUNCTION
  Z3-MK-TACTIC
  
  C
  
  NAME
  
  Source
  Return a tactic associated with the given name. The complete list of tactics may be obtained using the procedures Z3_get_num_tactics and Z3_get_tactic_name. It may also be obtained using the command (help-tactic) in the SMT 2.0 front-end.
- EXTERNAL FUNCTION
  Z3-MK-TRANSITIVE-CLOSURE
  
  C
  
  F
  
  Source
  create transitive closure of binary relation.
- EXTERNAL FUNCTION
  Z3-MK-TREE-ORDER
  
  C
  
  A
  
  ID
  
  Source
  create a tree ordering relation over signature a identified using index id.
- EXTERNAL FUNCTION
  Z3-MK-TRUE
  
  C
  
  Source
  Create an AST node representing true.
- EXTERNAL FUNCTION
  Z3-MK-TUPLE-SORT
  
  C
  
  MK-TUPLE-NAME
  
  NUM-FIELDS
  
  FIELD-NAMES
  
  FIELD-SORTS
  
  MK-TUPLE-DECL
  
  PROJ-DECL
  
  Source
  Create a tuple type.
- EXTERNAL FUNCTION
  Z3-MK-U32STRING
  
  C
  
  LEN
  
  CHARS
  
  Source
  Create a string constant out of the string that is passed in It takes the length of the string as well to take into account 0 characters. The string is unescaped.
- EXTERNAL FUNCTION
  Z3-MK-UBV-TO-STR
  
  C
  
  S
  
  Source
  Unsigned bit-vector to string conversion.
- EXTERNAL FUNCTION
  Z3-MK-UNARY-MINUS
  
  C
  
  ARG
  
  Source
  Create an AST node representing - arg.
- EXTERNAL FUNCTION
  Z3-MK-UNINTERPRETED-SORT
  
  C
  
  S
  
  Source
  Create a free (uninterpreted) type using the given name (symbol).
- EXTERNAL FUNCTION
  Z3-MK-UNSIGNED-INT
  
  C
  
  V
  
  TY
  
  Source
  Create a numeral of a int, bit-vector, or finite-domain sort.
- EXTERNAL FUNCTION
  Z3-MK-UNSIGNED-INT64
  
  C
  
  V
  
  TY
  
  Source
  Create a numeral of a int, bit-vector, or finite-domain sort.
- EXTERNAL FUNCTION
  Z3-MK-XOR
  
  C
  
  T1
  
  T2
  
  Source
  Create an AST node representing t1 xor t2.
- EXTERNAL FUNCTION
  Z3-MK-ZERO-EXT
  
  C
  
  I
  
  T1
  
  Source
  Extend the given bit-vector with zeros to the (unsigned) equivalent bit-vector of size m+i, where m is the size of the given bit-vector.
- EXTERNAL FUNCTION
  Z3-MODEL-DEC-REF
  
  C
  
  M
  
  Source
  Decrement the reference counter of the given model.
- EXTERNAL FUNCTION
  Z3-MODEL-EVAL
  
  C
  
  M
  
  AST
  
  MODEL-COMPLETION
  
  V
  
  Source
  Evaluate the AST node t in the given model. Return true if succeeded, and store the result in v.
- EXTERNAL FUNCTION
  Z3-MODEL-EXTRAPOLATE
  
  C
  
  M
  
  FML
  
  Source
  Extrapolates a model of a formula
- EXTERNAL FUNCTION
  Z3-MODEL-GET-CONST-DECL
  
  C
  
  M
  
  I
  
  Source
  Return the i-th constant in the given model.
- EXTERNAL FUNCTION
  Z3-MODEL-GET-CONST-INTERP
  
  C
  
  M
  
  A
  
  Source
  Return the interpretation (i.e., assignment) of constant a in the model m. Return NULL, if the model does not assign an interpretation for a. That should be interpreted as: the value of a does not matter.
- EXTERNAL FUNCTION
  Z3-MODEL-GET-FUNC-DECL
  
  C
  
  M
  
  I
  
  Source
  Return the declaration of the i-th function in the given model.
- EXTERNAL FUNCTION
  Z3-MODEL-GET-FUNC-INTERP
  
  C
  
  M
  
  F
  
  Source
  Return the interpretation of the function f in the model m. Return NULL, if the model does not assign an interpretation for f. That should be interpreted as: the f does not matter.
- EXTERNAL FUNCTION
  Z3-MODEL-GET-NUM-CONSTS
  
  C
  
  M
  
  Source
  Return the number of constants assigned by the given model.
- EXTERNAL FUNCTION
  Z3-MODEL-GET-NUM-FUNCS
  
  C
  
  M
  
  Source
  Return the number of function interpretations in the given model.
- EXTERNAL FUNCTION
  Z3-MODEL-GET-NUM-SORTS
  
  C
  
  M
  
  Source
  Return the number of uninterpreted sorts that m assigns an interpretation to.
- EXTERNAL FUNCTION
  Z3-MODEL-GET-SORT
  
  C
  
  M
  
  I
  
  Source
  Return a uninterpreted sort that m assigns an interpretation.
- EXTERNAL FUNCTION
  Z3-MODEL-GET-SORT-UNIVERSE
  
  C
  
  M
  
  S
  
  Source
  Return the finite set of distinct values that represent the interpretation for sort s.
- EXTERNAL FUNCTION
  Z3-MODEL-HAS-INTERP
  
  C
  
  M
  
  A
  
  Source
  Test if there exists an interpretation (i.e., assignment) for a in the model m.
- EXTERNAL FUNCTION
  Z3-MODEL-INC-REF
  
  C
  
  M
  
  Source
  Increment the reference counter of the given model.
- EXTERNAL FUNCTION
  Z3-MODEL-TO-STRING
  
  C
  
  M
  
  Source
  Convert the given model into a string.
- EXTERNAL FUNCTION
  Z3-MODEL-TRANSLATE
  
  C
  
  M
  
  DST
  
  Source
  translate model from context c to context dst.
- EXTERNAL FUNCTION
  Z3-OPEN-LOG
  
  FILENAME
  
  Source
  Log interaction to a file.
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-ASSERT
  
  C
  
  O
  
  A
  
  Source
  Assert hard constraint to the optimization context.
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-ASSERT-AND-TRACK
  
  C
  
  O
  
  A
  
  AST
  
  Source
  Assert tracked hard constraint to the optimization context.
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-ASSERT-SOFT
  
  C
  
  O
  
  A
  
  WEIGHT
  
  ID
  
  Source
  Assert soft constraint to the optimization context. param c - context param o - optimization context param a - formula param weight - a penalty for violating soft constraint. Negative weights convert into rewards. param id - optional identifier to group soft constraints
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-CHECK
  
  C
  
  O
  
  NUM-ASSUMPTIONS
  
  ASSUMPTIONS
  
  Source
  Check consistency and produce optimal values. param c - context param o - optimization context param num_assumptions - number of additional assumptions param assumptions - the additional assumptions
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-DEC-REF
  
  C
  
  D
  
  Source
  Decrement the reference counter of the given optimize context.
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-FROM-FILE
  
  C
  
  O
  
  S
  
  Source
  Parse an SMT-LIB2 file with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context.
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-FROM-STRING
  
  C
  
  O
  
  S
  
  Source
  Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context.
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-GET-ASSERTIONS
  
  C
  
  O
  
  Source
  Return the set of asserted formulas on the optimization context.
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-GET-HELP
  
  C
  
  AST
  
  Source
  Return a string containing a description of parameters accepted by optimize.
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-GET-LOWER
  
  C
  
  O
  
  IDX
  
  Source
  Retrieve lower bound value or approximation for the i'th optimization objective.
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-GET-LOWER-AS-VECTOR
  
  C
  
  O
  
  IDX
  
  Source
  Retrieve lower bound value or approximation for the i'th optimization objective. The returned vector is of length 3. It always contains numerals. The three numerals are coefficients a, b, c and encode the result of Z3_optimize_get_lower a * infinity + b + c * epsilon.
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-GET-MODEL
  
  C
  
  O
  
  Source
  Retrieve the model for the last Z3_optimize_check
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-GET-OBJECTIVES
  
  C
  
  O
  
  Source
  Return objectives on the optimization context. If the objective function is a max-sat objective it is returned as a Pseudo-Boolean (minimization) sum of the form (+ (if f1 w1 0) (if f2 w2 0) ...) If the objective function is entered as a maximization objective, then return the corresponding minimization objective. In this way the resulting objective function is always returned as a minimization objective.
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-GET-PARAM-DESCRS
  
  C
  
  O
  
  Source
  Return the parameter description set for the given optimize object.
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-GET-REASON-UNKNOWN
  
  C
  
  D
  
  Source
  Retrieve a string that describes the last status returned by Z3_optimize_check.
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-GET-STATISTICS
  
  C
  
  D
  
  Source
  Retrieve statistics information from the last call to Z3_optimize_check
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-GET-UNSAT-CORE
  
  C
  
  O
  
  Source
  Retrieve the unsat core for the last Z3_optimize_check The unsat core is a subset of the assumptions a.
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-GET-UPPER
  
  C
  
  O
  
  IDX
  
  Source
  Retrieve upper bound value or approximation for the i'th optimization objective.
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-GET-UPPER-AS-VECTOR
  
  C
  
  O
  
  IDX
  
  Source
  Retrieve upper bound value or approximation for the i'th optimization objective.
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-INC-REF
  
  C
  
  D
  
  Source
  Increment the reference counter of the given optimize context
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-MAXIMIZE
  
  C
  
  O
  
  AST
  
  Source
  Add a maximization constraint. param c - context param o - optimization context param t - arithmetical term
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-MINIMIZE
  
  C
  
  O
  
  AST
  
  Source
  Add a minimization constraint. param c - context param o - optimization context param t - arithmetical term
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-POP
  
  C
  
  D
  
  Source
  Backtrack one level.
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-PUSH
  
  C
  
  D
  
  Source
  Create a backtracking point.
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-REGISTER-MODEL-EH
  
  C
  
  O
  
  M
  
  CTX
  
  MODEL-EH
  
  Source
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-SET-PARAMS
  
  C
  
  O
  
  P
  
  Source
  Set parameters on optimization context.
- EXTERNAL FUNCTION
  Z3-OPTIMIZE-TO-STRING
  
  C
  
  O
  
  Source
  Print the current context as a string. param c - context. param o - optimization context.
- EXTERNAL FUNCTION
  Z3-PARAM-DESCRS-DEC-REF
  
  C
  
  P
  
  Source
  Decrement the reference counter of the given parameter description set.
- EXTERNAL FUNCTION
  Z3-PARAM-DESCRS-GET-DOCUMENTATION
  
  C
  
  P
  
  S
  
  Source
  Retrieve documentation string corresponding to parameter name s.
- EXTERNAL FUNCTION
  Z3-PARAM-DESCRS-GET-KIND
  
  C
  
  P
  
  N
  
  Source
  Return the kind associated with the given parameter name n.
- EXTERNAL FUNCTION
  Z3-PARAM-DESCRS-GET-NAME
  
  C
  
  P
  
  I
  
  Source
  Return the name of the parameter at given index i.
- EXTERNAL FUNCTION
  Z3-PARAM-DESCRS-INC-REF
  
  C
  
  P
  
  Source
  Increment the reference counter of the given parameter description set.
- EXTERNAL FUNCTION
  Z3-PARAM-DESCRS-SIZE
  
  C
  
  P
  
  Source
  Return the number of parameters in the given parameter description set.
- EXTERNAL FUNCTION
  Z3-PARAM-DESCRS-TO-STRING
  
  C
  
  P
  
  Source
  Convert a parameter description set into a string. This function is mainly used for printing the contents of a parameter description set.
- EXTERNAL FUNCTION
  Z3-PARAMS-DEC-REF
  
  C
  
  P
  
  Source
  Decrement the reference counter of the given parameter set.
- EXTERNAL FUNCTION
  Z3-PARAMS-INC-REF
  
  C
  
  P
  
  Source
  Increment the reference counter of the given parameter set.
- EXTERNAL FUNCTION
  Z3-PARAMS-SET-BOOL
  
  C
  
  P
  
  K
  
  V
  
  Source
  Add a Boolean parameter k with value v to the parameter set p.
- EXTERNAL FUNCTION
  Z3-PARAMS-SET-DOUBLE
  
  C
  
  P
  
  K
  
  V
  
  Source
  Add a double parameter k with value v to the parameter set p.
- EXTERNAL FUNCTION
  Z3-PARAMS-SET-SYMBOL
  
  C
  
  P
  
  K
  
  V
  
  Source
  Add a symbol parameter k with value v to the parameter set p.
- EXTERNAL FUNCTION
  Z3-PARAMS-SET-UINT
  
  C
  
  P
  
  K
  
  V
  
  Source
  Add a unsigned parameter k with value v to the parameter set p.
- EXTERNAL FUNCTION
  Z3-PARAMS-TO-STRING
  
  C
  
  P
  
  Source
  Convert a parameter set into a string. This function is mainly used for printing the contents of a parameter set.
- EXTERNAL FUNCTION
  Z3-PARAMS-VALIDATE
  
  C
  
  P
  
  D
  
  Source
  Validate the parameter set p against the parameter description set d.
- EXTERNAL FUNCTION
  Z3-PARSE-SMTLIB2-FILE
  
  C
  
  FILE-NAME
  
  NUM-SORTS
  
  SORT-NAMES
  
  SORTS
  
  NUM-DECLS
  
  DECL-NAMES
  
  DECLS
  
  Source
  Similar to Z3_parse_smtlib2_string, but reads the benchmark from a file.
- EXTERNAL FUNCTION
  Z3-PARSE-SMTLIB2-STRING
  
  C
  
  STR
  
  NUM-SORTS
  
  SORT-NAMES
  
  SORTS
  
  NUM-DECLS
  
  DECL-NAMES
  
  DECLS
  
  Source
  Parse the given string using the SMT-LIB2 parser.
- EXTERNAL FUNCTION
  Z3-PATTERN-TO-AST
  
  C
  
  P
  
  Source
  Convert a Z3_pattern into Z3_ast. This is just type casting.
- EXTERNAL FUNCTION
  Z3-PATTERN-TO-STRING
  
  C
  
  P
  
  Source
- EXTERNAL FUNCTION
  Z3-POLYNOMIAL-SUBRESULTANTS
  
  C
  
  P
  
  Q
  
  X
  
  Source
  Return the nonzero subresultants of p and q with respect to the "variable" x.
- EXTERNAL FUNCTION
  Z3-PROBE-AND
  
  X
  
  P1
  
  P2
  
  Source
  Return a probe that evaluates to "true" when p1 and p2 evaluates to true.
- EXTERNAL FUNCTION
  Z3-PROBE-APPLY
  
  C
  
  P
  
  G
  
  Source
  Execute the probe over the goal. The probe always produce a double value. "Boolean" probes return 0.0 for false, and a value different from 0.0 for true.
- EXTERNAL FUNCTION
  Z3-PROBE-CONST
  
  X
  
  VAL
  
  Source
  Return a probe that always evaluates to val.
- EXTERNAL FUNCTION
  Z3-PROBE-DEC-REF
  
  C
  
  P
  
  Source
  Decrement the reference counter of the given probe.
- EXTERNAL FUNCTION
  Z3-PROBE-EQ
  
  X
  
  P1
  
  P2
  
  Source
  Return a probe that evaluates to "true" when the value returned by p1 is equal to the value returned by p2.
- EXTERNAL FUNCTION
  Z3-PROBE-GE
  
  X
  
  P1
  
  P2
  
  Source
  Return a probe that evaluates to "true" when the value returned by p1 is greater than or equal to the value returned by p2.
- EXTERNAL FUNCTION
  Z3-PROBE-GET-DESCR
  
  C
  
  NAME
  
  Source
  Return a string containing a description of the probe with the given name.
- EXTERNAL FUNCTION
  Z3-PROBE-GT
  
  X
  
  P1
  
  P2
  
  Source
  Return a probe that evaluates to "true" when the value returned by p1 is greater than the value returned by p2.
- EXTERNAL FUNCTION
  Z3-PROBE-INC-REF
  
  C
  
  P
  
  Source
  Increment the reference counter of the given probe.
- EXTERNAL FUNCTION
  Z3-PROBE-LE
  
  X
  
  P1
  
  P2
  
  Source
  Return a probe that evaluates to "true" when the value returned by p1 is less than or equal to the value returned by p2.
- EXTERNAL FUNCTION
  Z3-PROBE-LT
  
  X
  
  P1
  
  P2
  
  Source
  Return a probe that evaluates to "true" when the value returned by p1 is less than the value returned by p2.
- EXTERNAL FUNCTION
  Z3-PROBE-NOT
  
  X
  
  P
  
  Source
  Return a probe that evaluates to "true" when p does not evaluate to true.
- EXTERNAL FUNCTION
  Z3-PROBE-OR
  
  X
  
  P1
  
  P2
  
  Source
  Return a probe that evaluates to "true" when p1 or p2 evaluates to true.
- EXTERNAL FUNCTION
  Z3-QE-LITE
  
  C
  
  VARS
  
  BODY
  
  Source
- EXTERNAL FUNCTION
  Z3-QE-MODEL-PROJECT
  
  C
  
  M
  
  NUM-BOUNDS
  
  BOUND
  
  BODY
  
  Source
  Project variables given a model
- EXTERNAL FUNCTION
  Z3-QE-MODEL-PROJECT-SKOLEM
  
  C
  
  M
  
  NUM-BOUNDS
  
  BOUND
  
  BODY
  
  MAP
  
  Source
  Project variables given a model
- EXTERNAL FUNCTION
  Z3-QUERY-CONSTRUCTOR
  
  C
  
  CONSTR
  
  NUM-FIELDS
  
  CONSTRUCTOR
  
  TESTER
  
  ACCESSORS
  
  Source
  Query constructor for declared functions.
- EXTERNAL FUNCTION
  Z3-RCF-ADD
  
  C
  
  A
  
  B
  
  Source
  Return the value a + b.
- EXTERNAL FUNCTION
  Z3-RCF-DEL
  
  C
  
  A
  
  Source
  Delete a RCF numeral created using the RCF API.
- EXTERNAL FUNCTION
  Z3-RCF-DIV
  
  C
  
  A
  
  B
  
  Source
  Return the value a / b.
- EXTERNAL FUNCTION
  Z3-RCF-EQ
  
  C
  
  A
  
  B
  
  Source
  Return true if a == b.
- EXTERNAL FUNCTION
  Z3-RCF-GE
  
  C
  
  A
  
  B
  
  Source
  Return true if a >= b.
- EXTERNAL FUNCTION
  Z3-RCF-GET-NUMERATOR-DENOMINATOR
  
  C
  
  A
  
  N
  
  D
  
  Source
  Extract the "numerator" and "denominator" of the given RCF numeral. We have that a = n/d, moreover n and d are not represented using rational functions.
- EXTERNAL FUNCTION
  Z3-RCF-GT
  
  C
  
  A
  
  B
  
  Source
  Return true if a > b.
- EXTERNAL FUNCTION
  Z3-RCF-INV
  
  C
  
  A
  
  Source
  Return the value 1/a.
- EXTERNAL FUNCTION
  Z3-RCF-LE
  
  C
  
  A
  
  B
  
  Source
  Return true if a <= b.
- EXTERNAL FUNCTION
  Z3-RCF-LT
  
  C
  
  A
  
  B
  
  Source
  Return true if a < b.
- EXTERNAL FUNCTION
  Z3-RCF-MK-E
  
  C
  
  Source
  Return e (Euler's constant)
- EXTERNAL FUNCTION
  Z3-RCF-MK-INFINITESIMAL
  
  C
  
  Source
  Return a new infinitesimal that is smaller than all elements in the Z3 field.
- EXTERNAL FUNCTION
  Z3-RCF-MK-PI
  
  C
  
  Source
  Return Pi
- EXTERNAL FUNCTION
  Z3-RCF-MK-RATIONAL
  
  C
  
  VAL
  
  Source
  Return a RCF rational using the given string.
- EXTERNAL FUNCTION
  Z3-RCF-MK-ROOTS
  
  C
  
  N
  
  A
  
  ROOTS
  
  Source
  Store in roots the roots of the polynomial a[n-1]*x^{n-1 + ... + a[0]}. The output vector roots must have size n. It returns the number of roots of the polynomial.
- EXTERNAL FUNCTION
  Z3-RCF-MK-SMALL-INT
  
  C
  
  VAL
  
  Source
  Return a RCF small integer.
- EXTERNAL FUNCTION
  Z3-RCF-MUL
  
  C
  
  A
  
  B
  
  Source
  Return the value a * b.
- EXTERNAL FUNCTION
  Z3-RCF-NEG
  
  C
  
  A
  
  Source
  Return the value -a.
- EXTERNAL FUNCTION
  Z3-RCF-NEQ
  
  C
  
  A
  
  B
  
  Source
  Return true if a != b.
- EXTERNAL FUNCTION
  Z3-RCF-NUM-TO-DECIMAL-STRING
  
  C
  
  A
  
  PREC
  
  Source
  Convert the RCF numeral into a string in decimal notation.
- EXTERNAL FUNCTION
  Z3-RCF-NUM-TO-STRING
  
  C
  
  A
  
  COMPACT
  
  HTML
  
  Source
  Convert the RCF numeral into a string.
- EXTERNAL FUNCTION
  Z3-RCF-POWER
  
  C
  
  A
  
  K
  
  Source
  Return the value a^k.
- EXTERNAL FUNCTION
  Z3-RCF-SUB
  
  C
  
  A
  
  B
  
  Source
  Return the value a - b.
- EXTERNAL FUNCTION
  Z3-RESET-MEMORY
  
  Source
  Reset all allocated resources.
- EXTERNAL FUNCTION
  Z3-SET-AST-PRINT-MODE
  
  C
  
  MODE
  
  Source
  Select mode for the format used for pretty-printing AST nodes.
- EXTERNAL FUNCTION
  Z3-SET-ERROR
  
  C
  
  E
  
  Source
  Set an error.
- EXTERNAL FUNCTION
  Z3-SET-ERROR-HANDLER
  
  C
  
  H
  
  Source
- EXTERNAL FUNCTION
  Z3-SET-PARAM-VALUE
  
  C
  
  PARAM-ID
  
  PARAM-VALUE
  
  Source
  Set a configuration parameter.
- EXTERNAL FUNCTION
  Z3-SIMPLIFY
  
  C
  
  A
  
  Source
  Interface to simplifier.
- EXTERNAL FUNCTION
  Z3-SIMPLIFY-EX
  
  C
  
  A
  
  P
  
  Source
  Interface to simplifier.
- EXTERNAL FUNCTION
  Z3-SIMPLIFY-GET-HELP
  
  C
  
  Source
  Return a string describing all available parameters.
- EXTERNAL FUNCTION
  Z3-SIMPLIFY-GET-PARAM-DESCRS
  
  C
  
  Source
  Return the parameter description set for the simplify procedure.
- EXTERNAL FUNCTION
  Z3-SOLVER-ASSERT
  
  C
  
  S
  
  A
  
  Source
  Assert a constraint into the solver.
- EXTERNAL FUNCTION
  Z3-SOLVER-ASSERT-AND-TRACK
  
  C
  
  S
  
  A
  
  P
  
  Source
  Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p.
- EXTERNAL FUNCTION
  Z3-SOLVER-CHECK
  
  C
  
  S
  
  Source
  Check whether the assertions in a given solver are consistent or not.
- EXTERNAL FUNCTION
  Z3-SOLVER-CHECK-ASSUMPTIONS
  
  C
  
  S
  
  NUM-ASSUMPTIONS
  
  ASSUMPTIONS
  
  Source
  Check whether the assertions in the given solver and optional assumptions are consistent or not.
- EXTERNAL FUNCTION
  Z3-SOLVER-CUBE
  
  C
  
  S
  
  VARS
  
  BACKTRACK-LEVEL
  
  Source
  extract a next cube for a solver. The last cube is the constant true or false. The number of (non-constant) cubes is by default 1. For the sat solver cubing is controlled using parameters sat.lookahead.cube.cutoff and sat.lookahead.cube.fraction.
- EXTERNAL FUNCTION
  Z3-SOLVER-DEC-REF
  
  C
  
  S
  
  Source
  Decrement the reference counter of the given solver.
- EXTERNAL FUNCTION
  Z3-SOLVER-FROM-FILE
  
  C
  
  S
  
  FILE-NAME
  
  Source
  load solver assertions from a file.
- EXTERNAL FUNCTION
  Z3-SOLVER-FROM-STRING
  
  C
  
  S
  
  FILE-NAME
  
  Source
  load solver assertions from a string.
- EXTERNAL FUNCTION
  Z3-SOLVER-GET-ASSERTIONS
  
  C
  
  S
  
  Source
  Return the set of asserted formulas on the solver.
- EXTERNAL FUNCTION
  Z3-SOLVER-GET-CONSEQUENCES
  
  C
  
  S
  
  ASSUMPTIONS
  
  VARIABLES
  
  CONSEQUENCES
  
  Source
  retrieve consequences from solver that determine values of the supplied function symbols.
- EXTERNAL FUNCTION
  Z3-SOLVER-GET-HELP
  
  C
  
  S
  
  Source
  Return a string describing all solver available parameters.
- EXTERNAL FUNCTION
  Z3-SOLVER-GET-LEVELS
  
  C
  
  S
  
  LITERALS
  
  SZ
  
  LEVELS
  
  Source
  retrieve the decision depth of Boolean literals (variables or their negations). Assumes a check-sat call and no other calls (to extract models) have been invoked.
- EXTERNAL FUNCTION
  Z3-SOLVER-GET-MODEL
  
  C
  
  S
  
  Source
  Retrieve the model for the last Z3_solver_check or Z3_solver_check_assumptions
- EXTERNAL FUNCTION
  Z3-SOLVER-GET-NON-UNITS
  
  C
  
  S
  
  Source
  Return the set of non units in the solver state.
- EXTERNAL FUNCTION
  Z3-SOLVER-GET-NUM-SCOPES
  
  C
  
  S
  
  Source
  Return the number of backtracking points.
- EXTERNAL FUNCTION
  Z3-SOLVER-GET-PARAM-DESCRS
  
  C
  
  S
  
  Source
  Return the parameter description set for the given solver object.
- EXTERNAL FUNCTION
  Z3-SOLVER-GET-PROOF
  
  C
  
  S
  
  Source
  Retrieve the proof for the last Z3_solver_check or Z3_solver_check_assumptions
- EXTERNAL FUNCTION
  Z3-SOLVER-GET-REASON-UNKNOWN
  
  C
  
  S
  
  Source
  Return a brief justification for an "unknown" result (i.e., Z3_L_UNDEF) for the commands Z3_solver_check and Z3_solver_check_assumptions
- EXTERNAL FUNCTION
  Z3-SOLVER-GET-STATISTICS
  
  C
  
  S
  
  Source
  Return statistics for the given solver.
- EXTERNAL FUNCTION
  Z3-SOLVER-GET-TRAIL
  
  C
  
  S
  
  Source
  Return the trail modulo model conversion, in order of decision level The decision level can be retrieved using Z3_solver_get_level based on the trail.
- EXTERNAL FUNCTION
  Z3-SOLVER-GET-UNITS
  
  C
  
  S
  
  Source
  Return the set of units modulo model conversion.
- EXTERNAL FUNCTION
  Z3-SOLVER-GET-UNSAT-CORE
  
  C
  
  S
  
  Source
  Retrieve the unsat core for the last Z3_solver_check_assumptions The unsat core is a subset of the assumptions a.
- EXTERNAL FUNCTION
  Z3-SOLVER-IMPORT-MODEL-CONVERTER
  
  CTX
  
  SRC
  
  DST
  
  Source
  Ad-hoc method for importing model conversion from solver.
- EXTERNAL FUNCTION
  Z3-SOLVER-INC-REF
  
  C
  
  S
  
  Source
  Increment the reference counter of the given solver.
- EXTERNAL FUNCTION
  Z3-SOLVER-INTERRUPT
  
  C
  
  S
  
  Source
  Solver local interrupt. Normally you should use Z3_interrupt to cancel solvers because only one solver is enabled concurrently per context. However, per GitHub issue 1006, there are use cases where it is more convenient to cancel a specific solver. Solvers that are not selected for interrupts are left alone.
- EXTERNAL FUNCTION
  Z3-SOLVER-POP
  
  C
  
  S
  
  N
  
  Source
  Backtrack n backtracking points.
- EXTERNAL FUNCTION
  Z3-SOLVER-PROPAGATE-CONSEQUENCE
  
  C
  
  X
  
  NUM-FIXED
  
  FIXED
  
  NUM-EQS
  
  EQ-LHS
  
  EQ-RHS
  
  CONSEQ
  
  Source
  propagate a consequence based on fixed values. This is a callback a client may invoke during the fixed_eh callback. The callback adds a propagation consequence based on the fixed values of the ids.
- EXTERNAL FUNCTION
  Z3-SOLVER-PROPAGATE-CREATED
  
  C
  
  S
  
  CREATED-EH
  
  Source
- EXTERNAL FUNCTION
  Z3-SOLVER-PROPAGATE-DECLARE
  
  C
  
  NAME
  
  N
  
  DOMAIN
  
  RANGE
  
  Source
- EXTERNAL FUNCTION
  Z3-SOLVER-PROPAGATE-DISEQ
  
  C
  
  S
  
  EQ-EH
  
  Source
- EXTERNAL FUNCTION
  Z3-SOLVER-PROPAGATE-EQ
  
  C
  
  S
  
  EQ-EH
  
  Source
- EXTERNAL FUNCTION
  Z3-SOLVER-PROPAGATE-FINAL
  
  C
  
  S
  
  FINAL-EH
  
  Source
- EXTERNAL FUNCTION
  Z3-SOLVER-PROPAGATE-FIXED
  
  C
  
  S
  
  FIXED-EH
  
  Source
- EXTERNAL FUNCTION
  Z3-SOLVER-PROPAGATE-INIT
  
  C
  
  S
  
  USER-CONTEXT
  
  PUSH-EH
  
  POP-EH
  
  FRESH-EH
  
  Source
- EXTERNAL FUNCTION
  Z3-SOLVER-PROPAGATE-REGISTER
  
  C
  
  S
  
  E
  
  Source
  register an expression to propagate on with the solver. Only expressions of type Bool and type Bit-Vector can be registered for propagation.
- EXTERNAL FUNCTION
  Z3-SOLVER-PROPAGATE-REGISTER-CB
  
  C
  
  CB
  
  E
  
  Source
  register an expression to propagate on with the solver. Only expressions of type Bool and type Bit-Vector can be registered for propagation. Unlike ref Z3_solver_propagate_register, this function takes a solver callback context as argument. It can be invoked during a callback to register new expressions.
- EXTERNAL FUNCTION
  Z3-SOLVER-PUSH
  
  C
  
  S
  
  Source
  Create a backtracking point.
- EXTERNAL FUNCTION
  Z3-SOLVER-RESET
  
  C
  
  S
  
  Source
  Remove all assertions from the solver.
- EXTERNAL FUNCTION
  Z3-SOLVER-SET-PARAMS
  
  C
  
  S
  
  P
  
  Source
  Set the given solver using the given parameters.
- EXTERNAL FUNCTION
  Z3-SOLVER-TO-DIMACS-STRING
  
  C
  
  S
  
  INCLUDE-NAMES
  
  Source
  Convert a solver into a DIMACS formatted string. sa Z3_goal_to_diamcs_string for requirements.
- EXTERNAL FUNCTION
  Z3-SOLVER-TO-STRING
  
  C
  
  S
  
  Source
  Convert a solver into a string.
- EXTERNAL FUNCTION
  Z3-SOLVER-TRANSLATE
  
  SOURCE
  
  S
  
  TARGET
  
  Source
  Copy a solver s from the context source to the context target.
- EXTERNAL FUNCTION
  Z3-SORT-TO-AST
  
  C
  
  S
  
  Source
  Convert a Z3_sort into Z3_ast. This is just type casting.
- EXTERNAL FUNCTION
  Z3-SORT-TO-STRING
  
  C
  
  S
  
  Source
- EXTERNAL FUNCTION
  Z3-STATS-DEC-REF
  
  C
  
  S
  
  Source
  Decrement the reference counter of the given statistics object.
- EXTERNAL FUNCTION
  Z3-STATS-GET-DOUBLE-VALUE
  
  C
  
  S
  
  IDX
  
  Source
  Return the double value of the given statistical data.
- EXTERNAL FUNCTION
  Z3-STATS-GET-KEY
  
  C
  
  S
  
  IDX
  
  Source
  Return the key (a string) for a particular statistical data.
- EXTERNAL FUNCTION
  Z3-STATS-GET-UINT-VALUE
  
  C
  
  S
  
  IDX
  
  Source
  Return the unsigned value of the given statistical data.
- EXTERNAL FUNCTION
  Z3-STATS-INC-REF
  
  C
  
  S
  
  Source
  Increment the reference counter of the given statistics object.
- EXTERNAL FUNCTION
  Z3-STATS-IS-DOUBLE
  
  C
  
  S
  
  IDX
  
  Source
  Return true if the given statistical data is a double.
- EXTERNAL FUNCTION
  Z3-STATS-IS-UINT
  
  C
  
  S
  
  IDX
  
  Source
  Return true if the given statistical data is a unsigned integer.
- EXTERNAL FUNCTION
  Z3-STATS-SIZE
  
  C
  
  S
  
  Source
  Return the number of statistical data in s.
- EXTERNAL FUNCTION
  Z3-STATS-TO-STRING
  
  C
  
  S
  
  Source
  Convert a statistics into a string.
- EXTERNAL FUNCTION
  Z3-SUBSTITUTE
  
  C
  
  A
  
  NUM-EXPRS
  
  FROM
  
  TO
  
  Source
  Substitute every occurrence of from[i] in a with to[i], for i smaller than num_exprs. The result is the new AST. The arrays from and to must have size num_exprs. For every i smaller than num_exprs, we must have that sort of from[i] must be equal to sort of to[i].
- EXTERNAL FUNCTION
  Z3-SUBSTITUTE-VARS
  
  C
  
  A
  
  NUM-EXPRS
  
  TO
  
  Source
  Substitute the free variables in a with the expressions in to. For every i smaller than num_exprs, the variable with de-Bruijn index i is replaced with term to[i].
- EXTERNAL FUNCTION
  Z3-TACTIC-AND-THEN
  
  C
  
  T1
  
  T2
  
  Source
  Return a tactic that applies t1 to a given goal and t2 to every subgoal produced by t1.
- EXTERNAL FUNCTION
  Z3-TACTIC-APPLY
  
  C
  
  AST
  
  G
  
  Source
  Apply tactic t to the goal g.
- EXTERNAL FUNCTION
  Z3-TACTIC-APPLY-EX
  
  C
  
  AST
  
  G
  
  P
  
  Source
  Apply tactic t to the goal g using the parameter set p.
- EXTERNAL FUNCTION
  Z3-TACTIC-COND
  
  C
  
  P
  
  T1
  
  T2
  
  Source
  Return a tactic that applies t1 to a given goal if the probe p evaluates to true, and t2 if p evaluates to false.
- EXTERNAL FUNCTION
  Z3-TACTIC-DEC-REF
  
  C
  
  G
  
  Source
  Decrement the reference counter of the given tactic.
- EXTERNAL FUNCTION
  Z3-TACTIC-FAIL
  
  C
  
  Source
  Return a tactic that always fails.
- EXTERNAL FUNCTION
  Z3-TACTIC-FAIL-IF
  
  C
  
  P
  
  Source
  Return a tactic that fails if the probe p evaluates to false.
- EXTERNAL FUNCTION
  Z3-TACTIC-FAIL-IF-NOT-DECIDED
  
  C
  
  Source
  Return a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains false).
- EXTERNAL FUNCTION
  Z3-TACTIC-GET-DESCR
  
  C
  
  NAME
  
  Source
  Return a string containing a description of the tactic with the given name.
- EXTERNAL FUNCTION
  Z3-TACTIC-GET-HELP
  
  C
  
  AST
  
  Source
  Return a string containing a description of parameters accepted by the given tactic.
- EXTERNAL FUNCTION
  Z3-TACTIC-GET-PARAM-DESCRS
  
  C
  
  AST
  
  Source
  Return the parameter description set for the given tactic object.
- EXTERNAL FUNCTION
  Z3-TACTIC-INC-REF
  
  C
  
  AST
  
  Source
  Increment the reference counter of the given tactic.
- EXTERNAL FUNCTION
  Z3-TACTIC-OR-ELSE
  
  C
  
  T1
  
  T2
  
  Source
  Return a tactic that first applies t1 to a given goal, if it fails then returns the result of t2 applied to the given goal.
- EXTERNAL FUNCTION
  Z3-TACTIC-PAR-AND-THEN
  
  C
  
  T1
  
  T2
  
  Source
  Return a tactic that applies t1 to a given goal and then t2 to every subgoal produced by t1. The subgoals are processed in parallel.
- EXTERNAL FUNCTION
  Z3-TACTIC-PAR-OR
  
  C
  
  NUM
  
  TS
  
  Source
  Return a tactic that applies the given tactics in parallel.
- EXTERNAL FUNCTION
  Z3-TACTIC-REPEAT
  
  C
  
  AST
  
  MAX
  
  Source
  Return a tactic that keeps applying t until the goal is not modified anymore or the maximum number of iterations max is reached.
- EXTERNAL FUNCTION
  Z3-TACTIC-SKIP
  
  C
  
  Source
  Return a tactic that just return the given goal.
- EXTERNAL FUNCTION
  Z3-TACTIC-TRY-FOR
  
  C
  
  AST
  
  MS
  
  Source
  Return a tactic that applies t to a given goal for ms milliseconds. If t does not terminate in ms milliseconds, then it fails.
- EXTERNAL FUNCTION
  Z3-TACTIC-USING-PARAMS
  
  C
  
  AST
  
  P
  
  Source
  Return a tactic that applies t using the given set of parameters.
- EXTERNAL FUNCTION
  Z3-TACTIC-WHEN
  
  C
  
  P
  
  AST
  
  Source
  Return a tactic that applies t to a given goal is the probe p evaluates to true. If p evaluates to false, then the new tactic behaves like the skip tactic.
- EXTERNAL FUNCTION
  Z3-TO-APP
  
  C
  
  A
  
  Source
  Convert an ast into an APP_AST. This is just type casting.
- EXTERNAL FUNCTION
  Z3-TO-FUNC-DECL
  
  C
  
  A
  
  Source
  Convert an AST into a FUNC_DECL_AST. This is just type casting.
- EXTERNAL FUNCTION
  Z3-TOGGLE-WARNING-MESSAGES
  
  ENABLED
  
  Source
  Enable/disable printing warning messages to the console.
- EXTERNAL FUNCTION
  Z3-TRANSLATE
  
  SOURCE
  
  A
  
  TARGET
  
  Source
  Translate/Copy the AST a from context source to context target. AST a must have been created using context source. pre source != target
- EXTERNAL FUNCTION
  Z3-UPDATE-PARAM-VALUE
  
  C
  
  PARAM-ID
  
  PARAM-VALUE
  
  Source
  Set a value of a context parameter.
- EXTERNAL FUNCTION
  Z3-UPDATE-TERM
  
  C
  
  A
  
  NUM-ARGS
  
  ARGS
  
  Source
  Update the arguments of term a using the arguments args. The number of arguments num_args should coincide with the number of arguments to a. If a is a quantifier, then num_args has to be 1.