- 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!"