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

univariate solver: add_bit

Browse source
This commit is contained in:
Jakob Rath 2022-08-22 15:09:11 +02:00
parent d9a63ce786
commit 058c5771b9
2 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -144,6 +144,10 @@ namespace polysat {
add(bv->mk_ule(mk_numeral(val), x), sign, dep); add(bv->mk_ule(mk_numeral(val), x), sign, dep);
} }
void add_bit(unsigned idx, bool sign, dep_t dep) override {
add(bv->mk_bit2bool(x, idx), sign, dep);
}
lbool check() override { lbool check() override {
return s->check_sat(); return s->check_sat();
} }

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

@ -63,8 +63,8 @@ namespace polysat {
void add_ugt_const(rational const& val, bool sign, dep_t dep) { add_ule_const(val, !sign, dep); } 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); } 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) /// Assert i-th bit of x
// virtual void add_bit(unsigned idx, bool sign, dep_t dep); virtual void add_bit(unsigned idx, bool sign, dep_t dep) = 0;
virtual std::ostream& display(std::ostream& out) const = 0; virtual std::ostream& display(std::ostream& out) const = 0;
}; };