mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

updated encodings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-12-22 17:45:21 -08:00
parent f52baf1e17
commit a444a33c30
3 changed files with 89 additions and 58 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/parsers/smt2/smt2parser.cpp
View file

@ -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);

115
src/smt/theory_pb.cpp
View file

@ -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<unsigned>(v)) {
m_var_infos.resize(static_cast<unsigned>(v)+100);
}
}
void theory_pb::watch_literal(literal lit, ineq* c) {
ptr_vector<ineq>* ineqs;
if (!m_lwatch.find(lit.index(), ineqs)) {
init_watch(lit.var());
ptr_vector<ineq>* ineqs = m_var_infos[lit.var()].m_lit_watch[lit.sign()];
if (ineqs == 0) {
ineqs = alloc(ptr_vector<ineq>);
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<ineq>* ineqs;
if (!m_vwatch.find(v, ineqs)) {
init_watch(v);
ptr_vector<ineq>* ineqs = m_var_infos[v].m_var_watch;
if (ineqs == 0) {
ineqs = alloc(ptr_vector<ineq>);
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<ineq>* ineqs = 0;
if (m_vwatch.find(v, ineqs)) {
ptr_vector<ineq>* ineqs = m_var_infos[v].m_var_watch;
if (ineqs) {
remove(*ineqs, c);
}
}
void theory_pb::unwatch_literal(literal w, ineq* c) {
ptr_vector<ineq>* ineqs = 0;
if (m_lwatch.find(w.index(), ineqs)) {
remove(*ineqs, c);
void theory_pb::unwatch_literal(literal lit, ineq* c) {
ptr_vector<ineq>* 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<ptr_vector<ineq>*>::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<ineq*>::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<ineq>* 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<ineq*>::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<ptr_vector<ineq>*>::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<ineq*>::iterator itc = m_ineqs.begin(), endc = m_ineqs.end();
for (; itc != endc; ++itc) {
ineq& c = *itc->m_value;
display(out, c, true);
}
}

30
src/smt/theory_pb.h
View file

@ -193,10 +193,32 @@ namespace smt {
typedef ptr_vector<ineq> watch_list;
typedef map<arg_t, bool_var, arg_t::hash, arg_t::eq> 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<watch_list*> m_lwatch; // per literal.
u_map<watch_list*> m_vwatch; // per variable.
u_map<ineq*> m_ineqs; // per inequality.
svector<var_info> m_var_infos;
// u_map<watch_list*> m_lwatch; // per literal.
// u_map<watch_list*> m_vwatch; // per variable.
// u_map<ineq*> m_ineqs; // per inequality.
arg_map m_ineq_rep; // Simplex: representative inequality
u_map<row_info> 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);