Package org.sosy_lab.java_smt.delegate.debugging

Class DebuggingIntegerFormulaManager

java.lang.Object

org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager<NumeralFormula.IntegerFormula,NumeralFormula.IntegerFormula>

org.sosy_lab.java_smt.delegate.debugging.DebuggingIntegerFormulaManager

All Implemented Interfaces:

IntegerFormulaManager, NumeralFormulaManager<NumeralFormula.IntegerFormula,NumeralFormula.IntegerFormula>

public class DebuggingIntegerFormulaManager
extends DebuggingNumeralFormulaManager<NumeralFormula.IntegerFormula,NumeralFormula.IntegerFormula>
implements IntegerFormulaManager

Constructor Summary

Constructors

Constructor	Description
DebuggingIntegerFormulaManager(IntegerFormulaManager pDelegate, org.sosy_lab.java_smt.delegate.debugging.DebuggingAssertions pDebugging)

Method Summary

Modifier and Type	Method	Description
BooleanFormula	modularCongruence(NumeralFormula.IntegerFormula number1, NumeralFormula.IntegerFormula number2, long n)	Create a term representing the constraint number1 == number2 (mod n).
BooleanFormula	modularCongruence(NumeralFormula.IntegerFormula number1, NumeralFormula.IntegerFormula number2, BigInteger n)	Create a term representing the constraint number1 == number2 (mod n).
NumeralFormula.IntegerFormula	modulo(NumeralFormula.IntegerFormula numerator, NumeralFormula.IntegerFormula denominator)	Create a formula representing the modulo of two operands according to Boute's Euclidean definition (DOI: 10.1145/128861.128862).

Methods inherited from class org.sosy_lab.java_smt.delegate.debugging.DebuggingNumeralFormulaManager

add, distinct, divide, equal, floor, getFormulaType, greaterOrEquals, greaterThan, lessOrEquals, lessThan, makeNumber, makeNumber, makeNumber, makeNumber, makeNumber, makeNumber, makeVariable, multiply, negate, subtract, sum

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.IntegerFormulaManager

getFormulaType

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

add, distinct, divide, equal, floor, greaterOrEquals, greaterThan, lessOrEquals, lessThan, makeNumber, makeNumber, makeNumber, makeNumber, makeNumber, makeNumber, makeVariable, multiply, negate, subtract, sum

Constructor Detail

DebuggingIntegerFormulaManager

public DebuggingIntegerFormulaManager(IntegerFormulaManager pDelegate,
                                      org.sosy_lab.java_smt.delegate.debugging.DebuggingAssertions pDebugging)

Method Detail

modularCongruence

public BooleanFormula modularCongruence(NumeralFormula.IntegerFormula number1,
                                        NumeralFormula.IntegerFormula number2,
                                        BigInteger n)

Description copied from interface: IntegerFormulaManager

Create a term representing the constraint number1 == number2 (mod n). Note: this is not formally defined by the SMTLib standard, but supported by many solvers. Please consult the documentation of the used solver for details.

Specified by:

modularCongruence in interface IntegerFormulaManager

modularCongruence

public BooleanFormula modularCongruence(NumeralFormula.IntegerFormula number1,
                                        NumeralFormula.IntegerFormula number2,
                                        long n)

Description copied from interface: IntegerFormulaManager

Create a term representing the constraint number1 == number2 (mod n). Note: this is not formally defined by the SMTLib standard, but supported by many solvers. Please consult the documentation of the used solver for details.

Specified by:

modularCongruence in interface IntegerFormulaManager

modulo

public NumeralFormula.IntegerFormula modulo(NumeralFormula.IntegerFormula numerator,
                                            NumeralFormula.IntegerFormula denominator)

Description copied from interface: IntegerFormulaManager

Create a formula representing the modulo of two operands according to Boute's Euclidean definition (DOI: 10.1145/128861.128862). The quotient (division of numerator by denominator) of the modulo calculation (numerator - quotient * denominator = remainder, with remainder being the result of this operation) is floored for positive denominators and rounded up for negative denominators.

If the denominator evaluates to zero (modulo-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 modulo operation (cf. SMTLib standard version 2.6 for the division operator in Int or Real theory). The details of this are implementation specific and may change solver by solver.

Examples:

• modulo(10, 5) == 0
• modulo(10, 3) == 1
• modulo(10, -3) == 1
• modulo(-10, 5) == 0
• modulo(-10, 3) == 2
• modulo(-10, -3) == 2

Note: Some solvers, e.g., Yices2, abort with an exception when exploring a modulo-by-zero during the SAT-check. This is not compliant to the SMTLIB standard, but sadly happens.

Specified by:

modulo in interface IntegerFormulaManager