let model s xs =
  let rec mod_star rho = function
    | [] -> rho
    | x :: xs -> mod_star (mod1 x rho) xs

  and (|||) m1 m2 x rho =
    try m1 x rho with Not_found -> m2 x rho

  and mod1 x rho =
    if Term.Map.mem x rho then rho else
      (mod_la ||| mod_u) x rho

  and mod_la x rho =
    try 
      let a = interp Th.la s x in
      let rho' = Set.fold mod_la (Term.vars_of a) rho in
        Term.Map.add x (Arith.apply a rho') rho'
    with
        Not_found ->
          let a = 
            (try
               match c s x with
                 | Sign.Pos -> Arith.mk_one
                 | Sign.Neg -> Arith.mk_num (Q.negone)
                 | _ -> Arith.mk_zero
               with
                   Not_found -> Arith.mk_zero)
          in
            Term.Map.add x a rho
          
  and mod_u x rho =
    let u = interp Th.u s x in
    let rho' = Set.fold mod_u (Term.vars_of u) rho in
      Term.Map.add x (Term.apply rho' u) rho'

  in
  let restrict xs m =
    Term.Map.fold
      (fun x a m ->
         if List.exists (Term.eq x) xs then m 
         else Term.Map.remove x m)
      m m
  in
  let m = mod_star Term.Map.empty xs in
    restrict xs m