open AutoTypes;;
open AutoCache;;
-let debug_print s = () (* prerr_endline s;; *)
+let debug_print s = () (*prerr_endline s;;*)
(* {{{ *********** local given_clause wrapper ***********)
-let given_clause dbd ?tables maxm ?auto cache subst flags smart_flag status =
+let given_clause dbd ?tables maxm auto cache subst flags smart_flag status =
let active,passive,bag,cache,maxmeta,goal_steps,saturation_steps,timeout =
match tables with
| None ->
(* first time, do a huge saturation *)
let bag, equalities, cache, maxmeta =
- Saturation.find_equalities dbd status ?auto smart_flag cache
+ Saturation.find_equalities dbd status smart_flag auto cache
in
let passive = Saturation.make_passive equalities in
let active = Saturation.make_active [] in
(* saturate a bit more if cache cahnged *)
let bag, equalities, cache, maxm =
if cache_size oldcache <> cache_size cache then
- Saturation.saturate_more
- bag active maxm status smart_flag ?auto cache
+ Saturation.close_more
+ bag active maxm status smart_flag auto cache
else
bag, [], cache, maxm
in
let passive = Saturation.add_to_passive equalities passive in
let goal_steps, saturation_steps, timeout =
if flags.use_only_paramod then max_int,max_int,flags.timeout
- else max 80 minsteps, minsteps, infinity
+ else max 50 minsteps, minsteps, infinity
in
active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
in
let flags =
{flags with use_only_paramod=true;timeout=Unix.gettimeofday() +. 30.0}
in
- given_clause dbd ?tables 0 cache [] flags true (proof'''',newmeta)
+ given_clause dbd ?tables 0 None cache [] flags true (proof'''',newmeta)
with
| None, active, passive, bag,_,_ ->
raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
;;
let equational_case
- dbd tables maxm ?auto cache depth fake_proof goalno goalty subst context
+ dbd tables maxm auto cache depth fake_proof goalno goalty subst context
flags
=
let ppterm = ppterm context in
prerr_endline ("PARAMOD SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty );
+(*
prerr_endline "<CACHE>";
prerr_endline (cache_print context cache);
prerr_endline "</CACHE>";
+*)
match
- given_clause dbd ?tables maxm ?auto cache subst flags false (fake_proof,goalno)
+ given_clause dbd ?tables maxm auto cache subst flags false (fake_proof,goalno)
with
| None, active,passive, bag, cache, maxmeta ->
let tables = Some (active,passive,bag,cache) in
(flags.use_only_paramod && ensure_equational goalty)
;;
let cache_add_success sort cache k v =
- if sort = P then cache_add_success cache k v else cache
+ if sort = P then cache_add_success cache k v else cache_remove_underinspection
+ cache k
;;
let rec auto_main dbd tables maxm context flags elems cache =
if is_equational_case goalty flags then
match
equational_case dbd tables maxm
- ~auto:callback_for_paramod cache
+ (Some callback_for_paramod) cache
depth fake_proof goalno goalty subst context flags
with
| Some elems, tables, cache, maxm ->
- elems, tables, cache, maxm (* manca cache *)
+ elems, tables, cache, maxm
| None, tables,cache,maxm ->
applicative_case dbd tables maxm depth subst fake_proof goalno
goalty metasenv context cache