1(*  Title:      Tools/Argo/argo_term.ML
2    Author:     Sascha Boehme
3
4Internal language of the Argo solver.
5
6Terms are fully-shared via hash-consing. Alpha-equivalent terms have the same identifier.
7*)
8
9signature ARGO_TERM =
10sig
11  (* data types *)
12  type meta
13  datatype term = T of meta * Argo_Expr.kind * term list
14
15  (* term operations *)
16  val id_of: term -> int
17  val expr_of: term -> Argo_Expr.expr
18  val type_of: term -> Argo_Expr.typ
19  val eq_term: term * term -> bool
20  val term_ord: term ord
21
22  (* context *)
23  type context
24  val context: context
25
26  (* identifying expressions *)
27  datatype item = Expr of Argo_Expr.expr | Term of term
28  datatype identified = New of term | Known of term
29  val identify_item: item -> context -> identified * context
30end
31
32structure Argo_Term: ARGO_TERM =
33struct
34
35(* data types *)
36
37(*
38  The type meta is intentionally hidden to prevent that functions outside of this structure
39  are able to build terms. Meta stores the identifier of the term as well as the complete
40  expression underlying the term.
41*)
42
43datatype meta = M of int * Argo_Expr.expr
44datatype term = T of meta * Argo_Expr.kind * term list
45
46
47(* term operations *)
48
49fun id_of (T (M (id, _), _, _)) = id
50fun expr_of (T (M (_, e), _, _)) = e
51fun type_of t = Argo_Expr.type_of (expr_of t)
52
53(*
54  Comparing terms is fast as only the identifiers are compared. No expressions need to
55  be taken into account.
56*)
57
58fun eq_term (t1, t2) = (id_of t1 = id_of t2)
59fun term_ord (t1, t2) = int_ord (id_of t1, id_of t2)
60
61
62(* sharing of terms *)
63
64(*
65  Kinds are short representation of expressions. Constants and numbers carry additional
66  information and have no arguments. Their kind is hence similar to them. All other expressions
67  are stored in a flat way with identifiers of shared terms as arguments instead of expression
68  as arguments.
69*)
70
71datatype kind =
72  Con of string * Argo_Expr.typ |
73  Num of Rat.rat |
74  Exp of int list
75
76fun kind_of (Argo_Expr.E (Argo_Expr.Con c, _)) _ = Con c
77  | kind_of (Argo_Expr.E (Argo_Expr.Num n, _)) _ = Num n
78  | kind_of (Argo_Expr.E (k, _)) is = Exp (Argo_Expr.int_of_kind k :: is)
79
80fun int_of_kind (Con _) = 1
81  | int_of_kind (Num _) = 2
82  | int_of_kind (Exp _) = 3
83
84fun kind_ord (Con c1, Con c2) = Argo_Expr.con_ord (c1, c2)
85  | kind_ord (Num n1, Num n2) = Rat.ord (n1, n2)
86  | kind_ord (Exp is1, Exp is2) = dict_ord int_ord (is1, is2)
87  | kind_ord (k1, k2) = int_ord (int_of_kind k1, int_of_kind k2)
88
89structure Kindtab = Table(type key = kind val ord = kind_ord)
90
91(*
92  The context keeps track of the next unused identifier as well as all shared terms,
93  which are indexed by their unique kind. For each term, a boolean marker flag is stored.
94  When set to true on an atom, the atom is already asserted to the solver core. When set to
95  true on an if-then-else term, the term has already been lifted.
96
97  Zero is intentionally avoided as identifier, since literals use term identifiers
98  with a sign as literal identifiers.
99*)
100
101type context = {
102  next_id: int,
103  terms: (term * bool) Kindtab.table}
104
105fun mk_context next_id terms: context = {next_id=next_id, terms=terms}
106
107val context = mk_context 1 Kindtab.empty
108
109fun note_atom true kind (t, false) ({next_id, terms}: context) =
110      mk_context next_id (Kindtab.update (kind, (t, true)) terms)
111  | note_atom _ _ _ cx = cx
112
113fun with_unique_id kind is_atom (e as Argo_Expr.E (k, _)) ts ({next_id, terms}: context) =
114  let val t = T (M (next_id, e), k, ts)
115  in ((t, false), mk_context (next_id + 1) (Kindtab.update (kind, (t, is_atom)) terms)) end
116
117fun unique kind is_atom e ts (cx as {terms, ...}: context) =
118  (case Kindtab.lookup terms kind of
119    SOME tp => (tp, note_atom is_atom kind tp cx)
120  | NONE => with_unique_id kind is_atom e ts cx)
121
122
123(* identifying expressions *)
124
125(*
126  Only atoms, i.e., boolean propositons, and if-then-else expressions need to be identified.
127  Other terms are identified implicitly. The identification process works bottom-up.
128
129  The solver core needs to know whether an atom has already been added. Likewise, the clausifier
130  needs to know whether an if-then-else expression has already been lifted. Therefore,
131  the identified term is marked as either "new" when identified for the first time or
132  "known" when it has already been identified before.
133*)
134
135datatype item = Expr of Argo_Expr.expr | Term of term
136datatype identified = New of term | Known of term
137
138fun identify_head is_atom e (ts, cx) = unique (kind_of e (map id_of ts)) is_atom e ts cx
139
140fun identify is_atom (e as Argo_Expr.E (_, es)) cx =
141  identify_head is_atom e (fold_map (apfst fst oo identify false) es cx)
142
143fun identified (t, true) = Known t
144  | identified (t, false) = New t
145
146fun identify_item (Expr e) cx = identify true e cx |>> identified
147  | identify_item (Term (t as T (_, _, ts))) cx =
148      identify_head true (expr_of t) (ts, cx) |>> identified
149
150end
151
152structure Argo_Termtab = Table(type key = Argo_Term.term val ord = Argo_Term.term_ord)
153