← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/centaur/ubdds/param.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/centaur/ubdds/param.lisp
1
1
; UBDD Library
2
2
; Copyright (C) 2008-2011 Warren Hunt and Bob Boyer
 
3
; License: A 3-clause BSD license.  See the LICENSE file distributed with ACL2.
3
4
; Significantly revised in 2008 by Jared Davis and Sol Swords.
4
5
; Now maintained by Centaur Technology.
5
6
;
7
8
;   Centaur Technology Formal Verification Group
8
9
;   7600-C N. Capital of Texas Highway, Suite 300, Austin, TX 78731, USA.
9
10
;   http://www.centtech.com/
10
 
;
11
 
; This program is free software; you can redistribute it and/or modify it under
12
 
; the terms of the GNU General Public License as published by the Free Software
13
 
; Foundation; either version 2 of the License, or (at your option) any later
14
 
; version.  This program is distributed in the hope that it will be useful but
15
 
; WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
16
 
; FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License for
17
 
; more details.  You should have received a copy of the GNU General Public
18
 
; License along with this program; if not, write to the Free Software
19
 
; Foundation, Inc., 51 Franklin Street, Suite 500, Boston, MA 02110-1335, USA.
20
11
 
21
12
; param.lisp -- bdd parameterization
22
13
 
38
29
(local (in-theory (enable eval-bdd eval-bdd-list ubddp ubdd-listp
39
30
                          q-compose q-compose-list)))
40
31
 
41
 
(make-event
42
 
 
43
 
; Disabling waterfall parallelism because this book allegedly uses memoization
44
 
; while performing its proofs.
45
 
 
46
 
 (if (and (hons-enabledp state) 
47
 
          (f-get-global 'parallel-execution-enabled state)) 
48
 
     (er-progn (set-waterfall-parallelism nil)
49
 
               (value '(value-triple nil)))
50
 
   (value '(value-triple nil))))
51
 
 
52
 
 
53
32
;; -------------------------------------------------------------------
54
33
;; Function Definitions
55
34
;; -------------------------------------------------------------------