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

start make_asserting for non-unit coeff

Browse source
This commit is contained in:
Jakob Rath 2022-08-19 17:06:28 +02:00
parent ee208efdc5
commit 3e99828c3c
4 changed files with 66 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

49
src/math/polysat/solver.cpp
View file

@ -1253,12 +1253,57 @@ namespace polysat {
auto c_new = ule(intersection.hi() - intersection.lo(), z - intersection.lo());
out_lits.push_back(c_new.blit());
}
return;
} else {
out_lits.shrink(out_lits_original_size);
// TODO: SAT-based approach
find_implied_constraint_sat(cz, z, z_val, out_lits);
}
}
void solver::find_implied_constraint_sat(signed_constraints const& cz, pvar z, rational z_val, sat::literal_vector& out_lits)
{
unsigned bit_width = size(z);
auto p_factory = mk_univariate_bitblast_factory();
auto p_us = (*p_factory)(bit_width);
auto& us = *p_us;
// Find max z1 such that z1 < z_val and all cz true under z := z1 (and current assignment)
rational z1 = z_val;
for (signed_constraint const& c : cz)
c.add_to_univariate_solver(*this, us, 0);
us.add_ult_const(z_val, false, 0); // z1 < z_val
// First check if any such z1 exists
switch (us.check()) {
case l_false:
// No such z1 exists
z1 = m_pdd[z]->max_value(); // -1
break;
case l_true:
// z1 exists. Try to make it as small as possible by setting bits to 0
for (unsigned j = bit_width; j-- > 0; ) {
switch (us.check()) {
case l_true:
// TODO
break;
case l_false:
// TODO
break;
default:
UNREACHABLE(); // TODO: see below
}
}
break;
default:
UNREACHABLE(); // TODO: should we link the child solver's resources to polysat's resource counter?
}
// Find min z2 such that z2 > z_val and all cz true under z := z2 (and current assignment)
// TODO
}
}

1
src/math/polysat/solver.h
View file

@ -236,6 +236,7 @@ namespace polysat {
clause_ref make_asserting(clause& cl, pvar z, rational z_val);
void find_implied_constraint(signed_constraints const& cz, pvar z, rational z_val, sat::literal_vector& out_lits);
void find_implied_constraint_sat(signed_constraints const& cz, pvar z, rational z_val, sat::literal_vector& out_lits);
public:

8
src/math/polysat/univariate/univariate_solver.cpp
View file

@ -136,6 +136,14 @@ namespace polysat {
add(m.mk_eq(bv->mk_bv_not(mk_poly(in)), mk_poly(out)), sign, dep);
}
void add_ule_const(rational const& val, bool sign, dep_t dep) override {
add(bv->mk_ule(x, mk_numeral(val)), sign, dep);
}
void add_uge_const(rational const& val, bool sign, dep_t dep) override {
add(bv->mk_ule(mk_numeral(val), x), sign, dep);
}
lbool check() override {
return s->check_sat();
}

10
src/math/polysat/univariate/univariate_solver.h
View file

@ -56,6 +56,16 @@ namespace polysat {
virtual void add_xor(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) = 0;
virtual void add_not(univariate const& in, univariate const& out, bool sign, dep_t dep) = 0;
/// Add x <= val or x > val, depending on sign
virtual void add_ule_const(rational const& val, bool sign, dep_t dep) = 0;
/// Add x >= val or x < val, depending on sign
virtual void add_uge_const(rational const& val, bool sign, dep_t dep) = 0;
void add_ugt_const(rational const& val, bool sign, dep_t dep) { add_ule_const(val, !sign, dep); }
void add_ult_const(rational const& val, bool sign, dep_t dep) { add_uge_const(val, !sign, dep); }
// TODO: assert bit; use bv->mk_bit2bool(x, idx)
// virtual void add_bit(unsigned idx, bool sign, dep_t dep);
virtual std::ostream& display(std::ostream& out) const = 0;
};