Skip to content

Commit

Permalink
Merge branch 'owlapiv4' of https://github.com/alanruttenberg/lsw2 int…
Browse files Browse the repository at this point in the history
…o owlapiv4
  • Loading branch information
alanruttenberg committed Feb 14, 2018
2 parents 45ccba3 + f2e453c commit e29de4f
Showing 1 changed file with 11 additions and 1 deletion.
12 changes: 11 additions & 1 deletion logic/axiom.lisp
Original file line number Diff line number Diff line change
Expand Up @@ -265,7 +265,17 @@

;; return predicates, constants, function symbols in formula
(defun formula-elements (sexp)
(when (not (keywordp (car sexp)))
;; expecting an sexp but accept a spec.
;; sexp might be missing :fact
;; spec can be '(:name ...) '((:kind ..))) ((:forall ..))
;; it's a spec if
;; 1) it starts with a keyword other than :forall ...
;; 2) the first element is an axiom
;; 3) The first element is a list
(when (or (and (keywordp (car sexp))
(not (member (car sexp) '(:forall :exists :and :or :iff :implies := :not))))
(consp (car sexp))
(typep (car sexp) 'axiom))
(setq sexp `(:and ,@(mapcar 'axiom-sexp (collect-axioms-from-spec sexp)))))
(let ((predicates nil)
(constants nil)
Expand Down

0 comments on commit e29de4f

Please sign in to comment.