Z3
Expr.cs
Go to the documentation of this file.
1/*++
2Copyright (<c>) 2012 Microsoft Corporation
3
4Module Name:
5
6 Expr.cs
7
8Abstract:
9
10 Z3 Managed API: Expressions
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2012-03-20
15
16Notes:
17
18--*/
19
20using System.Diagnostics;
21using System;
22using System.Linq;
23
24
25namespace Microsoft.Z3
26{
30 public class Expr : AST
31 {
37 public Expr Simplify(Params p = null)
38 {
39
40 if (p == null)
41 return Expr.Create(Context, Native.Z3_simplify(Context.nCtx, NativeObject));
42 else
43 return Expr.Create(Context, Native.Z3_simplify_ex(Context.nCtx, NativeObject, p.NativeObject));
44 }
45
50 {
51 get
52 {
53 return new FuncDecl(Context, Native.Z3_get_app_decl(Context.nCtx, NativeObject));
54 }
55 }
56
62 {
63 get { return (Z3_lbool)Native.Z3_get_bool_value(Context.nCtx, NativeObject); }
64 }
65
69 public uint NumArgs
70 {
71 get { return Native.Z3_get_app_num_args(Context.nCtx, NativeObject); }
72 }
73
77 public Expr[] Args
78 {
79 get
80 {
81
82 uint n = NumArgs;
83 Expr[] res = new Expr[n];
84 for (uint i = 0; i < n; i++)
85 res[i] = Expr.Create(Context, Native.Z3_get_app_arg(Context.nCtx, NativeObject, i));
86 return res;
87 }
88 }
89
93 public Expr Arg(uint i)
94 {
95 return Expr.Create(Context, Native.Z3_get_app_arg(Context.nCtx, NativeObject, i));
96 }
97
102 public void Update(Expr[] args)
103 {
104 Debug.Assert(args != null);
105 Debug.Assert(args.All(a => a != null));
106
107 Context.CheckContextMatch<Expr>(args);
108 if (IsApp && args.Length != NumArgs)
109 throw new Z3Exception("Number of arguments does not match");
110 NativeObject = Native.Z3_update_term(Context.nCtx, NativeObject, (uint)args.Length, Expr.ArrayToNative(args));
111 }
112
121 public Expr Substitute(Expr[] from, Expr[] to)
122 {
123 Debug.Assert(from != null);
124 Debug.Assert(to != null);
125 Debug.Assert(from.All(f => f != null));
126 Debug.Assert(to.All(t => t != null));
127
128 Context.CheckContextMatch<Expr>(from);
129 Context.CheckContextMatch<Expr>(to);
130 if (from.Length != to.Length)
131 throw new Z3Exception("Argument sizes do not match");
132 return Expr.Create(Context, Native.Z3_substitute(Context.nCtx, NativeObject, (uint)from.Length, Expr.ArrayToNative(from), Expr.ArrayToNative(to)));
133 }
134
139 public Expr Substitute(Expr from, Expr to)
140 {
141 Debug.Assert(from != null);
142 Debug.Assert(to != null);
143
144 return Substitute(new Expr[] { from }, new Expr[] { to });
145 }
146
154 {
155 Debug.Assert(to != null);
156 Debug.Assert(to.All(t => t != null));
157
158 Context.CheckContextMatch<Expr>(to);
159 return Expr.Create(Context, Native.Z3_substitute_vars(Context.nCtx, NativeObject, (uint)to.Length, Expr.ArrayToNative(to)));
160 }
161
167 new public Expr Translate(Context ctx)
168 {
169 return (Expr)base.Translate(ctx);
170 }
171
175 public override string ToString()
176 {
177 return base.ToString();
178 }
179
183 public bool IsNumeral
184 {
185 get { return Native.Z3_is_numeral_ast(Context.nCtx, NativeObject) != 0; }
186 }
187
192 public bool IsWellSorted
193 {
194 get { return Native.Z3_is_well_sorted(Context.nCtx, NativeObject) != 0; }
195 }
196
200 public Sort Sort
201 {
202 get
203 {
204 return Sort.Create(Context, Native.Z3_get_sort(Context.nCtx, NativeObject));
205 }
206 }
207
208 #region Constants
212 public bool IsConst
213 {
214 get { return IsApp && NumArgs == 0 && FuncDecl.DomainSize == 0; }
215 }
216 #endregion
217
218 #region Integer Numerals
222 public bool IsIntNum
223 {
224 get { return IsNumeral && IsInt; }
225 }
226 #endregion
227
228 #region Real Numerals
232 public bool IsRatNum
233 {
234 get { return IsNumeral && IsReal; }
235 }
236 #endregion
237
238 #region Algebraic Numbers
243 {
244 get { return 0 != Native.Z3_is_algebraic_number(Context.nCtx, NativeObject); }
245 }
246 #endregion
247
248 #region Term Kind Tests
249
250 #region Boolean Terms
254 public bool IsBool
255 {
256 get
257 {
258 return (IsExpr &&
259 Native.Z3_is_eq_sort(Context.nCtx,
260 Native.Z3_mk_bool_sort(Context.nCtx),
261 Native.Z3_get_sort(Context.nCtx, NativeObject)) != 0);
262 }
263 }
264
268 public bool IsTrue { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TRUE; } }
269
273 public bool IsFalse { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FALSE; } }
274
278 public bool IsEq { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EQ; } }
279
283 public bool IsDistinct { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DISTINCT; } }
284
288 public bool IsITE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ITE; } }
289
293 public bool IsAnd { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AND; } }
294
298 public bool IsOr { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OR; } }
299
303 public bool IsIff { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IFF; } }
304
308 public bool IsXor { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR; } }
309
313 public bool IsNot { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_NOT; } }
314
318 public bool IsImplies { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IMPLIES; } }
319
323 public bool IsAtMost { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_AT_MOST; } }
324
328 public uint AtMostBound { get { Debug.Assert(IsAtMost); return (uint)FuncDecl.Parameters[0].Int; } }
329
333 public bool IsAtLeast { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_AT_LEAST; } }
334
338 public uint AtLeastBound { get { Debug.Assert(IsAtLeast); return (uint)FuncDecl.Parameters[0].Int; } }
339
343 public bool IsPbEq { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_EQ; } }
344
348 public bool IsPbLe { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_LE; } }
349
353 public bool IsPbGe { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PB_GE; } }
354
355 #endregion
356
357 #region Arithmetic Terms
361 public bool IsInt
362 {
363 get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_INT_SORT; }
364 }
365
369 public bool IsReal
370 {
371 get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_REAL_SORT; }
372 }
373
377 public bool IsArithmeticNumeral { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ANUM; } }
378
382 public bool IsLE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LE; } }
383
387 public bool IsGE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GE; } }
388
392 public bool IsLT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LT; } }
393
397 public bool IsGT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GT; } }
398
402 public bool IsAdd { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ADD; } }
403
407 public bool IsSub { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SUB; } }
408
412 public bool IsUMinus { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UMINUS; } }
413
417 public bool IsMul { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MUL; } }
418
422 public bool IsDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DIV; } }
423
427 public bool IsIDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IDIV; } }
428
432 public bool IsRemainder { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REM; } }
433
437 public bool IsModulus { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MOD; } }
438
442 public bool IsIntToReal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_REAL; } }
443
447 public bool IsRealToInt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_INT; } }
448
452 public bool IsRealIsInt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IS_INT; } }
453 #endregion
454
455 #region Array Terms
459 public bool IsArray
460 {
461 get
462 {
463 return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
464 (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
465 == Z3_sort_kind.Z3_ARRAY_SORT);
466 }
467 }
468
474 public bool IsStore { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_STORE; } }
475
479 public bool IsSelect { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SELECT; } }
480
485 public bool IsConstantArray { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONST_ARRAY; } }
486
491 public bool IsDefaultArray { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT; } }
492
497 public bool IsArrayMap { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_MAP; } }
498
504 public bool IsAsArray { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AS_ARRAY; } }
505 #endregion
506
507 #region Set Terms
511 public bool IsSetUnion { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_UNION; } }
512
516 public bool IsSetIntersect { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_INTERSECT; } }
517
521 public bool IsSetDifference { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_DIFFERENCE; } }
522
526 public bool IsSetComplement { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_COMPLEMENT; } }
527
531 public bool IsSetSubset { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_SUBSET; } }
532 #endregion
533
534 #region Bit-vector terms
538 public bool IsBV
539 {
540 get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_BV_SORT; }
541 }
542
546 public bool IsBVNumeral { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNUM; } }
547
551 public bool IsBVBitOne { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT1; } }
552
556 public bool IsBVBitZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT0; } }
557
561 public bool IsBVUMinus { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNEG; } }
562
566 public bool IsBVAdd { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BADD; } }
567
571 public bool IsBVSub { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSUB; } }
572
576 public bool IsBVMul { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BMUL; } }
577
581 public bool IsBVSDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV; } }
582
586 public bool IsBVUDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV; } }
587
591 public bool IsBVSRem { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM; } }
592
596 public bool IsBVURem { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM; } }
597
601 public bool IsBVSMod { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD; } }
602
606 internal bool IsBVSDiv0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV0; } }
607
611 internal bool IsBVUDiv0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV0; } }
612
616 internal bool IsBVSRem0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM0; } }
617
621 internal bool IsBVURem0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM0; } }
622
626 internal bool IsBVSMod0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD0; } }
627
631 public bool IsBVULE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULEQ; } }
632
636 public bool IsBVSLE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLEQ; } }
637
641 public bool IsBVUGE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGEQ; } }
642
646 public bool IsBVSGE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGEQ; } }
647
651 public bool IsBVULT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULT; } }
652
656 public bool IsBVSLT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLT; } }
657
661 public bool IsBVUGT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGT; } }
662
666 public bool IsBVSGT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGT; } }
667
671 public bool IsBVAND { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BAND; } }
672
676 public bool IsBVOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BOR; } }
677
681 public bool IsBVNOT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOT; } }
682
686 public bool IsBVXOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXOR; } }
687
691 public bool IsBVNAND { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNAND; } }
692
696 public bool IsBVNOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOR; } }
697
701 public bool IsBVXNOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXNOR; } }
702
706 public bool IsBVConcat { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONCAT; } }
707
711 public bool IsBVSignExtension { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SIGN_EXT; } }
712
716 public bool IsBVZeroExtension { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ZERO_EXT; } }
717
721 public bool IsBVExtract { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXTRACT; } }
722
726 public bool IsBVRepeat { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REPEAT; } }
727
731 public bool IsBVReduceOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDOR; } }
732
736 public bool IsBVReduceAND { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDAND; } }
737
741 public bool IsBVComp { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BCOMP; } }
742
746 public bool IsBVShiftLeft { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSHL; } }
747
751 public bool IsBVShiftRightLogical { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BLSHR; } }
752
756 public bool IsBVShiftRightArithmetic { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BASHR; } }
757
761 public bool IsBVRotateLeft { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_LEFT; } }
762
766 public bool IsBVRotateRight { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_RIGHT; } }
767
772 public bool IsBVRotateLeftExtended { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT; } }
773
778 public bool IsBVRotateRightExtended { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT; } }
779
785 public bool IsIntToBV { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_INT2BV; } }
786
792 public bool IsBVToInt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BV2INT; } }
793
799 public bool IsBVCarry { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CARRY; } }
800
805 public bool IsBVXOR3 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR3; } }
806
807 #endregion
808
809 #region Labels
814 public bool IsLabel { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL; } }
815
820 public bool IsLabelLit { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } }
821 #endregion
822
823 #region Sequences and Strings
824
829 public bool IsString { get { return IsApp && Native.Z3_is_string(Context.nCtx, NativeObject) != 0; } }
830
835 public string String { get { return Native.Z3_get_string(Context.nCtx, NativeObject); } }
836
841 public bool IsConcat { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_CONCAT; } }
842
847 public bool IsPrefix { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_PREFIX; } }
848
853 public bool IsSuffix { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_SUFFIX; } }
854
859 public bool IsContains { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_CONTAINS; } }
860
865 public bool IsExtract { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_EXTRACT; } }
866
871 public bool IsReplace { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_REPLACE; } }
872
877 public bool IsAt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_AT; } }
878
883 public bool IsLength { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_LENGTH; } }
884
889 public bool IsIndex { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_INDEX; } }
890
891
892 #endregion
893
894 #region Proof Terms
900 public bool IsOEQ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OEQ; } }
901
905 public bool IsProofTrue { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRUE; } }
906
910 public bool IsProofAsserted { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ASSERTED; } }
911
915 public bool IsProofGoal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_GOAL; } }
916
926 public bool IsProofModusPonens { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS; } }
927
935 public bool IsProofReflexivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY; } }
936
946 public bool IsProofSymmetry { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SYMMETRY; } }
947
958 public bool IsProofTransitivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY; } }
959
979 public bool IsProofTransitivityStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR; } }
980
981
993 public bool IsProofMonotonicity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MONOTONICITY; } }
994
1003 public bool IsProofQuantIntro { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO; } }
1004
1021 public bool IsProofDistributivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY; } }
1022
1031 public bool IsProofAndElimination { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_AND_ELIM; } }
1032
1041 public bool IsProofOrElimination { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM; } }
1042
1060 public bool IsProofRewrite { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE; } }
1061
1073 public bool IsProofRewriteStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR; } }
1074
1081 public bool IsProofPullQuant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT; } }
1082
1083
1095 public bool IsProofPushQuant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT; } }
1096
1107 public bool IsProofElimUnusedVars { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS; } }
1108
1121 public bool IsProofDER { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DER; } }
1122
1129 public bool IsProofQuantInst { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INST; } }
1130
1135 public bool IsProofHypothesis { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS; } }
1136
1148 public bool IsProofLemma { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_LEMMA; } }
1149
1160 public bool IsProofUnitResolution { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION; } }
1161
1169 public bool IsProofIFFTrue { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_TRUE; } }
1170
1178 public bool IsProofIFFFalse { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_FALSE; } }
1179
1191 public bool IsProofCommutativity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY; } }
1192
1227 public bool IsProofDefAxiom { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM; } }
1228
1250 public bool IsProofDefIntro { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_INTRO; } }
1251
1260 public bool IsProofApplyDef { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_APPLY_DEF; } }
1261
1269 public bool IsProofIFFOEQ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_OEQ; } }
1270
1297 public bool IsProofNNFPos { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_POS; } }
1298
1322 public bool IsProofNNFNeg { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_NEG; } }
1323
1335 public bool IsProofSkolemize { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE; } }
1336
1346 public bool IsProofModusPonensOEQ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ; } }
1347
1365 public bool IsProofTheoryLemma { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TH_LEMMA; } }
1366 #endregion
1367
1368 #region Relational Terms
1372 public bool IsRelation
1373 {
1374 get
1375 {
1376 return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
1377 Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
1378 == (uint)Z3_sort_kind.Z3_RELATION_SORT);
1379 }
1380 }
1381
1390 public bool IsRelationStore { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_STORE; } }
1391
1395 public bool IsEmptyRelation { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_EMPTY; } }
1396
1400 public bool IsIsEmptyRelation { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_IS_EMPTY; } }
1401
1405 public bool IsRelationalJoin { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_JOIN; } }
1406
1411 public bool IsRelationUnion { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_UNION; } }
1412
1417 public bool IsRelationWiden { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_WIDEN; } }
1418
1423 public bool IsRelationProject { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_PROJECT; } }
1424
1435 public bool IsRelationFilter { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_FILTER; } }
1436
1451 public bool IsRelationNegationFilter { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER; } }
1452
1460 public bool IsRelationRename { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_RENAME; } }
1461
1465 public bool IsRelationComplement { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_COMPLEMENT; } }
1466
1475 public bool IsRelationSelect { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_SELECT; } }
1476
1487 public bool IsRelationClone { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_CLONE; } }
1488 #endregion
1489
1490 #region Finite domain terms
1494 public bool IsFiniteDomain
1495 {
1496 get
1497 {
1498 return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
1499 Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_FINITE_DOMAIN_SORT);
1500 }
1501 }
1502
1506 public bool IsFiniteDomainLT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FD_LT; } }
1507 #endregion
1508
1509 #region Floating-point terms
1513 public bool IsFP
1514 {
1515 get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_FLOATING_POINT_SORT; }
1516 }
1517
1521 public bool IsFPRM
1522 {
1523 get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_ROUNDING_MODE_SORT; }
1524 }
1525
1529 public bool IsFPNumeral { get { return IsFP && IsNumeral; } }
1530
1534 public bool IsFPRMNumeral { get { return IsFPRM && IsNumeral; } }
1535
1539 public bool IsFPRMRoundNearestTiesToEven{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } }
1540
1544 public bool IsFPRMRoundNearestTiesToAway{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }
1545
1549 public bool IsFPRMRoundTowardNegative{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } }
1550
1554 public bool IsFPRMRoundTowardPositive{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } }
1555
1559 public bool IsFPRMRoundTowardZero{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } }
1560
1564 public bool IsFPRMExprRNE{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } }
1565
1569 public bool IsFPRMExprRNA { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }
1570
1574 public bool IsFPRMExprRTN { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } }
1575
1579 public bool IsFPRMExprRTP { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } }
1580
1584 public bool IsFPRMExprRTZ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } }
1585
1589 public bool IsFPRMExpr {
1590 get {
1591 return IsApp &&
1592 (FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY||
1593 FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN ||
1594 FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE ||
1595 FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE ||
1596 FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO);
1597 }
1598 }
1599
1603 public bool IsFPPlusInfinity{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_PLUS_INF; } }
1604
1608 public bool IsFPMinusInfinity{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MINUS_INF; } }
1609
1613 public bool IsFPNaN { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_NAN; } }
1614
1618 public bool IsFPPlusZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_PLUS_ZERO; } }
1619
1623 public bool IsFPMinusZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MINUS_ZERO; } }
1624
1628 public bool IsFPAdd { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_ADD; } }
1629
1630
1634 public bool IsFPSub { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_SUB; } }
1635
1639 public bool IsFPNeg { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_NEG; } }
1640
1644 public bool IsFPMul { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MUL; } }
1645
1649 public bool IsFPDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_DIV; } }
1650
1654 public bool IsFPRem { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_REM; } }
1655
1659 public bool IsFPAbs { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_ABS; } }
1660
1664 public bool IsFPMin { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MIN; } }
1665
1669 public bool IsFPMax { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MAX; } }
1670
1674 public bool IsFPFMA { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_FMA; } }
1675
1679 public bool IsFPSqrt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_SQRT; } }
1680
1684 public bool IsFPRoundToIntegral { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_ROUND_TO_INTEGRAL; } }
1685
1689 public bool IsFPEq { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_EQ; } }
1690
1694 public bool IsFPLt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_LT; } }
1695
1699 public bool IsFPGt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_GT; } }
1700
1704 public bool IsFPLe { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_LE; } }
1705
1709 public bool IsFPGe { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_GE; } }
1710
1714 public bool IsFPisNaN { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_NAN; } }
1715
1719 public bool IsFPisInf { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_INF; } }
1720
1724 public bool IsFPisZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_ZERO; } }
1725
1729 public bool IsFPisNormal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_NORMAL; } }
1730
1734 public bool IsFPisSubnormal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_SUBNORMAL; } }
1735
1739 public bool IsFPisNegative { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_NEGATIVE; } }
1740
1744 public bool IsFPisPositive { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_POSITIVE; } }
1745
1749 public bool IsFPFP { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_FP; } }
1750
1754 public bool IsFPToFp { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_FP; } }
1755
1759 public bool IsFPToFpUnsigned { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_FP_UNSIGNED; } }
1760
1764 public bool IsFPToUBV { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_UBV; } }
1765
1769 public bool IsFPToSBV { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_SBV; } }
1770
1774 public bool IsFPToReal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_REAL; } }
1775
1776
1780 public bool IsFPToIEEEBV { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_IEEE_BV; } }
1781
1782 #endregion
1783 #endregion
1784
1785 #region Bound Variables
1805 public uint Index
1806 {
1807 get
1808 {
1809 if (!IsVar)
1810 throw new Z3Exception("Term is not a bound variable.");
1811
1812 return Native.Z3_get_index_value(Context.nCtx, NativeObject);
1813 }
1814 }
1815 #endregion
1816
1817 #region Internal
1821 internal protected Expr(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
1822
1823#if DEBUG
1824 internal override void CheckNativeObject(IntPtr obj)
1825 {
1826 if (Native.Z3_is_app(Context.nCtx, obj) == 0 &&
1827 Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_VAR_AST &&
1828 Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_QUANTIFIER_AST)
1829 throw new Z3Exception("Underlying object is not a term");
1830 base.CheckNativeObject(obj);
1831 }
1832#endif
1833
1834 internal static Expr Create(Context ctx, FuncDecl f, params Expr[] arguments)
1835 {
1836 Debug.Assert(ctx != null);
1837 Debug.Assert(f != null);
1838
1839 IntPtr obj = Native.Z3_mk_app(ctx.nCtx, f.NativeObject,
1840 AST.ArrayLength(arguments),
1841 AST.ArrayToNative(arguments));
1842 return Create(ctx, obj);
1843 }
1844
1845 new internal static Expr Create(Context ctx, IntPtr obj)
1846 {
1847 Debug.Assert(ctx != null);
1848
1849 Z3_ast_kind k = (Z3_ast_kind)Native.Z3_get_ast_kind(ctx.nCtx, obj);
1850 if (k == Z3_ast_kind.Z3_QUANTIFIER_AST)
1851 return new Quantifier(ctx, obj);
1852 IntPtr s = Native.Z3_get_sort(ctx.nCtx, obj);
1853 Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, s);
1854
1855 if (0 != Native.Z3_is_algebraic_number(ctx.nCtx, obj)) // is this a numeral ast?
1856 return new AlgebraicNum(ctx, obj);
1857
1858 if (Native.Z3_is_numeral_ast(ctx.nCtx, obj) != 0)
1859 {
1860
1861 switch (sk)
1862 {
1863 case Z3_sort_kind.Z3_INT_SORT: return new IntNum(ctx, obj);
1864 case Z3_sort_kind.Z3_REAL_SORT: return new RatNum(ctx, obj);
1865 case Z3_sort_kind.Z3_BV_SORT: return new BitVecNum(ctx, obj);
1866 case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPNum(ctx, obj);
1867 case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMNum(ctx, obj);
1868 case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT: return new FiniteDomainNum(ctx, obj);
1869 }
1870 }
1871
1872 switch (sk)
1873 {
1874 case Z3_sort_kind.Z3_BOOL_SORT: return new BoolExpr(ctx, obj);
1875 case Z3_sort_kind.Z3_INT_SORT: return new IntExpr(ctx, obj);
1876 case Z3_sort_kind.Z3_REAL_SORT: return new RealExpr(ctx, obj);
1877 case Z3_sort_kind.Z3_BV_SORT: return new BitVecExpr(ctx, obj);
1878 case Z3_sort_kind.Z3_ARRAY_SORT: return new ArrayExpr(ctx, obj);
1879 case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeExpr(ctx, obj);
1880 case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPExpr(ctx, obj);
1881 case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMExpr(ctx, obj);
1882 case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT: return new FiniteDomainExpr(ctx, obj);
1883 case Z3_sort_kind.Z3_RE_SORT: return new ReExpr(ctx, obj);
1884 case Z3_sort_kind.Z3_SEQ_SORT: return new SeqExpr(ctx, obj);
1885 }
1886
1887 return new Expr(ctx, obj);
1888 }
1889 #endregion
1890 }
1891}
The abstract syntax tree (AST) class.
Definition: AST.cs:31
bool IsVar
Indicates whether the AST is a BoundVariable
Definition: AST.cs:162
bool IsApp
Indicates whether the AST is an application
Definition: AST.cs:154
bool IsExpr
Indicates whether the AST is an Expr
Definition: AST.cs:136
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Expressions are terms.
Definition: Expr.cs:31
uint AtMostBound
Retrieve bound of at-most
Definition: Expr.cs:328
bool IsContains
Check whether expression is a contains.
Definition: Expr.cs:859
bool IsInt
Indicates whether the term is of integer sort.
Definition: Expr.cs:362
bool IsBVXOR3
Indicates whether the term is a bit-vector ternary XOR
Definition: Expr.cs:805
bool IsConst
Indicates whether the term represents a constant.
Definition: Expr.cs:213
bool IsProofTransitivityStar
Indicates whether the term is a proof by condensed transitivity of a relation
Definition: Expr.cs:979
bool IsXor
Indicates whether the term is an exclusive or
Definition: Expr.cs:308
bool IsFPToReal
Indicates whether the term is a floating-point conversion to real term
Definition: Expr.cs:1774
bool IsFPMinusInfinity
Indicates whether the term is a floating-point -oo
Definition: Expr.cs:1608
bool IsBVSLE
Indicates whether the term is a signed bit-vector less-than-or-equal
Definition: Expr.cs:636
bool IsFPRMRoundNearestTiesToAway
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
Definition: Expr.cs:1544
Z3_lbool BoolValue
Indicates whether the expression is the true or false expression or something else (Z3_L_UNDEF).
Definition: Expr.cs:62
bool IsProofTheoryLemma
Indicates whether the term is a proof for theory lemma
Definition: Expr.cs:1365
bool IsFP
Indicates whether the terms is of floating-point sort.
Definition: Expr.cs:1514
bool IsIntNum
Indicates whether the term is an integer numeral.
Definition: Expr.cs:223
bool IsRelationUnion
Indicates whether the term is the union or convex hull of two relations.
Definition: Expr.cs:1411
bool IsBVConcat
Indicates whether the term is a bit-vector concatenation (binary)
Definition: Expr.cs:706
bool IsFiniteDomain
Indicates whether the term is of an array sort.
Definition: Expr.cs:1495
bool IsProofQuantIntro
Indicates whether the term is a quant-intro proof
Definition: Expr.cs:1003
bool IsConcat
Check whether expression is a concatenation.
Definition: Expr.cs:841
bool IsAt
Check whether expression is an at.
Definition: Expr.cs:877
uint Index
The de-Bruijn index of a bound variable.
Definition: Expr.cs:1806
bool IsProofHypothesis
Indicates whether the term is a hypothesis marker.
Definition: Expr.cs:1135
bool IsProofTrue
Indicates whether the term is a Proof for the expression 'true'.
Definition: Expr.cs:905
bool IsBVBitZero
Indicates whether the term is a one-bit bit-vector with value zero
Definition: Expr.cs:556
bool IsRelationNegationFilter
Indicates whether the term is an intersection of a relation with the negation of another.
Definition: Expr.cs:1451
bool IsBVZeroExtension
Indicates whether the term is a bit-vector zero extension
Definition: Expr.cs:716
bool IsProofNNFPos
Indicates whether the term is a proof for a positive NNF step
Definition: Expr.cs:1297
bool IsFPToFpUnsigned
Indicates whether the term is a floating-point conversion from unsigned bit-vector term
Definition: Expr.cs:1759
bool IsFPDiv
Indicates whether the term is a floating-point division term
Definition: Expr.cs:1649
bool IsBVShiftRightLogical
Indicates whether the term is a bit-vector logical shift right
Definition: Expr.cs:751
bool IsPbEq
Indicates whether the term is pbeq
Definition: Expr.cs:343
bool IsFPLe
Indicates whether the term is a floating-point less-than or equal term
Definition: Expr.cs:1704
Expr Substitute(Expr from, Expr to)
Substitute every occurrence of from in the expression with to.
Definition: Expr.cs:139
Expr Substitute(Expr[] from, Expr[] to)
Substitute every occurrence of from[i] in the expression with to[i], for i smaller than num_exprs.
Definition: Expr.cs:121
bool IsFPLt
Indicates whether the term is a floating-point less-than term
Definition: Expr.cs:1694
bool IsBVCarry
Indicates whether the term is a bit-vector carry
Definition: Expr.cs:799
bool IsFPRMExprRTN
Indicates whether the term is the floating-point rounding numeral roundTowardNegative
Definition: Expr.cs:1574
bool IsBVRotateLeft
Indicates whether the term is a bit-vector rotate left
Definition: Expr.cs:761
bool IsTrue
Indicates whether the term is the constant true.
Definition: Expr.cs:268
bool IsFPRMRoundTowardPositive
Indicates whether the term is the floating-point rounding numeral roundTowardPositive
Definition: Expr.cs:1554
bool IsBVAdd
Indicates whether the term is a bit-vector addition (binary)
Definition: Expr.cs:566
bool IsFPRoundToIntegral
Indicates whether the term is a floating-point roundToIntegral term
Definition: Expr.cs:1684
bool IsFPEq
Indicates whether the term is a floating-point equality term
Definition: Expr.cs:1689
bool IsRelationStore
Indicates whether the term is an relation store
Definition: Expr.cs:1390
bool IsBVSGE
Indicates whether the term is a signed bit-vector greater-than-or-equal
Definition: Expr.cs:646
uint NumArgs
The number of arguments of the expression.
Definition: Expr.cs:70
bool IsProofReflexivity
Indicates whether the term is a proof for (R t t), where R is a reflexive relation.
Definition: Expr.cs:935
bool IsReplace
Check whether expression is a replace.
Definition: Expr.cs:871
new Expr Translate(Context ctx)
Translates (copies) the term to the Context ctx .
Definition: Expr.cs:167
bool IsProofModusPonensOEQ
Indicates whether the term is a proof by modus ponens for equi-satisfiability.
Definition: Expr.cs:1346
bool IsFPFMA
Indicates whether the term is a floating-point fused multiply-add term
Definition: Expr.cs:1674
bool IsRatNum
Indicates whether the term is a real numeral.
Definition: Expr.cs:233
bool IsNumeral
Indicates whether the term is a numeral
Definition: Expr.cs:184
bool IsBVComp
Indicates whether the term is a bit-vector comparison
Definition: Expr.cs:741
bool IsFPRMExprRTZ
Indicates whether the term is the floating-point rounding numeral roundTowardZero
Definition: Expr.cs:1584
bool IsProofIFFFalse
Indicates whether the term is a proof by iff-false
Definition: Expr.cs:1178
bool IsFPRMRoundTowardZero
Indicates whether the term is the floating-point rounding numeral roundTowardZero
Definition: Expr.cs:1559
bool IsBVULT
Indicates whether the term is an unsigned bit-vector less-than
Definition: Expr.cs:651
bool IsFPisPositive
Indicates whether the term is a floating-point isPositive predicate term
Definition: Expr.cs:1744
bool IsRelationSelect
Indicates whether the term is a relational select
Definition: Expr.cs:1475
bool IsProofElimUnusedVars
Indicates whether the term is a proof for elimination of unused variables.
Definition: Expr.cs:1107
bool IsFPToUBV
Indicates whether the term is a floating-point conversion to unsigned bit-vector term
Definition: Expr.cs:1764
bool IsFalse
Indicates whether the term is the constant false.
Definition: Expr.cs:273
bool IsPbLe
Indicates whether the term is pble
Definition: Expr.cs:348
bool IsEq
Indicates whether the term is an equality predicate.
Definition: Expr.cs:278
bool IsProofLemma
Indicates whether the term is a proof by lemma
Definition: Expr.cs:1148
bool IsBVReduceOR
Indicates whether the term is a bit-vector reduce OR
Definition: Expr.cs:731
bool IsArrayMap
Indicates whether the term is an array map.
Definition: Expr.cs:497
bool IsProofDefIntro
Indicates whether the term is a proof for introduction of a name
Definition: Expr.cs:1250
bool IsBVNumeral
Indicates whether the term is a bit-vector numeral
Definition: Expr.cs:546
bool IsBVAND
Indicates whether the term is a bit-wise AND
Definition: Expr.cs:671
bool IsPbGe
Indicates whether the term is pbge
Definition: Expr.cs:353
bool IsFPAbs
Indicates whether the term is a floating-point term absolute value term
Definition: Expr.cs:1659
bool IsRelationFilter
Indicates whether the term is a relation filter
Definition: Expr.cs:1435
bool IsProofApplyDef
Indicates whether the term is a proof for application of a definition
Definition: Expr.cs:1260
bool IsProofIFFTrue
Indicates whether the term is a proof by iff-true
Definition: Expr.cs:1169
bool IsIntToReal
Indicates whether the term is a coercion of integer to real (unary)
Definition: Expr.cs:442
bool IsFPisNormal
Indicates whether the term is a floating-point isNormal term
Definition: Expr.cs:1729
bool IsString
Check whether expression is a string constant.
Definition: Expr.cs:829
bool IsProofQuantInst
Indicates whether the term is a proof for quantifier instantiation
Definition: Expr.cs:1129
bool IsFPMax
Indicates whether the term is a floating-point maximum term
Definition: Expr.cs:1669
Expr SubstituteVars(Expr[] to)
Substitute the free variables in the expression with the expressions in to
Definition: Expr.cs:153
bool IsIff
Indicates whether the term is an if-and-only-if (Boolean equivalence, binary)
Definition: Expr.cs:303
bool IsBVNOR
Indicates whether the term is a bit-wise NOR
Definition: Expr.cs:696
bool IsFPNaN
Indicates whether the term is a floating-point NaN
Definition: Expr.cs:1613
bool IsBVXOR
Indicates whether the term is a bit-wise XOR
Definition: Expr.cs:686
bool IsBVUGE
Indicates whether the term is an unsigned bit-vector greater-than-or-equal
Definition: Expr.cs:641
bool IsExtract
Check whether expression is an extract.
Definition: Expr.cs:865
bool IsFPisZero
Indicates whether the term is a floating-point isZero predicate term
Definition: Expr.cs:1724
bool IsProofDER
Indicates whether the term is a proof for destructive equality resolution
Definition: Expr.cs:1121
bool IsIndex
Check whether expression is a sequence index.
Definition: Expr.cs:889
bool IsRelationClone
Indicates whether the term is a relational clone (copy)
Definition: Expr.cs:1487
bool IsFiniteDomainLT
Indicates whether the term is a less than predicate over a finite domain.
Definition: Expr.cs:1506
bool IsIntToBV
Indicates whether the term is a coercion from integer to bit-vector
Definition: Expr.cs:785
bool IsLE
Indicates whether the term is a less-than-or-equal
Definition: Expr.cs:382
Expr[] Args
The arguments of the expression.
Definition: Expr.cs:78
bool IsBVUMinus
Indicates whether the term is a bit-vector unary minus
Definition: Expr.cs:561
bool IsBVShiftRightArithmetic
Indicates whether the term is a bit-vector arithmetic shift left
Definition: Expr.cs:756
Expr(Context ctx, IntPtr obj)
Constructor for Expr
Definition: Expr.cs:1821
bool IsOr
Indicates whether the term is an n-ary disjunction
Definition: Expr.cs:298
bool IsFPToSBV
Indicates whether the term is a floating-point conversion to signed bit-vector term
Definition: Expr.cs:1769
bool IsBVXNOR
Indicates whether the term is a bit-wise XNOR
Definition: Expr.cs:701
bool IsFPRMExprRNA
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToAway
Definition: Expr.cs:1569
bool IsFPGe
Indicates whether the term is a floating-point greater-than or equal term
Definition: Expr.cs:1709
bool IsFPMin
Indicates whether the term is a floating-point minimum term
Definition: Expr.cs:1664
bool IsSetUnion
Indicates whether the term is set union
Definition: Expr.cs:511
bool IsProofModusPonens
Indicates whether the term is proof via modus ponens
Definition: Expr.cs:926
bool IsBVReduceAND
Indicates whether the term is a bit-vector reduce AND
Definition: Expr.cs:736
bool IsAsArray
Indicates whether the term is an as-array term.
Definition: Expr.cs:504
bool IsBVToInt
Indicates whether the term is a coercion from bit-vector to integer
Definition: Expr.cs:792
bool IsIDiv
Indicates whether the term is integer division (binary)
Definition: Expr.cs:427
bool IsFPMul
Indicates whether the term is a floating-point multiplication term
Definition: Expr.cs:1644
bool IsModulus
Indicates whether the term is modulus (binary)
Definition: Expr.cs:437
bool IsFPNumeral
Indicates whether the term is a floating-point numeral
Definition: Expr.cs:1529
bool IsProofRewriteStar
Indicates whether the term is a proof by rewriting
Definition: Expr.cs:1073
bool IsSetIntersect
Indicates whether the term is set intersection
Definition: Expr.cs:516
string String
Retrieve string corresponding to string constant.
Definition: Expr.cs:835
bool IsBVRotateRight
Indicates whether the term is a bit-vector rotate right
Definition: Expr.cs:766
bool IsFPRMRoundNearestTiesToEven
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
Definition: Expr.cs:1539
bool IsFPisSubnormal
Indicates whether the term is a floating-point isSubnormal predicate term
Definition: Expr.cs:1734
bool IsAtLeast
Indicates whether the term is at-least
Definition: Expr.cs:333
bool IsITE
Indicates whether the term is a ternary if-then-else term
Definition: Expr.cs:288
bool IsAdd
Indicates whether the term is addition (binary)
Definition: Expr.cs:402
bool IsLT
Indicates whether the term is a less-than
Definition: Expr.cs:392
bool IsFPRMNumeral
Indicates whether the term is a floating-point rounding mode numeral
Definition: Expr.cs:1534
bool IsStore
Indicates whether the term is an array store.
Definition: Expr.cs:474
bool IsBVNAND
Indicates whether the term is a bit-wise NAND
Definition: Expr.cs:691
bool IsBVShiftLeft
Indicates whether the term is a bit-vector shift left
Definition: Expr.cs:746
bool IsMul
Indicates whether the term is multiplication (binary)
Definition: Expr.cs:417
bool IsFPisNegative
Indicates whether the term is a floating-point isNegative predicate term
Definition: Expr.cs:1739
bool IsFPRem
Indicates whether the term is a floating-point remainder term
Definition: Expr.cs:1654
bool IsAtMost
Indicates whether the term is at-most
Definition: Expr.cs:323
bool IsFPToIEEEBV
Indicates whether the term is a floating-point conversion to IEEE-754 bit-vector term
Definition: Expr.cs:1780
bool IsProofPullQuant
Indicates whether the term is a proof for pulling quantifiers out.
Definition: Expr.cs:1081
bool IsFPGt
Indicates whether the term is a floating-point greater-than term
Definition: Expr.cs:1699
bool IsDistinct
Indicates whether the term is an n-ary distinct predicate (every argument is mutually distinct).
Definition: Expr.cs:283
bool IsRelation
Indicates whether the term is of relation sort.
Definition: Expr.cs:1373
bool IsFPisInf
Indicates whether the term is a floating-point isInf predicate term
Definition: Expr.cs:1719
bool IsProofNNFNeg
Indicates whether the term is a proof for a negative NNF step
Definition: Expr.cs:1322
bool IsDiv
Indicates whether the term is division (binary)
Definition: Expr.cs:422
bool IsBVRotateRightExtended
Indicates whether the term is a bit-vector rotate right (extended)
Definition: Expr.cs:778
Expr Arg(uint i)
The i'th argument of the expression.
Definition: Expr.cs:93
bool IsGT
Indicates whether the term is a greater-than
Definition: Expr.cs:397
bool IsBVSDiv
Indicates whether the term is a bit-vector signed division (binary)
Definition: Expr.cs:581
bool IsReal
Indicates whether the term is of sort real.
Definition: Expr.cs:370
override string ToString()
Returns a string representation of the expression.
Definition: Expr.cs:175
bool IsLabel
Indicates whether the term is a label (used by the Boogie Verification condition generator).
Definition: Expr.cs:814
bool IsRemainder
Indicates whether the term is remainder (binary)
Definition: Expr.cs:432
bool IsProofTransitivity
Indicates whether the term is a proof by transitivity of a relation
Definition: Expr.cs:958
bool IsRelationalJoin
Indicates whether the term is a relational join
Definition: Expr.cs:1405
bool IsOEQ
Indicates whether the term is a binary equivalence modulo namings.
Definition: Expr.cs:900
bool IsDefaultArray
Indicates whether the term is a default array.
Definition: Expr.cs:491
bool IsConstantArray
Indicates whether the term is a constant array.
Definition: Expr.cs:485
bool IsGE
Indicates whether the term is a greater-than-or-equal
Definition: Expr.cs:387
bool IsRelationRename
Indicates whether the term is the renaming of a column in a relation
Definition: Expr.cs:1460
bool IsIsEmptyRelation
Indicates whether the term is a test for the emptiness of a relation
Definition: Expr.cs:1400
bool IsProofAsserted
Indicates whether the term is a proof for a fact asserted by the user.
Definition: Expr.cs:910
bool IsFPRM
Indicates whether the terms is of floating-point rounding mode sort.
Definition: Expr.cs:1522
bool IsProofOrElimination
Indicates whether the term is a proof by elimination of not-or
Definition: Expr.cs:1041
bool IsRealToInt
Indicates whether the term is a coercion of real to integer (unary)
Definition: Expr.cs:447
bool IsAnd
Indicates whether the term is an n-ary conjunction
Definition: Expr.cs:293
bool IsFPPlusInfinity
Indicates whether the term is a floating-point +oo
Definition: Expr.cs:1603
bool IsBV
Indicates whether the terms is of bit-vector sort.
Definition: Expr.cs:539
bool IsProofMonotonicity
Indicates whether the term is a monotonicity proof object.
Definition: Expr.cs:993
bool IsFPisNaN
Indicates whether the term is a floating-point isNaN predicate term
Definition: Expr.cs:1714
bool IsBool
Indicates whether the term has Boolean sort.
Definition: Expr.cs:255
bool IsFPRMRoundTowardNegative
Indicates whether the term is the floating-point rounding numeral roundTowardNegative
Definition: Expr.cs:1549
void Update(Expr[] args)
Update the arguments of the expression using the arguments args The number of new arguments should c...
Definition: Expr.cs:102
bool IsProofDefAxiom
Indicates whether the term is a proof for Tseitin-like axioms
Definition: Expr.cs:1227
bool IsWellSorted
Indicates whether the term is well-sorted.
Definition: Expr.cs:193
bool IsImplies
Indicates whether the term is an implication
Definition: Expr.cs:318
bool IsSuffix
Check whether expression is a suffix.
Definition: Expr.cs:853
bool IsBVSRem
Indicates whether the term is a bit-vector signed remainder (binary)
Definition: Expr.cs:591
bool IsFPToFp
Indicates whether the term is a floating-point conversion term
Definition: Expr.cs:1754
bool IsLabelLit
Indicates whether the term is a label literal (used by the Boogie Verification condition generator).
Definition: Expr.cs:820
uint AtLeastBound
Retrieve bound of at-least
Definition: Expr.cs:338
bool IsProofUnitResolution
Indicates whether the term is a proof by unit resolution
Definition: Expr.cs:1160
bool IsProofGoal
Indicates whether the term is a proof for a fact (tagged as goal) asserted by the user.
Definition: Expr.cs:915
bool IsFPSqrt
Indicates whether the term is a floating-point square root term
Definition: Expr.cs:1679
bool IsSelect
Indicates whether the term is an array select.
Definition: Expr.cs:479
bool IsNot
Indicates whether the term is a negation
Definition: Expr.cs:313
bool IsFPFP
Indicates whether the term is a floating-point constructor term
Definition: Expr.cs:1749
FuncDecl FuncDecl
The function declaration of the function that is applied in this expression.
Definition: Expr.cs:50
bool IsFPMinusZero
Indicates whether the term is a floating-point -zero
Definition: Expr.cs:1623
bool IsRelationProject
Indicates whether the term is a projection of columns (provided as numbers in the parameters).
Definition: Expr.cs:1423
bool IsUMinus
Indicates whether the term is a unary minus
Definition: Expr.cs:412
bool IsRelationWiden
Indicates whether the term is the widening of two relations
Definition: Expr.cs:1417
bool IsBVRepeat
Indicates whether the term is a bit-vector repetition
Definition: Expr.cs:726
bool IsSub
Indicates whether the term is subtraction (binary)
Definition: Expr.cs:407
bool IsRelationComplement
Indicates whether the term is the complement of a relation
Definition: Expr.cs:1465
bool IsFPPlusZero
Definition: Expr.cs:1618
bool IsBVOR
Indicates whether the term is a bit-wise OR
Definition: Expr.cs:676
bool IsBVSub
Indicates whether the term is a bit-vector subtraction (binary)
Definition: Expr.cs:571
bool IsBVRotateLeftExtended
Indicates whether the term is a bit-vector rotate left (extended)
Definition: Expr.cs:772
bool IsProofSymmetry
Indicates whether the term is proof by symmetricity of a relation
Definition: Expr.cs:946
bool IsProofSkolemize
Indicates whether the term is a proof for a Skolemization step
Definition: Expr.cs:1335
bool IsBVMul
Indicates whether the term is a bit-vector multiplication (binary)
Definition: Expr.cs:576
bool IsLength
Check whether expression is a sequence length.
Definition: Expr.cs:883
bool IsFPSub
Indicates whether the term is a floating-point subtraction term
Definition: Expr.cs:1634
bool IsBVUDiv
Indicates whether the term is a bit-vector unsigned division (binary)
Definition: Expr.cs:586
bool IsProofCommutativity
Indicates whether the term is a proof by commutativity
Definition: Expr.cs:1191
bool IsAlgebraicNumber
Indicates whether the term is an algebraic number
Definition: Expr.cs:243
bool IsProofRewrite
Indicates whether the term is a proof by rewriting
Definition: Expr.cs:1060
bool IsFPRMExprRNE
Indicates whether the term is the floating-point rounding numeral roundNearestTiesToEven
Definition: Expr.cs:1564
bool IsArithmeticNumeral
Indicates whether the term is an arithmetic numeral.
Definition: Expr.cs:377
bool IsProofAndElimination
Indicates whether the term is a proof by elimination of AND
Definition: Expr.cs:1031
bool IsEmptyRelation
Indicates whether the term is an empty relation
Definition: Expr.cs:1395
bool IsProofPushQuant
Indicates whether the term is a proof for pushing quantifiers in.
Definition: Expr.cs:1095
bool IsProofDistributivity
Indicates whether the term is a distributivity proof object.
Definition: Expr.cs:1021
bool IsBVURem
Indicates whether the term is a bit-vector unsigned remainder (binary)
Definition: Expr.cs:596
bool IsBVULE
Indicates whether the term is an unsigned bit-vector less-than-or-equal
Definition: Expr.cs:631
bool IsBVSLT
Indicates whether the term is a signed bit-vector less-than
Definition: Expr.cs:656
bool IsBVExtract
Indicates whether the term is a bit-vector extraction
Definition: Expr.cs:721
bool IsBVSignExtension
Indicates whether the term is a bit-vector sign extension
Definition: Expr.cs:711
bool IsRealIsInt
Indicates whether the term is a check that tests whether a real is integral (unary)
Definition: Expr.cs:452
bool IsSetDifference
Indicates whether the term is set difference
Definition: Expr.cs:521
Expr Simplify(Params p=null)
Returns a simplified version of the expression.
Definition: Expr.cs:37
bool IsBVUGT
Indicates whether the term is an unsigned bit-vector greater-than
Definition: Expr.cs:661
bool IsPrefix
Check whether expression is a prefix.
Definition: Expr.cs:847
bool IsFPRMExprRTP
Indicates whether the term is the floating-point rounding numeral roundTowardPositive
Definition: Expr.cs:1579
bool IsFPAdd
Indicates whether the term is a floating-point addition term
Definition: Expr.cs:1628
bool IsFPRMExpr
Indicates whether the term is a floating-point rounding mode numeral
Definition: Expr.cs:1589
bool IsBVSMod
Indicates whether the term is a bit-vector signed modulus
Definition: Expr.cs:601
bool IsBVBitOne
Indicates whether the term is a one-bit bit-vector with value one
Definition: Expr.cs:551
bool IsFPNeg
Indicates whether the term is a floating-point negation term
Definition: Expr.cs:1639
bool IsArray
Indicates whether the term is of an array sort.
Definition: Expr.cs:460
bool IsBVNOT
Indicates whether the term is a bit-wise NOT
Definition: Expr.cs:681
bool IsBVSGT
Indicates whether the term is a signed bit-vector greater-than
Definition: Expr.cs:666
bool IsSetSubset
Indicates whether the term is set subset
Definition: Expr.cs:531
bool IsSetComplement
Indicates whether the term is set complement
Definition: Expr.cs:526
bool IsProofIFFOEQ
Indicates whether the term is a proof iff-oeq
Definition: Expr.cs:1269
int Int
The int value of the parameter.
Definition: FuncDecl.cs:219
Function declarations.
Definition: FuncDecl.cs:31
Parameter[] Parameters
The parameters of the function declaration
Definition: FuncDecl.cs:164
uint DomainSize
The size of the domain of the function declaration Arity
Definition: FuncDecl.cs:101
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:137
A Params objects represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
The Sort class implements type information for ASTs.
Definition: Sort.cs:29
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:32
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types.
Definition: z3_api.h:180
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:1000
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:150
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102