--- /dev/null
+; to check, run : lfsc sat.plf smt.plf th_base.plf example.plf\r
+\r
+; -------------------------------------------------------------------------------- \r
+; input :\r
+; ( a = b )\r
+; ( b = f(c) )\r
+; ( a != f(c) V a != b )\r
+\r
+; theory lemma (by transitivity) :\r
+; ( a != b V b != f(c) V a = f(c) )\r
+\r
+\r
+; With the theory lemma, the input is unsatisfiable.\r
+; -------------------------------------------------------------------------------- \r
+\r
+\r
+\r
+(check \r
+(% s sort\r
+(% a (term s)\r
+(% b (term s)\r
+(% c (term s)\r
+(% f (term (arrow s s))\r
+\r
+; -------------------- declaration of input formula -----------------------------------\r
+\r
+(% A1 (th_holds (= s a b))\r
+(% A2 (th_holds (= s b (apply _ _ f c)))\r
+(% A3 (th_holds (or (not (= s a (apply _ _ f c))) (not (= s a b))))\r
+\r
+\r
+; ------------------- specify that the following is a proof of the empty clause -----------------\r
+\r
+(: (holds cln)\r
+\r
+; ---------- use atoms (a1, a2, a3) to map theory literals to boolean literals (v1, v2, v3) ------\r
+\r
+(decl_atom (= s a b) (\ v1 (\ a1\r
+(decl_atom (= s b (apply _ _ f c)) (\ v2 (\ a2\r
+(decl_atom (= s a (apply _ _ f c)) (\ v3 (\ a3\r
+\r
+\r
+; --------------------------- proof of theory lemma ---------------------------------------------\r
+\r
+(satlem _ _\r
+(ast _ _ _ a1 (\ l1\r
+(ast _ _ _ a2 (\ l2\r
+(asf _ _ _ a3 (\ l3\r
+(clausify_false\r
+\r
+; this should be a proof of l1 ^ l2 ^ ~l3 => false\r
+; this is done by theory proof rules (currently just use "trust")\r
+\r
+ trust\r
+\r
+))))))) (\ CT\r
+; CT is the clause ( ~v1 V ~v2 V v3 )\r
+\r
+; -------------------- clausification of input formulas -----------------------------------------\r
+\r
+(satlem _ _\r
+(asf _ _ _ a1 (\ l1\r
+(clausify_false\r
+\r
+; input formula A1 is ( ~l1 )\r
+; the following should be a proof of l1 ^ ( ~l1 ) => false\r
+; this is done by natural deduction rules\r
+\r
+ (contra _ A1 l1)\r
+\r
+))) (\ C1\r
+; C1 is the clause ( v1 )\r
+\r
+\r
+(satlem _ _\r
+(asf _ _ _ a2 (\ l2\r
+(clausify_false\r
+\r
+; input formula A2 is ( ~l2 )\r
+; the following should be a proof of l2 ^ ( ~l2 ) => false\r
+; this is done by natural deduction rules\r
+\r
+ (contra _ A2 l2)\r
+ \r
+))) (\ C2 \r
+; C2 is the clause ( v2 )\r
+\r
+\r
+(satlem _ _\r
+(ast _ _ _ a3 (\ l3\r
+(ast _ _ _ a1 (\ l1\r
+(clausify_false\r
+\r
+; input formula A3 is ( ~a3 V ~a1 ) \r
+; the following should be a proof of a3 ^ a1 ^ ( ~a3 V ~a1 ) => false\r
+; this is done by natural deduction rules\r
+\r
+ (contra _ l1 (or_elim_1 _ _ (not_not_intro _ l3) A3))\r
+\r
+))))) (\ C3 \r
+; C3 is the clause ( ~v3 V ~v1 )\r
+\r
+\r
+\r
+; -------------------- resolution proof ------------------------------------------------------------\r
+\r
+(satlem_simplify _ _ _ \r
+\r
+(R _ _ C1\r
+(R _ _ C2\r
+(R _ _ CT C3 v3) v2) v1)\r
+\r
+(\ x x))\r
+\r
+))))))))))))))))))))))))))\r
+)
\ No newline at end of file
--- /dev/null
+(declare bool type)\r
+(declare tt bool)\r
+(declare ff bool)\r
+\r
+(declare var type) \r
+\r
+(declare lit type)\r
+(declare pos (! x var lit))\r
+(declare neg (! x var lit))\r
+\r
+(declare clause type)\r
+(declare cln clause)\r
+(declare clc (! x lit (! c clause clause)))\r
+\r
+; constructs for general clauses for R, Q, satlem\r
+\r
+(declare concat (! c1 clause (! c2 clause clause)))\r
+(declare clr (! l lit (! c clause clause))) \r
+\r
+; code to check resolutions\r
+\r
+(program append ((c1 clause) (c2 clause)) clause\r
+ (match c1 (cln c2) ((clc l c1') (clc l (append c1' c2)))))\r
+\r
+; we use marks as follows:\r
+; -- mark 1 to record if we are supposed to remove a positive occurrence of the variable.\r
+; -- mark 2 to record if we are supposed to remove a negative occurrence of the variable.\r
+; -- mark 3 if we did indeed remove the variable positively\r
+; -- mark 4 if we did indeed remove the variable negatively\r
+(program simplify_clause ((c clause)) clause\r
+ (match c\r
+ (cln cln)\r
+ ((clc l c1)\r
+ (match l\r
+ ; Set mark 1 on v if it is not set, to indicate we should remove it.\r
+ ; After processing the rest of the clause, set mark 3 if we were already \r
+ ; supposed to remove v (so if mark 1 was set when we began). Clear mark3\r
+ ; if we were not supposed to be removing v when we began this call.\r
+ ((pos v)\r
+ (let m (ifmarked v tt (do (markvar v) ff))\r
+ (let c' (simplify_clause c1)\r
+ (match m\r
+ (tt (do (ifmarked3 v v (markvar3 v)) c')) \r
+ (ff (do (ifmarked3 v (markvar3 v) v) (markvar v) (clc l c')))))))\r
+ ; the same as the code for tt, but using different marks.\r
+ ((neg v)\r
+ (let m (ifmarked2 v tt (do (markvar2 v) ff))\r
+ (let c' (simplify_clause c1)\r
+ (match m\r
+ (tt (do (ifmarked4 v v (markvar4 v)) c')) \r
+ (ff (do (ifmarked4 v (markvar4 v) v) (markvar2 v) (clc l c')))))))))\r
+ ((concat c1 c2) (append (simplify_clause c1) (simplify_clause c2)))\r
+ ((clr l c1)\r
+ (match l\r
+ ; set mark 1 to indicate we should remove v, and fail if\r
+ ; mark 3 is not set after processing the rest of the clause\r
+ ; (we will set mark 3 if we remove a positive occurrence of v).\r
+ ((pos v)\r
+ (let m (ifmarked v tt (do (markvar v) ff))\r
+ (let m3 (ifmarked3 v (do (markvar3 v) tt) ff)\r
+ (let c' (simplify_clause c1)\r
+ (ifmarked3 v (do (match m3 (tt v) (ff (markvar3 v)))\r
+ (match m (tt v) (ff (markvar v))) c')\r
+ (fail clause))))))\r
+ ; same as the tt case, but with different marks.\r
+ ((neg v)\r
+ (let m2 (ifmarked2 v tt (do (markvar2 v) ff))\r
+ (let m4 (ifmarked4 v (do (markvar4 v) tt) ff)\r
+ (let c' (simplify_clause c1)\r
+ (ifmarked4 v (do (match m4 (tt v) (ff (markvar4 v)))\r
+ (match m2 (tt v) (ff (markvar2 v))) c')\r
+ (fail clause))))))\r
+ ))))\r
+\r
+\r
+; resolution proofs\r
+ \r
+(declare holds (! c clause type))\r
+\r
+(declare R (! c1 clause (! c2 clause \r
+ (! u1 (holds c1)\r
+ (! u2 (holds c2)\r
+ (! n var\r
+ (holds (concat (clr (pos n) c1)\r
+ (clr (neg n) c2))))))))) \r
+\r
+(declare Q (! c1 clause (! c2 clause \r
+ (! u1 (holds c1)\r
+ (! u2 (holds c2)\r
+ (! n var\r
+ (holds (concat (clr (neg n) c1)\r
+ (clr (pos n) c2)))))))))\r
+ \r
+(declare satlem_simplify\r
+ (! c1 clause\r
+ (! c2 clause\r
+ (! c3 clause\r
+ (! u1 (holds c1)\r
+ (! r (^ (simplify_clause c1) c2)\r
+ (! u2 (! x (holds c2) (holds c3))\r
+ (holds c3))))))))\r
+ \r
+(declare satlem\r
+ (! c clause\r
+ (! c2 clause\r
+ (! u (holds c)\r
+ (! u2 (! v (holds c) (holds c2))\r
+ (holds c2))))))\r
+\r
+; A little example to demonstrate simplify_clause.\r
+; It can handle nested clr's of both polarities,\r
+; and correctly cleans up marks when it leaves a\r
+; clr or clc scope. Uncomment and run with \r
+; --show-runs to see it in action.\r
+; \r
+; (check \r
+; (% v1 var\r
+; (% u1 (holds (concat (clr (neg v1) (clr (pos v1) (clc (pos v1) (clr (pos v1) (clc (pos v1) (clc (neg v1) cln))))))\r
+; (clc (pos v1) (clc (pos v1) cln))))\r
+; (satlem _ _ _ u1 (\ x x))))))\r
+\r
+\r
+;(check \r
+; (% v1 var\r
+; (% u1 (holds (clr (neg v1) (concat (clc (neg v1) cln)\r
+; (clr (neg v1) (clc (neg v1) cln)))))\r
+; (satlem _ _ _ u1 (\ x x))))))
\ No newline at end of file
--- /dev/null
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;
+; 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 )
\ No newline at end of file
--- /dev/null
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\r
+;\r
+; Atomization / Clausification\r
+;\r
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\r
+ \r
+; binding between an LF var and an (atomic) formula\r
+(declare atom (! v var (! p formula type)))\r
+\r
+(declare decl_atom\r
+ (! f formula\r
+ (! u (! v var \r
+ (! a (atom v f)\r
+ (holds cln)))\r
+ (holds cln))))\r
+ \r
+; direct clausify\r
+(declare clausify_form\r
+ (! f formula\r
+ (! v var\r
+ (! a (atom v f)\r
+ (! u (th_holds f)\r
+ (holds (clc (pos v) cln)))))))\r
+ \r
+(declare clausify_form_not\r
+ (! f formula\r
+ (! v var\r
+ (! a (atom v f)\r
+ (! u (th_holds (not f))\r
+ (holds (clc (neg v) cln)))))))\r
+\r
+(declare clausify_false\r
+ (! u (th_holds false)\r
+ (holds cln)))\r
+\r
+ \r
+(declare th_let_pf\r
+ (! f formula\r
+ (! u (th_holds f)\r
+ (! u2 (! v (th_holds f) (holds cln))\r
+ (holds cln)))))\r
+\r
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\r
+;\r
+; Theory reasoning\r
+; - make a series of assumptions and then derive a contradiction (or false)\r
+; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false"\r
+; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn"\r
+;\r
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\r
+\r
+(declare ast\r
+ (! v var\r
+ (! f formula\r
+ (! C clause\r
+ (! r (atom v f) ;this is specified\r
+ (! u (! o (th_holds f)\r
+ (holds C))\r
+ (holds (clc (neg v) C))))))))\r
+\r
+(declare asf\r
+ (! v var\r
+ (! f formula\r
+ (! C clause\r
+ (! r (atom v f)\r
+ (! u (! o (th_holds (not f))\r
+ (holds C))\r
+ (holds (clc (pos v) C))))))))\r
+\r
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\r
+;\r
+; Theory of Equality and Congruence Closure\r
+;\r
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;\r
+\r
+; temporary : \r
+(declare trust (th_holds false))\r
+\r
+(declare refl\r
+ (! s sort\r
+ (! t (term s)\r
+ (th_holds (= s t t)))))\r
+\r
+(declare symm (! s sort\r
+ (! x (term s)\r
+ (! y (term s)\r
+ (! u (th_holds (= _ x y))\r
+ (th_holds (= _ y x)))))))\r
+\r
+(declare trans (! s sort\r
+ (! x (term s)\r
+ (! y (term s)\r
+ (! z (term s)\r
+ (! u (th_holds (= _ x y))\r
+ (! u (th_holds (= _ y z))\r
+ (th_holds (= _ x z)))))))))\r
+\r
+(declare cong (! s1 sort\r
+ (! s2 sort\r
+ (! a1 (term (arrow s1 s2))\r
+ (! b1 (term (arrow s1 s2))\r
+ (! a2 (term s1)\r
+ (! b2 (term s1)\r
+ (! u1 (th_holds (= _ a1 b1))\r
+ (! u2 (th_holds (= _ a2 b2))\r
+ (th_holds (= _ (apply _ _ a1 a2) (apply _ _ b1 b2))))))))))))\r
+ \r
projects / cvc5.git / commitdiff