de.uni_freiburg.informatik.ultimate.logic

Class ConstantTerm

java.lang.Object

de.uni_freiburg.informatik.ultimate.logic.Term

de.uni_freiburg.informatik.ultimate.logic.ConstantTerm

public class ConstantTerm
extends Term

A term representing constants. The Java-type of the constant depends on the SMTLIB-type and the origin of the term. If this term has numeral sort and stems from model evaluation, the Java-type of the constant will be Rational. If it comes from user input it typically is BigInteger for numerals or BigDecimal for decimals (note that you can also use Rational with the API, but the parser won't do that). A constant term is created by the Script.numeral(java.math.BigInteger), Script.decimal(BigDecimal), Script.binary(String), Script.hexadecimal(String), and Script.string(String). Also Rational.toTerm(Sort) creates a constant term.

Author:

hoenicke, Juergen Christ

Field Summary

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

mTmpCtr

Method Summary

Modifier and Type	Method and Description
Sort	getSort() Returns the SMTLIB sort of this term.
java.lang.Object	getValue() Gets the constant value.
static int	hashConstant(java.lang.Object value, Sort sort)
java.lang.String	toString() Prints an SMTLIB representation of this term.
java.lang.String	toStringDirect() Prints the canonical SMTLIB representation of this term.
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, hashCode

Methods inherited from class java.lang.Object

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

Method Detail

getValue

public java.lang.Object getValue()

Gets the constant value. If this term has numeral sort and stems from model evaluation, the Java-type of the constant will be Rational. If it comes from user input it typically is BigInteger for numerals or BigDecimal for decimals (note that you can also use Rational with the API, but the parser won't do that). For string literals this is a QuotedObject containing a string. Bit vector constants are represented by BigInteger.

Returns:

the value.

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.

toString

public java.lang.String toString()

Description copied from class: Term

Prints an SMTLIB representation of this term. This introduces lets for common subexpressions to prevent exponential blow-up when printing a term with lots of sharing.

Overrides:

toString in class Term

Returns:

an SMTLIB representation.

toStringDirect

public java.lang.String toStringDirect()

Description copied from class: Term

Prints the canonical SMTLIB representation of this term. This does not eliminate common sub-expressions and can cause exponential blow-up.

Overrides:

toStringDirect in class Term

Returns:

the canonical SMTLIB representation.

hashConstant

public static final int hashConstant(java.lang.Object value,
                                     Sort sort)

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