1(* ---------------------------------------------------------------------- 2 contains configuration info for HolSatLib that is independent of the 3 SAT solver 4 5 SAT solver specific config is in SatSolver.sml 6 7 the main reason for having this as an opaque type is to give 8 HolSatLib a stable signature 9 ---------------------------------------------------------------------- *) 10 11structure satConfig :> satConfig = 12struct 13 14local 15 16open Globals HolKernel Parse 17 18in 19 20open SatSolvers Abbrev 21 22type sat_config = 23 { 24 pterm : term, (* input problem term *) 25 solver: sat_solver, (* solver to use *) 26 infile: string option, (* DIMACS input file; overrides pterm if SOME *) 27 proof : string option, 28 (* proof trace file in HolSatLib format; overrides solver if SOME*) 29 flags : {is_cnf:bool,is_proved:bool} 30 (* problem already in cnf, result is checked in HOL *) 31 } 32 33val base_config = 34 {pterm = boolSyntax.T, solver = minisatp, infile = NONE, proof = NONE, 35 flags = {is_cnf=false,is_proved=true}} 36 37(* getters *) 38 39fun get_term (c:sat_config) = (#pterm c) 40 41fun get_solver (c:sat_config) = (#solver c) 42 43(* if SOME, then valOf is name of cnf file on disk that is to be used directly*) 44fun get_infile (c:sat_config) = (#infile c) 45 46(* if SOME, then valOf is name of proof file (HolSat format) on disk that is 47 to be used directly *) 48fun get_proof (c:sat_config) = (#proof c) 49 50(* if true, then we skip the def_cnf conversion. 51 if infile is SOME, then this is set to true *) 52fun get_flag_is_cnf (c:sat_config) = #is_cnf (#flags c) 53 54fun get_flag_is_proved (c:sat_config) = #is_proved (#flags c) 55 56(* setters *) 57fun set_term tm (c:sat_config) = 58 {pterm = tm, solver = #solver c, infile = #infile c, proof = #proof c, 59 flags = {is_cnf = #is_cnf (#flags c),is_proved = #is_proved (#flags c)}} 60 61fun set_solver ss (c:sat_config) = 62 {pterm = #pterm c, solver = ss, infile = #infile c, proof = #proof c, 63 flags = {is_cnf = #is_cnf (#flags c),is_proved = #is_proved (#flags c)}} 64 65fun set_infile nm (c:sat_config) = (* also sets is_cnf to true *) 66 {pterm = #pterm c, solver = #solver c, infile = SOME nm, proof = #proof c, 67 flags = {is_cnf = true,is_proved = #is_proved (#flags c)}} 68 69fun set_proof nm (c:sat_config) = (* also sets is_cnf to true *) 70 {pterm = #pterm c, solver = #solver c, infile = #infile c, proof = SOME nm, 71 flags = {is_cnf = true,is_proved = #is_proved (#flags c)}} 72 73fun set_flag_is_cnf is (c:sat_config) = 74 {pterm = #pterm c, solver = #solver c, infile = #infile c, proof = #proof c, 75 flags = {is_cnf = is,is_proved = #is_proved (#flags c)}} 76 77fun set_flag_is_proved ip (c:sat_config) = 78 {pterm = #pterm c, solver = #solver c, infile = #infile c, proof = #proof c, 79 flags = {is_cnf = #is_cnf (#flags c),is_proved = ip}} 80 81(* destruction (does not return flags) *) 82fun dest_config c = (get_term c, get_solver c, get_infile c, get_proof c, 83 get_flag_is_cnf c, get_flag_is_proved c) 84 85end 86end 87