equal
deleted
inserted
replaced
36 consts |
36 consts |
37 pat :: "'a \<Rightarrow> pattern" |
37 pat :: "'a \<Rightarrow> pattern" |
38 nopat :: "'a \<Rightarrow> pattern" |
38 nopat :: "'a \<Rightarrow> pattern" |
39 |
39 |
40 definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool" where "trigger _ P = P" |
40 definition trigger :: "pattern list list \<Rightarrow> bool \<Rightarrow> bool" where "trigger _ P = P" |
41 |
|
42 |
|
43 subsection {* Quantifier weights *} |
|
44 |
|
45 text {* |
|
46 Weight annotations to quantifiers influence the priority of quantifier |
|
47 instantiations. They should be handled with care for solvers, which support |
|
48 them, because incorrect choices of weights might render a problem unsolvable. |
|
49 *} |
|
50 |
|
51 definition weight :: "int \<Rightarrow> bool \<Rightarrow> bool" where "weight _ P = P" |
|
52 |
|
53 text {* |
|
54 Weights must be nonnegative. The value @{text 0} is equivalent to providing |
|
55 no weight at all. |
|
56 |
|
57 Weights should only be used at quantifiers and only inside triggers (if the |
|
58 quantifier has triggers). Valid usages of weights are as follows: |
|
59 |
|
60 \begin{itemize} |
|
61 \item |
|
62 @{term "\<forall>x. trigger [[pat (P x)]] (weight 2 (P x))"} |
|
63 \item |
|
64 @{term "\<forall>x. weight 3 (P x)"} |
|
65 \end{itemize} |
|
66 *} |
|
67 |
41 |
68 |
42 |
69 subsection {* Higher-order encoding *} |
43 subsection {* Higher-order encoding *} |
70 |
44 |
71 text {* |
45 text {* |
428 "(if P then Q else \<not>R) \<or> P \<or> R" |
402 "(if P then Q else \<not>R) \<or> P \<or> R" |
429 by auto |
403 by auto |
430 |
404 |
431 hide_type (open) pattern |
405 hide_type (open) pattern |
432 hide_const fun_app z3div z3mod |
406 hide_const fun_app z3div z3mod |
433 hide_const (open) trigger pat nopat weight |
407 hide_const (open) trigger pat nopat |
434 |
408 |
435 end |
409 end |