;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; 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)

(define formula_op1
	(! f formula
	formula))

(define formula_op2
	(! f1 formula
	(! f2 formula
	   formula)))
	
(define formula_op3
	(! f1 formula
	(! f2 formula
	(! f3 formula
	   formula))))
	   
(declare not formula_op1)
(declare and formula_op2)
(declare or formula_op2)
(declare impl formula_op2)
(declare iff formula_op2)
(declare xor formula_op2)
(declare ifte formula_op3)

; 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

; boolean terms
(declare t_true (term Bool))
(declare t_false (term Bool))
(declare t_t_neq_f
 (th_holds (not (= Bool t_true t_false))))
(declare pred_eq_t
 (! x (term Bool)
 (! u (th_holds (p_app x))
   (th_holds (= Bool x t_true)))))
(declare pred_eq_f
 (! x (term Bool)
 (! u (th_holds (not (p_app x)))
   (th_holds (= Bool x t_false)))))

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

; binding between an LF var and an (atomic) formula

(declare atom (! v var (! p formula type)))

; binding between two LF vars
(declare bvatom (! sat_v var (! bv_v var type)))

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

;; declare atom enhanced with mapping
;; between SAT prop variable and BVSAT prop variable
(declare decl_bvatom
  (! f formula
  (! u (! v var
       (! bv_v var
       (! a (atom v f)
       (! bva (atom bv_v f)
       (! vbv (bvatom v bv_v)
         (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
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; for eager bit-blasting
(declare iff_symm
	(! f formula
	   (th_holds (iff f f))))


;; contradiction

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

; truth
(declare truth (th_holds true))

;; 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))))))

(declare not_or_elim
  (! f1 formula
  (! f2 formula
  (! u2 (th_holds (not (or f1 f2)))
    (th_holds (and (not f1) (not f2)))))))
    
;; 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)))))

(declare not_and_elim
  (! f1 formula
  (! f2 formula
  (! u2 (th_holds (not (and f1 f2)))
    (th_holds (or (not f1) (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
  (! u2 (th_holds (impl f1 f2))
    (th_holds (or (not f1) f2))))))

(declare not_impl_elim
  (! f1 formula
  (! f2 formula
  (! u (th_holds (not (impl f1 f2)))
    (th_holds (and f1 (not f2)))))))
    
;; iff elimination

(declare iff_elim_1
  (! f1 formula
  (! f2 formula
  (! u1 (th_holds (iff f1 f2))
    (th_holds (or (not f1) f2))))))

(declare iff_elim_2
  (! f1 formula
  (! f2 formula
  (! u1 (th_holds (iff f1 f2))
    (th_holds (or f1 (not f2)))))))

(declare not_iff_elim
  (! f1 formula
  (! f2 formula
  (! u2 (th_holds (not (iff f1 f2)))
    (th_holds (iff f1 (not f2)))))))

; xor elimination

(declare xor_elim_1
  (! f1 formula
  (! f2 formula
  (! u1 (th_holds (xor f1 f2))
    (th_holds (or (not f1) (not f2)))))))

(declare xor_elim_2
  (! f1 formula
  (! f2 formula
  (! u1 (th_holds (xor f1 f2))
    (th_holds (or f1 f2))))))

(declare not_xor_elim
  (! f1 formula
  (! f2 formula
  (! u2 (th_holds (not (xor f1 f2)))
    (th_holds (iff f1 f2))))))

;; ite elimination

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

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

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

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

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

(declare not_ite_elim_3
  (! a formula
  (! b formula
  (! c formula
  (! u2 (th_holds (not (ifte a b c)))
    (th_holds (or (not b) (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))))))))

;; Bitvector lemma constructors to assume
;; the unit clause containing the assumptions
;; it also requires the mapping between bv_v and v
;; The resolution proof proving false will use bv_v as the definition clauses use bv_v
;; but the Problem clauses in the main SAT solver will use v so the learned clause is in terms of v
(declare bv_asf
  (! v var
  (! bv_v var
  (! f formula
  (! C clause
  (! r (atom v f) ;; passed in
  (! x (bvatom v bv_v) ; establishes the equivalence of v to bv_
  (! u (! o (holds (clc (neg bv_v) cln)) ;; l binding to be used in proof
         (holds C))
    (holds (clc (pos v) C))))))))))
    
(declare bv_ast
  (! v var
  (! bv_v var	
  (! f formula
  (! C clause
  (! r (atom v f)       ; this is specified
  (! x (bvatom v bv_v) ; establishes the equivalence of v to bv_v
  (! u (! o (holds (clc (pos bv_v) cln))
         (holds C))
    (holds (clc (neg 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 )