Enum z3_sys::DeclKind

#[repr(u32)]
pub enum DeclKind {
    TRUE,
    FALSE,
    EQ,
    DISTINCT,
    ITE,
    AND,
    OR,
    IFF,
    XOR,
    NOT,
    IMPLIES,
    OEQ,
    INTERP,
    ANUM,
    AGNUM,
    LE,
    GE,
    LT,
    GT,
    ADD,
    SUB,
    UMINUS,
    MUL,
    DIV,
    IDIV,
    REM,
    MOD,
    TO_REAL,
    TO_INT,
    IS_INT,
    POWER,
    STORE,
    SELECT,
    CONST_ARRAY,
    ARRAY_MAP,
    ARRAY_DEFAULT,
    SET_UNION,
    SET_INTERSECT,
    SET_DIFFERENCE,
    SET_COMPLEMENT,
    SET_SUBSET,
    AS_ARRAY,
    ARRAY_EXT,
    BNUM,
    BIT1,
    BIT0,
    BNEG,
    BADD,
    BSUB,
    BMUL,
    BSDIV,
    BUDIV,
    BSREM,
    BUREM,
    BSMOD,
    BSDIV0,
    BUDIV0,
    BSREM0,
    BUREM0,
    BSMOD0,
    ULEQ,
    SLEQ,
    UGEQ,
    SGEQ,
    ULT,
    SLT,
    UGT,
    SGT,
    BAND,
    BOR,
    BNOT,
    BXOR,
    BNAND,
    BNOR,
    BXNOR,
    CONCAT,
    SIGN_EXT,
    ZERO_EXT,
    EXTRACT,
    REPEAT,
    BREDOR,
    BREDAND,
    BCOMP,
    BSHL,
    BLSHR,
    BASHR,
    ROTATE_LEFT,
    ROTATE_RIGHT,
    EXT_ROTATE_LEFT,
    EXT_ROTATE_RIGHT,
    BIT2BOOL,
    INT2BV,
    BV2INT,
    CARRY,
    XOR3,
    BSMUL_NO_OVFL,
    BUMUL_NO_OVFL,
    BSMUL_NO_UDFL,
    BSDIV_I,
    BUDIV_I,
    BSREM_I,
    BUREM_I,
    BSMOD_I,
    PR_UNDEF,
    PR_TRUE,
    PR_ASSERTED,
    PR_GOAL,
    PR_MODUS_PONENS,
    PR_REFLEXIVITY,
    PR_SYMMETRY,
    PR_TRANSITIVITY,
    PR_TRANSITIVITY_STAR,
    PR_MONOTONICITY,
    PR_QUANT_INTRO,
    PR_DISTRIBUTIVITY,
    PR_AND_ELIM,
    PR_NOT_OR_ELIM,
    PR_REWRITE,
    PR_REWRITE_STAR,
    PR_PULL_QUANT,
    PR_PUSH_QUANT,
    PR_ELIM_UNUSED_VARS,
    PR_DER,
    PR_QUANT_INST,
    PR_HYPOTHESIS,
    PR_LEMMA,
    PR_UNIT_RESOLUTION,
    PR_IFF_TRUE,
    PR_IFF_FALSE,
    PR_COMMUTATIVITY,
    PR_DEF_AXIOM,
    PR_DEF_INTRO,
    PR_APPLY_DEF,
    PR_IFF_OEQ,
    PR_NNF_POS,
    PR_NNF_NEG,
    PR_SKOLEMIZE,
    PR_MODUS_PONENS_OEQ,
    PR_TH_LEMMA,
    PR_HYPER_RESOLVE,
    RA_STORE,
    RA_EMPTY,
    RA_IS_EMPTY,
    RA_JOIN,
    RA_UNION,
    RA_WIDEN,
    RA_PROJECT,
    RA_FILTER,
    RA_NEGATION_FILTER,
    RA_RENAME,
    RA_COMPLEMENT,
    RA_SELECT,
    RA_CLONE,
    FD_CONSTANT,
    FD_LT,
    SEQ_UNIT,
    SEQ_EMPTY,
    SEQ_CONCAT,
    SEQ_PREFIX,
    SEQ_SUFFIX,
    SEQ_CONTAINS,
    SEQ_EXTRACT,
    SEQ_REPLACE,
    SEQ_AT,
    SEQ_LENGTH,
    SEQ_INDEX,
    SEQ_TO_RE,
    SEQ_IN_RE,
    STR_TO_INT,
    INT_TO_STR,
    RE_PLUS,
    RE_STAR,
    RE_OPTION,
    RE_CONCAT,
    RE_UNION,
    RE_RANGE,
    RE_LOOP,
    RE_INTERSECT,
    RE_EMPTY_SET,
    RE_FULL_SET,
    RE_COMPLEMENT,
    LABEL,
    LABEL_LIT,
    DT_CONSTRUCTOR,
    DT_RECOGNISER,
    DT_IS,
    DT_ACCESSOR,
    DT_UPDATE_FIELD,
    PB_AT_MOST,
    PB_AT_LEAST,
    PB_LE,
    PB_GE,
    PB_EQ,
    FPA_RM_NEAREST_TIES_TO_EVEN,
    FPA_RM_NEAREST_TIES_TO_AWAY,
    FPA_RM_TOWARD_POSITIVE,
    FPA_RM_TOWARD_NEGATIVE,
    FPA_RM_TOWARD_ZERO,
    FPA_NUM,
    FPA_PLUS_INF,
    FPA_MINUS_INF,
    FPA_NAN,
    FPA_PLUS_ZERO,
    FPA_MINUS_ZERO,
    FPA_ADD,
    FPA_SUB,
    FPA_NEG,
    FPA_MUL,
    FPA_DIV,
    FPA_REM,
    FPA_ABS,
    FPA_MIN,
    FPA_MAX,
    FPA_FMA,
    FPA_SQRT,
    FPA_ROUND_TO_INTEGRAL,
    FPA_EQ,
    FPA_LT,
    FPA_GT,
    FPA_LE,
    FPA_GE,
    FPA_IS_NAN,
    FPA_IS_INF,
    FPA_IS_ZERO,
    FPA_IS_NORMAL,
    FPA_IS_SUBNORMAL,
    FPA_IS_NEGATIVE,
    FPA_IS_POSITIVE,
    FPA_FP,
    FPA_TO_FP,
    FPA_TO_FP_UNSIGNED,
    FPA_TO_UBV,
    FPA_TO_SBV,
    FPA_TO_REAL,
    FPA_TO_IEEE_BV,
    FPA_BVWRAP,
    FPA_BV2RM,
    INTERNAL,
    UNINTERPRETED,
}

The different kinds of interpreted function kinds.

This corresponds to Z3_decl_kind in the C API.

Variants

TRUE

The constant true.

FALSE

The constant false.

EQ

The equality predicate.

DISTINCT

The n-ary distinct predicate (every argument is mutually distinct).

ITE

The ternary if-then-else term.

AND

n-ary conjunction.

OR

n-ary disjunction.

IFF

equivalence (binary).

XOR

Exclusive or.

NOT

Negation.

IMPLIES

Implication.

OEQ

Binary equivalence modulo namings. This binary predicate is used in proof terms. It captures equisatisfiability and equivalence modulo renamings.

INTERP

Marks a sub-formula for interpolation.

ANUM

Arithmetic numeral.

AGNUM

Arithmetic algebraic numeral. Algebraic numbers are used to represent irrational numbers in Z3.

LE

<=.

GE

>=.

LT

<.

GT

>.

ADD

Addition - Binary.

SUB

Binary subtraction.

UMINUS

Unary minus.

MUL

Multiplication - Binary.

DIV

Division - Binary.

IDIV

Integer division - Binary.

REM

Remainder - Binary.

MOD

Modulus - Binary.

TO_REAL

Coercion of integer to real - Unary.

TO_INT

Coercion of real to integer - Unary.

IS_INT

Check if real is also an integer - Unary.

POWER

Power operator x^y.

STORE

Array store. It satisfies select(store(a,i,v),j) = if i = j then v else select(a,j). Array store takes at least 3 arguments.

SELECT

Array select.

CONST_ARRAY

The constant array. For example, select(const(v),i) = v holds for every v and i. The function is unary.

ARRAY_MAP

Array map operator. It satisfies map[f](a1,..,a_n)[i] = f(a1[i],...,a_n[i]) for every i.

ARRAY_DEFAULT

Default value of arrays. For example default(const(v)) = v. The function is unary.

SET_UNION

Set union between two Boolean arrays (two arrays whose range type is Boolean). The function is binary.

SET_INTERSECT

Set intersection between two Boolean arrays. The function is binary.

SET_DIFFERENCE

Set difference between two Boolean arrays. The function is binary.

SET_COMPLEMENT

Set complement of a Boolean array. The function is unary.

SET_SUBSET

Subset predicate between two Boolean arrays. The relation is binary.

AS_ARRAY

An array value that behaves as the function graph of the function passed as parameter.

ARRAY_EXT

Array extensionality function. It takes two arrays as arguments and produces an index, such that the arrays are different if they are different on the index.

BNUM

Bit-vector numeral.

BIT1

One bit bit-vector.

BIT0

Zero bit bit-vector.

BNEG

Unary minus.

BADD

Binary addition.

BSUB

Binary subtraction.

BMUL

Binary multiplication.

BSDIV

Binary signed division.

BUDIV

Binary unsigned division.

BSREM

Binary signed remainder.

BUREM

Binary unsigned remainder.

BSMOD

Binary signed modulus.

BSDIV0

Unary function. bsdiv(x, 0) is congruent to bsdiv0(x).

BUDIV0

Unary function. budiv(x, 0) is congruent to budiv0(x).

BSREM0

Unary function. bsrem(x, 0) is congruent to bsrem0(x).

BUREM0

Unary function. burem(x, 0) is congruent to burem0(x).

BSMOD0

Unary function. bsmod(x, 0) is congruent to bsmod0(x).

ULEQ

Unsigned bit-vector <= - Binary relation.

SLEQ

Signed bit-vector <= - Binary relation.

UGEQ

Unsigned bit-vector >= - Binary relation.

SGEQ

Signed bit-vector >= - Binary relation.

ULT

Unsigned bit-vector < - Binary relation.

SLT

Signed bit-vector < - Binary relation.

UGT

Unsigned bit-vector > - Binary relation.

SGT

Signed bit-vector > - Binary relation.

BAND

Bit-wise and - Binary.

BOR

Bit-wise or - Binary.

BNOT

Bit-wise not - Unary.

BXOR

Bit-wise xor - Binary.

BNAND

Bit-wise nand - Binary.

BNOR

Bit-wise nor - Binary.

BXNOR

Bit-wise xnor - Binary.

CONCAT

Bit-vector concatenation - Binary.

SIGN_EXT

Bit-vector sign extension.

ZERO_EXT

Bit-vector zero extension.

EXTRACT

Bit-vector extraction.

REPEAT

Repeat bit-vector n times.

BREDOR

Bit-vector reduce or - Unary.

BREDAND

Bit-vector reduce and - Unary.

BCOMPBSHL

Shift left.

BLSHR

Logical shift right.

BASHR

Arithmetical shift right.

ROTATE_LEFT

Left rotation.

ROTATE_RIGHT

Right rotation.

EXT_ROTATE_LEFT

(extended) Left rotation. Similar to DeclKind::ROTATE_LEFT, but it is a binary operator instead of a parametric one.

EXT_ROTATE_RIGHT

(extended) Right rotation. Similar to DeclKind::ROTATE_RIGHT, but it is a binary operator instead of a parametric one.

BIT2BOOLINT2BV

Coerce integer to bit-vector.

NB. This function is not supported by the decision procedures. Only the most rudimentary simplification rules are applied to this function.

BV2INT

Coerce bit-vector to integer.

NB. This function is not supported by the decision procedures. Only the most rudimentary simplification rules are applied to this function.

CARRY

Compute the carry bit in a full-adder. The meaning is given by the equivalence:

(carry l1 l2 l3) <=> (or (and l1 l2) (and l1 l3) (and l2 l3)))

XOR3

Compute ternary XOR.

The meaning is given by the equivalence:

(xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3)

BSMUL_NO_OVFL

Check that bit-wise signed multiplication does not overflow.

Signed multiplication overflows if the operands have the same sign and the result of multiplication does not fit within the available bits.

See also:

• Z3_mk_bvmul_no_overflow

BUMUL_NO_OVFL

Check that bit-wise unsigned multiplication does not overflow.

Unsigned multiplication overflows if the result does not fit within the available bits.

See also:

• Z3_mk_bvmul_no_overflow

BSMUL_NO_UDFL

Check that bit-wise signed multiplication does not underflow.

Signed multiplication underflows if the operands have opposite signs and the result of multiplication does not fit within the available bits.

See also:

• Z3_mk_bvmul_no_underflow

BSDIV_I

Binary signed division.

It has the same semantics as DeclKind::BSDIV, but created in a context where the second operand can be assumed to be non-zero.

BUDIV_I

Binary unsigned division.

It has the same semantics as DeclKind::BUDIV, but created in a context where the second operand can be assumed to be non-zero.

BSREM_I

Binary signed remainder.

It has the same semantics as DeclKind::BSREM, but created in a context where the second operand can be assumed to be non-zero.

BUREM_I

Binary unsigned remainder.

It has the same semantics as DeclKind::BUREM, but created in a context where the second operand can be assumed to be non-zero.

BSMOD_I

Binary signed modulus.

It has the same semantics as DeclKind::BSMOD, but created in a context where the second operand can be assumed to be non-zero.

PR_UNDEF

Undef/Null proof object.

PR_TRUE

Proof for the expression 'true'.

PR_ASSERTED

Proof for a fact asserted by the user.

PR_GOAL

Proof for a fact (tagged as goal) asserted by the user.

PR_MODUS_PONENS

Given a proof for p and a proof for (implies p q), produces a proof for q.

T1: p
T2: (implies p q)
[mp T1 T2]: q

The second antecedents may also be a proof for (iff p q).

PR_REFLEXIVITY

A proof for (R t t), where R is a reflexive relation.

This proof object has no antecedents.

The only reflexive relations that are used are equivalence modulo namings, equality and equivalence. That is, R is either ~, = or iff.

PR_SYMMETRY

Given an symmetric relation R and a proof for (R t s), produces a proof for (R s t).

T1: (R t s)
[symmetry T1]: (R s t)

T1 is the antecedent of this proof object.

PR_TRANSITIVITY

Given a transitive relation R, and proofs for (R t s) and (R s u), produces a proof for (R t u).

T1: (R t s)
T2: (R s u)
[trans T1 T2]: (R t u)

PR_TRANSITIVITY_STAR

Condensed transitivity proof.

It combines several symmetry and transitivity proofs.

Example:

T1: (R a b)
T2: (R c b)
T3: (R c d)
[trans* T1 T2 T3]: (R a d)

R must be a symmetric and transitive relation.

Assuming that this proof object is a proof for (R s t), then a proof checker must check if it is possible to prove (R s t) using the antecedents, symmetry and transitivity. That is, if there is a path from s to t, if we view every antecedent (R a b) as an edge between a and b.

PR_MONOTONICITY

Monotonicity proof object.

T1: (R t_1 s_1)
...
Tn: (R t_n s_n)
[monotonicity T1 ... Tn]: (R (f t_1 ... t_n) (f s_1 ... s_n))

Remark: if t_i == s_i, then the antecedent Ti is suppressed. That is, reflexivity proofs are suppressed to save space.

PR_QUANT_INTRO

Given a proof for (~ p q), produces a proof for (~ (forall (x) p) (forall (x) q)).

T1: (~ p q)
[quant-intro T1]: (~ (forall (x) p) (forall (x) q))

PR_DISTRIBUTIVITY

Distributivity proof object.

Given that f (= or) distributes over g (= and), produces a proof for

(= (f a (g c d))
(g (f a c) (f a d)))

If f and g are associative, this proof also justifies the following equality:

(= (f (g a b) (g c d))
(g (f a c) (f a d) (f b c) (f b d)))

where each f and g can have arbitrary number of arguments.

This proof object has no antecedents.

Remark: This rule is used by the CNF conversion pass and instantiated by f = or, and g = and.

PR_AND_ELIM

Given a proof for (and l_1 ... l_n), produces a proof for l_i.

T1: (and l_1 ... l_n)
[and-elim T1]: l_i

PR_NOT_OR_ELIM

Given a proof for (not (or l_1 ... l_n)), produces a proof for (not l_i).

T1: (not (or l_1 ... l_n))
[not-or-elim T1]: (not l_i)

PR_REWRITE

A proof for a local rewriting step (= t s).

The head function symbol of t is interpreted.

This proof object has no antecedents.

The conclusion of a rewrite rule is either an equality (= t s), an equivalence (iff t s), or equi-satisfiability (~ t s).

Remark: if f is bool, then = is iff.

Examples:

(= (+ x 0) x)
(= (+ x 1 2) (+ 3 x))
(iff (or x false) x)

PR_REWRITE_STAR

A proof for rewriting an expression t into an expression s.

This proof object can have n antecedents. The antecedents are proofs for equalities used as substitution rules.

The object is also used in a few cases. The cases are:

• When applying contextual simplification (CONTEXT_SIMPLIFIER=true).
• When converting bit-vectors to Booleans (BIT2BOOL=true).

PR_PULL_QUANT

A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))).

This proof object has no antecedents.

PR_PUSH_QUANT

A proof for:

(iff (forall (x_1 ... x_m) (and p_1[x_1 ... x_m] ... p_n[x_1 ... x_m]))
(and (forall (x_1 ... x_m) p_1[x_1 ... x_m])
...
(forall (x_1 ... x_m) p_n[x_1 ... x_m])))

This proof object has no antecedents.

PR_ELIM_UNUSED_VARS

A proof for

(iff (forall (x_1 ... x_n y_1 ... y_m) p[x_1 ... x_n])
(forall (x_1 ... x_n) p[x_1 ... x_n]))

It is used to justify the elimination of unused variables.

This proof object has no antecedents.

PR_DER

A proof for destructive equality resolution:

(iff (forall (x) (or (not (= x t)) P[x])) P[t])

if x does not occur in t.

This proof object has no antecedents.

Several variables can be eliminated simultaneously.

PR_QUANT_INST

A proof of (or (not (forall (x) (P x))) (P a)).

PR_HYPOTHESIS

Mark a hypothesis in a natural deduction style proof.

PR_LEMMA

T1: false
[lemma T1]: (or (not l_1) ... (not l_n))

This proof object has one antecedent: a hypothetical proof for false.

It converts the proof in a proof for (or (not l_1) ... (not l_n)), when T1 contains the open hypotheses: l_1, ..., l_n.

The hypotheses are closed after an application of a lemma.

Furthermore, there are no other open hypotheses in the subtree covered by the lemma.

PR_UNIT_RESOLUTION

T1:      (or l_1 ... l_n l_1' ... l_m')
T2:      (not l_1)
...
T(n+1):  (not l_n)
[unit-resolution T1 ... T(n+1)]: (or l_1' ... l_m')

PR_IFF_TRUE

T1: p
[iff-true T1]: (iff p true)

PR_IFF_FALSE

T1: (not p)
[iff-false T1]: (iff p false)

PR_COMMUTATIVITY

[comm]: (= (f a b) (f b a))

f is a commutative operator.

This proof object has no antecedents.

Remark: if f is bool, then = is iff.

PR_DEF_AXIOM

Proof object used to justify Tseitin's like axioms:

(or (not (and p q)) p)
(or (not (and p q)) q)
(or (not (and p q r)) p)
(or (not (and p q r)) q)
(or (not (and p q r)) r)
...
(or (and p q) (not p) (not q))
(or (not (or p q)) p q)
(or (or p q) (not p))
(or (or p q) (not q))
(or (not (iff p q)) (not p) q)
(or (not (iff p q)) p (not q))
(or (iff p q) (not p) (not q))
(or (iff p q) p q)
(or (not (ite a b c)) (not a) b)
(or (not (ite a b c)) a c)
(or (ite a b c) (not a) (not b))
(or (ite a b c) a (not c))
(or (not (not a)) (not a))
(or (not a) a)

This proof object has no antecedents.

Note: all axioms are propositional tautologies. Note also that and and or can take multiple arguments. You can recover the propositional tautologies by unfolding the Boolean connectives in the axioms a small bounded number of steps (=3).

PR_DEF_INTRO

Introduces a name for a formula/term.

Suppose e is an expression with free variables x, and def-intro introduces the name n(x). The possible cases are:

When e is of Boolean type:

[def-intro]: (and (or n (not e)) (or (not n) e))

or:

[def-intro]: (or (not n) e)

when e only occurs positively.

When e is of the form (ite cond th el):

[def-intro]: (and (or (not cond) (= n th)) (or cond (= n el)))

Otherwise:

[def-intro]: (= n e)

PR_APPLY_DEF

[apply-def T1]: F ~ n

F is 'equivalent' to n, given that T1 is a proof that n is a name for F.

PR_IFF_OEQ

T1: (iff p q)
[iff~ T1]: (~ p q)

PR_NNF_POS

Proof for a (positive) NNF step. Example:

T1: (not s_1) ~ r_1
T2: (not s_2) ~ r_2
T3: s_1 ~ r_1'
T4: s_2 ~ r_2'
[nnf-pos T1 T2 T3 T4]: (~ (iff s_1 s_2)
(and (or r_1 r_2') (or r_1' r_2)))

The negation normal form steps NNF_POS and NNF_NEG are used in the following cases:

• When creating the NNF of a positive force quantifier. The quantifier is retained (unless the bound variables are eliminated). Example:

  T1: q ~ q_new
  [nnf-pos T1]: (~ (forall (x T) q) (forall (x T) q_new))
  

• When recursively creating NNF over Boolean formulas, where the top-level connective is changed during NNF conversion. The relevant Boolean connectives for NNF_POS are implies, iff, xor, ite. NNF_NEG furthermore handles the case where negation is pushed over Boolean connectives and and or.

PR_NNF_NEG

Proof for a (negative) NNF step. Examples:

T1: (not s_1) ~ r_1
...
Tn: (not s_n) ~ r_n
[nnf-neg T1 ... Tn]: (not (and s_1 ... s_n)) ~ (or r_1 ... r_n)

and

T1: (not s_1) ~ r_1
...
Tn: (not s_n) ~ r_n
[nnf-neg T1 ... Tn]: (not (or s_1 ... s_n)) ~ (and r_1 ... r_n)

and

T1: (not s_1) ~ r_1
T2: (not s_2) ~ r_2
T3: s_1 ~ r_1'
T4: s_2 ~ r_2'
[nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2))
(and (or r_1 r_2) (or r_1' r_2')))

PR_SKOLEMIZE

Proof for:

[sk]: (~ (not (forall x (p x y))) (not (p (sk y) y)))
[sk]: (~ (exists x (p x y)) (p (sk y) y))

This proof object has no antecedents.

PR_MODUS_PONENS_OEQ

Modus ponens style rule for equi-satisfiability.

T1: p
T2: (~ p q)
[mp~ T1 T2]: q

PR_TH_LEMMA

Generic proof for theory lemmas.

The theory lemma function comes with one or more parameters.

The first parameter indicates the name of the theory.

For the theory of arithmetic, additional parameters provide hints for checking the theory lemma.

The hints for arithmetic are:

• farkas - followed by rational coefficients. Multiply the coefficients to the inequalities in the lemma, add the (negated) inequalities and obtain a contradiction.
• triangle-eq - Indicates a lemma related to the equivalence:

  (iff (= t1 t2) (and (<= t1 t2) (<= t2 t1)))
  

• gcd-test - Indicates an integer linear arithmetic lemma that uses a gcd test.

PR_HYPER_RESOLVE

Hyper-resolution rule.

The premises of the rules is a sequence of clauses. The first clause argument is the main clause of the rule. with a literal from the first (main) clause.

Premises of the rules are of the form

(or l0 l1 l2 .. ln)

or

(=> (and l1 l2 .. ln) l0)

or in the most general (ground) form:

(=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln))

In other words we use the following (Prolog style) convention for Horn implications:

• the head of a Horn implication is position 0,
• the first conjunct in the body of an implication is position 1
• the second conjunct in the body of an implication is position 2

For general implications where the head is a disjunction, the first n positions correspond to the n disjuncts in the head. The next m positions correspond to the m conjuncts in the body.

The premises can be universally quantified so that the most general non-ground form is:

(forall (vars) (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln)))

The hyper-resolution rule takes a sequence of parameters. The parameters are substitutions of bound variables separated by pairs of literal positions from the main clause and side clause.

RA_STORE

Insert a record into a relation.

The function takes n+1 arguments, where the first argument is the relation and the remaining n elements correspond to the n columns of the relation.

RA_EMPTY

Creates the empty relation.

RA_IS_EMPTY

Tests if the relation is empty.

RA_JOIN

Create the relational join.

RA_UNION

Create the union or convex hull of two relations.

The function takes two arguments.

RA_WIDEN

Widen two relations.

The function takes two arguments.

RA_PROJECT

Project the columns (provided as numbers in the parameters).

The function takes one argument.

RA_FILTER

Filter (restrict) a relation with respect to a predicate.

The first argument is a relation.

The second argument is a predicate with free de-Bruijn indices corresponding to the columns of the relation.

So the first column in the relation has index 0.

RA_NEGATION_FILTER

Intersect the first relation with respect to negation of the second relation (the function takes two arguments).

Logically, the specification can be described by a function

target = filter_by_negation(pos, neg, columns)

where columns are pairs c1, d1, .., cN, dN of columns from pos and neg, such that target are elements in x in pos, such that there is no y in neg that agrees with x on the columns c1, d1, .., cN, dN.

RA_RENAME

Rename columns in the relation.

The function takes one argument.

The parameters contain the renaming as a cycle.

RA_COMPLEMENT

Complement the relation.

RA_SELECT

Check if a record is an element of the relation.

The function takes n+1 arguments, where the first argument is a relation, and the remaining n arguments correspond to a record.

RA_CLONE

Create a fresh copy (clone) of a relation.

The function is logically the identity, but in the context of a register machine allows for DeclKind::RA_UNION to perform destructive updates to the first argument.

FD_CONSTANTFD_LT

A less than predicate over the finite domain SortKind::FiniteDomain.

SEQ_UNITSEQ_EMPTYSEQ_CONCATSEQ_PREFIXSEQ_SUFFIXSEQ_CONTAINSSEQ_EXTRACTSEQ_REPLACESEQ_ATSEQ_LENGTHSEQ_INDEXSEQ_TO_RESEQ_IN_RESTR_TO_INTINT_TO_STRRE_PLUSRE_STARRE_OPTIONRE_CONCATRE_UNIONRE_RANGERE_LOOPRE_INTERSECTRE_EMPTY_SETRE_FULL_SETRE_COMPLEMENTLABEL

A label (used by the Boogie Verification condition generator).

The label has two parameters, a string and a Boolean polarity.

It takes one argument, a formula.

LABEL_LIT

A label literal (used by the Boogie Verification condition generator).

A label literal has a set of string parameters. It takes no arguments.

DT_CONSTRUCTOR

Datatype constructor.

DT_RECOGNISER

Datatype recognizer.

DT_IS

Datatype recognizer.

DT_ACCESSOR

Datatype accessor.

DT_UPDATE_FIELD

Datatype field update.

PB_AT_MOST

Cardinality constraint.

Example: x + y + z <= 2

PB_AT_LEAST

Cardinality constraint.

Example: x + y + z >= 2

PB_LE

Generalized Pseudo-Boolean cardinality constraint.

Example: 2*x + 3*y <= 4

PB_GE

Generalized Pseudo-Boolean cardinality constraint.

Example: 2*x + 3*y + 2*z >= 4

PB_EQ

Generalized Pseudo-Boolean equality constraint.

Example: 2*x + 1*y + 2*z + 1*u = 4

FPA_RM_NEAREST_TIES_TO_EVEN

Floating-point rounding mode RNE

FPA_RM_NEAREST_TIES_TO_AWAY

Floating-point rounding mode RNA

FPA_RM_TOWARD_POSITIVE

Floating-point rounding mode RTP

FPA_RM_TOWARD_NEGATIVE

Floating-point rounding mode RTN

FPA_RM_TOWARD_ZERO

Floating-point rounding mode RTZ

FPA_NUM

Floating-point value

FPA_PLUS_INF

Floating-point +oo

FPA_MINUS_INF

Floating-point -oo

FPA_NAN

Floating-point NaN

FPA_PLUS_ZERO

Floating-point +zero

FPA_MINUS_ZERO

Floating-point -zero

FPA_ADD

Floating-point addition

FPA_SUB

Floating-point subtraction

FPA_NEG

Floating-point negation

FPA_MUL

Floating-point multiplication

FPA_DIV

Floating-point division

FPA_REM

Floating-point remainder

FPA_ABS

Floating-point absolute value

FPA_MIN

Floating-point minimum

FPA_MAX

Floating-point maximum

FPA_FMA

Floating-point fused multiply-add

FPA_SQRT

Floating-point square root

FPA_ROUND_TO_INTEGRAL

Floating-point round to integral

FPA_EQ

Floating-point equality

FPA_LT

Floating-point less than

FPA_GT

Floating-point greater than

FPA_LE

Floating-point less than or equal

FPA_GE

Floating-point greater than or equal

FPA_IS_NAN

Floating-point isNaN

FPA_IS_INF

Floating-point isInfinite

FPA_IS_ZERO

Floating-point isZero

FPA_IS_NORMAL

Floating-point isNormal

FPA_IS_SUBNORMAL

Floating-point isSubnormal

FPA_IS_NEGATIVE

Floating-point isNegative

FPA_IS_POSITIVE

Floating-point isPositive

FPA_FP

Floating-point constructor from 3 bit-vectors

FPA_TO_FP

Floating-point conversion (various)

FPA_TO_FP_UNSIGNED

Floating-point conversion from unsigned bit-vector

FPA_TO_UBV

Floating-point conversion to unsigned bit-vector

FPA_TO_SBV

Floating-point conversion to signed bit-vector

FPA_TO_REAL

Floating-point conversion to real number

FPA_TO_IEEE_BV

Floating-point conversion to IEEE-754 bit-vector

FPA_BVWRAP

Implicitly) represents the internal bitvector-representation of a floating-point term (used for the lazy encoding of non-relevant terms in theory_fpa)

FPA_BV2RM

Conversion of a 3-bit bit-vector term to a floating-point rounding-mode term.

The conversion uses the following values:

0 = 000 = DeclKind::FPA_RM_NEAREST_TIES_TO_EVEN, 1 = 001 = DeclKind::FPA_RM_NEAREST_TIES_TO_AWAY, 2 = 010 = DeclKind::FPA_RM_TOWARD_POSITIVE, 3 = 011 = DeclKind::FPA_RM_TOWARD_NEGATIVE, 4 = 100 = DeclKind::FPA_RM_TOWARD_ZERO.

INTERNAL

Internal (often interpreted) symbol, but no additional information is exposed. Tools may use the string representation of the function declaration to obtain more information.

UNINTERPRETED

Kind used for uninterpreted symbols.

Trait Implementations

impl Debug for DeclKind

fn fmt(&self, __arg_0: &mut Formatter) -> Result

Formats the value using the given formatter.

impl Copy for DeclKind

impl Clone for DeclKind

fn clone(&self) -> DeclKind

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl PartialEq for DeclKind

fn eq(&self, __arg_0: &DeclKind) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

This method tests for !=.

impl Eq for DeclKind

impl Hash for DeclKind

fn hash<__H: Hasher>(&self, __arg_0: &mut __H)

Feeds this value into the given [Hasher].

fn hash_slice<H>(data: &[Self], state: &mut H) where
    H: Hasher, 

Feeds a slice of this type into the given [Hasher].