de.uni_freiburg.informatik.ultimate.logic

Class QuantifiedFormula

java.lang.Object

de.uni_freiburg.informatik.ultimate.logic.Term

de.uni_freiburg.informatik.ultimate.logic.QuantifiedFormula

public class QuantifiedFormula
extends Term

Represents a quantified formula in SMTLIB 2. This class represents the SMTLIB 2 construct

 (forall ((var_1 sort_1) ... (var_n sort_n)) ...)
 

or

 (exists ((var_1 sort_1) ... (var_n sort_n)) ...)
 

. A quantified formula is created by Script.quantifier(int, TermVariable[], Term, Term[][]).

Author:

hoenicke

Field Summary

Fields

Modifier and Type	Field and Description
static int	EXISTS
static int	FORALL

Fields inherited from class de.uni_freiburg.informatik.ultimate.logic.Term

mTmpCtr

Method Summary

Modifier and Type	Method and Description
int	getQuantifier()
Sort	getSort() Returns the SMTLIB sort of this term.
Term	getSubformula() Get the formula under the quantifier.
TermVariable[]	getVariables() Get the quantified variables.
int	hashCode()
static int	hashQuantifier(int quant, TermVariable[] vars, Term f)
void	toStringHelper(java.util.ArrayDeque<java.lang.Object> mTodo) Convert a term to a string in a stack based fashion.

Methods inherited from class de.uni_freiburg.informatik.ultimate.logic.Term

getFreeVars, getTheory, toString, toStringDirect

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

EXISTS

public static final int EXISTS

See Also:

Constant Field Values

FORALL

public static final int FORALL

See Also:

Constant Field Values

Method Detail

getQuantifier

public int getQuantifier()

Returns:

the quantifier

getVariables

public TermVariable[] getVariables()

Get the quantified variables.

Returns:

the variables

getSubformula

public Term getSubformula()

Get the formula under the quantifier.

Returns:

the sub-formula.

getSort

public Sort getSort()

Description copied from class: Term

Returns the SMTLIB sort of this term.

Specified by:

getSort in class Term

Returns:

the sort of the term.

hashCode

public int hashCode()

Overrides:

hashCode in class Term

hashQuantifier

public static final int hashQuantifier(int quant,
                                       TermVariable[] vars,
                                       Term f)

toStringHelper

public void toStringHelper(java.util.ArrayDeque<java.lang.Object> mTodo)

Description copied from class: Term

Convert a term to a string in a stack based fashion. This is used for internal purposes. External users can just use toString() or toStringDirect().

Specified by:

toStringHelper in class Term

Parameters:

mTodo - The stack where to put the strings and sub terms.

See Also:

PrintTerm