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

Quantifier expressions. More...

+ Inheritance diagram for Quantifier:

Properties

bool IsUniversal [get]
 Indicates whether the quantifier is universal.
bool IsExistential [get]
 Indicates whether the quantifier is existential.
uint Weight [get]
 The weight of the quantifier.
uint NumPatterns [get]
 The number of patterns.
Pattern[] Patterns [get]
 The patterns.
uint NumNoPatterns [get]
 The number of no-patterns.
Pattern[] NoPatterns [get]
 The no-patterns.
uint NumBound [get]
 The number of bound variables.
Symbol[] BoundVariableNames [get]
 The symbols for the bound variables.
Sort[] BoundVariableSorts [get]
 The sorts of the bound variables.
BoolExpr Body [get]
 The body of the quantifier.

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.

The symbols for the bound variables.

Definition at line 117 of file Quantifier.cs.

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.

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines