src/Tools/Argo/argo_cls.ML
changeset 63960 3daf02070be5
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/Argo/argo_cls.ML	Thu Sep 29 20:54:44 2016 +0200
     1.3 @@ -0,0 +1,45 @@
     1.4 +(*  Title:      Tools/Argo/argo_cls.ML
     1.5 +    Author:     Sascha Boehme
     1.6 +
     1.7 +Representation of clauses. Clauses are disjunctions of literals with a proof that explains
     1.8 +why the disjunction holds.
     1.9 +*)
    1.10 +
    1.11 +signature ARGO_CLS =
    1.12 +sig
    1.13 +  type clause = Argo_Lit.literal list * Argo_Proof.proof
    1.14 +  val eq_clause: clause * clause -> bool
    1.15 +
    1.16 +  (* two-literal watches for clauses *)
    1.17 +  type table
    1.18 +  val table: table
    1.19 +  val put_watches: clause -> Argo_Lit.literal * Argo_Lit.literal -> table -> table
    1.20 +  val get_watches: table -> clause -> Argo_Lit.literal * Argo_Lit.literal
    1.21 +end
    1.22 +
    1.23 +structure Argo_Cls: ARGO_CLS =
    1.24 +struct
    1.25 +
    1.26 +type clause = Argo_Lit.literal list * Argo_Proof.proof
    1.27 +
    1.28 +fun eq_clause ((_, p1), (_, p2)) = Argo_Proof.eq_proof_id (apply2 Argo_Proof.id_of (p1, p2))
    1.29 +fun clause_ord ((_, p1), (_, p2)) = Argo_Proof.proof_id_ord (apply2 Argo_Proof.id_of (p1, p2))
    1.30 +
    1.31 +
    1.32 +(* two-literal watches for clauses *)
    1.33 +
    1.34 +(*
    1.35 +  The CDCL solver keeps a mapping of some literals to clauses. Exactly two literals
    1.36 +  of a clause are used to index the clause.
    1.37 +*)
    1.38 +
    1.39 +structure Clstab = Table(type key = clause val ord = clause_ord)
    1.40 +
    1.41 +type table = (Argo_Lit.literal * Argo_Lit.literal) Clstab.table
    1.42 +
    1.43 +val table: table = Clstab.empty
    1.44 +
    1.45 +fun put_watches cls lp table = Clstab.update (cls, lp) table
    1.46 +fun get_watches table cls = the (Clstab.lookup table cls)
    1.47 +
    1.48 +end