Z3
Expr.cs
Go to the documentation of this file.
1 /*++
2 Copyright (<c>) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  Expr.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Expressions
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-03-20
15 
16 Notes:
17 
18 --*/
19 
20 using System;
22 
23 namespace Microsoft.Z3
24 {
28  [ContractVerification(true)]
29  public class Expr : AST
30  {
36  public Expr Simplify(Params p = null)
37  {
38  Contract.Ensures(Contract.Result<Expr>() != null);
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 
49  public FuncDecl FuncDecl
50  {
51  get
52  {
53  Contract.Ensures(Contract.Result<FuncDecl>() != null);
54  return new FuncDecl(Context, Native.Z3_get_app_decl(Context.nCtx, NativeObject));
55  }
56  }
57 
62  public Z3_lbool BoolValue
63  {
64  get { return (Z3_lbool)Native.Z3_get_bool_value(Context.nCtx, NativeObject); }
65  }
66 
70  public uint NumArgs
71  {
72  get { return Native.Z3_get_app_num_args(Context.nCtx, NativeObject); }
73  }
74 
78  public Expr[] Args
79  {
80  get
81  {
82  Contract.Ensures(Contract.Result<Expr[]>() != null);
83 
84  uint n = NumArgs;
85  Expr[] res = new Expr[n];
86  for (uint i = 0; i < n; i++)
87  res[i] = Expr.Create(Context, Native.Z3_get_app_arg(Context.nCtx, NativeObject, i));
88  return res;
89  }
90  }
91 
96  public void Update(Expr[] args)
97  {
98  Contract.Requires(args != null);
99  Contract.Requires(Contract.ForAll(args, a => a != null));
100 
101  Context.CheckContextMatch<Expr>(args);
102  if (IsApp && args.Length != NumArgs)
103  throw new Z3Exception("Number of arguments does not match");
104  NativeObject = Native.Z3_update_term(Context.nCtx, NativeObject, (uint)args.Length, Expr.ArrayToNative(args));
105  }
106 
115  public Expr Substitute(Expr[] from, Expr[] to)
116  {
117  Contract.Requires(from != null);
118  Contract.Requires(to != null);
119  Contract.Requires(Contract.ForAll(from, f => f != null));
120  Contract.Requires(Contract.ForAll(to, t => t != null));
121  Contract.Ensures(Contract.Result<Expr>() != null);
122 
123  Context.CheckContextMatch<Expr>(from);
124  Context.CheckContextMatch<Expr>(to);
125  if (from.Length != to.Length)
126  throw new Z3Exception("Argument sizes do not match");
127  return Expr.Create(Context, Native.Z3_substitute(Context.nCtx, NativeObject, (uint)from.Length, Expr.ArrayToNative(from), Expr.ArrayToNative(to)));
128  }
129 
134  public Expr Substitute(Expr from, Expr to)
135  {
136  Contract.Requires(from != null);
137  Contract.Requires(to != null);
138  Contract.Ensures(Contract.Result<Expr>() != null);
139 
140  return Substitute(new Expr[] { from }, new Expr[] { to });
141  }
142 
149  public Expr SubstituteVars(Expr[] to)
150  {
151  Contract.Requires(to != null);
152  Contract.Requires(Contract.ForAll(to, t => t != null));
153  Contract.Ensures(Contract.Result<Expr>() != null);
154 
155  Context.CheckContextMatch<Expr>(to);
156  return Expr.Create(Context, Native.Z3_substitute_vars(Context.nCtx, NativeObject, (uint)to.Length, Expr.ArrayToNative(to)));
157  }
158 
164  new public Expr Translate(Context ctx)
165  {
166  Contract.Requires(ctx != null);
167  Contract.Ensures(Contract.Result<Expr>() != null);
168 
169  if (ReferenceEquals(Context, ctx))
170  return this;
171  else
172  return Expr.Create(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx));
173  }
174 
178  public override string ToString()
179  {
180  return base.ToString();
181  }
182 
186  public bool IsNumeral
187  {
188  get { return Native.Z3_is_numeral_ast(Context.nCtx, NativeObject) != 0; }
189  }
190 
195  public bool IsWellSorted
196  {
197  get { return Native.Z3_is_well_sorted(Context.nCtx, NativeObject) != 0; }
198  }
199 
203  public Sort Sort
204  {
205  get
206  {
207  Contract.Ensures(Contract.Result<Sort>() != null);
208  return Sort.Create(Context, Native.Z3_get_sort(Context.nCtx, NativeObject));
209  }
210  }
211 
212  #region Constants
213  public bool IsConst
217  {
218  get { return IsApp && NumArgs == 0 && FuncDecl.DomainSize == 0; }
219  }
220  #endregion
221 
222  #region Integer Numerals
223  public bool IsIntNum
227  {
228  get { return IsNumeral && IsInt; }
229  }
230  #endregion
231 
232  #region Real Numerals
233  public bool IsRatNum
237  {
238  get { return IsNumeral && IsReal; }
239  }
240  #endregion
241 
242  #region Algebraic Numbers
243  public bool IsAlgebraicNumber
247  {
248  get { return Native.Z3_is_algebraic_number(Context.nCtx, NativeObject) != 0; }
249  }
250  #endregion
251 
252  #region Term Kind Tests
253 
254  #region Boolean Terms
255  public bool IsBool
259  {
260  get
261  {
262  return (IsExpr &&
263  Native.Z3_is_eq_sort(Context.nCtx,
264  Native.Z3_mk_bool_sort(Context.nCtx),
265  Native.Z3_get_sort(Context.nCtx, NativeObject)) != 0);
266  }
267  }
268 
272  public bool IsTrue { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TRUE; } }
273 
277  public bool IsFalse { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FALSE; } }
278 
282  public bool IsEq { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EQ; } }
283 
287  public bool IsDistinct { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DISTINCT; } }
288 
292  public bool IsITE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ITE; } }
293 
297  public bool IsAnd { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AND; } }
298 
302  public bool IsOr { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OR; } }
303 
307  public bool IsIff { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IFF; } }
308 
312  public bool IsXor { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR; } }
313 
317  public bool IsNot { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_NOT; } }
318 
322  public bool IsImplies { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IMPLIES; } }
323 
324  #endregion
325 
326  #region Interpolation
327  public bool IsInterpolant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_INTERP; } }
332  #endregion
333 
334  #region Arithmetic Terms
335  public bool IsInt
339  {
340  get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_INT_SORT; }
341  }
342 
346  public bool IsReal
347  {
348  get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_REAL_SORT; }
349  }
350 
354  public bool IsArithmeticNumeral { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ANUM; } }
355 
359  public bool IsLE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LE; } }
360 
364  public bool IsGE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GE; } }
365 
369  public bool IsLT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LT; } }
370 
374  public bool IsGT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GT; } }
375 
379  public bool IsAdd { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ADD; } }
380 
384  public bool IsSub { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SUB; } }
385 
389  public bool IsUMinus { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UMINUS; } }
390 
394  public bool IsMul { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MUL; } }
395 
399  public bool IsDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DIV; } }
400 
404  public bool IsIDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IDIV; } }
405 
409  public bool IsRemainder { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REM; } }
410 
414  public bool IsModulus { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MOD; } }
415 
419  public bool IsIntToReal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_REAL; } }
420 
424  public bool IsRealToInt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_INT; } }
425 
429  public bool IsRealIsInt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IS_INT; } }
430  #endregion
431 
432  #region Array Terms
433  public bool IsArray
437  {
438  get
439  {
440  return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
441  (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
442  == Z3_sort_kind.Z3_ARRAY_SORT);
443  }
444  }
445 
451  public bool IsStore { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_STORE; } }
452 
456  public bool IsSelect { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SELECT; } }
457 
462  public bool IsConstantArray { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONST_ARRAY; } }
463 
468  public bool IsDefaultArray { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT; } }
469 
474  public bool IsArrayMap { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_MAP; } }
475 
481  public bool IsAsArray { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AS_ARRAY; } }
482  #endregion
483 
484  #region Set Terms
485  public bool IsSetUnion { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_UNION; } }
489 
493  public bool IsSetIntersect { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_INTERSECT; } }
494 
498  public bool IsSetDifference { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_DIFFERENCE; } }
499 
503  public bool IsSetComplement { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_COMPLEMENT; } }
504 
508  public bool IsSetSubset { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_SUBSET; } }
509  #endregion
510 
511  #region Bit-vector terms
512  public bool IsBV
516  {
517  get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_BV_SORT; }
518  }
519 
523  public bool IsBVNumeral { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNUM; } }
524 
528  public bool IsBVBitOne { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT1; } }
529 
533  public bool IsBVBitZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT0; } }
534 
538  public bool IsBVUMinus { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNEG; } }
539 
543  public bool IsBVAdd { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BADD; } }
544 
548  public bool IsBVSub { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSUB; } }
549 
553  public bool IsBVMul { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BMUL; } }
554 
558  public bool IsBVSDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV; } }
559 
563  public bool IsBVUDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV; } }
564 
568  public bool IsBVSRem { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM; } }
569 
573  public bool IsBVURem { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM; } }
574 
578  public bool IsBVSMod { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD; } }
579 
583  internal bool IsBVSDiv0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV0; } }
584 
588  internal bool IsBVUDiv0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV0; } }
589 
593  internal bool IsBVSRem0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM0; } }
594 
598  internal bool IsBVURem0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM0; } }
599 
603  internal bool IsBVSMod0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD0; } }
604 
608  public bool IsBVULE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULEQ; } }
609 
613  public bool IsBVSLE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLEQ; } }
614 
618  public bool IsBVUGE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGEQ; } }
619 
623  public bool IsBVSGE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGEQ; } }
624 
628  public bool IsBVULT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULT; } }
629 
633  public bool IsBVSLT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLT; } }
634 
638  public bool IsBVUGT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGT; } }
639 
643  public bool IsBVSGT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGT; } }
644 
648  public bool IsBVAND { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BAND; } }
649 
653  public bool IsBVOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BOR; } }
654 
658  public bool IsBVNOT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOT; } }
659 
663  public bool IsBVXOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXOR; } }
664 
668  public bool IsBVNAND { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNAND; } }
669 
673  public bool IsBVNOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOR; } }
674 
678  public bool IsBVXNOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXNOR; } }
679 
683  public bool IsBVConcat { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONCAT; } }
684 
688  public bool IsBVSignExtension { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SIGN_EXT; } }
689 
693  public bool IsBVZeroExtension { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ZERO_EXT; } }
694 
698  public bool IsBVExtract { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXTRACT; } }
699 
703  public bool IsBVRepeat { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REPEAT; } }
704 
708  public bool IsBVReduceOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDOR; } }
709 
713  public bool IsBVReduceAND { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDAND; } }
714 
718  public bool IsBVComp { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BCOMP; } }
719 
723  public bool IsBVShiftLeft { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSHL; } }
724 
728  public bool IsBVShiftRightLogical { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BLSHR; } }
729 
733  public bool IsBVShiftRightArithmetic { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BASHR; } }
734 
738  public bool IsBVRotateLeft { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_LEFT; } }
739 
743  public bool IsBVRotateRight { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_RIGHT; } }
744 
749  public bool IsBVRotateLeftExtended { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT; } }
750 
755  public bool IsBVRotateRightExtended { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT; } }
756 
762  public bool IsIntToBV { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_INT2BV; } }
763 
769  public bool IsBVToInt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BV2INT; } }
770 
776  public bool IsBVCarry { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CARRY; } }
777 
782  public bool IsBVXOR3 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR3; } }
783 
784  #endregion
785 
786  #region Labels
787  public bool IsLabel { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL; } }
792 
797  public bool IsLabelLit { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } }
798  #endregion
799 
800  #region Proof Terms
801  public bool IsOEQ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OEQ; } }
807 
811  public bool IsProofTrue { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRUE; } }
812 
816  public bool IsProofAsserted { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ASSERTED; } }
817 
821  public bool IsProofGoal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_GOAL; } }
822 
832  public bool IsProofModusPonens { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS; } }
833 
841  public bool IsProofReflexivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY; } }
842 
852  public bool IsProofSymmetry { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SYMMETRY; } }
853 
864  public bool IsProofTransitivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY; } }
865 
885  public bool IsProofTransitivityStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR; } }
886 
887 
899  public bool IsProofMonotonicity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MONOTONICITY; } }
900 
909  public bool IsProofQuantIntro { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO; } }
910 
927  public bool IsProofDistributivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY; } }
928 
937  public bool IsProofAndElimination { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_AND_ELIM; } }
938 
947  public bool IsProofOrElimination { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM; } }
948 
966  public bool IsProofRewrite { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE; } }
967 
982  public bool IsProofRewriteStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR; } }
983 
990  public bool IsProofPullQuant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT; } }
991 
1000  public bool IsProofPullQuantStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR; } }
1001 
1013  public bool IsProofPushQuant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT; } }
1014 
1025  public bool IsProofElimUnusedVars { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS; } }
1026 
1039  public bool IsProofDER { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DER; } }
1040 
1047  public bool IsProofQuantInst { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INST; } }
1048 
1053  public bool IsProofHypothesis { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS; } }
1054 
1066  public bool IsProofLemma { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_LEMMA; } }
1067 
1078  public bool IsProofUnitResolution { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION; } }
1079 
1087  public bool IsProofIFFTrue { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_TRUE; } }
1088 
1096  public bool IsProofIFFFalse { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_FALSE; } }
1097 
1109  public bool IsProofCommutativity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY; } }
1110 
1145  public bool IsProofDefAxiom { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM; } }
1146 
1168  public bool IsProofDefIntro { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_INTRO; } }
1169 
1178  public bool IsProofApplyDef { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_APPLY_DEF; } }
1179 
1187  public bool IsProofIFFOEQ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_OEQ; } }
1188 
1215  public bool IsProofNNFPos { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_POS; } }
1216 
1240  public bool IsProofNNFNeg { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_NEG; } }
1241 
1252  public bool IsProofNNFStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_STAR; } }
1253 
1262  public bool IsProofCNFStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_CNF_STAR; } }
1263 
1275  public bool IsProofSkolemize { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE; } }
1276 
1286  public bool IsProofModusPonensOEQ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ; } }
1287 
1305  public bool IsProofTheoryLemma { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TH_LEMMA; } }
1306  #endregion
1307 
1308  #region Relational Terms
1309  public bool IsRelation
1313  {
1314  get
1315  {
1316  return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
1317  Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
1318  == (uint)Z3_sort_kind.Z3_RELATION_SORT);
1319  }
1320  }
1321 
1330  public bool IsRelationStore { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_STORE; } }
1331 
1335  public bool IsEmptyRelation { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_EMPTY; } }
1336 
1340  public bool IsIsEmptyRelation { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_IS_EMPTY; } }
1341 
1345  public bool IsRelationalJoin { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_JOIN; } }
1346 
1351  public bool IsRelationUnion { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_UNION; } }
1352 
1357  public bool IsRelationWiden { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_WIDEN; } }
1358 
1363  public bool IsRelationProject { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_PROJECT; } }
1364 
1375  public bool IsRelationFilter { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_FILTER; } }
1376 
1391  public bool IsRelationNegationFilter { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER; } }
1392 
1400  public bool IsRelationRename { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_RENAME; } }
1401 
1405  public bool IsRelationComplement { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_COMPLEMENT; } }
1406 
1415  public bool IsRelationSelect { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_SELECT; } }
1416 
1427  public bool IsRelationClone { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_CLONE; } }
1428  #endregion
1429 
1430  #region Finite domain terms
1431  public bool IsFiniteDomain
1435  {
1436  get
1437  {
1438  return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
1439  Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_FINITE_DOMAIN_SORT);
1440  }
1441  }
1442 
1446  public bool IsFiniteDomainLT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FD_LT; } }
1447  #endregion
1448 
1449  #region Floating-point terms
1450  public bool IsFP
1454  {
1455  get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_FLOATING_POINT_SORT; }
1456  }
1457 
1461  public bool IsFPRM
1462  {
1463  get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_ROUNDING_MODE_SORT; }
1464  }
1465 
1469  public bool IsFPNumeral { get { return IsFP && IsNumeral; } }
1470 
1474  public bool IsFPRMNumeral { get { return IsFPRM && IsNumeral; } }
1475 
1479  public bool IsFPRMRoundNearestTiesToEven{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } }
1480 
1484  public bool IsFPRMRoundNearestTiesToAway{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }
1485 
1489  public bool IsFPRMRoundTowardNegative{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } }
1490 
1494  public bool IsFPRMRoundTowardPositive{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } }
1495 
1499  public bool IsFPRMRoundTowardZero{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } }
1500 
1504  public bool IsFPRMExprRNE{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN; } }
1505 
1509  public bool IsFPRMExprRNA { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY; } }
1510 
1514  public bool IsFPRMExprRTN { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE; } }
1515 
1519  public bool IsFPRMExprRTP { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE; } }
1520 
1524  public bool IsFPRMExprRTZ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO; } }
1525 
1529  public bool IsFPRMExpr {
1530  get {
1531  return IsApp &&
1532  (FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY||
1533  FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN ||
1534  FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_POSITIVE ||
1535  FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_NEGATIVE ||
1536  FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO);
1537  }
1538  }
1539 
1543  public bool IsFPPlusInfinity{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_PLUS_INF; } }
1544 
1548  public bool IsFPMinusInfinity{ get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MINUS_INF; } }
1549 
1553  public bool IsFPNaN { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_NAN; } }
1554 
1558  public bool IsFPPlusZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_PLUS_ZERO; } }
1559 
1563  public bool IsFPMinusZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MINUS_ZERO; } }
1564 
1568  public bool IsFPAdd { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_ADD; } }
1569 
1570 
1574  public bool IsFPSub { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_SUB; } }
1575 
1579  public bool IsFPNeg { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_NEG; } }
1580 
1584  public bool IsFPMul { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MUL; } }
1585 
1589  public bool IsFPDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_DIV; } }
1590 
1594  public bool IsFPRem { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_REM; } }
1595 
1599  public bool IsFPAbs { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_ABS; } }
1600 
1604  public bool IsFPMin { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MIN; } }
1605 
1609  public bool IsFPMax { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_MAX; } }
1610 
1614  public bool IsFPFMA { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_FMA; } }
1615 
1619  public bool IsFPSqrt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_SQRT; } }
1620 
1624  public bool IsFPRoundToIntegral { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_ROUND_TO_INTEGRAL; } }
1625 
1629  public bool IsFPEq { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_EQ; } }
1630 
1634  public bool IsFPLt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_LT; } }
1635 
1639  public bool IsFPGt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_GT; } }
1640 
1644  public bool IsFPLe { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_LE; } }
1645 
1649  public bool IsFPGe { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_GE; } }
1650 
1654  public bool IsFPisNaN { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_NAN; } }
1655 
1659  public bool IsFPisInf { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_INF; } }
1660 
1664  public bool IsFPisZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_ZERO; } }
1665 
1669  public bool IsFPisNormal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_NORMAL; } }
1670 
1674  public bool IsFPisSubnormal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_SUBNORMAL; } }
1675 
1679  public bool IsFPisNegative { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_NEGATIVE; } }
1680 
1684  public bool IsFPisPositive { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_IS_POSITIVE; } }
1685 
1689  public bool IsFPFP { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_FP; } }
1690 
1694  public bool IsFPToFp { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_FP; } }
1695 
1699  public bool IsFPToFpUnsigned { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_FP_UNSIGNED; } }
1700 
1704  public bool IsFPToUBV { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_UBV; } }
1705 
1709  public bool IsFPToSBV { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_SBV; } }
1710 
1714  public bool IsFPToReal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_REAL; } }
1715 
1716 
1720  public bool IsFPToIEEEBV { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FPA_TO_IEEE_BV; } }
1721 
1722  #endregion
1723  #endregion
1724 
1725  #region Bound Variables
1726  public uint Index
1746  {
1747  get
1748  {
1749  if (!IsVar)
1750  throw new Z3Exception("Term is not a bound variable.");
1751 
1752  Contract.EndContractBlock();
1753 
1754  return Native.Z3_get_index_value(Context.nCtx, NativeObject);
1755  }
1756  }
1757  #endregion
1758 
1759  #region Internal
1760  internal protected Expr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
1764 
1765 #if DEBUG
1766  [Pure]
1767  internal override void CheckNativeObject(IntPtr obj)
1768  {
1769  if (Native.Z3_is_app(Context.nCtx, obj) == 0 &&
1770  Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_VAR_AST &&
1771  Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_QUANTIFIER_AST)
1772  throw new Z3Exception("Underlying object is not a term");
1773  base.CheckNativeObject(obj);
1774  }
1775 #endif
1776 
1777  [Pure]
1778  internal static Expr Create(Context ctx, FuncDecl f, params Expr[] arguments)
1779  {
1780  Contract.Requires(ctx != null);
1781  Contract.Requires(f != null);
1782  Contract.Ensures(Contract.Result<Expr>() != null);
1783 
1784  IntPtr obj = Native.Z3_mk_app(ctx.nCtx, f.NativeObject,
1785  AST.ArrayLength(arguments),
1786  AST.ArrayToNative(arguments));
1787  return Create(ctx, obj);
1788  }
1789 
1790  [Pure]
1791  new internal static Expr Create(Context ctx, IntPtr obj)
1792  {
1793  Contract.Requires(ctx != null);
1794  Contract.Ensures(Contract.Result<Expr>() != null);
1795 
1796  Z3_ast_kind k = (Z3_ast_kind)Native.Z3_get_ast_kind(ctx.nCtx, obj);
1797  if (k == Z3_ast_kind.Z3_QUANTIFIER_AST)
1798  return new Quantifier(ctx, obj);
1799  IntPtr s = Native.Z3_get_sort(ctx.nCtx, obj);
1800  Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, s);
1801 
1802  if (Native.Z3_is_algebraic_number(ctx.nCtx, obj) != 0) // is this a numeral ast?
1803  return new AlgebraicNum(ctx, obj);
1804 
1805  if (Native.Z3_is_numeral_ast(ctx.nCtx, obj) != 0)
1806  {
1807  switch (sk)
1808  {
1809  case Z3_sort_kind.Z3_INT_SORT: return new IntNum(ctx, obj);
1810  case Z3_sort_kind.Z3_REAL_SORT: return new RatNum(ctx, obj);
1811  case Z3_sort_kind.Z3_BV_SORT: return new BitVecNum(ctx, obj);
1812  case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPNum(ctx, obj);
1813  case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMNum(ctx, obj);
1814  case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT: return new FiniteDomainNum(ctx, obj);
1815  }
1816  }
1817 
1818  switch (sk)
1819  {
1820  case Z3_sort_kind.Z3_BOOL_SORT: return new BoolExpr(ctx, obj);
1821  case Z3_sort_kind.Z3_INT_SORT: return new IntExpr(ctx, obj);
1822  case Z3_sort_kind.Z3_REAL_SORT: return new RealExpr(ctx, obj);
1823  case Z3_sort_kind.Z3_BV_SORT: return new BitVecExpr(ctx, obj);
1824  case Z3_sort_kind.Z3_ARRAY_SORT: return new ArrayExpr(ctx, obj);
1825  case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeExpr(ctx, obj);
1826  case Z3_sort_kind.Z3_FLOATING_POINT_SORT: return new FPExpr(ctx, obj);
1827  case Z3_sort_kind.Z3_ROUNDING_MODE_SORT: return new FPRMExpr(ctx, obj);
1828  case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT: return new FiniteDomainExpr(ctx, obj);
1829  case Z3_sort_kind.Z3_RE_SORT: return new ReExpr(ctx, obj);
1830  case Z3_sort_kind.Z3_SEQ_SORT: return new SeqExpr(ctx, obj);
1831  }
1832 
1833  return new Expr(ctx, obj);
1834  }
1835  #endregion
1836  }
1837 }
Z3_sort_kind
The different kinds of Z3 types (See #Z3_get_sort_kind).
Definition: z3_api.h:153
Finite-domain numerals
FloatiungPoint Numerals
Definition: FPNum.cs:28
def IsInt(a)
Definition: z3py.py:2942
Expr Simplify(Params p=null)
Returns a simplified version of the expression.
Definition: Expr.cs:36
uint DomainSize
The size of the domain of the function declaration Arity
Definition: FuncDecl.cs:100
Bit-vector numerals
Definition: BitVecNum.cs:32
Boolean expressions
Definition: BoolExpr.cs:31
Floating-point rounding mode numerals
Definition: FPRMNum.cs:31
Expr SubstituteVars(Expr[] to)
Substitute the free variables in the expression with the expressions in to
Definition: Expr.cs:149
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:115
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
Expressions are terms.
Definition: Expr.cs:29
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:183
Integer Numerals
Definition: IntNum.cs:32
Bit-vector expressions
Definition: BitVecExpr.cs:31
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:105
Finite-domain expressions
new Expr Translate(Context ctx)
Translates (copies) the term to the Context ctx .
Definition: Expr.cs:164
override string ToString()
Returns a string representation of the expression.
Definition: Expr.cs:178
FloatingPoint Expressions
Definition: FPExpr.cs:31
Array expressions
Definition: ArrayExpr.cs:31
Datatype expressions
Definition: DatatypeExpr.cs:31
A Params objects represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
Quantifier expressions.
Definition: Quantifier.cs:29
void Update(Expr[] args)
Update the arguments of the expression using the arguments args The number of new arguments should c...
Definition: Expr.cs:96
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
The Sort class implements type information for ASTs.
Definition: Sort.cs:29
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:30
Rational Numerals
Definition: RatNum.cs:32
The abstract syntax tree (AST) class.
Definition: AST.cs:31
FloatingPoint RoundingMode Expressions
Definition: FPRMExpr.cs:31
Sequence expressions
Definition: SeqExpr.cs:31
Regular expression expressions
Definition: ReExpr.cs:31
Algebraic numbers
Definition: AlgebraicNum.cs:32
Expr Substitute(Expr from, Expr to)
Substitute every occurrence of from in the expression with to.
Definition: Expr.cs:134
Int expressions
Definition: IntExpr.cs:31
Function declarations.
Definition: FuncDecl.cs:29
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:955
Real expressions
Definition: RealExpr.cs:31