diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 00f63afd5..bb0c5bfb9 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -2183,7 +2183,7 @@ namespace smt2 { SASSERT(curr_id() == m_check_sat_assuming); next(); unsigned spos = expr_stack().size(); - check_rparen_next("invalid check-sat-assuming command, '(', expected"); + check_lparen_next("invalid check-sat-assuming command, '(', expected"); parse_assumptions(); check_rparen_next("invalid check-sat-assuming command, ')', expected"); m_ctx.check_sat(expr_stack().size() - spos, expr_stack().c_ptr() + spos); diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index a2f8ceba9..68553453d 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -527,7 +527,8 @@ namespace smt { c->m_compilation_threshold = UINT_MAX; } init_watch_var(*c); - m_ineqs.insert(abv, c); + init_watch(abv); + m_var_infos[abv].m_ineq = c; m_ineqs_trail.push_back(abv); if (m_enable_simplex) { @@ -687,35 +688,43 @@ namespace smt { watch_literal(lit, &c); } + void theory_pb::init_watch(bool_var v) { + if (m_var_infos.size() <= static_cast(v)) { + m_var_infos.resize(static_cast(v)+100); + } + } + void theory_pb::watch_literal(literal lit, ineq* c) { - ptr_vector* ineqs; - if (!m_lwatch.find(lit.index(), ineqs)) { + init_watch(lit.var()); + ptr_vector* ineqs = m_var_infos[lit.var()].m_lit_watch[lit.sign()]; + if (ineqs == 0) { ineqs = alloc(ptr_vector); - m_lwatch.insert(lit.index(), ineqs); + m_var_infos[lit.var()].m_lit_watch[lit.sign()] = ineqs; } ineqs->push_back(c); } void theory_pb::watch_var(bool_var v, ineq* c) { - ptr_vector* ineqs; - if (!m_vwatch.find(v, ineqs)) { + init_watch(v); + ptr_vector* ineqs = m_var_infos[v].m_var_watch; + if (ineqs == 0) { ineqs = alloc(ptr_vector); - m_vwatch.insert(v, ineqs); + m_var_infos[v].m_var_watch = ineqs; } ineqs->push_back(c); } void theory_pb::unwatch_var(bool_var v, ineq* c) { - ptr_vector* ineqs = 0; - if (m_vwatch.find(v, ineqs)) { + ptr_vector* ineqs = m_var_infos[v].m_var_watch; + if (ineqs) { remove(*ineqs, c); } } - void theory_pb::unwatch_literal(literal w, ineq* c) { - ptr_vector* ineqs = 0; - if (m_lwatch.find(w.index(), ineqs)) { - remove(*ineqs, c); + void theory_pb::unwatch_literal(literal lit, ineq* c) { + ptr_vector* ineqs = m_var_infos[lit.var()].m_lit_watch[lit.sign()]; + if (ineqs) { + remove(*ineqs, c); } } @@ -741,22 +750,9 @@ namespace smt { void theory_pb::reset_eh() { - // m_watch; - u_map*>::iterator it = m_lwatch.begin(), end = m_lwatch.end(); - for (; it != end; ++it) { - dealloc(it->m_value); + for (unsigned i = 0; i < m_var_infos.size(); ++i) { + m_var_infos[i].reset(); } - it = m_vwatch.begin(), end = m_vwatch.end(); - for (; it != end; ++it) { - dealloc(it->m_value); - } - u_map::iterator itc = m_ineqs.begin(), endc = m_ineqs.end(); - for (; itc != endc; ++itc) { - dealloc(itc->m_value); - } - m_lwatch.reset(); - m_vwatch.reset(); - m_ineqs.reset(); m_ineqs_trail.reset(); m_ineqs_lim.reset(); m_stats.reset(); @@ -777,7 +773,8 @@ namespace smt { ptr_vector* ineqs = 0; literal nlit(v, is_true); TRACE("pb", tout << "assign: " << ~nlit << "\n";); - if (m_lwatch.find(nlit.index(), ineqs)) { + ineqs = m_var_infos[v].m_lit_watch[nlit.sign()]; + if (ineqs != 0) { if (m_enable_simplex) { mpq_inf num(mpq(is_true?1:0),mpq(0)); if (!update_bound(v, ~nlit, is_true, num)) { @@ -797,14 +794,15 @@ namespace smt { } } } - if (m_vwatch.find(v, ineqs)) { + ineqs = m_var_infos[v].m_var_watch; + if (ineqs != 0) { for (unsigned i = 0; i < ineqs->size(); ++i) { ineq* c = (*ineqs)[i]; assign_watch(v, is_true, *c); } } - ineq* c = 0; - if (m_ineqs.find(v, c)) { + ineq* c = m_var_infos[v].m_ineq; + if (c != 0) { if (m_enable_simplex) { row_info const& info = m_ineq_row_info.find(v); scoped_eps_numeral coeff(m_mpq_inf_mgr); @@ -1317,10 +1315,9 @@ namespace smt { unsigned sz = m_ineqs_lim[new_lim]; while (m_ineqs_trail.size() > sz) { bool_var v = m_ineqs_trail.back(); - ineq* c = 0; - VERIFY(m_ineqs.find(v, c)); + ineq* c = m_var_infos[v].m_ineq; clear_watch(*c); - m_ineqs.remove(v); + m_var_infos[v].m_ineq = 0; m_ineqs_trail.pop_back(); if (m_enable_simplex) { row_info r_info; @@ -1866,9 +1863,11 @@ namespace smt { } void theory_pb::validate_final_check() { - u_map::iterator itc = m_ineqs.begin(), endc = m_ineqs.end(); - for (; itc != endc; ++itc) { - validate_final_check(*itc->m_value); + for (unsigned i = 0; i < m_var_infos.size(); ++i) { + ineq* c = m_var_infos[i].m_ineq; + if (c) { + validate_final_check(*c); + } } } @@ -2076,29 +2075,37 @@ namespace smt { return p; } + void theory_pb::display_watch(std::ostream& out, bool_var v, bool sign) const { + watch_list const* w = m_var_infos[v].m_lit_watch[sign]; + if (!w) return; + watch_list const& wl = *w; + out << "watch: " << literal(v, sign) << " |-> "; + for (unsigned i = 0; i < wl.size(); ++i) { + out << wl[i]->lit() << " "; + } + out << "\n"; + } + void theory_pb::display(std::ostream& out) const { - u_map*>::iterator it = m_lwatch.begin(), end = m_lwatch.end(); - for (; it != end; ++it) { - out << "watch: " << to_literal(it->m_key) << " |-> "; - watch_list const& wl = *it->m_value; + for (unsigned vi = 0; vi < m_var_infos.size(); ++vi) { + display_watch(out, vi, false); + display_watch(out, vi, true); + } + for (unsigned vi = 0; vi < m_var_infos.size(); ++vi) { + watch_list const* w = m_var_infos[vi].m_var_watch; + if (!w) continue; + out << "watch (v): " << literal(vi) << " |-> "; + watch_list const& wl = *w; for (unsigned i = 0; i < wl.size(); ++i) { out << wl[i]->lit() << " "; } out << "\n"; } - it = m_vwatch.begin(), end = m_vwatch.end(); - for (; it != end; ++it) { - out << "watch (v): " << literal(it->m_key) << " |-> "; - watch_list const& wl = *it->m_value; - for (unsigned i = 0; i < wl.size(); ++i) { - out << wl[i]->lit() << " "; + for (unsigned vi = 0; vi < m_var_infos.size(); ++vi) { + ineq* c = m_var_infos[vi].m_ineq; + if (c) { + display(out, *c, true); } - out << "\n"; - } - u_map::iterator itc = m_ineqs.begin(), endc = m_ineqs.end(); - for (; itc != endc; ++itc) { - ineq& c = *itc->m_value; - display(out, c, true); } } diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index 1a08b7b61..7f621f9c5 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -193,10 +193,32 @@ namespace smt { typedef ptr_vector watch_list; typedef map arg_map; + struct var_info { + watch_list* m_lit_watch[2]; + watch_list* m_var_watch; + ineq* m_ineq; + + var_info(): m_var_watch(0), m_ineq(0) + { + m_lit_watch[0] = 0; + m_lit_watch[1] = 0; + } + + void reset() { + dealloc(m_lit_watch[0]); + dealloc(m_lit_watch[1]); + dealloc(m_var_watch); + dealloc(m_ineq); + } + }; + + theory_pb_params m_params; - u_map m_lwatch; // per literal. - u_map m_vwatch; // per variable. - u_map m_ineqs; // per inequality. + + svector m_var_infos; +// u_map m_lwatch; // per literal. +// u_map m_vwatch; // per variable. +// u_map m_ineqs; // per inequality. arg_map m_ineq_rep; // Simplex: representative inequality u_map m_ineq_row_info; // Simplex: row information per variable uint_set m_vars; // Simplex: 0-1 variables. @@ -221,6 +243,7 @@ namespace smt { literal compile_arg(expr* arg); void add_watch(ineq& c, unsigned index); void del_watch(watch_list& watch, unsigned index, ineq& c, unsigned ineq_index); + void init_watch(bool_var v); void init_watch_literal(ineq& c); void init_watch_var(ineq& c); void clear_watch(ineq& c); @@ -242,6 +265,7 @@ namespace smt { std::ostream& display(std::ostream& out, ineq const& c, bool values = false) const; std::ostream& display(std::ostream& out, arg_t const& c, bool values = false) const; virtual void display(std::ostream& out) const; + void display_watch(std::ostream& out, bool_var v, bool sign) const; void display_resolved_lemma(std::ostream& out) const; void add_clause(ineq& c, literal_vector const& lits);