rairlab/Spectra
1
0
Fork 0
mirror of https://github.com/RAIRLab/Spectra.git synced 2025-10-05 22:21:20 +00:00
Code Issues Projects Releases Packages Wiki Activity

Some more tweaks

Browse source
This commit is contained in:
Naveen Sundar Govindarajulu 2017-01-18 22:58:41 -05:00
parent afde7793e5
commit d1e0cb891a
7 changed files with 55 additions and 54 deletions
Download patch file Download diff file Expand all files Collapse all files

18
snark-20120808r02/snark-interface.lisp
View file

@ -66,14 +66,14 @@
(setup-snark :time-limit time-limit :verbose verbose)
(if sortal-setup-fn (funcall sortal-setup-fn))
(let* ((n-a (make-hash-table :test #'equalp))
(a-n (make-hash-table :test #'equalp)))
(a-n (make-hash-table :test #'equalp))
)
(mapcar (lambda (axiom)
(let ((name (gensym)))
(setf (gethash (princ-to-string axiom) a-n) name)
(setf (gethash (princ-to-string name) n-a) axiom))) axioms)
(mapcar (lambda (axiom)
(snark::assert axiom :name (gethash (princ-to-string axiom) a-n)
))
(snark::assert axiom))
(mapcar #'!@ axioms))
(if (equalp :PROOF-FOUND (snark:prove (!@ f)))
(list t (remove nil
@ -101,8 +101,7 @@
(setf (gethash (princ-to-string axiom) a-n) name)
(setf (gethash (princ-to-string name) n-a) axiom))) axioms)
(mapcar (lambda (axiom)
(snark::assert axiom :name (gethash (princ-to-string axiom) a-n)
))
(snark::assert axiom))
(mapcar #'!@ axioms))
(if (equalp :PROOF-FOUND (snark:prove (!@ f)))
"YES"
@ -126,8 +125,7 @@
(setf (gethash (princ-to-string axiom) a-n) name)
(setf (gethash (princ-to-string name) n-a) axiom))) axioms)
(mapcar (lambda (axiom)
(snark::assert axiom :name (gethash (princ-to-string axiom) a-n)
))
(snark::assert axiom))
(mapcar #'!@ axioms))
(let ((proof (snark:prove (!@ f) :answer (!@ (list 'ans var)) )))
@ -154,8 +152,7 @@
(setf (gethash (princ-to-string axiom) a-n) name)
(setf (gethash (princ-to-string name) n-a) axiom))) axioms)
(mapcar (lambda (axiom)
(snark::assert axiom :name (gethash (princ-to-string axiom) a-n)
))
(snark::assert axiom))
(mapcar #'!@ axioms))
(let ((proof (snark:prove (!@ f) :answer (!@ (cons 'ans vars)) )))
@ -179,8 +176,7 @@
(setf (gethash (princ-to-string axiom) a-n) name)
(setf (gethash (princ-to-string name) n-a) axiom))) axioms)
(mapcar (lambda (axiom)
(snark::assert axiom :name (gethash (princ-to-string axiom) a-n)
))
(snark::assert axiom))
(mapcar #'!@ axioms))
(let ((proof (snark:prove (!@ f) :answer (!@ (cons 'ans vars)) )))