let rec process fct (s, p) =
  Is.initialize fct s p;        (* 1. store initial configuration into global variables. *)
  eval ();                      (* 2. run rule interpreter. *)  
  assert(G.is_empty !Infsys.g); (* 3. restore final configuration from global variables. *)
  Is.finalize () 

and eval () =
  if G.is_empty !Infsys.g then
    Is.normalize ()
  else
    begin
      eval1 ();
      eval ()
    end

and eval1 () =
  try
    let ((atm, rho) as fct) = G.get !Infsys.g in
      (match Atom.atom_of atm with
         | Atom.TT ->
             ()
         | Atom.FF ->
             raise(Jst.Inconsistent(rho))
         | Atom.Equal(a, b) ->
             let e = Fact.Equal.make a b rho in
               (match Fact.Equal.status e with
                  | Term.Variable -> merge_v e
                  | Term.Pure(i) ->  merge_i i e 
                  | Term.Mixed(i, a) -> abstract fct i a)
         | Atom.Diseq(a, b) ->
             let d = Fact.Diseq.make a b rho in
               (match Fact.Diseq.status d with
                  | Term.Variable -> dismerge_v d
                  | Term.Pure(i) -> dismerge_i i d
                  | Term.Mixed(i, a) -> abstract fct i a)
         | Atom.Nonneg(a) ->
             let nn = Fact.Nonneg.make a rho in
               (match Fact.Nonneg.status nn with
                 | Term.Variable -> nonneg_la nn
                 | Term.Pure(i) when i = Th.la -> nonneg_la nn
                 | Term.Pure(i)  -> abstract fct i (Fact.Nonneg.term_of nn)
                 | Term.Mixed(i, a) -> abstract fct i a)
         | Atom.Pos(a) ->
             let pp = Fact.Pos.make a rho in
               (match Fact.Pos.status pp with
                 | Term.Variable -> pos_la pp
                 | Term.Pure(i) when i = Th.la -> pos_la pp
                 | Term.Pure(i) -> abstract fct i (Fact.Pos.term_of pp)
                 | Term.Mixed(i, a) -> abstract fct i a))
  with
      Not_found -> ()

            
and merge_v e =
  assert(Fact.Equal.is_var e);
  Partition.merge !Infsys.p e;
  propagate ()

and merge_i i e = 
  assert(Fact.Equal.is_pure i e);
  Is.merge i e;
  propagate ()
    
and abstract fct i a =
  G.put fct !Infsys.g; 
  Is.abstract i a;
  propagate ()
    
        


(** Propagate all fresh variable equalities and disequalities in partitioning p to individual procedures. *)


and propagate () =
  try
    let e = Partition.fresh_equal !Infsys.p in
      Is.propagate e;
      propagate ()
  with
      Not_found -> 
        (try
           let d = Partition.fresh_diseq !Infsys.p in
             Is.propagate_diseq d;
             propagate ()
         with
             Not_found -> ())
        
and dismerge_v d =
  assert(Fact.Diseq.is_var d);
  Partition.dismerge !Infsys.p d;
  propagate ()

and dismerge_i i d = 
  assert(Fact.Diseq.is_pure i d);
  Is.dismerge i d;
  propagate ()

and nonneg_la nn = 
  assert(Fact.Nonneg.is_pure Th.la nn);
  Is.nonneg nn;
  propagate ()

and pos_la pp = 
  assert(Fact.Pos.is_pure Th.la pp);
  Is.pos pp;
  propagate ()




(** Two terms a, b are disequal in (e, p) if asserting a = b yields a contradiction. This also takes into account all implicit disequalites. *)


and is_diseq_complete ((s, p) as cfg) a b =
  let d = (Atom.mk_diseq (a, b), Jst.dep0) in
    try
      let _ = process d cfg in
        None
    with
        Jst.Inconsistent(rho) -> Some(rho)