Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Params.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  Parameter.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Parameters
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 Params : Z3Object
30  {
34  public void Add(Symbol name, bool value)
35  {
36  Contract.Requires(name != null);
37 
38  Native.Z3_params_set_bool(Context.nCtx, NativeObject, name.NativeObject, (value) ? 1 : 0);
39  }
40 
44  public void Add(Symbol name, uint value)
45  {
46  Contract.Requires(name != null);
47 
48  Native.Z3_params_set_uint(Context.nCtx, NativeObject, name.NativeObject, value);
49  }
50 
54  public void Add(Symbol name, double value)
55  {
56  Contract.Requires(name != null);
57 
58  Native.Z3_params_set_double(Context.nCtx, NativeObject, name.NativeObject, value);
59  }
60 
64  public void Add(Symbol name, Symbol value)
65  {
66  Contract.Requires(name != null);
67  Contract.Requires(value != null);
68 
69  Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, value.NativeObject);
70  }
71 
75  public void Add(string name, bool value)
76  {
77  Native.Z3_params_set_bool(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (value) ? 1 : 0);
78  }
79 
83  public void Add(string name, uint value)
84  {
85  Native.Z3_params_set_uint(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value);
86  }
87 
91  public void Add(string name, double value)
92  {
93  Native.Z3_params_set_double(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value);
94  }
95 
99  public void Add(string name, Symbol value)
100  {
101  Contract.Requires(value != null);
102 
103  Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value.NativeObject);
104  }
105 
109  public override string ToString()
110  {
111  return Native.Z3_params_to_string(Context.nCtx, NativeObject);
112  }
113 
114  #region Internal
115  internal Params(Context ctx)
116  : base(ctx, Native.Z3_mk_params(ctx.nCtx))
117  {
118  Contract.Requires(ctx != null);
119  }
120 
121  internal class DecRefQueue : Z3.DecRefQueue
122  {
123  public override void IncRef(Context ctx, IntPtr obj)
124  {
125  Native.Z3_params_inc_ref(ctx.nCtx, obj);
126  }
127 
128  public override void DecRef(Context ctx, IntPtr obj)
129  {
130  Native.Z3_params_dec_ref(ctx.nCtx, obj);
131  }
132  };
133 
134  internal override void IncRef(IntPtr o)
135  {
136  Context.Params_DRQ.IncAndClear(Context, o);
137  base.IncRef(o);
138  }
139 
140  internal override void DecRef(IntPtr o)
141  {
142  Context.Params_DRQ.Add(o);
143  base.DecRef(o);
144  }
145  #endregion
146  }
147 }