mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 20:33:38 +00:00
Code Activity

Revert "scale theory-aware priority by bvar_inc"

Browse source 
This reverts commit aa8bf2668f.
This commit is contained in:
Murphy Berzish 2017-01-16 15:46:28 -05:00
parent 4b6582b8f3
commit 4e2847dea4
2 changed files with 7 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/smt/smt_case_split_queue.cpp
View file

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

1
src/smt/smt_context.h
View file

@ -824,7 +824,6 @@ namespace smt {
* or some other axiom that means at least one of them must be assigned 'true'. * 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); 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". * Provide a hint to the branching heuristic about the priority of a "theory-aware literal".