Simplifier Class Reference

Simplifiers are the basic building block for creating custom solvers with incremental pre-processing. The complete list of simplifiers may be obtained using Context.NumSimplifiers and Context.SimplifierNames. It may also be obtained using the command (help-simplifier) in the SMT 2.0 front-end. More...

Inheritance diagram for Simplifier:

Properties
string	Help [get]
	A string containing a description of parameters accepted by the tactic. More...
ParamDescrs	ParameterDescriptions [get]
	Retrieves parameter descriptions for Simplifiers. More...
Properties inherited from Z3Object
Context	Context [get]
	Access Context object More...

Additional Inherited Members
Public Member Functions inherited from Z3Object
void	Dispose ()
	Disposes of the underlying native Z3 object. More...

Detailed Description

Simplifiers are the basic building block for creating custom solvers with incremental pre-processing. The complete list of simplifiers may be obtained using Context.NumSimplifiers and Context.SimplifierNames. It may also be obtained using the command (help-simplifier) in the SMT 2.0 front-end.

Definition at line 29 of file Simplifiers.cs.

Property Documentation

Help

string Help

get

A string containing a description of parameters accepted by the tactic.

Definition at line 34 of file Simplifiers.cs.

        {
            get
            {
 
                return Native.Z3_simplifier_get_help(Context.nCtx, NativeObject);
            }
        }

ParameterDescriptions

ParamDescrs ParameterDescriptions

get

Retrieves parameter descriptions for Simplifiers.

Definition at line 46 of file Simplifiers.cs.

        {
            get { return new ParamDescrs(Context, Native.Z3_simplifier_get_param_descrs(Context.nCtx, NativeObject)); }
        }