Package org.sosy_lab.java_smt.api
Interface IntegerFormulaManager
-
- All Superinterfaces:
NumeralFormulaManager<NumeralFormula.IntegerFormula,NumeralFormula.IntegerFormula>
- All Known Implementing Classes:
DebuggingIntegerFormulaManager
public interface IntegerFormulaManager extends NumeralFormulaManager<NumeralFormula.IntegerFormula,NumeralFormula.IntegerFormula>
Interface which operates overNumeralFormula.IntegerFormula
s.Integer formulas always take integral formulas as arguments.
-
-
Method Summary
All Methods Instance Methods Abstract Methods Default Methods Modifier and Type Method Description default FormulaType<NumeralFormula.IntegerFormula>
getFormulaType()
BooleanFormula
modularCongruence(NumeralFormula.IntegerFormula number1, NumeralFormula.IntegerFormula number2, long n)
Create a term representing the constraintnumber1 == number2 (mod n)
.BooleanFormula
modularCongruence(NumeralFormula.IntegerFormula number1, NumeralFormula.IntegerFormula number2, BigInteger n)
Create a term representing the constraintnumber1 == number2 (mod n)
.NumeralFormula.IntegerFormula
modulo(NumeralFormula.IntegerFormula numerator, NumeralFormula.IntegerFormula denumerator)
Create a formula representing the modulo of two operands.-
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
-
-
-
-
Method Detail
-
modularCongruence
BooleanFormula modularCongruence(NumeralFormula.IntegerFormula number1, NumeralFormula.IntegerFormula number2, BigInteger n)
Create a term representing the constraintnumber1 == number2 (mod n)
.
-
modularCongruence
BooleanFormula modularCongruence(NumeralFormula.IntegerFormula number1, NumeralFormula.IntegerFormula number2, long n)
Create a term representing the constraintnumber1 == number2 (mod n)
.
-
modulo
NumeralFormula.IntegerFormula modulo(NumeralFormula.IntegerFormula numerator, NumeralFormula.IntegerFormula denumerator)
Create a formula representing the modulo of two operands.If the denumerator 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 for the division operator in Ints or Reals theory).
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.
-
getFormulaType
default FormulaType<NumeralFormula.IntegerFormula> getFormulaType()
- Specified by:
getFormulaType
in interfaceNumeralFormulaManager<NumeralFormula.IntegerFormula,NumeralFormula.IntegerFormula>
-
-