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