1 files changed, 37 insertions, 0 deletions
diff --git a/books/workshops/2015/peng-greenstreet/support/config.lisp b/books/workshops/2015/peng-greenstreet/support/config.lisp
new file mode 100644
index 0000000..42b3871
--- /dev/null
+++ b/books/workshops/2015/peng-greenstreet/support/config.lisp
@@ -0,0 +1,37 @@
+;; Copyright (C) 2015, University of British Columbia
+;; Written (originally) by Yan Peng (13th March, 2014)
+;;
+;; License: A 3-clause BSD license.
+;; See the LICENSE file distributed with this software
+
+
+(in-package "ACL2")
+(include-book "std/util/defaggregate" :dir :system)
+
+(std::defaggregate smtlink-config
+  (dir-interface
+   dir-files
+   SMT-module
+   SMT-class
+   smt-cmd
+   dir-expanded)
+  :tag :smtlink-config)
+
+(defconst *default-smtlink-config*
+  (make-smtlink-config :dir-interface nil
+                       :dir-files nil
+                       :SMT-module "ACL2_to_Z3"
+                       :SMT-class "ACL22SMT"
+                       :smt-cmd "/usr/local/bin/python"
+                       :dir-expanded nil))
+
+(encapsulate
+  (((smt-cnf) => *))
+  (local (defun smt-cnf ()
+	   *default-smtlink-config*)))
+
+(defun default-smtlink-config ()
+  (declare (xargs :guard t))
+  (change-smtlink-config *default-smtlink-config*))
+
+(defattach smt-cnf default-smtlink-config)