Z3
Data Structures | Typedefs | Enumerations
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  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 Z3_solver_callback = System.IntPtr
 

Enumerations

enum class  Status { UNSATISFIABLE = -1 , UNKNOWN = 0 , SATISFIABLE = 1 }
 Status values. More...
 

Typedef Documentation

◆ voidp

typedef System IntPtr voidp

Definition at line 32 of file OnClause.cs.

◆ Z3_app

typedef System IntPtr Z3_app

Definition at line 27 of file NativeContext.cs.

◆ Z3_ast

typedef System IntPtr Z3_ast

Definition at line 28 of file NativeContext.cs.

◆ Z3_ast_vector

typedef System IntPtr Z3_ast_vector

Definition at line 29 of file NativeContext.cs.

◆ Z3_context

typedef System IntPtr Z3_context

Definition at line 29 of file Context.cs.

◆ Z3_func_decl

typedef System IntPtr Z3_func_decl

Definition at line 30 of file NativeContext.cs.

◆ Z3_func_entry

using Z3_func_entry = System.IntPtr

Definition at line 33 of file NativeFuncInterp.cs.

◆ Z3_func_interp

using Z3_func_interp = System.IntPtr

Definition at line 32 of file NativeFuncInterp.cs.

◆ Z3_model

using Z3_model = System.IntPtr

Definition at line 31 of file NativeFuncInterp.cs.

◆ Z3_params

using Z3_params = System.IntPtr

Definition at line 32 of file NativeSolver.cs.

◆ Z3_pattern

using Z3_pattern = System.IntPtr

Definition at line 31 of file NativeContext.cs.

◆ Z3_solver

typedef System IntPtr Z3_solver

Definition at line 32 of file NativeContext.cs.

◆ Z3_solver_callback

using Z3_solver_callback = System.IntPtr

Definition at line 30 of file UserPropagator.cs.

◆ Z3_sort

typedef System IntPtr Z3_sort

Definition at line 33 of file NativeContext.cs.

◆ Z3_stats

typedef System IntPtr Z3_stats

Definition at line 34 of file NativeContext.cs.

◆ Z3_symbol

typedef System IntPtr Z3_symbol

Definition at line 35 of file NativeContext.cs.

Enumeration Type Documentation

◆ Status

enum Status
strong

Status values.

Enumerator
UNSATISFIABLE 

Used to signify an unsatisfiable status.

UNKNOWN 

Used to signify an unknown status.

SATISFIABLE 

Used to signify a satisfiable status.

Definition at line 28 of file Status.cs.

29  {
33  UNSATISFIABLE = -1,
34 
38  UNKNOWN = 0,
39 
43  SATISFIABLE = 1
44  }
@ UNKNOWN
Used to signify an unknown status.
@ UNSATISFIABLE
Used to signify an unsatisfiable status.
@ SATISFIABLE
Used to signify a satisfiable status.