diff --git a/src/math/polysat/interval.h b/src/math/polysat/interval.h index fac4bdd81..530339e74 100644 --- a/src/math/polysat/interval.h +++ b/src/math/polysat/interval.h @@ -118,6 +118,14 @@ namespace polysat { return false; } +#if 0 + // TODO: intersection of wrapping intervals might not be an interval!!! + // + // Example: + // [---------[ + // -----[ [---- + // would give + // [-[ [--[ eval_interval intersect(eval_interval const& other) const { if (is_full()) return other; if (other.is_full()) return *this; @@ -138,6 +146,8 @@ namespace polysat { return eval_interval::proper(i_lo, i_lo_val, i_hi, i_hi_val); } +#endif + }; inline std::ostream& operator<<(std::ostream& os, eval_interval const& i) { diff --git a/src/math/polysat/simplify_clause.cpp b/src/math/polysat/simplify_clause.cpp index 136be5cc5..14dc97f77 100644 --- a/src/math/polysat/simplify_clause.cpp +++ b/src/math/polysat/simplify_clause.cpp @@ -225,4 +225,117 @@ namespace polysat { return true; } + + + +#if 0 + // All variables of clause 'cl' except 'z' are assigned. + // Goal: a possibly weaker clause that implies a restriction on z around z_val + clause_ref simplify_clause::make_asserting(clause& cl, pvar z, rational z_val) { + signed_constraints cz; // constraints of 'cl' that contain 'z' + sat::literal_vector lits; // literals of the new clause + for (sat::literal lit : cl) { + signed_constraint c = s.lit2cnstr(lit); + if (c.contains_var(z)) + cz.push_back(c); + else + lits.push_back(lit); + } + SASSERT(!cz.empty()); + if (cz.size() == 1) { + // TODO: even in this case, if the constraint is non-linear in z, we might want to extract a maximal forbidden interval around z_val. + return nullptr; + } + else { + // multiple constraints that contain z + find_implied_constraint(cz, z, z_val, lits); + return clause::from_literals(std::move(lits)); + } + } + + // Each constraint in 'cz' is univariate in 'z' under the current assignment. + // Goal: a literal that is implied by the disjunction of cz and ensures z != z_val in viable. + // (plus side conditions that do not depend on z) + void simplify_clause::find_implied_constraint(signed_constraints const& cz, pvar z, rational z_val, sat::literal_vector& out_lits) + { + unsigned const out_lits_original_size = out_lits.size(); + + forbidden_intervals fi(s); + fi_record entry; + + auto intersection = eval_interval::full(); + bool all_unit = true; + + for (signed_constraint const& c : cz) { + if (fi.get_interval(c, z, entry) && entry.coeff == 1) { + intersection = intersection.intersect(entry.interval); + for (auto const& sc : entry.side_cond) + out_lits.push_back(sc.blit()); + } else { + all_unit = false; + break; + } + } + + if (all_unit) { + SASSERT(!intersection.is_currently_empty()); + // Unit intervals from all constraints + // => build constraint from intersection of forbidden intervals + // z \not\in [l;u[ <=> z - l >= u - l + if (intersection.is_proper()) { + auto c_new = s.ule(intersection.hi() - intersection.lo(), z - intersection.lo()); + out_lits.push_back(c_new.blit()); + } + } else { + out_lits.shrink(out_lits_original_size); + find_implied_constraint_sat(cz, z, z_val, out_lits); + } + } + + void simplify_clause::find_implied_constraint_sat(signed_constraints const& cz, pvar z, rational z_val, sat::literal_vector& out_lits) + { + unsigned bit_width = s.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(s, 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 = s.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 + } +#endif + } diff --git a/src/math/polysat/simplify_clause.h b/src/math/polysat/simplify_clause.h index 41f9fa6a1..51963083b 100644 --- a/src/math/polysat/simplify_clause.h +++ b/src/math/polysat/simplify_clause.h @@ -36,6 +36,10 @@ namespace polysat { pdd abstract(pdd const& p, pdd& v); + 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: simplify_clause(solver& s); diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 85ccd7f26..58f55df22 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -1158,116 +1158,4 @@ namespace polysat { return all_ok; } - - - // All variables of clause 'cl' except 'z' are assigned. - // Goal: a possibly weaker clause that implies a restriction on z around z_val - clause_ref solver::make_asserting(clause& cl, pvar z, rational z_val) { - signed_constraints cz; // constraints of 'cl' that contain 'z' - sat::literal_vector lits; // literals of the new clause - for (sat::literal lit : cl) { - signed_constraint c = lit2cnstr(lit); - if (c.contains_var(z)) - cz.push_back(c); - else - lits.push_back(lit); - } - SASSERT(!cz.empty()); - if (cz.size() == 1) { - // TODO: even in this case, if the constraint is non-linear in z, we might want to extract a maximal forbidden interval around z_val. - return nullptr; - } - else { - // multiple constraints that contain z - find_implied_constraint(cz, z, z_val, lits); - return clause::from_literals(std::move(lits)); - } - } - - // Each constraint in 'cz' is univariate in 'z' under the current assignment. - // Goal: a literal that is implied by the disjunction of cz and ensures z != z_val in viable. - // (plus side conditions that do not depend on z) - void solver::find_implied_constraint(signed_constraints const& cz, pvar z, rational z_val, sat::literal_vector& out_lits) - { - unsigned const out_lits_original_size = out_lits.size(); - - forbidden_intervals fi(*this); - fi_record entry; - - auto intersection = eval_interval::full(); - bool all_unit = true; - - for (signed_constraint const& c : cz) { - if (fi.get_interval(c, z, entry) && entry.coeff == 1) { - intersection = intersection.intersect(entry.interval); - for (auto const& sc : entry.side_cond) - out_lits.push_back(sc.blit()); - } else { - all_unit = false; - break; - } - } - - if (all_unit) { - SASSERT(!intersection.is_currently_empty()); - // Unit intervals from all constraints - // => build constraint from intersection of forbidden intervals - // z \not\in [l;u[ <=> z - l >= u - l - if (intersection.is_proper()) { - auto c_new = ule(intersection.hi() - intersection.lo(), z - intersection.lo()); - out_lits.push_back(c_new.blit()); - } - } else { - out_lits.shrink(out_lits_original_size); - 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 - } - } - - diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 45abf7e41..81cb0fb65 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -234,10 +234,6 @@ namespace polysat { bool can_propagate(); void propagate(); - 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: /**