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

don't rely on initializer list implementations, there are no constructors in the standard

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-12-22 10:48:37 -08:00
parent 09fa657be9
commit d183ac23d0
9 changed files with 22 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -444,7 +444,11 @@ namespace polysat {
}
void core::add_axiom(char const* name, core_vector const& cs, bool is_redundant) {
s.add_axiom(name, cs, is_redundant);
s.add_axiom(name, cs.begin(), cs.end(), is_redundant);
}
void core::add_axiom(char const* name, constraint_or_dependency const* begin, constraint_or_dependency const* end, bool is_redundant) {
s.add_axiom(name, begin, end, is_redundant);
}
std::ostream& core::display(std::ostream& out) const {

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

@ -136,6 +136,7 @@ namespace polysat {
* Where d_i are logical interpretations of dependencies and sc_j are signed constraints.
*/
void add_axiom(char const* name, core_vector const& cs, bool is_redundant);
void add_axiom(char const* name, constraint_or_dependency const* begin, constraint_or_dependency const* end, bool is_redundant);
pvar add_var(unsigned sz);
pdd var(pvar p) { return m_vars[p]; }

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

@ -69,7 +69,7 @@ namespace polysat {
// c := X*y ~ X*Z
bool is_Xy_l_XZ(pvar y, pdd& x, pdd& z) const { return is_xY(y, lhs(), x) && (false); }
bool verify_Xy_l_XZ(pvar y, pdd const& x, pdd const& z) const { lhs() == c.var(y) * x && rhs() == z * x; }
bool verify_Xy_l_XZ(pvar y, pdd const& x, pdd const& z) const { return lhs() == c.var(y) * x && rhs() == z * x; }
// c := Ax ~ Y
bool is_Ax_l_Y(pvar x, pdd& a, pdd& y) const;

7
src/sat/smt/polysat/saturation.cpp
View file

@ -80,7 +80,7 @@ namespace polysat {
else
UNREACHABLE();
}
c.add_axiom(name, core_vector(lemma.begin(), lemma.end()), is_redundant);
c.add_axiom(name, lemma.begin(), lemma.end(), is_redundant);
m_propagated = true;
}
@ -114,7 +114,6 @@ namespace polysat {
* p <= q, q <= p => p = q
*/
void saturation::propagate_infer_equality(pvar x, inequality const& i) {
set_rule("[x] p <= q, q <= p => p - q = 0");
if (i.is_strict())
return;
if (i.lhs().degree(x) == 0 && i.rhs().degree(x) == 0)
@ -226,8 +225,10 @@ namespace polysat {
return { q, p2 };
else if (q == p2)
return { p, q2 };
else
else {
SASSERT(q == q2);
return { p, p2 };
}
};
if (match_constraints([&](auto const& sc2) { return sc2.is_umul_ovfl() && sc.sign() != sc2.sign() && match_mul_arg(sc2); }, id)) {
auto sc2 = c.get_constraint(id);

3
src/sat/smt/polysat/saturation.h
View file

@ -28,9 +28,7 @@ namespace polysat {
using clause = std::initializer_list<constraint_id_or_constraint>;
core& c;
constraints& C;
char const* m_rule = nullptr;
bool m_propagated = false;
void set_rule(char const* r) { m_rule = r; }
void propagate(signed_constraint const& sc, std::initializer_list<constraint_id> const& premises);
void add_clause(char const* name, clause const& cs, bool is_redundant);
@ -45,7 +43,6 @@ namespace polysat {
void propagate_infer_equality(pvar x, inequality const& a_l_b);
void propagate_umul_ovfl(pvar v, umul_ovfl const& sc);
void try_ugt_x(pvar v, inequality const& i);
void try_ugt_y(pvar v, inequality const& i);
void try_ugt_z(pvar z, inequality const& i);

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

@ -98,7 +98,7 @@ namespace polysat {
public:
virtual ~solver_interface() {}
virtual void add_eq_literal(pvar v, rational const& val) = 0;
virtual bool add_axiom(char const* name, core_vector const& core, bool redundant) = 0;
virtual bool add_axiom(char const* name, constraint_or_dependency const* begin, constraint_or_dependency const* end, bool redundant) = 0;
virtual void set_conflict(constraint_id_vector const& core) = 0;
virtual dependency propagate(signed_constraint sc, constraint_id_vector const& deps) = 0;
virtual void propagate(dependency const& d, bool sign, constraint_id_vector const& deps) = 0;

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

@ -467,6 +467,7 @@ namespace polysat {
}
bool viable::set_conflict_by_interval_rec(pvar v, unsigned w, entry** intervals, unsigned num_intervals, bool& create_lemma, uint_set& vars_to_explain) {
#if 0
SASSERT(std::all_of(intervals, intervals + num_intervals, [w](entry const* e) { return e->bit_width <= w; }));
// TODO: assert invariants on intervals list
rational const& mod_value = rational::power_of_two(w);
@ -499,7 +500,7 @@ namespace polysat {
m_alloc.push_back(tmp);
};
#if 0
while (!longest->interval.currently_contains(e->interval.hi_val())) {
unsigned j = (i + 1) % num_intervals;
entry* n = intervals[j];

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

@ -256,9 +256,10 @@ namespace polysat {
return ctx.get_trail_stack();
}
bool solver::add_axiom(char const* name, core_vector const& cs, bool is_redundant) {
bool solver::add_axiom(char const* name, constraint_or_dependency const* begin, constraint_or_dependency const* end, bool is_redundant) {
sat::literal_vector lits;
for (auto e : cs) {
for (auto it = begin; it != end; ++it) {
auto const& e = *it;
if (std::holds_alternative<dependency>(e)) {
auto d = *std::get_if<dependency>(&e);
SASSERT(!d.is_null());

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

@ -161,7 +161,7 @@ namespace polysat {
// callbacks from core
void add_eq_literal(pvar v, rational const& val) override;
void set_conflict(constraint_id_vector const& core) override;
bool add_axiom(char const* name, core_vector const& core, bool redundant) override;
bool add_axiom(char const* name, constraint_or_dependency const* begin, constraint_or_dependency const* end, bool redundant) override;
dependency propagate(signed_constraint sc, constraint_id_vector const& deps) override;
void propagate(dependency const& d, bool sign, constraint_id_vector const& deps) override;
trail_stack& trail() override;
@ -169,6 +169,10 @@ namespace polysat {
void get_bitvector_suffixes(pvar v, pvar_vector& out) override;
void get_fixed_bits(pvar v, svector<justified_fixed_bits>& fixed_bits) override;
bool add_axiom(char const* name, core_vector const& clause, bool redundant) {
return add_axiom(name, clause.begin(), clause.end(), redundant);
}
std::pair<sat::literal_vector, euf::enode_pair_vector> explain_deps(dependency_vector const& deps);
expr_ref constraint2expr(signed_constraint const& sc);