Z3
src/api/dotnet/Params.cs
Go to the documentation of this file.
00001 /*++
00002 Copyright (c) 2012 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     Parameter.cs
00007 
00008 Abstract:
00009 
00010     Z3 Managed API: Parameters
00011 
00012 Author:
00013 
00014     Christoph Wintersteiger (cwinter) 2012-03-20
00015 
00016 Notes:
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines