search

abau / co4

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

output of labelled systems is broken #97

Open jwaldmann opened 10 years ago

jwaldmann commented 10 years ago

for commit 229aa47e087ba09aa40b94c0c663fcfb0759d782 , these are rejected by ceta:

TRS_Standard/Zantema_05/z25.xml
TRS_Standard/Transformed_CSR_04/Ex24_Luc06_C.xml
TRS_Standard/Zantema_05/jw38.xml
TRS_Standard/AotoYamada_05/Ex1SimplyTyped.xml
TRS_Standard/Waldmann_06/jwcime1.xml
TRS_Standard/Zantema_05/z28.xml
TRS_Standard/Mixed_TRS/2.xml
TRS_Standard/Waldmann_06/jwtpa2.xml
TRS_Standard/Waldmann_06/jwteparla1.xml
TRS_Standard/Secret_05_TRS/teparla1.xml
TRS_Standard/Secret_06_TRS/tpa01.xml
TRS_Standard/Transformed_CSR_04/Ex4_7_77_Bor03_C.xml
TRS_Standard/Transformed_CSR_04/Ex1_GL02a_C.xml
TRS_Standard/Secret_07_TRS/3.xml
TRS_Standard/Waldmann_06/jwteparla2.xml
TRS_Standard/Zantema_05/jw08.xml
TRS_Standard/Zantema_05/jw11.xml
TRS_Standard/Secret_07_TRS/5.xml
TRS_Standard/Secret_06_TRS/gen-22.xml
TRS_Standard/Zantema_05/z19.xml
TRS_Standard/Mixed_TRS/3.xml

Error message seems always like this:

 problem during labeling:
   labeled rule f#[[1, 1]](b[[]], f[[0, 0]](c[[]], x)) -> f#[[0, 0]](c[[]], f[[1, 0]](b[[]], x)) missing
jwaldmann commented 10 years ago

here's an explanation of what I think is happening: each pattern (from a map representation) should be translated to

if ((arg1 matches pat1.1) &&  ... && (argN matches pat1.N)) then val1
else <continuation>

but CPF does not have &&. If we just nest if-then-elses, then this leads to duplication of subtrees

if (arg1 matches pat1.1) then ... if (argN matches pat1.N) then val1 else <continuation>
...
else <continuation>

This will blow up the formula size in the case that the pattern is long.

My work-around is to expand the pattern (convert to 2^bitwidth^arity exact patterns) and translate this into a sum

sum ( if (arg1 == pat1.1) then ... if (argN == pat1.N) then val1 else 0 .. else 0
       , ... )

This is allowed since the Exact patterns are disjoint.

We could get a linear sized translation only by simulating && with numbers.

rene-thiemann commented 10 years ago

I do not understand the problem. CPF can easily simulate &&. Assume we want to model

if (arg1 matches pat1 && ... && argn matches patn) then val1 else <continuation>

where I further assume that argi matches pati evaluates to 0 iff argi matches pati does not hold. (0 = false, anything else = true), then this is easily encoded into CPF as follows (using some sloppy notation):

if min (arg1 matches pat1, ..., argn matches patn) = 0 then <continuation> else val1

Furthermore, also matching is easily encoded into CPF, e.g., x = n for concrete natural number n becomes if x = n then 1 else 0, matching Any becomes the constant 1, negation not pat becomes if pat = 0 then 1 else 0, etc.

So I cannot understand the 2^bitwidth^arity-argument above.

jwaldmann commented 10 years ago

OK, then min encodes &&.