mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

All constraints have bvars now

Browse source
This commit is contained in:
Jakob Rath 2022-11-07 14:14:36 +01:00
parent 586ffdf402
commit 89acd96a89
3 changed files with 4 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/clause_builder.cpp
View file

@ -60,7 +60,6 @@ namespace polysat {
void clause_builder::push(signed_constraint c) {
SASSERT(c);
SASSERT(c->has_bvar());
if (c.is_always_false()) // filter out trivial constraints such as "4 < 2"
return;
if (c.is_always_true()) {

9
src/math/polysat/constraint.h
View file

@ -47,6 +47,7 @@ namespace polysat {
class constraint {
friend class constraint_manager;
friend class signed_constraint;
friend class clause;
friend class ule_constraint;
friend class umul_ovfl_constraint;
@ -58,14 +59,13 @@ namespace polysat {
lbool m_external_sign = l_undef;
bool m_is_active = false;
bool m_is_pwatched = false;
/** The boolean variable associated to this constraint, if any.
* If this is not null_bool_var, then the constraint corresponds to a literal on the assignment stack.
* Convention: the plain constraint corresponds the positive sat::literal.
*/
/** The boolean variable associated to this constraint */
sat::bool_var m_bvar = sat::null_bool_var;
constraint(constraint_manager& m, ckind_t k): m_kind(k) {}
bool has_bvar() const { return m_bvar != sat::null_bool_var; }
public:
virtual ~constraint() {}
@ -104,7 +104,6 @@ namespace polysat {
unsigned_vector const& vars() const { return m_vars; }
unsigned var(unsigned idx) const { return m_vars[idx]; }
bool contains_var(pvar v) const { return m_vars.contains(v); }
bool has_bvar() const { return m_bvar != sat::null_bool_var; }
sat::bool_var bvar() const { SASSERT(has_bvar()); return m_bvar; }
std::string bvar2string() const;
unsigned level(solver& s) const;

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

@ -1245,8 +1245,6 @@ namespace polysat {
if (m_search[i].is_boolean())
skip.insert(m_search[i].lit().var());
for (auto c : m_constraints) {
if (!c->has_bvar())
continue;
if (skip.contains(c->bvar()))
continue;