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