这两天在写一个检查归结的racket程序
(define (complementary-literals? l1 l2)
(let* ([l1str (symbol->string l1)]
[l2str (symbol->string l2)]
[l1neg (equal? #\~ (string-ref l1str 0))]
[l2neg (equal? #\~ (string-ref l2str 0))]
[symbol1 (if l1neg (substring l1str 1) l1str)]
[symbol2 (if l2neg (substring l2str 1) l2str)])
(and (xor l1neg l2neg)
(equal? symbol1 symbol2))))
(define (resolve clause1 clause2);;clause1 and 2 both list '(a v c) '(~a b d)
(let ([temp #f])
(for* ([next1 clause1]
[next2 clause2]);;next1 and 2 both symbol from list1 and 2
(cond
[(complementary-literals? next1 next2) (set! temp (delete next2 (delete next1 (append clause1 clause2) '()) '()))]))
(if (not (boolean? temp)) temp -1)));;return -1 if two clauses different, return list if two cluases can combine
(define (delete n lst clean);;delete an element from a list
(cond
((empty? lst) clean)
((equal? n (car lst)) (delete n (cdr lst) clean))
(else
(delete n (cdr lst) (append clean (list (car lst)))))))
这里面resolve作用是拿2个list 对比2个list里每一个symbol是否有例如a ~a这种形式
如果有就返回剩下的比如(resolve '(a b c) '(~a d e))就会返回‘(b c d e)
但是如果是(resolve '(a b c) '(~a ~b d)) 我期望的是返回‘(c d)
现在返回给我的是’(a c ~a d)
我现在想的是做一个recursion 可是停止的情况想不出来

(define (complementary-literals? l1 l2)
(let* ([l1str (symbol->string l1)]
[l2str (symbol->string l2)]
[l1neg (equal? #\~ (string-ref l1str 0))]
[l2neg (equal? #\~ (string-ref l2str 0))]
[symbol1 (if l1neg (substring l1str 1) l1str)]
[symbol2 (if l2neg (substring l2str 1) l2str)])
(and (xor l1neg l2neg)
(equal? symbol1 symbol2))))
(define c-l? complementary-literals?)
(define (resolve l1 l2)
(cond ((null? l1) l2)
((null? l2) l1)
((c-l? (car l1) (car l2))
(resolve (cdr l1) (cdr l2)))
(else
(append l1 l2))))
;;;test
(resolve '(a b c) '(a d e))
(resolve '(a b c) '(~a d e))
(resolve '(a b c) '(~a ~b d))

#lang racket
(define (rm-elem? elem)
(let* ((elem-str (symbol->string elem)))
(cond ((equal? #\~ (string-ref elem-str 0))
(string->symbol (substring elem-str 1)))
(else #f))))
(define (resolve-h l1 rm-l temp)
(cond ((or (null? l1) (null? rm-l)) (list rm-l temp))
((rm-elem? (car l1))
=> (lambda (result)
(resolve-h (cdr l1) (remove result rm-l) temp)))
(else
(resolve-h (cdr l1) rm-l (cons (car l1) temp)))))
(define (resolve l1 l2)
(let* ((result-lst ((lambda (x)
(resolve-h (car x) (cadr x) '()))
(resolve-h l1 l2 '())))
(fl1 (car result-lst))
(fl2 (cadr result-lst)))
(remove-duplicates
(append fl1 fl2))))
;;;test
(resolve '(a b c) '(a d e))
(resolve '(a b c) '(~a d e))
(resolve '(a b c) '(~a ~b d))
(resolve '(b c a) '(~a d f))
(resolve '(b d a c f) '(a c ~f e ~b d))
#|
result:
'(c b a e d)
'(c b e d)
'(c d)
'(c b f d)
'(c a d e)
|#