mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

scale theory-aware priority by bvar_inc

Browse source
This commit is contained in:
Murphy Berzish 2017-01-14 15:28:58 -05:00
parent a9ec8666f0
commit aa8bf2668f
2 changed files with 13 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/smt/smt_case_split_queue.cpp
View file

@ -42,18 +42,23 @@ namespace smt {
struct theory_aware_act_lt {
svector<double> const & m_activity;
theory_var_priority_map const & m_theory_var_priority;
theory_aware_act_lt(svector<double> const & act, theory_var_priority_map const & a):m_activity(act),m_theory_var_priority(a) {}
double const & m_bvar_inc;
theory_aware_act_lt(svector<double> const & act,
theory_var_priority_map const & a,
double const & bvar_inc):m_activity(act),m_theory_var_priority(a),m_bvar_inc(bvar_inc) {}
bool operator()(bool_var v1, bool_var v2) const {
double p_v1, p_v2;
if (!m_theory_var_priority.find(v1, p_v1)) {
p_v1 = 0.0;
}
p_v1 = 0.0;
}
p_v1 *= m_bvar_inc;
if (!m_theory_var_priority.find(v2, p_v2)) {
p_v2 = 0.0;
}
// add clause activity
p_v1 += m_activity[v1];
p_v2 += m_activity[v2];
p_v2 *= m_bvar_inc;
// add clause activity
p_v1 += m_activity[v1];
p_v2 += m_activity[v2];
return p_v1 > p_v2;
}
};
@ -1239,7 +1244,7 @@ namespace smt {
m_context(ctx),
m_params(p),
m_theory_var_priority(),
m_queue(1024, theory_aware_act_lt(ctx.get_activity_vector(), m_theory_var_priority)) {
m_queue(1024, theory_aware_act_lt(ctx.get_activity_vector(), m_theory_var_priority, ctx.get_bvar_inc())) {
}
virtual void activity_increased_eh(bool_var v) {

1
src/smt/smt_context.h
View file

@ -824,6 +824,7 @@ namespace smt {
* or some other axiom that means at least one of them must be assigned 'true'.
*/
void mk_th_case_split(unsigned num_lits, literal * lits);
double get_bvar_inc() const { return m_bvar_inc; }
/*
* Provide a hint to the branching heuristic about the priority of a "theory-aware literal".