- prerr_endline
- (Printf.sprintf "Found proof, %fs"
- (Unix.gettimeofday() -. initial_timestamp));
- (*
- prerr_endline "Proof:";
- List.iter (fun x ->
- prerr_endline (Pp.pp_unit_clause (fst(Terms.M.find x bag)))) l;
- *)
- Unsatisfiable [ bag, i, l ]
- | Stop (Unsatisfiable _) -> Error "stop bug solution found!"
+ 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
+ let passives =
+ add_passive_clauses ~no_weight:true passive_empty_set passives
+ in
+ let g_passives =
+ add_passive_goals ~no_weight:true g_passive_empty_set g_passives
+ in
+ let g_actives = [] in
+ let actives = [], IDX.DT.empty in
+ try
+ given_clause ~useage ~noinfer:false
+ bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives
+ with
+ | Sup.Success (bag, _, (i,_,_,_),subst) ->
+ compute_result bag i subst
+ | Stop (Unsatisfiable _) -> Error "solution found!"
+ | Stop o -> o
+ ;;
+
+let fast_eq_check s goal =
+ let (_,_,_,_,_,g_passives) as s = initialize_goal s goal in
+ if is_passive_g_set_empty g_passives then Error "not an equation"
+ else
+ try
+ goal_narrowing 0 2 None s
+ with
+ | Sup.Success (bag, _, (i,_,_,_),subst) ->
+ compute_result bag i subst
+ | Stop (Unsatisfiable _) -> Error "solution found!"