1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
qi_params.h
Abstract:
<abstract>
Author:
Leonardo de Moura (leonardo) 2008-06-15.
Revision History:
--*/
#pragma once
#include "util/util.h"
#include "util/params.h"
enum quick_checker_mode {
MC_NO, // do not use (cheap) model checking based instantiation
MC_UNSAT, // instantiate unsatisfied instances
MC_NO_SAT // instantiate unsatisfied and not-satisfied instances
};
struct qi_params {
std::string m_qi_cost;
std::string m_qi_new_gen;
double m_qi_eager_threshold = 10.0;
double m_qi_lazy_threshold = 20.0;
unsigned m_qi_max_eager_multipatterns = 0;
unsigned m_qi_max_lazy_multipattern_matching = 2;
bool m_qi_profile = false;
unsigned m_qi_profile_freq = UINT_MAX;
quick_checker_mode m_qi_quick_checker = MC_NO;
bool m_qi_lazy_quick_checker = true;
bool m_qi_promote_unsat = true;
unsigned m_qi_max_instances = UINT_MAX;
bool m_qi_persist_instances = false; // re-assert MBQI instances at base level on a re-search
unsigned m_qi_max_persistent_instances = 1000; // pattern-based instances re-asserted alongside
bool m_qi_lazy_instantiation = false;
bool m_qi_conservative_final_check = false;
bool m_qi_update_generation = true;
bool m_qe_lite = false;
bool m_mbqi = true;
unsigned m_mbqi_max_cexs = 1;
bool m_mbqi_instances_after_giveup = true; // internal: let MBQI continue after a theory gave up (disabled in MBQI's auxiliary context)
unsigned m_mbqi_max_cexs_incr = 1;
unsigned m_mbqi_max_iterations = 1000;
bool m_mbqi_trace = false;
unsigned m_mbqi_force_template = 10;
const char * m_mbqi_id = nullptr;
qi_params(params_ref const & p = params_ref()):
/*
The "weight 0" performance bug
------------------------------
The parameters m_qi_cost and m_qi_new_gen influence quantifier instantiation.
- m_qi_cost: specify the cost of a quantifier instantiation. Z3 will block instantiations using m_qi_eager_threshold and m_qi_lazy_threshold.
- m_qi_new_gen: specify how the "generation" tag of an enode created by quantifier instantiation is set.
Enodes in the input problem have generation 0.
Some combinations of m_qi_cost and m_qi_new_gen will prevent Z3 from breaking matching loops.
For example, the "Weight 0" performance bug was triggered by the following combination:
- m_qi_cost: (+ weight generation)
- m_qi_new_gen: cost
If a quantifier has weight 0, then the cost of instantiating it with a term in the input problem has cost 0.
The new enodes created during the instantiation will be tagged with generation = const = 0. So, every enode
will have generation 0, and consequently every quantifier instantiation will have cost 0.
Although dangerous, this feature was requested by the Boogie team. In their case, the patterns are carefully constructed,
and there are no matching loops. Moreover, the tag some quantifiers with weight 0 to instruct Z3 to never block their instances.
An example is the select-store axiom. They need this feature to be able to analyze code that contains very long execution paths.
So, unless requested by the user, the default weight must be > 0. Otherwise, Z3 will execute without any
matching loop detection.
*/
m_qi_cost("(+ weight generation)"),
m_qi_new_gen("cost")
{
updt_params(p);
}
void updt_params(params_ref const & p);
void display(std::ostream & out) const;
};