isabelle: src/HOL/SAT.thy@3837045cc8a1 (annotated)

17618 1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	1	(* Title: HOL/SAT.thy
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	2	Author: Alwen Tiu, Tjark Weber
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	3	Copyright 2005
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	4
17627 ff1923b1978b cnf_struct renamed to cnf webertj parents: 17625 diff changeset	5	Basic setup for the 'sat' and 'satx' tactic.
17618 1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	6	*)
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	7
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	8	header {* Reconstructing external resolution proofs for propositional logic *}
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	9
26521 f8c4e79db153 tuned imports haftmann parents: 21588 diff changeset	10	theory SAT
f8c4e79db153 tuned imports haftmann parents: 21588 diff changeset	11	imports Refute
17722 8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	12	uses
26521 f8c4e79db153 tuned imports haftmann parents: 21588 diff changeset	13	"Tools/sat_funcs.ML"
17618 1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	14	begin
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	15
17722 8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	16	text {* \medskip Late package setup: default values for refute, see
21588 cd0dc678a205 simplified method setup; wenzelm parents: 17809 diff changeset	17	also theory @{theory Refute}. *}
17722 8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	18
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	19	refute_params
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	20	["itself"=1,
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	21	minsize=1,
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	22	maxsize=8,
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	23	maxvars=10000,
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	24	maxtime=60,
34120 f9920a3ddf50 added "no_assms" option to Refute, and include structured proof assumptions by default; blanchet parents: 32232 diff changeset	25	satsolver="auto",
f9920a3ddf50 added "no_assms" option to Refute, and include structured proof assumptions by default; blanchet parents: 32232 diff changeset	26	no_assms="false"]
17722 8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	27
32232 6c394343360f proper context for SAT tactics; wenzelm parents: 30549 diff changeset	28	ML {* structure sat = SATFunc(cnf) *}
17618 1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	29
32232 6c394343360f proper context for SAT tactics; wenzelm parents: 30549 diff changeset	30	method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o sat.sat_tac) *}
17618 1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	31	"SAT solver"
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	32
32232 6c394343360f proper context for SAT tactics; wenzelm parents: 30549 diff changeset	33	method_setup satx = {* Scan.succeed (SIMPLE_METHOD' o sat.satx_tac) *}
17618 1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	34	"SAT solver (with definitional CNF)"
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	35
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	36	end

author	wenzelm
	Thu, 13 Jan 2011 17:39:35 +0100
changeset 41537	3837045cc8a1
parent 39036	dff91b90d74c
child 46096	a00685a18e55
permissions	-rw-r--r--