Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Sort.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  Sort.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Sorts
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-03-15
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 Sort : AST
30  {
38  public static bool operator ==(Sort a, Sort b)
39  {
40  return Object.ReferenceEquals(a, b) ||
41  (!Object.ReferenceEquals(a, null) &&
42  !Object.ReferenceEquals(b, null) &&
43  a.Context == b.Context &&
44  Native.Z3_is_eq_sort(a.Context.nCtx, a.NativeObject, b.NativeObject) != 0);
45  }
46 
54  public static bool operator !=(Sort a, Sort b)
55  {
56  return !(a == b);
57  }
58 
64  public override bool Equals(object o)
65  {
66  Sort casted = o as Sort;
67  if (casted == null) return false;
68  return this == casted;
69  }
70 
75  public override int GetHashCode()
76  {
77  return base.GetHashCode();
78  }
79 
83  new public uint Id
84  {
85  get { return Native.Z3_get_sort_id(Context.nCtx, NativeObject); }
86  }
87 
91  public Z3_sort_kind SortKind
92  {
93  get { return (Z3_sort_kind)Native.Z3_get_sort_kind(Context.nCtx, NativeObject); }
94  }
95 
99  public Symbol Name
100  {
101  get {
102  Contract.Ensures(Contract.Result<Symbol>() != null);
103  return Symbol.Create(Context, Native.Z3_get_sort_name(Context.nCtx, NativeObject)); }
104  }
105 
109  public override string ToString()
110  {
111  return Native.Z3_sort_to_string(Context.nCtx, NativeObject);
112  }
113 
114  #region Internal
115 
116 
117 
118  internal protected Sort(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
119  internal Sort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
120 
121  #if DEBUG
122  internal override void CheckNativeObject(IntPtr obj)
123  {
124  if (Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_SORT_AST)
125  throw new Z3Exception("Underlying object is not a sort");
126  base.CheckNativeObject(obj);
127  }
128  #endif
129 
130  [ContractVerification(true)]
131  new internal static Sort Create(Context ctx, IntPtr obj)
132  {
133  Contract.Requires(ctx != null);
134  Contract.Ensures(Contract.Result<Sort>() != null);
135 
136  switch ((Z3_sort_kind)Native.Z3_get_sort_kind(ctx.nCtx, obj))
137  {
138  case Z3_sort_kind.Z3_ARRAY_SORT: return new ArraySort(ctx, obj);
139  case Z3_sort_kind.Z3_BOOL_SORT: return new BoolSort(ctx, obj);
140  case Z3_sort_kind.Z3_BV_SORT: return new BitVecSort(ctx, obj);
141  case Z3_sort_kind.Z3_DATATYPE_SORT: return new DatatypeSort(ctx, obj);
142  case Z3_sort_kind.Z3_INT_SORT: return new IntSort(ctx, obj);
143  case Z3_sort_kind.Z3_REAL_SORT: return new RealSort(ctx, obj);
144  case Z3_sort_kind.Z3_UNINTERPRETED_SORT: return new UninterpretedSort(ctx, obj);
145  case Z3_sort_kind.Z3_FINITE_DOMAIN_SORT: return new FiniteDomainSort(ctx, obj);
146  case Z3_sort_kind.Z3_RELATION_SORT: return new RelationSort(ctx, obj);
147  default:
148  throw new Z3Exception("Unknown sort kind");
149  }
150  }
151  #endregion
152  }
153 
157  public class BoolSort : Sort
158  {
159  #region Internal
160  internal BoolSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
161  internal BoolSort(Context ctx) : base(ctx, Native.Z3_mk_bool_sort(ctx.nCtx)) { Contract.Requires(ctx != null); }
162  #endregion
163  };
164 
168  public class ArithSort : Sort
169  {
170  #region Internal
171  internal ArithSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
172  #endregion
173  };
174 
178  public class IntSort : ArithSort
179  {
180  #region Internal
181  internal IntSort(Context ctx, IntPtr obj)
182  : base(ctx, obj)
183  {
184  Contract.Requires(ctx != null);
185  }
186  internal IntSort(Context ctx)
187  : base(ctx, Native.Z3_mk_int_sort(ctx.nCtx))
188  {
189  Contract.Requires(ctx != null);
190  }
191  #endregion
192  }
193 
197  public class RealSort : ArithSort
198  {
199  #region Internal
200  internal RealSort(Context ctx, IntPtr obj)
201  : base(ctx, obj)
202  {
203  Contract.Requires(ctx != null);
204  }
205  internal RealSort(Context ctx)
206  : base(ctx, Native.Z3_mk_real_sort(ctx.nCtx))
207  {
208  Contract.Requires(ctx != null);
209  }
210  #endregion
211  }
212 
216  public class BitVecSort : Sort
217  {
221  public uint Size
222  {
223  get { return Native.Z3_get_bv_sort_size(Context.nCtx, NativeObject); }
224  }
225 
226  #region Internal
227  internal BitVecSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
228  internal BitVecSort(Context ctx, uint size) : base(ctx, Native.Z3_mk_bv_sort(ctx.nCtx, size)) { Contract.Requires(ctx != null); }
229  #endregion
230  };
231 
235  [ContractVerification(true)]
236  public class ArraySort : Sort
237  {
241  public Sort Domain
242  {
243  get {
244  Contract.Ensures(Contract.Result<Sort>() != null);
245 
246  return Sort.Create(Context, Native.Z3_get_array_sort_domain(Context.nCtx, NativeObject)); }
247  }
248 
252  public Sort Range
253  {
254  get {
255  Contract.Ensures(Contract.Result<Sort>() != null);
256 
257  return Sort.Create(Context, Native.Z3_get_array_sort_range(Context.nCtx, NativeObject)); }
258  }
259 
260  #region Internal
261  internal ArraySort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
262  internal ArraySort(Context ctx, Sort domain, Sort range)
263  : base(ctx, Native.Z3_mk_array_sort(ctx.nCtx, domain.NativeObject, range.NativeObject))
264  {
265  Contract.Requires(ctx != null);
266  Contract.Requires(domain != null);
267  Contract.Requires(range != null);
268  }
269  #endregion
270  };
271 
275  [ContractVerification(true)]
276  public class DatatypeSort : Sort
277  {
281  public uint NumConstructors
282  {
283  get { return Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject); }
284  }
285 
289  public FuncDecl[] Constructors
290  {
291  get
292  {
293  Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
294 
295  uint n = NumConstructors;
296  FuncDecl[] res = new FuncDecl[n];
297  for (uint i = 0; i < n; i++)
298  res[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, i));
299  return res;
300  }
301  }
302 
306  public FuncDecl[] Recognizers
307  {
308  get
309  {
310  Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
311 
312  uint n = NumConstructors;
313  FuncDecl[] res = new FuncDecl[n];
314  for (uint i = 0; i < n; i++)
315  res[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, i));
316  return res;
317  }
318  }
319 
323  public FuncDecl[][] Accessors
324  {
325  get
326  {
327  Contract.Ensures(Contract.Result<FuncDecl[][]>() != null);
328 
329  uint n = NumConstructors;
330  FuncDecl[][] res = new FuncDecl[n][];
331  for (uint i = 0; i < n; i++)
332  {
333  FuncDecl fd = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, i));
334  uint ds = fd.DomainSize;
335  FuncDecl[] tmp = new FuncDecl[ds];
336  for (uint j = 0; j < ds; j++)
337  tmp[j] = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, i, j));
338  res[i] = tmp;
339  }
340  return res;
341  }
342  }
343 
344  #region Internal
345  internal DatatypeSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
346 
347  internal DatatypeSort(Context ctx, Symbol name, Constructor[] constructors)
348  : base(ctx, Native.Z3_mk_datatype(ctx.nCtx, name.NativeObject, (uint)constructors.Length, ArrayToNative(constructors)))
349  {
350  Contract.Requires(ctx != null);
351  Contract.Requires(name != null);
352  Contract.Requires(constructors != null);
353  }
354  #endregion
355  };
356 
360  public class UninterpretedSort : Sort
361  {
362  #region Internal
363  internal UninterpretedSort(Context ctx, IntPtr obj)
364  : base(ctx, obj)
365  {
366  Contract.Requires(ctx != null);
367  }
368  internal UninterpretedSort(Context ctx, Symbol s)
369  : base(ctx, Native.Z3_mk_uninterpreted_sort(ctx.nCtx, s.NativeObject))
370  {
371  Contract.Requires(ctx != null);
372  Contract.Requires(s != null);
373  }
374  #endregion
375  }
376 
380  [ContractVerification(true)]
381  public class TupleSort : Sort
382  {
386  public FuncDecl MkDecl
387  {
388  get {
389  Contract.Ensures(Contract.Result<FuncDecl>() != null);
390 
391  return new FuncDecl(Context, Native.Z3_get_tuple_sort_mk_decl(Context.nCtx, NativeObject)); }
392  }
393 
397  public uint NumFields
398  {
399  get { return Native.Z3_get_tuple_sort_num_fields(Context.nCtx, NativeObject); }
400  }
401 
405  public FuncDecl[] FieldDecls
406  {
407  get
408  {
409  Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
410 
411  uint n = NumFields;
412  FuncDecl[] res = new FuncDecl[n];
413  for (uint i = 0; i < n; i++)
414  res[i] = new FuncDecl(Context, Native.Z3_get_tuple_sort_field_decl(Context.nCtx, NativeObject, i));
415  return res;
416  }
417  }
418 
419  #region Internal
420  internal TupleSort(Context ctx, Symbol name, uint numFields, Symbol[] fieldNames, Sort[] fieldSorts)
421  : base(ctx)
422  {
423  Contract.Requires(ctx != null);
424  Contract.Requires(name != null);
425 
426  IntPtr t = IntPtr.Zero;
427  NativeObject = Native.Z3_mk_tuple_sort(ctx.nCtx, name.NativeObject, numFields,
428  Symbol.ArrayToNative(fieldNames), AST.ArrayToNative(fieldSorts),
429  ref t, new IntPtr[numFields]);
430  }
431  #endregion
432  };
433 
437  [ContractVerification(true)]
438  public class EnumSort : Sort
439  {
443  public FuncDecl[] ConstDecls
444  {
445  get {
446  Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
447 
448  return _constdecls; }
449  }
450 
454  public Expr[] Consts
455  {
456  get {
457  Contract.Ensures(Contract.Result<Expr[]>() != null);
458 
459  return _consts; }
460  }
461 
465  public FuncDecl[] TesterDecls
466  {
467  get {
468  Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
469 
470  return _testerdecls;
471  }
472  }
473 
474  #region Object Invariant
475 
476  [ContractInvariantMethod]
477  private void ObjectInvariant()
478  {
479  Contract.Invariant(this._constdecls != null);
480  Contract.Invariant(this._testerdecls != null);
481  Contract.Invariant(this._consts != null);
482  }
483 
484 
485  #endregion
486 
487  #region Internal
488  readonly private FuncDecl[] _constdecls = null, _testerdecls = null;
489  readonly private Expr[] _consts = null;
490 
491  internal EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
492  : base(ctx)
493  {
494  Contract.Requires(ctx != null);
495  Contract.Requires(name != null);
496  Contract.Requires(enumNames != null);
497 
498  int n = enumNames.Length;
499  IntPtr[] n_constdecls = new IntPtr[n];
500  IntPtr[] n_testers = new IntPtr[n];
501  NativeObject = Native.Z3_mk_enumeration_sort(ctx.nCtx, name.NativeObject, (uint)n,
502  Symbol.ArrayToNative(enumNames), n_constdecls, n_testers);
503  _constdecls = new FuncDecl[n];
504  for (uint i = 0; i < n; i++)
505  _constdecls[i] = new FuncDecl(ctx, n_constdecls[i]);
506  _testerdecls = new FuncDecl[n];
507  for (uint i = 0; i < n; i++)
508  _testerdecls[i] = new FuncDecl(ctx, n_testers[i]);
509  _consts = new Expr[n];
510  for (uint i = 0; i < n; i++)
511  _consts[i] = ctx.MkApp(_constdecls[i]);
512  }
513  #endregion
514  };
515 
519  [ContractVerification(true)]
520  public class ListSort : Sort
521  {
525  public FuncDecl NilDecl { get {
526  Contract.Ensures(Contract.Result<FuncDecl>() != null);
527  return nilDecl; } }
528 
532  public Expr Nil
533  {
534  get
535  {
536  Contract.Ensures(Contract.Result<Expr>() != null);
537  return nilConst;
538  }
539  }
540 
544  public FuncDecl IsNilDecl
545  {
546  get
547  {
548  Contract.Ensures(Contract.Result<FuncDecl>() != null);
549  return isNilDecl;
550  }
551  }
552 
556  public FuncDecl ConsDecl
557  {
558  get
559  {
560  Contract.Ensures(Contract.Result<FuncDecl>() != null);
561  return consDecl;
562  }
563  }
564 
569  public FuncDecl IsConsDecl
570  {
571  get
572  {
573  Contract.Ensures(Contract.Result<FuncDecl>() != null);
574  return isConsDecl;
575  }
576  }
577 
581  public FuncDecl HeadDecl
582  {
583  get
584  {
585  Contract.Ensures(Contract.Result<FuncDecl>() != null);
586  return headDecl;
587  }
588  }
589 
593  public FuncDecl TailDecl
594  {
595  get
596  {
597  Contract.Ensures(Contract.Result<FuncDecl>() != null);
598  return tailDecl;
599  }
600  }
601 
602  #region Object Invariant
603 
604  [ContractInvariantMethod]
605  private void ObjectInvariant()
606  {
607  Contract.Invariant(nilConst != null);
608  Contract.Invariant(nilDecl != null);
609  Contract.Invariant(isNilDecl != null);
610  Contract.Invariant(consDecl != null);
611  Contract.Invariant(isConsDecl != null);
612  Contract.Invariant(headDecl != null);
613  Contract.Invariant(tailDecl != null);
614  }
615 
616 
617  #endregion
618 
619  #region Internal
620  readonly private FuncDecl nilDecl, isNilDecl, consDecl, isConsDecl, headDecl, tailDecl;
621  readonly private Expr nilConst;
622 
623  internal ListSort(Context ctx, Symbol name, Sort elemSort)
624  : base(ctx)
625  {
626  Contract.Requires(ctx != null);
627  Contract.Requires(name != null);
628  Contract.Requires(elemSort != null);
629 
630  IntPtr inil = IntPtr.Zero,
631  iisnil = IntPtr.Zero,
632  icons = IntPtr.Zero,
633  iiscons = IntPtr.Zero,
634  ihead = IntPtr.Zero,
635  itail = IntPtr.Zero;
636 
637  NativeObject = Native.Z3_mk_list_sort(ctx.nCtx, name.NativeObject, elemSort.NativeObject,
638  ref inil, ref iisnil, ref icons, ref iiscons, ref ihead, ref itail);
639  nilDecl = new FuncDecl(ctx, inil);
640  isNilDecl = new FuncDecl(ctx, iisnil);
641  consDecl = new FuncDecl(ctx, icons);
642  isConsDecl = new FuncDecl(ctx, iiscons);
643  headDecl = new FuncDecl(ctx, ihead);
644  tailDecl = new FuncDecl(ctx, itail);
645  nilConst = ctx.MkConst(nilDecl);
646  }
647  #endregion
648  };
649 
653  [ContractVerification(true)]
654  public class RelationSort : Sort
655  {
659  public uint Arity
660  {
661  get { return Native.Z3_get_relation_arity(Context.nCtx, NativeObject); }
662  }
663 
667  public Sort[] ColumnSorts
668  {
669  get
670  {
671  Contract.Ensures(Contract.Result<Sort[]>() != null);
672 
673  if (m_columnSorts != null)
674  return m_columnSorts;
675 
676  uint n = Arity;
677  Sort[] res = new Sort[n];
678  for (uint i = 0; i < n; i++)
679  res[i] = Sort.Create(Context, Native.Z3_get_relation_column(Context.nCtx, NativeObject, i));
680  return res;
681  }
682  }
683 
684  #region Internal
685  private Sort[] m_columnSorts = null;
686 
687  internal RelationSort(Context ctx, IntPtr obj)
688  : base(ctx, obj)
689  {
690  Contract.Requires(ctx != null);
691  }
692  #endregion
693  }
694 
698  [ContractVerification(true)]
699  public class FiniteDomainSort : Sort
700  {
704  public ulong Size
705  {
706  get { ulong res = 0; Native.Z3_get_finite_domain_sort_size(Context.nCtx, NativeObject, ref res); return res; }
707  }
708 
709  #region Internal
710  internal FiniteDomainSort(Context ctx, IntPtr obj)
711  : base(ctx, obj)
712  {
713  Contract.Requires(ctx != null);
714  }
715  internal FiniteDomainSort(Context ctx, Symbol name, ulong size)
716  : base(ctx, Native.Z3_mk_finite_domain_sort(ctx.nCtx, name.NativeObject, size))
717  {
718  Contract.Requires(ctx != null);
719  Contract.Requires(name != null);
720 
721  }
722  #endregion
723  }
724 
728  [ContractVerification(true)]
729  public class SetSort : Sort
730  {
731  #region Internal
732  internal SetSort(Context ctx, IntPtr obj)
733  : base(ctx, obj)
734  {
735  Contract.Requires(ctx != null);
736  }
737  internal SetSort(Context ctx, Sort ty)
738  : base(ctx, Native.Z3_mk_set_sort(ctx.nCtx, ty.NativeObject))
739  {
740  Contract.Requires(ctx != null);
741  Contract.Requires(ty != null);
742  }
743  #endregion
744  }
745 }
Generated on Thu Nov 22 2012 18:37:19 for Z3 by   doxygen 1.8.2