1(*  Title:      Tools/Argo/argo_thy.ML
2    Author:     Sascha Boehme
3
4Combination of all theory solvers.
5
6Currently, it is assumed that theories have distinct domains. Theory solvers do not
7exchange knowledge among each other. This should be changed in the future. Relevant work is:
8
9  Greg Nelson and Derek C. Oppen. Simplification by cooperating decision procedures. In ACM
10  Transactions on Programming Languages and Systems, 1(2):245-257, 1979.
11
12  Leonardo de Moura and Nikolaj Bj/orner. Model-based Theory Combination. In Electronic Notes
13  in Theoretical Computer Science, volume 198(2), pages 37-49, 2008.
14*)
15
16signature ARGO_THY =
17sig
18  (* context *)
19  type context
20  val context: context
21
22  (* enriching the context *)
23  val add_atom: Argo_Term.term -> context -> Argo_Lit.literal option * context
24
25  (* main operations *)
26  val prepare: context -> context
27  val assume: Argo_Common.literal -> context -> Argo_Lit.literal Argo_Common.implied * context
28  val check: context -> Argo_Lit.literal Argo_Common.implied * context
29  val explain: Argo_Lit.literal -> context -> Argo_Cls.clause * context
30  val add_level: context -> context
31  val backtrack: context -> context
32end
33
34structure Argo_Thy: ARGO_THY =
35struct
36
37(* context *)
38
39type context = Argo_Cc.context * Argo_Simplex.context
40
41val context = (Argo_Cc.context, Argo_Simplex.context)
42
43fun map_cc f (cc, simplex) =
44  let val (x, cc) = f cc
45  in (x, (cc, simplex)) end
46
47fun map_simplex f (cc, simplex) =
48  let val (x, simplex) = f simplex
49  in (x, (cc, simplex)) end
50
51
52(* enriching the context *)
53
54fun add_atom t (cc, simplex) =
55  let
56    val (lit1, cc) = Argo_Cc.add_atom t cc
57    val (lit2, simplex) = Argo_Simplex.add_atom t simplex
58  in
59    (case fold (union Argo_Lit.eq_lit o the_list) [lit1, lit2] [] of
60      [] => (NONE, (cc, simplex))
61    | [lit] => (SOME lit, (cc, simplex))
62    | _ => raise Fail "unsynchronized theory solvers")
63  end
64    
65
66
67(* main operations *)
68
69fun prepare (cc, simplex) = (cc, Argo_Simplex.prepare simplex)
70
71local
72
73exception CONFLICT of Argo_Cls.clause * context
74
75datatype tag = All | Cc | Simplex
76
77fun apply f cx =
78  (case f cx of
79    (Argo_Common.Conflict cls, cx) => raise CONFLICT (cls, cx)
80  | (Argo_Common.Implied lits, cx) => (lits, cx))
81
82fun with_lits tag f (txs, lits, cx) =
83  let val (lits', cx) = f cx
84  in (fold (fn l => cons (tag, (l, NONE))) lits' txs, union Argo_Lit.eq_lit lits' lits, cx) end
85
86fun apply0 (tag, f) = with_lits tag (apply f)
87fun apply1 (tag, f) (tag', x) = if tag <> tag' then with_lits tag (apply (f x)) else I
88
89val assumes = [(Cc, map_cc o Argo_Cc.assume), (Simplex, map_simplex o Argo_Simplex.assume)]
90val checks = [(Cc, map_cc Argo_Cc.check), (Simplex, map_simplex Argo_Simplex.check)]
91
92fun propagate ([], lits, cx) = (Argo_Common.Implied lits, cx)
93  | propagate (txs, lits, cx) = propagate (fold_product apply1 assumes txs ([], lits, cx))
94
95in
96
97fun assume lp cx = propagate ([(All, lp)], [], cx)
98  handle CONFLICT (cls, cx) => (Argo_Common.Conflict cls, cx)
99
100fun check cx = propagate (fold apply0 checks ([], [], cx))
101  handle CONFLICT (cls, cx) => (Argo_Common.Conflict cls, cx)
102
103end
104
105fun explain lit (cc, simplex) =
106  (case Argo_Cc.explain lit cc of
107    SOME (cls, cc) => (cls, (cc, simplex))
108  | NONE =>
109      (case Argo_Simplex.explain lit simplex of
110        SOME (cls, simplex) => (cls, (cc, simplex))
111      | NONE => raise Fail "bad literal without explanation"))
112
113fun add_level (cc, simplex) = (Argo_Cc.add_level cc, Argo_Simplex.add_level simplex)
114
115fun backtrack (cc, simplex) = (Argo_Cc.backtrack cc, Argo_Simplex.backtrack simplex)
116
117end
118