GL counterexample handler problem

[Andrew Brock]

Hi everyone,

I've written a tail recursive function as part of an ACL2 model of some RTL. Glucose returns a counterexample for the proof I am trying to prove about this model to GL, but GL falls into a hole processing that counter example.  FWIW, we expect the tail recursive function to be limited to 100 recursions.

(7F6657FE5F10) : 0 (STORE-PROOF-GLCP-REWRITE-APPLY-RULES ((REWRITE-RULE # 114258 NIL EQUAL ...) (REWRITE-RULE # 114215 NIL EQUAL ...) (REWRITE-RULE # 114172 NIL EQUAL ...) (REWRITE-RULE # 114132 NIL EQUAL ...) (REWRITE-RULE # 114101 NIL EQUAL ...) ...) ((:REWRITE EQUAL-OF-FAIG-CONST->4V-2) (:REWRITE EQUAL-OF-FAIG-CONST->4V-1) (:REWRITE EQUAL-OF-BOOL-TO-4V-2) (:REWRITE EQUAL-OF-BOOL-TO-4V-1) (:REWRITE FAIG-CONST->4V-EQUAL-F-GL) ...) EQUAL (1 (:G-NUMBER #)) NIL #((# # # # # ...) #(505) #(363)) 999931 (:GLCP-CONFIG (GL::ABORT-INDETERMINATE . T) (GL::ABORT-CTREX . T) (GL::EXEC-CTREX . T) (GL::CTREX-TRANSFORM LAMBDA # X) ...) #((#) NIL NIL) #(#(7253) #(7253) #() NIL NIL) ACL2_INVISIBLE::|The Live State Itself|) 117
 (7F6657FE5F88) : 1 (STORE-PROOF-GLCP-INTERP-FNCALL EQUAL (1 (:G-NUMBER #)) (EQUAL '1 X) NIL #((# # # # # ...) #(505) #(363)) 999931 (:GLCP-CONFIG (GL::ABORT-INDETERMINATE . T) (GL::ABORT-CTREX . T) (GL::EXEC-CTREX . T) (GL::CTREX-TRANSFORM LAMBDA # X) ...) #((#) NIL NIL) #(#(7253) #(7253) #() NIL NIL) ACL2_INVISIBLE::|The Live State Itself|) 445
 (7F6657FE6010) : 2 (STORE-PROOF-GLCP-INTERP-TERM-EQUIVS (EQUAL '1 X) ((X :G-NUMBER #)) NIL #((# # # # # ...) #(505) #(363)) 999931 (:GLCP-CONFIG (GL::ABORT-INDETERMINATE . T) (GL::ABORT-CTREX . T) (GL::EXEC-CTREX . T) (GL::CTREX-TRANSFORM LAMBDA # X) ...) #((#) NIL NIL) #(#(7253) #(7253) #() NIL NIL) ACL2_INVISIBLE::|The Live State Itself|) 285
 (7F6657FE6078) : 3 (STORE-PROOF-GLCP-INTERP-TERM-EQUIVS (BIT->BOOL$INLINE (BINARY-LOGIOR # #)) ((__FUNCTION__ . IS-DEBIT) (ST # # # # ...)) NIL #((# # # # # ...) #(505) #(363)) 999932 (:GLCP-CONFIG (GL::ABORT-INDETERMINATE . T) (GL::ABORT-CTREX . T) (GL::EXEC-CTREX . T) (GL::CTREX-TRANSFORM LAMBDA # X) ...) #((#) NIL NIL) #(#(7253) #(7253) #() NIL NIL) ACL2_INVISIBLE::|The Live State Itself|) 285
 (7F6657FE60E0) : 4 (STORE-PROOF-GLCP-MAYBE-INTERP (BIT->BOOL$INLINE (BINARY-LOGIOR # #)) ((__FUNCTION__ . IS-DEBIT) (ST # # # # ...)) NIL T #((# # # # # ...) #(505) #(363)) 999932 (:GLCP-CONFIG (GL::ABORT-INDETERMINATE . T) (GL::ABORT-CTREX . T) (GL::EXEC-CTREX . T) (GL::CTREX-TRANSFORM LAMBDA # X) ...) #((#) NIL NIL) #(#(7253) #(7253) #() NIL NIL) ACL2_INVISIBLE::|The Live State Itself|) 1837
 (7F6657FE6168) : 5 (STORE-PROOF-GLCP-INTERP-IF (ATOM ST) 'NIL (BIT->BOOL$INLINE (BINARY-LOGIOR # #)) (IF (ATOM ST) 'NIL (BIT->BOOL$INLINE #)) ((__FUNCTION__ . IS-DEBIT) (ST # # # # ...)) NIL #((# # # # # ...) #(505) #(363)) 999932 (:GLCP-CONFIG (GL::ABORT-INDETERMINATE . T) (GL::ABORT-CTREX . T) (GL::EXEC-CTREX . T) (GL::CTREX-TRANSFORM LAMBDA # X) ...) #((#) NIL NIL) #(#(7253) #(7253) #() NIL NIL) ACL2_INVISIBLE::|The Live State Itself|) 477
<snip, full trace attached>

GL isn't exhausting heap or stack or anything in trying to parse this counterexample: it simply keeps running (for up to several days), not making any visible progress. I eventually have to abort it. Does anyone have any idea what's going on here? Is there a way I should be writing my model to avoid having problems like this?

Thank you,
Andrew

[Sol Swords]

It's not handling a counterexample in that trace -- it's still symbolically interpreting some term.  (Maybe the counterexample was for the initial vacuity check?) It seems to be in the midst of arbrocks-recursive-function-p1, ~20 recursions deep.

Just a guess, but is this function structured something like this?

(defun foo (x)

  (if (test0 x)

     (base-case x)

    (if (test1 x)

        (foo (step1 x))

      (foo (step2 x)))))

If there are two recursive calls occuring on different branches and the IF test between them doesn't resolve to a constant, then symbolic execution of the function is exponential in the recursion depth.  Boolean-listp has this problem, for example.  This sort of problem can often be solved for GL by using an alternate definition like this:

(defun foo (x)
  (if (test0 x)
     (base-case x)
    (foo (if (test1 x) (step1 x) (step2 x))))).

Maybe someday GL will have a preprocessing step that takes care of things like this.

- Sol

--
--
ACL2-books help:
To post new messages: acl2-...@googlegroups.com
To unsubscribe: acl2-books-unsubscribe@googlegroups.com
More options: http://groups.google.com/group/acl2-books?hl=en

---
You received this message because you are subscribed to the Google Groups "acl2-books" group.
To unsubscribe from this group and stop receiving emails from it, send an email to acl2-books+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Andrew Brock]

This is as part of the vacuity check, and you are correct: the function was structured exactly like that. I've restructured it, and this gives better results...

Well, it gives different results. Now we exhaust our hons space 50,000 frames deep into a recursive call, ending in 850 bfr-+-ss calls and
*(7F665795A770) : 0 (%CONS-NHASH-VECTOR ???) NIL
 (7F665795A7D8) : 1 (%CONS-NHASH-VECTOR 1603250563 0) 197
 (7F665795A800) : 2 (MAKE-HASH-TABLE :TEST -1 :SIZE 1122275328 :REHASH-SIZE 1.5 :REHASH-THRESHOLD 1.4285715 :HASH-FUNCTION -1 :WEAK NIL :FINALIZEABLE NIL :ADDRESS-BASED T :LOCK-FREE NIL :SHARED NIL) 2429
 (7F665795A900) : 3 (HL-HSPACE-HONS-WASH #S(HL-HSPACE :STR-HT #<HASH-TABLE :TEST EQUAL size 4702/5065 #x3020005181FD> :ADDR-HT #<HASH-TABLE :TEST EQL size 0/62 #x3020DBE6869D> ...)) 1301
 (7F665795A9A8) : 4 (HL-ADDR-LIMIT-ACTION #S(HL-HSPACE :STR-HT #<HASH-TABLE :TEST EQUAL size 4702/5065 #x3020005181FD> :ADDR-HT #<HASH-TABLE :TEST EQL size 0/62 #x3020DBE6869D> ...)) 1925
 (7F665795AA10) : 5 (HL-HSPACE-HONS-NORMED ((#) (# #)) ((# #) (# #) (# #) (# #) (# #) ...) NIL #S(HL-HSPACE :STR-HT #<HASH-TABLE :TEST EQUAL size 4702/5065 #x3020005181FD> :ADDR-HT #<HASH-TABLE :TEST EQL size 0/62 #x3020DBE6869D> ...)) 1053
 (7F665795AA78) : 6 (AIG-XOR ((# # # # # ...)) ((#) (# #))) 173
 (7F665795AAA0) : 7 (BFR-+-SS ((# # # # # ...)) (T) ((#) (#) (#) (#) (#) ...)) 237
 (7F665795AB00) : 8 (BFR-+-SS ((# # # # # ...)) (T) ((#) (#) (#) (#) (#) ...)) 629
 (7F665795AB70) : 9 (BFR-+-SS ((# # # # # ...)) (T) ((#) (#) (#) (#) (#) ...)) 629
 (7F665795ABE0) : 10 (BFR-+-SS ((# # # # # ...)) (T) ((#) (#) (#) (#) (#) ...)) 629
 (7F665795AC50) : 11 (BFR-+-SS ((# # # # # ...)) (T) ((#) (#) (#) (#) (#) ...)) 629

David thinks an inequality operator (we use >= and <) may be causing the blowup, but somewhat skeptical of that. I'm looking into cleaning up the function definition further. Does this seem like a reasonable outcome of this refactor?

Thanks,
Andrew

To unsubscribe: acl2-books-...@googlegroups.com

More options: http://groups.google.com/group/acl2-books?hl=en

---
You received this message because you are subscribed to the Google Groups "acl2-books" group.

To unsubscribe from this group and stop receiving emails from it, send an email to acl2-books+...@googlegroups.com.

[Sol Swords]

I don't have any idea what's causing the blowup now, but < won't cause a call of bfr-+-ss.  The fact that you're 850 frames deep in bfr-+-ss means that you're dealing with numbers that are >= 850 bits wide, which you perhaps don't intend?  So probably the next step is to investigate how your symbolic integers are growing.  In AIG mode, the fact that some computed value can't be more than N bits doesn't necessarily imply that its symbolic representation won't be much greater than that, with the upper bits all being unsatisfiable formulas.  You can sometimes use GL-MBE to deal with this.

Another thing to maybe think about is how your recursion is supposed to terminate.  If you're depending on, say, counting a symbolic number down to 0, that might not work in AIG mode, for similar reasons.  (It might be that that is where the bfr-+-ss is coming from -- it looks like one of the operands is (T) = -1, but that's 850 bits deep so it could be something else.)