+let inductive l =
+ let queries = ref [] in
+ let univ = None in
+ let handle = get_handle () in
+ let rec aux = function
+ | [] -> ()
+ | term :: tail ->
+ aux tail;
+ print_string ("? " ^ CicPp.ppterm term ^ nl);
+ let t = U.start_time () in
+ let m = C3.get_constraints term in
+ let q = G.query_of_constraints univ m (None, None, None) in
+ if not (List.mem q ! queries) then
+ begin
+ issue handle q;
+ Printf.eprintf "[%i] " (pred ! query_num); flush stderr;
+ Printf.printf "%i GEN: %s"
+ (pred ! query_num) (U.stop_time t ^ nl);
+ flush stdout; queries := q :: ! queries
+ end
+ in
+ aux l;
+ Printf.eprintf "\nmqgtop: inductive: %i queries issued\n"
+ (List.length ! queries);
+ flush stderr;
+ C.close handle
+