Z3
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, string value)
65  {
66  Contract.Requires(value != null);
67 
68  Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, Context.MkSymbol(value).NativeObject);
69  }
70 
74  public void Add(Symbol name, Symbol value)
75  {
76  Contract.Requires(name != null);
77  Contract.Requires(value != null);
78 
79  Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, value.NativeObject);
80  }
81 
85  public void Add(string name, bool value)
86  {
87  Native.Z3_params_set_bool(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (value) ? 1 : 0);
88  }
89 
93  public void Add(string name, uint value)
94  {
95  Native.Z3_params_set_uint(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value);
96  }
97 
101  public void Add(string name, double value)
102  {
103  Native.Z3_params_set_double(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value);
104  }
105 
109  public void Add(string name, Symbol value)
110  {
111  Contract.Requires(value != null);
112 
113  Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value.NativeObject);
114  }
115 
119  public void Add(string name, string value)
120  {
121  Contract.Requires(value != null);
122 
123  Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, Context.MkSymbol(value).NativeObject);
124  }
125 
129  public override string ToString()
130  {
131  return Native.Z3_params_to_string(Context.nCtx, NativeObject);
132  }
133 
134  #region Internal
135  internal Params(Context ctx)
136  : base(ctx, Native.Z3_mk_params(ctx.nCtx))
137  {
138  Contract.Requires(ctx != null);
139  }
140 
141  internal class DecRefQueue : IDecRefQueue
142  {
143  public DecRefQueue() : base() { }
144  public DecRefQueue(uint move_limit) : base(move_limit) { }
145  internal override void IncRef(Context ctx, IntPtr obj)
146  {
147  Native.Z3_params_inc_ref(ctx.nCtx, obj);
148  }
149 
150  internal override void DecRef(Context ctx, IntPtr obj)
151  {
152  Native.Z3_params_dec_ref(ctx.nCtx, obj);
153  }
154  };
155 
156  internal override void IncRef(IntPtr o)
157  {
158  Context.Params_DRQ.IncAndClear(Context, o);
159  base.IncRef(o);
160  }
161 
162  internal override void DecRef(IntPtr o)
163  {
164  Context.Params_DRQ.Add(o);
165  base.DecRef(o);
166  }
167  #endregion
168  }
169 }
static void Z3_params_set_uint(Z3_context a0, Z3_params a1, IntPtr a2, uint a3)
Definition: Native.cs:1983
void Add(string name, uint value)
Adds a parameter setting.
Definition: Params.cs:93
void Add(Symbol name, bool value)
Adds a parameter setting.
Definition: Params.cs:34
void Add(string name, string value)
Adds a parameter setting.
Definition: Params.cs:119
void Add(Symbol name, string value)
Adds a parameter setting.
Definition: Params.cs:64
void Add(Symbol name, Symbol value)
Adds a parameter setting.
Definition: Params.cs:74
override string ToString()
A string representation of the parameter set.
Definition: Params.cs:129
void Add(string name, Symbol value)
Adds a parameter setting.
Definition: Params.cs:109
static string Z3_params_to_string(Z3_context a0, Z3_params a1)
Definition: Native.cs:2004
void Add(string name, bool value)
Adds a parameter setting.
Definition: Params.cs:85
A Params objects represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
void Add(Symbol name, double value)
Adds a parameter setting.
Definition: Params.cs:54
static void Z3_params_set_symbol(Z3_context a0, Z3_params a1, IntPtr a2, IntPtr a3)
Definition: Native.cs:1997
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:84
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
static void Z3_params_set_double(Z3_context a0, Z3_params a1, IntPtr a2, double a3)
Definition: Native.cs:1990
Z3_params Z3_API Z3_mk_params(__in Z3_context c)
Create a Z3 (empty) parameter set. Starting at Z3 4.0, parameter sets are used to configure many comp...
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:31
static void Z3_params_set_bool(Z3_context a0, Z3_params a1, IntPtr a2, int a3)
Definition: Native.cs:1976
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
void Add(Symbol name, uint value)
Adds a parameter setting.
Definition: Params.cs:44
void Add(string name, double value)
Adds a parameter setting.
Definition: Params.cs:101