mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

bug fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-01 16:24:15 -08:00
parent 7dea0b855b
commit d91820fe51
12 changed files with 48 additions and 41 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -217,6 +217,7 @@ namespace polysat {
case l_true:
break;
case l_false:
TRACE("bv", tout << "refine\n");
return sat::check_result::CR_CONTINUE;
case l_undef:
r = l_undef;
@ -228,6 +229,7 @@ namespace polysat {
case l_true:
break;
case l_false:
TRACE("bv", tout << "saturate\n");
return sat::check_result::CR_CONTINUE;
case l_undef:
r = l_undef;
@ -238,6 +240,7 @@ namespace polysat {
case l_true:
break;
case l_false:
TRACE("bv", tout << "blast\n");
return sat::check_result::CR_CONTINUE;
case l_undef:
r = l_undef;

2
src/sat/smt/polysat/core.h
View file

@ -130,7 +130,7 @@ namespace polysat {
void band(pdd const& a, pdd const& b, pdd const& r) { add_opdef(m_constraints.band(a, b, r)); }
pdd bnot(pdd p) { return -p - 1; }
pdd mul(unsigned n, pdd const* args) { return m_monomials.mk(n, args); }
pvar mul(unsigned n, pdd const* args) { return m_monomials.mk(n, args); }
/*

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

@ -26,40 +26,24 @@ namespace polysat {
m_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, m_hash, m_eq)
{}
pdd monomials::mk(unsigned n, pdd const* args) {
SASSERT(n > 0);
if (n == 1)
return args[0];
if (n == 2 && args[0].is_val())
return args[0]*args[1];
if (n == 2 && args[1].is_val())
return args[0]*args[1];
pvar monomials::mk(unsigned n, pdd const* args) {
SASSERT(n > 1);
auto& m = args[0].manager();
unsigned sz = m.power_of_2();
m_tmp.reset();
pdd offset = c.value(rational(1), sz);
for (unsigned i = 0; i < n; ++i) {
pdd const& p = args[i];
if (p.is_val())
offset *= p;
else
m_tmp.push_back(p);
}
if (m_tmp.empty())
return offset;
if (m_tmp.size() == 1)
return offset * m_tmp[0];
std::stable_sort(m_tmp.begin(), m_tmp.end(),
[&](pdd const& a, pdd const& b) { return a.index() < b.index(); });
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 offset * m_monomials[j].var;
return m_monomials[j].var.var();
}
struct del_monomial : public trail {
@ -73,7 +57,7 @@ namespace polysat {
};
auto & mon = m_monomials.back();
mon.var = c.add_var(sz);
mon.var = c.var(c.add_var(sz));
mon.def = c.value(rational(1), sz);
for (auto p : m_tmp) {
mon.arg_vals.push_back(rational(0));
@ -81,13 +65,15 @@ namespace polysat {
}
m_table.insert(index);
c.trail().push(del_monomial(*this));
return offset * mon.var;
return mon.var.var();
}
pdd monomials::subst(pdd const& p) {
pdd r = p;
for (unsigned i = m_monomials.size(); i-- > 0;)
r = r.subst_pdd(m_monomials[i].var.var(), m_monomials[i].def);
for (unsigned i = m_monomials.size(); i-- > 0;) {
if (&r.manager() == &m_monomials[i].var.manager())
r = r.subst_pdd(m_monomials[i].var.var(), m_monomials[i].def);
}
return r;
}
@ -201,8 +187,7 @@ namespace polysat {
else
cs.push_back(C.eq(mon.var, offset * mon.args[free_index]));
c.add_axiom("p = k => p * q = k * q", cs, true);
return true;
return c.add_axiom("p = k => p * q = k * q", cs, true);
}
// parity p >= i => parity p * q >= i

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

@ -87,7 +87,7 @@ namespace polysat {
monomials(core& c);
pdd mk(unsigned n, pdd const* args);
pvar mk(unsigned n, pdd const* args);
pdd subst(pdd const& p);

2
src/sat/smt/polysat/ule_constraint.cpp
View file

@ -319,7 +319,7 @@ namespace polysat {
std::ostream& ule_constraint::display(std::ostream& out) const {
display(out, l_true, m_lhs, m_rhs);
if (m_lhs != m_unfold_lhs || m_rhs != m_unfold_rhs)
display(out << " alias ( ", l_true, m_unfold_lhs, m_unfold_rhs) << ")";
display(out << " alias (", l_true, m_unfold_lhs, m_unfold_rhs) << ")";
return out;
}

2
src/sat/smt/polysat/ule_constraint.h
View file

@ -40,7 +40,7 @@ namespace polysat {
lbool eval() const override;
lbool eval(assignment const& a) const override;
lbool eval_unfold(assignment const& a) const override;
bool is_linear() const override { return lhs().is_linear() && rhs().is_linear(); }
bool is_linear() const override { return lhs().is_linear_or_value() && rhs().is_linear_or_value(); }
void activate(core& c, bool sign, dependency const& dep);
void propagate(core& c, lbool value, dependency const& dep) {}
bool is_eq() const { return m_rhs.is_zero(); }

2
src/sat/smt/polysat/umul_ovfl_constraint.h
View file

@ -38,7 +38,7 @@ namespace polysat {
lbool eval(assignment const& a) const override;
void activate(core& c, bool sign, dependency const& dep) override;
void propagate(core& c, lbool value, dependency const& dep) override;
bool is_linear() const override { return p().is_linear() && q().is_linear(); }
bool is_linear() const override { return p().is_linear_or_value() && q().is_linear_or_value(); }
};

5
src/sat/smt/polysat/viable.cpp
View file

@ -550,9 +550,8 @@ namespace polysat {
if (value == l_false)
sc = ~sc;
if (!sc.is_linear()) {
return true;
}
if (!sc.is_linear())
return true;
entry* ne = alloc_entry(v, idx);
if (!m_forbidden_intervals.get_interval(sc, v, *ne)) {

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

@ -608,7 +608,21 @@ namespace polysat {
vector<dd::pdd> args;
for (expr* arg : *to_app(a))
args.push_back(expr2pdd(arg));
internalize_set(a, m_core.mul(args.size(), args.data()));
if (args.size() == 1) {
internalize_set(a, args[0]);
return;
}
if (args.size() == 2 && args[0].is_val()) {
internalize_set(a, args[0] * args[1]);
return;
}
if (args.size() == 2 && args[1].is_val()) {
internalize_set(a, args[0] * args[1]);
return;
}
auto pv = m_core.mul(args.size(), args.data());
m_pddvar2var.setx(pv, get_th_var(a), UINT_MAX);
internalize_set(a, m_core.var(pv));
}
// TODO - test that internalize works with recursive call on bit2bool

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

@ -74,7 +74,8 @@ namespace polysat {
case sat::check_result::CR_CONTINUE:
return sat::check_result::CR_CONTINUE;
case sat::check_result::CR_GIVEUP:
return intblast();
return sat::check_result::CR_GIVEUP;
// return intblast();
}
UNREACHABLE();
return sat::check_result::CR_GIVEUP;
@ -315,6 +316,7 @@ namespace polysat {
}
bool solver::add_axiom(char const* name, constraint_or_dependency const* begin, constraint_or_dependency const* end, bool is_redundant) {
TRACE("bv", tout << "add " << name << "\n");
sat::literal_vector lits;
euf::enode_pair_vector eqs;
for (auto it = begin; it != end; ++it) {
@ -335,8 +337,10 @@ namespace polysat {
for (auto& lit : lits)
lit.neg();
for (auto lit : lits)
if (s().value(lit) == l_true)
if (s().value(lit) == l_true) {
TRACE("bv", tout << "literal is true " << ctx.literal2expr(lit) << "\n");
return false;
}
validate_axiom(lits);
s().add_clause(lits.size(), lits.data(), sat::status::th(is_redundant, get_id(), hint));
return true;