1210 |
1212 |
1211 ## HOL-SMT |
1213 ## HOL-SMT |
1212 |
1214 |
1213 HOL-SMT: HOL-Word $(OUT)/HOL-SMT |
1215 HOL-SMT: HOL-Word $(OUT)/HOL-SMT |
1214 |
1216 |
1215 $(OUT)/HOL-SMT: $(OUT)/HOL-Word SMT/SMT_Base.thy SMT/Z3.thy \ |
1217 $(OUT)/HOL-SMT: $(OUT)/HOL-Word SMT/ROOT.ML SMT/SMT_Base.thy SMT/Z3.thy \ |
1216 SMT/SMT.thy SMT/Tools/smt_normalize.ML SMT/Tools/smt_monomorph.ML \ |
1218 SMT/SMT.thy SMT/Tools/smt_normalize.ML SMT/Tools/smt_monomorph.ML \ |
1217 SMT/Tools/smt_translate.ML SMT/Tools/smtlib_interface.ML \ |
1219 SMT/Tools/smt_translate.ML SMT/Tools/smtlib_interface.ML \ |
1218 SMT/Tools/smt_solver.ML SMT/Tools/cvc3_solver.ML \ |
1220 SMT/Tools/smt_solver.ML SMT/Tools/cvc3_solver.ML \ |
1219 SMT/Tools/yices_solver.ML SMT/Tools/z3_proof_terms.ML \ |
1221 SMT/Tools/yices_solver.ML SMT/Tools/z3_proof_terms.ML \ |
1220 SMT/Tools/z3_proof_rules.ML SMT/Tools/z3_proof.ML \ |
1222 SMT/Tools/z3_proof_rules.ML SMT/Tools/z3_proof.ML \ |
1221 SMT/Tools/z3_model.ML SMT/Tools/z3_interface.ML SMT/Tools/z3_solver.ML |
1223 SMT/Tools/z3_model.ML SMT/Tools/z3_interface.ML SMT/Tools/z3_solver.ML |
1222 @cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT |
1224 @cd SMT; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-Word HOL-SMT |
1223 |
1225 |
1224 |
1226 |
1225 ## HOL-SMT-Examples |
1227 ## HOL-SMT_Examples |
1226 |
1228 |
1227 HOL-SMT-Examples: HOL-SMT $(LOG)/HOL-SMT-Examples.gz |
1229 HOL-SMT_Examples: HOL-SMT $(LOG)/HOL-SMT_Examples.gz |
1228 |
1230 |
1229 $(LOG)/HOL-SMT-Examples.gz: $(OUT)/HOL-SMT SMT/Examples/ROOT.ML \ |
1231 $(LOG)/HOL-SMT_Examples.gz: $(OUT)/HOL-SMT SMT/Examples/ROOT.ML \ |
1230 SMT/Examples/SMT_Examples.thy SMT/Examples/cert/z3_arith_quant_01 \ |
1232 SMT/Examples/SMT_Examples.thy SMT/Examples/cert/z3_arith_quant_01 \ |
1231 SMT/Examples/cert/z3_arith_quant_01.proof \ |
1233 SMT/Examples/cert/z3_arith_quant_01.proof \ |
1232 SMT/Examples/cert/z3_arith_quant_02 \ |
1234 SMT/Examples/cert/z3_arith_quant_02 \ |
1233 SMT/Examples/cert/z3_arith_quant_02.proof \ |
1235 SMT/Examples/cert/z3_arith_quant_02.proof \ |
1234 SMT/Examples/cert/z3_arith_quant_03 \ |
1236 SMT/Examples/cert/z3_arith_quant_03 \ |
1379 SMT/Examples/cert/z3_prop_09.proof SMT/Examples/cert/z3_prop_10 \ |
1381 SMT/Examples/cert/z3_prop_09.proof SMT/Examples/cert/z3_prop_10 \ |
1380 SMT/Examples/cert/z3_prop_10.proof |
1382 SMT/Examples/cert/z3_prop_10.proof |
1381 @cd SMT; $(ISABELLE_TOOL) usedir $(OUT)/HOL-SMT Examples |
1383 @cd SMT; $(ISABELLE_TOOL) usedir $(OUT)/HOL-SMT Examples |
1382 |
1384 |
1383 |
1385 |
|
1386 ## HOL-Boogie |
|
1387 |
|
1388 HOL-Boogie: HOL-SMT $(OUT)/HOL-Boogie |
|
1389 |
|
1390 $(OUT)/HOL-Boogie: $(OUT)/HOL-SMT Boogie/ROOT.ML Boogie/Boogie.thy \ |
|
1391 Boogie/Tools/boogie_vcs.ML Boogie/Tools/boogie_loader.ML \ |
|
1392 Boogie/Tools/boogie_commands.ML Boogie/Tools/boogie_split.ML |
|
1393 @cd Boogie; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL-SMT HOL-Boogie |
|
1394 |
|
1395 |
|
1396 ## HOL-Boogie_Examples |
|
1397 |
|
1398 HOL-Boogie_Examples: HOL-Boogie $(LOG)/HOL-Boogie_Examples.gz |
|
1399 |
|
1400 $(LOG)/HOL-Boogie_Examples.gz: $(OUT)/HOL-SMT Boogie/Examples/ROOT.ML \ |
|
1401 Boogie/Examples/Boogie_Max.thy Boogie/Examples/Boogie_Max.b2i \ |
|
1402 Boogie/Examples/Boogie_Dijkstra.thy Boogie/Examples/VCC_Max.thy \ |
|
1403 Boogie/Examples/Boogie_Dijkstra.b2i Boogie/Examples/VCC_Max.b2i \ |
|
1404 Boogie/Examples/cert/Boogie_b_max \ |
|
1405 Boogie/Examples/cert/Boogie_b_max.proof \ |
|
1406 Boogie/Examples/cert/Boogie_b_Dijkstra \ |
|
1407 Boogie/Examples/cert/Boogie_b_Dijkstra.proof \ |
|
1408 Boogie/Examples/cert/VCC_b_maximum \ |
|
1409 Boogie/Examples/cert/VCC_b_maximum.proof |
|
1410 @cd Boogie; $(ISABELLE_TOOL) usedir $(OUT)/HOL-Boogie Examples |
|
1411 |
|
1412 |
1384 ## clean |
1413 ## clean |
1385 |
1414 |
1386 clean: |
1415 clean: |
1387 @rm -f $(OUT)/HOL-Plain $(OUT)/HOL-Main $(OUT)/HOL \ |
1416 @rm -f $(OUT)/HOL-Plain $(OUT)/HOL-Main $(OUT)/HOL \ |
1388 $(OUT)/HOL-Nominal $(OUT)/TLA $(LOG)/HOL.gz \ |
1417 $(OUT)/HOL-Nominal $(OUT)/TLA $(LOG)/HOL.gz \ |