← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/projects/taspi/code/gen-helper/bdd-functions.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/projects/taspi/code/gen-helper/bdd-functions.lisp
5
5
(in-package "ACL2")
6
6
(include-book "sets")
7
7
 
8
 
(make-event
9
 
 
10
 
; ; David Rager, 3/1/2013: Disabling waterfall parallelism because this book
11
 
; allegedly uses memoization while performing its proofs.
12
 
 
13
 
 (if (and (hons-enabledp state) 
14
 
          (f-get-global 'parallel-execution-enabled state)) 
15
 
     (er-progn (set-waterfall-parallelism nil)
16
 
               (value '(value-triple nil)))
17
 
   (value '(value-triple nil)))
18
 
 :check-expansion nil)
19
 
 
20
8
(defmacro qcons (x y)
21
9
  ;; should this be called qhons?
22
10
  `(cond ((or (and (eq ,x t)   (eq ,y t))
174
162
(dis+ind q-and)
175
163
 
176
164
(defun q-no-conflicts (x list)
177
 
  ":Doc-Section TASPI
178
 
   Determines if bipartition x is consistent with each of those in list. ~/
179
 
   ~/
180
 
   Arguments: 
181
 
     (1) x - a bipartition                                                
182
 
     (2) list - a list of bipartitions
183
 
 
184
 
   Details: Set operations are used to determine if the bipartition x does not
185
 
            conflict with each of the bipartitions in list.  Bipartitions must
186
 
            be bdd based (as opposed to list based) and the underlying taxa list
187
 
            must be preserved between x and each member of list. 
188
 
            The bipartitions are assumed to be ordered such that no bipartition
189
 
            x following y in list exists such that y is a subset of x and x=/y.
190
 
            See also no-conflicts (list based)."
 
165
 
 
166
;;; Legacy doc string replaced Nov. 2014 by auto-generated defxdoc form;
 
167
;;; see projects/taspi/taspi-xdoc.lisp.
 
168
 
 
169
; ":Doc-Section TASPI
 
170
;  Determines if bipartition x is consistent with each of those in list. ~/
 
171
;  ~/
 
172
;  Arguments: 
 
173
;    (1) x - a bipartition                                                
 
174
;    (2) list - a list of bipartitions
 
175
 
 
176
;  Details: Set operations are used to determine if the bipartition x does not
 
177
;           conflict with each of the bipartitions in list.  Bipartitions must
 
178
;           be bdd based (as opposed to list based) and the underlying taxa list
 
179
;           must be preserved between x and each member of list. 
 
180
;           The bipartitions are assumed to be ordered such that no bipartition
 
181
;           x following y in list exists such that y is a subset of x and x=/y.
 
182
;           See also no-conflicts (list based)."
191
183
  (declare (xargs :guard t))
192
184
  (if (consp list)
193
185
      (if (q-and x (car list))
211
203
(dis+ind q-no-conflicts)
212
204
 
213
205
(defun q-no-conflicts-gen (x list)
214
 
  ":Doc-Section TASPI
215
 
   Determines if bipartition x is consistent with each of those in list. ~/
216
 
   ~/
217
 
   Arguments: 
218
 
     (1) x - a bipartition                                                
219
 
     (2) list - a list of bipartitions
220
 
 
221
 
   Details: Set operations are used to determine if the bipartition x does not
222
 
            conflict with each of the bipartitions in list.  Bipartitions must
223
 
            be bdd based (as opposed to list based) and the underlying taxa list
224
 
            must be preserved between x and each member of list. 
225
 
            Assumes no ordering of bipartitions in list.
226
 
            See also q-no-conflicts."
 
206
 
 
207
;;; Legacy doc string replaced Nov. 2014 by auto-generated defxdoc form;
 
208
;;; see projects/taspi/taspi-xdoc.lisp.
 
209
 
 
210
; ":Doc-Section TASPI
 
211
;  Determines if bipartition x is consistent with each of those in list. ~/
 
212
;  ~/
 
213
;  Arguments: 
 
214
;    (1) x - a bipartition                                                
 
215
;    (2) list - a list of bipartitions
 
216
 
 
217
;  Details: Set operations are used to determine if the bipartition x does not
 
218
;           conflict with each of the bipartitions in list.  Bipartitions must
 
219
;           be bdd based (as opposed to list based) and the underlying taxa list
 
220
;           must be preserved between x and each member of list. 
 
221
;           Assumes no ordering of bipartitions in list.
 
222
;           See also q-no-conflicts."
227
223
  (declare (xargs :guard t))
228
224
  (if (consp list)
229
225
      (if (q-and x (car list))
234
230
    t))
235
231
 
236
232
(defun q-no-conflicts-list (list)
237
 
   ":Doc-Section TASPI
238
 
   Determines if the list of bipartitions list is consistent. ~/
239
 
   ~/
240
 
   Arguments: 
241
 
     (1) list - a list of bipartitions
242
 
 
243
 
   Details: Set operations are used to determine if the list of bipartitions 
244
 
            do not conflict.  Bipartitions must be list based (as opposed to
245
 
            bdd based), and an underlying taxa list must be preserved between
246
 
            every pair of bipartitions in the list. The bipartitions are 
247
 
            assumed to be ordered such that no bipartition x following y in
248
 
            list exists such that y is a subset of x and x=/y.
249
 
            See also no-conflicts-list (list based) and q-no-conflicts-list-gen."
 
233
 
 
234
;;; Legacy doc string replaced Nov. 2014 by auto-generated defxdoc form;
 
235
;;; see projects/taspi/taspi-xdoc.lisp.
 
236
 
 
237
;  ":Doc-Section TASPI
 
238
;  Determines if the list of bipartitions list is consistent. ~/
 
239
;  ~/
 
240
;  Arguments: 
 
241
;    (1) list - a list of bipartitions
 
242
 
 
243
;  Details: Set operations are used to determine if the list of bipartitions 
 
244
;           do not conflict.  Bipartitions must be list based (as opposed to
 
245
;           bdd based), and an underlying taxa list must be preserved between
 
246
;           every pair of bipartitions in the list. The bipartitions are 
 
247
;           assumed to be ordered such that no bipartition x following y in
 
248
;           list exists such that y is a subset of x and x=/y.
 
249
;           See also no-conflicts-list (list based) and q-no-conflicts-list-gen."
250
250
  (declare (xargs :guard t))
251
251
  (if (consp list)
252
252
      (and (q-no-conflicts (car list) (cdr list))
266
266
(dis+ind q-no-conflicts-list)
267
267
 
268
268
(defun q-no-conflicts-list-gen (list)
269
 
   ":Doc-Section TASPI
270
 
   Determines if the list of bipartitions list is consistent. ~/
271
 
   ~/
272
 
   Arguments: 
273
 
     (1) list - a list of bipartitions
274
 
 
275
 
   Details: Set operations are used to determine if the list of bipartitions 
276
 
            do not conflict.  Bipartitions must be list based (as opposed to
277
 
            bdd based), and an underlying taxa list must be preserved between
278
 
            every pair of bipartitions in the list. No ordering on the 
279
 
            bipartitions is assumed.
280
 
            See also q-no-conflicts-list."
 
269
 
 
270
;;; Legacy doc string replaced Nov. 2014 by auto-generated defxdoc form;
 
271
;;; see projects/taspi/taspi-xdoc.lisp.
 
272
 
 
273
;  ":Doc-Section TASPI
 
274
;  Determines if the list of bipartitions list is consistent. ~/
 
275
;  ~/
 
276
;  Arguments: 
 
277
;    (1) list - a list of bipartitions
 
278
 
 
279
;  Details: Set operations are used to determine if the list of bipartitions 
 
280
;           do not conflict.  Bipartitions must be list based (as opposed to
 
281
;           bdd based), and an underlying taxa list must be preserved between
 
282
;           every pair of bipartitions in the list. No ordering on the 
 
283
;           bipartitions is assumed.
 
284
;           See also q-no-conflicts-list."
281
285
  (declare (xargs :guard t))
282
286
  (if (consp list)
283
287
      (and (q-no-conflicts-gen (car list) (cdr list))
286
290
 
287
291
; Finds bipartitions in l that refine bipartition tree.
288
292
(defun subtrees-implying (branch l)
289
 
  ":Doc-Section TASPI
290
 
   Returns bipartitions that refine a tree *below* the branch given.~/
291
 
   ~/
292
 
   Arguments:
293
 
      (1) branch - a bdd based bipartition
294
 
      (2) l - a list of bdd based bipartitions
295
 
 
296
 
   Details: All bipartitions must be based on the same taxa list.  
297
 
            *Below* is defined in terms of the rooting given by taxa list."
 
293
 
 
294
;;; Legacy doc string replaced Nov. 2014 by auto-generated defxdoc form;
 
295
;;; see projects/taspi/taspi-xdoc.lisp.
 
296
 
 
297
; ":Doc-Section TASPI
 
298
;  Returns bipartitions that refine a tree *below* the branch given.~/
 
299
;  ~/
 
300
;  Arguments:
 
301
;     (1) branch - a bdd based bipartition
 
302
;     (2) l - a list of bdd based bipartitions
 
303
 
 
304
;  Details: All bipartitions must be based on the same taxa list.  
 
305
;           *Below* is defined in terms of the rooting given by taxa list."
298
306
  (declare (xargs :guard t))
299
307
  (cond ((atom l) nil)
300
308
        ((qs-subset (car l) branch)
317
325
(dis+ind subtrees-implying)
318
326
 
319
327
(defun subtrees-not-implying (branch l)
320
 
   ":Doc-Section TASPI
321
 
   Returns bipartitions that are not *below* the branch given.~/
322
 
   ~/
323
 
   Arguments:
324
 
      (1) branch - a bdd based bipartition
325
 
      (2) l - a list of bdd based bipartitions
326
 
 
327
 
   Details: All bipartitions must be based on the same taxa list.  
328
 
            *Below* is defined in terms of the rooting given by taxa list."
 
328
 
 
329
;;; Legacy doc string replaced Nov. 2014 by auto-generated defxdoc form;
 
330
;;; see projects/taspi/taspi-xdoc.lisp.
 
331
 
 
332
;  ":Doc-Section TASPI
 
333
;  Returns bipartitions that are not *below* the branch given.~/
 
334
;  ~/
 
335
;  Arguments:
 
336
;     (1) branch - a bdd based bipartition
 
337
;     (2) l - a list of bdd based bipartitions
 
338
 
 
339
;  Details: All bipartitions must be based on the same taxa list.  
 
340
;           *Below* is defined in terms of the rooting given by taxa list."
329
341
  (declare (xargs :guard t))
330
342
  (cond ((atom l) nil)
331
343
        ((not (qs-subset (car l) branch))