Extend documentation for Int/Real division, modulo and modular congruence

Author: BaierD

src/org/sosy_lab/java_smt/api/IntegerFormulaManager.java

@@ -19,31 +19,42 @@
 public interface IntegerFormulaManager
     extends NumeralFormulaManager<IntegerFormula, IntegerFormula> {
 
-  /** Create a term representing the constraint {@code number1 == number2 (mod n)}. */
+  /**
+   * Create a term representing the constraint {@code 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.
+   */
   BooleanFormula modularCongruence(IntegerFormula number1, IntegerFormula number2, BigInteger n);
 
-  /** Create a term representing the constraint {@code number1 == number2 (mod n)}. */
+  /**
+   * Create a term representing the constraint {@code 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.
+   */
   BooleanFormula modularCongruence(IntegerFormula number1, IntegerFormula number2, long n);
 
   /**
    * Create a formula representing the modulo of two operands according to Boute's Euclidean
-   * definition. The quotient (div numerator denominator) of the internal modulo calculation is
-   * floored for positive denominators and rounded up for negative denominators.
+   * 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.
    *
    * <p>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 for the division operator in
-   * Ints or Reals theory).
+   * 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.
    *
    * <p>Examples:
    *
    * <ul>
-   *   <li>10 % 5 == 0
-   *   <li>10 % 3 == 1
-   *   <li>10 % (-3) == 1
-   *   <li>-10 % 5 == 0
-   *   <li>-10 % 3 == 2
-   *   <li>-10 % (-3) == 2
+   *   <li>modulo(10, 5) == 0
+   *   <li>modulo(10, 3) == 1
+   *   <li>modulo(10, -3) == 1
+   *   <li>modulo(-10, 5) == 0
+   *   <li>modulo(-10, 3) == 2
+   *   <li>modulo(-10, -3) == 2
    * </ul>
    *
    * <p>Note: Some solvers, e.g., Yices2, abort with an exception when exploring a modulo-by-zero

src/org/sosy_lab/java_smt/api/NumeralFormulaManager.java

@@ -69,12 +69,13 @@ public interface NumeralFormulaManager<
 
   /**
    * Create a formula representing the division of two operands according to Boute's Euclidean
-   * definition.
+   * definition (DOI: 10.1145/128861.128862).
    *
    * <p>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).
+   * value for the result of the division (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.
    *
    * <p>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.