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.