isabelle: src/HOL/SAT.thy@ff13585fbdab (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
17809 195045659c06 Tactics sat and satx reimplemented, several improvements webertj parents: 17722 diff changeset	33	method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD (sat.sat_tac 1)) *}
17618 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
17809 195045659c06 Tactics sat and satx reimplemented, several improvements webertj parents: 17722 diff changeset	36	method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD (sat.satx_tac 1)) *}
17618 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
	Sat, 27 May 2006 17:42:00 +0200
changeset 19735	ff13585fbdab
parent 17809	195045659c06
child 21588	cd0dc678a205
permissions	-rw-r--r--