Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
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.
 

Additional Inherited Members

- Public Member Functions inherited from Expr
Expr Simplify (Params p=null)
 Returns a simplified version of the expression.
 
void Update (Expr[] args)
 Update the arguments of the expression using the arguments args The number of new arguments should coincide with the current number of arguments.
 
Expr Substitute (Expr[] from, Expr[] to)
 Substitute every occurrence of from[i] in the expression with to[i], for i smaller than num_exprs.
 
Expr Substitute (Expr from, Expr to)
 Substitute every occurrence of from in the expression with to.
 
Expr SubstituteVars (Expr[] to)
 Substitute the free variables in the expression with the expressions in to
 
new Expr Translate (Context ctx)
 Translates (copies) the term to the Context ctx .
 
override string ToString ()
 Returns a string representation of the expression.
 
- Static Public Member Functions inherited from AST
static bool operator== (AST a, AST b)
 Comparison operator.
 
static bool operator!= (AST a, AST b)
 Comparison operator.
 
- Protected Member Functions inherited from BoolExpr
 BoolExpr (Context ctx)
 Constructor for BoolExpr
 

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.