mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

bugfixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-02 08:23:28 -08:00
parent f70f1bb85c
commit c467f093d0
6 changed files with 45 additions and 71 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/sat/smt/polysat/core.cpp
View file

@ -201,6 +201,9 @@ namespace polysat {
sat::check_result core::check() {
lbool r = l_true;
if (propagate())
return sat::check_result::CR_CONTINUE;
switch (assign_variable()) {
case l_true:
break;
@ -462,10 +465,21 @@ namespace polysat {
c.m_prop_queue.pop_back();
}
};
if (m_constraint_index[index.id].value != l_undef)
auto& value = m_constraint_index[index.id].value;
TRACE("bv", tout << "assignment " << index.id << " " << m_constraint_index[index.id].sc << " := " << value << " sign: " << sign << "\n");
if (value != l_undef &&
((value == l_false && !sign) || (value == l_true && sign))) {
TRACE("bv", display(tout << "index " << m_constraint_index[index.id].d << " " << m_constraint_index[index.id].sc << "\n"));
}
SASSERT(value == l_undef || (value == l_false && sign) || (value == l_true && !sign));
if (value != l_undef)
return;
m_prop_queue.push_back(index);
m_constraint_index[index.id].value = to_lbool(!sign);
value = to_lbool(!sign);
s.trail().push(unassign(*this, index.id));
}

45
src/sat/smt/polysat/monomials.cpp
View file

@ -20,10 +20,7 @@ namespace polysat {
monomials::monomials(core& c):
c(c),
C(c.cs()),
m_hash(*this),
m_eq(*this),
m_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, m_hash, m_eq)
C(c.cs())
{}
pvar monomials::mk(unsigned n, pdd const* args) {
@ -31,40 +28,20 @@ namespace polysat {
auto& m = args[0].manager();
unsigned sz = m.power_of_2();
m_tmp.reset();
for (unsigned i = 0; i < n; ++i)
pdd def = c.value(rational(1), sz);
for (unsigned i = 0; i < n; ++i) {
m_tmp.push_back(args[i]);
std::stable_sort(m_tmp.begin(), m_tmp.end(),
[&](pdd const& a, pdd const& b) { return a.index() < b.index(); });
pdd offset = c.value(rational(0), sz);
unsigned index = m_monomials.size();
m_monomials.push_back({m_tmp, offset, offset, {}, rational(0) });
unsigned j;
if (m_table.find(index, j)) {
m_monomials.pop_back();
return m_monomials[j].var.var();
def *= args[i];
}
struct del_monomial : public trail {
monomials& m;
del_monomial(monomials& m):m(m) {}
void undo() override {
unsigned index = m.m_monomials.size()-1;
m.m_table.erase(index);
m.m_monomials.pop_back();
}
};
pdd var = c.var(c.add_var(sz));
m_monomials.push_back({m_tmp, var, def, {}, rational(0) });
auto & mon = m_monomials.back();
mon.var = c.var(c.add_var(sz));
mon.def = c.value(rational(1), sz);
for (auto p : m_tmp) {
for (auto p : m_tmp)
mon.arg_vals.push_back(rational(0));
mon.def *= p;
}
m_table.insert(index);
c.trail().push(del_monomial(*this));
c.trail().push(push_back_vector(m_monomials));
return mon.var.var();
}
@ -175,7 +152,7 @@ namespace polysat {
free_index = j;
}
constraint_or_dependency_vector cs;
pdd offset = c.value(rational(1), m.power_of_2());
pdd offset = c.value(rational(1), mon.num_bits());
for (unsigned j = mon.size(); j-- > 0; ) {
if (j != free_index) {
cs.push_back(~C.eq(mon.args[j], mon.arg_vals[j]));

25
src/sat/smt/polysat/monomials.h
View file

@ -40,31 +40,6 @@ namespace polysat {
vector<monomial> m_monomials;
pdd_vector m_tmp;
struct mon_eq {
monomials& m;
mon_eq(monomials& m):m(m) {}
bool operator()(unsigned i, unsigned j) const {
auto const& a = m.m_monomials[i].args;
auto const& b = m.m_monomials[j].args;
return a == b;
};
};
struct pdd_hash {
typedef pdd data_t;
unsigned operator()(pdd const& p) const { return p.hash(); }
};
struct mon_hash {
monomials& m;
mon_hash(monomials& m):m(m) {}
unsigned operator()(unsigned i) const {
auto const& a = m.m_monomials[i].args;
return vector_hash<pdd_hash>()(a);
}
};
mon_hash m_hash;
mon_eq m_eq;
hashtable<unsigned, mon_hash, mon_eq> m_table;
unsigned_vector m_to_refine;
void init_to_refine();

19
src/sat/smt/polysat_internalize.cpp
View file

@ -803,16 +803,23 @@ namespace polysat {
}
};
constraint_id solver::eq_constraint(pdd p, pdd q, dependency d) {
constraint_id solver::eq_constraint(pdd p, pdd q, bool sign, dependency d) {
pdd r = p - q;
constraint_id idx;
if (m_eq2constraint.find(r.index(), idx))
return idx;
std::pair<constraint_id, bool> elem;
bool is_new = true;
if (m_eq2constraint.find(r.index(), elem)) {
if (elem.second == sign)
return elem.first;
is_new = false;
}
auto sc = m_core.eq(p, q);
idx = m_core.register_constraint(sc, d);
m_eq2constraint.insert(r.index(), idx);
m_eqs.push_back(r);
ctx.push(undo_add_eq(*this, r.index()));
if (is_new) {
m_eq2constraint.insert(r.index(), { idx, sign });
m_eqs.push_back(r);
ctx.push(undo_add_eq(*this, r.index()));
}
return idx;
}

5
src/sat/smt/polysat_solver.cpp
View file

@ -217,8 +217,9 @@ namespace polysat {
m_var_eqs_head++;
pdd p = var2pdd(v1);
pdd q = var2pdd(v2);
TRACE("bv", tout << ctx.bpp(n) << " == " << ctx.bpp(var2enode(v2)) << "\n");
auto d = dependency(v1, v2);
constraint_id id = eq_constraint(p, q, d);
constraint_id id = eq_constraint(p, q, false, d);
m_core.assign_eh(id, false);
}
@ -232,7 +233,7 @@ namespace polysat {
pdd q = var2pdd(v2);
sat::literal eq = expr2literal(ne.eq());
auto d = dependency(eq.var());
auto id = eq_constraint(p, q, d);
auto id = eq_constraint(p, q, true, d);
TRACE("bv", tout << eq << " := " << s().value(eq) << " @" << s().scope_lvl() << "\n");
m_core.assign_eh(id, true);
}

4
src/sat/smt/polysat_solver.h
View file

@ -199,9 +199,9 @@ namespace polysat {
void quot_rem(expr* quot, expr* rem, expr* x, expr* y);
vector<pdd> m_eqs;
u_map<constraint_id> m_eq2constraint;
u_map<std::pair<constraint_id, bool>> m_eq2constraint;
struct undo_add_eq;
constraint_id eq_constraint(pdd p, pdd q, dependency d);
constraint_id eq_constraint(pdd p, pdd q, bool sign, dependency d);
// callbacks from core
lbool add_eq_literal(pvar v, rational const& val, dependency& d) override;