;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; SMT syntax and semantics (not theory-specific)
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; depends on sat.plf

(declare formula type)
(declare th_holds (! f formula type))

; standard logic definitions
(declare true formula)
(declare false formula)
(declare not (! f formula formula))
(declare and (! f1 formula (! f2 formula formula)))
(declare or (! f1 formula (! f2 formula formula)))
(declare impl (! f1 formula (! f2 formula formula)))
(declare iff (! f1 formula (! f2 formula formula)))
(declare xor (! f1 formula (! f2 formula formula)))
(declare ifte (! b formula (! f1 formula (! f2 formula formula))))

; terms
(declare sort type)
(declare term (! t sort type))	; declared terms in formula

; standard definitions for =, ite, let and flet
(declare = (! s sort
           (! x (term s)
           (! y (term s)
             formula))))
(declare ite (! s sort
             (! f formula
             (! t1 (term s)
             (! t2 (term s)
               (term s))))))
(declare let (! s sort
             (! t (term s)
             (! f (! v (term s) formula)
               formula))))
(declare flet (! f1 formula
              (! f2 (! v formula formula)
                formula)))

; We view applications of predicates as terms of sort "Bool".
; Such terms can be injected as atomic formulas using "p_app".
(declare Bool sort)				; the special sort for predicates
(declare p_app (! x (term Bool) formula))	; propositional application of term


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; CNF Clausification
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; binding between an LF var and an (atomic) formula
(declare atom (! v var (! p formula type)))

(declare decl_atom
  (! f formula
  (! u (! v var
       (! a (atom v f)
         (holds cln)))
    (holds cln))))

; clausify a formula directly
(declare clausify_form
  (! f formula
  (! v var
  (! a (atom v f)
  (! u (th_holds f)
    (holds (clc (pos v) cln)))))))
    
(declare clausify_form_not
  (! f formula
  (! v var
  (! a (atom v f)
  (! u (th_holds (not f))
    (holds (clc (neg v) cln)))))))
    
(declare clausify_false
  (! u (th_holds false)
    (holds cln)))

(declare th_let_pf
  (! f formula
  (! u (th_holds f)
  (! u2 (! v (th_holds f) (holds cln))
    (holds cln)))))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; Natural deduction rules : used for CNF
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


;; contradiction

(declare contra
  (! f formula
  (! r1 (th_holds f)
  (! r2 (th_holds (not f))
    (th_holds false)))))

;; not not

(declare not_not_intro
  (! f formula
  (! u (th_holds f)
    (th_holds (not (not f))))))

(declare not_not_elim
  (! f formula
  (! u (th_holds (not (not f)))
    (th_holds f))))

;; or elimination

(declare or_elim_1
  (! f1 formula
  (! f2 formula
  (! u1 (th_holds (not f1))
  (! u2 (th_holds (or f1 f2))
    (th_holds f2))))))

(declare or_elim_2
  (! f1 formula
  (! f2 formula
  (! u1 (th_holds (not f2))
  (! u2 (th_holds (or f1 f2))
    (th_holds f1))))))

;; and elimination

(declare and_elim_1
  (! f1 formula
  (! f2 formula
  (! u (th_holds (and f1 f2))
    (th_holds f1)))))

(declare and_elim_2
  (! f1 formula
  (! f2 formula
  (! u (th_holds (and f1 f2))
    (th_holds f2)))))

;; not impl elimination

(declare not_impl_elim_1
  (! f1 formula
  (! f2 formula
  (! u (th_holds (not (impl f1 f2)))
    (th_holds f1)))))

(declare not_impl_elim_2
  (! f1 formula
  (! f2 formula
  (! u (th_holds (not (impl f1 f2)))
    (th_holds (not f2))))))

;; impl elimination

(declare impl_intro (! f1 formula
                    (! f2 formula
                    (! i1 (! u (th_holds f1)
                              (th_holds f2))
                      (th_holds (impl f1 f2))))))

(declare impl_elim
  (! f1 formula
  (! f2 formula
  (! u1 (th_holds f1)
  (! u2 (th_holds (impl f1 f2))
    (th_holds f2))))))

;; iff elimination

(declare iff_elim_1
  (! f1 formula
  (! f2 formula
  (! u1 (th_holds (iff f1 f2))
    (th_holds (impl f1 f2))))))

(declare iff_elim_2
  (! f1 formula
  (! f2 formula
  (! u1 (th_holds (iff f1 f2))
    (th_holds (impl f2 f1))))))

(declare not_iff_elim_1
  (! f1 formula
  (! f2 formula
  (! u1 (th_holds (not f1))
  (! u2 (th_holds (not (iff f1 f2)))
    (th_holds f2))))))

(declare not_iff_elim_2
  (! f1 formula
  (! f2 formula
  (! u1 (th_holds f1)
  (! u2 (th_holds (not (iff f1 f2)))
    (th_holds (not f2)))))))

;; ite elimination

(declare ite_elim_1
  (! a formula
  (! b formula
  (! c formula
  (! u1 (th_holds a)
  (! u2 (th_holds (ifte a b c))
    (th_holds b)))))))

(declare ite_elim_2
  (! a formula
  (! b formula
  (! c formula
  (! u1 (th_holds (not a))
  (! u2 (th_holds (ifte a b c))
    (th_holds c)))))))

(declare ite_elim_3
  (! a formula
  (! b formula
  (! c formula
  (! u1 (th_holds (not b))
  (! u2 (th_holds (ifte a b c))
    (th_holds c)))))))

(declare ite_elim_2n
  (! a formula
  (! b formula
  (! c formula
  (! u1 (th_holds a)
  (! u2 (th_holds (ifte (not a) b c))
    (th_holds c)))))))

(declare not_ite_elim_1
  (! a formula
  (! b formula
  (! c formula
  (! u1 (th_holds a)
  (! u2 (th_holds (not (ifte a b c)))
    (th_holds (not b))))))))

(declare not_ite_elim_2
  (! a formula
  (! b formula
  (! c formula
  (! u1 (th_holds (not a))
  (! u2 (th_holds (not (ifte a b c)))
    (th_holds (not c))))))))

(declare not_ite_elim_3
  (! a formula
  (! b formula
  (! c formula
  (! u1 (th_holds b)
  (! u2 (th_holds (not (ifte a b c)))
    (th_holds (not c))))))))

(declare not_ite_elim_2n
  (! a formula
  (! b formula
  (! c formula
  (! u1 (th_holds a)
  (! u2 (th_holds (not (ifte (not a) b c)))
    (th_holds (not c))))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; For theory lemmas
; - make a series of assumptions and then derive a contradiction (or false)
; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false"
; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn"
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(declare ast
  (! v var
  (! f formula
  (! C clause
  (! r (atom v f)       ;this is specified
  (! u (! o (th_holds f)
         (holds C))
    (holds (clc (neg v) C))))))))

(declare asf
  (! v var
  (! f formula
  (! C clause
  (! r (atom v f)
  (! u (! o (th_holds (not f))
         (holds C))
    (holds (clc (pos v) C))))))))
    



;; Example:
;;
;; Given theory literals (F1....Fn), and an input formula A of the form (th_holds (or F1 (or F2 .... (or F{n-1} Fn))))).
;;
;; We introduce atoms (a1,...,an) to map boolean literals (v1,...,vn) top literals (F1,...,Fn).
;; Do this at the beginning of the proof:
;;
;; (decl_atom F1 (\ v1 (\ a1
;; (decl_atom F2 (\ v2 (\ a2
;; ....
;; (decl_atom Fn (\ vn (\ an
;;
;;  A is then clausified by the following proof:
;;
;;(satlem _ _
;;(asf _ _ _ a1 (\ l1
;;(asf _ _ _ a2 (\ l2
;;...
;;(asf _ _ _ an (\ ln
;;(clausify_false
;;
;;   (contra _
;;      (or_elim_1 _ _ l{n-1}
;;	...
;;      (or_elim_1 _ _ l2
;; 	(or_elim_1 _ _ l1 A))))) ln)
;;	
;;))))))) (\ C
;;
;; We now have the free variable C, which should be the clause (v1 V ... V vn).
;;
;; Polarity of literals should be considered, say we have A of the form (th_holds (or (not F1) (or F2 (not F3)))).
;; Where necessary, we use "ast" instead of "asf", introduce negations by "not_not_intro" for pattern matching, and flip
;; the arguments of contra:
;;
;;(satlem _ _
;;(ast _ _ _ a1 (\ l1
;;(asf _ _ _ a2 (\ l2
;;(ast _ _ _ a3 (\ l3
;;(clausify_false
;;
;;   (contra _ l3
;;      (or_elim_1 _ _ l2
;; 	(or_elim_1 _ _ (not_not_intro l1) A))))
;;	
;;))))))) (\ C
;;
;; C should be the clause (~v1 V v2 V ~v3 )