00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 using System;
00021 using System.Diagnostics.Contracts;
00022
00023 namespace Microsoft.Z3
00024 {
00028 [ContractVerification(true)]
00029 public class Params : Z3Object
00030 {
00034 public void Add(Symbol name, bool value)
00035 {
00036 Contract.Requires(name != null);
00037
00038 Native.Z3_params_set_bool(Context.nCtx, NativeObject, name.NativeObject, (value) ? 1 : 0);
00039 }
00040
00044 public void Add(Symbol name, uint value)
00045 {
00046 Contract.Requires(name != null);
00047
00048 Native.Z3_params_set_uint(Context.nCtx, NativeObject, name.NativeObject, value);
00049 }
00050
00054 public void Add(Symbol name, double value)
00055 {
00056 Contract.Requires(name != null);
00057
00058 Native.Z3_params_set_double(Context.nCtx, NativeObject, name.NativeObject, value);
00059 }
00060
00064 public void Add(Symbol name, string value)
00065 {
00066 Contract.Requires(value != null);
00067
00068 Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, Context.MkSymbol(value).NativeObject);
00069 }
00070
00074 public void Add(Symbol name, Symbol value)
00075 {
00076 Contract.Requires(name != null);
00077 Contract.Requires(value != null);
00078
00079 Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, value.NativeObject);
00080 }
00081
00085 public void Add(string name, bool value)
00086 {
00087 Native.Z3_params_set_bool(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (value) ? 1 : 0);
00088 }
00089
00093 public void Add(string name, uint value)
00094 {
00095 Native.Z3_params_set_uint(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value);
00096 }
00097
00101 public void Add(string name, double value)
00102 {
00103 Native.Z3_params_set_double(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value);
00104 }
00105
00109 public void Add(string name, Symbol value)
00110 {
00111 Contract.Requires(value != null);
00112
00113 Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value.NativeObject);
00114 }
00115
00119 public void Add(string name, string value)
00120 {
00121 Contract.Requires(value != null);
00122
00123 Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, Context.MkSymbol(value).NativeObject);
00124 }
00125
00129 public override string ToString()
00130 {
00131 return Native.Z3_params_to_string(Context.nCtx, NativeObject);
00132 }
00133
00134 #region Internal
00135 internal Params(Context ctx)
00136 : base(ctx, Native.Z3_mk_params(ctx.nCtx))
00137 {
00138 Contract.Requires(ctx != null);
00139 }
00140
00141 internal class DecRefQueue : IDecRefQueue
00142 {
00143 public override void IncRef(Context ctx, IntPtr obj)
00144 {
00145 Native.Z3_params_inc_ref(ctx.nCtx, obj);
00146 }
00147
00148 public override void DecRef(Context ctx, IntPtr obj)
00149 {
00150 Native.Z3_params_dec_ref(ctx.nCtx, obj);
00151 }
00152 };
00153
00154 internal override void IncRef(IntPtr o)
00155 {
00156 Context.Params_DRQ.IncAndClear(Context, o);
00157 base.IncRef(o);
00158 }
00159
00160 internal override void DecRef(IntPtr o)
00161 {
00162 Context.Params_DRQ.Add(o);
00163 base.DecRef(o);
00164 }
00165 #endregion
00166 }
00167 }