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

support op_constraint in univariate solver

Browse source
This commit is contained in:
Jakob Rath 2022-03-17 14:03:42 +01:00
parent c4370eb7e6
commit edeba9b56a
2 changed files with 35 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -101,6 +101,34 @@ namespace polysat {
add(bv->mk_bvsmul_no_udfl(mk_poly(lhs), mk_poly(rhs)), !sign, dep); add(bv->mk_bvsmul_no_udfl(mk_poly(lhs), mk_poly(rhs)), !sign, dep);
} }
void add_lshr(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) override {
add(m.mk_eq(bv->mk_bv_lshr(mk_poly(in1), mk_poly(in2)), mk_poly(out)), sign, dep);
}
void add_ashr(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) override {
add(m.mk_eq(bv->mk_bv_ashr(mk_poly(in1), mk_poly(in2)), mk_poly(out)), sign, dep);
}
void add_shl(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) override {
add(m.mk_eq(bv->mk_bv_shl(mk_poly(in1), mk_poly(in2)), mk_poly(out)), sign, dep);
}
void add_and(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) override {
add(m.mk_eq(bv->mk_bv_and(mk_poly(in1), mk_poly(in2)), mk_poly(out)), sign, dep);
}
void add_or(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) override {
add(m.mk_eq(bv->mk_bv_or(mk_poly(in1), mk_poly(in2)), mk_poly(out)), sign, dep);
}
void add_xor(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) override {
add(m.mk_eq(bv->mk_bv_xor(mk_poly(in1), mk_poly(in2)), mk_poly(out)), sign, dep);
}
void add_not(univariate const& in, univariate const& out, bool sign, dep_t dep) override {
add(m.mk_eq(bv->mk_bv_not(mk_poly(in)), mk_poly(out)), sign, dep);
}
lbool check() override { lbool check() override {
return s->check_sat(); return s->check_sat();
} }

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

@ -48,7 +48,13 @@ namespace polysat {
virtual void add_umul_ovfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0; virtual void add_umul_ovfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0;
virtual void add_smul_ovfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0; virtual void add_smul_ovfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0;
virtual void add_smul_udfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0; virtual void add_smul_udfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0;
// op constraints? virtual void add_lshr(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) = 0;
virtual void add_ashr(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) = 0;
virtual void add_shl(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) = 0;
virtual void add_and(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) = 0;
virtual void add_or(univariate const& in1, univariate const& in2, univariate const& out, bool sign, dep_t dep) = 0;
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;
virtual std::ostream& display(std::ostream& out) const = 0; virtual std::ostream& display(std::ostream& out) const = 0;
}; };