Showing content from https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html below:
Z3: Microsoft.Z3 Namespace Reference
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...
RetroSearch is an open source project built by @garambo
| Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4