java.lang.Object
- org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager<ParamFormulaType,ResultFormulaType>

All Implemented Interfaces:: NumeralFormulaManager<ParamFormulaType,ResultFormulaType>

Direct Known Subclasses:: DebuggingIntegerFormulaManager, DebuggingRationalFormulaManager

public class DebuggingNumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>
extends Object
implements NumeralFormulaManager<ParamFormulaType,ResultFormulaType>

Constructor Summary

Constructors
Constructor	Description
`DebuggingNumeralFormulaManager(NumeralFormulaManager<ParamFormulaType,ResultFormulaType> pDelegate, org.sosy_lab.java_smt.delegate.debugging.DebuggingAssertions pDebugging)`

Method Summary

All Methods Instance Methods Concrete Methods
Modifier and Type	Method	Description
`ResultFormulaType`	`add(ParamFormulaType number1, ParamFormulaType number2)`
`BooleanFormula`	`distinct(List<ParamFormulaType> pNumbers)`	All given numbers are pairwise unequal.
`ResultFormulaType`	`divide(ParamFormulaType numerator, ParamFormulaType denominator)`	Create a formula representing the division of two operands according to Boute's Euclidean definition.
`BooleanFormula`	`equal(ParamFormulaType number1, ParamFormulaType number2)`
`NumeralFormula.IntegerFormula`	`floor(ParamFormulaType formula)`	The `floor` operation returns the nearest integer formula that is less or equal to the given argument formula.
`FormulaType<ResultFormulaType>`	`getFormulaType()`
`BooleanFormula`	`greaterOrEquals(ParamFormulaType number1, ParamFormulaType number2)`
`BooleanFormula`	`greaterThan(ParamFormulaType number1, ParamFormulaType number2)`
`BooleanFormula`	`lessOrEquals(ParamFormulaType number1, ParamFormulaType number2)`
`BooleanFormula`	`lessThan(ParamFormulaType number1, ParamFormulaType number2)`
`ResultFormulaType`	`makeNumber(double number)`	Create a numeric literal with a given value.
`ResultFormulaType`	`makeNumber(long number)`
`ResultFormulaType`	`makeNumber(String pI)`
`ResultFormulaType`	`makeNumber(BigDecimal number)`	Create a numeric literal with a given value.
`ResultFormulaType`	`makeNumber(BigInteger number)`
`ResultFormulaType`	`makeNumber(Rational pRational)`
`ResultFormulaType`	`makeVariable(String pVar)`	Creates a variable with exactly the given name.
`ResultFormulaType`	`multiply(ParamFormulaType number1, ParamFormulaType number2)`
`ResultFormulaType`	`negate(ParamFormulaType number)`
`ResultFormulaType`	`subtract(ParamFormulaType number1, ParamFormulaType number2)`
`ResultFormulaType`	`sum(List<ParamFormulaType> operands)`

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

- Constructor Detail
  - DebuggingNumeralFormulaManager
```
public DebuggingNumeralFormulaManager(NumeralFormulaManager<ParamFormulaType,ResultFormulaType> pDelegate,
                                      org.sosy_lab.java_smt.delegate.debugging.DebuggingAssertions pDebugging)
```
- Method Detail
  - makeNumber
```
public ResultFormulaType makeNumber(long number)
```
    Specified by:
    
    makeNumber in interface NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>
  - makeNumber
```
public ResultFormulaType makeNumber(BigInteger number)
```
    Specified by:
    
    makeNumber in interface NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>
  - makeNumber
```
public ResultFormulaType makeNumber(double number)
```
    Description copied from interface: NumeralFormulaManager
    
    Create a numeric literal with a given value. Note: if the theory represented by this instance cannot handle rational numbers, the value may get rounded or otherwise represented imprecisely.
    
    Specified by:
    
    makeNumber in interface NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>
  - makeNumber
```
public ResultFormulaType makeNumber(BigDecimal number)
```
    Description copied from interface: NumeralFormulaManager
    
    Create a numeric literal with a given value. Note: if the theory represented by this instance cannot handle rational numbers, the value may get rounded or otherwise represented imprecisely.
    
    Specified by:
    
    makeNumber in interface NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>
  - makeNumber
```
public ResultFormulaType makeNumber(String pI)
```
    Specified by:
    
    makeNumber in interface NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>
  - makeNumber
```
public ResultFormulaType makeNumber(Rational pRational)
```
    Specified by:
    
    makeNumber in interface NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>
  - makeVariable
```
public ResultFormulaType makeVariable(String pVar)
```
    Description copied from interface: NumeralFormulaManager
    
    Creates a variable with exactly the given name.
    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 NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>
  - getFormulaType
```
public FormulaType<ResultFormulaType> getFormulaType()
```
    Specified by:
    
    getFormulaType in interface NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>
  - negate
```
public ResultFormulaType negate(ParamFormulaType number)
```
    Specified by:
    
    negate in interface NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>
  - add
```
public ResultFormulaType add(ParamFormulaType number1,
                             ParamFormulaType number2)
```
    Specified by:
    
    add in interface NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>
  - sum
```
public ResultFormulaType sum(List<ParamFormulaType> operands)
```
    Specified by:
    
    sum in interface NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>
  - subtract
```
public ResultFormulaType subtract(ParamFormulaType number1,
                                  ParamFormulaType number2)
```
    Specified by:
    
    subtract in interface NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>
  - divide
```
public ResultFormulaType divide(ParamFormulaType numerator,
                                ParamFormulaType denominator)
```
    Description copied from interface: NumeralFormulaManager
    
    Create a formula representing the division of two operands according to Boute's Euclidean definition.
    If the denominator evaluates to zero (division-by-zero), either directly as value or indirectly via an additional constraint, then the solver is allowed to choose an arbitrary value for the result of the division (cf. SMTLIB standard for the division operator in Ints or Reals theory).
    Note: Some solvers, e.g., Yices2, abort with an exception when exploring a division-by-zero during the SAT-check. This is not compliant to the SMTLIB standard, but sadly happens.
    
    Specified by:
    
    divide in interface NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>
  - multiply
```
public ResultFormulaType multiply(ParamFormulaType number1,
                                  ParamFormulaType number2)
```
    Specified by:
    
    multiply in interface NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>
  - equal
```
public BooleanFormula equal(ParamFormulaType number1,
                            ParamFormulaType number2)
```
    Specified by:
    
    equal in interface NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>
  - distinct
```
public BooleanFormula distinct(List<ParamFormulaType> pNumbers)
```
    Description copied from interface: NumeralFormulaManager
    
    All given numbers are pairwise unequal.
    
    Specified by:
    
    distinct in interface NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>
  - greaterThan
```
public BooleanFormula greaterThan(ParamFormulaType number1,
                                  ParamFormulaType number2)
```
    Specified by:
    
    greaterThan in interface NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>
  - greaterOrEquals
```
public BooleanFormula greaterOrEquals(ParamFormulaType number1,
                                      ParamFormulaType number2)
```
    Specified by:
    
    greaterOrEquals in interface NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>
  - lessThan
```
public BooleanFormula lessThan(ParamFormulaType number1,
                               ParamFormulaType number2)
```
    Specified by:
    
    lessThan in interface NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>
  - lessOrEquals
```
public BooleanFormula lessOrEquals(ParamFormulaType number1,
                                   ParamFormulaType number2)
```
    Specified by:
    
    lessOrEquals in interface NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>
  - floor
```
public NumeralFormula.IntegerFormula floor(ParamFormulaType formula)
```
    Description copied from interface: NumeralFormulaManager
    
    The floor operation returns the nearest integer formula that is less or equal to the given argument formula.
    For rational formulas, SMTlib2 denotes this operation as to_int.
    
    Specified by:
    
    floor in interface NumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>

Class DebuggingNumeralFormulaManager<ParamFormulaType extends NumeralFormula,​ResultFormulaType extends NumeralFormula>

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Constructor Detail

DebuggingNumeralFormulaManager

Method Detail

makeNumber

makeNumber

makeNumber

makeNumber

makeNumber

makeNumber

makeVariable

getFormulaType

negate

add

sum

subtract

divide

multiply

equal

distinct

greaterThan

greaterOrEquals

lessThan

lessOrEquals

floor

Class DebuggingNumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>