mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 23:03:41 +00:00
Code Activity

minor changes

Browse source
This commit is contained in:
Jakob Rath 2024-02-08 15:25:00 +01:00
parent 705203ea4c
commit 3eb42cdf4b
6 changed files with 8 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/polysat/constraints.cpp
View file

@ -1,4 +1,4 @@
/*++ /*++
Copyright (c) 2021 Microsoft Corporation Copyright (c) 2021 Microsoft Corporation
Module Name: Module Name:
@ -131,7 +131,7 @@ namespace polysat {
if (l.lo().val() == 0) if (l.lo().val() == 0)
val = 0; val = 0;
else else
val = l.manager().max_value() + 1 - l.lo().val(); val = l.manager().two_to_N() - l.lo().val();
return true; return true;
} }

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

@ -146,7 +146,7 @@ namespace polysat {
/* /*
* Add a named clause. Dependencies are assumed, signed constraints are guaranteeed. * Add a named clause. Dependencies are assumed, signed constraints are guaranteed.
* In other words, the clause represents the formula /\ d_i -> \/ sc_j * In other words, the clause represents the formula /\ d_i -> \/ sc_j
* Where d_i are logical interpretations of dependencies and sc_j are signed constraints. * Where d_i are logical interpretations of dependencies and sc_j are signed constraints.
*/ */

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

@ -175,7 +175,6 @@ namespace polysat {
// 3. now the reference returned from lhs.offset() may be invalid // 3. now the reference returned from lhs.offset() may be invalid
pdd const rhs_plus_one = rhs + 1; pdd const rhs_plus_one = rhs + 1;
// TODO: potential bug here: first call offset(), then rhs+1 has to reallocate pdd_manager::m_values, then the reference to offset is broken.
if (rhs.is_val() && !rhs.is_zero() && lhs.offset() == rhs_plus_one.val()) { if (rhs.is_val() && !rhs.is_zero() && lhs.offset() == rhs_plus_one.val()) {
TRACE("bv", tout << "p - k <= -k - 1 --> k <= p\n"); TRACE("bv", tout << "p - k <= -k - 1 --> k <= p\n");
pdd k = -(rhs + 1); pdd k = -(rhs + 1);

4
src/sat/smt/polysat_model.cpp
View file

@ -89,9 +89,9 @@ namespace polysat {
} }
std::ostream& solver::display(std::ostream& out) const { std::ostream& solver::display(std::ostream& out) const {
for (unsigned v = 0; v < get_num_vars(); ++v) for (theory_var v = 0; v < get_num_vars(); ++v)
if (m_var2pdd_valid.get(v, false)) if (m_var2pdd_valid.get(v, false))
out << ctx.bpp(var2enode(v)) << " := " << m_var2pdd[v] << "\n"; out << "tv" << v << " is " << ctx.bpp(var2enode(v)) << " := " << m_var2pdd[v] << "\n";
m_core.display(out); m_core.display(out);
m_intblast.display(out); m_intblast.display(out);
return out; return out;

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

@ -495,16 +495,16 @@ namespace polysat {
expr_ref_vector args(m); expr_ref_vector args(m);
for (auto const& mon : p) { for (auto const& mon : p) {
auto c = mon.coeff; rational const& c = mon.coeff;
if (mon.vars.empty()) if (mon.vars.empty())
args.push_back(mk_num(c)); args.push_back(mk_num(c));
else if (mon.coeff == 1 && mon.vars.size() == 1) else if (c == 1 && mon.vars.size() == 1)
args.push_back(mk_var(mon.vars[0])); args.push_back(mk_var(mon.vars[0]));
else if (mon.vars.size() == 1) else if (mon.vars.size() == 1)
args.push_back(bv.mk_bv_mul(mk_num(c), mk_var(mon.vars[0]))); args.push_back(bv.mk_bv_mul(mk_num(c), mk_var(mon.vars[0])));
else { else {
expr_ref_vector args2(m); expr_ref_vector args2(m);
for (auto v : mon.vars) for (pvar v : mon.vars)
args2.push_back(mk_var(v)); args2.push_back(mk_var(v));
if (c == 1) if (c == 1)
args.push_back(bv.mk_bv_mul(args2)); args.push_back(bv.mk_bv_mul(args2));

2
src/sat/smt/sat_th.h
View file

@ -177,8 +177,6 @@ namespace euf {
void add_equiv(sat::literal a, sat::literal b); void add_equiv(sat::literal a, sat::literal b);
void add_equiv_and(sat::literal a, sat::literal_vector const& bs); void add_equiv_and(sat::literal a, sat::literal_vector const& bs);
bool add_redundant(sat::literal_vector const& lits, th_proof_hint const* ps) { return add_clause(lits.size(), lits.data(), ps, true); } bool add_redundant(sat::literal_vector const& lits, th_proof_hint const* ps) { return add_clause(lits.size(), lits.data(), ps, true); }
bool add_redundant(unsigned n, sat::literal* lits, th_proof_hint const* ps);
bool is_true(sat::literal lit); bool is_true(sat::literal lit);
bool is_true(sat::literal a, sat::literal b) { return is_true(a) || is_true(b); } bool is_true(sat::literal a, sat::literal b) { return is_true(a) || is_true(b); }