diff -r b0ff69f0a248 -r 39f73a59e855 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Oct 20 08:10:47 2009 +0200 +++ b/src/HOL/IsaMakefile Tue Oct 20 10:11:30 2009 +0200 @@ -6,7 +6,7 @@ default: HOL generate: HOL-Generate-HOL HOL-Generate-HOLLight -images: HOL HOL-Base HOL-Plain HOL-Main HOL-Algebra HOL-Nominal HOL-NSA HOL-Word TLA HOL4 +images: HOL HOL-Base HOL-Plain HOL-Main HOL-Algebra HOL-Nominal HOL-NSA HOL-SMT HOL-Word TLA HOL4 #Note: keep targets sorted (except for HOL-Library and HOL-ex) test: \ @@ -40,7 +40,7 @@ HOL-Prolog \ HOL-SET-Protocol \ HOL-SizeChange \ - HOL-SMT \ + HOL-SMT-Examples \ HOL-Statespace \ HOL-Subst \ TLA-Buffer \ @@ -1146,15 +1146,222 @@ HOL-SMT: HOL-Word $(LOG)/HOL-SMT.gz -$(LOG)/HOL-SMT.gz: $(OUT)/HOL-Word SMT/SMT_Definitions.thy SMT/SMT.thy \ +$(LOG)/HOL-SMT.gz: $(OUT)/HOL-Word SMT/SMT_Base.thy SMT/Z3.thy SMT/SMT.thy \ SMT/Tools/smt_normalize.ML SMT/Tools/smt_monomorph.ML \ SMT/Tools/smt_translate.ML SMT/Tools/smt_builtin.ML \ SMT/Tools/smtlib_interface.ML SMT/Tools/smt_solver.ML \ SMT/Tools/cvc3_solver.ML SMT/Tools/yices_solver.ML \ - SMT/Tools/z3_interface.ML SMT/Tools/z3_solver.ML SMT/Tools/z3_model.ML + SMT/Tools/z3_proof_terms.ML SMT/Tools/z3_proof_rules.ML \ + SMT/Tools/z3_proof.ML SMT/Tools/z3_model.ML SMT/Tools/z3_interface.ML \ + SMT/Tools/z3_solver.ML @cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT +## HOL-SMT-Examples + +HOL-SMT-Examples: HOL-SMT $(LOG)/HOL-SMT-Examples.gz + +$(LOG)/HOL-SMT-Examples.gz: $(OUT)/HOL-SMT SMT/Examples/ROOT.ML \ + SMT/Examples/SMT_Examples.thy \ + SMT/Examples/cert/z3_arith_quant_01 \ + SMT/Examples/cert/z3_arith_quant_01.proof \ + SMT/Examples/cert/z3_arith_quant_02 \ + SMT/Examples/cert/z3_arith_quant_02.proof \ + SMT/Examples/cert/z3_arith_quant_03 \ + SMT/Examples/cert/z3_arith_quant_03.proof \ + SMT/Examples/cert/z3_arith_quant_04 \ + SMT/Examples/cert/z3_arith_quant_04.proof \ + SMT/Examples/cert/z3_arith_quant_05 \ + SMT/Examples/cert/z3_arith_quant_05.proof \ + SMT/Examples/cert/z3_arith_quant_06 \ + SMT/Examples/cert/z3_arith_quant_06.proof \ + SMT/Examples/cert/z3_arith_quant_07 \ + SMT/Examples/cert/z3_arith_quant_07.proof \ + SMT/Examples/cert/z3_arith_quant_08 \ + SMT/Examples/cert/z3_arith_quant_08.proof \ + SMT/Examples/cert/z3_arith_quant_09 \ + SMT/Examples/cert/z3_arith_quant_09.proof \ + SMT/Examples/cert/z3_arith_quant_10 \ + SMT/Examples/cert/z3_arith_quant_10.proof \ + SMT/Examples/cert/z3_arith_quant_11 \ + SMT/Examples/cert/z3_arith_quant_11.proof \ + SMT/Examples/cert/z3_arith_quant_12 \ + SMT/Examples/cert/z3_arith_quant_12.proof \ + SMT/Examples/cert/z3_arith_quant_13 \ + SMT/Examples/cert/z3_arith_quant_13.proof \ + SMT/Examples/cert/z3_arith_quant_14 \ + SMT/Examples/cert/z3_arith_quant_14.proof \ + SMT/Examples/cert/z3_arith_quant_15 \ + SMT/Examples/cert/z3_arith_quant_15.proof \ + SMT/Examples/cert/z3_arith_quant_16 \ + SMT/Examples/cert/z3_arith_quant_16.proof \ + SMT/Examples/cert/z3_arith_quant_17 \ + SMT/Examples/cert/z3_arith_quant_17.proof \ + SMT/Examples/cert/z3_arith_quant_18 \ + SMT/Examples/cert/z3_arith_quant_18.proof \ + SMT/Examples/cert/z3_bv_01 \ + SMT/Examples/cert/z3_bv_01.proof \ + SMT/Examples/cert/z3_bv_02 \ + SMT/Examples/cert/z3_bv_02.proof \ + SMT/Examples/cert/z3_bv_arith_01 \ + SMT/Examples/cert/z3_bv_arith_01.proof \ + SMT/Examples/cert/z3_bv_arith_02 \ + SMT/Examples/cert/z3_bv_arith_02.proof \ + SMT/Examples/cert/z3_bv_arith_03 \ + SMT/Examples/cert/z3_bv_arith_03.proof \ + SMT/Examples/cert/z3_bv_arith_04 \ + SMT/Examples/cert/z3_bv_arith_04.proof \ + SMT/Examples/cert/z3_bv_arith_05 \ + SMT/Examples/cert/z3_bv_arith_05.proof \ + SMT/Examples/cert/z3_bv_arith_06 \ + SMT/Examples/cert/z3_bv_arith_06.proof \ + SMT/Examples/cert/z3_bv_arith_07 \ + SMT/Examples/cert/z3_bv_arith_07.proof \ + SMT/Examples/cert/z3_bv_arith_08 \ + SMT/Examples/cert/z3_bv_arith_08.proof \ + SMT/Examples/cert/z3_bv_arith_09 \ + SMT/Examples/cert/z3_bv_arith_09.proof \ + SMT/Examples/cert/z3_bv_arith_10 \ + SMT/Examples/cert/z3_bv_arith_10.proof \ + SMT/Examples/cert/z3_bv_bit_01 \ + SMT/Examples/cert/z3_bv_bit_01.proof \ + SMT/Examples/cert/z3_bv_bit_02 \ + SMT/Examples/cert/z3_bv_bit_02.proof \ + SMT/Examples/cert/z3_bv_bit_03 \ + SMT/Examples/cert/z3_bv_bit_03.proof \ + SMT/Examples/cert/z3_bv_bit_04 \ + SMT/Examples/cert/z3_bv_bit_04.proof \ + SMT/Examples/cert/z3_bv_bit_05 \ + SMT/Examples/cert/z3_bv_bit_05.proof \ + SMT/Examples/cert/z3_bv_bit_06 \ + SMT/Examples/cert/z3_bv_bit_06.proof \ + SMT/Examples/cert/z3_bv_bit_07 \ + SMT/Examples/cert/z3_bv_bit_07.proof \ + SMT/Examples/cert/z3_bv_bit_08 \ + SMT/Examples/cert/z3_bv_bit_08.proof \ + SMT/Examples/cert/z3_bv_bit_09 \ + SMT/Examples/cert/z3_bv_bit_09.proof \ + SMT/Examples/cert/z3_bv_bit_10 \ + SMT/Examples/cert/z3_bv_bit_10.proof \ + SMT/Examples/cert/z3_bv_bit_11 \ + SMT/Examples/cert/z3_bv_bit_11.proof \ + SMT/Examples/cert/z3_bv_bit_12 \ + SMT/Examples/cert/z3_bv_bit_12.proof \ + SMT/Examples/cert/z3_bv_bit_13 \ + SMT/Examples/cert/z3_bv_bit_13.proof \ + SMT/Examples/cert/z3_bv_bit_14 \ + SMT/Examples/cert/z3_bv_bit_14.proof \ + SMT/Examples/cert/z3_bv_bit_15 \ + SMT/Examples/cert/z3_bv_bit_15.proof \ + SMT/Examples/cert/z3_fol_01 \ + SMT/Examples/cert/z3_fol_01.proof \ + SMT/Examples/cert/z3_fol_02 \ + SMT/Examples/cert/z3_fol_02.proof \ + SMT/Examples/cert/z3_fol_03 \ + SMT/Examples/cert/z3_fol_03.proof \ + SMT/Examples/cert/z3_fol_04 \ + SMT/Examples/cert/z3_fol_04.proof \ + SMT/Examples/cert/z3_hol_01 \ + SMT/Examples/cert/z3_hol_01.proof \ + SMT/Examples/cert/z3_hol_02 \ + SMT/Examples/cert/z3_hol_02.proof \ + SMT/Examples/cert/z3_hol_03 \ + SMT/Examples/cert/z3_hol_03.proof \ + SMT/Examples/cert/z3_hol_04 \ + SMT/Examples/cert/z3_hol_04.proof \ + SMT/Examples/cert/z3_hol_05 \ + SMT/Examples/cert/z3_hol_05.proof \ + SMT/Examples/cert/z3_hol_06 \ + SMT/Examples/cert/z3_hol_06.proof \ + SMT/Examples/cert/z3_hol_07 \ + SMT/Examples/cert/z3_hol_07.proof \ + SMT/Examples/cert/z3_hol_08 \ + SMT/Examples/cert/z3_hol_08.proof \ + SMT/Examples/cert/z3_linarith_01 \ + SMT/Examples/cert/z3_linarith_01.proof \ + SMT/Examples/cert/z3_linarith_02 \ + SMT/Examples/cert/z3_linarith_02.proof \ + SMT/Examples/cert/z3_linarith_03 \ + SMT/Examples/cert/z3_linarith_03.proof \ + SMT/Examples/cert/z3_linarith_04 \ + SMT/Examples/cert/z3_linarith_04.proof \ + SMT/Examples/cert/z3_linarith_05 \ + SMT/Examples/cert/z3_linarith_05.proof \ + SMT/Examples/cert/z3_linarith_06 \ + SMT/Examples/cert/z3_linarith_06.proof \ + SMT/Examples/cert/z3_linarith_07 \ + SMT/Examples/cert/z3_linarith_07.proof \ + SMT/Examples/cert/z3_linarith_08 \ + SMT/Examples/cert/z3_linarith_08.proof \ + SMT/Examples/cert/z3_linarith_09 \ + SMT/Examples/cert/z3_linarith_09.proof \ + SMT/Examples/cert/z3_linarith_10 \ + SMT/Examples/cert/z3_linarith_10.proof \ + SMT/Examples/cert/z3_linarith_11 \ + SMT/Examples/cert/z3_linarith_11.proof \ + SMT/Examples/cert/z3_linarith_12 \ + SMT/Examples/cert/z3_linarith_12.proof \ + SMT/Examples/cert/z3_linarith_13 \ + SMT/Examples/cert/z3_linarith_13.proof \ + SMT/Examples/cert/z3_linarith_14 \ + SMT/Examples/cert/z3_linarith_14.proof \ + SMT/Examples/cert/z3_linarith_15 \ + SMT/Examples/cert/z3_linarith_15.proof \ + SMT/Examples/cert/z3_linarith_16 \ + SMT/Examples/cert/z3_linarith_16.proof \ + SMT/Examples/cert/z3_mono_01 \ + SMT/Examples/cert/z3_mono_01.proof \ + SMT/Examples/cert/z3_mono_02 \ + SMT/Examples/cert/z3_mono_02.proof \ + SMT/Examples/cert/z3_nat_arith_01 \ + SMT/Examples/cert/z3_nat_arith_01.proof \ + SMT/Examples/cert/z3_nat_arith_02 \ + SMT/Examples/cert/z3_nat_arith_02.proof \ + SMT/Examples/cert/z3_nat_arith_03 \ + SMT/Examples/cert/z3_nat_arith_03.proof \ + SMT/Examples/cert/z3_nat_arith_04 \ + SMT/Examples/cert/z3_nat_arith_04.proof \ + SMT/Examples/cert/z3_nat_arith_05 \ + SMT/Examples/cert/z3_nat_arith_05.proof \ + SMT/Examples/cert/z3_nat_arith_06 \ + SMT/Examples/cert/z3_nat_arith_06.proof \ + SMT/Examples/cert/z3_nat_arith_07 \ + SMT/Examples/cert/z3_nat_arith_07.proof \ + SMT/Examples/cert/z3_nlarith_01 \ + SMT/Examples/cert/z3_nlarith_01.proof \ + SMT/Examples/cert/z3_nlarith_02 \ + SMT/Examples/cert/z3_nlarith_02.proof \ + SMT/Examples/cert/z3_nlarith_03 \ + SMT/Examples/cert/z3_nlarith_03.proof \ + SMT/Examples/cert/z3_nlarith_04 \ + SMT/Examples/cert/z3_nlarith_04.proof \ + SMT/Examples/cert/z3_pair_01 \ + SMT/Examples/cert/z3_pair_01.proof \ + SMT/Examples/cert/z3_pair_02 \ + SMT/Examples/cert/z3_pair_02.proof \ + SMT/Examples/cert/z3_prop_01 \ + SMT/Examples/cert/z3_prop_01.proof \ + SMT/Examples/cert/z3_prop_02 \ + SMT/Examples/cert/z3_prop_02.proof \ + SMT/Examples/cert/z3_prop_03 \ + SMT/Examples/cert/z3_prop_03.proof \ + SMT/Examples/cert/z3_prop_04 \ + SMT/Examples/cert/z3_prop_04.proof \ + SMT/Examples/cert/z3_prop_05 \ + SMT/Examples/cert/z3_prop_05.proof \ + SMT/Examples/cert/z3_prop_06 \ + SMT/Examples/cert/z3_prop_06.proof \ + SMT/Examples/cert/z3_prop_07 \ + SMT/Examples/cert/z3_prop_07.proof \ + SMT/Examples/cert/z3_prop_08 \ + SMT/Examples/cert/z3_prop_08.proof \ + SMT/Examples/cert/z3_prop_09 \ + SMT/Examples/cert/z3_prop_09.proof \ + SMT/Examples/cert/z3_prop_10 \ + SMT/Examples/cert/z3_prop_10.proof + @cd SMT; $(ISABELLE_TOOL) usedir $(OUT)/HOL-SMT Examples + + ## clean clean: @@ -1177,4 +1384,6 @@ $(LOG)/HOL-Unix.gz $(OUT)/HOL-Word $(LOG)/HOL-Word.gz \ $(LOG)/HOL-Word-Examples.gz $(OUT)/HOL-NSA \ $(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz \ - $(LOG)/HOL-Mirabelle.gz $(LOG)/HOL-SMT.gz + $(LOG)/HOL-Mirabelle.gz $(LOG)/HOL-SMT.gz \ + $(LOG)/HOL-SMT-Examples.gz +