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
|
;; Copyright (C) 2015, University of British Columbia
;; Written by Yan Peng (August 2nd 2016)
;;
;; License: A 3-clause BSD license.
;; See the LICENSE file distributed with ACL2
;;
(in-package "ACL2")
;; load other packages needed to define our new packages...
(include-book "std/portcullis" :dir :system)
(include-book "centaur/fty/portcullis" :dir :system)
(include-book "centaur/sv/tutorial/support" :dir :system)
;; define our new packages
(defpkg "SMT"
(set-difference-eq
(union-eq
*acl2-exports*
*standard-acl2-imports*
*common-lisp-symbols-from-main-lisp-package*
;; Things we want to export
'()
;; Things we want to import
'(b*
define
defconsts
more-returns
l<
tshell-ensure
tshell-call
set-raw-mode-on
defines
defxdoc
defsection
def-join-thms
termify-clause-set
body
lambda-formals
lambda-body
pseudo-lambdap
conjoin-clauses
conjoin
conjoin2
disjoin
disjoin2
disjoin-lst
pseudo-term-list-listp
iff-implies-equal-not
split-keyword-alist
dumb-negate-lit
must-succeed
prefixp
symbol-fix
symbol-list-fix
with-fast-alists
formals
strip-cadrs
bfix
real/rationalp
read-string
str::cat
str::nat-to-dec-string
str::strtok
str::count
str::substrp
str::isubstrp
str::strpos
str::firstn-chars
str::strval
str::search
str::nat-to-hex-chars
str::hex-digit-char-list*p
str::charlisteqv
str::character-list-fix
str::str-fix
str::downcase-string
std::defaggregate
std::defval
fty::defprod
fty::deflist
fty::deffixtype
fty::defalist
fty::defoption
sv::def-saved-event
sv::deftutorial
sv::$
)
)
;; Things to remove
'(true-list-fix ; removed by Matt K. 12/2018, when added to *acl2-exports*
good-atom-listp)))
|
