Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/HOL/SMT/IsaMakefile
author boehmes
Fri, 18 Sep 2009 18:13:19 +0200
changeset 32618 42865636d006
permissions -rw-r--r--
added new method "smt": an oracle-based connection to external SMT solvers 
     1 

     2 ## targets

     3 

     4 default: HOL-SMT

     5 images: HOL-SMT

     6 test: 

     7 

     8 all: images test

     9 

    10 

    11 ## global settings

    12 

    13 SRC = $(ISABELLE_HOME)/src

    14 OUT = $(ISABELLE_OUTPUT)

    15 LOG = $(OUT)/log

    16 

    17 USEDIR = $(ISATOOL) usedir -v true 

    18 

    19 

    20 ## HOL-SMT

    21 

    22 HOL-SMT: $(OUT)/HOL-SMT

    23 

    24 $(OUT)/HOL-SMT: $(OUT)/HOL-Word ROOT.ML SMT_Definitions.thy SMT.thy \

    25   Tools/cancel_conj_disj.ML Tools/smt_normalize.ML Tools/smt_monomorph.ML \

    26   Tools/smt_translate.ML Tools/smt_builtin.ML Tools/smtlib_interface.ML \

    27   Tools/smt_solver.ML Tools/cvc3_solver.ML Tools/yices_solver.ML \

    28   Tools/z3_interface.ML Tools/z3_solver.ML Tools/z3_model.ML \

    29   Tools/z3_proof.ML Tools/z3_proof_rules.ML Tools/z3_proof_terms.ML

    30 	@$(USEDIR) -b HOL-Word HOL-SMT

    31 

    32 $(OUT)/HOL-Word:

    33 	@$(ISATOOL) make HOL-Word -C $(SRC)/HOL

    34 

    35 

    36 ## clean

    37 

    38 clean:

    39 	@rm -f $(OUT)/HOL-SMT
wneuper/isa