search

abau / co4

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

semantic labelling: try very brute argument filter #57

Closed jwaldmann closed 10 years ago

jwaldmann commented 10 years ago

just for fun and testing: if all marked symbols have empty argument filter (that is, no children), then everything boils down to finding an order for these marked (and labelled) symbols. We don't need to consider the term structure at all, and can drop the LPO computation. I want to see whether this works for interesting examples (large model, but empty filter).

For testing CO4: if the argument filter allocator produces known empty lists, then the generated formula should automatically be small?

abau commented 10 years ago 
--brute-filter           use argument filter that deletes all children (default: false)

Works for

tpdb-6.0.2/XML/TRS/Zantema/jw01.xml --brute-filter -m 2

For testing CO4

tpdb-6.0.2/XML/TRS/Zantema/jw01.xml -m 2 gives #variables (Minisat): 156948 in the first iteration. The brute filter reduces the number of allocated variables to #variables (Minisat): 3698.