Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules 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 (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(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  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 &&
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
341  {
342  return (Native.Z3_is_numeral_ast(Context.nCtx, NativeObject) != 0 &&
343  Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_INT_SORT);
344  }
345  }
346 
350  public bool IsReal
351  {
352  get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_REAL_SORT; }
353  }
354 
358  public bool IsArithmeticNumeral { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ANUM; } }
359 
363  public bool IsLE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LE; } }
364 
368  public bool IsGE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GE; } }
369 
373  public bool IsLT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LT; } }
374 
378  public bool IsGT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_GT; } }
379 
383  public bool IsAdd { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ADD; } }
384 
388  public bool IsSub { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SUB; } }
389 
393  public bool IsUMinus { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UMINUS; } }
394 
398  public bool IsMul { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MUL; } }
399 
403  public bool IsDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_DIV; } }
404 
408  public bool IsIDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IDIV; } }
409 
413  public bool IsRemainder { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REM; } }
414 
418  public bool IsModulus { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_MOD; } }
419 
423  public bool IsIntToReal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_REAL; } }
424 
428  public bool IsRealToInt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_TO_INT; } }
429 
433  public bool IsRealIsInt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_IS_INT; } }
434  #endregion
435 
436  #region Array Terms
437  public bool IsArray
441  {
442  get
443  {
444  return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
446  == Z3_sort_kind.Z3_ARRAY_SORT);
447  }
448  }
449 
455  public bool IsStore { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_STORE; } }
456 
460  public bool IsSelect { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SELECT; } }
461 
466  public bool IsConstantArray { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONST_ARRAY; } }
467 
472  public bool IsDefaultArray { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_DEFAULT; } }
473 
478  public bool IsArrayMap { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ARRAY_MAP; } }
479 
485  public bool IsAsArray { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_AS_ARRAY; } }
486  #endregion
487 
488  #region Set Terms
489  public bool IsSetUnion { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_UNION; } }
493 
497  public bool IsSetIntersect { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_INTERSECT; } }
498 
502  public bool IsSetDifference { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_DIFFERENCE; } }
503 
507  public bool IsSetComplement { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_COMPLEMENT; } }
508 
512  public bool IsSetSubset { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SET_SUBSET; } }
513  #endregion
514 
515  #region Bit-vector terms
516  public bool IsBV
520  {
521  get { return Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_BV_SORT; }
522  }
523 
527  public bool IsBVNumeral { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNUM; } }
528 
532  public bool IsBVBitOne { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT1; } }
533 
537  public bool IsBVBitZero { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BIT0; } }
538 
542  public bool IsBVUMinus { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNEG; } }
543 
547  public bool IsBVAdd { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BADD; } }
548 
552  public bool IsBVSub { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSUB; } }
553 
557  public bool IsBVMul { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BMUL; } }
558 
562  public bool IsBVSDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV; } }
563 
567  public bool IsBVUDiv { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV; } }
568 
572  public bool IsBVSRem { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM; } }
573 
577  public bool IsBVURem { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM; } }
578 
582  public bool IsBVSMod { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD; } }
583 
587  internal bool IsBVSDiv0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSDIV0; } }
588 
592  internal bool IsBVUDiv0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUDIV0; } }
593 
597  internal bool IsBVSRem0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSREM0; } }
598 
602  internal bool IsBVURem0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BUREM0; } }
603 
607  internal bool IsBVSMod0 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSMOD0; } }
608 
612  public bool IsBVULE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULEQ; } }
613 
617  public bool IsBVSLE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLEQ; } }
618 
622  public bool IsBVUGE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGEQ; } }
623 
627  public bool IsBVSGE { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGEQ; } }
628 
632  public bool IsBVULT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ULT; } }
633 
637  public bool IsBVSLT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SLT; } }
638 
642  public bool IsBVUGT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_UGT; } }
643 
647  public bool IsBVSGT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SGT; } }
648 
652  public bool IsBVAND { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BAND; } }
653 
657  public bool IsBVOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BOR; } }
658 
662  public bool IsBVNOT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOT; } }
663 
667  public bool IsBVXOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXOR; } }
668 
672  public bool IsBVNAND { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNAND; } }
673 
677  public bool IsBVNOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BNOR; } }
678 
682  public bool IsBVXNOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BXNOR; } }
683 
687  public bool IsBVConcat { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CONCAT; } }
688 
692  public bool IsBVSignExtension { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SIGN_EXT; } }
693 
697  public bool IsBVZeroExtension { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ZERO_EXT; } }
698 
702  public bool IsBVExtract { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXTRACT; } }
703 
707  public bool IsBVRepeat { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_REPEAT; } }
708 
712  public bool IsBVReduceOR { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDOR; } }
713 
717  public bool IsBVReduceAND { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BREDAND; } }
718 
722  public bool IsBVComp { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BCOMP; } }
723 
727  public bool IsBVShiftLeft { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BSHL; } }
728 
732  public bool IsBVShiftRightLogical { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BLSHR; } }
733 
737  public bool IsBVShiftRightArithmetic { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BASHR; } }
738 
742  public bool IsBVRotateLeft { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_LEFT; } }
743 
747  public bool IsBVRotateRight { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_ROTATE_RIGHT; } }
748 
753  public bool IsBVRotateLeftExtended { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_LEFT; } }
754 
759  public bool IsBVRotateRightExtended { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_EXT_ROTATE_RIGHT; } }
760 
766  public bool IsIntToBV { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_INT2BV; } }
767 
773  public bool IsBVToInt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_BV2INT; } }
774 
780  public bool IsBVCarry { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_CARRY; } }
781 
786  public bool IsBVXOR3 { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_XOR3; } }
787 
788  #endregion
789 
790  #region Labels
791  public bool IsLabel { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL; } }
796 
801  public bool IsLabelLit { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } }
802  #endregion
803 
804  #region Proof Terms
805  public bool IsOEQ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_OEQ; } }
811 
815  public bool IsProofTrue { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRUE; } }
816 
820  public bool IsProofAsserted { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ASSERTED; } }
821 
825  public bool IsProofGoal { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_GOAL; } }
826 
836  public bool IsProofModusPonens { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS; } }
837 
845  public bool IsProofReflexivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REFLEXIVITY; } }
846 
856  public bool IsProofSymmetry { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SYMMETRY; } }
857 
868  public bool IsProofTransitivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY; } }
869 
889  public bool IsProofTransitivityStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TRANSITIVITY_STAR; } }
890 
891 
903  public bool IsProofMonotonicity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MONOTONICITY; } }
904 
913  public bool IsProofQuantIntro { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INTRO; } }
914 
931  public bool IsProofDistributivity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DISTRIBUTIVITY; } }
932 
941  public bool IsProofAndElimination { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_AND_ELIM; } }
942 
951  public bool IsProofOrElimination { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NOT_OR_ELIM; } }
952 
970  public bool IsProofRewrite { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE; } }
971 
986  public bool IsProofRewriteStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR; } }
987 
994  public bool IsProofPullQuant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT; } }
995 
1004  public bool IsProofPullQuantStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR; } }
1005 
1017  public bool IsProofPushQuant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PUSH_QUANT; } }
1018 
1029  public bool IsProofElimUnusedVars { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_ELIM_UNUSED_VARS; } }
1030 
1043  public bool IsProofDER { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DER; } }
1044 
1051  public bool IsProofQuantInst { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_QUANT_INST; } }
1052 
1057  public bool IsProofHypothesis { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_HYPOTHESIS; } }
1058 
1070  public bool IsProofLemma { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_LEMMA; } }
1071 
1082  public bool IsProofUnitResolution { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_UNIT_RESOLUTION; } }
1083 
1091  public bool IsProofIFFTrue { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_TRUE; } }
1092 
1100  public bool IsProofIFFFalse { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_FALSE; } }
1101 
1113  public bool IsProofCommutativity { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_COMMUTATIVITY; } }
1114 
1149  public bool IsProofDefAxiom { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_AXIOM; } }
1150 
1172  public bool IsProofDefIntro { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_DEF_INTRO; } }
1173 
1182  public bool IsProofApplyDef { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_APPLY_DEF; } }
1183 
1191  public bool IsProofIFFOEQ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_IFF_OEQ; } }
1192 
1219  public bool IsProofNNFPos { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_POS; } }
1220 
1244  public bool IsProofNNFNeg { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_NEG; } }
1245 
1256  public bool IsProofNNFStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_STAR; } }
1257 
1266  public bool IsProofCNFStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_CNF_STAR; } }
1267 
1279  public bool IsProofSkolemize { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_SKOLEMIZE; } }
1280 
1290  public bool IsProofModusPonensOEQ { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_MODUS_PONENS_OEQ; } }
1291 
1309  public bool IsProofTheoryLemma { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_TH_LEMMA; } }
1310  #endregion
1311 
1312  #region Relational Terms
1313  public bool IsRelation
1317  {
1318  get
1319  {
1320  return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
1321  Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject))
1322  == (uint)Z3_sort_kind.Z3_RELATION_SORT);
1323  }
1324  }
1325 
1334  public bool IsRelationStore { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_STORE; } }
1335 
1339  public bool IsEmptyRelation { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_EMPTY; } }
1340 
1344  public bool IsIsEmptyRelation { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_IS_EMPTY; } }
1345 
1349  public bool IsRelationalJoin { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_JOIN; } }
1350 
1355  public bool IsRelationUnion { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_UNION; } }
1356 
1361  public bool IsRelationWiden { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_WIDEN; } }
1362 
1367  public bool IsRelationProject { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_PROJECT; } }
1368 
1379  public bool IsRelationFilter { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_FILTER; } }
1380 
1395  public bool IsRelationNegationFilter { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_NEGATION_FILTER; } }
1396 
1404  public bool IsRelationRename { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_RENAME; } }
1405 
1409  public bool IsRelationComplement { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_COMPLEMENT; } }
1410 
1419  public bool IsRelationSelect { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_SELECT; } }
1420 
1431  public bool IsRelationClone { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_RA_CLONE; } }
1432  #endregion
1433 
1434  #region Finite domain terms
1435  public bool IsFiniteDomain
1439  {
1440  get
1441  {
1442  return (Native.Z3_is_app(Context.nCtx, NativeObject) != 0 &&
1443  Native.Z3_get_sort_kind(Context.nCtx, Native.Z3_get_sort(Context.nCtx, NativeObject)) == (uint)Z3_sort_kind.Z3_FINITE_DOMAIN_SORT);
1444  }
1445  }
1446 
1450  public bool IsFiniteDomainLT { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_FD_LT; } }
1451  #endregion
1452  #endregion
1453 
1454  #region Bound Variables
1455  public uint Index
1475  {
1476  get
1477  {
1478  if (!IsVar)
1479  throw new Z3Exception("Term is not a bound variable.");
1480 
1481  Contract.EndContractBlock();
1482 
1483  return Native.Z3_get_index_value(Context.nCtx, NativeObject);
1484  }
1485  }
1486  #endregion
1487 
1488  #region Internal
1489  internal protected Expr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
1496  internal protected Expr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
1497 
1498 #if DEBUG
1499  [Pure]
1500  internal override void CheckNativeObject(IntPtr obj)
1501  {
1502  if (Native.Z3_is_app(Context.nCtx, obj) == 0 &&
1503  Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_VAR_AST &&
1504  Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_QUANTIFIER_AST)
1505  throw new Z3Exception("Underlying object is not a term");
1506  base.CheckNativeObject(obj);
1507  }
1508 #endif
1509 
1510  [Pure]
1511  internal static Expr Create(Context ctx, FuncDecl f, params Expr[] arguments)
1512  {
1513  Contract.Requires(ctx != null);
1514  Contract.Requires(f != null);
1515  Contract.Ensures(Contract.Result<Expr>() != null);
1516 
1517  IntPtr obj = Native.Z3_mk_app(ctx.nCtx, f.NativeObject,
1518  AST.ArrayLength(arguments),
1519  AST.ArrayToNative(arguments));
1520  return Create(ctx, obj);
1521  }
1522 
1523  [Pure]
1524  new internal static Expr Create(Context ctx, IntPtr obj)
1525  {
1526  Contract.Requires(ctx != null);
1527  Contract.Ensures(Contract.Result<Expr>() != null);
1528 
1529  Z3_ast_kind k = (Z3_ast_kind)Native.Z3_get_ast_kind(ctx.nCtx, obj);
1530  if (k == Z3_ast_kind.Z3_QUANTIFIER_AST)
1531  return new Quantifier(ctx, obj);
1532  IntPtr s = Native.Z3_get_sort(ctx.nCtx, obj);
1533  Z3_sort_kind sk = (Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, s);
1534 
1535  if (Native.Z3_is_algebraic_number(ctx.nCtx, obj) != 0) // is this a numeral ast?
1536  return new AlgebraicNum(ctx, obj);
1537 
1538  if (Native.Z3_is_numeral_ast(ctx.nCtx, obj) != 0)
1539  {
1540  switch (sk)
1541  {
1542  case Z3_sort_kind.Z3_INT_SORT: return new IntNum(ctx, obj);
1543  case Z3_sort_kind.Z3_REAL_SORT: return new RatNum(ctx, obj);
1544  case Z3_sort_kind.Z3_BV_SORT: return new BitVecNum(ctx, obj);
1545  }
1546  }
1547 
1548  switch (sk)
1549  {
1550  case Z3_sort_kind.Z3_BOOL_SORT: return new BoolExpr(ctx, obj);
1551  case Z3_sort_kind.Z3_INT_SORT: return new IntExpr(ctx, obj);
1552  case Z3_sort_kind.Z3_REAL_SORT: return new RealExpr(ctx, obj);
1553  case Z3_sort_kind.Z3_BV_SORT: return new BitVecExpr(ctx, obj);
1554  case Z3_sort_kind.Z3_ARRAY_SORT: return new ArrayExpr(ctx, obj);
1555  case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeExpr(ctx, obj);
1556  }
1557 
1558  return new Expr(ctx, obj);
1559  }
1560  #endregion
1561  }
1562 }
Z3_sort_kind
The different kinds of Z3 types (See Z3_get_sort_kind).
Definition: z3_api.h:186
static Z3_ast Z3_update_term(Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3)
Definition: Native.cs:3574
Expr Simplify(Params p=null)
Returns a simplified version of the expression.
Definition: Expr.cs:36
static uint Z3_get_app_num_args(Z3_context a0, Z3_app a1)
Definition: Native.cs:3222
uint DomainSize
The size of the domain of the function declaration Arity
Definition: FuncDecl.cs:100
static uint Z3_get_sort_kind(Z3_context a0, Z3_sort a1)
Definition: Native.cs:2950
static uint Z3_get_bool_value(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3278
Z3_sort_kind
Z3_sort_kind
Definition: Enumerations.cs:34
static Z3_ast Z3_substitute(Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3, [In] Z3_ast[] a4)
Definition: Native.cs:3582
static Z3_ast Z3_substitute_vars(Z3_context a0, Z3_ast a1, uint a2, [In] Z3_ast[] a3)
Definition: Native.cs:3590
static Z3_ast Z3_translate(Z3_context a0, Z3_ast a1, Z3_context a2)
Definition: Native.cs:3598
Expr SubstituteVars(Expr[] to)
Substitute the free variables in the expression with the expressions in to
Definition: Expr.cs:149
Z3_decl_kind
Z3_decl_kind
Definition: Enumerations.cs:59
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_ast_kind
Z3_ast_kind
Definition: Enumerations.cs:48
Z3_decl_kind DeclKind
The kind of the function declaration.
Definition: FuncDecl.cs:138
Expressions are terms.
Definition: Expr.cs:29
static int Z3_is_well_sorted(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3270
Z3_ast_kind
The different kinds of Z3 AST (abstract syntax trees). That is, terms, formulas and types...
Definition: z3_api.h:212
static uint Z3_get_index_value(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3454
def IsInt
Definition: z3py.py:2851
static Z3_sort Z3_get_sort(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3262
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
static Z3_ast Z3_get_app_arg(Z3_context a0, Z3_app a1, uint a2)
Definition: Native.cs:3230
static int Z3_is_eq_sort(Z3_context a0, Z3_sort a1, Z3_sort a2)
Definition: Native.cs:2942
static Z3_ast Z3_simplify_ex(Z3_context a0, Z3_ast a1, Z3_params a2)
Definition: Native.cs:3550
A ParameterSet represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
static int Z3_is_algebraic_number(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3310
static uint Z3_get_ast_kind(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3286
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:31
Z3_lbool
Z3_lbool
Definition: Enumerations.cs:10
The Sort class implements type information for ASTs.
Definition: Sort.cs:29
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:27
static Z3_ast Z3_simplify(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3542
The abstract syntax tree (AST) class.
Definition: AST.cs:31
Expr(Context ctx, IntPtr obj)
Constructor for Expr
Definition: Expr.cs:1496
static int Z3_is_app(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3294
Expr Substitute(Expr from, Expr to)
Substitute every occurrence of from in the expression with to.
Definition: Expr.cs:134
static Z3_func_decl Z3_get_app_decl(Z3_context a0, Z3_app a1)
Definition: Native.cs:3214
Function declarations.
Definition: FuncDecl.cs:29
Z3_decl_kind
The different kinds of interpreted function kinds.
Definition: z3_api.h:880
static Z3_sort Z3_mk_bool_sort(Z3_context a0)
Definition: Native.cs:1882
static int Z3_is_numeral_ast(Z3_context a0, Z3_ast a1)
Definition: Native.cs:3302