Start of some debuggability when evaluating formula. check-rules-run …

…prints bad, missing sorted.

logic/expand-model.lisp

@@ -365,11 +365,19 @@
 	)
     ;; Report props in kb but not reference, but skip the equality assertions we added
     (loop for prop in (remove '= props :key 'car)
-	  if (not (member prop everything :test 'equalp)) do (incf bad) and do (print prop) else do (incf good))
+	  if (not (member prop everything :test 'equalp))
+	    do (incf bad)
+	    and collect prop into bad-ones
+	  else do (incf good)
+	  finally
+    	     (map nil 'print (sort bad-ones 'string-lessp :key 'princ-to-string)))
+
     (print "---")
 
     (loop for prop in everything
 	  if (not (member prop props :test 'equalp))
-	    sum 1 into missing and do (print prop)  
-	  finally (return (list (length base) good bad missing)))
+	    sum 1 into missing and collect prop into missing-ones
+	  finally 
+	     (map nil 'print (sort missing-ones 'string-lessp :key 'princ-to-string))
+	     (return (list (length base) good bad missing)))
     ))

logic/formula-tester.lisp

@@ -20,6 +20,8 @@
 (defmacro getenv ( &environment env)
   env)
 
+(defvar *debug-eval-formula* nil)
+
 (defun evaluate-formula (formula interpretation)
   "Take a logical formula and test against an interpretation given as the list of positive propositions. 
 Works by transforming the formula into a function, compiling it, and running it. The list macros are used 
@@ -46,7 +48,12 @@ to avoid consing, which can land up be quite a lot"
 			       (let ((success t))
 				 (dolist (,@vars universe)
 				   (unless ,body
-				     (return-from ,label (setq success nil))))
+				     (progn (when *debug-eval-formula*
+					      (when (member (car ',(third body)) '(list2 list3 list4 list5))
+						(let ((form ',(cdr (third body))))
+						  (setq form (list* (second (car form)) (cdr form)))
+						  (format t ":forall ~a missed ~a=~a~%"  form ',(first vars) ,(first vars)   ))))
+					    (return-from ,label (setq success nil)))))
 				 success)))
 			  `(:forall (,(car vars))
 			     (:forall (,@(cdr vars))
@@ -57,7 +64,12 @@ to avoid consing, which can land up be quite a lot"
 			    `(block ,label
 			       (dolist (,@vars universe nil)
 				 (if ,body
-				     (return-from ,label t)))))
+				     (return-from ,label t)))
+			       (when *debug-eval-formula*
+				 (when (member (car ',(third body)) '(list2 list3 list4 list5))
+				   (let ((form ',(cdr (third body))))
+				     (setq form (list* (second (car form)) (cdr form)))
+				     (format t ":exists ~a no success~%"  form    ))))))
 			  `(:exists (,(car vars))
 			     (:exists (,@(cdr vars))
 			       ,body))))