# HG changeset patch
# User blanchet
# Date 1354924130 -3600
# Node ID 960a3429615c21e640573f75ee5209c0cc11c2fb
# Parent  702278df3b57aff4c55fec3bffb0206ace927432
more MaSh tweaking -- in particular, export the same facts in "MaSh_Export" as are later tried in "MaSh_Eval"

diff -r 702278df3b57 -r 960a3429615c src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Fri Dec 07 23:14:39 2012 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy	Sat Dec 08 00:48:50 2012 +0100
@@ -14,6 +14,8 @@
   [provers = spass, max_relevant = 32, strict, dont_slice, type_enc = mono_native,
    lam_trans = combs_and_lifting, timeout = 2, dont_preplay, minimize]
 
+declare [[sledgehammer_instantiate_inducts]]
+
 ML {*
 open MaSh_Export
 *}
diff -r 702278df3b57 -r 960a3429615c src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Fri Dec 07 23:14:39 2012 +0100
+++ b/src/HOL/TPTP/mash_export.ML	Sat Dec 08 00:48:50 2012 +0100
@@ -28,7 +28,6 @@
 structure MaSh_Export : MASH_EXPORT =
 struct
 
-open Sledgehammer_Fact
 open Sledgehammer_MePo
 open Sledgehammer_MaSh
 
@@ -45,8 +44,7 @@
 
 fun all_facts ctxt =
   let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in
-    nearly_all_facts ctxt false no_fact_override Symtab.empty css [] []
-                     @{prop True}
+    Sledgehammer_Fact.all_facts ctxt false Symtab.empty [] [] css
   end
 
 fun add_thy_parent_facts thy_map thy =
diff -r 702278df3b57 -r 960a3429615c src/HOL/Tools/Sledgehammer/MaSh/src/mash.py
--- a/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py	Fri Dec 07 23:14:39 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/MaSh/src/mash.py	Sat Dec 08 00:48:50 2012 +0100
@@ -29,8 +29,8 @@
 parser = ArgumentParser(description='MaSh - Machine Learning for Sledgehammer.  \n\n\
 MaSh allows to use different machine learning algorithms to predict relevant facts for Sledgehammer.\n\n\
 --------------- Example Usage ---------------\n\
-First initialize:\n./mash.py -l test.log -o ../tmp/ --init --inputDir ../data/Nat/ \n\
-Then create predictions:\n./mash.py -i ../data/Nat/mash_commands -p ../tmp/test.pred -l test.log -o ../tmp/ --statistics\n\
+First initialize:\n./mash.py -l test.log -o ../tmp/ --init --inputDir ../data/Jinja/ \n\
+Then create predictions:\n./mash.py -i ../data/Jinja/mash_commands -p ../data/Jinja/mash_suggestions -l test.log -o ../tmp/ --statistics\n\
 \n\n\
 Author: Daniel Kuehlwein, July 2012',formatter_class=RawDescriptionHelpFormatter)
 parser.add_argument('-i','--inputFile',help='File containing all problems to be solved.')
@@ -40,7 +40,7 @@
 parser.add_argument('--numberOfPredictions',default=200,help="Number of premises to write in the output. Default=200.",type=int)
 
 parser.add_argument('--init',default=False,action='store_true',help="Initialize Mash. Requires --inputDir to be defined. Default=False.")
-parser.add_argument('--inputDir',default='../data/Nat/',\
+parser.add_argument('--inputDir',default='../data/Jinja/',\
                     help='Directory containing all the input data. MaSh expects the following files: mash_features,mash_dependencies,mash_accessibility')
 parser.add_argument('--depFile', default='mash_dependencies',
                     help='Name of the file with the premise dependencies. The file must be in inputDir. Default = mash_dependencies')
@@ -217,11 +217,11 @@
 
 if __name__ == '__main__':
     # Example:
-    # Nat
-    #args = ['-l','testIsabelle.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Nat/','--predef']
-    #args = ['-i', '../data/Nat/mash_commands','-p','../tmp/testIsabelle.pred','-l','testIsabelle.log','--predef','-o','../tmp/','--statistics','--saveStats','../tmp/natATPMP.stats']
-    #args = ['-l','testNB.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Nat/']
-    #args = ['-i', '../data/Nat/mash_commands','-p','../tmp/testNB.pred','-l','../tmp/testNB.log','--nb','-o','../tmp/','--statistics','--saveStats','../tmp/natATPNB.stats','--cutOff','500']
+    # Jinja
+    #args = ['-l','testIsabelle.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Jinja/','--predef']
+    #args = ['-i', '../data/Jinja/mash_commands','-p','../tmp/testIsabelle.pred','-l','testIsabelle.log','--predef','-o','../tmp/','--statistics','--saveStats','../tmp/natATPMP.stats']
+    #args = ['-l','testNB.log','-o','../tmp/','--statistics','--init','--inputDir','../data/Jinja/']
+    #args = ['-i', '../data/Jinja/mash_commands','-p','../tmp/testNB.pred','-l','../tmp/testNB.log','--nb','-o','../tmp/','--statistics','--saveStats','../tmp/natATPNB.stats','--cutOff','500']
     # List
     #args = ['-l','testIsabelle.log','-o','../tmp/','--statistics','--init','--inputDir','../data/List/','--isabelle']
     #args = ['-i', '../data/List/mash_commands','-p','../tmp/testIsabelle.pred','-l','testIsabelle.log','--isabelle','-o','../tmp/','--statistics']
diff -r 702278df3b57 -r 960a3429615c src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Dec 07 23:14:39 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sat Dec 08 00:48:50 2012 +0100
@@ -593,9 +593,9 @@
     |> exists (exists_Const is_exists) ts ? cons skos_feature
   end
 
-(* Too many dependencies is a sign that a crazy decision procedure is at work.
-   There isn't much to learn from such proofs. *)
-val max_dependencies = 10
+(* Too many dependencies is a sign that a decision procedure is at work. There
+   isn't much to learn from such proofs. *)
+val max_dependencies = 20
 val atp_dependency_default_max_facts = 50
 
 (* "type_definition_xxx" facts are characterized by their use of "CollectI". *)