java.lang.Object
- org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>

All Implemented Interfaces:: BitvectorFormulaManager

public abstract class AbstractBitvectorFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>
extends Object
implements BitvectorFormulaManager

Field Summary

Fields
Modifier and Type Field Description

protected FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> formulaCreator

Constructor Summary

Constructors
Modifier	Constructor	Description
`protected`	`AbstractBitvectorFormulaManager(FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> pCreator, AbstractBooleanFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> pBmgr)`

Method Summary

All Methods Instance Methods Abstract Methods Concrete Methods
Modifier and Type	Method	Description
`BitvectorFormula`	`add(BitvectorFormula pNumber1, BitvectorFormula pNumber2)`	This method returns the addition of the given bitvectors.
`protected abstract TFormulaInfo`	`add(TFormulaInfo pParam1, TFormulaInfo pParam2)`
`BitvectorFormula`	`and(BitvectorFormula pBits1, BitvectorFormula pBits2)`	This method returns the bit-wise AND of the given bitvectors.
`protected abstract TFormulaInfo`	`and(TFormulaInfo pParam1, TFormulaInfo pParam2)`
`BitvectorFormula`	`concat(BitvectorFormula pNumber, BitvectorFormula pAppend)`	Concatenate two bitvectors.
`protected abstract TFormulaInfo`	`concat(TFormulaInfo number, TFormulaInfo pAppend)`
`BooleanFormula`	`distinct(List<BitvectorFormula> pBits)`	All given bitvectors are pairwise unequal.
`protected TFormulaInfo`	`distinctImpl(List<TFormulaInfo> pBits)`
`BitvectorFormula`	`divide(BitvectorFormula pNumber1, BitvectorFormula pNumber2, boolean signed)`	This method returns the division for two bitvector formulas.
`protected abstract TFormulaInfo`	`divide(TFormulaInfo pParam1, TFormulaInfo pParam2, boolean signed)`
`BooleanFormula`	`equal(BitvectorFormula pNumber1, BitvectorFormula pNumber2)`	This method returns the bit-wise equality of the given bitvectors.
`protected abstract TFormulaInfo`	`equal(TFormulaInfo pParam1, TFormulaInfo pParam2)`
`BitvectorFormula`	`extend(BitvectorFormula pNumber, int pExtensionBits, boolean pSigned)`	Extend a bitvector to the left (add most significant bits).
`protected abstract TFormulaInfo`	`extend(TFormulaInfo pNumber, int pExtensionBits, boolean pSigned)`
`BitvectorFormula`	`extract(BitvectorFormula pNumber, int pMsb, int pLsb)`	Extract a range of bits from a bitvector.
`protected abstract TFormulaInfo`	`extract(TFormulaInfo pNumber, int pMsb, int pLsb)`
`protected TFormulaInfo`	`extractInfo(Formula pBits)`
`protected FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl>`	`getFormulaCreator()`
`int`	`getLength(BitvectorFormula pNumber)`	This method returns the length of a bitvector, also denoted as bit-size.
`BooleanFormula`	`greaterOrEquals(BitvectorFormula pNumber1, BitvectorFormula pNumber2, boolean signed)`	Compare the given bitvectors.
`protected abstract TFormulaInfo`	`greaterOrEquals(TFormulaInfo pParam1, TFormulaInfo pParam2, boolean signed)`
`BooleanFormula`	`greaterThan(BitvectorFormula pNumber1, BitvectorFormula pNumber2, boolean signed)`	Compare the given bitvectors.
`protected abstract TFormulaInfo`	`greaterThan(TFormulaInfo pParam1, TFormulaInfo pParam2, boolean signed)`
`BooleanFormula`	`lessOrEquals(BitvectorFormula pNumber1, BitvectorFormula pNumber2, boolean signed)`	Compare the given bitvectors.
`protected abstract TFormulaInfo`	`lessOrEquals(TFormulaInfo pParam1, TFormulaInfo pParam2, boolean signed)`
`BooleanFormula`	`lessThan(BitvectorFormula pNumber1, BitvectorFormula pNumber2, boolean signed)`	Compare the given bitvectors.
`protected abstract TFormulaInfo`	`lessThan(TFormulaInfo pParam1, TFormulaInfo pParam2, boolean signed)`
`BitvectorFormula`	`makeBitvector(int pLength, long i)`	Convert a number into a bitvector with given size.
`BitvectorFormula`	`makeBitvector(int pLength, BigInteger i)`	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.
`protected TFormulaInfo`	`makeBitvectorImpl(int pLength, long pI)`
`protected abstract TFormulaInfo`	`makeBitvectorImpl(int pLength, BigInteger pI)`
`protected abstract TFormulaInfo`	`makeBitvectorImpl(int length, TFormulaInfo pParam1)`
`BitvectorFormula`	`makeVariable(int pLength, String pVar)`	Creates a variable with exactly the given name and bitwidth.
`BitvectorFormula`	`makeVariable(FormulaType.BitvectorType type, String pVar)`
`protected abstract TFormulaInfo`	`makeVariableImpl(int pLength, String pVar)`
`BitvectorFormula`	`multiply(BitvectorFormula pNumber1, BitvectorFormula pNumber2)`	This method returns the multiplication of the given bitvectors.
`protected abstract TFormulaInfo`	`multiply(TFormulaInfo pParam1, TFormulaInfo pParam2)`
`BitvectorFormula`	`negate(BitvectorFormula pNumber)`	This method returns the negated number, i.e., it is multiplied by "-1".
`protected abstract TFormulaInfo`	`negate(TFormulaInfo pParam1)`
`BitvectorFormula`	`not(BitvectorFormula pBits)`	This method returns the bit-wise complement of the given bitvector.
`protected abstract TFormulaInfo`	`not(TFormulaInfo pParam1)`
`BitvectorFormula`	`or(BitvectorFormula pBits1, BitvectorFormula pBits2)`	This method returns the bit-wise OR of the given bitvectors.
`protected abstract TFormulaInfo`	`or(TFormulaInfo pParam1, TFormulaInfo pParam2)`
`BitvectorFormula`	`remainder(BitvectorFormula pNumber1, BitvectorFormula pNumber2, boolean signed)`	This method returns the remainder (remainder(dividend, divisor) == remainder) for the Euclidean division (dividend = quotient * divisor + remainder) of two bitvector formulas.
`protected abstract TFormulaInfo`	`remainder(TFormulaInfo pParam1, TFormulaInfo pParam2, boolean signed)`
`BitvectorFormula`	`rotateLeft(BitvectorFormula pNumber, int pToRotate)`	This method returns a term representing the left rotation (towards most-significant bit) of number by toRotate.
`BitvectorFormula`	`rotateLeft(BitvectorFormula pNumber, BitvectorFormula pToRotate)`	This method returns a term representing the left rotation (towards most-significant bit) of number by toRotate.
`protected TFormulaInfo`	`rotateLeft(TFormulaInfo pNumber, TFormulaInfo pToRotate)`
`protected TFormulaInfo`	`rotateLeftByConstant(TFormulaInfo pNumber, int pToRotate)`
`BitvectorFormula`	`rotateRight(BitvectorFormula pNumber, int pToRotate)`	This method returns a term representing the right rotation (towards least-significant bit) of number by toRotate.
`BitvectorFormula`	`rotateRight(BitvectorFormula pNumber, BitvectorFormula pToRotate)`	This method returns a term representing the right rotation (towards least-significant bit) of number by toRotate.
`protected TFormulaInfo`	`rotateRight(TFormulaInfo pNumber, TFormulaInfo pToRotate)`
`protected TFormulaInfo`	`rotateRightByConstant(TFormulaInfo pNumber, int pToRotate)`
`BitvectorFormula`	`shiftLeft(BitvectorFormula pNumber, BitvectorFormula toShift)`	This method returns a term representing the left shift (towards most-significant bit) of number by toShift.
`protected abstract TFormulaInfo`	`shiftLeft(TFormulaInfo pNumber, TFormulaInfo pToShift)`
`BitvectorFormula`	`shiftRight(BitvectorFormula pNumber, BitvectorFormula pToShift, boolean signed)`	Return a term representing the (arithmetic if signed is true) right shift of number by toShift.
`protected abstract TFormulaInfo`	`shiftRight(TFormulaInfo pNumber, TFormulaInfo toShift, boolean signed)`
`BitvectorFormula`	`smodulo(BitvectorFormula pNumber1, BitvectorFormula pNumber2)`	This method returns the two complement signed remainder (smodulo(dividend, divisor) == remainder) for the Euclidean division (dividend = quotient * divisor + remainder) of two bitvector formulas, with the sign of the remainder following the sign of the divisor.
`protected abstract TFormulaInfo`	`smodulo(TFormulaInfo pParam1, TFormulaInfo pParam2)`
`BitvectorFormula`	`subtract(BitvectorFormula pNumber1, BitvectorFormula pNumber2)`	This method returns the subtraction of the given bitvectors.
`protected abstract TFormulaInfo`	`subtract(TFormulaInfo pParam1, TFormulaInfo pParam2)`
`NumeralFormula.IntegerFormula`	`toIntegerFormula(BitvectorFormula pI, boolean signed)`	Convert/Cast/Interpret a signed/unsigned bitvector formula as an integer formula.
`protected abstract TFormulaInfo`	`toIntegerFormulaImpl(TFormulaInfo pI, boolean signed)`
`protected TType`	`toSolverType(FormulaType<?> formulaType)`
`protected BigInteger`	`transformValueToRange(int pLength, BigInteger pI)`	transform a negative value into its positive counterpart.
`BitvectorFormula`	`xor(BitvectorFormula pBits1, BitvectorFormula pBits2)`	This method returns the bit-wise XOR of the given bitvectors.
`protected abstract TFormulaInfo`	`xor(TFormulaInfo pParam1, TFormulaInfo pParam2)`

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface org.sosy_lab.java_smt.api.BitvectorFormulaManager
extract, modulo

- Field Detail
  - formulaCreator
```
protected final FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> formulaCreator
```
- Constructor Detail
  - AbstractBitvectorFormulaManager
```
protected AbstractBitvectorFormulaManager(FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> pCreator,
                                          AbstractBooleanFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl> pBmgr)
```
- Method Detail
  - 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 least significant bits.
    
    Specified by:
    
    makeBitvector in interface BitvectorFormulaManager
  - makeBitvectorImpl
```
protected abstract TFormulaInfo makeBitvectorImpl(int length,
                                                  TFormulaInfo pParam1)
```
  - 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
  - toIntegerFormulaImpl
```
protected abstract TFormulaInfo toIntegerFormulaImpl(TFormulaInfo pI,
                                                     boolean signed)
```
  - negate
```
public BitvectorFormula negate(BitvectorFormula pNumber)
```
    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
  - negate
```
protected abstract TFormulaInfo negate(TFormulaInfo pParam1)
```
  - add
```
public BitvectorFormula add(BitvectorFormula pNumber1,
                            BitvectorFormula pNumber2)
```
    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:
    
    pNumber1 - a Formula
    
    pNumber2 - a Formula
    
    Returns:
    
    number1 + number2
  - add
```
protected abstract TFormulaInfo add(TFormulaInfo pParam1,
                                    TFormulaInfo pParam2)
```
  - subtract
```
public BitvectorFormula subtract(BitvectorFormula pNumber1,
                                 BitvectorFormula pNumber2)
```
    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:
    
    pNumber1 - a Formula
    
    pNumber2 - a Formula
    
    Returns:
    
    number1 - number2
  - subtract
```
protected abstract TFormulaInfo subtract(TFormulaInfo pParam1,
                                         TFormulaInfo pParam2)
```
  - divide
```
public BitvectorFormula divide(BitvectorFormula pNumber1,
                               BitvectorFormula pNumber2,
                               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 divisor 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 dividend is non-negative, and
    "1" interpreted as bitvector (i.e., all bits set to "0", except the last bit), if the dividend is negative.
    
    We refer to the SMTLIB standard version 2.6 for the division operator in BV theory for additional information.
    Specified by:
    
    divide in interface BitvectorFormulaManager
    
    Parameters:
    
    pNumber1 - dividend of the operation.
    
    pNumber2 - divisor of the operation.
    
    signed - whether to interpret all operands as signed or as unsigned numbers.
  - divide
```
protected abstract TFormulaInfo divide(TFormulaInfo pParam1,
                                       TFormulaInfo pParam2,
                                       boolean signed)
```
  - remainder
```
public BitvectorFormula remainder(BitvectorFormula pNumber1,
                                  BitvectorFormula pNumber2,
                                  boolean signed)
```
    Description copied from interface: BitvectorFormulaManager
    This method returns the remainder (remainder(dividend, divisor) == remainder) for the Euclidean division (dividend = quotient * divisor + remainder) of two bitvector formulas.
    For unsigned bitvectors, this returns the remainder of unsigned bitvector division.
    For signed bitvectors, the sign of the result follows the sign of the dividend, i.e. the quotient of the division is rounded in such a way that the sign of the result of the remainder operation follows the sign of the dividend. A user can assume the following example equations, with bitvectors interpreted as signed decimal numbers, to hold:
    
    remainder(10, 5, true) == 0
    remainder(10, 3, true) == 1
    remainder(10, -3, true) == 1
    remainder(-10, 5, true) == 0
    remainder(-10, 3, true) == -1
    remainder(-10, -3, true) == -1
    
    If the divisor 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 dividend itself. We refer to the SMTLIB standard version 2.6 for the division and remainder operators in BV theory.
    We refer to the SMTLIB standard version 2.6 for the remainder operator in BV theory for additional information.
    Specified by:
    
    remainder in interface BitvectorFormulaManager
    
    Parameters:
    
    pNumber1 - dividend of the operation. The sign bit is carried over from this bitvector for signed operations.
    
    pNumber2 - divisor of the operation.
    
    signed - whether to interpret all operands as signed or as unsigned numbers.
  - remainder
```
protected abstract TFormulaInfo remainder(TFormulaInfo pParam1,
                                          TFormulaInfo pParam2,
                                          boolean signed)
```
  - smodulo
```
public BitvectorFormula smodulo(BitvectorFormula pNumber1,
                                BitvectorFormula pNumber2)
```
    Description copied from interface: BitvectorFormulaManager
    This method returns the two complement signed remainder (smodulo(dividend, divisor) == remainder) for the Euclidean division (dividend = quotient * divisor + remainder) of two bitvector formulas, with the sign of the remainder following the sign of the divisor.
    The sign of the result follows the sign of the divisor; i.e. the quotient calculated in the modulo operation is rounded in such a way that the result of the smodulo operation follows the sign of the divisor. A user can assume the following example equations, with bitvectors interpreted as signed decimal numbers, to hold:
    
    smodulo(10, 5) == 0
    smodulo(10, 3) == 1
    smodulo(10, -3) == -2
    smodulo(-10, 5) == 0
    smodulo(-10, 3) == 2
    smodulo(-10, -3) == -1
    
    If the divisor 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 dividend itself. We refer to the SMTLIB standard version 2.6 for the division and remainder operators in BV theory.
    For unsigned modulo, we refer to the unsigned remainder method BitvectorFormulaManager.remainder(BitvectorFormula, BitvectorFormula, boolean).
    We refer to the SMTLIB standard version 2.6 for the smodulo operator in BV theory for additional information.
    Specified by:
    
    smodulo in interface BitvectorFormulaManager
    
    Parameters:
    
    pNumber1 - dividend of the operation.
    
    pNumber2 - divisor of the operation.
  - smodulo
```
protected abstract TFormulaInfo smodulo(TFormulaInfo pParam1,
                                        TFormulaInfo pParam2)
```
  - multiply
```
public BitvectorFormula multiply(BitvectorFormula pNumber1,
                                 BitvectorFormula pNumber2)
```
    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:
    
    pNumber1 - a Formula
    
    pNumber2 - a Formula
    
    Returns:
    
    number1 - number2
  - multiply
```
protected abstract TFormulaInfo multiply(TFormulaInfo pParam1,
                                         TFormulaInfo pParam2)
```
  - equal
```
public BooleanFormula equal(BitvectorFormula pNumber1,
                            BitvectorFormula pNumber2)
```
    Description copied from interface: BitvectorFormulaManager
    
    This method returns the bit-wise equality of the given bitvectors.
    
    Specified by:
    
    equal in interface BitvectorFormulaManager
    
    Parameters:
    
    pNumber1 - a Formula
    
    pNumber2 - a Formula
    
    Returns:
    
    number1 == number2
  - equal
```
protected abstract TFormulaInfo equal(TFormulaInfo pParam1,
                                      TFormulaInfo pParam2)
```
  - greaterThan
```
public BooleanFormula greaterThan(BitvectorFormula pNumber1,
                                  BitvectorFormula pNumber2,
                                  boolean signed)
```
    Description copied from interface: BitvectorFormulaManager
    
    Compare the given bitvectors.
    
    Specified by:
    
    greaterThan in interface BitvectorFormulaManager
    
    Parameters:
    
    pNumber1 - a Formula
    
    pNumber2 - a Formula
    
    signed - interpret the bitvectors as signed numbers instead of unsigned numbers
    
    Returns:
    
    number1 > number2
  - greaterThan
```
protected abstract TFormulaInfo greaterThan(TFormulaInfo pParam1,
                                            TFormulaInfo pParam2,
                                            boolean signed)
```
  - greaterOrEquals
```
public BooleanFormula greaterOrEquals(BitvectorFormula pNumber1,
                                      BitvectorFormula pNumber2,
                                      boolean signed)
```
    Description copied from interface: BitvectorFormulaManager
    
    Compare the given bitvectors.
    
    Specified by:
    
    greaterOrEquals in interface BitvectorFormulaManager
    
    Parameters:
    
    pNumber1 - a Formula
    
    pNumber2 - a Formula
    
    signed - interpret the bitvectors as signed numbers instead of unsigned numbers
    
    Returns:
    
    number1 >= number2
  - greaterOrEquals
```
protected abstract TFormulaInfo greaterOrEquals(TFormulaInfo pParam1,
                                                TFormulaInfo pParam2,
                                                boolean signed)
```
  - lessThan
```
public BooleanFormula lessThan(BitvectorFormula pNumber1,
                               BitvectorFormula pNumber2,
                               boolean signed)
```
    Description copied from interface: BitvectorFormulaManager
    
    Compare the given bitvectors.
    
    Specified by:
    
    lessThan in interface BitvectorFormulaManager
    
    Parameters:
    
    pNumber1 - a Formula
    
    pNumber2 - a Formula
    
    signed - interpret the bitvectors as signed numbers instead of unsigned numbers
    
    Returns:
    
    number1 < number2
  - lessThan
```
protected abstract TFormulaInfo lessThan(TFormulaInfo pParam1,
                                         TFormulaInfo pParam2,
                                         boolean signed)
```
  - lessOrEquals
```
public BooleanFormula lessOrEquals(BitvectorFormula pNumber1,
                                   BitvectorFormula pNumber2,
                                   boolean signed)
```
    Description copied from interface: BitvectorFormulaManager
    
    Compare the given bitvectors.
    
    Specified by:
    
    lessOrEquals in interface BitvectorFormulaManager
    
    Parameters:
    
    pNumber1 - a Formula
    
    pNumber2 - a Formula
    
    signed - interpret the bitvectors as signed numbers instead of unsigned numbers
    
    Returns:
    
    number1 <= number2
  - lessOrEquals
```
protected abstract TFormulaInfo lessOrEquals(TFormulaInfo pParam1,
                                             TFormulaInfo pParam2,
                                             boolean signed)
```
  - not
```
public BitvectorFormula not(BitvectorFormula pBits)
```
    Description copied from interface: BitvectorFormulaManager
    
    This method returns the bit-wise complement of the given bitvector.
    
    Specified by:
    
    not in interface BitvectorFormulaManager
    
    Parameters:
    
    pBits - Formula
    
    Returns:
    
    ~bits
  - not
```
protected abstract TFormulaInfo not(TFormulaInfo pParam1)
```
  - and
```
public BitvectorFormula and(BitvectorFormula pBits1,
                            BitvectorFormula pBits2)
```
    Description copied from interface: BitvectorFormulaManager
    
    This method returns the bit-wise AND of the given bitvectors.
    
    Specified by:
    
    and in interface BitvectorFormulaManager
    
    Parameters:
    
    pBits1 - a Formula
    
    pBits2 - a Formula
    
    Returns:
    
    bits1 & bits2
  - and
```
protected abstract TFormulaInfo and(TFormulaInfo pParam1,
                                    TFormulaInfo pParam2)
```
  - or
```
public BitvectorFormula or(BitvectorFormula pBits1,
                           BitvectorFormula pBits2)
```
    Description copied from interface: BitvectorFormulaManager
    
    This method returns the bit-wise OR of the given bitvectors.
    
    Specified by:
    
    or in interface BitvectorFormulaManager
    
    Parameters:
    
    pBits1 - a Formula
    
    pBits2 - a Formula
    
    Returns:
    
    bits1 | bits2
  - or
```
protected abstract TFormulaInfo or(TFormulaInfo pParam1,
                                   TFormulaInfo pParam2)
```
  - xor
```
public BitvectorFormula xor(BitvectorFormula pBits1,
                            BitvectorFormula pBits2)
```
    Description copied from interface: BitvectorFormulaManager
    
    This method returns the bit-wise XOR of the given bitvectors.
    
    Specified by:
    
    xor in interface BitvectorFormulaManager
    
    Parameters:
    
    pBits1 - a Formula
    
    pBits2 - a Formula
    
    Returns:
    
    bits1 ^ bits2
  - xor
```
protected abstract TFormulaInfo xor(TFormulaInfo pParam1,
                                    TFormulaInfo pParam2)
```
  - makeBitvector
```
public BitvectorFormula makeBitvector(int pLength,
                                      long i)
```
    Description copied from interface: BitvectorFormulaManager
    
    Convert a number into a bitvector with given size.
    
    Specified by:
    
    makeBitvector in interface BitvectorFormulaManager
  - makeBitvectorImpl
```
protected TFormulaInfo makeBitvectorImpl(int pLength,
                                         long pI)
```
  - makeBitvector
```
public BitvectorFormula makeBitvector(int pLength,
                                      BigInteger i)
```
    Description copied from interface: BitvectorFormulaManager
    
    Convert a number into a bitvector with given size.
    
    Specified by:
    
    makeBitvector in interface BitvectorFormulaManager
  - makeBitvectorImpl
```
protected abstract TFormulaInfo makeBitvectorImpl(int pLength,
                                                  BigInteger pI)
```
  - transformValueToRange
```
protected final BigInteger transformValueToRange(int pLength,
                                                 BigInteger pI)
```
    transform a negative value into its positive counterpart.
    
    Throws:
    
    IllegalArgumentException - if the value is out of range for the given size.
  - makeVariable
```
public BitvectorFormula makeVariable(FormulaType.BitvectorType type,
                                     String pVar)
```
    Specified by:
    
    makeVariable in interface BitvectorFormulaManager
    
    See Also:
    
    BitvectorFormulaManager.makeVariable(int, String)
  - makeVariable
```
public BitvectorFormula makeVariable(int pLength,
                                     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
  - makeVariableImpl
```
protected abstract TFormulaInfo makeVariableImpl(int pLength,
                                                 String pVar)
```
  - shiftRight
```
public BitvectorFormula shiftRight(BitvectorFormula pNumber,
                                   BitvectorFormula pToShift,
                                   boolean signed)
```
    Return a term representing the (arithmetic if signed is true) right shift of number by toShift.
    
    Specified by:
    
    shiftRight in interface BitvectorFormulaManager
  - shiftRight
```
protected abstract TFormulaInfo shiftRight(TFormulaInfo pNumber,
                                           TFormulaInfo toShift,
                                           boolean signed)
```
  - shiftLeft
```
public BitvectorFormula shiftLeft(BitvectorFormula pNumber,
                                  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
  - shiftLeft
```
protected abstract TFormulaInfo shiftLeft(TFormulaInfo pNumber,
                                          TFormulaInfo pToShift)
```
  - rotateLeft
```
public BitvectorFormula rotateLeft(BitvectorFormula pNumber,
                                   int pToRotate)
```
    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
    
    pToRotate - the number of bits to be moved
  - rotateLeftByConstant
```
protected TFormulaInfo rotateLeftByConstant(TFormulaInfo pNumber,
                                            int pToRotate)
```
  - rotateLeft
```
public BitvectorFormula rotateLeft(BitvectorFormula pNumber,
                                   BitvectorFormula pToRotate)
```
    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
    
    pToRotate - unsigned bitvector, represents the number of bits to be moved
  - rotateLeft
```
protected TFormulaInfo rotateLeft(TFormulaInfo pNumber,
                                  TFormulaInfo pToRotate)
```
  - rotateRight
```
public BitvectorFormula rotateRight(BitvectorFormula pNumber,
                                    int pToRotate)
```
    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
    
    pToRotate - the number of bits to be moved
  - rotateRightByConstant
```
protected TFormulaInfo rotateRightByConstant(TFormulaInfo pNumber,
                                             int pToRotate)
```
  - rotateRight
```
public BitvectorFormula rotateRight(BitvectorFormula pNumber,
                                    BitvectorFormula pToRotate)
```
    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
    
    pToRotate - unsigned bitvector, represents the number of bits to be moved
  - rotateRight
```
protected TFormulaInfo rotateRight(TFormulaInfo pNumber,
                                   TFormulaInfo pToRotate)
```
  - concat
```
public final BitvectorFormula concat(BitvectorFormula pNumber,
                                     BitvectorFormula pAppend)
```
    Description copied from interface: BitvectorFormulaManager
    
    Concatenate two bitvectors.
    
    Specified by:
    
    concat in interface BitvectorFormulaManager
  - concat
```
protected abstract TFormulaInfo concat(TFormulaInfo number,
                                       TFormulaInfo pAppend)
```
  - extract
```
public final BitvectorFormula extract(BitvectorFormula pNumber,
                                      int pMsb,
                                      int pLsb)
```
    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:
    
    pNumber - from where the bits are extracted.
    
    pMsb - Upper index for the most significant bit. Must be in interval from lsb to bitsize-1.
    
    pLsb - Lower index for the least significant bit. Must be in interval from 0 to msb.
  - extract
```
protected abstract TFormulaInfo extract(TFormulaInfo pNumber,
                                        int pMsb,
                                        int pLsb)
```
  - extend
```
public final BitvectorFormula extend(BitvectorFormula pNumber,
                                     int pExtensionBits,
                                     boolean pSigned)
```
    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:
    
    pNumber - The bitvector to extend.
    
    pExtensionBits - How many bits to add.
    
    pSigned - Whether the extension should depend on the sign bit.
  - extend
```
protected abstract TFormulaInfo extend(TFormulaInfo pNumber,
                                       int pExtensionBits,
                                       boolean pSigned)
```
  - getLength
```
public int getLength(BitvectorFormula pNumber)
```
    Description copied from interface: BitvectorFormulaManager
    
    This method returns the length of a bitvector, also denoted as bit-size.
    
    Specified by:
    
    getLength in interface BitvectorFormulaManager
  - distinct
```
public final BooleanFormula distinct(List<BitvectorFormula> pBits)
```
    Description copied from interface: BitvectorFormulaManager
    
    All given bitvectors are pairwise unequal.
    
    Specified by:
    
    distinct in interface BitvectorFormulaManager
  - distinctImpl
```
protected TFormulaInfo distinctImpl(List<TFormulaInfo> pBits)
```
  - getFormulaCreator
```
protected final FormulaCreator<TFormulaInfo,TType,TEnv,TFuncDecl> getFormulaCreator()
```
  - extractInfo
```
protected final TFormulaInfo extractInfo(Formula pBits)
```
  - toSolverType
```
protected final TType toSolverType(FormulaType<?> formulaType)
```

Class AbstractBitvectorFormulaManager<TFormulaInfo,​TType,​TEnv,​TFuncDecl>

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Methods inherited from interface org.sosy_lab.java_smt.api.BitvectorFormulaManager

Field Detail

formulaCreator

Constructor Detail

AbstractBitvectorFormulaManager

Method Detail

makeBitvector

makeBitvectorImpl

toIntegerFormula

toIntegerFormulaImpl

negate

negate

add

add

subtract

subtract

divide

divide

remainder

remainder

smodulo

smodulo

multiply

multiply

equal

equal

greaterThan

greaterThan

greaterOrEquals

greaterOrEquals

lessThan

lessThan

lessOrEquals

lessOrEquals

not

not

and

and

or

or

xor

xor

makeBitvector

makeBitvectorImpl

makeBitvector

makeBitvectorImpl

transformValueToRange

makeVariable

makeVariable

makeVariableImpl

shiftRight

shiftRight

shiftLeft

shiftLeft

rotateLeft

rotateLeftByConstant

rotateLeft

rotateLeft

rotateRight

rotateRightByConstant

rotateRight

rotateRight

concat

concat

extract

extract

extend

extend

getLength

distinct

distinctImpl

getFormulaCreator

extractInfo

toSolverType

Class AbstractBitvectorFormulaManager<TFormulaInfo,TType,TEnv,TFuncDecl>