semantic labelling: better main program

jwaldmann commented 10 years ago

at the moment, tc/CO4/Test/TermComp2014/Main.hs repeatedly removes at least one rule, each time using the same configuration. This is wasting time. There should be a driver program that applies some cheap methods first.

Cheap methods are (without sem. labeling)

compute SCCs of EDG (using ren/cap)
for each SCC: natural and perhaps arctic matrix int. for small dimension (use this: https://github.com/jwaldmann/matchbox/blob/master/MB.hs#L164)

Then more expensive methods from the co4 tree

semantic labelling (with increasing bit width etc.)

And of course, if an expensive step was successful, then start again with the cheap ones, starting with re-computing the EDG (it may look different since we removed some rules). This is the "recursive decomposition" method from http://www.jaist.ac.jp/~hirokawa/publications/03cade.pdf (Sect. 4)

The strategy of the main program should be expressed by something like https://github.com/jwaldmann/transformer-combinators but the API looks somewhat ugly.

jwaldmann commented 10 years ago

for SCC, see https://github.com/jwaldmann/haskell-tpdb/commit/90a5596e6a0396204ea3fd9e78d9c807ba96a44b

jwaldmann commented 10 years ago

some cleanup in https://github.com/jwaldmann/co4/commit/1a7d29c73df8be7b1ab8af51f81d94b7469502ca

Still one bug (will open separate issue)

abau / co4

semantic labelling: better main program #82