mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-22 19:12:02 -07:00
parent 96f10b8c1c
commit 03276b12b1
2 changed files with 13 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/smt/arith_eq_adapter.cpp
View file

@ -253,13 +253,13 @@ namespace smt {
context & ctx = get_context();
TRACE("arith_eq_adapter", tout << "restart\n";);
enode_pair_vector tmp(m_restart_pairs);
enode_pair_vector::iterator it = tmp.begin();
enode_pair_vector::iterator end = tmp.end();
m_restart_pairs.reset();
for (; it != end && !ctx.inconsistent(); ++it) {
TRACE("arith_eq_adapter", tout << "creating arith_eq_adapter axioms at the base level #" << it->first->get_owner_id() << " #" <<
it->second->get_owner_id() << "\n";);
mk_axioms(it->first, it->second);
for (auto const& p : tmp) {
if (ctx.inconsistent())
break;
TRACE("arith_eq_adapter", tout << "creating arith_eq_adapter axioms at the base level #" << p.first->get_owner_id() << " #" <<
p.second->get_owner_id() << "\n";);
mk_axioms(p.first, p.second);
}
}
@ -268,11 +268,9 @@ namespace smt {
}
void arith_eq_adapter::display_already_processed(std::ostream & out) const {
obj_pair_map<enode, enode, data>::iterator it = m_already_processed.begin();
obj_pair_map<enode, enode, data>::iterator end = m_already_processed.end();
for (; it != end; ++it) {
enode * n1 = it->get_key1();
enode * n2 = it->get_key2();
for (auto const& d : m_already_processed) {
enode * n1 = d.get_key1();
enode * n2 = d.get_key2();
out << "eq_adapter: #" << n1->get_owner_id() << " #" << n2->get_owner_id() << "\n";
}
}

8
src/smt/smt_solver.cpp
View file

@ -209,10 +209,10 @@ namespace {
}
void user_propagate_init(
void* ctx,
std::function<void(void*)>& push_eh,
std::function<void(void*, unsigned)>& pop_eh,
solver::fresh_eh_t& fresh_eh) override {
void* ctx,
solver::push_eh_t& push_eh,
solver::pop_eh_t& pop_eh,
solver::fresh_eh_t& fresh_eh) override {
m_context.user_propagate_init(ctx, push_eh, pop_eh, fresh_eh);
}