unison-code / unison

Unison's source code
http://unison-code.github.io/
Other
104 stars 17 forks source link

gecode-solver solves blocks in static order #30

Open matsc-at-sics-se opened 6 years ago

matsc-at-sics-se commented 6 years ago

It should begin with the most recently failed block, or use accumulated failure count. For example:

uni import --target=X86 ../experiments/x86/selected-functions/speed-toplas/rasta.mapping.comp_Jboundaries.mir -o rasta.mapping.comp_Jboundaries.uni --targetoption=skylake --maxblocksize=25 --explicitcallreg --goal=speed --copyremat --lint
uni linearize --target=X86 rasta.mapping.comp_Jboundaries.uni -o rasta.mapping.comp_Jboundaries.lssa.uni --targetoption=skylake --lint
uni extend --target=X86 rasta.mapping.comp_Jboundaries.lssa.uni -o rasta.mapping.comp_Jboundaries.ext.uni --targetoption=skylake --lint
uni augment --target=X86 rasta.mapping.comp_Jboundaries.ext.uni -o rasta.mapping.comp_Jboundaries.alt.uni --targetoption=skylake --copyremat --lint
uni normalize --target=X86 ../experiments/x86/selected-functions/speed-toplas/rasta.mapping.comp_Jboundaries.asm.mir -o rasta.mapping.comp_Jboundaries.llvm.mir --targetoption=skylake 
uni model --target=X86 --basefile=rasta.mapping.comp_Jboundaries.llvm.mir rasta.mapping.comp_Jboundaries.alt.uni -o rasta.mapping.comp_Jboundaries.json --targetoption=skylake 
gecode-presolver -dzn rasta.mapping.comp_Jboundaries.dzn -verbose  rasta.mapping.comp_Jboundaries.json | aeson-pretty > rasta.mapping.comp_Jboundaries.ext.json
[...]
gecode-solver -dzn rasta.mapping.comp_Jboundaries.dzn -o rasta.mapping.comp_Jboundaries.out.json.temp -l rasta.mapping.comp_Jboundaries.lb.json   rasta.mapping.comp_Jboundaries.ext.json
[...]
[global] solving problem (i: 5, state: 0.222222(c), cost: {[13258..14278]})
[global] found solution (failures: 0, nodes: 27)
[b0]     repeated solution
[b1]     repeated solution
[b2]     proven unsatisfiable (failures: 18, nodes: 45)
[b2]     could not find solution (unsatisfiable)
[global] could not find a full solution
[global] solving problem (i: 6, state: 0.333333, cost: {[13258..14278]})
[global] found solution (failures: 1, nodes: 30)
[b0]     repeated solution
[b1]     found optimal solution (cost: {2}, failures: 7, nodes: 21)
[b2]     found optimal solution (cost: {36}, failures: 96, nodes: 233)
[b3]     found optimal solution (cost: {4}, failures: 6, nodes: 25)
[b4]     found optimal solution (cost: {16}, failures: 88, nodes: 212)
[b5]     repeated solution
[...]