Z3
Loading...
Searching...
No Matches
src
api
dotnet
Simplifiers.cs
Go to the documentation of this file.
1
/*++
2
Copyright (c) 2012 Microsoft Corporation
3
4
Module Name:
5
6
Simplifiers.cs
7
8
Abstract:
9
10
Z3 Managed API: Simplifiers
11
12
Author:
13
14
Christoph Wintersteiger (cwinter) 2012-03-21
15
16
--*/
17
18
using
System;
19
using
System.Diagnostics;
20
21
namespace
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
46
public
ParamDescrs
ParameterDescriptions
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
}
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition
Context.cs:34
Microsoft.Z3.ParamDescrs
A ParamDescrs describes a set of parameters.
Definition
ParamDescrs.cs:29
Microsoft.Z3.Simplifier
Simplifiers are the basic building block for creating custom solvers with incremental pre-processing....
Definition
Simplifiers.cs:30
Microsoft.Z3.Simplifier.Help
string Help
A string containing a description of parameters accepted by the tactic.
Definition
Simplifiers.cs:35
Microsoft.Z3.Simplifier.ParameterDescriptions
ParamDescrs ParameterDescriptions
Retrieves parameter descriptions for Simplifiers.
Definition
Simplifiers.cs:47
Microsoft.Z3.Z3Object
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition
Z3Object.cs:33
Microsoft.Z3.Z3Object.Context
Context Context
Access Context object.
Definition
Z3Object.cs:111
Z3_mk_simplifier
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 ...
Microsoft.Z3
Definition
AlgebraicNum.cs:27
Generated on Sat Dec 20 2025 19:33:21 for Z3 by
1.9.8