mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 04:43:39 +00:00
Code Activity

refactor: remove commented-out code

Browse source
This commit is contained in:
Murphy Berzish 2017-02-23 15:08:05 -05:00
parent 858c754b15
commit 6387d59f5c
1 changed files with 0 additions and 113 deletions
Download patch file Download diff file Expand all files Collapse all files

113
src/smt/smt_case_split_queue.cpp
View file

@ -1112,119 +1112,6 @@ namespace smt {
} }
}; };
/*
class theory_aware_branching_queue : public case_split_queue {
protected:
context & m_context;
smt_params & m_params;
theory_var_priority_map m_theory_var_priority;
theory_aware_act_queue m_theory_queue;
case_split_queue * m_base_queue;
int_hashtable<int_hash, default_eq<bool_var> > m_theory_vars;
map<bool_var, lbool, int_hash, default_eq<bool_var> > m_theory_var_phase;
public:
theory_aware_branching_queue(context & ctx, smt_params & p, case_split_queue * base_queue) :
m_context(ctx),
m_params(p),
m_theory_var_priority(),
m_theory_queue(1024, theory_aware_act_lt(m_theory_var_priority)),
m_base_queue(base_queue) {
}
virtual void activity_increased_eh(bool_var v) {
m_base_queue->activity_increased_eh(v);
}
virtual void mk_var_eh(bool_var v) {
// do nothing. we only "react" if/when we learn this is an important theory literal
m_base_queue->mk_var_eh(v);
}
virtual void del_var_eh(bool_var v) {
if (m_theory_queue.contains(v)) {
m_theory_queue.erase(v);
}
m_base_queue->del_var_eh(v);
}
virtual void assign_lit_eh(literal l) {
m_base_queue->assign_lit_eh(l);
}
virtual void unassign_var_eh(bool_var v) {
if (m_theory_vars.contains(v) && !m_theory_queue.contains(v)) {
m_theory_queue.insert(v);
}
m_base_queue->unassign_var_eh(v);
}
virtual void relevant_eh(expr * n) {
m_base_queue->relevant_eh(n);
}
virtual void init_search_eh() {
m_base_queue->init_search_eh();
}
virtual void end_search_eh() {
m_base_queue->end_search_eh();
}
virtual void internalize_instance_eh(expr * e, unsigned gen) {
m_base_queue->internalize_instance_eh(e, gen);
}
virtual void reset() {
m_theory_queue.reset();
m_theory_vars.reset();
m_theory_var_phase.reset();
m_theory_var_priority.reset();
m_base_queue->reset();
}
virtual void push_scope() {
m_base_queue->push_scope();
}
virtual void pop_scope(unsigned num_scopes) {
m_base_queue->pop_scope(num_scopes);
}
virtual void next_case_split(bool_var & next, lbool & phase) {
while (!m_theory_queue.empty()) {
next = m_theory_queue.erase_min();
// if this literal is unassigned, it is the theory literal with the highest priority,
// so case split on this
if (m_context.get_assignment(next) == l_undef) {
TRACE("theory_aware_branching", tout << "Theory-aware branch on l#" << next << std::endl;);
if (!m_theory_var_phase.find(next, phase)) {
phase = l_undef;
}
return;
}
}
// if we reach this point, the theory literal queue is empty,
// so fall back to the base queue
m_base_queue->next_case_split(next, phase);
}
virtual void add_theory_aware_branching_info(bool_var v, double priority, lbool phase) {
TRACE("theory_aware_branching", tout << "Add theory-aware branching information for l#" << v << ": priority=" << priority << std::endl;);
m_theory_vars.insert(v);
m_theory_var_phase.insert(v, phase);
m_theory_var_priority.insert(v, priority);
m_theory_queue.reserve(v+1);
m_theory_queue.insert(v);
}
virtual void display(std::ostream & out) {
// TODO
m_base_queue->display(out);
}
};
*/
class theory_aware_branching_queue : public case_split_queue { class theory_aware_branching_queue : public case_split_queue {
protected: protected:
context & m_context; context & m_context;