Z3
 
Loading...
Searching...
No Matches
Simplifiers.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2012 Microsoft Corporation
3
4Module Name:
5
6 Simplifiers.cs
7
8Abstract:
9
10 Z3 Managed API: Simplifiers
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2012-03-21
15
16--*/
17
18using System;
19using System.Diagnostics;
20
21namespace Microsoft.Z3
22{
29 public class Simplifier : Z3Object
30 {
34 public string Help
35 {
36 get
37 {
38
39 return Native.Z3_simplifier_get_help(Context.nCtx, NativeObject);
40 }
41 }
42
47 {
48 get { return new ParamDescrs(Context, Native.Z3_simplifier_get_param_descrs(Context.nCtx, NativeObject)); }
49 }
50
51 #region Internal
52 internal Simplifier(Context ctx, IntPtr obj)
53 : base(ctx, obj)
54 {
55 Debug.Assert(ctx != null);
56 }
57 internal Simplifier(Context ctx, string name)
58 : base(ctx, Native.Z3_mk_simplifier(ctx.nCtx, name))
59 {
60 Debug.Assert(ctx != null);
61 }
62
63 internal override void IncRef(IntPtr o)
64 {
65 Native.Z3_simplifier_inc_ref(Context.nCtx, o);
66 }
67
68 internal override void DecRef(IntPtr o)
69 {
70 lock (Context)
71 {
72 if (Context.nCtx != IntPtr.Zero)
73 Native.Z3_simplifier_dec_ref(Context.nCtx, o);
74 }
75 }
76 #endregion
77 }
78}
The main interaction with Z3 happens via the Context.
Definition Context.cs:34
A ParamDescrs describes a set of parameters.
Simplifiers are the basic building block for creating custom solvers with incremental pre-processing....
string Help
A string containing a description of parameters accepted by the tactic.
ParamDescrs ParameterDescriptions
Retrieves parameter descriptions for Simplifiers.
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition Z3Object.cs:33
Context Context
Access Context object.
Definition Z3Object.cs:111
Z3_simplifier Z3_API Z3_mk_simplifier(Z3_context c, Z3_string name)
Return a simplifier associated with the given name. The complete list of simplifiers may be obtained ...