From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id TAA03012; Sat, 9 Oct 2004 19:56:17 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id TAA03001 for ; Sat, 9 Oct 2004 19:56:16 +0200 (MET DST) Received: from hermes.jf.intel.com (fmr05.intel.com [134.134.136.6]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id i99HuFQ0013596; Sat, 9 Oct 2004 19:56:16 +0200 Received: from talaria.jf.intel.com (talaria.jf.intel.com [10.7.209.7]) by hermes.jf.intel.com (8.12.9-20030918-01/8.12.9/d: major-outer.mc,v 1.15 2004/01/30 18:16:28 root Exp $) with ESMTP id i99Hxkck016258; Sat, 9 Oct 2004 17:59:46 GMT Received: from orsmsxvs041.jf.intel.com (orsmsxvs041.jf.intel.com [192.168.65.54]) by talaria.jf.intel.com (8.12.9-20030918-01/8.12.9/d: major-inner.mc,v 1.11 2004/07/29 22:51:53 root Exp $) with SMTP id i99HlNPZ029842; Sat, 9 Oct 2004 17:47:25 GMT Received: from orsmsx332.amr.corp.intel.com ([192.168.65.60]) by orsmsxvs041.jf.intel.com (SAVSMTP 3.1.2.35) with SMTP id M2004100910561300739 ; Sat, 09 Oct 2004 10:56:13 -0700 Received: from orsmsx407.amr.corp.intel.com ([192.168.65.50]) by orsmsx332.amr.corp.intel.com with Microsoft SMTPSVC(6.0.3790.0); Sat, 9 Oct 2004 10:56:13 -0700 X-MimeOLE: Produced By Microsoft Exchange V6.5.7226.0 Content-class: urn:content-classes:message MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: quoted-printable Subject: RE: [Caml-list] Are you sure the new "=" of 3.08 is good ? Date: Sat, 9 Oct 2004 10:56:12 -0700 Message-ID: <012676D607FCF54E986746512C22CE7D0FE7BD@orsmsx407> Thread-Topic: [Caml-list] Are you sure the new "=" of 3.08 is good ? Thread-Index: AcStXUkxB3a3NTQMQuejYJ4q8G9bnAAyj+fg From: "Harrison, John R" To: "Damien Doligez" , "caml-list" X-OriginalArrivalTime: 09 Oct 2004 17:56:13.0684 (UTC) FILETIME=[4459BB40:01C4AE29] X-Scanned-By: MIMEDefang 2.31 (www . roaringpenguin . com / mimedefang) X-Miltered: at concorde with ID 4168263F.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Loop: caml-list@inria.fr X-Spam: no; 0.00; caml-list:01 johnh:01 prover:01 pierre:01 weis:01 pointers:01 speedup:01 hashing:01 pointers:01 hash:01 prover:01 caml:01 equality:01 pointer:03 stuff:05 Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk | What I did in my soon-to-be-released automatic prover, following | advice from Pierre Weis, was to hash-cons all the terms used by the | program. Now I only need to use pointer equality: if the pointers | are not the same then I know the terms are not the same. The speedup | was a factor of 100 because my program does lots of comparisons and | hashing of terms. Yes, it might well be worth looking at that again. I tried it once in CAML Light and the results were disappointing. But one reason was that something like weak pointers either didn't exist or I didn't know about them, so my hash tables rendered some ephemeral stuff=20 non-collectible. I'll look forward to the release of your prover! John. ------------------- To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/ Beginner's list: http://groups.yahoo.com/group/ocaml_beginners