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