Z3
Properties
ListSort Class Reference

List sorts. More...

+ Inheritance diagram for ListSort:

Properties

FuncDecl NilDecl [get]
 The declaration of the nil function of this list sort. More...
 
Expr Nil [get]
 The empty list. More...
 
FuncDecl IsNilDecl [get]
 The declaration of the isNil function of this list sort. More...
 
FuncDecl ConsDecl [get]
 The declaration of the cons function of this list sort. More...
 
FuncDecl IsConsDecl [get]
 The declaration of the isCons function of this list sort. More...
 
FuncDecl HeadDecl [get]
 The declaration of the head function of this list sort. More...
 
FuncDecl TailDecl [get]
 The declaration of the tail function of this list sort. More...
 
- Properties inherited from Sort
new uint Id [get]
 Returns a unique identifier for the sort. More...
 
Z3_sort_kind SortKind [get]
 The kind of the sort. More...
 
Symbol Name [get]
 The name of the sort More...
 
- Properties inherited from AST
uint Id [get]
 A unique identifier for the AST (unique among all ASTs). More...
 
Z3_ast_kind ASTKind [get]
 The kind of the AST. More...
 
bool IsExpr [get]
 Indicates whether the AST is an Expr More...
 
bool IsApp [get]
 Indicates whether the AST is an application More...
 
bool IsVar [get]
 Indicates whether the AST is a BoundVariable More...
 
bool IsQuantifier [get]
 Indicates whether the AST is a Quantifier More...
 
bool IsSort [get]
 Indicates whether the AST is a Sort More...
 
bool IsFuncDecl [get]
 Indicates whether the AST is a FunctionDeclaration More...
 

Additional Inherited Members

- Public Member Functions inherited from Sort
override bool Equals (object o)
 Equality operator for objects of type Sort. More...
 
override int GetHashCode ()
 Hash code generation for Sorts More...
 
override string ToString ()
 A string representation of the sort. More...
 
- Public Member Functions inherited from AST
override bool Equals (object o)
 Object comparison. More...
 
virtual int CompareTo (object other)
 Object Comparison. More...
 
override int GetHashCode ()
 The AST's hash code. More...
 
AST Translate (Context ctx)
 Translates (copies) the AST to the Context ctx . More...
 
override string ToString ()
 A string representation of the AST. More...
 
string SExpr ()
 A string representation of the AST in s-expression notation. More...
 
- Public Member Functions inherited from Z3Object
void Dispose ()
 Disposes of the underlying native Z3 object. More...
 
- Static Public Member Functions inherited from Sort
static bool operator== (Sort a, Sort b)
 Comparison operator. More...
 
static bool operator!= (Sort a, Sort b)
 Comparison operator. More...
 
- Static Public Member Functions inherited from AST
static bool operator== (AST a, AST b)
 Comparison operator. More...
 
static bool operator!= (AST a, AST b)
 Comparison operator. More...
 

Detailed Description

List sorts.

Definition at line 29 of file ListSort.cs.

Property Documentation

◆ ConsDecl

FuncDecl ConsDecl
get

The declaration of the cons function of this list sort.

Definition at line 71 of file ListSort.cs.

71  {
72  get
73  {
74  Contract.Ensures(Contract.Result<FuncDecl>() != null);
75  return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, 1));
76  }
77  }

◆ HeadDecl

FuncDecl HeadDecl
get

The declaration of the head function of this list sort.

Definition at line 96 of file ListSort.cs.

96  {
97  get
98  {
99  Contract.Ensures(Contract.Result<FuncDecl>() != null);
100  return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, 1, 0));
101  }
102  }

◆ IsConsDecl

FuncDecl IsConsDecl
get

The declaration of the isCons function of this list sort.

Definition at line 84 of file ListSort.cs.

84  {
85  get
86  {
87  Contract.Ensures(Contract.Result<FuncDecl>() != null);
88  return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, 1));
89  }
90  }

◆ IsNilDecl

FuncDecl IsNilDecl
get

The declaration of the isNil function of this list sort.

Definition at line 59 of file ListSort.cs.

59  {
60  get
61  {
62  Contract.Ensures(Contract.Result<FuncDecl>() != null);
63  return new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, 0));
64  }
65  }

◆ Nil

Expr Nil
get

The empty list.

Definition at line 47 of file ListSort.cs.

47  {
48  get
49  {
50  Contract.Ensures(Contract.Result<Expr>() != null);
51  return Context.MkApp(NilDecl);
52  }
53  }
Expr MkApp(FuncDecl f, params Expr[] args)
Create a new function application.
Definition: Context.cs:807
FuncDecl NilDecl
The declaration of the nil function of this list sort.
Definition: ListSort.cs:35

◆ NilDecl

FuncDecl NilDecl
get

The declaration of the nil function of this list sort.

Definition at line 35 of file ListSort.cs.

35  {
36  get
37  {
38  Contract.Ensures(Contract.Result<FuncDecl>() != null);
39  return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, 0));
40  }
41  }

◆ TailDecl

FuncDecl TailDecl
get

The declaration of the tail function of this list sort.

Definition at line 108 of file ListSort.cs.

108  {
109  get
110  {
111  Contract.Ensures(Contract.Result<FuncDecl>() != null);
112  return new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, 1, 1));
113  }
114  }