|
Z3
|
|
Loading...
Searching...
No Matches
|
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 | EqualityPairs |
| A list of equalities used as justifications for propagation. 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 | 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 | 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.
| enum Status |
Status values.
| Enumerator | |
|---|---|
| UNSATISFIABLE | Used to signify an unsatisfiable status. |
| UNKNOWN | Used to signify an unknown status. |
| SATISFIABLE | Used to signify a satisfiable status. |
1.9.8