matita/components/ng_paramodulation/paramod.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
  13
  14 let print s = prerr_endline (Lazy.force s) ;;
  15 let noprint s = ();;
  16 let debug = noprint;;
  17
  18 let monster = 100;;
  19
  20 module type Paramod =
  21   sig
  22     type t
  23     type input
  24     type szsontology =
  25       | Unsatisfiable of
  26           (t Terms.bag * int * t Terms.substitution * int list) list
  27       | GaveUp
  28       | Error of string
  29       | Timeout of int * t Terms.bag
  30     type bag = t Terms.bag * int
  31     type state
  32     val empty_state : state
  33     val bag_of_state : state -> bag
  34     val replace_bag: state -> bag -> state
  35     val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
  36     val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
  37     val forward_infer_step :
  38       state ->
  39       t Terms.unit_clause ->
  40       int ->
  41       state
  42     val goal_narrowing :
  43       int
  44       -> int
  45       -> float option
  46       -> state
  47       -> state
  48     val paramod :
  49       useage:bool ->
  50       max_steps:int ->
  51       ?timeout:float ->
  52       bag ->
  53       g_passives:t Terms.unit_clause list ->
  54       passives:t Terms.unit_clause list -> szsontology
  55     val demod :
  56       state -> input* input -> szsontology
  57     val fast_eq_check :
  58       state -> input* input -> szsontology
  59     val nparamod :
  60       useage:bool ->
  61       max_steps:int ->
  62       ?timeout:float ->
  63       state -> input* input -> szsontology
  64   end
  65
  66 module Paramod (B : Orderings.Blob) = struct
  67   module Pp = Pp.Pp (B)
  68   module FU = FoUnif.Founif(B)
  69   module IDX = Index.Index(B)
  70   module Sup = Superposition.Superposition(B)
  71   module Utils = FoUtils.Utils(B)
  72   module Order = B
  73   module WeightOrderedPassives =
  74       struct
  75         type t = B.t Terms.passive_clause
  76         let compare = Utils.compare_passive_clauses_weight
  77       end
  78
  79   module AgeOrderedPassives =
  80       struct
  81         type t = B.t Terms.passive_clause
  82         let compare = Utils.compare_passive_clauses_age
  83       end
  84
  85   module WeightPassiveSet = Set.Make(WeightOrderedPassives)
  86   module AgePassiveSet = Set.Make(AgeOrderedPassives)
  87
  88   type t = B.t
  89   type input = B.input
  90   type bag = B.t Terms.bag * int
  91   type szsontology =
  92     | Unsatisfiable of
  93         (B.t Terms.bag * int * B.t Terms.substitution * int list) list
  94     | GaveUp
  95     | Error of string
  96     | Timeout of int * B.t Terms.bag
  97   exception Stop of szsontology
  98   type state =
  99       t Terms.bag
 100       * int
 101       * Index.Index(B).active_set
 102       * (IDX.DT.t * WeightPassiveSet.t * AgePassiveSet.t)
 103       * B.t Terms.unit_clause list
 104       * (WeightPassiveSet.t * AgePassiveSet.t)
 105
 106   let empty_state =
 107     Terms.empty_bag,
 108     0,
 109     ([],IDX.DT.empty),
 110     (IDX.DT.empty,WeightPassiveSet.empty,AgePassiveSet.empty),
 111     [],
 112     (WeightPassiveSet.empty,AgePassiveSet.empty)
 113   ;;
 114
 115   let bag_of_state (bag,n,_,_,_,_) = bag,n
 116   ;;
 117
 118   let replace_bag (_,_,a,b,c,d) (bag,n) = bag,n,a,b,c,d
 119   ;;
 120
 121   let add_passive_clause ?(no_weight=false)
 122       (passive_t,passives_w,passives_a) cl =
 123     let pcl = if no_weight then (0,cl)
 124     else Utils.mk_passive_clause cl in
 125     IDX.index_unit_clause passive_t cl,
 126     WeightPassiveSet.add pcl passives_w,
 127     AgePassiveSet.add pcl passives_a
 128   ;;
 129
 130   let add_passive_goal ?(no_weight=false) (passives_w,passives_a) g =
 131     let g = if no_weight then (0,g)
 132     else Utils.mk_passive_goal g in
 133     WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a
 134   ;;
 135
 136   let remove_passive_clause (passive_t,passives_w,passives_a) cl =
 137     let passive_t = IDX.remove_unit_clause passive_t (snd cl) in
 138     let passives_w = WeightPassiveSet.remove cl passives_w in
 139     let passives_a = AgePassiveSet.remove cl passives_a in
 140       passive_t,passives_w,passives_a
 141   ;;
 142
 143   let add_passive_clauses ?(no_weight=false) =
 144     List.fold_left (add_passive_clause ~no_weight)
 145   ;;
 146
 147   let add_passive_goals ?(no_weight=false)
 148       (passives_w,passives_a) new_clauses =
 149     let new_clauses_w,new_clauses_a =
 150       List.fold_left (add_passive_goal ~no_weight)
 151       (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses
 152     in
 153       (WeightPassiveSet.union new_clauses_w passives_w,
 154        AgePassiveSet.union new_clauses_a passives_a)
 155   ;;
 156
 157   let remove_passive_goal (passives_w,passives_a) cl =
 158     let passives_w = WeightPassiveSet.remove cl passives_w in
 159     let passives_a = AgePassiveSet.remove cl passives_a in
 160       passives_w,passives_a
 161   ;;
 162
 163   let is_passive_set_empty (_,passives_w,passives_a) =
 164     if (WeightPassiveSet.is_empty passives_w) then begin
 165       assert (AgePassiveSet.is_empty passives_a); true
 166     end else begin
 167       assert (not (AgePassiveSet.is_empty passives_a)); false
 168     end
 169   ;;
 170
 171   let is_passive_g_set_empty (passives_w,passives_a) =
 172     if (WeightPassiveSet.is_empty passives_w) then begin
 173       assert (AgePassiveSet.is_empty passives_a); true
 174     end else begin
 175       assert (not (AgePassiveSet.is_empty passives_a)); false
 176     end
 177   ;;
 178
 179   let passive_set_cardinal (_,passives_w,_)
 180       = WeightPassiveSet.cardinal passives_w
 181   ;;
 182
 183   let g_passive_set_cardinal (passives_w,_)
 184       = WeightPassiveSet.cardinal passives_w
 185   ;;
 186
 187   let passive_empty_set =
 188     (IDX.DT.empty,WeightPassiveSet.empty,AgePassiveSet.empty)
 189   ;;
 190
 191   let g_passive_empty_set =
 192     (WeightPassiveSet.empty,AgePassiveSet.empty)
 193   ;;
 194
 195   let pick_min_passive ~use_age (_,passives_w,passives_a) =
 196     if use_age then AgePassiveSet.min_elt passives_a
 197     else WeightPassiveSet.min_elt passives_w
 198   ;;
 199
 200   let pick_min_g_passive ~use_age (passives_w,passives_a) =
 201     if use_age then AgePassiveSet.min_elt passives_a
 202     else WeightPassiveSet.min_elt passives_w
 203   ;;
 204
 205   let mk_unit_clause bag maxvar (t,ty) =
 206     let c, maxvar = Utils.mk_unit_clause maxvar (B.embed ty) (B.embed t) in
 207     let bag, c = Terms.add_to_bag c bag in
 208     (bag, maxvar), c
 209   ;;
 210
 211   let mk_clause bag maxvar (t,ty) =
 212     let (proof,ty) = B.saturate t ty in
 213     let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
 214     let bag, c = Terms.add_to_bag c bag in
 215     (bag, maxvar), c
 216   ;;
 217
 218   let mk_passive (bag,maxvar) = mk_clause bag maxvar;;
 219
 220   let mk_goal (bag,maxvar) = mk_clause bag maxvar;;
 221
 222   let initialize_goal (bag,maxvar,actives,passives,_,_) t =
 223     let (bag,maxvar), g = mk_unit_clause bag maxvar t in
 224     let g_passives = g_passive_empty_set in
 225     (* if the goal is not an equation we returns an empty
 226        passive set *)
 227     let g_passives =
 228       if Terms.is_eq_clause g then add_passive_goal g_passives g
 229       else g_passives
 230     in
 231       (bag,maxvar,actives,passives,[],g_passives)
 232
 233
 234   (* TODO : global age over facts and goals (without comparing weights) *)
 235   let select ~use_age passives g_passives =
 236     if is_passive_set_empty passives then begin
 237       if (is_passive_g_set_empty g_passives) then
 238         raise (Stop GaveUp) (* we say we are incomplete *)
 239       else
 240        let g_cl = pick_min_g_passive ~use_age:use_age g_passives in
 241         (true,g_cl,passives,remove_passive_goal g_passives g_cl)
 242     end
 243     else let cl = pick_min_passive ~use_age:use_age passives in
 244       if is_passive_g_set_empty g_passives then
 245         (false,cl,remove_passive_clause passives cl,g_passives)
 246       else
 247         let g_cl = pick_min_g_passive ~use_age:use_age g_passives in
 248         let (id1,_,_,_),(id2,_,_,_) = snd cl, snd g_cl in
 249         let cmp = if use_age then id1 <= id2
 250         else fst cl <= fst g_cl
 251         in
 252           if cmp then
 253             (false,cl,remove_passive_clause passives cl,g_passives)
 254           else
 255             (true,g_cl,passives,remove_passive_goal g_passives g_cl)
 256   ;;
 257
 258   let backward_infer_step bag maxvar actives passives
 259                           g_actives g_passives g_current iterno =
 260     (* superposition left, simplifications on goals *)
 261       debug (lazy "infer_left step...");
 262       let bag, maxvar, new_goals =
 263         Sup.infer_left bag maxvar g_current actives
 264       in
 265         debug (lazy "Performed infer_left step");
 266         let bag = Terms.replace_in_bag (g_current,false,iterno) bag in
 267           bag, maxvar, actives, passives, g_current::g_actives,
 268     (add_passive_goals g_passives new_goals)
 269   ;;
 270
 271   let pp_clauses actives passives =
 272     let actives_l, _ = actives in
 273     let passive_t,_,_ = passives in
 274     let wset = IDX.elems passive_t in
 275       ("Actives :" ^ (String.concat ";\n"
 276         (List.map Pp.pp_unit_clause actives_l)))
 277       ^
 278       ("Passives:" ^(String.concat ";\n"
 279         (List.map (fun (_,cl) -> Pp.pp_unit_clause cl)
 280                (IDX.ClauseSet.elements wset))))
 281   ;;
 282
 283   let forward_infer_step
 284       ((bag,maxvar,actives,passives,g_actives,g_passives) as s)
 285       current iterno =
 286     (* forward step *)
 287
 288     (* e = select P           *
 289      * e' = demod A e         *
 290      * A' = demod [e'] A      *
 291      * A'' = A' + e'          *
 292      * e'' = fresh e'         *
 293      * new = supright e'' A'' *
 294      * new'= demod A'' new    *
 295      * P' = P + new'          *)
 296     debug (lazy ("Forward infer step for "^ (Pp.pp_unit_clause current)));
 297     debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives)))));
 298     noprint (lazy (pp_clauses actives passives));
 299     let _ = noprint
 300       (lazy
 301          ("Actives before simplification:" ^ (String.concat ";\n"
 302             (List.map Pp.pp_unit_clause (fst actives))))) in
 303     match Sup.keep_simplified current actives bag maxvar
 304     with
 305       | _,None -> debug(lazy("None")); s
 306       | bag,Some (current,actives) ->
 307     debug (lazy ("simplified to " ^ (Pp.pp_unit_clause current)));
 308     let _ = noprint
 309       (lazy
 310          ("Actives after simplification:" ^ (String.concat ";\n"
 311             (List.map Pp.pp_unit_clause (fst actives))))) in
 312     let bag, maxvar, actives, new_clauses =
 313       Sup.infer_right bag maxvar current actives
 314     in
 315       debug
 316         (lazy
 317          ("New clauses :" ^ (String.concat ";\n"
 318             (List.map Pp.pp_unit_clause new_clauses))));
 319       debug (lazy "Demodulating goals with actives...");
 320       (* keep goals demodulated w.r.t. actives and check if solved *)
 321       let bag, g_actives =
 322         List.fold_left
 323           (fun (bag,acc) c ->
 324              match
 325                Sup.simplify_goal ~no_demod:false maxvar (snd actives) bag acc c
 326              with
 327                | None -> bag, acc
 328                | Some (bag,c1) -> bag,if c==c1 then c::acc else c::c1::acc)
 329           (bag,[]) g_actives
 330       in
 331       let ctable = IDX.index_unit_clause IDX.DT.empty current in
 332       let bag, maxvar, new_goals =
 333         List.fold_left
 334           (fun (bag,m,acc) g ->
 335              let bag, m, ng = Sup.infer_left bag m g ([current],ctable) in
 336                bag,m,ng@acc)
 337           (bag,maxvar,[]) g_actives
 338       in
 339       let bag = Terms.replace_in_bag (current,false,iterno) bag in
 340         (* prerr_endline (Pp.pp_bag bag); *)
 341     bag, maxvar, actives,
 342     add_passive_clauses passives new_clauses, g_actives,
 343     add_passive_goals g_passives new_goals
 344   ;;
 345
 346   let debug_status (_,_,actives,passives,g_actives,g_passives) =
 347     lazy
 348       ((Printf.sprintf "Number of active goals : %d\n"
 349           (List.length g_actives)) ^
 350        (Printf.sprintf "Number of passive goals : %d\n"
 351           (g_passive_set_cardinal g_passives)) ^
 352        (Printf.sprintf "Number of actives : %d\n"
 353           (List.length (fst actives))) ^
 354        (Printf.sprintf "Number of passives : %d\n"
 355          (passive_set_cardinal passives)))
 356   ;;
 357
 358
 359   (* we just check if any of the active goals is subsumed by a
 360      passive clause, or if any of the passive goal is subsumed
 361      by an active or passive clause *)
 362   let last_chance (bag,maxvar,actives,passives,g_actives,g_passives) =
 363     debug (lazy("Last chance " ^ string_of_float
 364                   (Unix.gettimeofday())));
 365     let actives_l, active_t = actives in
 366     let passive_t,wset,_ = passives in
 367     let _ = noprint
 368       (lazy
 369          ("Actives :" ^ (String.concat ";\n"
 370             (List.map Pp.pp_unit_clause actives_l)))) in
 371     let wset = IDX.elems passive_t in
 372     let _ = noprint
 373       (lazy
 374          ("Passives:" ^(String.concat ";\n"
 375             (List.map (fun (_,cl) -> Pp.pp_unit_clause cl)
 376                (IDX.ClauseSet.elements wset))))) in
 377     let g_passives =
 378       WeightPassiveSet.fold
 379         (fun (_,x) acc ->
 380           if List.exists (Sup.are_alpha_eq x) g_actives then acc
 381           else x::acc)
 382           (fst g_passives) []
 383     in
 384       ignore
 385       (List.iter
 386         (fun x ->
 387             ignore
 388              (debug (lazy("ckecking goal vs a: " ^ Pp.pp_unit_clause x));
 389                Sup.simplify_goal ~no_demod:true maxvar active_t bag [] x))
 390        g_passives);
 391       ignore
 392       (List.iter
 393          (fun x ->
 394             ignore
 395               (debug (lazy("ckecking goal vs p: " ^ Pp.pp_unit_clause x));
 396         Sup.simplify_goal ~no_demod:true maxvar passive_t bag [] x))
 397         (g_actives@g_passives));
 398     raise (Stop (Timeout (maxvar,bag)))
 399
 400   let check_timeout = function
 401     | None -> false
 402     | Some timeout -> Unix.gettimeofday () > timeout
 403
 404   let rec given_clause ~useage
 405     bag maxvar iterno weight_picks max_steps timeout
 406     actives passives g_actives g_passives
 407   =
 408     let iterno = iterno + 1 in
 409     if iterno = max_steps || check_timeout timeout then
 410       last_chance (bag,maxvar,actives,passives,g_actives,g_passives)
 411     else
 412     let use_age = useage && (weight_picks = (iterno / 6 + 1)) in
 413     let weight_picks = if use_age then 0 else weight_picks+1
 414     in
 415
 416     let rec aux_select bag
 417         (passives:IDX.DT.t * WeightPassiveSet.t * AgePassiveSet.t)
 418         g_passives =
 419       let backward,(weight,current),passives,g_passives =
 420         select ~use_age passives g_passives
 421       in
 422         if use_age && weight > monster then
 423           let bag,cl = Terms.add_to_bag current bag in
 424             if backward then
 425               aux_select bag passives (add_passive_goal g_passives cl)
 426             else
 427               aux_select bag (add_passive_clause passives cl) g_passives
 428         else
 429           let bag = Terms.replace_in_bag (current,false,iterno) bag in
 430         if backward then
 431           let _ = debug (lazy("Selected goal : " ^ Pp.pp_unit_clause current)) in
 432          match
 433            Sup.simplify_goal
 434              ~no_demod:false maxvar (snd actives) bag g_actives current
 435          with
 436            | None -> aux_select bag passives g_passives
 437            | Some (bag,g_current) ->
 438                backward_infer_step bag maxvar actives passives
 439                  g_actives g_passives g_current iterno
 440         else
 441           let _ = debug (lazy("Selected fact : " ^ Pp.pp_unit_clause current))
 442           in
 443             if Sup.orphan_murder bag (fst actives) current then
 444               let _ = debug (lazy "Orphan murdered") in
 445               let bag = Terms.replace_in_bag (current,true,iterno) bag in
 446                 aux_select bag passives g_passives
 447             else
 448               let s = bag,maxvar,actives,passives,g_actives,g_passives in
 449               let s1 = forward_infer_step s current iterno
 450               in
 451                 if s == s1 then aux_select bag passives g_passives
 452                 else s1
 453     in
 454       (*prerr_endline "Active table :";
 455        (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x))
 456           (fst actives)); *)
 457
 458     let (bag,maxvar,actives,passives,g_actives,g_passives) as status  =
 459       aux_select bag passives g_passives
 460     in
 461       debug (debug_status status);
 462       given_clause ~useage
 463         bag maxvar iterno weight_picks max_steps timeout
 464         actives passives g_actives g_passives
 465   ;;
 466
 467   let check_and_infer ~no_demod iterno status current =
 468     let bag,maxvar,actives,passives,g_actives,g_passives = status in
 469     match
 470       Sup.simplify_goal
 471         ~no_demod maxvar (snd actives) bag g_actives current
 472     with
 473       | None -> debug (lazy "None"); status
 474       | Some (bag,g_current) ->
 475           let _ =
 476             debug (lazy("Infer on goal : "
 477                         ^ Pp.pp_unit_clause g_current))
 478           in
 479             backward_infer_step bag maxvar actives passives
 480               g_actives g_passives g_current iterno
 481
 482   (* similar to given_clause, but it merely works on goals,
 483      in parallel, at each iteration *)
 484   let rec goal_narrowing iterno max_steps timeout status
 485   =
 486     debug (debug_status status);
 487     let iterno = iterno + 1 in
 488     if iterno = max_steps || check_timeout timeout then
 489       last_chance status
 490     else
 491     let _,_,_,_,_,g_passives = status in
 492     let passive_goals = WeightPassiveSet.elements (fst g_passives) in
 493     let newstatus =
 494       List.fold_left
 495         (fun acc g ->
 496            let bag,maxvar,actives,passives,g_actives,g_passives = acc in
 497            let g_passives =
 498              remove_passive_goal g_passives g in
 499            let current = snd g in
 500            let _ =
 501              debug (lazy("Selected goal gn: " ^ Pp.pp_unit_clause current))
 502            in
 503              (* we work both on the original goal and the demodulated one*)
 504            let acc = check_and_infer ~no_demod:false iterno acc current
 505            in check_and_infer ~no_demod:true iterno acc current)
 506         status passive_goals
 507     in
 508       goal_narrowing iterno max_steps timeout newstatus
 509
 510     let compute_result bag i subst =
 511       let l =
 512         let rec traverse ongoal (accg,acce) i =
 513           match Terms.get_from_bag i bag with
 514             | (id,_,_,Terms.Exact _),_,_ ->
 515                 if ongoal then [i],acce else
 516                   if (List.mem i acce) then accg,acce else accg,acce@[i]
 517             | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),_,_ ->
 518                 if (not ongoal) && (List.mem i acce) then accg,acce
 519                 else
 520                   let accg,acce =
 521                     traverse false (traverse ongoal (accg,acce) i1) i2
 522                   in
 523                     if ongoal then i::accg,acce else accg,i::acce
 524         in
 525         let gsteps,esteps = traverse true ([],[]) i in
 526           (List.rev esteps)@gsteps
 527       in
 528       debug (lazy ("steps: " ^ (string_of_int (List.length l))));
 529       let max_w =
 530         List.fold_left
 531           (fun acc i ->
 532              let (cl,_,_) = Terms.get_from_bag i bag in
 533                max acc (Order.compute_unit_clause_weight cl)) 0 l in
 534         debug (lazy ("Max weight : " ^ (string_of_int max_w)));
 535 (*        List.iter (fun id -> let ((_,lit,_,proof as cl),d,it) =
 536             Terms.get_from_bag id bag in
 537               if d then
 538                 prerr_endline
 539                 (Printf.sprintf "Id : %d, selected at %d, weight %d,disc, by %s"
 540                    id it (Order.compute_unit_clause_weight cl)
 541                    (Pp.pp_proof_step proof))
 542               else
 543                prerr_endline
 544                 (Printf.sprintf "Id : %d, selected at %d, weight %d by %s"
 545                    id it (Order.compute_unit_clause_weight cl)
 546                    (Pp.pp_proof_step proof))) l;*)
 547         debug (lazy ("Proof:" ^
 548           (String.concat "\n"
 549              (List.map
 550                 (fun x ->
 551                    let cl,_,_ = Terms.get_from_bag x bag in
 552                      Pp.pp_unit_clause cl) l))));
 553         Unsatisfiable [ bag, i, subst, l ]
 554
 555   let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
 556     let _initial_timestamp = Unix.gettimeofday () in
 557     let passives =
 558       add_passive_clauses ~no_weight:true passive_empty_set passives
 559     in
 560     let g_passives =
 561       add_passive_goals ~no_weight:true g_passive_empty_set g_passives
 562     in
 563     let g_actives = [] in
 564     let actives = [], IDX.DT.empty in
 565     try
 566      given_clause ~useage ~noinfer:false
 567       bag maxvar 0  0 max_steps timeout actives passives g_actives g_passives
 568     with
 569     | Sup.Success (bag, _, (i,_,_,_),subst) ->
 570         compute_result bag i subst
 571     | Stop (Unsatisfiable _) -> Error "solution found!"
 572     | Stop o -> o
 573   ;;
 574
 575 let demod s goal =
 576   let bag,maxvar,actives,passives,g_actives,g_passives = s in
 577   let (bag,maxvar), g = mk_goal (bag,maxvar) goal in
 578   let bag, ((i,_,_,_) as g1) = Sup.demodulate bag g (snd actives) in
 579     if g1 = g then GaveUp else compute_result bag i []
 580 (*
 581   if Terms.is_eq_clause g then
 582
 583   else GaveUp *)
 584
 585 let fast_eq_check s goal =
 586   let (_,_,_,_,_,g_passives) as s = initialize_goal s goal in
 587   if is_passive_g_set_empty g_passives then Error "not an equation"
 588   else
 589   try
 590     goal_narrowing 0 2 None s
 591   with
 592     | Sup.Success (bag, _, (i,_,_,_),subst) ->
 593         compute_result bag i subst
 594     | Stop (Unsatisfiable _) -> Error "solution found!"
 595     | Stop o -> o
 596   ;;
 597
 598 let nparamod ~useage ~max_steps ?timeout s goal =
 599   let bag,maxvar,actives,passives,g_actives,g_passives
 600       = initialize_goal s goal in
 601   if is_passive_g_set_empty g_passives then Error "not an equation"
 602   else
 603     try given_clause ~useage ~noinfer:false
 604       bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives
 605   with
 606     | Sup.Success (bag, _, (i,_,_,_),subst) ->
 607         compute_result bag i subst
 608     | Stop (Unsatisfiable _) -> Error "solution found!"
 609     | Stop o -> o
 610   ;;
 611
 612 end