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

remove eq constraint, fix gc for external constraints

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-11 20:09:28 +02:00
parent f8a3857adb
commit b36bc11b85
15 changed files with 133 additions and 275 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/CMakeLists.txt
View file

@ -5,7 +5,6 @@ z3_add_component(polysat
clause_builder.cpp
conflict_core.cpp
constraint.cpp
eq_constraint.cpp
explain.cpp
forbidden_intervals.cpp
justification.cpp

56
src/math/polysat/constraint.cpp
View file

@ -17,7 +17,6 @@ Author:
#include "math/polysat/solver.h"
#include "math/polysat/log.h"
#include "math/polysat/log_helper.h"
#include "math/polysat/eq_constraint.h"
#include "math/polysat/ule_constraint.h"
namespace polysat {
@ -67,11 +66,21 @@ namespace polysat {
void constraint_manager::register_external(constraint* c) {
SASSERT(c);
SASSERT(c->unit_dep());
SASSERT(c->unit_dep()->is_leaf());
unsigned const dep = c->unit_dep()->leaf_value();
SASSERT(!m_external_constraints.contains(dep));
m_external_constraints.insert(dep, c);
SASSERT(!c->is_external());
if (c->unit_dep() && c->unit_dep()->is_leaf()) {
unsigned const dep = c->unit_dep()->leaf_value();
SASSERT(!m_external_constraints.contains(dep));
m_external_constraints.insert(dep, c);
}
c->set_external();
++m_num_external;
}
void constraint_manager::unregister_external(constraint* c) {
if (c->unit_dep() && c->unit_dep()->is_leaf())
m_external_constraints.remove(c->unit_dep()->leaf_value());
c->unset_external();
--m_num_external;
}
// Release constraints at the given level and above.
@ -111,31 +120,32 @@ namespace polysat {
}
}
void constraint_manager::gc() {
gc_clauses();
gc_constraints();
void constraint_manager::gc(solver& s) {
gc_clauses(s);
gc_constraints(s);
}
void constraint_manager::gc_clauses() {
void constraint_manager::gc_clauses(solver& s) {
// place to gc redundant clauses
}
void constraint_manager::gc_constraints() {
void constraint_manager::gc_constraints(solver& s) {
uint_set used_vars;
for (auto const& cls : m_clauses)
for (auto const& cl : cls)
for (auto lit : *cl)
used_vars.insert(lit.var());
#if 0
// anything on the search stack is justified by a clause?
for (auto const& a : s().m_search)
for (auto const& a : s.m_search)
if (a.is_boolean())
used_vars.insert(a.lit().var());
#endif
for (unsigned i = 0; i < m_constraints.size(); ++i) {
constraint* c = m_constraints[i];
constraint* c = m_constraints[i];
if (c->has_bvar() && used_vars.contains(c->bvar()))
continue;
if (c->is_external())
continue;
erase_bvar(c);
m_constraints.swap(i, m_constraints.size() - 1);
m_constraints.pop_back();
--i;
@ -144,13 +154,13 @@ namespace polysat {
}
bool constraint_manager::should_gc() {
// TODO: maybe replace this by a better heuristic
// maintain a counter of temporary constraints? (#constraints - #bvars)
return true;
// TODO control gc decay rate
return m_constraints.size() > m_num_external + 100;
}
signed_constraint constraint_manager::eq(pdd const& p) {
return {dedup(alloc(eq_constraint, *this, p)), true};
pdd z = p.manager().zero();
return {dedup(alloc(ule_constraint, *this, p, z)), true};
}
signed_constraint constraint_manager::ule(pdd const& a, pdd const& b) {
@ -192,14 +202,6 @@ namespace polysat {
return signed_constraint(const_cast<constraint*>(src), !is_strict);
}
eq_constraint& constraint::to_eq() {
return *dynamic_cast<eq_constraint*>(this);
}
eq_constraint const& constraint::to_eq() const {
return *dynamic_cast<eq_constraint const*>(this);
}
ule_constraint& constraint::to_ule() {
return *dynamic_cast<ule_constraint*>(this);
}

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

@ -19,10 +19,9 @@ Author:
namespace polysat {
enum ckind_t { eq_t, ule_t };
enum ckind_t { ule_t };
class constraint;
class eq_constraint;
class ule_constraint;
class signed_constraint;
@ -47,6 +46,7 @@ namespace polysat {
// Association to external dependency values (i.e., external names for constraints)
u_map<constraint*> m_external_constraints;
unsigned m_num_external = 0;
// Manage association of constraints to boolean variables
void assign_bv2c(sat::bool_var bv, constraint* c);
@ -58,8 +58,8 @@ namespace polysat {
constraint* dedup(constraint* c);
void gc_constraints();
void gc_clauses();
void gc_constraints(solver& s);
void gc_clauses(solver& s);
public:
constraint_manager(bool_var_manager& bvars): m_bvars(bvars) {}
@ -73,12 +73,13 @@ namespace polysat {
/// Register a unit clause with an external dependency.
void register_external(constraint* c);
void unregister_external(constraint* c);
/// Release clauses at the given level and above.
void release_level(unsigned lvl);
/// Garbage-collect temporary constraints (i.e., those that do not have a boolean variable).
void gc();
void gc(solver& s);
bool should_gc();
constraint* lookup(sat::bool_var var) const;
@ -113,13 +114,13 @@ namespace polysat {
class constraint {
friend class constraint_manager;
friend class clause;
friend class eq_constraint;
friend class ule_constraint;
// constraint_manager* m_manager;
clause* m_unit_clause = nullptr; ///< If this constraint was asserted by a unit clause, we store that clause here.
ckind_t m_kind;
unsigned_vector m_vars;
bool m_is_external = 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.
@ -138,7 +139,7 @@ namespace polysat {
virtual bool operator==(constraint const& other) const = 0;
bool operator!=(constraint const& other) const { return !operator==(other); }
bool is_eq() const { return m_kind == ckind_t::eq_t; }
virtual bool is_eq() const { return false; }
bool is_ule() const { return m_kind == ckind_t::ule_t; }
ckind_t kind() const { return m_kind; }
virtual std::ostream& display(std::ostream& out, lbool status = l_undef) const = 0;
@ -150,9 +151,8 @@ namespace polysat {
virtual bool is_currently_true(solver& s, bool is_positive) const = 0;
virtual void narrow(solver& s, bool is_positive) = 0;
virtual inequality as_inequality(bool is_positive) const = 0;
eq_constraint& to_eq();
eq_constraint const& to_eq() const;
ule_constraint& to_ule();
ule_constraint const& to_ule() const;
unsigned_vector& vars() { return m_vars; }
@ -165,6 +165,10 @@ namespace polysat {
clause* unit_clause() const { return m_unit_clause; }
void set_unit_clause(clause* cl);
p_dependency* unit_dep() const { return m_unit_clause ? m_unit_clause->dep() : nullptr; }
void set_external() { m_is_external = true; }
void unset_external() { m_is_external = false; }
bool is_external() const { return m_is_external; }
};
inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); }

108
src/math/polysat/eq_constraint.cpp
View file

@ -1,108 +0,0 @@
/*++
Copyright (c) 2021 Microsoft Corporation
Module Name:
polysat eq_constraints
Author:
Nikolaj Bjorner (nbjorner) 2021-03-19
Jakob Rath 2021-04-6
--*/
#include "math/polysat/constraint.h"
#include "math/polysat/solver.h"
#include "math/polysat/log.h"
namespace polysat {
std::ostream& eq_constraint::display(std::ostream& out, lbool status) const {
out << p();
if (status == l_true) out << " == 0";
else if (status == l_false) out << " != 0";
else out << " ==/!= 0";
return display_extra(out, status);
}
void eq_constraint::narrow(solver& s, bool is_positive) {
LOG("Assignment: " << assignments_pp(s));
auto q = p().subst_val(s.assignment());
LOG("Substituted: " << p() << " := " << q);
if (q.is_zero()) {
if (!is_positive) {
LOG("Conflict (zero under current assignment)");
s.set_conflict({this, is_positive});
}
return;
}
if (q.is_never_zero()) {
if (is_positive) {
LOG("Conflict (never zero under current assignment)");
s.set_conflict({this, is_positive});
}
return;
}
if (q.is_unilinear()) {
// a*x + b == 0
pvar v = q.var();
s.push_cjust(v, {this, is_positive});
rational a = q.hi().val();
rational b = q.lo().val();
s.m_viable.intersect_eq(a, v, b, is_positive);
rational val;
if (s.m_viable.find_viable(v, val) == dd::find_t::singleton)
s.propagate(v, val, {this, is_positive});
return;
}
// TODO: what other constraints can be extracted cheaply?
}
bool eq_constraint::is_always_false(bool is_positive) const {
if (is_positive)
return p().is_never_zero();
else
return p().is_zero();
}
bool eq_constraint::is_currently_false(solver& s, bool is_positive) const {
pdd r = p().subst_val(s.assignment());
if (is_positive)
return r.is_never_zero();
else
return r.is_zero();
}
bool eq_constraint::is_currently_true(solver& s, bool is_positive) const {
pdd r = p().subst_val(s.assignment());
if (is_positive)
return r.is_zero();
else
return r.is_never_zero();
}
inequality eq_constraint::as_inequality(bool is_positive) const {
pdd zero = p() - p();
if (is_positive)
// p <= 0
return inequality(p(), zero, false, this);
else
// 0 < p
return inequality(zero, p(), true, this);
}
unsigned eq_constraint::hash() const {
return p().hash();
}
bool eq_constraint::operator==(constraint const& other) const {
return other.is_eq() && p() == other.to_eq().p();
}
}

43
src/math/polysat/eq_constraint.h
View file

@ -1,43 +0,0 @@
/*++
Copyright (c) 2021 Microsoft Corporation
Module Name:
polysat equality constraints
Author:
Nikolaj Bjorner (nbjorner) 2021-03-19
Jakob Rath 2021-04-6
--*/
#pragma once
#include "math/polysat/constraint.h"
namespace polysat {
class eq_constraint final : public constraint {
friend class constraint_manager;
pdd m_poly;
eq_constraint(constraint_manager& m, pdd const& p):
constraint(m, ckind_t::eq_t), m_poly(p) {
m_vars.append(p.free_vars());
}
public:
~eq_constraint() override {}
pdd const & p() const { return m_poly; }
std::ostream& display(std::ostream& out, lbool status) const override;
bool is_always_false(bool is_positive) const override;
bool is_currently_false(solver& s, bool is_positive) const override;
bool is_currently_true(solver& s, bool is_positive) const override;
void narrow(solver& s, bool is_positive) override;
inequality as_inequality(bool is_positive) const override;
unsigned hash() const override;
bool operator==(constraint const& other) const override;
};
}

4
src/math/polysat/explain.cpp
View file

@ -26,8 +26,8 @@ namespace polysat {
LOG_H3("Resolving upon v" << v);
LOG("c1: " << c1);
LOG("c2: " << c2);
pdd a = c1->to_eq().p();
pdd b = c2->to_eq().p();
pdd a = c1->to_ule().p();
pdd b = c2->to_ule().p();
pdd r = a;
if (!a.resolve(v, b, r) && !b.resolve(v, a, r))
return {};

13
src/math/polysat/forbidden_intervals.cpp
View file

@ -180,11 +180,12 @@ namespace polysat {
bool forbidden_intervals::get_interval(solver& s, signed_constraint const& c, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond)
{
inequality ineq = c.as_inequality();
if (!c->is_ule())
return false;
// Current only works when degree(v) is at most one on both sides
pdd lhs = ineq.lhs;
pdd rhs = ineq.rhs;
if (ineq.is_strict)
pdd lhs = c->to_ule().lhs();
pdd rhs = c->to_ule().rhs();
if (!c.is_positive())
swap(lhs, rhs);
unsigned const deg1 = lhs.degree(v);
unsigned const deg2 = rhs.degree(v);
@ -317,7 +318,7 @@ namespace polysat {
out_neg_cond = s.m_constraints.eq(condition_body);
if (is_trivial) {
if (!ineq.is_strict)
if (c.is_positive())
// TODO: we cannot use empty intervals for interpolation. So we
// can remove the empty case (make it represent 'full' instead),
// and return 'false' here. Then we do not need the proper/full
@ -345,7 +346,7 @@ namespace polysat {
else
SASSERT(y_coeff.is_one());
if (ineq.is_strict) {
if (!c.is_positive()) {
swap(lo, hi);
lo_val.swap(hi_val);
}

47
src/math/polysat/linear_solver.cpp
View file

@ -113,32 +113,14 @@ namespace polysat {
* when equality is asserted, set range on v as v == 0 or v > 0.
*/
void linear_solver::new_eq(eq_constraint& c) {
var_t v = internalize_pdd(c.p());
auto pr = std::make_pair(v, v);
m_bool_var2row.setx(c.bvar(), pr, pr);
}
void linear_solver::new_le(ule_constraint& c) {
var_t v = internalize_pdd(c.lhs());
var_t w = internalize_pdd(c.rhs());
auto pr = std::make_pair(v, w);
m_bool_var2row.setx(c.bvar(), pr, pr);
}
void linear_solver::assert_eq(bool is_positive, eq_constraint& c) {
unsigned c_dep = constraint_idx2dep(m_active.size() - 1);
var_t v = m_bool_var2row[c.bvar()].first;
unsigned sz = c.p().power_of_2();
auto* fp = sz2fixplex(sz);
if (!fp)
return;
rational z(0), o(1);
if (is_positive)
fp->set_bounds(v, z, z, c_dep);
else
fp->set_bounds(v, o, z, c_dep);
}
}
//
// v <= w:
@ -194,33 +176,16 @@ namespace polysat {
void linear_solver::new_constraint(constraint& c) {
switch (c.kind()) {
case ckind_t::eq_t:
new_eq(c.to_eq());
break;
case ckind_t::ule_t:
if (c.is_ule())
new_le(c.to_ule());
break;
default:
UNREACHABLE();
break;
}
}
void linear_solver::activate_constraint(bool is_positive, constraint& c) {
if (!c.is_ule())
return;
m_active.push_back(&c);
m_trail.push_back(trail_i::set_active_i);
switch (c.kind()) {
case ckind_t::eq_t:
assert_eq(is_positive, c.to_eq());
break;
case ckind_t::ule_t:
assert_le(is_positive, c.to_ule());
break;
default:
UNREACHABLE();
break;
}
assert_le(is_positive, c.to_ule());
}
void linear_solver::linearize(pdd const& p) {

3
src/math/polysat/linear_solver.h
View file

@ -29,7 +29,6 @@ Author:
#include "util/small_object_allocator.h"
#include "math/polysat/fixplex.h"
#include "math/polysat/constraint.h"
#include "math/polysat/eq_constraint.h"
#include "math/polysat/ule_constraint.h"
namespace polysat {
@ -98,9 +97,7 @@ namespace polysat {
var_t fresh_var(unsigned sz);
var_t internalize_pdd(pdd const& p);
void new_eq(eq_constraint& eq);
void new_le(ule_constraint& le);
void assert_eq(bool is_positive, eq_constraint& eq);
void assert_le(bool is_positive, ule_constraint& le);
// bind monomial to variable.

8
src/math/polysat/saturation.cpp
View file

@ -33,6 +33,8 @@ namespace polysat {
bool inf_saturate::perform(pvar v, conflict_core& core) {
for (auto c1 : core) {
if (!c1->is_ule())
continue;
auto c = c1.as_inequality();
if (try_ugt_x(v, core, c))
return true;
@ -292,6 +294,8 @@ namespace polysat {
pdd x = s().var(v);
pdd z = x;
for (auto dd : core) {
if (!dd->is_ule())
continue;
auto d = dd.as_inequality();
if (is_Xy_l_XZ(v, d, x, z) && try_ugt_y(v, core, c, d, x, z))
return true;
@ -308,6 +312,8 @@ namespace polysat {
pdd y = s().var(x);
pdd a = y;
for (auto dd : core) {
if (!dd->is_ule())
continue;
auto d = dd.as_inequality();
if (is_Y_l_Ax(x, d, a, y) && try_y_l_ax_and_x_l_z(x, core, c, d, a, y))
return true;
@ -338,6 +344,8 @@ namespace polysat {
pdd y = s().var(z);
pdd x = y;
for (auto dd : core) {
if (!dd->is_ule())
continue;
auto d = dd.as_inequality();
if (is_YX_l_zX(z, d, x, y) && try_ugt_z(z, core, c, d, x, y))
return true;

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

@ -56,20 +56,18 @@ namespace polysat {
(m_stats.m_num_conflicts < m_max_conflicts) &&
(m_stats.m_num_decisions < m_max_decisions);
}
lbool solver::check_sat() {
LOG("Starting");
m_disjunctive_lemma.reset();
while (m_lim.inc()) {
while (inc()) {
m_stats.m_num_iterations++;
LOG_H1("Next solving loop iteration (#" << m_stats.m_num_iterations << ")");
LOG("Free variables: " << m_free_vars);
LOG("Assignment: " << assignments_pp(*this));
if (!m_conflict.empty()) LOG("Conflict: " << m_conflict);
IF_LOGGING(m_viable.log());
if (!is_conflict() && m_constraints.should_gc())
m_constraints.gc();
if (!is_conflict() && m_constraints.should_gc()) m_constraints.gc(*this);
if (pending_disjunctive_lemma()) { LOG_H2("UNDEF (handle lemma externally)"); return l_undef; }
else if (is_conflict() && at_base_level()) { LOG_H2("UNSAT"); return l_false; }
@ -116,31 +114,31 @@ namespace polysat {
m_free_vars.del_var_eh(v);
}
signed_constraint solver::mk_eq(pdd const& p) {
signed_constraint solver::eq(pdd const& p) {
return m_constraints.eq(p);
}
signed_constraint solver::mk_diseq(pdd const& p) {
signed_constraint solver::diseq(pdd const& p) {
return ~m_constraints.eq(p);
}
signed_constraint solver::mk_ule(pdd const& p, pdd const& q) {
signed_constraint solver::ule(pdd const& p, pdd const& q) {
return m_constraints.ule(p, q);
}
signed_constraint solver::mk_ult(pdd const& p, pdd const& q) {
signed_constraint solver::ult(pdd const& p, pdd const& q) {
return m_constraints.ult(p, q);
}
signed_constraint solver::mk_sle(pdd const& p, pdd const& q) {
signed_constraint solver::sle(pdd const& p, pdd const& q) {
return m_constraints.sle(p, q);
}
signed_constraint solver::mk_slt(pdd const& p, pdd const& q) {
signed_constraint solver::slt(pdd const& p, pdd const& q) {
return m_constraints.slt(p, q);
}
void solver::new_constraint(signed_constraint c, unsigned dep, bool activate) {
void solver::ext_constraint(signed_constraint c, unsigned dep, bool activate) {
VERIFY(at_base_level());
SASSERT(c);
SASSERT(activate || dep != null_dependency); // if we don't activate the constraint, we need the dependency to access it again later.
@ -148,7 +146,11 @@ namespace polysat {
clause* unit = m_constraints.store(clause::from_unit(m_level, c, mk_dep_ref(dep)));
c->set_unit_clause(unit);
if (dep != null_dependency)
m_constraints.register_external(c.get());
if (!c->is_external()) {
m_constraints.register_external(c.get());
m_trail.push_back(trail_instr_t::ext_constraint_i);
m_ext_constraint_trail.push_back(c.get());
}
LOG("New constraint: " << c);
#if ENABLE_LINEAR_SOLVER
@ -303,6 +305,11 @@ namespace polysat {
m_cjust_trail.pop_back();
break;
}
case trail_instr_t::ext_constraint_i: {
constraint* c = m_ext_constraint_trail.back();
m_constraints.unregister_external(c);
m_ext_constraint_trail.pop_back();
}
default:
UNREACHABLE();
}

41
src/math/polysat/solver.h
View file

@ -24,7 +24,6 @@ Author:
#include "math/polysat/conflict_core.h"
#include "math/polysat/constraint.h"
#include "math/polysat/clause_builder.h"
#include "math/polysat/eq_constraint.h"
#include "math/polysat/explain.h"
#include "math/polysat/ule_constraint.h"
#include "math/polysat/justification.h"
@ -64,6 +63,7 @@ namespace polysat {
friend class assignment_pp;
friend class assignments_pp;
friend class inf_saturate;
friend class constraint_manager;
typedef ptr_vector<constraint> constraints;
typedef vector<signed_constraint> signed_constraints;
@ -111,6 +111,7 @@ namespace polysat {
svector<trail_instr_t> m_trail;
unsigned_vector m_qhead_trail;
unsigned_vector m_cjust_trail;
ptr_vector<constraint> m_ext_constraint_trail;
unsigned_vector m_base_levels; // External clients can push/pop scope.
@ -216,13 +217,13 @@ namespace polysat {
void backjump(unsigned new_level);
void add_lemma(clause_ref lemma);
signed_constraint mk_eq(pdd const& p);
signed_constraint mk_diseq(pdd const& p);
signed_constraint mk_ule(pdd const& p, pdd const& q);
signed_constraint mk_ult(pdd const& p, pdd const& q);
signed_constraint mk_sle(pdd const& p, pdd const& q);
signed_constraint mk_slt(pdd const& p, pdd const& q);
void new_constraint(signed_constraint c, unsigned dep, bool activate);
signed_constraint eq(pdd const& p);
signed_constraint diseq(pdd const& p);
signed_constraint ule(pdd const& p, pdd const& q);
signed_constraint ult(pdd const& p, pdd const& q);
signed_constraint sle(pdd const& p, pdd const& q);
signed_constraint slt(pdd const& p, pdd const& q);
void ext_constraint(signed_constraint c, unsigned dep, bool activate);
static void insert_constraint(signed_constraints& cs, signed_constraint c);
bool inc() { return m_lim.inc(); }
@ -290,20 +291,20 @@ namespace polysat {
* Create polynomial constraints (but do not activate them).
* Each constraint is tracked by a dependency.
*/
void new_eq(pdd const& p, unsigned dep) { new_constraint(mk_eq(p), dep, false); }
void new_diseq(pdd const& p, unsigned dep) { new_constraint(mk_diseq(p), dep, false); }
void new_ule(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_ule(p, q), dep, false); }
void new_ult(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_ult(p, q), dep, false); }
void new_sle(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_sle(p, q), dep, false); }
void new_slt(pdd const& p, pdd const& q, unsigned dep) { new_constraint(mk_slt(p, q), dep, false); }
void new_eq(pdd const& p, unsigned dep) { ext_constraint(eq(p), dep, false); }
void new_diseq(pdd const& p, unsigned dep) { ext_constraint(diseq(p), dep, false); }
void new_ule(pdd const& p, pdd const& q, unsigned dep) { ext_constraint(ule(p, q), dep, false); }
void new_ult(pdd const& p, pdd const& q, unsigned dep) { ext_constraint(ult(p, q), dep, false); }
void new_sle(pdd const& p, pdd const& q, unsigned dep) { ext_constraint(sle(p, q), dep, false); }
void new_slt(pdd const& p, pdd const& q, unsigned dep) { ext_constraint(slt(p, q), dep, false); }
/** Create and activate polynomial constraints. */
void add_eq(pdd const& p, unsigned dep = null_dependency) { new_constraint(mk_eq(p), dep, true); }
void add_diseq(pdd const& p, unsigned dep = null_dependency) { new_constraint(mk_diseq(p), dep, true); }
void add_ule(pdd const& p, pdd const& q, unsigned dep = null_dependency) { new_constraint(mk_ule(p, q), dep, true); }
void add_ult(pdd const& p, pdd const& q, unsigned dep = null_dependency) { new_constraint(mk_ult(p, q), dep, true); }
void add_sle(pdd const& p, pdd const& q, unsigned dep = null_dependency) { new_constraint(mk_sle(p, q), dep, true); }
void add_slt(pdd const& p, pdd const& q, unsigned dep = null_dependency) { new_constraint(mk_slt(p, q), dep, true); }
void add_eq(pdd const& p, unsigned dep = null_dependency) { ext_constraint(eq(p), dep, true); }
void add_diseq(pdd const& p, unsigned dep = null_dependency) { ext_constraint(diseq(p), dep, true); }
void add_ule(pdd const& p, pdd const& q, unsigned dep = null_dependency) { ext_constraint(ule(p, q), dep, true); }
void add_ult(pdd const& p, pdd const& q, unsigned dep = null_dependency) { ext_constraint(ult(p, q), dep, true); }
void add_sle(pdd const& p, pdd const& q, unsigned dep = null_dependency) { ext_constraint(sle(p, q), dep, true); }
void add_slt(pdd const& p, pdd const& q, unsigned dep = null_dependency) { ext_constraint(slt(p, q), dep, true); }
/**
* Activate the constraint corresponding to the given boolean variable.

1
src/math/polysat/trail.h
View file

@ -24,6 +24,7 @@ namespace polysat {
assign_i,
just_i,
assign_bool_i,
ext_constraint_i
};

26
src/math/polysat/ule_constraint.cpp
View file

@ -20,7 +20,9 @@ namespace polysat {
std::ostream& ule_constraint::display(std::ostream& out, lbool status) const {
out << m_lhs;
if (status == l_true) out << " <= ";
if (is_eq() && status == l_true) out << " == ";
else if (is_eq() && status == l_false) out << " != ";
else if (status == l_true) out << " <= ";
else if (status == l_false) out << " > ";
else out << " <=/> ";
out << m_rhs;
@ -45,6 +47,23 @@ namespace polysat {
return;
}
// p <= 0, e.g., p == 0
if (q.is_zero() && p.is_unilinear()) {
// a*x + b == 0
pvar v = q.var();
s.push_cjust(v, { this, is_positive });
rational a = q.hi().val();
rational b = q.lo().val();
s.m_viable.intersect_eq(a, v, b, is_positive);
rational val;
if (s.m_viable.find_viable(v, val) == dd::find_t::singleton)
s.propagate(v, val, { this, is_positive });
return;
}
pvar v = null_var;
rational a, b, c, d;
if (p.is_unilinear() && q.is_unilinear() && p.var() == q.var()) {
@ -88,8 +107,11 @@ namespace polysat {
bool ule_constraint::is_always_false(bool is_positive, pdd const& lhs, pdd const& rhs) const {
// TODO: other conditions (e.g. when forbidden interval would be full)
if (is_positive)
if (is_positive) {
if (rhs.is_zero())
return lhs.is_never_zero();
return lhs.is_val() && rhs.is_val() && lhs.val() > rhs.val();
}
else {
if (lhs.is_zero())
return true; // 0 > ... is always false

2
src/math/polysat/ule_constraint.h
View file

@ -44,6 +44,8 @@ namespace polysat {
inequality as_inequality(bool is_positive) const override;
unsigned hash() const override;
bool operator==(constraint const& other) const override;
bool is_eq() const { return m_rhs.is_zero(); }
pdd const& p() const { SASSERT(is_eq()); return m_lhs; }
};
}