+ 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 demod s goal =
+ let bag,maxvar,actives,passives,g_actives,g_passives = s in
+ let (bag,maxvar), g = mk_goal (bag,maxvar) goal in
+ let bag, ((i,_,_,_) as g1) = Sup.demodulate bag g (snd actives) in
+ if g1 = g then GaveUp else compute_result bag i []
+(*
+ if Terms.is_eq_clause g then
+
+ else GaveUp *)
+
+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!"
+ | Stop o -> o
+ ;;
+
+let nparamod ~useage ~max_steps ?timeout s goal =
+ let bag,maxvar,actives,passives,g_actives,g_passives
+ = initialize_goal s goal in
+ if is_passive_g_set_empty g_passives then Error "not an equation"
+ else
+ 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!"