abau / co4

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

semantic labelling: symbol map: should use common bit width #79

Open jwaldmann opened 10 years ago

jwaldmann commented 10 years ago

I think this looks strange:

Symbol Map:
fromList [((nat 0 0),"b"),((nat 1 1),"c"),((nat 2 2),"a"),((nat 2 3),"x")]

They should all have identical bit width, this might avoid merging problems?

abau commented 10 years ago

I didn't experience any problems with symbols of different bitwidth. In fact, this saves some variables:

#variables: 7180, #clauses: 20399, #literals: 50893, clause density: 2.8410863509749302

versus

#variables: 7152, #clauses: 20343, #literals: 50781, clause density: 2.8443791946308723

for tpdb-6.0.2/XML/TRS/D33/07.xml. But a simple revert

git revert 790dcf2c372a91d2780a20551c6e76c60ee934f6

makes all symbols to have a common bitwidth again.