equal
deleted
inserted
replaced
|
1 (* Title: Tools/Argo/argo_cls.ML |
|
2 Author: Sascha Boehme |
|
3 |
|
4 Representation of clauses. Clauses are disjunctions of literals with a proof that explains |
|
5 why the disjunction holds. |
|
6 *) |
|
7 |
|
8 signature ARGO_CLS = |
|
9 sig |
|
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 |
|
18 end |
|
19 |
|
20 structure Argo_Cls: ARGO_CLS = |
|
21 struct |
|
22 |
|
23 type clause = Argo_Lit.literal list * Argo_Proof.proof |
|
24 |
|
25 fun eq_clause ((_, p1), (_, p2)) = Argo_Proof.eq_proof_id (apply2 Argo_Proof.id_of (p1, p2)) |
|
26 fun 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 |
|
36 structure Clstab = Table(type key = clause val ord = clause_ord) |
|
37 |
|
38 type table = (Argo_Lit.literal * Argo_Lit.literal) Clstab.table |
|
39 |
|
40 val table: table = Clstab.empty |
|
41 |
|
42 fun put_watches cls lp table = Clstab.update (cls, lp) table |
|
43 fun get_watches table cls = the (Clstab.lookup table cls) |
|
44 |
|
45 end |