- let mk_clause bag maxvar (t,ty) =
- let (proof,ty) = B.saturate t ty in
- let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
- let bag, c = Utils.add_to_bag bag c in
- bag, maxvar, c
- in
- let bag, maxvar, goal = mk_clause Terms.M.empty 0 t in
- let g_actives = [] in
- let g_passives = PassiveSet.singleton (Utils.mk_passive_clause goal) in
- let passives, bag, maxvar =
- List.fold_left
- (fun (cl, bag, maxvar) t ->
- let bag, maxvar, c = mk_clause bag maxvar t in
- (add_passive_clause cl c), bag, maxvar)
- (PassiveSet.empty, bag, maxvar) table
- in
- let actives = [], IDX.DT.empty in
- try given_clause bag maxvar actives passives g_actives g_passives
- with
- | Sup.Success (bag, _, (i,_,_,_)) ->
- let l =
- let rec traverse ongoal (accg,acce) i =
- match Terms.M.find i bag with
- | (id,_,_,Terms.Exact _) ->
- if ongoal then [i],acce else
- if (List.mem i acce) then accg,acce else accg,acce@[i]
- | (_,_,_,Terms.Step (_,i1,i2,_,_,_)) ->
- if (not ongoal) && (List.mem i acce) then accg,acce
- else
- let accg,acce =
- traverse false (traverse ongoal (accg,acce) i1) i2
- in
- if ongoal then i::accg,acce else accg,i::acce
+ let paramod ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
+ let initial_timestamp = Unix.gettimeofday () in
+ let passives = add_passive_clauses passive_empty_set passives in
+ let g_passives = add_passive_clauses passive_empty_set g_passives in
+ let g_actives = [] in
+ let actives = [], IDX.DT.empty in
+ try
+ given_clause
+ bag maxvar 0 max_steps timeout actives passives g_actives g_passives
+ with
+ | Sup.Success (bag, _, (i,_,_,_)) ->
+ let l =
+ let rec traverse ongoal (accg,acce) i =
+ match Terms.M.find i bag with
+ | (id,_,_,Terms.Exact _),_ ->
+ if ongoal then [i],acce else
+ if (List.mem i acce) then accg,acce else accg,acce@[i]
+ | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),_ ->
+ if (not ongoal) && (List.mem i acce) then accg,acce
+ else
+ let accg,acce =
+ traverse false (traverse ongoal (accg,acce) i1) i2
+ in
+ if ongoal then i::accg,acce else accg,i::acce
+ in
+ let gsteps,esteps = traverse true ([],[]) i in
+ (List.rev esteps)@gsteps