A journey with the preprocessor and defprod

How many fields does it take to break defprod?  Hint: you already know the answer.  42!

Why is this?  Suppose you have the following forms:

(include-book "centaur/fty/deftypes" :dir :system)
(fty::defprod slow-it-down
 ((a booleanp) (b booleanp) (c booleanp) (d booleanp) (e booleanp)
 (f booleanp) (g booleanp) (h booleanp) (i booleanp) (j booleanp)
 (k booleanp) (l booleanp) (m booleanp) (n booleanp) (o booleanp)
 (p booleanp) (q booleanp) (r booleanp) (s booleanp) (tt booleanp)
 (u booleanp) (v booleanp) (w booleanp) (xx booleanp) (y booleanp)
 (z booleanp) (aa booleanp) (ab booleanp) (ac booleanp) (ad booleanp)
 (ae booleanp) (af booleanp) (ag booleanp) (ah booleanp) (ai booleanp)
 (aj booleanp) (ak booleanp) (al booleanp) (am booleanp) (an booleanp)
 (ao booleanp) (ap booleanp)
 (aq booleanp) ;; the offending threshold
 ))

As of May 16, 2016, you’ll get a nice error that says the preprocessor’s rewrite stack has reached its limit and quit:

HARD ACL2 ERROR in PREPROCESS: The call depth limit of 1000 has been
exceeded in the ACL2 preprocessor (a sort of rewriter). There is probably
a loop caused by some set of enabled simple rules.

But there are no such looping rules (that I found).  This is evident by the error going away (and an analogous proof completes over a weekend in 130,000 seconds — hah!).

You might think it clever to disable the preprocessor.  That _might_ work, but there are three difficulties with that:

  1. There isn’t any published way to disable the preprocessor at the top-level (there may not be any), and we’re deep inside defprod
  2. Modifying defprod not to call the preprocessor in just the right place could break  other uses of defprod
  3. The subgoal generated when you do disable the preprocessor looks a lot like something a preprocessor could be good at (though, I suspect that in ACL2 we need generalization):
    (IMPLIES
     (AND
      (ALISTP X)
      (CONSP X)
      (CONSP (CDR X))
      (CONSP (CDDR X))
      (CONSP (CDDDR X))
      (CONSP (CDDDDR X))
      (CONSP (CDR (CDDDDR X)))
      (CONSP (CDDR (CDDDDR X)))
      (CONSP (CDDDR (CDDDDR X)))
      (CONSP (CDDDDR (CDDDDR X)))
      ...)
     (EQUAL (LIST (CONS 'B (<booleanp-fix> (CDR (CAR X))))
                  (CONS 'C (<booleanp-fix> (CDR (CADR X)))))
            X))

With what solution did I end up?

Change the format of the defprod from the default of being represented as an alist to being represented as a tree.

It’s still slow, and I’ll probably clean it up some more, but now it finishes in 666.04 seconds instead of 130,000.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s