search

abau / co4

COmplexity COncerned COnstraint COmpiler
GNU General Public License v3.0
2 stars 3 forks source link

Problem with Usable Rules #91

Closed rene-thiemann closed 10 years ago

rene-thiemann commented 10 years ago

Looking at the proof https://github.com/jwaldmann/co4/blob/usable-rules/JFP_Ex31.plain.2 again, although the issue with unlabProc seem to be fixed, there might be a problem in the computation of usable rules.

For example, in https://github.com/jwaldmann/co4/blob/usable-rules/JFP_Ex31.plain.2#L134-135 the two top-rules are mentioned in the set of usable rules, although they are obviously not usable (neither the pairs nor any of the other rules contain the symbol top). Is this intended, or may the SAT-solver over approximate the usable rules by just guessing a set of suitable usable rules which are closed under right-hand sides?

jwaldmann commented 10 years ago

yes, the usability is guessed (it is the UsableSymbol map here https://github.com/jwaldmann/co4/blob/usable-rules/tc/CO4/Test/TermComp2014/Standalone.hs#L97 ) and then closure is verified in the constraint (https://github.com/jwaldmann/co4/blob/usable-rules/tc/CO4/Test/TermComp2014/Standalone.hs#L187 )

rene-thiemann commented 10 years ago

ok, then that's fine.