Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://z3prover.github.io/api/html/class_microsoft_1_1_z3_1_1_expr.html below:

Z3: Expr Class Reference

Expressions are terms. More...

Expressions are terms.

Definition at line 30 of file Expr.cs.

The i'th argument of the expression.

Definition at line 93 of file Expr.cs.

.Create(

, Native.Z3_get_app_arg(

.nCtx, NativeObject, i));

Expr(Context ctx, IntPtr obj)

Constructor for Expr

Context Context

Access Context object

Create a duplicate of expression. This feature is to allow extending the life-time of expressions that were passed down as arguments by the user propagator callbacks. By default the life-time of arguments to callbacks is within the callback only.

Definition at line 178 of file Expr.cs.

Returns a simplified version of the expression.

Parameters

p A set of parameters to configure the simplifier

See also

Context.SimplifyHelp

Definition at line 37 of file Expr.cs.

.Create(

, Native.Z3_simplify_ex(

.nCtx, NativeObject, p.NativeObject));

Substitute every occurrence of from in the expression with to.

See also

Substitute(Expr[],Expr[])

Definition at line 139 of file Expr.cs.

Debug.Assert(from !=

);

Debug.Assert(to !=

);

Expr Substitute(Expr[] from, Expr[] to)

Substitute every occurrence of from[i] in the expression with to[i], for i smaller than num_exprs.

Substitute every occurrence of from[i] in the expression with to[i], for i smaller than num_exprs.

The result is the new expression. 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].

Definition at line 121 of file Expr.cs.

Debug.Assert(from !=

);

Debug.Assert(to !=

);

Debug.Assert(from.All(f => f !=

));

Debug.Assert(to.All(t => t !=

));

(from.Length != to.Length)

Z3Exception(

);

.Create(

, Native.Z3_substitute(

.nCtx, NativeObject, (uint)from.Length,

.ArrayToNative(from),

.ArrayToNative(to)));

Referenced by Expr.Substitute().

Substitute the free variables in the expression 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].

Definition at line 153 of file Expr.cs.

Debug.Assert(to !=

);

Debug.Assert(to.All(t => t !=

));

.Create(

, Native.Z3_substitute_vars(

.nCtx, NativeObject, (uint)to.Length,

.ArrayToNative(to)));

Returns a string representation of the expression.

Definition at line 185 of file Expr.cs.

base.ToString();

Translates (copies) the term to the Context ctx .

Parameters

Returns

A copy of the term which is associated with ctx

Definition at line 167 of file Expr.cs.

(

)base.Translate(ctx);

Referenced by Expr.Translate().

Update the arguments of the expression using the arguments args The number of new arguments should coincide with the current number of arguments.

Definition at line 102 of file Expr.cs.

Debug.Assert(args !=

);

Debug.Assert(args.All(a => a !=

));

Z3Exception(

);

NativeObject = Native.Z3_update_term(

.nCtx, NativeObject, (uint)args.Length,

.ArrayToNative(args));

bool IsApp

Indicates whether the AST is an application

uint NumArgs

The number of arguments of the expression.

The arguments of the expression.

Definition at line 77 of file Expr.cs.

(uint i = 0; i < n; i++)

res[i] =

.Create(

, Native.Z3_get_app_arg(

.nCtx, NativeObject, i));

Retrieve bound of at-least

Definition at line 348 of file Expr.cs.

bool IsAtLeast

Indicates whether the term is at-least

FuncDecl FuncDecl

The function declaration of the function that is applied in this expression.

int Int

The int value of the parameter.

Parameter[] Parameters

The parameters of the function declaration

Retrieve bound of at-most

Definition at line 338 of file Expr.cs.

bool IsAtMost

Indicates whether the term is at-most

Indicates whether the expression is the true or false expression or something else (Z3_L_UNDEF).

Definition at line 61 of file Expr.cs.

{

(

)Native.Z3_get_bool_value(

.nCtx, NativeObject); }

Z3_lbool

Lifted Boolean type: false, undefined, true.

The function declaration of the function that is applied in this expression.

Definition at line 49 of file Expr.cs.

Referenced by Model.ConstInterp().

The de-Bruijn index of a bound variable.

Bound variables are indexed by de-Bruijn indices. It is perhaps easiest to explain the meaning of de-Bruijn indices by indicating the compilation process from non-de-Bruijn formulas to de-Bruijn format.

abs1(x, x, n) = b_n

abs1(y, x, n) = y

abs1(f(t1,...,tn), x, n) = f(abs1(t1,x,n), ..., abs1(tn,x,n))

abs1(

(x1) phi, x, n) =

(x1) (abs1(phi, x, n+1))

expr forall(expr const &x, expr const &b)

The last line is significant: the index of a bound variable is different depending on the scope in which it appears. The deeper x appears, the higher is its index.

Definition at line 1815 of file Expr.cs.

Z3Exception(

);

Native.Z3_get_index_value(

.nCtx, NativeObject);

bool IsVar

Indicates whether the AST is a BoundVariable

Indicates whether the term is addition (binary)

Definition at line 412 of file Expr.cs.

Z3_decl_kind DeclKind

The kind of the function declaration.

Z3_decl_kind

The different kinds of interpreted function kinds.

Indicates whether the term is an algebraic number

Definition at line 252 of file Expr.cs.

{

0 != Native.Z3_is_algebraic_number(

.nCtx, NativeObject); }

Indicates whether the term is an n-ary conjunction

Definition at line 303 of file Expr.cs.

Indicates whether the term is an arithmetic numeral.

Definition at line 387 of file Expr.cs.

Indicates whether the term is of an array sort.

Definition at line 469 of file Expr.cs.

(Native.Z3_is_app(

.nCtx, NativeObject) != 0 &&

Z3_sort_kind

The different kinds of Z3 types (See Z3_get_sort_kind).

Indicates whether the term is an array map.

It satisfies mapf[i] = f(a1[i],...,a_n[i]) for every i.

Definition at line 507 of file Expr.cs.

Indicates whether the term is an as-array term.

An as-array term is n array value that behaves as the function graph of the function passed as parameter.

Definition at line 514 of file Expr.cs.

Check whether expression is an at.

Returns

a Boolean

Definition at line 887 of file Expr.cs.

Indicates whether the term is at-least

Definition at line 343 of file Expr.cs.

Indicates whether the term is at-most

Definition at line 333 of file Expr.cs.

Indicates whether the term has Boolean sort.

Definition at line 264 of file Expr.cs.

Native.Z3_is_eq_sort(

.nCtx,

Native.Z3_mk_bool_sort(

.nCtx),

Native.Z3_get_sort(

.nCtx, NativeObject)) != 0);

bool IsExpr

Indicates whether the AST is an Expr

Indicates whether the terms is of bit-vector sort.

Definition at line 548 of file Expr.cs.

{

Native.Z3_get_sort_kind(

.nCtx, Native.Z3_get_sort(

.nCtx, NativeObject)) == (uint)

.Z3_BV_SORT; }

Indicates whether the term is a bit-vector addition (binary)

Definition at line 576 of file Expr.cs.

Indicates whether the term is a bit-wise AND

Definition at line 681 of file Expr.cs.

Indicates whether the term is a one-bit bit-vector with value one

Definition at line 561 of file Expr.cs.

Indicates whether the term is a one-bit bit-vector with value zero

Definition at line 566 of file Expr.cs.

Indicates whether the term is a bit-vector 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)))

Definition at line 809 of file Expr.cs.

Indicates whether the term is a bit-vector comparison

Definition at line 751 of file Expr.cs.

Indicates whether the term is a bit-vector concatenation (binary)

Definition at line 716 of file Expr.cs.

Indicates whether the term is a bit-vector extraction

Definition at line 731 of file Expr.cs.

Indicates whether the term is a bit-vector multiplication (binary)

Definition at line 586 of file Expr.cs.

Indicates whether the term is a bit-wise NAND

Definition at line 701 of file Expr.cs.

Indicates whether the term is a bit-wise NOR

Definition at line 706 of file Expr.cs.

Indicates whether the term is a bit-wise NOT

Definition at line 691 of file Expr.cs.

Indicates whether the term is a bit-vector numeral

Definition at line 556 of file Expr.cs.

Indicates whether the term is a bit-wise OR

Definition at line 686 of file Expr.cs.

Indicates whether the term is a bit-vector reduce AND

Definition at line 746 of file Expr.cs.

Indicates whether the term is a bit-vector reduce OR

Definition at line 741 of file Expr.cs.

Indicates whether the term is a bit-vector repetition

Definition at line 736 of file Expr.cs.

Indicates whether the term is a bit-vector rotate left

Definition at line 771 of file Expr.cs.

Indicates whether the term is a bit-vector rotate left (extended)

Similar to Z3_OP_ROTATE_LEFT, but it is a binary operator instead of a parametric one.

Definition at line 782 of file Expr.cs.

Indicates whether the term is a bit-vector rotate right

Definition at line 776 of file Expr.cs.

Indicates whether the term is a bit-vector rotate right (extended)

Similar to Z3_OP_ROTATE_RIGHT, but it is a binary operator instead of a parametric one.

Definition at line 788 of file Expr.cs.

Indicates whether the term is a bit-vector signed division (binary)

Definition at line 591 of file Expr.cs.

Indicates whether the term is a signed bit-vector greater-than-or-equal

Definition at line 656 of file Expr.cs.

Indicates whether the term is a signed bit-vector greater-than

Definition at line 676 of file Expr.cs.

Indicates whether the term is a bit-vector shift left

Definition at line 756 of file Expr.cs.

Indicates whether the term is a bit-vector arithmetic shift left

Definition at line 766 of file Expr.cs.

Indicates whether the term is a bit-vector logical shift right

Definition at line 761 of file Expr.cs.

Indicates whether the term is a bit-vector sign extension

Definition at line 721 of file Expr.cs.

Indicates whether the term is a signed bit-vector less-than-or-equal

Definition at line 646 of file Expr.cs.

Indicates whether the term is a signed bit-vector less-than

Definition at line 666 of file Expr.cs.

Indicates whether the term is a bit-vector signed modulus

Definition at line 611 of file Expr.cs.

Indicates whether the term is a bit-vector signed remainder (binary)

Definition at line 601 of file Expr.cs.

Indicates whether the term is a bit-vector subtraction (binary)

Definition at line 581 of file Expr.cs.

Indicates whether the term is a coercion from bit-vector to integer

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

Definition at line 802 of file Expr.cs.

Indicates whether the term is a bit-vector unsigned division (binary)

Definition at line 596 of file Expr.cs.

Indicates whether the term is an unsigned bit-vector greater-than-or-equal

Definition at line 651 of file Expr.cs.

Indicates whether the term is an unsigned bit-vector greater-than

Definition at line 671 of file Expr.cs.

Indicates whether the term is an unsigned bit-vector less-than-or-equal

Definition at line 641 of file Expr.cs.

Indicates whether the term is an unsigned bit-vector less-than

Definition at line 661 of file Expr.cs.

Indicates whether the term is a bit-vector unary minus

Definition at line 571 of file Expr.cs.

Indicates whether the term is a bit-vector unsigned remainder (binary)

Definition at line 606 of file Expr.cs.

Indicates whether the term is a bit-wise XNOR

Definition at line 711 of file Expr.cs.

Indicates whether the term is a bit-wise XOR

Definition at line 696 of file Expr.cs.

Indicates whether the term is a bit-vector ternary XOR

The meaning is given by the equivalence (xor3 l1 l2 l3) <=> (xor (xor l1 l2) l3)

Definition at line 815 of file Expr.cs.

Indicates whether the term is a bit-vector zero extension

Definition at line 726 of file Expr.cs.

Check whether expression is a concatenation.

Returns

a Boolean

Definition at line 851 of file Expr.cs.

Indicates whether the term represents a constant.

Definition at line 222 of file Expr.cs.

uint DomainSize

The size of the domain of the function declaration Arity

Indicates whether the term is a constant array.

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

Definition at line 495 of file Expr.cs.

Check whether expression is a contains.

Returns

a Boolean

Definition at line 869 of file Expr.cs.

Indicates whether the term is a default array.

For example default(const(v)) = v. The function is unary.

Definition at line 501 of file Expr.cs.

Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct).

Definition at line 293 of file Expr.cs.

Indicates whether the term is division (binary)

Definition at line 432 of file Expr.cs.

Indicates whether the term is an empty relation

Definition at line 1405 of file Expr.cs.

Indicates whether the term is an equality predicate.

Definition at line 288 of file Expr.cs.

Check whether expression is an extract.

Returns

a Boolean

Definition at line 875 of file Expr.cs.

Indicates whether the term is the constant false.

Definition at line 283 of file Expr.cs.

Indicates whether the term is of an array sort.

Definition at line 1504 of file Expr.cs.

(Native.Z3_is_app(

.nCtx, NativeObject) != 0 &&

Native.Z3_get_sort_kind(

.nCtx, Native.Z3_get_sort(

.nCtx, NativeObject)) == (uint)

.Z3_FINITE_DOMAIN_SORT);

Indicates whether the term is a less than predicate over a finite domain.

Definition at line 1516 of file Expr.cs.

Indicates whether the terms is of floating-point sort.

Definition at line 1523 of file Expr.cs.

{

Native.Z3_get_sort_kind(

.nCtx, Native.Z3_get_sort(

.nCtx, NativeObject)) == (uint)

.Z3_FLOATING_POINT_SORT; }

Indicates whether the term is a floating-point term absolute value term

Definition at line 1669 of file Expr.cs.

Indicates whether the term is a floating-point addition term

Definition at line 1638 of file Expr.cs.

Indicates whether the term is a floating-point division term

Definition at line 1659 of file Expr.cs.

Indicates whether the term is a floating-point equality term

Definition at line 1699 of file Expr.cs.

Indicates whether the term is a floating-point fused multiply-add term

Definition at line 1684 of file Expr.cs.

Indicates whether the term is a floating-point constructor term

Definition at line 1759 of file Expr.cs.

Indicates whether the term is a floating-point greater-than or equal term

Definition at line 1719 of file Expr.cs.

Indicates whether the term is a floating-point greater-than term

Definition at line 1709 of file Expr.cs.

Indicates whether the term is a floating-point isInf predicate term

Definition at line 1729 of file Expr.cs.

Indicates whether the term is a floating-point isNaN predicate term

Definition at line 1724 of file Expr.cs.

Indicates whether the term is a floating-point isNegative predicate term

Definition at line 1749 of file Expr.cs.

Indicates whether the term is a floating-point isNormal term

Definition at line 1739 of file Expr.cs.

Indicates whether the term is a floating-point isPositive predicate term

Definition at line 1754 of file Expr.cs.

Indicates whether the term is a floating-point isSubnormal predicate term

Definition at line 1744 of file Expr.cs.

Indicates whether the term is a floating-point isZero predicate term

Definition at line 1734 of file Expr.cs.

Indicates whether the term is a floating-point less-than or equal term

Definition at line 1714 of file Expr.cs.

Indicates whether the term is a floating-point less-than term

Definition at line 1704 of file Expr.cs.

Indicates whether the term is a floating-point maximum term

Definition at line 1679 of file Expr.cs.

Indicates whether the term is a floating-point minimum term

Definition at line 1674 of file Expr.cs.

Indicates whether the term is a floating-point -oo

Definition at line 1618 of file Expr.cs.

Indicates whether the term is a floating-point -zero

Definition at line 1633 of file Expr.cs.

Indicates whether the term is a floating-point multiplication term

Definition at line 1654 of file Expr.cs.

Indicates whether the term is a floating-point NaN

Definition at line 1623 of file Expr.cs.

Indicates whether the term is a floating-point negation term

Definition at line 1649 of file Expr.cs.

Indicates whether the term is a floating-point numeral

Definition at line 1539 of file Expr.cs.

bool IsFP

Indicates whether the terms is of floating-point sort.

bool IsNumeral

Indicates whether the term is a numeral

Indicates whether the term is a floating-point +oo

Definition at line 1613 of file Expr.cs.

Indicates whether the term is a floating-point +zero

Definition at line 1628 of file Expr.cs.

Indicates whether the term is a floating-point remainder term

Definition at line 1664 of file Expr.cs.

Indicates whether the terms is of floating-point rounding mode sort.

Definition at line 1531 of file Expr.cs.

{

Native.Z3_get_sort_kind(

.nCtx, Native.Z3_get_sort(

.nCtx, NativeObject)) == (uint)

.Z3_ROUNDING_MODE_SORT; }

Indicates whether the term is a floating-point rounding mode numeral

Definition at line 1599 of file Expr.cs.

Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway

Definition at line 1579 of file Expr.cs.

Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven

Definition at line 1574 of file Expr.cs.

Indicates whether the term is the floating-point rounding numeral roundTowardNegative

Definition at line 1584 of file Expr.cs.

Indicates whether the term is the floating-point rounding numeral roundTowardPositive

Definition at line 1589 of file Expr.cs.

Indicates whether the term is the floating-point rounding numeral roundTowardZero

Definition at line 1594 of file Expr.cs.

Indicates whether the term is a floating-point rounding mode numeral

Definition at line 1544 of file Expr.cs.

bool IsFPRM

Indicates whether the terms is of floating-point rounding mode sort.

Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway

Definition at line 1554 of file Expr.cs.

Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven

Definition at line 1549 of file Expr.cs.

Indicates whether the term is the floating-point rounding numeral roundTowardNegative

Definition at line 1559 of file Expr.cs.

Indicates whether the term is the floating-point rounding numeral roundTowardPositive

Definition at line 1564 of file Expr.cs.

Indicates whether the term is the floating-point rounding numeral roundTowardZero

Definition at line 1569 of file Expr.cs.

Indicates whether the term is a floating-point roundToIntegral term

Definition at line 1694 of file Expr.cs.

Indicates whether the term is a floating-point square root term

Definition at line 1689 of file Expr.cs.

Indicates whether the term is a floating-point subtraction term

Definition at line 1644 of file Expr.cs.

Indicates whether the term is a floating-point conversion term

Definition at line 1764 of file Expr.cs.

Indicates whether the term is a floating-point conversion from unsigned bit-vector term

Definition at line 1769 of file Expr.cs.

Indicates whether the term is a floating-point conversion to IEEE-754 bit-vector term

Definition at line 1790 of file Expr.cs.

Indicates whether the term is a floating-point conversion to real term

Definition at line 1784 of file Expr.cs.

Indicates whether the term is a floating-point conversion to signed bit-vector term

Definition at line 1779 of file Expr.cs.

Indicates whether the term is a floating-point conversion to unsigned bit-vector term

Definition at line 1774 of file Expr.cs.

Indicates whether the term is a greater-than-or-equal

Definition at line 397 of file Expr.cs.

Indicates whether the term is a greater-than

Definition at line 407 of file Expr.cs.

Indicates whether the term is integer division (binary)

Definition at line 437 of file Expr.cs.

Indicates whether the term is an if-and-only-if (Boolean equivalence, binary)

Definition at line 313 of file Expr.cs.

Indicates whether the term is an implication

Definition at line 328 of file Expr.cs.

Check whether expression is a sequence index.

Returns

a Boolean

Definition at line 899 of file Expr.cs.

Indicates whether the term is of integer sort.

Definition at line 371 of file Expr.cs.

{

Native.Z3_get_sort_kind(

.nCtx, Native.Z3_get_sort(

.nCtx, NativeObject)) == (uint)

.Z3_INT_SORT; }

Indicates whether the term is an integer numeral.

Definition at line 232 of file Expr.cs.

bool IsInt

Indicates whether the term is of integer sort.

Indicates whether the term is a coercion from integer to bit-vector

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

Definition at line 795 of file Expr.cs.

Indicates whether the term is a coercion of integer to real (unary)

Definition at line 452 of file Expr.cs.

Indicates whether the term is a test for the emptiness of a relation

Definition at line 1410 of file Expr.cs.

Indicates whether the term is a ternary if-then-else term

Definition at line 298 of file Expr.cs.

Indicates whether the term is 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.

Definition at line 824 of file Expr.cs.

Indicates whether the term is a label literal (used by the Boogie Verification condition generator).

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

Definition at line 830 of file Expr.cs.

Indicates whether the term is a less-than-or-equal

Definition at line 392 of file Expr.cs.

Check whether expression is a sequence length.

Returns

a Boolean

Definition at line 893 of file Expr.cs.

Indicates whether the term is a less-than

Definition at line 402 of file Expr.cs.

Indicates whether the term is modulus (binary)

Definition at line 447 of file Expr.cs.

Indicates whether the term is multiplication (binary)

Definition at line 427 of file Expr.cs.

Indicates whether the term is a negation

Definition at line 323 of file Expr.cs.

Indicates whether the term is a numeral

Definition at line 193 of file Expr.cs.

{

Native.Z3_is_numeral_ast(

.nCtx, NativeObject) != 0; }

Indicates whether the term is a binary equivalence modulo namings.

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

Definition at line 910 of file Expr.cs.

Indicates whether the term is an n-ary disjunction

Definition at line 308 of file Expr.cs.

Indicates whether the term is pbeq

Definition at line 353 of file Expr.cs.

Indicates whether the term is pbge

Definition at line 363 of file Expr.cs.

Indicates whether the term is pble

Definition at line 358 of file Expr.cs.

Check whether expression is a prefix.

Returns

a Boolean

Definition at line 857 of file Expr.cs.

Indicates whether the term is a proof by elimination of AND

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

Definition at line 1041 of file Expr.cs.

Indicates whether the term is a proof for application of a definition

[apply-def T1]: F ~ n F is 'equivalent' to n, given that T1 is a proof that n is a name for F.

Definition at line 1270 of file Expr.cs.

Indicates whether the term is a proof for a fact asserted by the user.

Definition at line 920 of file Expr.cs.

Indicates whether the term is a proof by commutativity

f is a commutative operator.

This proof object has no antecedents. Remark: if f is bool, then = is iff.

Definition at line 1201 of file Expr.cs.

Indicates whether the term is a proof for Tseitin-like axioms

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).

Definition at line 1237 of file Expr.cs.

Indicates whether the term is a proof for introduction of a name

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:

or:

when e only occurs positively.

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

Otherwise: [def-intro]: (= n e)

Definition at line 1260 of file Expr.cs.

Indicates whether the term is a proof for destructive equality resolution

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.

Definition at line 1131 of file Expr.cs.

Indicates whether the term is a 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.

Definition at line 1031 of file Expr.cs.

Indicates whether the term is a proof for elimination of unused variables.

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.

Definition at line 1117 of file Expr.cs.

Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user.

Definition at line 925 of file Expr.cs.

Indicates whether the term is a hypothesis marker.

Mark a hypothesis in a natural deduction style proof.

Definition at line 1145 of file Expr.cs.

Indicates whether the term is a proof by iff-false

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

Definition at line 1188 of file Expr.cs.

Indicates whether the term is a proof iff-oeq

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

Definition at line 1279 of file Expr.cs.

Indicates whether the term is a proof by iff-true

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

Definition at line 1179 of file Expr.cs.

Indicates whether the term is a proof by lemma

T1: false

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 hypotheses: l_1, ..., l_n.

Definition at line 1158 of file Expr.cs.

Indicates whether the term is proof via 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)

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

Definition at line 936 of file Expr.cs.

Indicates whether the term is a proof by modus ponens for equi-satisfiability.

Modus ponens style rule for equi-satisfiability. T1: p T2: (~ p q)

Definition at line 1356 of file Expr.cs.

Indicates whether the term is a monotonicity proof object.

T1: (R t_1 s_1) ... Tn: (R t_n s_n)

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

Definition at line 1003 of file Expr.cs.

Indicates whether the term is a proof for a negative NNF step

Proof for a (negative) NNF step. Examples:

T1: (not s_1) ~ r_1 ... Tn: (not s_n) ~ r_n

and T1: (not s_1) ~ r_1 ... Tn: (not s_n) ~ 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'

(and (or r_1 r_2) (or r_1' r_2')))

Definition at line 1332 of file Expr.cs.

Indicates whether the term is a proof for a positive NNF step

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'

(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: (a) When creating the NNF of a positive force quantifier. The quantifier is retained (unless the bound variables are eliminated). Example T1: q ~ q_new

(b) 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'.

Definition at line 1307 of file Expr.cs.

Indicates whether the term is a proof by elimination of not-or

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)

Definition at line 1051 of file Expr.cs.

Indicates whether the term is a proof for pulling quantifiers out.

A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents.

Definition at line 1091 of file Expr.cs.

Indicates whether the term is a proof for pushing quantifiers in.

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

Definition at line 1105 of file Expr.cs.

Indicates whether the term is a proof for quantifier instantiation

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

Definition at line 1139 of file Expr.cs.

Indicates whether the term is a quant-intro proof

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

Definition at line 1013 of file Expr.cs.

Indicates whether the term is 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'.

Definition at line 945 of file Expr.cs.

Indicates whether the term is a proof by rewriting

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)

Definition at line 1070 of file Expr.cs.

Indicates whether the term is a proof by rewriting

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 used in a few cases:

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

Definition at line 1083 of file Expr.cs.

Indicates whether the term is a proof for a Skolemization step

Proof for:

This proof object has no antecedents.

Definition at line 1345 of file Expr.cs.

Indicates whether the term is proof by symmetricity of a relation

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.

Definition at line 956 of file Expr.cs.

Indicates whether the term is a proof for theory 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.

Definition at line 1375 of file Expr.cs.

Indicates whether the term is a proof by transitivity of a relation

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)

Definition at line 968 of file Expr.cs.

Indicates whether the term is a proof by condensed transitivity of a relation

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.

Definition at line 989 of file Expr.cs.

Indicates whether the term is a Proof for the expression 'true'.

Definition at line 915 of file Expr.cs.

Indicates whether the term is a proof by 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')

Definition at line 1170 of file Expr.cs.

Indicates whether the term is a real numeral.

Definition at line 242 of file Expr.cs.

bool IsReal

Indicates whether the term is of sort real.

Indicates whether the term is of sort real.

Definition at line 379 of file Expr.cs.

{

Native.Z3_get_sort_kind(

.nCtx, Native.Z3_get_sort(

.nCtx, NativeObject)) == (uint)

.Z3_REAL_SORT; }

Indicates whether the term is a check that tests whether a real is integral (unary)

Definition at line 462 of file Expr.cs.

Indicates whether the term is a coercion of real to integer (unary)

Definition at line 457 of file Expr.cs.

Indicates whether the term is of relation sort.

Definition at line 1382 of file Expr.cs.

(Native.Z3_is_app(

.nCtx, NativeObject) != 0 &&

Native.Z3_get_sort_kind(

.nCtx, Native.Z3_get_sort(

.nCtx, NativeObject))

Indicates whether the term is a relational join

Definition at line 1415 of file Expr.cs.

Indicates whether the term is a relational clone (copy)

Create a fresh copy (clone) of a relation. The function is logically the identity, but in the context of a register machine allows for terms of kind

See also

IsRelationUnion

to perform destructive updates to the first argument.

Definition at line 1497 of file Expr.cs.

Indicates whether the term is the complement of a relation

Definition at line 1475 of file Expr.cs.

Indicates whether the term is a relation 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.

Definition at line 1445 of file Expr.cs.

Indicates whether the term is an intersection of a relation with the negation of another.

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.

Definition at line 1461 of file Expr.cs.

Indicates whether the term is a projection of columns (provided as numbers in the parameters).

The function takes one argument.

Definition at line 1433 of file Expr.cs.

Indicates whether the term is the renaming of a column in a relation

The function takes one argument. The parameters contain the renaming as a cycle.

Definition at line 1470 of file Expr.cs.

Indicates whether the term is a relational 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.

Definition at line 1485 of file Expr.cs.

Indicates whether the term is an relation 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.

Definition at line 1400 of file Expr.cs.

Indicates whether the term is the union or convex hull of two relations.

The function takes two arguments.

Definition at line 1421 of file Expr.cs.

Indicates whether the term is the widening of two relations

The function takes two arguments.

Definition at line 1427 of file Expr.cs.

Indicates whether the term is remainder (binary)

Definition at line 442 of file Expr.cs.

Check whether expression is a replace.

Returns

a Boolean

Definition at line 881 of file Expr.cs.

Indicates whether the term is an array select.

Definition at line 489 of file Expr.cs.

Indicates whether the term is set complement

Definition at line 536 of file Expr.cs.

Indicates whether the term is set difference

Definition at line 531 of file Expr.cs.

Indicates whether the term is set intersection

Definition at line 526 of file Expr.cs.

Indicates whether the term is set subset

Definition at line 541 of file Expr.cs.

Indicates whether the term is set union

Definition at line 521 of file Expr.cs.

Indicates whether the term is an 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.

Definition at line 484 of file Expr.cs.

Check whether expression is a string constant.

Returns

a Boolean

Definition at line 839 of file Expr.cs.

{

{

&& Native.Z3_is_string(

.nCtx, NativeObject) != 0; } }

Indicates whether the term is subtraction (binary)

Definition at line 417 of file Expr.cs.

Check whether expression is a suffix.

Returns

a Boolean

Definition at line 863 of file Expr.cs.

Indicates whether the term is the constant true.

Definition at line 278 of file Expr.cs.

Indicates whether the term is a unary minus

Definition at line 422 of file Expr.cs.

Indicates whether the term is well-sorted.

Returns

True if the term is well-sorted, false otherwise.

Definition at line 202 of file Expr.cs.

{

Native.Z3_is_well_sorted(

.nCtx, NativeObject) != 0; }

Indicates whether the term is an exclusive or

Definition at line 318 of file Expr.cs.

The number of arguments of the expression.

Definition at line 69 of file Expr.cs.

{

Native.Z3_get_app_num_args(

.nCtx, NativeObject); }

Referenced by Expr.Update().

The Sort of the term.

Definition at line 210 of file Expr.cs.

Sort Sort

The Sort of the term.

Retrieve string corresponding to string constant.

the expression should be a string constant, (IsString should be true).

Definition at line 845 of file Expr.cs.

{

{

Native.Z3_get_string(

.nCtx, NativeObject); } }

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4