Package org.sosy_lab.java_smt.delegate.debugging

Class DebuggingNumeralFormulaManager<ParamFormulaType extends NumeralFormula,ResultFormulaType extends NumeralFormula>

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

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 denumerator)	Create a formula representing the division of two operands.
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 denumerator)

Description copied from interface: NumeralFormulaManager

Create a formula representing the division of two operands.

If the denumerator 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>