isabelle: src/HOL/SAT.thy@12ca66b887a0 (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
26521 f8c4e79db153 tuned imports haftmann parents: 21588 diff changeset	11	theory SAT
f8c4e79db153 tuned imports haftmann parents: 21588 diff changeset	12	imports Refute
17722 8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	13	uses
26521 f8c4e79db153 tuned imports haftmann parents: 21588 diff changeset	14	"Tools/cnf_funcs.ML"
f8c4e79db153 tuned imports haftmann parents: 21588 diff changeset	15	"Tools/sat_funcs.ML"
17618 1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	16	begin
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	17
17722 8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	18	text {* \medskip Late package setup: default values for refute, see
21588 cd0dc678a205 simplified method setup; wenzelm parents: 17809 diff changeset	19	also theory @{theory Refute}. *}
17722 8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	20
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	21	refute_params
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	22	["itself"=1,
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	23	minsize=1,
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	24	maxsize=8,
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	25	maxvars=10000,
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	26	maxtime=60,
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	27	satsolver="auto"]
8e098e040c2e explicit dependencies of SAT vs. Refute; wenzelm parents: 17631 diff changeset	28
17627 ff1923b1978b cnf_struct renamed to cnf webertj parents: 17625 diff changeset	29	ML {* structure sat = SATFunc(structure cnf = cnf); *}
17618 1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	30
21588 cd0dc678a205 simplified method setup; wenzelm parents: 17809 diff changeset	31	method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD' sat.sat_tac) *}
17618 1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	32	"SAT solver"
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	33
21588 cd0dc678a205 simplified method setup; wenzelm parents: 17809 diff changeset	34	method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD' sat.satx_tac) *}
17618 1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	35	"SAT solver (with definitional CNF)"
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	36
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	37	end

author	nipkow
	Thu, 11 Dec 2008 08:56:02 +0100
changeset 29108	12ca66b887a0
parent 26521	f8c4e79db153
child 30510	4120fc59dd85
permissions	-rw-r--r--