Presolver returns unsat

[romits800]

Optimizing function "fe25519_mul" does not give any solution, with the presolver proving that it is infeasible. After running Unison:

$ uni import --target=Mips ed25519_ref10.mir -o ed25519_ref10.uni --function=fe25519_mul --maxblocksize=25 --goal=speed
$ uni linearize --target=Mips ed25519_ref10.uni -o ed25519_ref10.lssa.uni
$ uni extend --target=Mips ed25519_ref10.lssa.uni -o ed25519_ref10.ext.uni
$ uni augment --target=Mips ed25519_ref10.ext.uni -o ed25519_ref10.alt.uni
$ uni model --target=Mips ed25519_ref10.alt.uni -o ed25519_ref10.json

The presolver returns:

$ gecode-presolver -o ed25519_ref10.ext.json -dzn ed25519_ref10.dzn --verbose ed25519_ref10.json
[pre]    proven absence of solutions with cost less or equal than {2147483646}
presolved in 65254.1 ms

I am attaching the .mir file, generated by:

llc ed25519_ref10.O3.ll -O2 -march=mips -mcpu=mips32 -unison -unison-no-clean -unison-only-functions="fe25519_mul"

ed25519_ref10_mir.tar.gz

[robcasloz]

Hi Romy, I had a look but the test case is too large for effective debugging. Could you try to reduce it, perhaps by disabling code-bloating LLVM IR opts or removing parts of the original C function? For the latter, I recommend you using a tool like C-Reduce.

[romits800]

Hi Roberto, I tried to reduce the size by reducing the size of the actual function: I attach the following files together with a script that runs them: test3.5.tar.gz : The largest example, where the presolver seems to work as expected test4.tar.gz: The smallest example that demonstrates the same behavior as described in the initial post.

test4.tar.gz test3.5.tar.gz

Let me know if the size is still large.

[robcasloz]

Thanks! Solved, I think :) Please check that this does not cause any regression in your experiments.