1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
|
; Making the dag-variable-alist
;
; Copyright (C) 2008-2011 Eric Smith and Stanford University
; Copyright (C) 2013-2024 Kestrel Institute
; Copyright (C) 2016-2020 Kestrel Technology, LLC
;
; License: A 3-clause BSD license. See the file books/3BSD-mod.txt.
;
; Author: Eric Smith (eric.smith@kestrel.edu)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(in-package "ACL2")
(include-book "dag-variable-alist")
(include-book "dag-arrays")
(local (include-book "kestrel/acl2-arrays/acl2-arrays" :dir :system))
;;;
;;; make-dag-variable-alist-aux
;;;
;returns the dag-variable-alist.
;if we have the dag-lst in hand, can we do better?
(defund make-dag-variable-alist-aux (n ;counts up
dag-array-name dag-array dag-len
;;gets populated:
dag-variable-alist)
(declare (xargs :measure (nfix (+ 1 (- dag-len n)))
:guard (and (pseudo-dag-arrayp dag-array-name dag-array dag-len)
(natp n)
(<= n dag-len)
(dag-variable-alistp dag-variable-alist))))
(if (or (>= n dag-len)
(not (mbt (natp n)))
(not (mbt (natp dag-len))))
dag-variable-alist
(let* ((expr (aref1 dag-array-name dag-array n)))
(make-dag-variable-alist-aux (+ 1 n)
dag-array-name dag-array dag-len
(if (atom expr) ;tests for variable
(add-to-dag-variable-alist expr n dag-variable-alist)
dag-variable-alist)))))
(defthm dag-variable-alistp-of-make-dag-variable-alist-aux
(implies (and (dag-variable-alistp dag-variable-alist)
(pseudo-dag-arrayp-aux dag-array-name dag-array (+ -1 dag-len)))
(dag-variable-alistp (make-dag-variable-alist-aux n dag-array-name dag-array dag-len dag-variable-alist)))
:hints (("Goal" :in-theory (enable make-dag-variable-alist-aux))))
(defthm all-<-of-strip-cdrs-of-make-dag-variable-alist-aux
(implies (and ;(pseudo-dag-arrayp-aux dag-array-name dag-array (+ -1 dag-len))
(all-< (strip-cdrs dag-variable-alist) dag-len)
)
(all-< (strip-cdrs (make-dag-variable-alist-aux n dag-array-name dag-array dag-len dag-variable-alist))
dag-len))
:hints (("Goal" :in-theory (enable make-dag-variable-alist-aux))))
(defthm bounded-dag-variable-alistp-of-make-dag-variable-alist-aux
(implies (and (pseudo-dag-arrayp-aux dag-array-name dag-array (+ -1 dag-len))
(bounded-dag-variable-alistp dag-variable-alist dag-len))
(bounded-dag-variable-alistp (make-dag-variable-alist-aux n dag-array-name dag-array dag-len dag-variable-alist)
dag-len))
:hints (("Goal" :in-theory (enable make-dag-variable-alist-aux))))
(defthm member-equal-of-strip-cars-of-make-dag-variable-alist-aux
(implies (member-equal var (strip-cars dag-variable-alist))
(member-equal var (strip-cars (make-dag-variable-alist-aux n dag-array-name dag-array dag-len dag-variable-alist))))
:hints (("Goal" :in-theory (enable make-dag-variable-alist-aux))))
(defthm member-equal-of-aref1-and-strip-cars-of-make-dag-variable-alist-aux
(implies (and (not (consp (aref1 dag-array-name dag-array nodenum)))
(pseudo-dag-arrayp dag-array-name dag-array dag-len)
(natp nodenum)
(< nodenum dag-len)
(<= n nodenum)
(natp n))
(member-equal (aref1 dag-array-name dag-array nodenum)
(strip-cars (make-dag-variable-alist-aux n dag-array-name dag-array dag-len dag-variable-alist))))
:hints (("Goal" :in-theory (enable make-dag-variable-alist-aux))))
(defthm make-dag-variable-alist-aux-base
(equal (make-dag-variable-alist-aux dag-len dag-array-name array dag-len dag-variable-alist)
dag-variable-alist)
:hints (("Goal" :expand (make-dag-variable-alist-aux dag-len dag-array-name array dag-len dag-variable-alist)
:in-theory (enable make-dag-variable-alist-aux))))
(defthm make-dag-variable-alist-aux-of-aset1-expandable
(implies (and (natp dag-len)
(natp n)
(<= n dag-len)
(< dag-len *max-1d-array-length*)
(pseudo-dag-arrayp dag-array-name dag-array dag-len))
(equal (make-dag-variable-alist-aux n dag-array-name (aset1-expandable dag-array-name dag-array dag-len expr) (+ 1 dag-len) dag-variable-alist)
(if (consp expr)
(make-dag-variable-alist-aux n dag-array-name dag-array dag-len dag-variable-alist)
(add-to-dag-variable-alist expr dag-len (make-dag-variable-alist-aux n dag-array-name dag-array dag-len dag-variable-alist)))))
:hints (("Goal" :expand ((make-dag-variable-alist-aux n dag-array-name
(aset1-expandable dag-array-name dag-array dag-len expr)
(+ 1 dag-len)
dag-variable-alist)
(make-dag-variable-alist-aux dag-len dag-array-name
(aset1-expandable dag-array-name dag-array dag-len var)
(+ 1 dag-len)
dag-variable-alist))
:in-theory (enable make-dag-variable-alist-aux))))
;;;
;;; make-dag-variable-alist
;;;
;; See also make-dag-indices.
(defund make-dag-variable-alist (dag-array-name dag-array dag-len)
(declare (xargs :guard (pseudo-dag-arrayp dag-array-name dag-array dag-len)))
(make-dag-variable-alist-aux 0 dag-array-name dag-array dag-len (empty-dag-variable-alist)))
(defthm dag-variable-alistp-of-make-dag-variable-alist
(implies (pseudo-dag-arrayp dag-array-name dag-array dag-len)
(dag-variable-alistp (make-dag-variable-alist dag-array-name dag-array dag-len)))
:hints (("Goal" :in-theory (enable make-dag-variable-alist pseudo-dag-arrayp))))
(defthm make-dag-variable-alist-of-0
(equal (make-dag-variable-alist dag-array-name dag-array 0)
(empty-dag-variable-alist))
:hints (("Goal" :in-theory (enable make-dag-variable-alist))))
(defthm all-<-of-strip-cdrs-of-make-dag-variable-alist
(implies (pseudo-dag-arrayp dag-array-name dag-array dag-len)
(all-< (strip-cdrs (make-dag-variable-alist dag-array-name dag-array dag-len))
dag-len))
:hints (("Goal" :in-theory (enable make-dag-variable-alist pseudo-dag-arrayp))))
(defthm bounded-dag-variable-alistp-of-make-dag-variable-alist
(implies (pseudo-dag-arrayp dag-array-name dag-array dag-len)
(bounded-dag-variable-alistp (make-dag-variable-alist dag-array-name dag-array dag-len) dag-len))
:hints (("Goal" :in-theory (enable make-dag-variable-alist pseudo-dag-arrayp))))
(defthm member-equal-of-aref1-and-strip-cars-of-make-dag-variable-alist
(implies (and (not (consp (aref1 dag-array-name dag-array nodenum)))
(pseudo-dag-arrayp dag-array-name dag-array dag-len)
(natp nodenum)
(< nodenum dag-len))
(member-equal (aref1 dag-array-name dag-array nodenum)
(strip-cars (make-dag-variable-alist dag-array-name dag-array dag-len))))
:hints (("Goal" :in-theory (enable make-dag-variable-alist))))
;covers extending the dag by one node
(defthm make-dag-variable-alist-of-aset1-expandable
(implies (and (natp dag-len)
(< dag-len *max-1d-array-length*)
(pseudo-dag-arrayp dag-array-name dag-array dag-len))
(equal (make-dag-variable-alist dag-array-name (aset1-expandable dag-array-name dag-array dag-len expr) (+ 1 dag-len))
(if (consp expr)
(make-dag-variable-alist dag-array-name dag-array dag-len)
(add-to-dag-variable-alist expr dag-len (make-dag-variable-alist dag-array-name dag-array dag-len)))))
:hints (("Goal" :expand ((make-dag-variable-alist-aux
0 dag-array-name
(aset1-expandable dag-array-name dag-array dag-len expr)
(+ 1 dag-len)
nil))
:in-theory (enable make-dag-variable-alist make-dag-variable-alist-aux))))
;drop?
(defthm <-of-cdr-of-assoc-equal-when-all-<-of-strip-cdrs
(implies (and (all-< (strip-cdrs alist) bound)
(ASSOC-EQUAL key alist))
(< (CDR (ASSOC-EQUAL key alist)) bound)))
;; (defthm <-of-cdr-of-assoc-equal-of-make-dag-variable-alist-aux
;; (implies (and (assoc-equal var (make-dag-variable-alist-aux n dag-array-name dag-array dag-len dag-variable-alist))
;; (bounded-dag-variable-alistp dag-variable-alist dag-len)
;; ;; (pseudo-dag-arrayp-aux dag-array-name dag-array (+ -1 dag-len))
;; ;;(<= n dag-len)
;; )
;; (< (cdr (assoc-equal var (make-dag-variable-alist-aux n dag-array-name dag-array dag-len dag-variable-alist)))
;; dag-len))
;; :hints (("Goal" :in-theory (enable make-dag-variable-alist-aux bounded-dag-variable-alistp))))
;; (defthm <-of-cdr-of-assoc-equal-of-make-dag-variable-alist
;; (implies (assoc-equal var (make-dag-variable-alist 'dag-array dag-array dag-len))
;; (< (cdr (assoc-equal var (make-dag-variable-alist 'dag-array dag-array dag-len)))
;; dag-len))
;; :hints (("Goal" :in-theory (enable make-dag-variable-alist))))
;; (defthm <-of-cdr-of-assoc-equal-of-make-dag-variable-alist-alt
;; (implies (and (<= dag-len bound)
;; (assoc-equal var (make-dag-variable-alist 'dag-array dag-array dag-len)))
;; (< (cdr (assoc-equal var (make-dag-variable-alist 'dag-array dag-array dag-len)))
;; bound))
;; :hints (("Goal" :use (:instance <-of-cdr-of-assoc-equal-of-make-dag-variable-alist)
;; :in-theory (disable <-of-cdr-of-assoc-equal-of-make-dag-variable-alist))))
|
