diff options
Diffstat (limited to 'src/lfsc/tests/signatures')
| -rwxr-xr-x | src/lfsc/tests/signatures/sat.plf | 127 | ||||
| -rwxr-xr-x | src/lfsc/tests/signatures/smt.plf | 423 | ||||
| -rwxr-xr-x | src/lfsc/tests/signatures/th_arrays.plf | 63 | ||||
| -rwxr-xr-x | src/lfsc/tests/signatures/th_base.plf | 99 | ||||
| -rw-r--r-- | src/lfsc/tests/signatures/th_bv.plf | 192 | ||||
| -rw-r--r-- | src/lfsc/tests/signatures/th_bv_bitblast.plf | 671 | ||||
| -rw-r--r-- | src/lfsc/tests/signatures/th_bv_rewrites.plf | 22 | ||||
| -rw-r--r-- | src/lfsc/tests/signatures/th_int.plf | 25 |
8 files changed, 1622 insertions, 0 deletions
diff --git a/src/lfsc/tests/signatures/sat.plf b/src/lfsc/tests/signatures/sat.plf new file mode 100755 index 0000000..b95caa8 --- /dev/null +++ b/src/lfsc/tests/signatures/sat.plf @@ -0,0 +1,127 @@ +(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)))))) diff --git a/src/lfsc/tests/signatures/smt.plf b/src/lfsc/tests/signatures/smt.plf new file mode 100755 index 0000000..fa89a45 --- /dev/null +++ b/src/lfsc/tests/signatures/smt.plf @@ -0,0 +1,423 @@ +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; +; 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 ) + + diff --git a/src/lfsc/tests/signatures/th_arrays.plf b/src/lfsc/tests/signatures/th_arrays.plf new file mode 100755 index 0000000..b54a4ed --- /dev/null +++ b/src/lfsc/tests/signatures/th_arrays.plf @@ -0,0 +1,63 @@ +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; +; Theory of Arrays +; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; depends on : th_base.plf + +; sorts + +(declare Array (! s1 sort (! s2 sort sort))) ; s1 is index, s2 is element + +; functions +(declare write (! s1 sort + (! s2 sort + (term (arrow (Array s1 s2) + (arrow s1 + (arrow s2 (Array s1 s2)))))))) + +(declare read (! s1 sort + (! s2 sort + (term (arrow (Array s1 s2) + (arrow s1 s2)))))) + +; inference rules + +; read( a[i] = b, i ) == b +(declare row1 (! s1 sort + (! s2 sort + (! t1 (term (Array s1 s2)) + (! t2 (term s1) + (! t3 (term s2) + (th_holds (= _ + (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t3)) t2) t3)))))))) + +(declare row (! s1 sort + (! s2 sort + (! t2 (term s1) + (! t3 (term s1) + (! t1 (term (Array s1 s2)) + (! t4 (term s2) + (! u (th_holds (not (= _ t2 t3))) + (th_holds (= _ (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t4)) t3) + (apply _ _ (apply _ _ (read s1 s2) t1) t3))))))))))) + +(declare negativerow (! s1 sort + (! s2 sort + (! t2 (term s1) + (! t3 (term s1) + (! t1 (term (Array s1 s2)) + (! t4 (term s2) + (! u (th_holds (not (= _ + (apply _ _ (apply _ _ (read s1 s2) (apply _ _ (apply _ _ (apply _ _ (write s1 s2) t1) t2) t4)) t3) + (apply _ _ (apply _ _ (read s1 s2) t1) t3)))) + (th_holds (= _ t2 t3)))))))))) + +(declare ext (! s1 sort + (! s2 sort + (! t1 (term (Array s1 s2)) + (! t2 (term (Array s1 s2)) + (! u1 (! k (term s1) + (! u2 (th_holds (or (= _ t1 t2) (not (= _ (apply _ _ (apply _ _ (read s1 s2) t1) k) (apply _ _ (apply _ _ (read s1 s2) t2) k))))) + (holds cln))) + (holds cln)))))))
\ No newline at end of file diff --git a/src/lfsc/tests/signatures/th_base.plf b/src/lfsc/tests/signatures/th_base.plf new file mode 100755 index 0000000..ffa8667 --- /dev/null +++ b/src/lfsc/tests/signatures/th_base.plf @@ -0,0 +1,99 @@ + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; +; Theory of Equality and Congruence Closure +; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; depends on : smt.plf + +; sorts : + +(declare arrow (! s1 sort (! s2 sort sort))) ; function constructor + +; functions : + +(declare apply (! s1 sort + (! s2 sort + (! t1 (term (arrow s1 s2)) + (! t2 (term s1) + (term s2)))))) + + +; inference rules : + +(declare trust (th_holds false)) ; temporary +(declare trust_f (! f formula (th_holds f))) ; temporary + +(declare refl + (! s sort + (! t (term s) + (th_holds (= s t t))))) + +(declare symm (! s sort + (! x (term s) + (! y (term s) + (! u (th_holds (= _ x y)) + (th_holds (= _ y x))))))) + +(declare trans (! s sort + (! x (term s) + (! y (term s) + (! z (term s) + (! u (th_holds (= _ x y)) + (! u (th_holds (= _ y z)) + (th_holds (= _ x z))))))))) + +(declare negsymm (! s sort + (! x (term s) + (! y (term s) + (! u (th_holds (not (= _ x y))) + (th_holds (not (= _ y x)))))))) + +(declare negtrans1 (! s sort + (! x (term s) + (! y (term s) + (! z (term s) + (! u (th_holds (not (= _ x y))) + (! u (th_holds (= _ y z)) + (th_holds (not (= _ x z)))))))))) + +(declare negtrans2 (! s sort + (! x (term s) + (! y (term s) + (! z (term s) + (! u (th_holds (= _ x y)) + (! u (th_holds (not (= _ y z))) + (th_holds (not (= _ x z)))))))))) + +(define negtrans negtrans1) + + +(declare cong (! s1 sort + (! s2 sort + (! a1 (term (arrow s1 s2)) + (! b1 (term (arrow s1 s2)) + (! a2 (term s1) + (! b2 (term s1) + (! u1 (th_holds (= _ a1 b1)) + (! u2 (th_holds (= _ a2 b2)) + (th_holds (= _ (apply _ _ a1 a2) (apply _ _ b1 b2)))))))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +; 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. +; ... diff --git a/src/lfsc/tests/signatures/th_bv.plf b/src/lfsc/tests/signatures/th_bv.plf new file mode 100644 index 0000000..0004b35 --- /dev/null +++ b/src/lfsc/tests/signatures/th_bv.plf @@ -0,0 +1,192 @@ +;;;; TEMPORARY: + +(declare trust-bad (th_holds false)) + +; helper stuff +(program mpz_sub ((x mpz) (y mpz)) mpz + (mp_add x (mp_mul (~1) y))) + +(program mp_ispos ((x mpz)) formula + (mp_ifneg x false true)) + +(program mpz_eq ((x mpz) (y mpz)) formula + (mp_ifzero (mpz_sub x y) true false)) + +(program mpz_lt ((x mpz) (y mpz)) formula + (mp_ifneg (mpz_sub x y) true false)) + +(program mpz_lte ((x mpz) (y mpz)) formula + (mp_ifneg (mpz_sub x y) true (mpz_eq x y))) + +(program mpz_ ((x mpz) (y mpz)) formula + (mp_ifzero (mpz_sub x y) true false)) + + +; "bitvec" is a term of type "sort" +; (declare BitVec sort) +(declare BitVec (! n mpz sort)) + +; bit type +(declare bit type) +(declare b0 bit) +(declare b1 bit) + +; bit vector type used for constants +(declare bv type) +(declare bvn bv) +(declare bvc (! b bit (! v bv bv))) + +; calculate the length of a bitvector +;; (program bv_len ((v bv)) mpz +;; (match v +;; (bvn 0) +;; ((bvc b v') (mp_add (bv_len v') 1)))) + + +; a bv constant term +(declare a_bv + (! n mpz + (! v bv + (term (BitVec n))))) + +(program bv_constants_are_disequal ((x bv) (y bv)) formula + (match x + (bvn (fail formula)) + ((bvc bx x') + (match y + (bvn (fail formula)) + ((bvc by y') (match bx + (b0 (match by (b0 (bv_constants_are_disequal x' y')) (b1 (true)))) + (b1 (match by (b0 (true)) (b1 (bv_constants_are_disequal x' y')))) + )) + )) +)) + +(declare bv_disequal_constants + (! n mpz + (! x bv + (! y bv + (! c (^ (bv_constants_are_disequal x y) true) + (th_holds (not (= (BitVec n) (a_bv n x) (a_bv n y))))))))) + +; a bv variable +(declare var_bv type) +; a bv variable term +(declare a_var_bv + (! n mpz + (! v var_bv + (term (BitVec n))))) + +; bit vector binary operators +(define bvop2 + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (term (BitVec n)))))) + +(declare bvand bvop2) +(declare bvor bvop2) +(declare bvor bvop2) +(declare bvxor bvop2) +(declare bvnand bvop2) +(declare bvnor bvop2) +(declare bvxnor bvop2) +(declare bvmul bvop2) +(declare bvadd bvop2) +(declare bvsub bvop2) +(declare bvudiv bvop2) +(declare bvurem bvop2) +(declare bvsdiv bvop2) +(declare bvsrem bvop2) +(declare bvsmod bvop2) +(declare bvshl bvop2) +(declare bvlshr bvop2) +(declare bvashr bvop2) +(declare concat bvop2) + +; bit vector unary operators +(define bvop1 + (! n mpz + (! x (term (BitVec n)) + (term (BitVec n))))) + + +(declare bvneg bvop1) +(declare bvnot bvop1) +(declare rotate_left bvop1) +(declare rotate_right bvop1) + +(declare bvcomp + (! n mpz + (! t1 (term (BitVec n)) + (! t2 (term (BitVec n)) + (term (BitVec 1)))))) + + +(declare concat + (! n mpz + (! m mpz + (! m' mpz + (! t1 (term (BitVec m)) + (! t2 (term (BitVec m')) + (term (BitVec n)))))))) + +;; side-condition fails in signature only?? +;; (! s (^ (mp_add m m') n) + +;; (declare repeat bvopp) + +(declare extract + (! n mpz + (! i mpz + (! j mpz + (! m mpz + (! t2 (term (BitVec m)) + (term (BitVec n)))))))) + +(declare zero_extend + (! n mpz + (! i mpz + (! m mpz + (! t2 (term (BitVec m)) + (term (BitVec n))))))) + +(declare sign_extend + (! n mpz + (! i mpz + (! m mpz + (! t2 (term (BitVec m)) + (term (BitVec n))))))) + +(declare repeat + (! n mpz + (! i mpz + (! m mpz + (! t2 (term (BitVec m)) + (term (BitVec n))))))) + + + +;; TODO: add checks for valid typing for these operators +;; (! c1 (^ (mpz_lte i j) +;; (! c2 (^ (mpz_lt i n) true) +;; (! c3 (^ (mp_ifneg i false true) true) +;; (! c4 (^ (mp_ifneg j false true) true) +;; (! s (^ (mp_add (mpz_sub i j) 1) m) + + +; bit vector predicates +(define bvpred + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + formula)))) + +(declare bvult bvpred) +(declare bvule bvpred) +(declare bvugt bvpred) +(declare bvuge bvpred) +(declare bvslt bvpred) +(declare bvsle bvpred) +(declare bvsgt bvpred) +(declare bvsge bvpred) diff --git a/src/lfsc/tests/signatures/th_bv_bitblast.plf b/src/lfsc/tests/signatures/th_bv_bitblast.plf new file mode 100644 index 0000000..ebb412f --- /dev/null +++ b/src/lfsc/tests/signatures/th_bv_bitblast.plf @@ -0,0 +1,671 @@ +; bit blasted terms as list of formulas +(declare bblt type) +(declare bbltn bblt) +(declare bbltc (! f formula (! v bblt bblt))) + +; calculate the length of a bit-blasted term +(program bblt_len ((v bblt)) mpz + (match v + (bbltn 0) + ((bbltc b v') (mp_add (bblt_len v') 1)))) + + +; (bblast_term x y) means term y corresponds to bit level interpretation x +(declare bblast_term + (! n mpz + (! x (term (BitVec n)) + (! y bblt + type)))) + +; FIXME: for unsupported bit-blast terms +(declare trust_bblast_term + (! n mpz + (! x (term (BitVec n)) + (! y bblt + (bblast_term n x y))))) + + +; Binds a symbol to the bblast_term to be used later on. +(declare decl_bblast + (! n mpz + (! b bblt + (! t (term (BitVec n)) + (! bb (bblast_term n t b) + (! s (^ (bblt_len b) n) + (! u (! v (bblast_term n t b) (holds cln)) + (holds cln)))))))) + +(declare decl_bblast_with_alias + (! n mpz + (! b bblt + (! t (term (BitVec n)) + (! a (term (BitVec n)) + (! bb (bblast_term n t b) + (! e (th_holds (= _ t a)) + (! s (^ (bblt_len b) n) + (! u (! v (bblast_term n a b) (holds cln)) + (holds cln)))))))))) + +; a predicate to represent the n^th bit of a bitvector term +(declare bitof + (! x var_bv + (! n mpz formula))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; BITBLASTING RULES +;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST CONSTANT +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program bblast_const ((v bv) (n mpz)) bblt + (mp_ifneg n (match v (bvn bbltn) + (default (fail bblt))) + (match v ((bvc b v') (bbltc (match b (b0 false) (b1 true)) (bblast_const v' (mp_add n (~ 1))))) + (default (fail bblt))))) + +(declare bv_bbl_const (! n mpz + (! f bblt + (! v bv + (! c (^ (bblast_const v (mp_add n (~ 1))) f) + (bblast_term n (a_bv n v) f)))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST VARIABLE +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program bblast_var ((x var_bv) (n mpz)) bblt + (mp_ifneg n bbltn + (bbltc (bitof x n) (bblast_var x (mp_add n (~ 1)))))) + +(declare bv_bbl_var (! n mpz + (! x var_bv + (! f bblt + (! c (^ (bblast_var x (mp_add n (~ 1))) f) + (bblast_term n (a_var_bv n x) f)))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST CONCAT +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program bblast_concat ((x bblt) (y bblt)) bblt + (match x + (bbltn (match y ((bbltc by y') (bbltc by (bblast_concat x y'))) + (bbltn bbltn))) + ((bbltc bx x') (bbltc bx (bblast_concat x' y))))) + +(declare bv_bbl_concat (! n mpz + (! m mpz + (! m1 mpz + (! x (term (BitVec m)) + (! y (term (BitVec m1)) + (! xb bblt + (! yb bblt + (! rb bblt + (! xbb (bblast_term m x xb) + (! ybb (bblast_term m1 y yb) + (! c (^ (bblast_concat xb yb ) rb) + (bblast_term n (concat n m m1 x y) rb))))))))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST EXTRACT +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program bblast_extract_rec ((x bblt) (i mpz) (j mpz) (n mpz)) bblt + (match x + ((bbltc bx x') (mp_ifneg (mpz_sub (mpz_sub j n) 1) + (mp_ifneg (mpz_sub (mpz_sub n i) 1) + (bbltc bx (bblast_extract_rec x' i j (mpz_sub n 1))) + (bblast_extract_rec x' i j (mpz_sub n 1))) + + bbltn)) + (bbltn bbltn))) + +(program bblast_extract ((x bblt) (i mpz) (j mpz) (n mpz)) bblt + (bblast_extract_rec x i j (mpz_sub n 1))) + +(declare bv_bbl_extract (! n mpz + (! i mpz + (! j mpz + (! m mpz + (! x (term (BitVec m)) + (! xb bblt + (! rb bblt + (! xbb (bblast_term m x xb) + (! c ( ^ (bblast_extract xb i j m) rb) + (bblast_term n (extract n i j m x) rb))))))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST ZERO/SIGN EXTEND +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program extend_rec ((x bblt) (i mpz) (b formula)) bblt + (mp_ifneg i x + (bbltc b (extend_rec x (mpz_sub i 1) b)))) + +(program bblast_zextend ((x bblt) (i mpz)) bblt + (extend_rec x (mpz_sub i 1) false)) + +(declare bv_bbl_zero_extend (! n mpz + (! k mpz + (! m mpz + (! x (term (BitVec m)) + (! xb bblt + (! rb bblt + (! xbb (bblast_term m x xb) + (! c ( ^ (bblast_zextend xb k m) rb) + (bblast_term n (zero_extend n k m x) rb)))))))))) + +(program bblast_sextend ((x bblt) (i mpz)) bblt + (match x (bbltn (fail bblt)) + ((bbltc xb x') (extend_rec x (mpz_sub i 1) xb)))) + +(declare bv_bbl_sign_extend (! n mpz + (! k mpz + (! m mpz + (! x (term (BitVec m)) + (! xb bblt + (! rb bblt + (! xbb (bblast_term m x xb) + (! c ( ^ (bblast_sextend xb k m) rb) + (bblast_term n (sign_extend n k m x) rb)))))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST BVAND +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program bblast_bvand ((x bblt) (y bblt)) bblt + (match x + (bbltn (match y (bbltn bbltn) (default (fail bblt)))) + ((bbltc bx x') (match y + (bbltn (fail bblt)) + ((bbltc by y') (bbltc (and bx by) (bblast_bvand x' y'))))))) + +(declare bv_bbl_bvand (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! xb bblt + (! yb bblt + (! rb bblt + (! xbb (bblast_term n x xb) + (! ybb (bblast_term n y yb) + (! c (^ (bblast_bvand xb yb ) rb) + (bblast_term n (bvand n x y) rb))))))))))) +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST BVNOT +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program bblast_bvnot ((x bblt)) bblt + (match x + (bbltn bbltn) + ((bbltc bx x') (bbltc (not bx) (bblast_bvnot x'))))) + +(declare bv_bbl_bvnot (! n mpz + (! x (term (BitVec n)) + (! xb bblt + (! rb bblt + (! xbb (bblast_term n x xb) + (! c (^ (bblast_bvnot xb ) rb) + (bblast_term n (bvnot n x) rb)))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST BVOR +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program bblast_bvor ((x bblt) (y bblt)) bblt + (match x + (bbltn (match y (bbltn bbltn) (default (fail bblt)))) + ((bbltc bx x') (match y + (bbltn (fail bblt)) + ((bbltc by y') (bbltc (or bx by) (bblast_bvor x' y'))))))) + +(declare bv_bbl_bvor (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! xb bblt + (! yb bblt + (! rb bblt + (! xbb (bblast_term n x xb) + (! ybb (bblast_term n y yb) + (! c (^ (bblast_bvor xb yb ) rb) + (bblast_term n (bvor n x y) rb))))))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST BVXOR +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program bblast_bvxor ((x bblt) (y bblt)) bblt + (match x + (bbltn (match y (bbltn bbltn) (default (fail bblt)))) + ((bbltc bx x') (match y + (bbltn (fail bblt)) + ((bbltc by y') (bbltc (xor bx by) (bblast_bvxor x' y'))))))) + +(declare bv_bbl_bvxor (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! xb bblt + (! yb bblt + (! rb bblt + (! xbb (bblast_term n x xb) + (! ybb (bblast_term n y yb) + (! c (^ (bblast_bvxor xb yb ) rb) + (bblast_term n (bvxor n x y) rb))))))))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST BVADD +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; return the carry bit after adding x y +;; FIXME: not the most efficient thing in the world +(program bblast_bvadd_carry ((a bblt) (b bblt) (carry formula)) formula +(match a + ( bbltn (match b (bbltn carry) (default (fail formula)))) + ((bbltc ai a') (match b + (bbltn (fail formula)) + ((bbltc bi b') (or (and ai bi) (and (xor ai bi) (bblast_bvadd_carry a' b' carry)))))))) + +;; ripple carry adder where carry is the initial carry bit +(program bblast_bvadd ((a bblt) (b bblt) (carry formula)) bblt +(match a + ( bbltn (match b (bbltn bbltn) (default (fail bblt)))) + ((bbltc ai a') (match b + (bbltn (fail bblt)) + ((bbltc bi b') (bbltc (xor (xor ai bi) (bblast_bvadd_carry a' b' carry)) + (bblast_bvadd a' b' carry))))))) + + +(program reverse_help ((x bblt) (acc bblt)) bblt +(match x + (bbltn acc) + ((bbltc xi x') (reverse_help x' (bbltc xi acc))))) + + +(program reverseb ((x bblt)) bblt + (reverse_help x bbltn)) + + +; AJR: use this version? +;(program bblast_bvadd_2h ((a bblt) (b bblt) (carry formula)) bblt +;(match a +; ( bbltn (match b (bbltn bbltn) (default (fail bblt)))) +; ((bbltc ai a') (match b +; (bbltn (fail bblt)) +; ((bbltc bi b') +; (let carry' (or (and ai bi) (and (xor ai bi) carry)) +; (bbltc (xor (xor ai bi) carry) +; (bblast_bvadd_2h a' b' carry')))))))) + +;(program bblast_bvadd_2 ((a bblt) (b bblt) (carry formula)) bblt +;(let ar (reverseb a) ;; reverse a and b so that we can build the circuit +;(let br (reverseb b) ;; from the least significant bit up +;(let ret (bblast_bvadd_2h ar br carry) +; (reverseb ret))))) + +(declare bv_bbl_bvadd (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! xb bblt + (! yb bblt + (! rb bblt + (! xbb (bblast_term n x xb) + (! ybb (bblast_term n y yb) + (! c (^ (bblast_bvadd xb yb false) rb) + (bblast_term n (bvadd n x y) rb))))))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST BVNEG +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program bblast_zero ((n mpz)) bblt +(mp_ifzero n bbltn + (bbltc false (bblast_zero (mp_add n (~1)))))) + +(program bblast_bvneg ((x bblt) (n mpz)) bblt + (bblast_bvadd (bblast_bvnot x) (bblast_zero n) true)) + + +(declare bv_bbl_bvneg (! n mpz + (! x (term (BitVec n)) + (! xb bblt + (! rb bblt + (! xbb (bblast_term n x xb) + (! c (^ (bblast_bvneg xb n) rb) + (bblast_term n (bvneg n x) rb)))))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST BVMUL +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +;; shift add multiplier + +;; (program concat ((a bblt) (b bblt)) bblt +;; (match a (bbltn b) +;; ((bbltc ai a') (bbltc ai (concat a' b))))) + + +(program top_k_bits ((a bblt) (k mpz)) bblt + (mp_ifzero k bbltn + (match a (bbltn (fail bblt)) + ((bbltc ai a') (bbltc ai (top_k_bits a' (mpz_sub k 1))))))) + +(program bottom_k_bits ((a bblt) (k mpz)) bblt + (reverseb (top_k_bits (reverseb a) k))) + +;; assumes the least signigicant bit is at the beginning of the list +(program k_bit ((a bblt) (k mpz)) formula +(mp_ifneg k (fail formula) +(match a (bbltn (fail formula)) + ((bbltc ai a') (mp_ifzero k ai (k_bit a' (mpz_sub k 1))))))) + +(program and_with_bit ((a bblt) (bt formula)) bblt +(match a (bbltn bbltn) + ((bbltc ai a') (bbltc (and bt ai) (and_with_bit a' bt))))) + +;; a is going to be the current result +;; carry is going to be false initially +;; b is the and of a and b[k] +;; res is going to be bbltn initially +(program mult_step_k_h ((a bblt) (b bblt) (res bblt) (carry formula) (k mpz)) bblt +(match a + (bbltn (match b (bbltn res) (default (fail bblt)))) + ((bbltc ai a') + (match b (bbltn (fail bblt)) + ((bbltc bi b') + (mp_ifneg (mpz_sub k 1) + (let carry_out (or (and ai bi) (and (xor ai bi) carry)) + (let curr (xor (xor ai bi) carry) + (mult_step_k_h a' b' (bbltc curr res) carry_out (mpz_sub k 1)))) + (mult_step_k_h a' b (bbltc ai res) carry (mpz_sub k 1)) +)))))) + +;; assumes that a, b and res have already been reversed +(program mult_step ((a bblt) (b bblt) (res bblt) (n mpz) (k mpz)) bblt +(let k' (mpz_sub n k ) +(let ak (top_k_bits a k') +(let b' (and_with_bit ak (k_bit b k)) + (mp_ifzero (mpz_sub k' 1) + (mult_step_k_h res b' bbltn false k) + (let res' (mult_step_k_h res b' bbltn false k) + (mult_step a b (reverseb res') n (mp_add k 1)))))))) + + +(program bblast_bvmul ((a bblt) (b bblt) (n mpz)) bblt +(let ar (reverseb a) ;; reverse a and b so that we can build the circuit +(let br (reverseb b) ;; from the least significant bit up +(let res (and_with_bit ar (k_bit br 0)) + (mp_ifzero (mpz_sub n 1) ;; if multiplying 1 bit numbers no need to call mult_step + res + (mult_step ar br res n 1)))))) + +(declare bv_bbl_bvmul (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! xb bblt + (! yb bblt + (! rb bblt + (! xbb (bblast_term n x xb) + (! ybb (bblast_term n y yb) + (! c (^ (bblast_bvmul xb yb n) rb) + (bblast_term n (bvmul n x y) rb))))))))))) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST EQUALS +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +; bit blast x = y +; for x,y of size n, it will return a conjuction (x.0 = y.0 ^ ( ... ^ (x.{n-1} = y.{n-1}))) +; f is the accumulator formula that builds the equality in the right order +(program bblast_eq_rec ((x bblt) (y bblt) (f formula)) formula + (match x + (bbltn (match y (bbltn f) (default (fail formula)))) + ((bbltc fx x') (match y + (bbltn (fail formula)) + ((bbltc fy y') (bblast_eq_rec x' y' (and (iff fx fy) f))))) + (default (fail formula)))) + +(program bblast_eq ((x bblt) (y bblt)) formula + (match x + ((bbltc bx x') (match y ((bbltc by y') (bblast_eq_rec x' y' (iff bx by))) + (default (fail formula)))) + (default (fail formula)))) + + +;; TODO: a temporary bypass for rewrites that we don't support yet. As soon +;; as we do, remove this rule. + +(declare bv_bbl_=_false + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! bbx (bblast_term n x bx) + (! bby (bblast_term n y by) + (! c (^ (bblast_eq bx by) f) + (th_holds (iff (= (BitVec n) x y) false)))))))))))) + +(declare bv_bbl_= + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! bbx (bblast_term n x bx) + (! bby (bblast_term n y by) + (! c (^ (bblast_eq bx by) f) + (th_holds (iff (= (BitVec n) x y) f)))))))))))) + +(declare bv_bbl_=_swap + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! bbx (bblast_term n x bx) + (! bby (bblast_term n y by) + (! c (^ (bblast_eq by bx) f) + (th_holds (iff (= (BitVec n) x y) f)))))))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST BVULT +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program bblast_bvult ((x bblt) (y bblt) (n mpz)) formula +(match x + ( bbltn (fail formula)) + ((bbltc xi x') (match y + (bbltn (fail formula)) + ((bbltc yi y') (mp_ifzero n + (and (not xi) yi) + (or (and (iff xi yi) (bblast_bvult x' y' (mp_add n (~1)))) (and (not xi) yi)))))))) + +(declare bv_bbl_bvult + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! bbx (bblast_term n x bx) + (! bby (bblast_term n y by) + (! c (^ (bblast_bvult bx by (mp_add n (~1))) f) + (th_holds (iff (bvult n x y) f)))))))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; BITBLAST BVSLT +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(program bblast_bvslt ((x bblt) (y bblt) (n mpz)) formula +(match x + ( bbltn (fail formula)) + ((bbltc xi x') (match y + (bbltn (fail formula)) + ((bbltc yi y') (mp_ifzero (mpz_sub n 1) + (and xi (not yi)) + (or (and (iff xi yi) + (bblast_bvult x' y' (mpz_sub n 2))) + (and xi (not yi))))))))) + +(declare bv_bbl_bvslt + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (! bx bblt + (! by bblt + (! f formula + (! bbx (bblast_term n x bx) + (! bby (bblast_term n y by) + (! c (^ (bblast_bvslt bx by n) f) + (th_holds (iff (bvslt n x y) f)))))))))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; BITBLASTING CONNECTORS +;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +; bit-blasting connections + +(declare intro_assump_t + (! f formula + (! v var + (! C clause + (! h (th_holds f) + (! a (atom v f) + (! u (! unit (holds (clc (pos v) cln)) + (holds C)) + (holds C)))))))) + +(declare intro_assump_f + (! f formula + (! v var + (! C clause + (! h (th_holds (not f)) + (! a (atom v f) + (! u (! unit (holds (clc (neg v) cln)) + (holds C)) + (holds C)))))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; REWRITE RULES +;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +; rewrite rule : +; x + y = y + x +(declare bvadd_symm + (! n mpz + (! x (term (BitVec n)) + (! y (term (BitVec n)) + (th_holds (= (BitVec n) (bvadd _ x y) (bvadd _ y x))))))) + +;; (declare bvcrazy_rewrite +;; (! n mpz +;; (! x (term (BitVec n)) +;; (! y (term (BitVec n)) +;; (! xn bv_poly +;; (! yn bv_poly +;; (! hxn (bv_normalizes x xn) +;; (! hyn (bv_normalizes y yn) +;; (! s (^ (rewrite_scc xn yn) true) +;; (! u (! x (term (BitVec n)) (holds cln)) +;; (holds cln))))))))))) + +;; (th_holds (= (BitVec n) (bvadd x y) (bvadd y x))))))) + + + +; necessary? +;; (program calc_bvand ((a bv) (b bv)) bv +;; (match a +;; (bvn (match b (bvn bvn) (default (fail bv)))) +;; ((bvc ba a') (match b +;; ((bvc bb b') (bvc (match ba (b0 b0) (b1 bb)) (calc_bvand a' b'))) +;; (default (fail bv)))))) + +;; ; rewrite rule (w constants) : +;; ; a & b = c +;; (declare bvand_const (! c bv +;; (! a bv +;; (! b bv +;; (! u (^ (calc_bvand a b) c) +;; (th_holds (= BitVec (bvand (a_bv a) (a_bv b)) (a_bv c)))))))) + + +;; making constant bit-vectors +(program mk_ones ((n mpz)) bv + (mp_ifzero n bvn (bvc b1 (mk_ones (mpz_sub n 1))))) + +(program mk_zero ((n mpz)) bv + (mp_ifzero n bvn (bvc b0 (mk_ones (mpz_sub n 1))))) + + + +;; (bvxnor a b) => (bvnot (bvxor a b)) +;; (declare bvxnor_elim +;; (! n mpz +;; (! a (term (BitVec n)) +;; (! b (term (BitVec n)) +;; (! a' (term (BitVec n)) +;; (! b' (term (BitVec n)) +;; (! rwa (rw_term _ a a') +;; (! rwb (rw_term _ b b') +;; (rw_term n (bvxnor _ a b) +;; (bvnot _ (bvxor _ a' b'))))))))))) + + + +;; ;; (bvxor a 0) => a +;; (declare bvxor_zero +;; (! n mpz +;; (! zero_bits bv +;; (! sc (^ (mk_zero n) zero_bits) +;; (! a (term (BitVec n)) +;; (! b (term (BitVec n)) +;; (! a' (term (BitVec n)) +;; (! rwa (rw_term _ a a') +;; (! rwb (rw_term _ b (a_bv _ zero_bits)) +;; (rw_term _ (bvxor _ a b) +;; a')))))))))) + +;; ;; (bvxor a 11) => (bvnot a) +;; (declare bvxor_one +;; (! n mpz +;; (! one_bits bv +;; (! sc (^ (mk_ones n) one_bits) +;; (! a (term (BitVec n)) +;; (! b (term (BitVec n)) +;; (! a' (term (BitVec n)) +;; (! rwa (rw_term _ a a') +;; (! rwb (rw_term _ b (a_bv _ one_bits)) +;; (rw_term _ (bvxor _ a b) +;; (bvnot _ a'))))))))))) + + +;; ;; (bvnot (bvnot a)) => a +;; (declare bvnot_idemp +;; (! n mpz +;; (! a (term (BitVec n)) +;; (! a' (term (BitVec n)) +;; (! rwa (rw_term _ a a') +;; (rw_term _ (bvnot _ (bvnot _ a)) +;; a')))))) diff --git a/src/lfsc/tests/signatures/th_bv_rewrites.plf b/src/lfsc/tests/signatures/th_bv_rewrites.plf new file mode 100644 index 0000000..4af9a09 --- /dev/null +++ b/src/lfsc/tests/signatures/th_bv_rewrites.plf @@ -0,0 +1,22 @@ +; +; Equality swap +; + +(declare rr_bv_eq + (! n mpz + (! t1 (term (BitVec n)) + (! t2 (term (BitVec n)) + (th_holds (iff (= (BitVec n) t2 t1) (= (BitVec n) t1 t2))))))) + +; +; Additional rules... +; + +; +; Default, if nothing else applied +; + +(declare rr_bv_default + (! t1 formula + (! t2 formula + (th_holds (iff t1 t2))))) diff --git a/src/lfsc/tests/signatures/th_int.plf b/src/lfsc/tests/signatures/th_int.plf new file mode 100644 index 0000000..9a0a2d6 --- /dev/null +++ b/src/lfsc/tests/signatures/th_int.plf @@ -0,0 +1,25 @@ +(declare Int sort) + +(define arithpred_Int (! x (term Int) + (! y (term Int) + formula))) + +(declare >_Int arithpred_Int) +(declare >=_Int arithpred_Int) +(declare <_Int arithpred_Int) +(declare <=_Int arithpred_Int) + +(define arithterm_Int (! x (term Int) + (! y (term Int) + (term Int)))) + +(declare +_Int arithterm_Int) +(declare -_Int arithterm_Int) +(declare *_Int arithterm_Int) ; is * ok to use? +(declare /_Int arithterm_Int) ; is / ok to use? + +; a constant term +(declare a_int (! x mpz (term Int))) + +; unary negation +(declare u-_Int (! t (term Int) (term Int))) |