Package io.github.cvc5

Class Op

java.lang.Object

io.github.cvc5.Op

public class Op
extends java.lang.Object

A cvc5 operator. An operator is a term that represents certain operators, instantiated with its required parameters, e.g., a Term of kind Kind.BITVECTOR_EXTRACT.

Field Summary

Fields

Modifier and Type	Field	Description
protected long	pointer
protected Solver	solver

Method Summary

Modifier and Type	Method	Description
protected void	deletePointer(long pointer)
boolean	equals(java.lang.Object t)	Syntactic equality operator.
Term	get(int i)	Get the index at position i.
Kind	getKind()
int	getNumIndices()
long	getPointer()
Solver	getSolver()
boolean	isIndexed()
boolean	isNull()
java.lang.String	toString()
protected java.lang.String	toString(long pointer)

Methods inherited from class java.lang.Object

clone, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

solver

protected final Solver solver

pointer

protected long pointer

Method Detail

deletePointer

protected void deletePointer(long pointer)

getPointer

public long getPointer()

equals

public boolean equals(java.lang.Object t)

Syntactic equality operator.

Overrides:

equals in class java.lang.Object

Parameters:

t - The operator to compare to for equality.

Returns:

True if the operators are syntactically identical.

Note:

Both operators must belong to the same solver object.

getKind

public Kind getKind()

Returns:

The kind of this operator.

isNull

public boolean isNull()

Returns:

True if this operator is a null term.

isIndexed

public boolean isIndexed()

Returns:

True iff this operator is indexed.

getNumIndices

public int getNumIndices()

Returns:

The number of indices of this op.

get

public Term get(int i)
         throws CVC5ApiException

Get the index at position i.

Parameters:

i - The position of the index to return.

Returns:

The index at position i.

Throws:

CVC5ApiException

toString

protected java.lang.String toString(long pointer)

Returns:

A string representation of this operator.

getSolver

public Solver getSolver()

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object