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