js modulo operator behaves differently than smtlib modulo

[santolucito]

In SMTLIB the modulo operator uses Boute's Euclidean definition (http://smtlib.cs.uiowa.edu/theories-Ints.shtml).

In JS, it uses its own interpretation. Critically, for any x, x%0 == NaN. In Boute's Euclidean definition x%0 should be 0 for any x.

As a specific issue, entering the pattern [1,2,1,0,0,0...] generates the code pattern((val,i) => 1 + (i % (i - 3)));

If we modify the example to be [1,2,1,1,0,0,...], the above code still works, probably because in JS:

1  + (3% (3 - 3))
1  + (3 % (3 - 3))
1  + (3 % (0))
1  + (NaN)
NaN

One solution might be to provide our own implementation of modulo. Using https://stackoverflow.com/a/41913619, we can create a new infix function (maybe called smtMod). Then all we need to do is find and replace % for smtMod before we evaluate the code.

This does mean that we slightly diverge from "normal" js semantics, but 1) I'm not sure that is an issue 2) this is probably a good case to do this. It does bring up a more general question of what we do when target language and synthesis language semantics diverge (note to self: wasn't this the failed paper with Bill and Max?)

[santolucito]

@Catherine-Ji if you want to tackle a more challenging, math-y issue, this could be interesting for you. It is similar to the work you were doing on adding DSL functions. No worries if not tho :)