Z3
FuncInterp.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  FuncInterp.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Function Interpretations
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-03-21
15 
16 Notes:
17 
18 --*/
19 
20 using System;
21 using System.Diagnostics.Contracts;
22 
23 namespace Microsoft.Z3
24 {
29  [ContractVerification(true)]
30  public class FuncInterp : Z3Object
31  {
36  public class Entry : Z3Object
37  {
41  public Expr Value
42  {
43  get
44  {
45  Contract.Ensures(Contract.Result<Expr>() != null);
46  return Expr.Create(Context, Native.Z3_func_entry_get_value(Context.nCtx, NativeObject));
47  }
48  }
49 
53  public uint NumArgs
54  {
55  get { return Native.Z3_func_entry_get_num_args(Context.nCtx, NativeObject); }
56  }
57 
61  public Expr[] Args
62  {
63  get
64  {
65  Contract.Ensures(Contract.Result<Expr[]>() != null);
66  Contract.Ensures(Contract.Result<Expr[]>().Length == this.NumArgs);
67 
68  uint n = NumArgs;
69  Expr[] res = new Expr[n];
70  for (uint i = 0; i < n; i++)
71  res[i] = Expr.Create(Context, Native.Z3_func_entry_get_arg(Context.nCtx, NativeObject, i));
72  return res;
73  }
74  }
75 
79  public override string ToString()
80  {
81  uint n = NumArgs;
82  string res = "[";
83  Expr[] args = Args;
84  for (uint i = 0; i < n; i++)
85  res += args[i] + ", ";
86  return res + Value + "]";
87  }
88 
89  #region Internal
90  internal Entry(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
91 
92  internal class DecRefQueue : IDecRefQueue
93  {
94  public override void IncRef(Context ctx, IntPtr obj)
95  {
96  Native.Z3_func_entry_inc_ref(ctx.nCtx, obj);
97  }
98 
99  public override void DecRef(Context ctx, IntPtr obj)
100  {
101  Native.Z3_func_entry_dec_ref(ctx.nCtx, obj);
102  }
103  };
104 
105  internal override void IncRef(IntPtr o)
106  {
107  Context.FuncEntry_DRQ.IncAndClear(Context, o);
108  base.IncRef(o);
109  }
110 
111  internal override void DecRef(IntPtr o)
112  {
113  Context.FuncEntry_DRQ.Add(o);
114  base.DecRef(o);
115  }
116  #endregion
117  };
118 
122  public uint NumEntries
123  {
124  get { return Native.Z3_func_interp_get_num_entries(Context.nCtx, NativeObject); }
125  }
126 
130  public Entry[] Entries
131  {
132  get
133  {
134  Contract.Ensures(Contract.Result<Entry[]>() != null);
135  Contract.Ensures(Contract.ForAll(0, Contract.Result<Entry[]>().Length, j => Contract.Result<Entry[]>()[j] != null));
136 
137  uint n = NumEntries;
138  Entry[] res = new Entry[n];
139  for (uint i = 0; i < n; i++)
140  res[i] = new Entry(Context, Native.Z3_func_interp_get_entry(Context.nCtx, NativeObject, i));
141  return res;
142  }
143  }
144 
148  public Expr Else
149  {
150  get
151  {
152  Contract.Ensures(Contract.Result<Expr>() != null);
153 
154  return Expr.Create(Context, Native.Z3_func_interp_get_else(Context.nCtx, NativeObject));
155  }
156  }
157 
161  public uint Arity
162  {
163  get { return Native.Z3_func_interp_get_arity(Context.nCtx, NativeObject); }
164  }
165 
169  public override string ToString()
170  {
171  string res = "";
172  res += "[";
173  foreach (Entry e in Entries)
174  {
175  uint n = e.NumArgs;
176  if (n > 1) res += "[";
177  Expr[] args = e.Args;
178  for (uint i = 0; i < n; i++)
179  {
180  if (i != 0) res += ", ";
181  res += args[i];
182  }
183  if (n > 1) res += "]";
184  res += " -> " + e.Value + ", ";
185  }
186  res += "else -> " + Else;
187  res += "]";
188  return res;
189  }
190 
191  #region Internal
192  internal FuncInterp(Context ctx, IntPtr obj)
193  : base(ctx, obj)
194  {
195  Contract.Requires(ctx != null);
196  }
197 
198  internal class DecRefQueue : IDecRefQueue
199  {
200  public override void IncRef(Context ctx, IntPtr obj)
201  {
202  Native.Z3_func_interp_inc_ref(ctx.nCtx, obj);
203  }
204 
205  public override void DecRef(Context ctx, IntPtr obj)
206  {
207  Native.Z3_func_interp_dec_ref(ctx.nCtx, obj);
208  }
209  };
210 
211  internal override void IncRef(IntPtr o)
212  {
213  Context.FuncInterp_DRQ.IncAndClear(Context, o);
214  base.IncRef(o);
215  }
216 
217  internal override void DecRef(IntPtr o)
218  {
219  Context.FuncInterp_DRQ.Add(o);
220  base.DecRef(o);
221  }
222  #endregion
223  }
224 }
override string ToString()
A string representation of the function entry.
Definition: FuncInterp.cs:79
Expr Value
Return the (symbolic) value of this entry.
Definition: FuncInterp.cs:42
override string ToString()
A string representation of the function interpretation.
Definition: FuncInterp.cs:169
uint NumArgs
The number of arguments of the expression.
Definition: Expr.cs:71
static void Z3_func_entry_inc_ref(Z3_context a0, Z3_func_entry a1)
Definition: Native.cs:3770
Expressions are terms.
Definition: Expr.cs:29
static uint Z3_func_entry_get_num_args(Z3_context a0, Z3_func_entry a1)
Definition: Native.cs:3792
static uint Z3_func_interp_get_arity(Z3_context a0, Z3_func_interp a1)
Definition: Native.cs:3762
static Z3_ast Z3_func_entry_get_arg(Z3_context a0, Z3_func_entry a1, uint a2)
Definition: Native.cs:3800
static uint Z3_func_interp_get_num_entries(Z3_context a0, Z3_func_interp a1)
Definition: Native.cs:3738
static Z3_ast Z3_func_interp_get_else(Z3_context a0, Z3_func_interp a1)
Definition: Native.cs:3754
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
static Z3_ast Z3_func_entry_get_value(Z3_context a0, Z3_func_entry a1)
Definition: Native.cs:3784
Expr[] Args
The arguments of the function entry.
Definition: FuncInterp.cs:62
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:31
uint NumArgs
The number of arguments of the entry.
Definition: FuncInterp.cs:54
An Entry object represents an element in the finite map used to encode a function interpretation...
Definition: FuncInterp.cs:36
static Z3_func_entry Z3_func_interp_get_entry(Z3_context a0, Z3_func_interp a1, uint a2)
Definition: Native.cs:3746
A function interpretation is represented as a finite map and an 'else' value. Each entry in the finit...
Definition: FuncInterp.cs:30