src/Tools/Argo/argo_cls.ML
author boehmes
Thu Sep 29 20:54:44 2016 +0200 (2016-09-29)
changeset 63960 3daf02070be5
permissions -rw-r--r--
new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
     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