|
Z3
|
|
|
Z3
|
|
Data Structures | |
| class | AlgebraicNum |
| Algebraic numbers More... | |
| class | ApplyResult |
| ApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced. More... | |
| class | ArithExpr |
| Arithmetic expressions (int/real) More... | |
| class | ArithSort |
| An arithmetic sort, i.e., Int or Real. More... | |
| class | ArrayExpr |
| Array expressions More... | |
| class | ArraySort |
| Array sorts. More... | |
| class | AST |
| The abstract syntax tree (AST) class. More... | |
| class | ASTMap |
| Map from AST to AST | |
| class | ASTVector |
| Vectors of ASTs. More... | |
| class | BitVecExpr |
| Bit-vector expressions More... | |
| class | BitVecNum |
| Bit-vector numerals More... | |
| class | BitVecSort |
| Bit-vector sorts. More... | |
| class | BoolExpr |
| Boolean expressions More... | |
| class | BoolSort |
| A Boolean sort. More... | |
| class | CharSort |
| A Character sort More... | |
| class | Constructor |
| Constructors are used for datatype sorts. More... | |
| class | ConstructorList |
| Lists of constructors More... | |
| class | Context |
| The main interaction with Z3 happens via the Context. More... | |
| class | DatatypeExpr |
| Datatype expressions More... | |
| class | DatatypeSort |
| Datatype sorts. More... | |
| class | EnumSort |
| Enumeration sorts. More... | |
| class | Expr |
| Expressions are terms. More... | |
| class | FiniteDomainExpr |
| Finite-domain expressions More... | |
| class | FiniteDomainNum |
| Finite-domain numerals More... | |
| class | FiniteDomainSort |
| Finite domain sorts. More... | |
| class | Fixedpoint |
| Object for managing fixedpoints More... | |
| class | FPExpr |
| FloatingPoint Expressions More... | |
| class | FPNum |
| FloatiungPoint Numerals More... | |
| class | FPRMExpr |
| FloatingPoint RoundingMode Expressions More... | |
| class | FPRMNum |
| Floating-point rounding mode numerals More... | |
| class | FPRMSort |
| The FloatingPoint RoundingMode sort More... | |
| class | FPSort |
| FloatingPoint sort More... | |
| class | FuncDecl |
| Function declarations. More... | |
| class | FuncInterp |
| A function interpretation is represented as a finite map and an 'else' value. Each entry in the finite map represents the value of a function given a set of arguments. More... | |
| class | Global |
| Global functions for Z3. | |
| class | Goal |
| A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers. More... | |
| class | IntExpr |
| Int expressions More... | |
| class | IntNum |
| Integer Numerals More... | |
| class | IntSort |
| An Integer sort More... | |
| class | IntSymbol |
| Numbered symbols More... | |
| class | Lambda |
| Lambda expressions. More... | |
| class | ListSort |
| List sorts. More... | |
| class | Log |
| Interaction logging for Z3. | |
| class | Model |
| A Model contains interpretations (assignments) of constants and functions. More... | |
| class | NativeContext |
| The main interaction with Z3 happens via the Context. NativeContext allows for efficient wrapper-reduced interaction with Z3 expressions. More... | |
| class | NativeFuncInterp |
| A function interpretation is represented as a finite map and an 'else' value. Each entry in the finite map represents the value of a function given a set of arguments. More... | |
| class | NativeModel |
| A Model contains interpretations (assignments) of constants and functions. More... | |
| class | NativeSolver |
| Solvers. More... | |
| class | OnClause |
| OnClause - clause inference callback More... | |
| class | Optimize |
| Object for managing optimization context More... | |
| class | ParamDescrs |
| A ParamDescrs describes a set of parameters. More... | |
| class | Params |
| A Params objects represents a configuration in the form of Symbol/value pairs. More... | |
| class | Pattern |
| Patterns comprise a list of terms. The list should be non-empty. If the list comprises of more than one term, it is also called a multi-pattern. More... | |
| class | Probe |
Probes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used. The complete list of probes may be obtained using the procedures Context.NumProbes and Context.ProbeNames. It may also be obtained using the command (help-tactic) in the SMT 2.0 front-end. More... | |
| class | Quantifier |
| Quantifier expressions. More... | |
| class | RatNum |
| Rational Numerals More... | |
| class | RealExpr |
| Real expressions More... | |
| class | RealSort |
| A real sort More... | |
| class | ReExpr |
| Regular expression expressions More... | |
| class | RelationSort |
| Relation sorts. More... | |
| class | ReSort |
| A regular expression sort More... | |
| class | SeqExpr |
| Sequence expressions More... | |
| class | SeqSort |
| A Sequence sort More... | |
| class | SetSort |
| Set sorts. More... | |
| class | Simplifier |
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... | |
| class | Solver |
| Solvers. More... | |
| class | Sort |
| The Sort class implements type information for ASTs. More... | |
| class | Statistics |
| Objects of this class track statistical information about solvers. More... | |
| class | StringSymbol |
| Named symbols More... | |
| class | Symbol |
| Symbols are used to name several term and type constructors. More... | |
| class | Tactic |
Tactics are the basic building block for creating custom solvers for specific problem domains. The complete list of tactics may be obtained using Context.NumTactics and Context.TacticNames. It may also be obtained using the command (help-tactic) in the SMT 2.0 front-end. More... | |
| class | TupleSort |
| Tuple sorts. More... | |
| class | UninterpretedSort |
| Uninterpreted Sorts More... | |
| class | UserPropagator |
| Propagator context for .Net More... | |
| class | EqualityPairs |
| A list of equalities used as justifications for propagation More... | |
| class | Version |
| Version information. | |
| class | Z3Exception |
| The exception base class for error reporting from Z3 More... | |
| class | Z3Object |
| Internal base class for interfacing with native Z3 objects. Should not be used externally. More... | |
Typedefs | |
| using | Z3_context = System.IntPtr |
| using | Z3_app = System.IntPtr |
| using | Z3_ast = System.IntPtr |
| using | Z3_ast_vector = System.IntPtr |
| using | Z3_func_decl = System.IntPtr |
| using | Z3_pattern = System.IntPtr |
| using | Z3_solver = System.IntPtr |
| using | Z3_sort = System.IntPtr |
| using | Z3_stats = System.IntPtr |
| using | Z3_symbol = System.IntPtr |
| using | Z3_model = System.IntPtr |
| using | Z3_func_interp = System.IntPtr |
| using | Z3_func_entry = System.IntPtr |
| using | Z3_params = System.IntPtr |
| using | voidp = System.IntPtr |
| using | uintp = System.IntPtr |
| using | Z3_solver_callback = System.IntPtr |
Enumerations | |
| enum class | Status { UNSATISFIABLE = -1 , UNKNOWN = 0 , SATISFIABLE = 1 } |
| Status values. More... | |
| using uintp = System.IntPtr |
Definition at line 33 of file OnClause.cs.
| typedef System IntPtr voidp |
Definition at line 32 of file OnClause.cs.
| typedef System IntPtr Z3_app |
Definition at line 27 of file NativeContext.cs.
| typedef System IntPtr Z3_ast |
Definition at line 28 of file NativeContext.cs.
| typedef System IntPtr Z3_ast_vector |
Definition at line 29 of file NativeContext.cs.
| typedef System IntPtr Z3_context |
Definition at line 29 of file Context.cs.
| typedef System IntPtr Z3_func_decl |
Definition at line 30 of file NativeContext.cs.
| using Z3_func_entry = System.IntPtr |
Definition at line 33 of file NativeFuncInterp.cs.
| using Z3_func_interp = System.IntPtr |
Definition at line 32 of file NativeFuncInterp.cs.
| using Z3_model = System.IntPtr |
Definition at line 31 of file NativeFuncInterp.cs.
| using Z3_params = System.IntPtr |
Definition at line 32 of file NativeSolver.cs.
| using Z3_pattern = System.IntPtr |
Definition at line 31 of file NativeContext.cs.
| typedef System IntPtr Z3_solver |
Definition at line 32 of file NativeContext.cs.
| using Z3_solver_callback = System.IntPtr |
Definition at line 30 of file UserPropagator.cs.
| typedef System IntPtr Z3_sort |
Definition at line 33 of file NativeContext.cs.
| typedef System IntPtr Z3_stats |
Definition at line 34 of file NativeContext.cs.
| typedef System IntPtr Z3_symbol |
Definition at line 35 of file NativeContext.cs.
1.9.1