Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules 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, 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 override void IncRef(Context ctx, IntPtr obj)
144  {
145  Native.Z3_params_inc_ref(ctx.nCtx, obj);
146  }
147 
148  public override void DecRef(Context ctx, IntPtr obj)
149  {
150  Native.Z3_params_dec_ref(ctx.nCtx, obj);
151  }
152  };
153 
154  internal override void IncRef(IntPtr o)
155  {
156  Context.Params_DRQ.IncAndClear(Context, o);
157  base.IncRef(o);
158  }
159 
160  internal override void DecRef(IntPtr o)
161  {
162  Context.Params_DRQ.Add(o);
163  base.DecRef(o);
164  }
165  #endregion
166  }
167 }
static void Z3_params_set_uint(Z3_context a0, Z3_params a1, IntPtr a2, uint a3)
Definition: Native.cs:1776
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:1797
void Add(string name, bool value)
Adds a parameter setting.
Definition: Params.cs:85
A ParameterSet 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:1790
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:1783
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:1769
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