Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
Properties
Quantifier Class Reference

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...
 

Detailed Description

Quantifier expressions.

Definition at line 29 of file Quantifier.cs.

Property Documentation

BoolExpr Body
get

The body of the quantifier.

Definition at line 151 of file Quantifier.cs.

Symbol [] BoundVariableNames
get

The symbols for the bound variables.

Definition at line 117 of file Quantifier.cs.

Sort [] BoundVariableSorts
get

The sorts of the bound variables.

Definition at line 134 of file Quantifier.cs.

bool IsExistential
get

Indicates whether the quantifier is existential.

Definition at line 43 of file Quantifier.cs.

bool IsUniversal
get

Indicates whether the quantifier is universal.

Definition at line 35 of file Quantifier.cs.

Pattern [] NoPatterns
get

The no-patterns.

Definition at line 92 of file Quantifier.cs.

uint NumBound
get

The number of bound variables.

Definition at line 109 of file Quantifier.cs.

uint NumNoPatterns
get

The number of no-patterns.

Definition at line 84 of file Quantifier.cs.

uint NumPatterns
get

The number of patterns.

Definition at line 59 of file Quantifier.cs.

Pattern [] Patterns
get

The patterns.

Definition at line 67 of file Quantifier.cs.

uint Weight
get

The weight of the quantifier.

Definition at line 51 of file Quantifier.cs.