+ let check_and_infer ~no_demod iterno status current =
+ let bag,maxvar,actives,passives,g_actives,g_passives = status in
+ match
+ Sup.simplify_goal
+ ~no_demod maxvar (snd actives) bag g_actives current
+ with
+ | None -> debug (lazy "None"); status
+ | Some (bag,g_current) ->
+ let _ =
+ debug (lazy("Infer on goal : "
+ ^ Pp.pp_unit_clause g_current))
+ in
+ backward_infer_step bag maxvar actives passives
+ g_actives g_passives g_current iterno
+
+ (* similar to given_clause, but it merely works on goals,
+ in parallel, at each iteration *)
+ let rec goal_narrowing iterno max_steps timeout status
+ =
+ debug (debug_status status);
+ let iterno = iterno + 1 in
+ if iterno = max_steps || check_timeout timeout then
+ last_chance status
+ else
+ let _,_,_,_,_,g_passives = status in
+ let passive_goals = WeightPassiveSet.elements (fst g_passives) in
+ let newstatus =
+ List.fold_left
+ (fun acc g ->
+ let bag,maxvar,actives,passives,g_actives,g_passives = acc in
+ let g_passives =
+ remove_passive_goal g_passives g in
+ let current = snd g in
+ let _ =
+ debug (lazy("Selected goal : " ^ Pp.pp_unit_clause current))
+ in
+ (* we work both on the original goal and the demodulated one*)
+ let acc = check_and_infer ~no_demod:false iterno acc current
+ in check_and_infer ~no_demod:true iterno acc current)
+ status passive_goals
+ in
+ goal_narrowing iterno max_steps timeout newstatus
+
+ let compute_result bag i subst =
+ let l =
+ let rec traverse ongoal (accg,acce) i =
+ match Terms.get_from_bag 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
+ in
+ debug (lazy ("steps: " ^ (string_of_int (List.length l))));
+ let max_w =
+ List.fold_left
+ (fun acc i ->
+ let (cl,_,_) = Terms.get_from_bag i bag in
+ max acc (Order.compute_unit_clause_weight cl)) 0 l in
+ debug (lazy ("Max weight : " ^ (string_of_int max_w)));
+(* List.iter (fun id -> let ((_,lit,_,proof as cl),d,it) =
+ Terms.get_from_bag id bag in
+ if d then
+ prerr_endline
+ (Printf.sprintf "Id : %d, selected at %d, weight %d,disc, by %s"
+ id it (Order.compute_unit_clause_weight cl)
+ (Pp.pp_proof_step proof))
+ else
+ prerr_endline
+ (Printf.sprintf "Id : %d, selected at %d, weight %d by %s"
+ id it (Order.compute_unit_clause_weight cl)
+ (Pp.pp_proof_step proof))) l;*)
+ debug (lazy ("Proof:" ^
+ (String.concat "\n"
+ (List.map
+ (fun x ->
+ let cl,_,_ = Terms.get_from_bag x bag in
+ Pp.pp_unit_clause cl) l))));
+ Unsatisfiable [ bag, i, subst, l ]
+
+ let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
+ let _initial_timestamp = Unix.gettimeofday () in