--- /dev/null
+; a = b ^ a = 00000 ^ b = 11111 is UNSAT\r
+\r
+(check\r
+(% a var_bv\r
+(% b var_bv\r
+(% f1 (th_holds (= BitVec (a_var_bv a) (a_var_bv b)))\r
+(% f2 (th_holds (= BitVec (a_var_bv a) (a_bv (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))))))\r
+(% f3 (th_holds (= BitVec (a_var_bv b) (a_bv (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))))))\r
+(: (holds cln)\r
+\r
+(decl_bv_atom_var 5 a (\ bv1 (\ ba1\r
+(decl_bv_atom_var 5 b (\ bv2 (\ ba2\r
+(decl_bv_atom_const _ (bvc b0 (bvc b0 (bvc b0 (bvc b0 (bvc b0 bvn))))) (\ bv3 (\ ba3\r
+(decl_bv_atom_const _ (bvc b1 (bvc b1 (bvc b1 (bvc b1 (bvc b1 bvn))))) (\ bv4 (\ ba4\r
+\r
+(decl_atom (bblast bv1 4) (\ v1 (\ a1\r
+(decl_atom (bblast bv2 4) (\ v2 (\ a2\r
+(decl_atom (bblast bv3 4) (\ v3 (\ a3\r
+(decl_atom (bblast bv4 4) (\ v4 (\ a4\r
+\r
+; bitblasting\r
+(th_let_pf _ (bv_bbl_eq _ _ _ _ _ _ ba1 ba2 f1) (\ bf1\r
+(th_let_pf _ (bv_bbl_eq _ _ _ _ _ _ ba1 ba3 f2) (\ bf2\r
+(th_let_pf _ (bv_bbl_eq _ _ _ _ _ _ ba2 ba4 f3) (\ bf3\r
+(th_let_pf _ (bv_bbl_const _ _ _ _ ba3) (\ bf4\r
+(th_let_pf _ (bv_bbl_const _ _ _ _ ba4) (\ bf5\r
+\r
+; CNFication\r
+; a.4 V ~b.4\r
+(satlem _ _\r
+(asf _ _ _ a1 (\ l1\r
+(ast _ _ _ a2 (\ l2\r
+(clausify_false\r
+ (contra _ (impl_elim _ _ l2 (iff_elim_2 _ _ (and_elim_1 _ _ bf1))) l1)\r
+))))) (\ C2\r
+\r
+; ~a.4 V 00000.4 \r
+(satlem _ _\r
+(ast _ _ _ a1 (\ l1\r
+(asf _ _ _ a3 (\ l3\r
+(clausify_false\r
+ (contra _ (impl_elim _ _ l1 (iff_elim_1 _ _ (and_elim_1 _ _ bf2))) l3)\r
+))))) (\ C3\r
+\r
+; b.4 V ~11111.4 \r
+(satlem _ _\r
+(asf _ _ _ a2 (\ l2\r
+(ast _ _ _ a4 (\ l4\r
+(clausify_false\r
+ (contra _ (impl_elim _ _ l4 (iff_elim_2 _ _ (and_elim_1 _ _ bf3))) l2)\r
+))))) (\ C6\r
+\r
+; ~00000.4\r
+(satlem _ _\r
+(ast _ _ _ a3 (\ l3\r
+(clausify_false\r
+ (contra _ l3 (and_elim_1 _ _ bf4))\r
+))) (\ C7\r
+\r
+; 11111.4\r
+(satlem _ _\r
+(asf _ _ _ a4 (\ l4\r
+(clausify_false\r
+ (contra _ (and_elim_1 _ _ bf5) l4)\r
+))) (\ C8\r
+\r
+\r
+(satlem_simplify _ _ _ \r
+(R _ _ \r
+ (R _ _ (R _ _ C8 C6 v4) C2 v2)\r
+ (R _ _ C3 C7 v3) v1) (\ x x))\r
+\r
+)))))))))))))))))))))))))))))))))))))))))))))))))))
\ No newline at end of file
--- /dev/null
+;a = b ^ a = 0 ^ b = 1\r
+\r
+; "bitvec" is a term of type "sort"\r
+(declare BitVec sort)\r
+\r
+; bit type\r
+(declare bit type)\r
+(declare b0 bit)\r
+(declare b1 bit)\r
+\r
+; bit vector type\r
+(declare bv type)\r
+(declare bvn bv)\r
+(declare bvc (! b bit (! v bv bv)))\r
+; a bv constant term\r
+(declare a_bv (! v bv (term BitVec)))\r
+\r
+; calculate the length of a bitvector\r
+(program bv_len ((v bv)) mpz \r
+ (match v\r
+ (bvn 0)\r
+ ((bvc b v') (mp_add (bv_len v') 1))))\r
+\r
+; a bv variable\r
+(declare var_bv type)\r
+; a bv variable term\r
+(declare a_var_bv (! v var_bv (term BitVec)))\r
+\r
+\r
+\r
+; bit vector operators\r
+(define bvoper (! x (term BitVec) \r
+ (! y (term BitVec) \r
+ (term BitVec))))\r
+(declare bvand bvoper)\r
+(declare bvadd bvoper)\r
+;....\r
+\r
+; variable used for bit-blasting (must be simply-typed)\r
+(declare bbl_var type)\r
+\r
+; all bit-vector terms are mapped with "bv_atom" to:\r
+; - a simply-typed term of type "bbl_var", which is used for bit-blasting\r
+; - a integer size\r
+(declare bv_atom (! x (term BitVec) (! y bbl_var (! n mpz type))))\r
+\r
+(declare decl_bv_atom_var (! n mpz ; must be specified\r
+ (! x var_bv\r
+ (! p (! w bbl_var\r
+ (! u (bv_atom (a_var_bv x) w n)\r
+ (holds cln)))\r
+ (holds cln)))))\r
+\r
+(declare decl_bv_atom_const (! n mpz\r
+ (! v bv\r
+ (! s (^ (bv_len v) n)\r
+ (! p (! w bbl_var\r
+ (! u (bv_atom (a_bv v) w n)\r
+ (holds cln)))\r
+ (holds cln))))))\r
+\r
+\r
+; a predicate to represent the n^th bit of a bitvector term\r
+(declare bblast (! x bbl_var (! n mpz formula)))\r
+\r
+; bit blast constant\r
+(program bblast_const ((x bbl_var) (v bv) (n mpz)) formula\r
+ (match v\r
+ (bvn (mp_ifneg n true (fail formula)))\r
+ ((bvc b v') (let n' (mp_add n (~ 1))\r
+ (let f (match b (b0 (not (bblast x n))) (b1 (bblast x n)))\r
+ (mp_ifzero n' f (and f (bblast_const x v' n'))))))))\r
+\r
+(declare bv_bbl_const (! n mpz\r
+ (! f formula\r
+ (! v bv\r
+ (! x bbl_var\r
+ (! u (bv_atom (a_bv v) x n)\r
+ (! c (^ (bblast_const x v (mp_add n (~ 1))) f)\r
+ (th_holds f))))))))\r
+\r
+; bit blast x = y\r
+(program bblast_eq ((x bbl_var) (y bbl_var) (n mpz)) formula\r
+ (let n' (mp_add n (~ 1))\r
+ (let f (iff (bblast x n) (bblast y n))\r
+ (mp_ifzero n' f (and f (bblast_eq x y n'))))))\r
+\r
+(declare bv_bbl_eq (! x (term BitVec)\r
+ (! y (term BitVec)\r
+ (! n mpz\r
+ (! f formula\r
+ (! x' bbl_var\r
+ (! y' bbl_var\r
+ (! ux' (bv_atom x x' n)\r
+ (! uy' (bv_atom y y' n)\r
+ (! u (th_holds (= BitVec x y))\r
+ (! c (^ (bblast_eq x' y' (mp_add n (~ 1))) f)\r
+ (th_holds f))))))))))))\r
+\r
+\r
+; rewrite rule :\r
+; x + y = y + x\r
+(declare bvadd_symm (! x (term BitVec)\r
+ (! y (term BitVec)\r
+ (! x' bbl_var\r
+ (! y' bbl_var\r
+ (! n mpz\r
+ (! ux (bv_atom x x' n)\r
+ (! uy (bv_atom y y' n)\r
+ (th_holds (= BitVec (bvadd x y) (bvadd y x)))))))))))\r
+\r
+(program calc_bvand ((a bv) (b bv)) bv\r
+ (match a\r
+ (bvn (match b (bvn bvn) (default (fail bv))))\r
+ ((bvc ba a') (match b\r
+ ((bvc bb b') (bvc (match ba (b0 b0) (b1 bb)) (calc_bvand a' b')))\r
+ (default (fail bv))))))\r
+\r
+; rewrite rule (w constants) :\r
+; a & b = c \r
+(declare bvand_const (! c bv\r
+ (! a bv\r
+ (! b bv\r
+ (! u (^ (calc_bvand a b) c)\r
+ (th_holds (= BitVec (bvand (a_bv a) (a_bv b)) (a_bv c))))))))
\ No newline at end of file
projects / cvc5.git / commitdiff