Generators for arithmetic: order of generation
Issue #118
resolved
The generator for the formula ?l[nat] l2[nat]: l<l2 finds no valid instances. This is because the bdds introduce an integer value (l-l2) and start generating 0> thisinteger Than again, it generates all integers (i guess for the -1 * l2 = someotherinteger and then it checks whether everything fits.
The order of generation could be changed so that "helping variables" only get generated at the end. Since in many cases they can be derived.
Comments (6)
-
reporter
-
reporter
see
#118, fixing notyetimplemteds in generatorfactory -
- changed milestone to Second Release
-
- changed milestone to Later
-
- removed milestone
Removing milestone: Later (automated comment)
-
reporter
- changed status to resolved
estitmators for arithmetic had been fixed some time ago. Works like a charm now...
- Log in to comment
Also, fix the notyetimplementeds in the Generatorfactory...