(defstep do-with-tcc (str1 str2) (try (quote str1) (try (then (quote str2) (fail)) (fail) (assert)) (postpone)) "Tries (str2) on all subgoals generated by (str1)" "") (defstep exp2 () (repeat (then (rewrite "exp2_def") (rewrite "expt_inverse") (rewrite "expt_plus") (rewrite "expt_div" :dir RL) (rewrite "expt_x1") (rewrite "expt_x0") (assert))) "exp2-catch-all-strategy, includes exp2_def expt_inverse expt_plus expt_div :dir RL expt_x1 expt_x0 and assert" "Rewriting with expt lemmas") (defstep exp2-const () (then (expand* "minint" "maxint") (repeat (rewrite "exp2_def")) (rewrite "exp2_0") (rewrite "exp2_1") (rewrite "exp2_2") (rewrite "exp2_3") (rewrite "exp2_4") (rewrite "exp2_5") (rewrite "exp2_6") (rewrite "exp2_7") (rewrite "exp2_8") (rewrite "exp2_9") (rewrite "exp2_10") (rewrite "exp2_11") (rewrite "exp2_12") (rewrite "exp2_13") (rewrite "exp2_23") (rewrite "exp2_28") (rewrite "exp2_29") (rewrite "exp2_52") (rewrite "exp2_53") (rewrite "exp2_54") (rewrite "exp2_55") (rewrite "exp2_56") (rewrite "exp2_57") (rewrite "exp2_63") (rewrite "exp2_64") (rewrite "exp2_71") (rewrite "exp2_127") (rewrite "exp2_128") (assert)) "Resolves 2^i for various values of i" "Using exp2 lemmas") (defstep exp2-const-inverse () (then (repeat (rewrite "exp2_def")) (repeat (rewrite "expt_inverse")) (exp2-const) ) "(exp2-const) plus (rewrite \"expt_inverse\")" "Using exp2 lemmas" ) (defstep case-replace-hide (step) (spread (case-replace step) ((hide -1)) ) "do (case-replace :hide? t)" "case-replacing ~a" ) (defstep case-replace-hide-all (step) (else (spread! (case-replace step) ((hide -1) (hide-all-but 1)) ) (spread! (case-replace step) ((hide-all-but 1)) ) ) "do (case-replace :hide? t) and (hide-all-but 1) on the second subgoal" "case-replacing ~a" ) (defstep case-replace-assert (step) (spread! (case-replace step) ((hide -1) (assert)) ) "do (case-replace :hide? t) and (assert) the second subgoal" "case-replacing ~a" ) (defstep case-replace-grind (step) (spread! (case-replace step) ((hide -1) (then (hide-all-but 1) (grind) ) ) ) "do (case-replace :hide? t) and (grind) the case" "case-replacing ~a" ) (defstep first (command first) (spread! (quote command) ((quote first) (skip)) ) "" "Using ~a and resolving this with ~a" ) (defstep second (command second) (spread! (quote command) ((skip) (quote second)) ) "" "Using ~a and resolving the other case with ~a" ) (defstep bv-const () (then (repeat (rewrite "b2n_fill_caret")) (rewrite "b2n_F") (rewrite "b2n_T") (rewrite "b2sign_F") (rewrite "b2sign_T") (repeat (rewrite "bv2nat_fill_F")) (repeat (rewrite "bv2nat_fill_T")) (repeat (rewrite "bv2int_fill_F")) (repeat (rewrite "bv2int_fill_T")) (assert) ) "" "Replacing various instances of bv2int(fill()), b2n() and b2sign()" ) (defstep bveq9 (&optional (fnum -1)) (then (stop-rewrite) (expand* "fill" "o" "^") (decompose-equality fnum) (inst-cp -1 0) (inst-cp -1 1) (inst-cp -1 2) (inst-cp -1 3) (inst-cp -1 4) (inst-cp -1 5) (inst-cp -1 6) (inst-cp -1 7) (inst -1 8) (expand* "h0" "h1" "h2" "h3" "h4" "h5" "h6" "h7" "h8" "h9" "hA" "hB" "hC" "hD" "hE" "hF") (ground)) "" "") (defstep add-unp-spec-s () (THEN (SKOSIMP*) (USE "not_sgl_and_dbl") (USE "op_exclude2") (EXPAND* "isADD" "isSUB" "isMUL" "isDIV" "isCMP" "isCVT" "isMOV" "isABS" "isNEG") (DO-WITH-TCC (CASE "is_double(I!1`op)=FALSE") (THEN (DELETE 4) (EXPAND "is_double") (BDDSIMP))) (EXPAND* "Snan?" "Ss_nan?" "Sq_nan?" "Sp_inf?" "Sn_inf?" "Sinf?" "Szero?" "Snonzero?" "Sbv2ieee_bv" "add_unpack" "add_unpack_spec" "nonzero?" "nonzero??") (REWRITE "unpack_F") (REWRITE "unpack_F") (LEMMA "spec_unpack_impl_sgl") (INST-CP -1 "I!1`F1" "FALSE") (INST -1 "I!1`F2" "FALSE") (NAME-REPLACE "U1" "unpack_impl(FALSE, FALSE, F1(I!1))") (NAME-REPLACE "U2" "unpack_impl(FALSE, FALSE, F2(I!1))") (ASSERT) (NAME-REPLACE "S2" "(spec_unpack_impl(U2`s, einf(U2), ez(U2), fz(U2), h(U2)(51)))") (NAME-REPLACE "S1" "(spec_unpack_impl(U1`s, einf(U1), ez(U1), fz(U1), h(U1)(51)))") (LEMMA "special_xors[8,24]") (INST-CP -1 "bv2ieee_bv[8, 24](I!1`F1)") (INST -1 "bv2ieee_bv[8, 24](I!1`F2)") (USE "STD_QNAN_is_qnan_s") (EXPAND* "zero?" "zero??" "bv2ieee_bv" "fill" "^" "o" "p_inf?" "n_inf?" "inf?" "fill" "isDIV" "isADD" "isSUB" "isMUL" "isCMP" "isCVT" "isMOV" "isABS" "isNEG" "is_double") (SMASH)) "" "") (defstep add-unp-spec-d () (THEN (SKOSIMP*) (USE "not_sgl_and_dbl") (USE "op_exclude2") (EXPAND* "isADD" "isSUB" "isMUL" "isDIV" "isCMP" "isCVT" "isMOV" "isABS" "isNEG") (DO-WITH-TCC (CASE "is_double(I!1`op)=TRUE") (THEN (DELETE 4) (EXPAND "is_double") (BDDSIMP))) (EXPAND* "Dnan?" "Ds_nan?" "Dq_nan?" "Dp_inf?" "Dn_inf?" "Dinf?" "Dzero?" "Dnonzero?" "Dbv2ieee_bv" "add_unpack" "add_unpack_spec" "nonzero?" "nonzero??") (REWRITE "unpack_F") (REWRITE "unpack_F") (LEMMA "spec_unpack_impl_dbl") (INST-CP -1 "I!1`F1" "FALSE") (INST -1 "I!1`F2" "FALSE") (NAME-REPLACE "U1" "unpack_impl(TRUE, FALSE, F1(I!1))") (NAME-REPLACE "U2" "unpack_impl(TRUE, FALSE, F2(I!1))") (ASSERT) (NAME-REPLACE "S2" "(spec_unpack_impl(U2`s, einf(U2), ez(U2), fz(U2), h(U2)(51)))") (NAME-REPLACE "S1" "(spec_unpack_impl(U1`s, einf(U1), ez(U1), fz(U1), h(U1)(51)))") (LEMMA "special_xors[11,53]") (INST-CP -1 "bv2ieee_bv[11,53](I!1`F1)") (INST -1 "bv2ieee_bv[11,53](I!1`F2)") (USE "STD_QNAN_is_qnan_d") (LEMMA "STDs_QNAN_is_qnan_d") (INST -1 "(exact_zero(isSUB(I!1`op), TRUE, F1(I!1), F2(I!1), ZERO(S1), ZERO(S2))`sign)") (LEMMA "INF_is_inf_d") (INST-CP -1 "(exact_zero(isSUB(I!1`op), TRUE, F1(I!1), F2(I!1), ZERO(S1), ZERO(S2))`sign)") (INST -1 "NOT I!1`F(63)") (EXPAND* "INF" "zero?" "zero??" "bv2ieee_bv" "fill" "^" "o" "p_inf?" "n_inf?" "inf?" "fill" "isDIV" "isADD" "isSUB" "isMUL" "isCMP" "isCVT" "isMOV" "isABS" "isNEG" "is_double") (SMASH)) "" "") (defstep fa () (repeat (then (assert) (flatten))) "" "Repeating assert/flatten" ) (defstep cr (formula &optional (hide? t) (all nil) (actuals? nil)) (spread (case formula) ((replace -1 :hide? hide? :actuals? actuals?) (if all (hide-all-but 1) (skip)) ) ) "Identical to (case-replace), with further arguments :hide? and :all. The latter will invoke (hide-all -but 1) on the second subgoal." "~%Assuming and applying ~a" ) (defstep renames () (then (reveal "RENAMES") (repeat (replace*)) (hide "RENAMES") (assert)) "Apply renames" "Applying renames")