|
Z3
|
|
|
Z3
|
|
Quantifier expressions. More...
Inheritance diagram for Quantifier:Properties | |
| bool | IsUniversal [get] |
| Indicates whether the quantifier is universal. More... | |
| bool | IsExistential [get] |
| Indicates whether the quantifier is existential. More... | |
| uint | Weight [get] |
| The weight of the quantifier. More... | |
| uint | NumPatterns [get] |
| The number of patterns. More... | |
| Pattern[] | Patterns [get] |
| The patterns. More... | |
| uint | NumNoPatterns [get] |
| The number of no-patterns. More... | |
| Pattern[] | NoPatterns [get] |
| The no-patterns. More... | |
| uint | NumBound [get] |
| The number of bound variables. More... | |
| Symbol[] | BoundVariableNames [get] |
| The symbols for the bound variables. More... | |
| Sort[] | BoundVariableSorts [get] |
| The sorts of the bound variables. More... | |
| BoolExpr | Body [get] |
| The body of the quantifier. More... | |
Quantifier expressions.
Definition at line 29 of file Quantifier.cs.
|
get |
The body of the quantifier.
Definition at line 151 of file Quantifier.cs.
|
get |
The symbols for the bound variables.
Definition at line 117 of file Quantifier.cs.
|
get |
The sorts of the bound variables.
Definition at line 134 of file Quantifier.cs.
|
get |
Indicates whether the quantifier is existential.
Definition at line 43 of file Quantifier.cs.
|
get |
Indicates whether the quantifier is universal.
Definition at line 35 of file Quantifier.cs.
|
get |
The no-patterns.
Definition at line 92 of file Quantifier.cs.
|
get |
The number of bound variables.
Definition at line 109 of file Quantifier.cs.
|
get |
The number of no-patterns.
Definition at line 84 of file Quantifier.cs.
|
get |
The number of patterns.
Definition at line 59 of file Quantifier.cs.
|
get |
The patterns.
Definition at line 67 of file Quantifier.cs.
|
get |
The weight of the quantifier.
Definition at line 51 of file Quantifier.cs.
1.8.9.1
