isabelle: src/HOL/SAT.thy@01e90256550d (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
21588 cd0dc678a205 simplified method setup; wenzelm parents: 17809 diff changeset	20	also theory @{theory Refute}. *}
17722 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
21588 cd0dc678a205 simplified method setup; wenzelm parents: 17809 diff changeset	33	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	34	"SAT solver"
1330157e156a new sat tactic imports resolution proofs from zChaff webertj parents: diff changeset	35
21588 cd0dc678a205 simplified method setup; wenzelm parents: 17809 diff changeset	36	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	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	paulson
	Fri, 02 Mar 2007 12:38:58 +0100
changeset 22383	01e90256550d
parent 21588	cd0dc678a205
child 26521	f8c4e79db153
permissions	-rw-r--r--