isabelle: src/HOL/SAT.thy@8e098e040c2e (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	ID: $Id$
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	3	Author: Alwen Tiu, Tjark Weber
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	4	Copyright 2005
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	5
17627 ff1923b1978b cnf_struct renamed to cnf webertj parents: 17625 diff changeset	6	Basic setup for the 'sat' and 'satx' tactic.
17618 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
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	9	header {* Reconstructing external resolution proofs for propositional logic *}
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	10
17722 8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	11	theory SAT imports Refute
17618 1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	12
17722 8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	13	uses
17618 1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	14	"Tools/cnf_funcs.ML"
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	15	"Tools/sat_funcs.ML"
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	16
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	17	begin
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	18
17722 8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	19	text {* \medskip Late package setup: default values for refute, see
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	20	also theory @{text Refute}. *}
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	21
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	22	refute_params
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	23	["itself"=1,
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	24	minsize=1,
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	25	maxsize=8,
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	26	maxvars=10000,
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	27	maxtime=60,
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	28	satsolver="auto"]
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	29
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	30
17627 ff1923b1978b cnf_struct renamed to cnf webertj parents: 17625 diff changeset	31	ML {* structure sat = SATFunc(structure cnf = cnf); *}
17618 1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	32
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	33	method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD sat.sat_tac) *}
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	34	"SAT solver"
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	method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD sat.satx_tac) *}
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	37	"SAT solver (with definitional CNF)"
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	38
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	39	end

author	wenzelm
	Thu, 29 Sep 2005 15:50:45 +0200
changeset 17722	8e098e040c2e
parent 17631	152ab92e1009
child 17809	195045659c06
permissions	-rw-r--r--