src/Tools/Argo/argo_cc.ML

+(*  Title:      Tools/Argo/argo_cc.ML
+    Author:     Sascha Boehme
+    Author:     Dmitriy Traytel and Matthias Franze, TU Muenchen
+
+Equality reasoning based on congurence closure. It features:
+
+  * congruence closure for any term that participates in equalities
+  * support for predicates
+
+These features might be added:
+
+  * caching of explanations while building proofs to obtain shorter proofs
+    and faster proof checking
+  * propagating relevant merges of equivalence classes to all other theory solvers
+  * propagating new relevant negated equalities to all other theory solvers
+  * creating lemma "f ~= g | a ~= b | f a = g b" for asserted negated equalities
+    between "f a" and "g b" (dynamic ackermannization)
+
+The implementation is inspired by:
+
+  Robert Nieuwenhuis and Albert Oliveras. Fast Congruence Closure and
+  Extensions. In Information and Computation, volume 205(4),
+  pages 557-580, 2007.
+
+  Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras,
+  Cesare Tinelli. DPLL(T): Fast decision procedures. In Lecture Notes in
+  Computer Science, volume 3114, pages 175-188. Springer, 2004.
+*)
+
+signature ARGO_CC =
+sig
+  (* context *)
+  type context
+  val context: context
+
+  (* simplification *)
+  val simplify: Argo_Rewr.context -> Argo_Rewr.context
+  
+  (* enriching the context *)
+  val add_atom: Argo_Term.term -> context -> Argo_Lit.literal option * context
+
+  (* main operations *)
+  val assume: Argo_Common.literal -> context -> Argo_Lit.literal Argo_Common.implied * context
+  val check: context -> Argo_Lit.literal Argo_Common.implied * context
+  val explain: Argo_Lit.literal -> context -> (Argo_Cls.clause * context) option
+  val add_level: context -> context
+  val backtrack: context -> context
+end
+
+structure Argo_Cc: ARGO_CC =
+struct
+
+(* tables indexed by pairs of terms *)
+
+val term2_ord = prod_ord Argo_Term.term_ord Argo_Term.term_ord
+
+structure Argo_Term2tab = Table(type key = Argo_Term.term * Argo_Term.term val ord = term2_ord)
+
+
+(* equality certificates *)
+
+(*
+  The solver keeps assumed equalities to produce explanations later on.
+
+  A flat equality (lp, (t1, t2)) consists of the assumed literal and its proof
+  as well as the terms t1 and t2 that are assumed to be equal. The literal expresses
+  the equality t1 = t2.
+
+  A congruence equality (t1, t2) is an equality t1 = t2 where both terms are
+  applications (f a) and (g b).
+
+  A symmetric equality eq is a marker for applying the symmetry rule to eq.
+*)
+
+datatype eq =
+  Flat of Argo_Common.literal * (Argo_Term.term * Argo_Term.term) |
+  Cong of Argo_Term.term * Argo_Term.term |
+  Symm of eq
+
+fun dest_eq (Flat (_, tp)) = tp
+  | dest_eq (Cong tp) = tp
+  | dest_eq (Symm eq) = swap (dest_eq eq)
+
+fun symm (Symm eq) = eq
+  | symm eq = Symm eq
+
+fun negate (Flat ((lit, p), tp)) = Flat ((Argo_Lit.negate lit, p), tp)
+  | negate (Cong tp) = Cong tp
+  | negate (Symm eq) = Symm (negate eq)
+
+fun dest_app (Argo_Term.T (_, Argo_Expr.App, [t1, t2])) = (t1, t2)
+  | dest_app _ = raise Fail "bad application"
+
+
+(* context *)
+
+(*
+  Each representative keeps track of the yet unimplied atoms in which this any member of
+  this representative's equivalence class occurs. An atom is either a list of equalities
+  between two terms, a list of predicates or a certificate. The certificate denotes that
+  this equivalence class contains already implied predicates, and the literal accompanying
+  the certificate specifies the polarity of these predicates.
+*)
+
+datatype atoms =
+  Eqs of (Argo_Term.term * Argo_Term.term) list |
+  Preds of Argo_Term.term list |
+  Cert of Argo_Common.literal
+
+(*
+  Each representative has an associated ritem that contains the members of the
+  equivalence class, the yet unimplied atoms and further information.
+*)
+
+type ritem = {
+  size: int, (* the size of the equivalence class *)
+  class: Argo_Term.term list, (* the equivalence class as a list of distinct terms *)
+  occs: Argo_Term.term list, (* a list of all application terms in which members of
+    the equivalence class occur either as function or as argument *)
+  neqs: (Argo_Term.term * eq) list, (* a list of terms from disjoint equivalence classes,
+    for each term of this list there is a certificate of a negated equality that is
+    required to explain why the equivalence classes are disjoint *)
+  atoms: atoms} (* the atoms of the representative *)
+
+type repr = Argo_Term.term Argo_Termtab.table
+type rdata = ritem Argo_Termtab.table
+type apps = Argo_Term.term Argo_Term2tab.table
+type trace = (Argo_Term.term * eq) Argo_Termtab.table
+
+type context = {
+  repr: repr, (* a table mapping terms to their representatives *)
+  rdata: rdata, (* a table mapping representatives to their ritems *)
+  apps: apps, (* a table mapping a function and an argument to their application *)
+  trace: trace, (* the proof forest used to trace assumed and implied equalities *)
+  prf: Argo_Proof.context, (* the proof context *)
+  back: (repr * rdata * apps * trace) list} (* backtracking information *)
+
+fun mk_context repr rdata apps trace prf back: context =
+  {repr=repr, rdata=rdata, apps=apps, trace=trace, prf=prf, back=back}
+
+val context =
+  mk_context Argo_Termtab.empty Argo_Termtab.empty Argo_Term2tab.empty Argo_Termtab.empty
+    Argo_Proof.cc_context []
+
+fun repr_of repr t = the_default t (Argo_Termtab.lookup repr t)
+fun repr_of' ({repr, ...}: context) = repr_of repr
+fun put_repr t r = Argo_Termtab.update (t, r)
+
+fun mk_ritem size class occs neqs atoms: ritem =
+  {size=size, class=class, occs=occs, neqs=neqs, atoms=atoms}
+
+fun as_ritem t = mk_ritem 1 [t] [] [] (Eqs [])
+fun as_pred_ritem t = mk_ritem 1 [t] [] [] (Preds [t])
+fun gen_ritem_of mk rdata r = the_default (mk r) (Argo_Termtab.lookup rdata r)
+fun ritem_of rdata = gen_ritem_of as_ritem rdata
+fun ritem_of_pred rdata = gen_ritem_of as_pred_ritem rdata
+fun ritem_of' ({rdata, ...}: context) = ritem_of rdata
+fun put_ritem r ri = Argo_Termtab.update (r, ri)
+
+fun add_occ r occ = Argo_Termtab.map_default (r, as_ritem r)
+  (fn {size, class, occs, neqs, atoms}: ritem => mk_ritem size class (occ :: occs) neqs atoms)
+
+fun put_atoms atoms ({size, class, occs, neqs, ...}: ritem) = mk_ritem size class occs neqs atoms
+
+fun add_eq_atom r atom = Argo_Termtab.map_default (r, as_ritem r)
+  (fn ri as {atoms=Eqs atoms, ...}: ritem => put_atoms (Eqs (atom :: atoms)) ri
+    | ri => put_atoms (Eqs [atom]) ri)
+
+fun lookup_app apps tp = Argo_Term2tab.lookup apps tp
+fun put_app tp app = Argo_Term2tab.update_new (tp, app)
+
+
+(* traces for explanations *)
+
+(*
+  Assumed and implied equalities are collected in a proof forest for being able to
+  produce explanations. For each equivalence class there is one proof tree. The
+  equality certificates are oriented towards a root term, that is not necessarily
+  the representative of the equivalence class.
+*)
+
+(*
+  Whenever two equivalence classes are merged due to an equality t1 = t2, the shorter
+  of the two paths, either from t1 to its root or t2 to its root, is re-oriented such
+  that the relevant ti becomes the new root of its tree. Then, a new edge between ti
+  and the other term of the equality t1 = t2 is added to connect the two proof trees.
+*)
+
+fun depth_of trace t =
+  (case Argo_Termtab.lookup trace t of
+    NONE => 0
+  | SOME (t', _) => 1 + depth_of trace t')
+
+fun reorient t trace =
+  (case Argo_Termtab.lookup trace t of
+    NONE => trace
+  | SOME (t', eq) => Argo_Termtab.update (t', (t, symm eq)) (reorient t' trace))
+
+fun new_edge from to eq trace = Argo_Termtab.update (from, (to, eq)) (reorient from trace)
+
+fun with_shortest f (t1, t2) eq trace =
+  (if depth_of trace t1 <= depth_of trace t2 then f t1 t2 eq else f t2 t1 (symm eq)) trace
+
+fun add_edge eq trace = with_shortest new_edge (dest_eq eq) eq trace
+
+(*
+  To produce an explanation that t1 and t2 are equal, the paths to their root are
+  extracted from the proof forest. Common ancestors in both paths are dropped.
+*)
+
+fun path_to_root trace path t =
+  (case Argo_Termtab.lookup trace t of
+    NONE => (t, path)
+  | SOME (t', _) => path_to_root trace (t :: path) t')
+
+fun drop_common root (t1 :: path1) (t2 :: path2) =
+      if Argo_Term.eq_term (t1, t2) then drop_common t1 path1 path2 else root
+  | drop_common root _ _ = root
+
+fun common_ancestor trace t1 t2 =
+  let val ((root, path1), (_, path2)) = apply2 (path_to_root trace []) (t1, t2)
+  in drop_common root path1 path2 end
+
+(*
+  The proof of an assumed literal is typically a hypothesis. If the assumed literal is
+  already known to be a unit literal, then there is already a proof for it.
+*)
+
+fun proof_of (lit, NONE) lits prf =
+      (insert Argo_Lit.eq_lit (Argo_Lit.negate lit) lits, Argo_Proof.mk_hyp lit prf)
+  | proof_of (_, SOME p) lits prf = (lits, (p, prf))
+
+(*
+  The explanation of equality between two terms t1 and t2 is computed based on the
+  paths from t1 and t2 to their common ancestor t in the proof forest. For each of
+  the two paths, a transitive proof of equality t1 = t and t = t2 is constructed,
+  such that t1 = t2 follows by transitivity.
+  
+  Each edge of the paths denotes an assumed or implied equality. Implied equalities
+  might be due to congruences (f a = g b) for which the equalities f = g and a = b
+  need to be explained recursively.
+*)
+
+fun mk_eq_proof trace t1 t2 lits prf =
+  if Argo_Term.eq_term (t1, t2) then (lits, Argo_Proof.mk_refl t1 prf)
+  else
+    let
+      val root = common_ancestor trace t1 t2
+      val (lits, (p1, prf)) = trans_proof I I trace t1 root lits prf
+      val (lits, (p2, prf)) = trans_proof swap symm trace t2 root lits prf
+    in (lits, Argo_Proof.mk_trans p1 p2 prf) end
+
+and trans_proof sw sy trace t root lits prf =
+  if Argo_Term.eq_term (t, root) then (lits, Argo_Proof.mk_refl t prf)
+  else
+    (case Argo_Termtab.lookup trace t of
+      NONE => raise Fail "bad trace"
+    | SOME (t', eq) => 
+        let
+          val (lits, (p1, prf)) = proof_step trace (sy eq) lits prf
+          val (lits, (p2, prf)) = trans_proof sw sy trace t' root lits prf
+        in (lits, uncurry Argo_Proof.mk_trans (sw (p1, p2)) prf) end)
+
+and proof_step _ (Flat (cert, _)) lits prf = proof_of cert lits prf
+  | proof_step trace (Cong tp) lits prf =
+      let
+        val ((t1, t2), (u1, u2)) = apply2 dest_app tp
+        val (lits, (p1, prf)) = mk_eq_proof trace t1 u1 lits prf
+        val (lits, (p2, prf)) = mk_eq_proof trace t2 u2 lits prf
+      in (lits, Argo_Proof.mk_cong p1 p2 prf) end
+  | proof_step trace (Symm eq) lits prf =
+      proof_step trace eq lits prf ||> uncurry Argo_Proof.mk_symm
+
+(*
+  All clauses produced by a theory solver are expected to be a lemma.
+  The lemma proof must hence be the last proof step.
+*)
+
+fun close_proof lit lits (p, prf) = (lit :: lits, Argo_Proof.mk_lemma [lit] p prf)
+
+(*
+  The explanation for the equality of t1 and t2 used the above algorithm.
+*)
+
+fun explain_eq lit t1 t2 ({repr, rdata, apps, trace, prf, back}: context) =
+  let val (lits, (p, prf)) = mk_eq_proof trace t1 t2 [] prf |-> close_proof lit
+  in ((lits, p), mk_context repr rdata apps trace prf back) end
+
+(*
+  The explanation that t1 and t2 are distinct uses the negated equality u1 ~= u2 that
+  explains why the equivalence class containing t1 and u1 and the equivalence class
+  containing t2 and u2 are disjoint. The explanations for t1 = u1 and u2 = t2 are
+  constructed using the above algorithm. By transitivity, it follows that t1 ~= t2.  
+*)
+
+fun finish_proof (Flat ((lit, _), _)) lits p prf = close_proof lit lits (p, prf)
+  | finish_proof (Cong _) _ _ _ = raise Fail "bad equality"
+  | finish_proof (Symm eq) lits p prf = Argo_Proof.mk_symm p prf |-> finish_proof eq lits
+
+fun explain_neq eq eq' ({repr, rdata, apps, trace, prf, back}: context) =
+  let
+    val (t1, t2) = dest_eq eq
+    val (u1, u2) = dest_eq eq'
+
+    val (lits, (p, prf)) = proof_step trace eq' [] prf
+    val (lits, (p1, prf)) = mk_eq_proof trace t1 u1 lits prf
+    val (lits, (p2, prf)) = mk_eq_proof trace u2 t2 lits prf
+    val (lits, (p, prf)) = 
+      Argo_Proof.mk_trans p p2 prf |-> Argo_Proof.mk_trans p1 |-> finish_proof eq lits
+  in ((lits, p), mk_context repr rdata apps trace prf back) end
+
+
+(* propagating new equalities *)
+
+exception CONFLICT of Argo_Cls.clause * context
+
+(*
+  comment missing
+*)
+
+fun same_repr repr r (t, _) = Argo_Term.eq_term (r, repr_of repr t)
+
+fun has_atom rdata r eq =
+  (case #atoms (ritem_of rdata r) of
+    Eqs eqs => member (Argo_Term.eq_term o snd) eqs eq
+  | _ => false)
+
+fun add_implied mk_lit repr rdata r neqs (atom as (t, eq)) (eqs, ls) =
+  let val r' = repr_of repr t
+  in
+    if Argo_Term.eq_term (r, r') then (eqs, insert Argo_Lit.eq_lit (mk_lit eq) ls)
+    else if exists (same_repr repr r') neqs andalso has_atom rdata r' eq then
+      (eqs, Argo_Lit.Neg eq :: ls)
+    else (atom :: eqs, ls)
+  end
+
+(*
+  comment missing
+*)
+
+fun copy_occ repr app (eqs, occs, apps) =
+  let val rp = apply2 (repr_of repr) (dest_app app)
+  in
+    (case lookup_app apps rp of
+      SOME app' => (Cong (app, app') :: eqs, occs, apps)
+    | NONE => (eqs, app :: occs, put_app rp app apps))
+  end
+
+(*
+  comment missing
+*)
+
+fun add_lits (Argo_Lit.Pos _, _) = fold (cons o Argo_Lit.Pos)
+  | add_lits (Argo_Lit.Neg _, _) = fold (cons o Argo_Lit.Neg)
+
+fun join_atoms f (Eqs eqs1) (Eqs eqs2) ls = f eqs1 eqs2 ls
+  | join_atoms _ (Preds ts1) (Preds ts2) ls = (Preds (union Argo_Term.eq_term ts1 ts2), ls)
+  | join_atoms _ (Preds ts) (Cert lp) ls = (Cert lp, add_lits lp ts ls)
+  | join_atoms _ (Cert lp) (Preds ts) ls = (Cert lp, add_lits lp ts ls)
+  | join_atoms _ (Cert lp) (Cert _) ls = (Cert lp, ls)
+  | join_atoms _ _ _ _ = raise Fail "bad atoms"
+
+(*
+  comment missing
+*)
+
+fun join r1 ri1 r2 ri2 eq (eqs, ls, {repr, rdata, apps, trace, prf, back}: context) =
+  let
+    val {size=size1, class=class1, occs=occs1, neqs=neqs1, atoms=atoms1}: ritem = ri1
+    val {size=size2, class=class2, occs=occs2, neqs=neqs2, atoms=atoms2}: ritem = ri2
+
+    val repr = fold (fn t => put_repr t r1) class2 repr
+    val class = fold cons class2 class1
+    val (eqs, occs, apps) = fold (copy_occ repr) occs2 (eqs, occs1, apps)
+    val trace = add_edge eq trace
+    val neqs = AList.merge Argo_Term.eq_term (K true) (neqs1, neqs2)
+    fun add r neqs = fold (add_implied Argo_Lit.Pos repr rdata r neqs)
+    fun adds eqs1 eqs2 ls = ([], ls) |> add r2 neqs2 eqs1 |> add r1 neqs1 eqs2 |>> Eqs
+    val (atoms, ls) = join_atoms adds atoms1 atoms2 ls
+    (* TODO: make sure that all implied literals are propagated *)
+    val rdata = put_ritem r1 (mk_ritem (size1 + size2) class occs neqs atoms) rdata
+  in (eqs, ls, mk_context repr rdata apps trace prf back) end
+
+(*
+  comment missing
+*)
+
+fun find_neq ({repr, ...}: context) ({neqs, ...}: ritem) r = find_first (same_repr repr r) neqs
+
+fun check_join (r1, r2) (ri1, ri2) eq (ecx as (_, _, cx)) =
+  (case find_neq cx ri2 r1 of
+    SOME (_, eq') => raise CONFLICT (explain_neq (negate (symm eq)) eq' cx)
+  | NONE =>
+      (case find_neq cx ri1 r2 of
+        SOME (_, eq') => raise CONFLICT (explain_neq (negate eq) eq' cx)
+      | NONE => join r1 ri1 r2 ri2 eq ecx))
+
+(*
+  comment missing
+*)
+
+fun with_max_class f (rp as (r1, r2)) (rip as (ri1: ritem, ri2: ritem)) eq =
+  if #size ri1 >= #size ri2 then f rp rip eq else f (r2, r1) (ri2, ri1) (symm eq)
+
+(*
+  comment missing
+*)
+
+fun propagate ([], ls, cx) = (rev ls, cx)
+  | propagate (eq :: eqs, ls, cx) =
+      let val rp = apply2 (repr_of' cx) (dest_eq eq)
+      in 
+        if Argo_Term.eq_term rp then propagate (eqs, ls, cx)
+        else propagate (with_max_class check_join rp (apply2 (ritem_of' cx) rp) eq (eqs, ls, cx))
+      end
+
+fun without lit (lits, cx) = (Argo_Common.Implied (remove Argo_Lit.eq_lit lit lits), cx)
+
+fun flat_merge (lp as (lit, _)) eq cx = without lit (propagate ([Flat (lp, eq)], [], cx))
+  handle CONFLICT (cls, cx) => (Argo_Common.Conflict cls, cx)
+
+(*
+  comment missing
+*)
+
+fun app_merge app tp (cx as {repr, rdata, apps, trace, prf, back}: context) =
+  let val rp as (r1, r2) = apply2 (repr_of repr) tp
+  in
+    (case lookup_app apps rp of
+      SOME app' =>
+        (case propagate ([Cong (app, app')], [], cx) of
+          ([], cx) => cx
+        | _ => raise Fail "bad application merge")
+    | NONE =>
+        let val rdata = add_occ r1 app (add_occ r2 app rdata)
+        in mk_context repr rdata (put_app rp app apps) trace prf back end)
+  end
+
+(*
+  A negated equality between t1 and t2 is only recorded if t1 and t2 are not already known
+  to belong to the same class. In that case, a conflict is raised with an explanation
+  why t1 and t2 are equal. Otherwise, the classes of t1 and t2 are marked as disjoint by
+  storing the negated equality in the ritems of t1's and t2's representative. All equalities
+  between terms of t1's and t2's class are implied as negated equalities. Those equalities
+  are found in the ritems of t1's and t2's representative.
+*)
+
+fun note_neq eq (r1, r2) (t1, t2) ({repr, rdata, apps, trace, prf, back}: context) =
+  let
+    val {size=size1, class=class1, occs=occs1, neqs=neqs1, atoms=atoms1}: ritem = ritem_of rdata r1
+    val {size=size2, class=class2, occs=occs2, neqs=neqs2, atoms=atoms2}: ritem = ritem_of rdata r2
+
+    fun add r (Eqs eqs) ls = fold (add_implied Argo_Lit.Neg repr rdata r []) eqs ([], ls) |>> Eqs
+      | add _ _ _ = raise Fail "bad negated equality between predicates"
+    val ((atoms1, atoms2), ls) = [] |> add r2 atoms1 ||>> add r1 atoms2
+    val ri1 = mk_ritem size1 class1 occs1 ((t2, eq) :: neqs1) atoms1
+    val ri2 = mk_ritem size2 class2 occs2 ((t1, symm eq) :: neqs2) atoms2
+  in (ls, mk_context repr (put_ritem r1 ri1 (put_ritem r2 ri2 rdata)) apps trace prf back) end
+
+fun flat_neq (lp as (lit, _)) (tp as (t1, t2)) cx =
+  let val rp = apply2 (repr_of' cx) tp
+  in
+    if Argo_Term.eq_term rp then
+      let val (cls, cx) = explain_eq (Argo_Lit.negate lit) t1 t2 cx
+      in (Argo_Common.Conflict cls, cx) end
+    else without lit (note_neq (Flat (lp, tp)) rp tp cx)
+  end
+
+
+(* simplification *)
+
+(*
+  Only equalities are subject to normalizations. An equality between two expressions e1 and e2
+  is normalized, if e1 is less than e2 based on the expression ordering. If e1 and e2 are
+  syntactically equal, the equality between these two expressions is normalized to the true
+  expression.
+*)
+
+fun norm_eq env =
+  let val e1 = Argo_Rewr.get env 1 and e2 = Argo_Rewr.get env 2
+  in
+    (case Argo_Expr.expr_ord (e1, e2) of
+      EQUAL => SOME (Argo_Proof.Rewr_Eq_Refl, Argo_Rewr.E Argo_Expr.true_expr)
+    | LESS => NONE
+    | GREATER => SOME (Argo_Proof.Rewr_Eq_Symm, Argo_Rewr.E (Argo_Expr.mk_eq e2 e1)))
+  end
+
+val simplify = Argo_Rewr.func "(eq (? 1) (? 2))" norm_eq
+
+
+(* declaring atoms *)
+
+(*
+  Only a genuinely new equality term t for the equality "t1 = t2" is added. If t1 and t2 belong
+  to the same equality class or if the classes of t1 and t2 are known to be disjoint, the
+  respective literal is returned together with an unmodified context.
+*)
+
+fun add_eq_term t t1 t2 (rp as (r1, r2)) (cx as {repr, rdata, apps, trace, prf, back}: context) =
+  if Argo_Term.eq_term rp then (SOME (Argo_Lit.Pos t), cx)
+  else if is_some (find_neq cx (ritem_of rdata r1) r2) then (SOME (Argo_Lit.Neg t), cx)
+  else
+    let val rdata = add_eq_atom r1 (t2, t) (add_eq_atom r2 (t1, t) rdata)
+    in (NONE, mk_context repr rdata apps trace prf back) end
+
+(*
+  Only a genuinely new predicate t, which is an application "t1 t2", is added.
+  If there is a predicate that is known to be congruent to the representatives of t1 and t2,
+  and that predicate or its negation has already been assummed, the respective literal of t
+  is returned together with an unmodified context.
+*)
+
+fun add_pred_term t rp (cx as {repr, rdata, apps, trace, prf, back}: context) =
+  (case lookup_app apps rp of
+    NONE => (NONE, mk_context repr (put_ritem t (as_pred_ritem t) rdata) apps trace prf back)
+  | SOME app =>
+      (case `(ritem_of_pred rdata) (repr_of repr app) of
+        ({atoms=Cert (Argo_Lit.Pos _, _), ...}: ritem, _) => (SOME (Argo_Lit.Pos t), cx)
+      | ({atoms=Cert (Argo_Lit.Neg _, _), ...}: ritem, _) => (SOME (Argo_Lit.Neg t), cx)
+      | (ri as {atoms=Preds ts, ...}: ritem, r) =>
+          let val rdata = put_ritem r (put_atoms (Preds (t :: ts)) ri) rdata
+          in (NONE, mk_context repr rdata apps trace prf back) end
+      | ({atoms=Eqs _, ...}: ritem, _) => raise Fail "bad predicate"))
+
+(*
+  For each term t that is an application "t1 t2", the reflexive equality t = t1 t2 is added
+  to the context. This is required for propagations of congruences.
+*)
+
+fun flatten (t as Argo_Term.T (_, Argo_Expr.App, [t1, t2])) cx =
+      flatten t1 (flatten t2 (app_merge t (t1, t2) cx))
+  | flatten _ cx = cx
+
+(*
+  Atoms to be added to the context must either be an equality "t1 = t2" or
+  an application "t1 t2" (a predicate). Besides adding the equality or the application,
+  reflexive equalities for for all applications in the terms t1 and t2 are added.
+*)
+
+fun add_atom (t as Argo_Term.T (_, Argo_Expr.Eq, [t1, t2])) cx =
+      add_eq_term t t1 t2 (apply2 (repr_of' cx) (t1, t2)) (flatten t1 (flatten t2 cx))
+  | add_atom (t as Argo_Term.T (_, Argo_Expr.App, [t1, t2])) cx =
+      let val cx = flatten t1 (flatten t2 (app_merge t (t1, t2) cx))
+      in add_pred_term t (apply2 (repr_of' cx) (t1, t2)) cx end
+  | add_atom _ cx = (NONE, cx)
+
+
+(* assuming external knowledge *)
+
+(*
+  Assuming a predicate r replaces all predicate atoms of r's ritem with the assumed certificate.
+  The predicate atoms are implied, either with positive or with negative polarity based on
+  the assumption.
+
+  There must not be a certificate for r since otherwise r would have been assumed before already.
+*)
+
+fun assume_pred lit mk_lit cert r ({repr, rdata, apps, trace, prf, back}: context) =
+  (case ritem_of_pred rdata r of
+    {size, class, occs, neqs, atoms=Preds ts}: ritem =>
+      let val rdata = put_ritem r (mk_ritem size class occs neqs cert) rdata
+      in without lit (map mk_lit ts, mk_context repr rdata apps trace prf back) end
+  | _ => raise Fail "bad predicate assumption")
+
+(*
+  Assumed equalities "t1 = t2" are treated as flat equalities between terms t1 and t2.
+  If t1 and t2 are applications, congruences are propagated as part of the merge between t1 and t2.
+  Negated equalities are handled likewise.
+
+  Assumed predicates do not trigger congruences. Only predicates of the same class are implied.
+*)
+
+fun assume (lp as (Argo_Lit.Pos (Argo_Term.T (_, Argo_Expr.Eq, [t1, t2])), _)) cx =
+      flat_merge lp (t1, t2) cx
+  | assume (lp as (Argo_Lit.Neg (Argo_Term.T (_, Argo_Expr.Eq, [t1, t2])), _)) cx =
+      flat_neq lp (t1, t2) cx
+  | assume (lp as (lit as Argo_Lit.Pos (t as Argo_Term.T (_, Argo_Expr.App, [_, _])), _)) cx =
+      assume_pred lit Argo_Lit.Pos (Cert lp) (repr_of' cx t) cx
+  | assume (lp as (lit as Argo_Lit.Neg (t as Argo_Term.T (_, Argo_Expr.App, [_, _])), _)) cx =
+      assume_pred lit Argo_Lit.Neg (Cert lp) (repr_of' cx t) cx
+  | assume _ cx = (Argo_Common.Implied [], cx)
+
+
+(* checking for consistency and pending implications *)
+
+(*
+  The internal model is always kept consistent. All implications are propagated as soon as
+  new information is assumed. Hence, there is nothing to be done here.
+*)
+
+fun check cx = (Argo_Common.Implied [], cx)
+
+
+(* explanations *)
+
+(*
+  The explanation for the predicate t, which is an application of t1 and t2, is constructed
+  from the explanation of the predicate application "u1 u2" as well as the equalities "u1 = t1"
+  and "u2 = t2" which both are constructed from the proof forest. The substitution rule is
+  the proof step that concludes "t1 t2" from "u1 u2" and the two equalities "u1 = t1"
+  and "u2 = t2".
+
+  The atoms part of the ritem of t's representative must be a certificate of an already
+  assumed predicate for otherwise there would be no explanation for t.
+*)
+
+fun explain_pred lit t t1 t2 ({repr, rdata, apps, trace, prf, back}: context) =
+  (case ritem_of_pred rdata (repr_of repr t) of
+    {atoms=Cert (cert as (lit', _)), ...}: ritem =>
+      let
+        val (u1, u2) = dest_app (Argo_Lit.term_of lit')
+        val (lits, (p, prf)) = proof_of cert [] prf
+        val (lits, (p1, prf)) = mk_eq_proof trace u1 t1 lits prf
+        val (lits, (p2, prf)) = mk_eq_proof trace u2 t2 lits prf
+        val (lits, (p, prf)) = Argo_Proof.mk_subst p p1 p2 prf |> close_proof lit lits
+      in ((lits, p), mk_context repr rdata apps trace prf back) end
+  | _ => raise Fail "no explanation for bad predicate")
+
+(*
+  Explanations are produced based on the proof forest that is constructed while assuming new
+  information and propagating this among the internal data structures.
+  
+  For predicates, no distinction between both polarities needs to be done here. The atoms
+  part of the relevant ritem knows the assumed polarity.
+*)
+
+fun explain (lit as Argo_Lit.Pos (Argo_Term.T (_, Argo_Expr.Eq, [t1, t2]))) cx =
+      SOME (explain_eq lit t1 t2 cx)
+  | explain (lit as Argo_Lit.Neg (Argo_Term.T (_, Argo_Expr.Eq, [t1, t2]))) cx =
+      let val (_, eq) = the (find_neq cx (ritem_of' cx (repr_of' cx t1)) (repr_of' cx t2))
+      in SOME (explain_neq (Flat ((lit, NONE), (t1, t2))) eq cx) end
+  | explain (lit as (Argo_Lit.Pos (t as Argo_Term.T (_, Argo_Expr.App, [t1, t2])))) cx =
+      SOME (explain_pred lit t t1 t2 cx)
+  | explain (lit as (Argo_Lit.Neg (t as Argo_Term.T (_, Argo_Expr.App, [t1, t2])))) cx =
+      SOME (explain_pred lit t t1 t2 cx)
+  | explain _ _ = NONE
+
+
+(* backtracking *)
+
+(*
+  All information that needs to be reconstructed on backtracking is stored on the backtracking
+  stack. On backtracking any current information is replaced by what was stored before. No copying
+  nor subtle updates are required thanks to immutable data structures.
+*)
+
+fun add_level ({repr, rdata, apps, trace, prf, back}: context) =
+  mk_context repr rdata apps trace prf ((repr, rdata, apps, trace) :: back)
+
+fun backtrack ({back=[], ...}: context) = raise Empty
+  | backtrack ({prf, back=(repr, rdata, apps, trace) :: back, ...}: context) =
+      mk_context repr rdata apps trace prf back
+
+end