| 109 | 109 |
;;; each non _and_ or _xor_ boolean sub-term is abstracted by a
|
| 110 | 110 |
;;; variable.
|
| 111 | 111 |
(defstruct (abst-bterm (:print-function print-abst-bterm))
|
| 112 | |
; by variables
|
|
112 |
(module nil) ; context module
|
| 113 | 113 |
(term nil) ; the original term
|
| 114 | 114 |
(subst nil) ; list of substitution
|
| 115 | 115 |
; or instance of abst-bterm(for _and_ abstraction)
|
|
| 166 | 166 |
(list-ac-subterms term *bool-and*)
|
| 167 | 167 |
nil))
|
| 168 | 168 |
|
| 169 | |
(defun make-and-abstraction (term subterms)
|
|
169 |
(defun make-and-abstraction (term subterms module)
|
| 170 | 170 |
(let ((subst nil))
|
| 171 | 171 |
(dolist (sub subterms)
|
| 172 | 172 |
(push (cons (get-hashed-bterm-variable sub) sub) subst))
|
| 173 | |
(make-abst-and :term term :subst (nreverse subst))))
|
| 174 | |
|
| 175 | |
(defun abstract-boolean-term (term)
|
| 176 | |
(let ((bterm (make-abst-bterm :term term))
|
|
173 |
(make-abst-and :term term :subst (nreverse subst) :module module)))
|
|
174 |
|
|
175 |
(defun abstract-boolean-term (term module)
|
|
176 |
(let ((bterm (make-abst-bterm :term term :module module))
|
| 177 | 177 |
(xor-subs (xtract-xor-subterms term))
|
| 178 | 178 |
(subst nil))
|
| 179 | 179 |
;; reset variable number & term hash
|
|
| 184 | 184 |
(dolist (xs xor-subs)
|
| 185 | 185 |
(let ((as (xtract-and-subterms xs)))
|
| 186 | 186 |
(if as
|
| 187 | |
(push (make-and-abstraction xs as) subst)
|
|
187 |
(push (make-and-abstraction xs as module) subst)
|
| 188 | 188 |
(push (cons (get-hashed-bterm-variable xs) xs) subst))))
|
| 189 | 189 |
;; top operator is not xor
|
| 190 | 190 |
(let ((as (xtract-and-subterms term)))
|
| 191 | |
(when as
|
| 192 | |
(push (make-and-abstraction term as) subst))))
|
|
191 |
(if as
|
|
192 |
(push (make-and-abstraction term as module) subst)
|
|
193 |
;; we anly accept xor-and formal form
|
|
194 |
(with-output-chaos-error ('invalid-term)
|
|
195 |
(format t "Given term is not xor-and normal form.")))))
|
| 193 | 196 |
(setf (abst-bterm-subst bterm) (nreverse subst))
|
| 194 | 197 |
bterm))
|
| 195 | 198 |
|
|
| 318 | 321 |
;;; resolve-abst-bterm : bterm
|
| 319 | 322 |
;;; retuns a list of substitution which makes bterm to be true.
|
| 320 | 323 |
;;;
|
|
324 |
(defvar .maximum-bterm-vars. 7)
|
|
325 |
|
| 321 | 326 |
(defun resolve-abst-bterm (bterm &optional (module (get-context-module)))
|
| 322 | 327 |
(declare (type abst-bterm bterm))
|
| 323 | |
(let* ((abst-term (make-bterm-representation bterm))
|
| 324 | |
(variables (term-variables abst-term))
|
| 325 | |
(list-subst (assign-tf variables))
|
| 326 | |
(answers nil))
|
| 327 | |
(dolist (subst list-subst)
|
| 328 | |
(let ((target (substitution-image-cp subst abst-term)))
|
| 329 | |
(reset-reduced-flag target)
|
| 330 | |
(when *debug-bterm*
|
| 331 | |
(with-in-module ((get-context-module))
|
| 332 | |
(format t "~%[resolver_target] ")
|
| 333 | |
(term-print-with-sort target)
|
| 334 | |
(print-next)
|
| 335 | |
(format t "~% mod = ~a" *current-module*)
|
| 336 | |
(print-next)
|
| 337 | |
(print-method-brief (term-head target))
|
| 338 | |
(print-next)
|
| 339 | |
(format t " str: ~a" (method-rewrite-strategy (term-head target)))))
|
| 340 | |
(setq target (reducer-no-stat target module :red))
|
| 341 | |
(when *debug-bterm*
|
| 342 | |
(with-in-module ((get-context-module))
|
| 343 | |
(format t "~% --> ")
|
| 344 | |
(term-print-with-sort $$term)))
|
| 345 | |
(when (is-true? $$term)
|
| 346 | |
(push subst answers))))
|
| 347 | |
answers))
|
| 348 | |
|
| 349 | |
;;; try-resolve-boolean-term : term -> Values (abst-bterm List(substitution))
|
|
328 |
(with-in-module (module)
|
|
329 |
(let* ((abst-term (make-bterm-representation bterm))
|
|
330 |
(variables (term-variables abst-term))
|
|
331 |
(answers nil))
|
|
332 |
(when (> (length variables) .maximum-bterm-vars.)
|
|
333 |
(with-output-chaos-warning ()
|
|
334 |
(format t "Sorry, but the current system can not handle more than ~d variables."
|
|
335 |
.maximum-bterm-vars.)
|
|
336 |
(return-from resolve-abst-bterm nil)))
|
|
337 |
(dolist (subst (assign-tf variables))
|
|
338 |
(let ((target (substitution-image-cp subst abst-term)))
|
|
339 |
(reset-reduced-flag target)
|
|
340 |
(when *debug-bterm*
|
|
341 |
(with-in-module ((get-context-module))
|
|
342 |
(format t "~%[resolver_target] ")
|
|
343 |
(term-print-with-sort target)
|
|
344 |
(print-next)
|
|
345 |
(format t "~% mod = ~a" *current-module*)
|
|
346 |
(print-next)
|
|
347 |
(print-method-brief (term-head target))
|
|
348 |
(print-next)
|
|
349 |
(format t " str: ~a" (method-rewrite-strategy (term-head target)))))
|
|
350 |
(setq target (reducer-no-stat target module :red))
|
|
351 |
(when *debug-bterm*
|
|
352 |
(with-in-module ((get-context-module))
|
|
353 |
(format t "~% --> ")
|
|
354 |
(term-print-with-sort $$term)))
|
|
355 |
(when (is-true? $$term)
|
|
356 |
(push subst answers))))
|
|
357 |
answers)))
|
|
358 |
|
|
359 |
;;; make-abst-boolean-term : term -> Values (abst-bterm List(substitution))
|
| 350 | 360 |
;;;
|
| 351 | 361 |
(defvar *abst-bterm* nil)
|
| 352 | 362 |
(defvar *abst-bterm-representation* nil)
|
| 353 | 363 |
|
| 354 | |
(defun try-resolve-boolean-term (term module)
|
|
364 |
(defun make-abst-boolean-term (term module)
|
| 355 | 365 |
(unless (sort= (term-sort term) *bool-sort*)
|
| 356 | 366 |
(with-output-chaos-warning ()
|
| 357 | 367 |
(format t "Given term is not of sort Bool. Ignored.")
|
| 358 | |
(return-from try-resolve-boolean-term nil)))
|
|
368 |
(return-from make-abst-boolean-term nil)))
|
| 359 | 369 |
(!setup-reduction module)
|
| 360 | 370 |
(with-in-module (module)
|
| 361 | 371 |
(reset-reduced-flag term)
|
| 362 | 372 |
(let ((target (reducer-no-stat term module :red)))
|
| 363 | 373 |
;; abstract
|
| 364 | |
(let ((bterm (abstract-boolean-term target)))
|
|
374 |
(let ((bterm (abstract-boolean-term target module)))
|
| 365 | 375 |
(setq *abst-bterm* bterm)
|
| 366 | 376 |
(setq *abst-bterm-representation*
|
| 367 | 377 |
(make-bterm-representation bterm))
|
|
| 381 | 391 |
(print-next)
|
| 382 | 392 |
(term-print-with-sort var)
|
| 383 | 393 |
(princ " |-> ")
|
| 384 | |
(term-print-with-sort mapping))))
|
| 385 | |
;; find answers
|
| 386 | |
(let ((ans (resolve-abst-bterm bterm module)))
|
| 387 | |
(cond (ans
|
| 388 | |
(format t "~%** The following assignment(s) can make the term 'true'.")
|
| 389 | |
(let ((num 0))
|
| 390 | |
(declare (type fixnum num))
|
| 391 | |
(let ((*print-indent* (+ 2 *print-indent*)))
|
| 392 | |
(dolist (sub ans)
|
| 393 | |
(print-next)
|
| 394 | |
(format t "(~d): " (incf num))
|
| 395 | |
(print-substitution sub)))))
|
| 396 | |
(t
|
| 397 | |
(format t "~%** No solution was found.")))
|
| 398 | |
(values bterm ans))))))))
|
|
394 |
(term-print-with-sort mapping))))))))))
|
|
395 |
|
|
396 |
;;; try-resolve-bterm
|
|
397 |
;;;
|
|
398 |
(defun try-resolve-bterm ()
|
|
399 |
(unless *abst-bterm*
|
|
400 |
(with-output-chaos-error ('no-bterm)
|
|
401 |
(format t "No abstracted boolean term is specified. ~%Please do :binspect or binspect first.")))
|
|
402 |
(let ((bterm *abst-bterm*)
|
|
403 |
(module (abst-bterm-module *abst-bterm*)))
|
|
404 |
;; find answers
|
|
405 |
(let ((ans (resolve-abst-bterm bterm module)))
|
|
406 |
(cond (ans
|
|
407 |
(with-in-module (module)
|
|
408 |
(format t "~%** The following assignment(s) can make the term 'true'.")
|
|
409 |
(let ((num 0))
|
|
410 |
(declare (type fixnum num))
|
|
411 |
(let ((*print-indent* (+ 2 *print-indent*)))
|
|
412 |
(dolist (sub ans)
|
|
413 |
(print-next)
|
|
414 |
(format t "(~d): " (incf num))
|
|
415 |
(print-substitution sub))))))
|
|
416 |
(t
|
|
417 |
(format t "~%** No solution was found.")))
|
|
418 |
(values bterm ans))))
|
| 399 | 419 |
|
| 400 | 420 |
;;;
|
| 401 | 421 |
(defun binspect-in-goal (goal-name preterm)
|
| 402 | 422 |
(let* ((goal-node (get-target-goal-node goal-name))
|
| 403 | 423 |
(context-module (goal-context (ptree-node-goal goal-node)))
|
| 404 | 424 |
(target (do-parse-term* preterm context-module)))
|
| 405 | |
(try-resolve-boolean-term target context-module)))
|
|
425 |
(make-abst-boolean-term target context-module)))
|
| 406 | 426 |
|
| 407 | 427 |
(defun binspect-in-module (mod-name preterm)
|
| 408 | 428 |
(multiple-value-bind (target context-module)
|
| 409 | 429 |
(do-parse-term* preterm mod-name)
|
| 410 | |
(try-resolve-boolean-term target context-module)))
|
|
430 |
(make-abst-boolean-term target context-module)))
|
| 411 | 431 |
|
| 412 | 432 |
;;; TOP LEVEL FUNCTION
|
| 413 | 433 |
;;; binspect-in
|
|
| 417 | 437 |
(t
|
| 418 | 438 |
(binspect-in-module goal-or-module-name preterm))))
|
| 419 | 439 |
|
|
440 |
;;; bresolve
|
|
441 |
;;;
|
|
442 |
(defun bresolve ()
|
|
443 |
(try-resolve-bterm))
|
|
444 |
|
| 420 | 445 |
;;; EOF
|