src/HOL/SMT.thy
changeset 40664 e023788a91a1
parent 40662 798aad2229c0
child 40681 872b08416fb4
     1.1 --- a/src/HOL/SMT.thy	Mon Nov 22 15:45:43 2010 +0100
     1.2 +++ b/src/HOL/SMT.thy	Mon Nov 22 23:37:00 2010 +0100
     1.3 @@ -54,6 +54,33 @@
     1.4  
     1.5  
     1.6  
     1.7 +subsection {* Quantifier weights *}
     1.8 +
     1.9 +text {*
    1.10 +Weight annotations to quantifiers influence the priority of quantifier
    1.11 +instantiations.  They should be handled with care for solvers, which support
    1.12 +them, because incorrect choices of weights might render a problem unsolvable.
    1.13 +*}
    1.14 +
    1.15 +definition weight :: "int \<Rightarrow> bool \<Rightarrow> bool" where "weight _ P = P"
    1.16 +
    1.17 +text {*
    1.18 +Weights must be non-negative.  The value @{text 0} is equivalent to providing
    1.19 +no weight at all.
    1.20 +
    1.21 +Weights should only be used at quantifiers and only inside triggers (if the
    1.22 +quantifier has triggers).  Valid usages of weights are as follows:
    1.23 +
    1.24 +\begin{itemize}
    1.25 +\item
    1.26 +@{term "\<forall>x. trigger [[pat (P x)]] (weight 2 (P x))"}
    1.27 +\item
    1.28 +@{term "\<forall>x. weight 3 (P x)"}
    1.29 +\end{itemize}
    1.30 +*}
    1.31 +
    1.32 +
    1.33 +
    1.34  subsection {* Distinctness *}
    1.35  
    1.36  text {*
    1.37 @@ -342,7 +369,7 @@
    1.38  
    1.39  hide_type (open) pattern
    1.40  hide_const Pattern term_eq
    1.41 -hide_const (open) trigger pat nopat distinct fun_app z3div z3mod
    1.42 +hide_const (open) trigger pat nopat weight distinct fun_app z3div z3mod
    1.43  
    1.44  
    1.45