Fixed degraded term memoization in rewriting.
tswd
8 years ago
976 | 976 | ;; compute the normal form of "term" |
977 | 977 | (reduce-term term strategy) |
978 | 978 | (setq normal-form term) |
979 | #| | |
979 | 980 | (unless (= rule-count (number-rewritings)) |
980 | 981 | (when *memo-debug* |
981 | 982 | (when (term-equational-equal term-nu normal-form) |
986 | 987 | (format t "~%(~d) new = " (number-rewritings)) |
987 | 988 | (term-print-with-sort normal-form)))) |
988 | 989 | ;; store the normal form |
989 | (set-hashed-term term-nu *term-memo-table* normal-form)))) | |
990 | (set-hashed-term term-nu *term-memo-table* normal-form)) | |
991 | |# | |
992 | (set-hashed-term term-nu *term-memo-table* normal-form))) | |
990 | 993 | normal-form)) |
991 | 994 | |
992 | 995 | (defmacro check-closed-world-assumption (?term) |