(defstep skolem-inst-strat () (then (auto-rewrite-defs :always? t) (repeat* (then (assert)(skolem!)(inst?)(bddsimp))) (grind)) "Trying repeated skolemization and instantioation" "") (defstep unptcc3 () (then (flatten) (expand* "SIGSIZE" "EXPSIZE") (assert) (reveal 1 2 3 4 5 6 7 8 9) (use "unpack_TCC3") (expand "unpack_top_impl") (assert)) "Strategie for TCCs" "") (defstep unptcc4 () (then (flatten) (expand* "SIGSIZE" "EXPSIZE") (assert) (reveal 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20) (use "unpack_TCC4") (expand "unpack_top_impl") (assert)) "Strategie for TCCs" "") (defstep do-with-tcc (str1 str2) (try (quote str1) (try (then (quote str2) (fail)) (fail) (assert)) (postpone)) "Case with unptcc3 afterwards" "") ;; shifter (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)" "") ;; used in proof of lzero_concat1 (defstep lz_tcc () (then (use "logN_is_logN") (smash)) "Strategie for TCCs" "") ;; lzero_exp2_impl_correct (defstep exp2-strat-neu () (repeat (then (rewrite "expt_inverse") (rewrite "expt_plus") (rewrite "expt_div" :dir RL) (rewrite "expt_x1") (rewrite "expt_x0") (assert))) "Prove simple ...." "Rewriting with expt lemmas") (defstep lz_tcc2 () ( then (skosimp*) (smash)) "" "") (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 (repeat (rewrite "exp2_def")) (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_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 "bv2int_fill_F")) (repeat (rewrite "bv2int_fill_T")) (assert) ) "" "Replacing various instances of bv2int(fill()), b2n() and b2sign()" ) (defstep log2-strat-ns () (then (rewrite "log2_ineq3") (rewrite "log2_mul2expt") (rewrite "log2_mul2expt") (rewrite "log2_mul2expt") (rewrite "log2_mul2expt") (rewrite "log2_exp2") (assert)) "" "") (defstep bveq9 (&optional (fnum -1)) (then (skip-msg "bveq9 invoked")(stop-rewrite) (replace*) (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 unp-spec-s () (THEN (SKOSIMP*) (EXPAND* "Snan?" "Ss_nan?" "Sq_nan?" "Sinf?" "Szero?" "Snonzero?") (USE "not_sgl_and_dbl") (USE "not_div_and_mul") (EXPAND* "Sbv2ieee_bv" "md_unpack" "md_unpack_spec" "isMUL" "isDIV" "is_double" "nonzero?") (DO-WITH-TCC (CASE-REPLACE "is_dblDIV(I!1`op)=FALSE") (BDDSIMP)) (DO-WITH-TCC (CASE-REPLACE "is_dblMUL(I!1`op)=FALSE") (BDDSIMP)) (REWRITE "unpack_F") (REWRITE "unpack_F") (LEMMA "spec_unpack_impl_sgl") (INST-CP -1 "I!1`F1" "TRUE") (INST -1 "I!1`F2" "TRUE") (NAME-REPLACE "U1" "unpack_impl(FALSE, TRUE, F1(I!1))") (NAME-REPLACE "U2" "unpack_impl(FALSE, TRUE, F2(I!1))") (ASSERT) (NAME-REPLACE "S2" "(spec_unpack_impl(einf(U2), ez(U2), fz(U2), h(U2)(51)))") (NAME-REPLACE "S1" "(spec_unpack_impl(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") (LEMMA "STDs_QNAN_is_qnan_s") (INST -1 "(I!1`F1(63) XOR I!1`F2(63))") (LEMMA "INF_is_inf_s") (INST -1 "(I!1`F1(63) XOR I!1`F2(63))") (EXPAND* "zero?" "bv2ieee_bv" "fill" "^" "o" "inf?" "fill") (SMASH)) "" "") (defstep unp-spec-d () (THEN (SKOSIMP*) (EXPAND* "Dnan?" "Ds_nan?" "Dq_nan?" "Dinf?" "Dzero?" "Dnonzero?") (USE "not_sgl_and_dbl") (USE "not_div_and_mul") (EXPAND* "Dbv2ieee_bv" "md_unpack" "md_unpack_spec" "isMUL" "isDIV" "is_double" "nonzero?") (DO-WITH-TCC (CASE-REPLACE "(is_dblDIV(I!1`op) OR is_dblMUL(I!1`op))=TRUE") (BDDSIMP)) (REWRITE "unpack_F") (REWRITE "unpack_F") (LEMMA "spec_unpack_impl_dbl") (INST-CP -1 "I!1`F1" "TRUE") (INST -1 "I!1`F2" "TRUE") (NAME-REPLACE "U1" "unpack_impl(TRUE, TRUE, F1(I!1))") (NAME-REPLACE "U2" "unpack_impl(TRUE, TRUE, F2(I!1))") (ASSERT) (NAME-REPLACE "S2" "(spec_unpack_impl(einf(U2), ez(U2), fz(U2), h(U2)(51)))") (NAME-REPLACE "S1" "(spec_unpack_impl(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 "(I!1`F1(63) XOR I!1`F2(63))") (LEMMA "INF_is_inf_d") (INST -1 "(I!1`F1(63) XOR I!1`F2(63))") (EXPAND* "zero?" "bv2ieee_bv" "fill" "^" "o" "inf?" "fill") (SMASH)) "" "")