Return-Path: Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <02684-0@swan.cl.cam.ac.uk>; Thu, 13 Feb 1992 14:59:39 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA02533; Thu, 13 Feb 92 06:49:03 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from sparta.oracorp.com by ted.cs.uidaho.edu (16.6/1.34) id AA02529; Thu, 13 Feb 92 06:48:53 -0800 Date: Thu, 13 Feb 92 09:50:12 EST From: shb@com.oracorp.sparta Received: by sparta.oracorp.com (4.1/1.3-ORA Corporation) id AA08108; Thu, 13 Feb 92 09:50:12 EST Message-Id: <9202131450.AA08108@sparta.oracorp.com> To: info-hol@edu.uidaho.cs.ted Subject: Huge expressions I'm verifying a security property for a computer system, and the HOL expression corresponding to its statement is huge. This generally makes things slow and painful. Here are two specific questions and a more general one on strategy: I've been setting max_print_depth to 10, but HOL88 (version 1.12) still takes a long time just to print the abbreviated expression, as if it has to think about all the stuff that it's decided not to print. Why is that? Is there anything I can do to speed things up? My guess is that the main HOL strategy for dealing with huge subexpressions is not letting them arise in the first place, limiting rewriting to keep things manageable. Is that right? If so, I'll investigate trying to break off parts of the problem before the expressions get huge. Steve Brackin ORA Corporation Ithaca, NY