lower skolem penalty to ensure that some useful facts with existentials, e.g. congruence of "setsum", eventually get picked up
authorblanchet
Wed May 16 18:16:51 2012 +0200 (2012-05-16)
changeset 4793408d7aff8c7e6
parent 47933 4e8e0245e8be
child 47935 631ea563c20a
lower skolem penalty to ensure that some useful facts with existentials, e.g. congruence of "setsum", eventually get picked up
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed May 16 18:16:51 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed May 16 18:16:51 2012 +0200
     1.3 @@ -223,7 +223,7 @@
     1.4     higher_order_irrel_weight = 1.05,
     1.5     abs_rel_weight = 0.5,
     1.6     abs_irrel_weight = 2.0,
     1.7 -   skolem_irrel_weight = 0.25,
     1.8 +   skolem_irrel_weight = 0.05,
     1.9     theory_const_rel_weight = 0.5,
    1.10     theory_const_irrel_weight = 0.25,
    1.11     chained_const_irrel_weight = 0.25,