New filtering function for "Auto" tactic using "just costraints"

diff --git a/helm/ocaml/tactics/filter_auto.ml b/helm/ocaml/tactics/filter_auto.ml
index 73494c8e3414e43cc8eef6d376d99dd4f4fae735..f4964f575327f8695eb08dfcfc8dda19e9ebf0fc 100644 (file)
--- a/helm/ocaml/tactics/filter_auto.ml
+++ b/helm/ocaml/tactics/filter_auto.ml
@@ -36,7 +36,7 @@ let escape = Str.global_replace (Str.regexp_string "\'") "\\'";;
 
 let hyp_const (conn:Mysql.dbd) uri =
   let uri = escape uri in
-  (*query to obtain all the constants in the hypothesis of the theorem*)
+  (*query to obtain all the constants in the hypothesis and conclusion of the theorem*)
   let query =
      "select h_occurrence from refObj where source='"^uri^
     "' and (h_position="^main_hypothesis^" or h_position="^in_hypothesis^
@@ -63,5 +63,94 @@ let filter_new_constants (conn:Mysql.dbd) const (_,uri) =
     NewConstraints.StringSet.subset hyp const
 ;;
 
+
+
+
+let rec exec_query (conn:Mysql.dbd) uris k = 
+  let add_must (n,from,where) uri =
+    let refObjn = "refObj" ^ (string_of_int n) in
+    let new_must =
+      [ refObjn^".h_occurrence = '" ^ uri ^ "'";
+        "("^refObjn^".h_position = " ^ main_conclusion^ " or "
+       ^refObjn^".h_position = " ^ in_conclusion^ " or "
+       ^refObjn^".h_position = " ^ main_hypothesis^ " or "
+       ^refObjn^".h_position = " ^ in_hypothesis^ ")"] in
+    let where' = 
+      if n = 0 then new_must@where
+      else 
+       (refObjn^".source = refObj" ^ (string_of_int (n-1)) 
+       ^ ".source")::new_must@where in
+  (n+1,("refObj as "^refObjn)::from,where')
+  in
+  let (_,from,where) = 
+    List.fold_left add_must (0,[],[]) uris in
+  let from,where = 
+    "no_concl_hyp"::from, 
+    ("no=" ^ (string_of_int k))::
+    ("no_concl_hyp.source = refObj0.source")::where
+  in
+  let from = String.concat "," from in
+  let where = String.concat " and " where in
+  let query = "select refObj0.source from " ^ from ^ " where " ^ where in
+   (* prerr_endline query;*)
+    Mysql.exec conn query
+;;
+
+let powerset set =
+  let rec powerset_r set sub =
+    if (NewConstraints.StringSet.is_empty set) then sub
+    else 
+      let a = NewConstraints.StringSet.min_elt set in
+      let newset = NewConstraints.StringSet.remove a set in
+      let newsub = NewConstraints.SetSet.union (NewConstraints.SetSet.add (NewConstraints.StringSet.singleton a)
+                   (NewConstraints.SetSet.fold 
+                      (fun s t -> (NewConstraints.SetSet.add (NewConstraints.StringSet.add a s) t)) 
+                           sub NewConstraints.SetSet.empty)) sub in
+      powerset_r newset newsub in
+powerset_r set NewConstraints.SetSet.empty
+;;
+
+let setset_to_listlist setset =
+  let listset = NewConstraints.SetSet.elements setset in
+  let res = 
+    List.map 
+      (fun set -> 
+        let el = NewConstraints.StringSet.elements set in
+        (List.length el, el)) listset in
+    (* ordered by descending cardinality *)
+List.sort (fun (n,_) (m,_) -> m - n) res
+
+let exist_element list_of_uris (_,uri) =
+  let ex u =
+    if u = uri then true
+    else false
+  in
+List.exists ex list_of_uris
+;;
+    
+
+let filter_uris (conn:Mysql.dbd) const uris =
+  let subsets_of_consts = 
+    setset_to_listlist (powerset const) in
+  let uris_of_const =
+    List.concat
+     (List.map 
+             (fun (m,s) -> 
+                (let res = 
+                   exec_query conn s m in
+                 let f a = 
+                   match (Array.to_list a) with
+                       [Some uri] -> uri
+                       | _ -> assert false in
+                   Mysql.map ~f:f res))
+             subsets_of_consts)
+      in
+List.filter (exist_element uris_of_const) uris
+;;  
+   
+let rec power n m =
+  if (m = 1) then n
+  else n*(power n (m-1))
+;;
        
 

diff --git a/helm/ocaml/tactics/filter_auto.mli b/helm/ocaml/tactics/filter_auto.mli
index 44dfd32a9d2352095a50e64589b3685f2ef4bf46..06909a836ea1aa57c6476f9a92b1d7cf7ad7ef75 100644 (file)
--- a/helm/ocaml/tactics/filter_auto.mli
+++ b/helm/ocaml/tactics/filter_auto.mli
@@ -23,7 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
-
+val power:
+ int -> int -> int 
 
 val filter_new_constants: 
        Mysql.dbd ->
@@ -31,3 +32,8 @@ val filter_new_constants:
        int * string ->
        bool
 
+val filter_uris:
+       Mysql.dbd ->
+       NewConstraints.StringSet.t ->
+       (int * string) list ->
+       (int * string) list

diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml
index 561997f6f86b317ba415c4a36adb82917a13d38a..f9c7feae7012589438ca3171d48d5e8407a4a6d1 100644 (file)
--- a/helm/ocaml/tactics/tacticChaser.ml
+++ b/helm/ocaml/tactics/tacticChaser.ml
@@ -156,7 +156,11 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st
     List.fold_right hyp ey NewConstraints.StringSet.empty in
   prerr_endline (NewConstraints.pp_StringSet (NewConstraints.StringSet.union hyp_const concl_const));
   (* uris with new constants in the proof are filtered *)
-  let uris = List.filter (Filter_auto.filter_new_constants conn (NewConstraints.StringSet.union hyp_const concl_const)) uris in 
+  let all_const = NewConstraints.StringSet.union hyp_const concl_const in
+  let uris = 
+    if (List.length uris < (Filter_auto.power 2 (List.length (NewConstraints.StringSet.elements all_const))))
+     then List.filter (Filter_auto.filter_new_constants conn all_const) uris 
+    else Filter_auto.filter_uris conn all_const uris in 
 (*
   let uris =
     (* ristretto all cache *)