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