Add support for integer modulo in MathSAT #459
Conversation
MathSAT5 has no native support for modulo on integer formulas. However, the operation can be implemented based on division and subtraction
… zero The solver may return any value if the divisor is zero. However, "modulo" is still a function and modulo(a,0) and modula(b,0) must evaluate to the same value whenever 'a' and 'b' are the same, MathSAT: Add special treatment for integer modulo when the divisor is zero The solver may return any value if the divisor is zero. However, "modulo" is still a function and modulo(a,0) and modula(b,0) must evaluate to the same value whenever 'a' and 'b' are the same, MathSAT: Add special treatment for integer modulo when the divisor is zero The solver may return any value if the divisor is zero. However, "modulo" is still a function and modulo(a,0) and modula(b,0) must evaluate to the same value whenever 'a' and 'b' are the same.
These test seem to depend on the number of UF symbols that were previously defined
| getFormulaCreator().callFunctionImpl(modZeroUF, ImmutableList.of(pNumber1)), | ||
| subtract(pNumber1, multiply(divide(pNumber1, pNumber2), pNumber2))); | ||
| } | ||
|
|
There was a problem hiding this comment.
Be aware that UFs return the same value for the same parameters.
If SMTLIB allows "any return value", then the return value could be random and return a different result at second call.
From technical point, returning the same result on second call would be fully ok for me. From SMTLIB point, please check what the standard and other solvers return for x/0 == x/0. Is this always satisfied?
There was a problem hiding this comment.
Be aware that UFs return the same value for the same parameters
I've added some test in the last commit, and this seems to match what the other solvers are doing.
SMTLIB says:
"Since in SMT-LIB logic all function symbols are interpreted as total
functions, terms of the form (/ t 0) *are* meaningful in every
instance of Reals. However, the declaration imposes no constraints
on their value. This means in particular that
- for every instance theory T and
- for every value v (as defined in the :values attribute) and
closed term t of sort Real,
there is a model of T that satisfies (= v (/ t 0)).
"
The definition talks about reals, but it also applies to integers. It's not entirely clear from it, but I would argue that x/0 == x/0 must hold as / is still a (mathematical) function and the same argument means that the result is the same.
There was a problem hiding this comment.
Valid point. Lets approve it.
| getFormulaCreator().callFunctionImpl(modZeroUF, ImmutableList.of(pNumber1)), | ||
| subtract(pNumber1, multiply(divide(pNumber1, pNumber2), pNumber2))); | ||
| } | ||
|
|
There was a problem hiding this comment.
Valid point. Lets approve it.
Hello,
MathSAT is missing native support for integer modulo. In this PR we add a work-around based on the definition
remainder = dividend - floor(dividend/divisor)*divisorto support the operation.