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
```