- | Sup.Success (bag, _, (i,_,_,_)) ->
- compute_result bag i
+ | 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