313 lines
7.1 KiB
Plaintext
313 lines
7.1 KiB
Plaintext
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
;
|
|
; SMT syntax and semantics (not theory-specific)
|
|
;
|
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
|
|
(declare formula type)
|
|
(declare th_holds (! f formula type))
|
|
|
|
; constants
|
|
(declare true formula)
|
|
(declare false formula)
|
|
|
|
; logical connectives
|
|
(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) ; sort in the theory
|
|
(declare arrow (! s1 sort (! s2 sort sort))) ; function constructor
|
|
|
|
(declare term (! t sort type)) ; declared terms in formula
|
|
|
|
(declare apply (! s1 sort
|
|
(! s2 sort
|
|
(! t1 (term (arrow s1 s2))
|
|
(! t2 (term s1)
|
|
(term s2))))))
|
|
|
|
(declare ite (! s sort
|
|
(! f formula
|
|
(! t1 (term s)
|
|
(! t2 (term s)
|
|
(term s))))))
|
|
|
|
; let/flet
|
|
(declare let (! s sort
|
|
(! t (term s)
|
|
(! f (! v (term s) formula)
|
|
formula))))
|
|
(declare flet (! f1 formula
|
|
(! f2 (! v formula formula)
|
|
formula)))
|
|
|
|
; predicates
|
|
(declare = (! s sort
|
|
(! x (term s)
|
|
(! y (term s)
|
|
formula))))
|
|
|
|
; To avoid duplicating some of the rules (e.g., cong), we will 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
|
|
|
|
|
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
; Examples
|
|
|
|
; an example of "(p1 or p2(0)) and t1=t2(1)"
|
|
;(! p1 (term Bool)
|
|
;(! p2 (term (arrow Int Bool))
|
|
;(! t1 (term Int)
|
|
;(! t2 (term (arrow Int Int))
|
|
;(! F (th_holds (and (or (p_app p1) (p_app (apply _ _ p2 0)))
|
|
; (= _ t1 (apply _ _ t2 1))))
|
|
; ...
|
|
|
|
; another example of "p3(a,b)"
|
|
;(! a (term Int)
|
|
;(! b (term Int)
|
|
;(! p3 (term (arrow Int (arrow Int Bool))) ; arrow is right assoc.
|
|
;(! F (th_holds (p_app (apply _ _ (apply _ _ p3 a) b))) ; apply is left assoc.
|
|
; ...
|
|
|
|
|
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
|
;
|
|
; 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))))))))
|
|
|
|
|
|
|
|
;; How to do CNF for disjunctions of theory literals.
|
|
;;
|
|
;; 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 for literals F1...Fn, mapping them to boolean literals v1...vn.
|
|
;; Do this at the beginning of the proof:
|
|
;;
|
|
;; (decl_atom F1 (\ v1 (\ a1
|
|
;; (decl_atom F2 (\ v2 (\ a2
|
|
;; ....
|
|
;; (decl_atom Fn (\ vn (\ an
|
|
;;
|
|
;; Our input A is 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).
|
|
;;
|
|
;; We also need to consider the polarity of literals, 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 ) |