Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
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;
21 using System.Diagnostics.Contracts;
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(args);
102  if (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(from);
124  Context.CheckContextMatch(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(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 
214 
215 
216  public bool IsConst
217  {
218  get { return IsExpr && NumArgs == 0 && FuncDecl.DomainSize == 0; }
219  }
220  #endregion
221 
222  #region Integer Numerals
223 
224 
225 
226  public bool IsIntNum
227  {
228  get { return IsNumeral && IsInt; }
229  }
230  #endregion
231 
232  #region Real Numerals
233 
234 
235 
236  public bool IsRatNum
237  {
238  get { return IsNumeral && IsReal; }
239  }
240  #endregion
241 
242  #region Algebraic Numbers
243 
244 
245 
246  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 
256 
257 
258  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 FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TRUE; } }
273 
277  public bool IsFalse { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FALSE; } }
278 
282  public bool IsEq { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EQ; } }
283 
287  public bool IsDistinct { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DISTINCT; } }
288 
292  public bool IsITE { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ITE; } }
293 
297  public bool IsAnd { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AND; } }
298 
302  public bool IsOr { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OR; } }
303 
307  public bool IsIff { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IFF; } }
308 
312  public bool IsXor { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR; } }
313 
317  public bool IsNot { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_NOT; } }
318 
322  public bool IsImplies { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IMPLIES; } }
323  #endregion
324 
325  #region Arithmetic Terms
326 
327 
328 
329  public bool IsInt
330  {
331  get
332  {
333  return (Native.Z3_is_numeral_ast(Context.nCtx, NativeObject) != 0 &&
334  Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_INT_SORT);
335  }
336  }
337 
341  public bool IsReal
342  {
343  get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_REAL_SORT; }
344  }
345 
349  public bool IsArithmeticNumeral { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ANUM; } }
350 
354  public bool IsLE { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LE; } }
355 
359  public bool IsGE { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GE; } }
360 
364  public bool IsLT { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LT; } }
365 
369  public bool IsGT { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GT; } }
370 
374  public bool IsAdd { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ADD; } }
375 
379  public bool IsSub { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SUB; } }
380 
384  public bool IsUMinus { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UMINUS; } }
385 
389  public bool IsMul { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MUL; } }
390 
394  public bool IsDiv { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DIV; } }
395 
399  public bool IsIDiv { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IDIV; } }
400 
404  public bool IsRemainder { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REM; } }
405 
409  public bool IsModulus { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MOD; } }
410 
414  public bool IsIntToReal { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_REAL; } }
415 
419  public bool IsRealToInt { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_INT; } }
420 
424  public bool IsRealIsInt { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IS_INT; } }
425  #endregion
426 
427  #region Array Terms
428 
429 
430 
431  public bool IsArray
432  {
433  get
434  {
435  return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
436  (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == Z3_sort_kind.Z3_ARRAY_SORT);
437  }
438  }
439 
445  public bool IsStore { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_STORE; } }
446 
450  public bool IsSelect { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SELECT; } }
451 
456  public bool IsConstantArray { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONST_ARRAY; } }
457 
462  public bool IsDefaultArray { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT; } }
463 
468  public bool IsArrayMap { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_MAP; } }
469 
475  public bool IsAsArray { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AS_ARRAY; } }
476  #endregion
477 
478  #region Set Terms
479 
480 
481 
482  public bool IsSetUnion { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_UNION; } }
483 
487  public bool IsSetIntersect { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_INTERSECT; } }
488 
492  public bool IsSetDifference { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_DIFFERENCE; } }
493 
497  public bool IsSetComplement { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_COMPLEMENT; } }
498 
502  public bool IsSetSubset { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_SUBSET; } }
503  #endregion
504 
505  #region Bit-vector terms
506 
507 
508 
509  public bool IsBV
510  {
511  get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_BV_SORT; }
512  }
513 
517  public bool IsBVNumeral { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNUM; } }
518 
522  public bool IsBVBitOne { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT1; } }
523 
527  public bool IsBVBitZero { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT0; } }
528 
532  public bool IsBVUMinus { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNEG; } }
533 
537  public bool IsBVAdd { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BADD; } }
538 
542  public bool IsBVSub { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSUB; } }
543 
547  public bool IsBVMul { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BMUL; } }
548 
552  public bool IsBVSDiv { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV; } }
553 
557  public bool IsBVUDiv { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV; } }
558 
562  public bool IsBVSRem { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM; } }
563 
567  public bool IsBVURem { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM; } }
568 
572  public bool IsBVSMod { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD; } }
573 
577  internal bool IsBVSDiv0 { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV0; } }
578 
582  internal bool IsBVUDiv0 { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV0; } }
583 
587  internal bool IsBVSRem0 { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM0; } }
588 
592  internal bool IsBVURem0 { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM0; } }
593 
597  internal bool IsBVSMod0 { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD0; } }
598 
602  public bool IsBVULE { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULEQ; } }
603 
607  public bool IsBVSLE { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLEQ; } }
608 
612  public bool IsBVUGE { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGEQ; } }
613 
617  public bool IsBVSGE { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGEQ; } }
618 
622  public bool IsBVULT { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULT; } }
623 
627  public bool IsBVSLT { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLT; } }
628 
632  public bool IsBVUGT { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGT; } }
633 
637  public bool IsBVSGT { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGT; } }
638 
642  public bool IsBVAND { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BAND; } }
643 
647  public bool IsBVOR { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BOR; } }
648 
652  public bool IsBVNOT { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOT; } }
653 
657  public bool IsBVXOR { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXOR; } }
658 
662  public bool IsBVNAND { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNAND; } }
663 
667  public bool IsBVNOR { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOR; } }
668 
672  public bool IsBVXNOR { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXNOR; } }
673 
677  public bool IsBVConcat { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONCAT; } }
678 
682  public bool IsBVSignExtension { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SIGN_EXT; } }
683 
687  public bool IsBVZeroExtension { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ZERO_EXT; } }
688 
692  public bool IsBVExtract { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXTRACT; } }
693 
697  public bool IsBVRepeat { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REPEAT; } }
698 
702  public bool IsBVReduceOR { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDOR; } }
703 
707  public bool IsBVReduceAND { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDAND; } }
708 
712  public bool IsBVComp { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BCOMP; } }
713 
717  public bool IsBVShiftLeft { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSHL; } }
718 
722  public bool IsBVShiftRightLogical { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BLSHR; } }
723 
727  public bool IsBVShiftRightArithmetic { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BASHR; } }
728 
732  public bool IsBVRotateLeft { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_LEFT; } }
733 
737  public bool IsBVRotateRight { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_RIGHT; } }
738 
743  public bool IsBVRotateLeftExtended { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT; } }
744 
749  public bool IsBVRotateRightExtended { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT; } }
750 
756  public bool IsIntToBV { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_INT2BV; } }
757 
763  public bool IsBVToInt { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BV2INT; } }
764 
770  public bool IsBVCarry { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CARRY; } }
771 
776  public bool IsBVXOR3 { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR3; } }
777 
778  #endregion
779 
780  #region Labels
781 
782 
783 
784 
785  public bool IsLabel { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL; } }
786 
791  public bool IsLabelLit { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } }
792  #endregion
793 
794  #region Proof Terms
795 
796 
797 
798 
799 
800  public bool IsOEQ { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OEQ; } }
801 
805  public bool IsProofTrue { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRUE; } }
806 
810  public bool IsProofAsserted { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ASSERTED; } }
811 
815  public bool IsProofGoal { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_GOAL; } }
816 
826  public bool IsProofModusPonens { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS; } }
827 
835  public bool IsProofReflexivity { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY; } }
836 
846  public bool IsProofSymmetry { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SYMMETRY; } }
847 
858  public bool IsProofTransitivity { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY; } }
859 
879  public bool IsProofTransitivityStar { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR; } }
880 
881 
893  public bool IsProofMonotonicity { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MONOTONICITY; } }
894 
903  public bool IsProofQuantIntro { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO; } }
904 
921  public bool IsProofDistributivity { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY; } }
922 
931  public bool IsProofAndElimination { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_AND_ELIM; } }
932 
941  public bool IsProofOrElimination { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM; } }
942 
960  public bool IsProofRewrite { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE; } }
961 
976  public bool IsProofRewriteStar { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR; } }
977 
984  public bool IsProofPullQuant { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT; } }
985 
994  public bool IsProofPullQuantStar { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR; } }
995 
1007  public bool IsProofPushQuant { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT; } }
1008 
1019  public bool IsProofElimUnusedVars { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS; } }
1020 
1033  public bool IsProofDER { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DER; } }
1034 
1041  public bool IsProofQuantInst { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INST; } }
1042 
1047  public bool IsProofHypothesis { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS; } }
1048 
1060  public bool IsProofLemma { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_LEMMA; } }
1061 
1072  public bool IsProofUnitResolution { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION; } }
1073 
1081  public bool IsProofIFFTrue { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_TRUE; } }
1082 
1090  public bool IsProofIFFFalse { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_FALSE; } }
1091 
1103  public bool IsProofCommutativity { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY; } }
1104 
1139  public bool IsProofDefAxiom { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM; } }
1140 
1162  public bool IsProofDefIntro { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_INTRO; } }
1163 
1172  public bool IsProofApplyDef { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_APPLY_DEF; } }
1173 
1181  public bool IsProofIFFOEQ { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_OEQ; } }
1182 
1209  public bool IsProofNNFPos { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_POS; } }
1210 
1234  public bool IsProofNNFNeg { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_NEG; } }
1235 
1246  public bool IsProofNNFStar { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_STAR; } }
1247 
1256  public bool IsProofCNFStar { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_CNF_STAR; } }
1257 
1269  public bool IsProofSkolemize { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE; } }
1270 
1280  public bool IsProofModusPonensOEQ { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ; } }
1281 
1299  public bool IsProofTheoryLemma { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TH_LEMMA; } }
1300  #endregion
1301 
1302  #region Relational Terms
1303 
1304 
1305 
1306  public bool IsRelation
1307  {
1308  get
1309  {
1310  return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
1311  (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == Z3_sort_kind.Z3_RELATION_SORT);
1312  }
1313  }
1314 
1323  public bool IsRelationStore { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_STORE; } }
1324 
1328  public bool IsEmptyRelation { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_EMPTY; } }
1329 
1333  public bool IsIsEmptyRelation { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_IS_EMPTY; } }
1334 
1338  public bool IsRelationalJoin { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_JOIN; } }
1339 
1344  public bool IsRelationUnion { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_UNION; } }
1345 
1350  public bool IsRelationWiden { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_WIDEN; } }
1351 
1356  public bool IsRelationProject { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_PROJECT; } }
1357 
1368  public bool IsRelationFilter { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_FILTER; } }
1369 
1384  public bool IsRelationNegationFilter { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER; } }
1385 
1393  public bool IsRelationRename { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_RENAME; } }
1394 
1398  public bool IsRelationComplement { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_COMPLEMENT; } }
1399 
1408  public bool IsRelationSelect { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_SELECT; } }
1409 
1420  public bool IsRelationClone { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_CLONE; } }
1421  #endregion
1422 
1423  #region Finite domain terms
1424 
1425 
1426 
1427  public bool IsFiniteDomain
1428  {
1429  get
1430  {
1431  return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
1432  (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == Z3_sort_kind.Z3_FINITE_DOMAIN_SORT);
1433  }
1434  }
1435 
1439  public bool IsFiniteDomainLT { get { return FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FD_LT; } }
1440  #endregion
1441  #endregion
1442 
1443  #region Bound Variables
1444 
1445 
1446 
1447 
1448 
1449 
1450 
1451 
1452 
1453 
1454 
1455 
1456 
1457 
1458 
1459 
1460 
1461 
1462 
1463  public uint Index
1464  {
1465  get
1466  {
1467  if (!IsVar)
1468  throw new Z3Exception("Term is not a bound variable.");
1469 
1470  Contract.EndContractBlock();
1471 
1472  return Native.Z3_get_index_value(Context.nCtx, NativeObject);
1473  }
1474  }
1475  #endregion
1476 
1477  #region Internal
1478 
1479 
1480 
1481  internal protected Expr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
1485  internal protected Expr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
1486 
1487 #if DEBUG
1488  [Pure]
1489  internal override void CheckNativeObject(IntPtr obj)
1490  {
1491  if (Native.Z3_is_app(Context.nCtx, obj) == 0 &&
1492  (Z3_ast_kind)Native.Z3_get_ast_kind(Context.nCtx, obj) != Z3_ast_kind.Z3_VAR_AST &&
1493  (Z3_ast_kind)Native.Z3_get_ast_kind(Context.nCtx, obj) != Z3_ast_kind.Z3_QUANTIFIER_AST)
1494  throw new Z3Exception("Underlying object is not a term");
1495  base.CheckNativeObject(obj);
1496  }
1497 #endif
1498 
1499  [Pure]
1500  internal static Expr Create(Context ctx, FuncDecl f, params Expr[] arguments)
1501  {
1502  Contract.Requires(ctx != null);
1503  Contract.Requires(f != null);
1504  Contract.Ensures(Contract.Result<Expr>() != null);
1505 
1506  IntPtr obj = Native.Z3_mk_app(ctx.nCtx, f.NativeObject,
1507  AST.ArrayLength(arguments),
1508  AST.ArrayToNative(arguments));
1509  return Create(ctx, obj);
1510  }
1511 
1512  [Pure]
1513  new internal static Expr Create(Context ctx, IntPtr obj)
1514  {
1515  Contract.Requires(ctx != null);
1516  Contract.Ensures(Contract.Result<Expr>() != null);
1517 
1518  Z3_ast_kind k = (Z3_ast_kind)Native.Z3_get_ast_kind(ctx.nCtx, obj);
1519  if (k == Z3_ast_kind.Z3_QUANTIFIER_AST)
1520  return new Quantifier(ctx, obj);
1521  IntPtr s = Native.Z3_get_sort(ctx.nCtx, obj);
1522  Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, s);
1523 
1524  if (Native.Z3_is_algebraic_number(ctx.nCtx, obj) != 0) // is this a numeral ast?
1525  return new AlgebraicNum(ctx, obj);
1526 
1527  if (Native.Z3_is_numeral_ast(ctx.nCtx, obj) != 0)
1528  {
1529  switch (sk)
1530  {
1531  case Z3_sort_kind.Z3_INT_SORT: return new IntNum(ctx, obj);
1532  case Z3_sort_kind.Z3_REAL_SORT: return new RatNum(ctx, obj);
1533  case Z3_sort_kind.Z3_BV_SORT: return new BitVecNum(ctx, obj);
1534  }
1535  }
1536 
1537  switch (sk)
1538  {
1539  case Z3_sort_kind.Z3_BOOL_SORT: return new BoolExpr(ctx, obj);
1540  case Z3_sort_kind.Z3_INT_SORT: return new IntExpr(ctx, obj);
1541  case Z3_sort_kind.Z3_REAL_SORT: return new RealExpr(ctx, obj);
1542  case Z3_sort_kind.Z3_BV_SORT: return new BitVecExpr(ctx, obj);
1543  case Z3_sort_kind.Z3_ARRAY_SORT: return new ArrayExpr(ctx, obj);
1544  case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeExpr(ctx, obj);
1545  }
1546 
1547  return new Expr(ctx, obj);
1548  }
1549  #endregion
1550  }
1551 
1555  public class BoolExpr : Expr
1556  {
1557  #region Internal
1558 
1559  internal protected BoolExpr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
1561  internal BoolExpr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
1562  #endregion
1563  }
1564 
1568  public class ArithExpr : Expr
1569  {
1570  #region Internal
1571 
1572  internal protected ArithExpr(Context ctx)
1573  : base(ctx)
1574  {
1575  Contract.Requires(ctx != null);
1576  }
1577  internal ArithExpr(Context ctx, IntPtr obj)
1578  : base(ctx, obj)
1579  {
1580  Contract.Requires(ctx != null);
1581  }
1582  #endregion
1583  }
1584 
1588  public class IntExpr : ArithExpr
1589  {
1590  #region Internal
1591 
1592  internal protected IntExpr(Context ctx)
1593  : base(ctx)
1594  {
1595  Contract.Requires(ctx != null);
1596  }
1597  internal IntExpr(Context ctx, IntPtr obj)
1598  : base(ctx, obj)
1599  {
1600  Contract.Requires(ctx != null);
1601  }
1602  #endregion
1603  }
1604 
1608  public class RealExpr : ArithExpr
1609  {
1610  #region Internal
1611 
1612  internal protected RealExpr(Context ctx)
1613  : base(ctx)
1614  {
1615  Contract.Requires(ctx != null);
1616  }
1617  internal RealExpr(Context ctx, IntPtr obj)
1618  : base(ctx, obj)
1619  {
1620  Contract.Requires(ctx != null);
1621  }
1622  #endregion
1623  }
1624 
1628  public class BitVecExpr : Expr
1629  {
1630 
1634  public uint SortSize
1635  {
1636  get { return ((BitVecSort)Sort).Size; }
1637  }
1638 
1639  #region Internal
1640 
1641  internal protected BitVecExpr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
1642  internal BitVecExpr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
1643  #endregion
1644  }
1645 
1649  public class ArrayExpr : Expr
1650  {
1651  #region Internal
1652 
1653  internal protected ArrayExpr(Context ctx)
1654  : base(ctx)
1655  {
1656  Contract.Requires(ctx != null);
1657  }
1658  internal ArrayExpr(Context ctx, IntPtr obj)
1659  : base(ctx, obj)
1660  {
1661  Contract.Requires(ctx != null);
1662  }
1663  #endregion
1664  }
1665 
1669  public class DatatypeExpr : Expr
1670  {
1671  #region Internal
1672 
1673  internal protected DatatypeExpr(Context ctx)
1674  : base(ctx)
1675  {
1676  Contract.Requires(ctx != null);
1677  }
1678  internal DatatypeExpr(Context ctx, IntPtr obj)
1679  : base(ctx, obj)
1680  {
1681  Contract.Requires(ctx != null);
1682  }
1683  #endregion
1684  }
1685 }
Generated on Thu Nov 22 2012 18:37:18 for Z3 by   doxygen 1.8.2