1(*  Title:      Tools/Argo/argo_cls.ML
2    Author:     Sascha Boehme
3
4Representation of clauses. Clauses are disjunctions of literals with a proof that explains
5why the disjunction holds.
6*)
7
8signature ARGO_CLS =
9sig
10  type clause = Argo_Lit.literal list * Argo_Proof.proof
11  val eq_clause: clause * clause -> bool
12
13  (* two-literal watches for clauses *)
14  type table
15  val table: table
16  val put_watches: clause -> Argo_Lit.literal * Argo_Lit.literal -> table -> table
17  val get_watches: table -> clause -> Argo_Lit.literal * Argo_Lit.literal
18end
19
20structure Argo_Cls: ARGO_CLS =
21struct
22
23type clause = Argo_Lit.literal list * Argo_Proof.proof
24
25fun eq_clause ((_, p1), (_, p2)) = Argo_Proof.eq_proof_id (apply2 Argo_Proof.id_of (p1, p2))
26fun clause_ord ((_, p1), (_, p2)) = Argo_Proof.proof_id_ord (apply2 Argo_Proof.id_of (p1, p2))
27
28
29(* two-literal watches for clauses *)
30
31(*
32  The CDCL solver keeps a mapping of some literals to clauses. Exactly two literals
33  of a clause are used to index the clause.
34*)
35
36structure Clstab = Table(type key = clause val ord = clause_ord)
37
38type table = (Argo_Lit.literal * Argo_Lit.literal) Clstab.table
39
40val table: table = Clstab.empty
41
42fun put_watches cls lp table = Clstab.update (cls, lp) table
43fun get_watches table cls = the (Clstab.lookup table cls)
44
45end
46