Some patches for EL optimizations

source/abox.lisp

@@ -962,7 +962,7 @@
 		  (unless hierarchy-p
 		    (unless role
 		      (setf role (get-tbox-role tbox role-name)))
-		    (when (role-has-ancestors-p role)
+		    (when (rest (rest (role-ancestors-internal role)))
 		      (setf hierarchy-p t)
 		      (setf (abox-language abox) (add-dl-simple-role-inclusions (abox-language abox)))))
 		  (unless complex-roles-p

source/gci-absorption.lisp

@@ -715,7 +715,15 @@
              #+:debug (atomic-concept-p qualification)
              (if (is-top-concept-p qualification)
                  (progn
-                   (push rhs-concept (role-domain-concept role))
+                   (let ((domain (role-domain-concept role)))
+                     (unless (listp domain)
+                       (setf (role-domain-concept role) (list domain))))
+                   (pushnew rhs-concept (role-domain-concept role))
+                   (let ((role-inverse (role-inverse-internal role)))
+                     (let ((inverse-range (role-range-concept role-inverse)))
+                       (unless (listp inverse-range)
+                         (setf (role-range-concept role-inverse) (list inverse-range))))
+                     (pushnew rhs-concept (role-range-concept role-inverse)))
                    (race-trace ("~&Absorbing EL+ simple domain restriction (implies ~S ~S) into role ~S~%"
                                 lhs rhs-concept role)))
                (let* ((el+-role-domain-qualifications
@@ -756,24 +764,16 @@
             (encode-concept-term encoded-definition concept))))
   (loop for role in (append *provisionally-inserted-roles* (tbox-encoded-role-list tbox)) do
         (unless (or (is-predefined-role-p role) (role-datatype role))
-          (let ((domain (or (role-domain-restriction role) (role-domain-concept role))))
+          (let ((domain (or (role-domain-concept role) (role-domain-restriction role))))
             (when domain
-              (if (listp domain)
-                  (progn
-                    #+:debug (assert (every #'concept-p-internal domain))
-                    (setf (role-domain-concept role) `(and .,(mapcar #'decode-concept domain))))
-                (progn
-                  ;;#+:debug (concept-p-internal domain) SBCL does not seem to like this!
-                  (setf (role-domain-concept role) (decode-concept domain))))))
-          (let ((range (or (role-range-restriction role) (role-range-concept role))))
+              (if (and (listp domain) (not (eq (first domain) 'not)))
+                  (setf (role-domain-concept role) `(and .,(mapcar #'decode-concept domain)))
+                (setf (role-domain-concept role) (decode-concept domain)))))
+          (let ((range (or (role-range-concept role) (role-range-restriction role))))
             (when range
-              (if (listp range)
-                  (progn
-                    #+:debug (assert (every #'concept-p-internal range))
-                    (setf (role-range-concept role) `(and .,(mapcar #'decode-concept range))))
-                (progn
-                  ;;#+:debug (concept-p-internal range)  SBCL does not seem to like this!
-                  (setf (role-range-concept role) (decode-concept range))))))))
+              (if (and (listp range) (not (eq (first range) 'not)))
+                  (setf (role-range-concept role) `(and .,(mapcar #'decode-concept range)))
+                (setf (role-range-concept role) (decode-concept range)))))))
   (tbox-nary-absorption-table tbox))
 
 (defun create-nary-disjointness-axioms (tbox gcis)

source/tbox.lisp

@@ -3999,7 +3999,7 @@ Always create a canonical name regardless of the order of the role parents."
                          (role-range-concept role)
                          ))
             (setf blocking-possibly-required t)))
-	(when (and (not hierarchy-p) (role-has-ancestors-p role))
+	(when (and (not hierarchy-p) (rest (rest (role-ancestors-internal role))))
 	  (setf hierarchy-p t))
 	(when (and (not complex-roles-p) (role-compositions role))
 	  (setf complex-roles-p t))
@@ -9113,9 +9113,11 @@ Always create a canonical name regardless of the order of the role parents."
           (process-subsumption-axiom lhs *bottom-concept* environment))
         (process-subsumption-implied-edges lhs role rhs environment)
         (process-role-domains lhs role rhs environment)
+        (process-role-range lhs role rhs environment)
         (process-role-compositions lhs role rhs environment)
         (loop for (l-lhs . l-rhs) in added-transitive-edges do
               (process-role-domains l-lhs role l-rhs environment)
+              (process-role-range l-lhs role l-rhs environment)
               (process-role-compositions l-lhs role l-rhs environment))
         (process-super-role-edges (cons (cons lhs rhs) added-transitive-edges) role environment)))))
 
@@ -9166,6 +9168,17 @@ Always create a canonical name regardless of the order of the role parents."
                     (when (member domain-role role-ancestors)
                       (process-subsumption-axioms lhs domains environment))))))))
 
+(defun process-role-range (lhs role rhs environment)
+  #+:debug 
+  (assert (or (and (atomic-concept-p lhs) (atomic-concept-p rhs))
+              (and (individual-p-internal lhs)
+                   (or (atomic-concept-p rhs) (individual-p-internal rhs)))))
+  (let ((range (role-range-restriction role)))
+    (when range
+      #+:debug (or (atomic-concept-p range) (and-concept-p range))
+      (process-subsumption-axioms rhs range environment)))
+  )
+
 (defun process-role-compositions (lhs role rhs environment)
   #+:debug 
   (assert (or (and (atomic-concept-p lhs) (atomic-concept-p rhs))