isabelle: src/HOL/SMT/SMT.thy@cba22e2999d5 (annotated)

32618 42865636d006 added new method "smt": an oracle-based connection to external SMT solvers boehmes parents: diff changeset	1	(* Title: HOL/SMT/SMT.thy
42865636d006 added new method "smt": an oracle-based connection to external SMT solvers boehmes parents: diff changeset	2	Author: Sascha Boehme, TU Muenchen
42865636d006 added new method "smt": an oracle-based connection to external SMT solvers boehmes parents: diff changeset	3	*)
42865636d006 added new method "smt": an oracle-based connection to external SMT solvers boehmes parents: diff changeset	4
33010 39f73a59e855 added proof reconstructon for Z3, boehmes parents: 32618 diff changeset	5	header {* Bindings to several SMT solvers *}
32618 42865636d006 added new method "smt": an oracle-based connection to external SMT solvers boehmes parents: diff changeset	6
42865636d006 added new method "smt": an oracle-based connection to external SMT solvers boehmes parents: diff changeset	7	theory SMT
33010 39f73a59e855 added proof reconstructon for Z3, boehmes parents: 32618 diff changeset	8	imports SMT_Base Z3
32618 42865636d006 added new method "smt": an oracle-based connection to external SMT solvers boehmes parents: diff changeset	9	uses
42865636d006 added new method "smt": an oracle-based connection to external SMT solvers boehmes parents: diff changeset	10	"Tools/cvc3_solver.ML"
42865636d006 added new method "smt": an oracle-based connection to external SMT solvers boehmes parents: diff changeset	11	"Tools/yices_solver.ML"
42865636d006 added new method "smt": an oracle-based connection to external SMT solvers boehmes parents: diff changeset	12	begin
42865636d006 added new method "smt": an oracle-based connection to external SMT solvers boehmes parents: diff changeset	13
33010 39f73a59e855 added proof reconstructon for Z3, boehmes parents: 32618 diff changeset	14	setup {* CVC3_Solver.setup #> Yices_Solver.setup *}
32618 42865636d006 added new method "smt": an oracle-based connection to external SMT solvers boehmes parents: diff changeset	15
33010 39f73a59e855 added proof reconstructon for Z3, boehmes parents: 32618 diff changeset	16	declare [[ smt_solver = z3, smt_timeout = 20 ]]
32618 42865636d006 added new method "smt": an oracle-based connection to external SMT solvers boehmes parents: diff changeset	17	declare [[ smt_unfold_defs = true ]]
33010 39f73a59e855 added proof reconstructon for Z3, boehmes parents: 32618 diff changeset	18	declare [[ smt_trace = false, smt_keep = "", smt_cert = "" ]]
39f73a59e855 added proof reconstructon for Z3, boehmes parents: 32618 diff changeset	19	declare [[ z3_proofs = false, z3_options = "" ]]
32618 42865636d006 added new method "smt": an oracle-based connection to external SMT solvers boehmes parents: diff changeset	20
42865636d006 added new method "smt": an oracle-based connection to external SMT solvers boehmes parents: diff changeset	21	end

author	blanchet
	Tue, 27 Oct 2009 16:52:06 +0100
changeset 33556	cba22e2999d5
parent 33010	39f73a59e855
child 33472	e88f67d679c4
permissions	-rw-r--r--