(declare bool type)
(declare tt bool)
(declare ff bool)

(declare var type)

(declare lit type)
(declare pos (! x var lit))
(declare neg (! x var lit))

(declare clause type)
(declare cln clause)
(declare clc (! x lit (! c clause clause)))

; constructs for general clauses for R, Q, satlem

(declare concat_cl (! c1 clause (! c2 clause clause)))
(declare clr (! l lit (! c clause clause)))

; code to check resolutions

(program append ((c1 clause) (c2 clause)) clause
  (match c1 (cln c2) ((clc l c1') (clc l (append c1' c2)))))

; we use marks as follows:
; -- mark 1 to record if we are supposed to remove a positive occurrence of the variable.
; -- mark 2 to record if we are supposed to remove a negative occurrence of the variable.
; -- mark 3 if we did indeed remove the variable positively
; -- mark 4 if we did indeed remove the variable negatively
(program simplify_clause ((c clause)) clause
  (match c
    (cln cln)
    ((clc l c1)
      (match l
        ; Set mark 1 on v if it is not set, to indicate we should remove it.
        ; After processing the rest of the clause, set mark 3 if we were already
        ; supposed to remove v (so if mark 1 was set when we began).  Clear mark3
        ; if we were not supposed to be removing v when we began this call.
        ((pos v)
          (let m (ifmarked v tt (do (markvar v) ff))
          (let c' (simplify_clause c1)
            (match m
              (tt (do (ifmarked3 v v (markvar3 v)) c'))
              (ff (do (ifmarked3 v (markvar3 v) v) (markvar v) (clc l c')))))))
        ; the same as the code for tt, but using different marks.
        ((neg v)
          (let m (ifmarked2 v tt (do (markvar2 v) ff))
          (let c' (simplify_clause c1)
            (match m
              (tt (do (ifmarked4 v v (markvar4 v)) c'))
              (ff (do (ifmarked4 v (markvar4 v) v) (markvar2 v) (clc l c')))))))))
    ((concat_cl c1 c2) (append (simplify_clause c1) (simplify_clause c2)))
    ((clr l c1)
      (match l
        ; set mark 1 to indicate we should remove v, and fail if
        ; mark 3 is not set after processing the rest of the clause
        ; (we will set mark 3 if we remove a positive occurrence of v).
        ((pos v)
            (let m (ifmarked v tt (do (markvar v) ff))
            (let m3 (ifmarked3 v (do (markvar3 v) tt) ff)
            (let c' (simplify_clause c1)
              (ifmarked3 v (do (match m3 (tt v) (ff (markvar3 v)))
                                (match m (tt v) (ff (markvar v))) c')
                          (fail clause))))))
        ; same as the tt case, but with different marks.
        ((neg v)
            (let m2 (ifmarked2 v tt (do (markvar2 v) ff))
            (let m4 (ifmarked4 v (do (markvar4 v) tt) ff)
            (let c' (simplify_clause c1)
              (ifmarked4 v (do (match m4 (tt v) (ff (markvar4 v)))
                                (match m2 (tt v) (ff (markvar2 v))) c')
                          (fail clause))))))
   ))))


; resolution proofs

(declare holds (! c clause type))

(declare R (! c1 clause (! c2 clause
           (! u1 (holds c1)
           (! u2 (holds c2)
           (! n var
            (holds (concat_cl (clr (pos n) c1)
                     (clr (neg n) c2)))))))))

(declare Q (! c1 clause (! c2 clause
           (! u1 (holds c1)
           (! u2 (holds c2)
           (! n var
            (holds (concat_cl (clr (neg n) c1)
                     (clr (pos n) c2)))))))))

(declare satlem_simplify
                (! c1 clause
                (! c2 clause
                (! c3 clause
                (! u1 (holds c1)
                (! r (^ (simplify_clause c1) c2)
                (! u2 (! x (holds c2) (holds c3))
                   (holds c3))))))))

(declare satlem
  (! c clause
  (! c2 clause
  (! u (holds c)
  (! u2 (! v (holds c) (holds c2))
    (holds c2))))))

; A little example to demonstrate simplify_clause.
; It can handle nested clr's of both polarities,
; and correctly cleans up marks when it leaves a
; clr or clc scope.  Uncomment and run with
; --show-runs to see it in action.
;
; (check
;   (% v1 var
;   (% u1 (holds (concat_cl (clr (neg v1) (clr (pos v1) (clc (pos v1) (clr (pos v1) (clc (pos v1) (clc (neg v1) cln))))))
;                    (clc (pos v1) (clc (pos v1) cln))))
;    (satlem _ _ _ u1 (\ x x))))))


;(check
;   (% v1 var
;   (% u1 (holds (clr (neg v1) (concat_cl (clc (neg v1) cln)
;                                      (clr (neg v1) (clc (neg v1) cln)))))
;    (satlem _ _ _ u1 (\ x x))))))