Package org.sosy_lab.java_smt.delegate.debugging

Class DebuggingBitvectorFormulaManager

java.lang.Object

org.sosy_lab.java_smt.delegate.debugging.DebuggingBitvectorFormulaManager

All Implemented Interfaces:

BitvectorFormulaManager

public class DebuggingBitvectorFormulaManager
extends Object
implements BitvectorFormulaManager

Constructor Summary

Constructors

Constructor	Description
DebuggingBitvectorFormulaManager(BitvectorFormulaManager pDelegate, org.sosy_lab.java_smt.delegate.debugging.DebuggingAssertions pDebugging)

Method Summary

Modifier and Type	Method	Description
BitvectorFormula	add(BitvectorFormula number1, BitvectorFormula number2)	This method returns the addition of the given bitvectors.
BitvectorFormula	and(BitvectorFormula bits1, BitvectorFormula bits2)	This method returns the bit-wise AND of the given bitvectors.
BitvectorFormula	concat(BitvectorFormula prefix, BitvectorFormula suffix)	Concatenate two bitvectors.
BooleanFormula	distinct(List<BitvectorFormula> pBits)	All given bitvectors are pairwise unequal.
BitvectorFormula	divide(BitvectorFormula numerator, BitvectorFormula denumerator, boolean signed)	This method returns the division for two bitvector formulas.
BooleanFormula	equal(BitvectorFormula number1, BitvectorFormula number2)	This method returns the bit-wise equality of the given bitvectors.
BitvectorFormula	extend(BitvectorFormula number, int extensionBits, boolean signed)	Extend a bitvector to the left (add most significant bits).
BitvectorFormula	extract(BitvectorFormula number, int msb, int lsb)	Extract a range of bits from a bitvector.
int	getLength(BitvectorFormula number)	This method returns the length of a bitvector, also denoted as bit-size.
BooleanFormula	greaterOrEquals(BitvectorFormula number1, BitvectorFormula number2, boolean signed)	Compare the given bitvectors.
BooleanFormula	greaterThan(BitvectorFormula number1, BitvectorFormula number2, boolean signed)	Compare the given bitvectors.
BooleanFormula	lessOrEquals(BitvectorFormula number1, BitvectorFormula number2, boolean signed)	Compare the given bitvectors.
BooleanFormula	lessThan(BitvectorFormula number1, BitvectorFormula number2, boolean signed)	Compare the given bitvectors.
BitvectorFormula	makeBitvector(int length, long pI)	Convert a number into a bitvector with given size.
BitvectorFormula	makeBitvector(int length, BigInteger pI)	Convert a number into a bitvector with given size.
BitvectorFormula	makeBitvector(int length, NumeralFormula.IntegerFormula pI)	Convert/Cast/Interpret a numeral formula into a bitvector with given size.
BitvectorFormula	makeVariable(int length, String pVar)	Creates a variable with exactly the given name and bitwidth.
BitvectorFormula	makeVariable(FormulaType.BitvectorType type, String pVar)
BitvectorFormula	multiply(BitvectorFormula number1, BitvectorFormula number2)	This method returns the multiplication of the given bitvectors.
BitvectorFormula	negate(BitvectorFormula number)	This method returns the negated number, i.e., it is multiplied by "-1".
BitvectorFormula	not(BitvectorFormula bits)	This method returns the bit-wise complement of the given bitvector.
BitvectorFormula	or(BitvectorFormula bits1, BitvectorFormula bits2)	This method returns the bit-wise OR of the given bitvectors.
BitvectorFormula	remainder(BitvectorFormula numerator, BitvectorFormula denumerator, boolean signed)	This method returns the remainder (modulo) for two bitvector formulas.
BitvectorFormula	rotateLeft(BitvectorFormula number, int toRotate)	This method returns a term representing the left rotation (towards most-significant bit) of number by toRotate.
BitvectorFormula	rotateLeft(BitvectorFormula number, BitvectorFormula toRotate)	This method returns a term representing the left rotation (towards most-significant bit) of number by toRotate.
BitvectorFormula	rotateRight(BitvectorFormula number, int toRotate)	This method returns a term representing the right rotation (towards least-significant bit) of number by toRotate.
BitvectorFormula	rotateRight(BitvectorFormula number, BitvectorFormula toRotate)	This method returns a term representing the right rotation (towards least-significant bit) of number by toRotate.
BitvectorFormula	shiftLeft(BitvectorFormula number, BitvectorFormula toShift)	This method returns a term representing the left shift (towards most-significant bit) of number by toShift.
BitvectorFormula	shiftRight(BitvectorFormula number, BitvectorFormula toShift, boolean signed)	This method returns a term representing the right shift (towards least-significant bit) of number by toShift.
BitvectorFormula	smodulo(BitvectorFormula numerator, BitvectorFormula denumerator)	This method returns the Signed Modular Remainder for two bitvector formulas.
BitvectorFormula	subtract(BitvectorFormula number1, BitvectorFormula number2)	This method returns the subtraction of the given bitvectors.
NumeralFormula.IntegerFormula	toIntegerFormula(BitvectorFormula pI, boolean signed)	Convert/Cast/Interpret a signed/unsigned bitvector formula as an integer formula.
BitvectorFormula	xor(BitvectorFormula bits1, BitvectorFormula bits2)	This method returns the bit-wise XOR of the given bitvectors.

Methods inherited from class java.lang.Object

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

Constructor Detail

DebuggingBitvectorFormulaManager

public DebuggingBitvectorFormulaManager(BitvectorFormulaManager pDelegate,
                                        org.sosy_lab.java_smt.delegate.debugging.DebuggingAssertions pDebugging)

Method Detail

makeBitvector

public BitvectorFormula makeBitvector(int length,
                                      long pI)

Description copied from interface: BitvectorFormulaManager

Convert a number into a bitvector with given size.

Specified by:

makeBitvector in interface BitvectorFormulaManager

makeBitvector

public BitvectorFormula makeBitvector(int length,
                                      BigInteger pI)

Description copied from interface: BitvectorFormulaManager

Convert a number into a bitvector with given size.

Specified by:

makeBitvector in interface BitvectorFormulaManager

makeBitvector

public BitvectorFormula makeBitvector(int length,
                                      NumeralFormula.IntegerFormula pI)

Description copied from interface: BitvectorFormulaManager

Convert/Cast/Interpret a numeral formula into a bitvector with given size.

If the numeral formula is too large for the given length, we cut off the largest bits and only use the lest significant bits.

Specified by:

makeBitvector in interface BitvectorFormulaManager

toIntegerFormula

public NumeralFormula.IntegerFormula toIntegerFormula(BitvectorFormula pI,
                                                      boolean signed)

Description copied from interface: BitvectorFormulaManager

Convert/Cast/Interpret a signed/unsigned bitvector formula as an integer formula.

Specified by:

toIntegerFormula in interface BitvectorFormulaManager

makeVariable

public BitvectorFormula makeVariable(int length,
                                     String pVar)

Description copied from interface: BitvectorFormulaManager

Creates a variable with exactly the given name and bitwidth.

Please make sure that the given name is valid in SMT-LIB2. Take a look at FormulaManager.isValidName(java.lang.String) for further information.

This method does not quote or unquote the given name, but uses the plain name "AS IS". Formula.toString() can return a different String than the given one.

Specified by:

makeVariable in interface BitvectorFormulaManager

makeVariable

public BitvectorFormula makeVariable(FormulaType.BitvectorType type,
                                     String pVar)

Specified by:

makeVariable in interface BitvectorFormulaManager

See Also:

BitvectorFormulaManager.makeVariable(int, String)

getLength

public int getLength(BitvectorFormula number)

Description copied from interface: BitvectorFormulaManager

This method returns the length of a bitvector, also denoted as bit-size.

Specified by:

getLength in interface BitvectorFormulaManager

negate

public BitvectorFormula negate(BitvectorFormula number)

Description copied from interface: BitvectorFormulaManager

This method returns the negated number, i.e., it is multiplied by "-1". The given number is interpreted as signed bitvector and corresponds to "2^BITSIZE - number". The result has the same length as the given number.

Specified by:

negate in interface BitvectorFormulaManager

add

public BitvectorFormula add(BitvectorFormula number1,
                            BitvectorFormula number2)

Description copied from interface: BitvectorFormulaManager

This method returns the addition of the given bitvectors. The result has the same length as the given parameters. There can be an overflow, i.e., as one would expect from bitvector logic. There is no difference in signed and unsigned numbers.

Specified by:

add in interface BitvectorFormulaManager

Parameters:

number1 - a Formula

number2 - a Formula

Returns:

number1 + number2

subtract

public BitvectorFormula subtract(BitvectorFormula number1,
                                 BitvectorFormula number2)

Description copied from interface: BitvectorFormulaManager

This method returns the subtraction of the given bitvectors. The result has the same length as the given parameters. There can be an overflow, i.e., as one would expect from bitvector logic. There is no difference in signed and unsigned numbers.

Specified by:

subtract in interface BitvectorFormulaManager

Parameters:

number1 - a Formula

number2 - a Formula

Returns:

number1 - number2

divide

public BitvectorFormula divide(BitvectorFormula numerator,
                               BitvectorFormula denumerator,
                               boolean signed)

Description copied from interface: BitvectorFormulaManager

This method returns the division for two bitvector formulas.

For signed bitvectors, the result is rounded towards zero (also called "truncated integer division", similar to the division in the C99 standard), e.g., a user can assume the following equations:

• 10 / 5 = 2
• 10 / 3 = 3
• 10 / (-3) = -3
• -10 / 5 = -2
• -10 / 3 = -3
• -10 / (-3) = 3

If the denumerator evaluates to zero (division-by-zero), either directly as value or indirectly via an additional constraint, then the result of the division is defined as:

• "-1" interpreted as bitvector (i.e., all bits set to "1"), if the numerator is non-negative, and
• "1" interpreted as bitvector (i.e., all bits set to "0", except the last bit), if the numerator is negative.

We refer to the SMTLIB standard for the division and modulo operators in BV theory.

Specified by:

divide in interface BitvectorFormulaManager

Parameters:

numerator - dividend

denumerator - divisor

signed - whether to interpret all operands as signed or as unsigned numbers.

smodulo

public BitvectorFormula smodulo(BitvectorFormula numerator,
                                BitvectorFormula denumerator)

Description copied from interface: BitvectorFormulaManager

This method returns the Signed Modular Remainder for two bitvector formulas.

The sign of the result follows the sign of the denumerator, e.g., a user can assume the following equations:

• 10 % 5 = 0
• 10 % 3 = 1
• 10 % (-3) = -2
• -10 % 5 = 0
• -10 % 3 = 2
• -10 % (-3) = -1

If the denumerator evaluates to zero (modulo-by-zero), either directly as value or indirectly via an additional constraint, then the result of the modulo operation is defined as the numerator itself. We refer to the SMTLIB standard for the division and modulo operators in BV theory.

Specified by:

smodulo in interface BitvectorFormulaManager

Parameters:

numerator - dividend

denumerator - divisor

remainder

public BitvectorFormula remainder(BitvectorFormula numerator,
                                  BitvectorFormula denumerator,
                                  boolean signed)

Description copied from interface: BitvectorFormulaManager

This method returns the remainder (modulo) for two bitvector formulas.

For signed bitvectors, the sign of the result follows the sign of the numerator, e.g., a user can assume the following equations:

• 10 % 5 = 0
• 10 % 3 = 1
• 10 % (-3) = 1
• -10 % 5 = 0
• -10 % 3 = -1
• -10 % (-3) = -1

If the denumerator evaluates to zero (modulo-by-zero), either directly as value or indirectly via an additional constraint, then the result of the modulo operation is defined as the numerator itself. We refer to the SMTLIB standard for the division and modulo operators in BV theory.

Specified by:

remainder in interface BitvectorFormulaManager

Parameters:

numerator - dividend

denumerator - divisor

signed - whether to interpret all operands as signed or as unsigned numbers.

multiply

public BitvectorFormula multiply(BitvectorFormula number1,
                                 BitvectorFormula number2)

Description copied from interface: BitvectorFormulaManager

This method returns the multiplication of the given bitvectors. The result has the same length as the given parameters. There can be an overflow, i.e., as one would expect from bitvector logic. There is no difference in signed and unsigned numbers.

Specified by:

multiply in interface BitvectorFormulaManager

Parameters:

number1 - a Formula

number2 - a Formula

Returns:

number1 - number2

equal

public BooleanFormula equal(BitvectorFormula number1,
                            BitvectorFormula number2)

Description copied from interface: BitvectorFormulaManager

This method returns the bit-wise equality of the given bitvectors.

Specified by:

equal in interface BitvectorFormulaManager

Parameters:

number1 - a Formula

number2 - a Formula

Returns:

number1 == number2

greaterThan

public BooleanFormula greaterThan(BitvectorFormula number1,
                                  BitvectorFormula number2,
                                  boolean signed)

Description copied from interface: BitvectorFormulaManager

Compare the given bitvectors.

Specified by:

greaterThan in interface BitvectorFormulaManager

Parameters:

number1 - a Formula

number2 - a Formula

signed - interpret the bitvectors as signed numbers instead of unsigned numbers

Returns:

number1 > number2

greaterOrEquals

public BooleanFormula greaterOrEquals(BitvectorFormula number1,
                                      BitvectorFormula number2,
                                      boolean signed)

Description copied from interface: BitvectorFormulaManager

Compare the given bitvectors.

Specified by:

greaterOrEquals in interface BitvectorFormulaManager

Parameters:

number1 - a Formula

number2 - a Formula

signed - interpret the bitvectors as signed numbers instead of unsigned numbers

Returns:

number1 >= number2

lessThan

public BooleanFormula lessThan(BitvectorFormula number1,
                               BitvectorFormula number2,
                               boolean signed)

Description copied from interface: BitvectorFormulaManager

Compare the given bitvectors.

Specified by:

lessThan in interface BitvectorFormulaManager

Parameters:

number1 - a Formula

number2 - a Formula

signed - interpret the bitvectors as signed numbers instead of unsigned numbers

Returns:

number1 < number2

lessOrEquals

public BooleanFormula lessOrEquals(BitvectorFormula number1,
                                   BitvectorFormula number2,
                                   boolean signed)

Description copied from interface: BitvectorFormulaManager

Compare the given bitvectors.

Specified by:

lessOrEquals in interface BitvectorFormulaManager

Parameters:

number1 - a Formula

number2 - a Formula

signed - interpret the bitvectors as signed numbers instead of unsigned numbers

Returns:

number1 <= number2

not

public BitvectorFormula not(BitvectorFormula bits)

Description copied from interface: BitvectorFormulaManager

This method returns the bit-wise complement of the given bitvector.

Specified by:

not in interface BitvectorFormulaManager

Parameters:

bits - Formula

Returns:

~bits

and

public BitvectorFormula and(BitvectorFormula bits1,
                            BitvectorFormula bits2)

Description copied from interface: BitvectorFormulaManager

This method returns the bit-wise AND of the given bitvectors.

Specified by:

and in interface BitvectorFormulaManager

Parameters:

bits1 - a Formula

bits2 - a Formula

Returns:

bits1 & bits2

or

public BitvectorFormula or(BitvectorFormula bits1,
                           BitvectorFormula bits2)

Description copied from interface: BitvectorFormulaManager

This method returns the bit-wise OR of the given bitvectors.

Specified by:

or in interface BitvectorFormulaManager

Parameters:

bits1 - a Formula

bits2 - a Formula

Returns:

bits1 | bits2

xor

public BitvectorFormula xor(BitvectorFormula bits1,
                            BitvectorFormula bits2)

Description copied from interface: BitvectorFormulaManager

This method returns the bit-wise XOR of the given bitvectors.

Specified by:

xor in interface BitvectorFormulaManager

Parameters:

bits1 - a Formula

bits2 - a Formula

Returns:

bits1 ^ bits2

shiftRight

public BitvectorFormula shiftRight(BitvectorFormula number,
                                   BitvectorFormula toShift,
                                   boolean signed)

Description copied from interface: BitvectorFormulaManager

This method returns a term representing the right shift (towards least-significant bit) of number by toShift. The result has the same length as the given number. On the left side, we fill up the most significant bits with ones (i.e., arithmetic shift), if the number is signed and negative, else we fill up with zeroes. For "toShift >= bitsize", we return a bitvector with value zero, if number was zero or positive, or all bits set to one, if negative.

Specified by:

shiftRight in interface BitvectorFormulaManager

shiftLeft

public BitvectorFormula shiftLeft(BitvectorFormula number,
                                  BitvectorFormula toShift)

Description copied from interface: BitvectorFormulaManager

This method returns a term representing the left shift (towards most-significant bit) of number by toShift. The result has the same length as the given number. On the right side, we fill up the least significant bits with zeroes. For "toShift >= bitsize", we return a bitvector with value zero.

Specified by:

shiftLeft in interface BitvectorFormulaManager

rotateLeft

public BitvectorFormula rotateLeft(BitvectorFormula number,
                                   int toRotate)

Description copied from interface: BitvectorFormulaManager

This method returns a term representing the left rotation (towards most-significant bit) of number by toRotate. The result has the same length as the given number. For "toRotate % bitsize == 0", we return the number itself.

Specified by:

rotateLeft in interface BitvectorFormulaManager

toRotate - the number of bits to be moved

rotateLeft

public BitvectorFormula rotateLeft(BitvectorFormula number,
                                   BitvectorFormula toRotate)

Description copied from interface: BitvectorFormulaManager

This method returns a term representing the left rotation (towards most-significant bit) of number by toRotate. The result has the same length as the given number. For "toRotate % bitsize == 0", we return the number itself.

Specified by:

rotateLeft in interface BitvectorFormulaManager

toRotate - unsigned bitvector, represents the number of bits to be moved

rotateRight

public BitvectorFormula rotateRight(BitvectorFormula number,
                                    int toRotate)

Description copied from interface: BitvectorFormulaManager

This method returns a term representing the right rotation (towards least-significant bit) of number by toRotate. The result has the same length as the given number. For "toRotate % bitsize == 0", we return the number itself.

Specified by:

rotateRight in interface BitvectorFormulaManager

toRotate - the number of bits to be moved

rotateRight

public BitvectorFormula rotateRight(BitvectorFormula number,
                                    BitvectorFormula toRotate)

Description copied from interface: BitvectorFormulaManager

This method returns a term representing the right rotation (towards least-significant bit) of number by toRotate. The result has the same length as the given number. For "toRotate % bitsize == 0", we return the number itself.

Specified by:

rotateRight in interface BitvectorFormulaManager

toRotate - unsigned bitvector, represents the number of bits to be moved

concat

public BitvectorFormula concat(BitvectorFormula prefix,
                               BitvectorFormula suffix)

Description copied from interface: BitvectorFormulaManager

Concatenate two bitvectors.

Specified by:

concat in interface BitvectorFormulaManager

extract

public BitvectorFormula extract(BitvectorFormula number,
                                int msb,
                                int lsb)

Description copied from interface: BitvectorFormulaManager

Extract a range of bits from a bitvector. We require 0 <= lsb <= msb < bitsize.

If msb equals lsb, then a single bit will be returned, i.e., the bit from the given position. If lsb equals 0 and msb equals bitsize-1, then the complete bitvector will be returned.

Specified by:

extract in interface BitvectorFormulaManager

Parameters:

number - from where the bits are extracted.

msb - Upper index for the most significant bit. Must be in interval from lsb to bitsize-1.

lsb - Lower index for the least significant bit. Must be in interval from 0 to msb.

extend

public BitvectorFormula extend(BitvectorFormula number,
                               int extensionBits,
                               boolean signed)

Description copied from interface: BitvectorFormulaManager

Extend a bitvector to the left (add most significant bits). If signed is set and the given number is negative, then the bit "1" will be added several times, else "0".

Specified by:

extend in interface BitvectorFormulaManager

Parameters:

number - The bitvector to extend.

extensionBits - How many bits to add.

signed - Whether the extension should depend on the sign bit.

distinct

public BooleanFormula distinct(List<BitvectorFormula> pBits)

Description copied from interface: BitvectorFormulaManager

All given bitvectors are pairwise unequal.

Specified by:

distinct in interface BitvectorFormulaManager