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

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-01-26 21:53:10 +01:00
commit d1fcc41c7f
8 changed files with 121 additions and 48 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -78,13 +78,13 @@ namespace polysat {
SASSERT(is_propagation(lit));
}
void bool_var_manager::asserted(sat::literal lit, unsigned lvl, dep_t dep) {
void bool_var_manager::asserted(sat::literal lit, unsigned lvl, dependency dep) {
LOG("Asserted " << lit << " @ " << lvl);
assign(kind_t::decision, lit, lvl, nullptr, dep);
SASSERT(is_decision(lit));
}
void bool_var_manager::assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, dep_t dep) {
void bool_var_manager::assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, dependency dep) {
SASSERT(!is_assigned(lit));
SASSERT(k != kind_t::unassigned);
m_value[lit.index()] = l_true;

8
src/math/polysat/boolean.h
View file

@ -29,7 +29,7 @@ namespace polysat {
svector<sat::bool_var> m_unused; // previously deleted variables that can be reused by new_var();
svector<lbool> m_value; // current value (indexed by literal)
unsigned_vector m_level; // level of assignment (indexed by variable)
svector<dep_t> m_deps; // dependencies of external asserts
dependency_vector m_deps; // dependencies of external asserts
unsigned_vector m_activity; //
svector<kind_t> m_kind; // decision or propagation?
// Clause associated with the assignment (indexed by variable):
@ -40,7 +40,7 @@ namespace polysat {
var_queue m_free_vars; // free Boolean variables
vector<ptr_vector<clause>> m_watch; // watch list for literals into clauses
void assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, dep_t dep = null_dependency);
void assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, dependency dep = null_dependency);
public:
@ -66,7 +66,7 @@ namespace polysat {
unsigned level(sat::literal lit) const { return level(lit.var()); }
clause* reason(sat::bool_var var) const { SASSERT(is_assigned(var)); return is_propagation(var) ? m_clause[var] : nullptr; }
clause* reason(sat::literal lit) const { return reason(lit.var()); }
dep_t dep(sat::literal lit) const { return lit == sat::null_literal ? null_dependency : m_deps[lit.var()]; }
dependency dep(sat::literal lit) const { return lit == sat::null_literal ? null_dependency : m_deps[lit.var()]; }
clause* lemma(sat::bool_var var) const { SASSERT(is_decision(var)); return m_clause[var]; }
@ -83,7 +83,7 @@ namespace polysat {
void propagate(sat::literal lit, unsigned lvl, clause& reason);
void decide(sat::literal lit, unsigned lvl, clause& lemma);
void eval(sat::literal lit, unsigned lvl);
void asserted(sat::literal lit, unsigned lvl, dep_t dep);
void asserted(sat::literal lit, unsigned lvl, dependency dep);
void unassign(sat::literal lit);
std::ostream& display(std::ostream& out) const;

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

@ -55,14 +55,7 @@ namespace polysat {
_backtrack.released = true;
// a*v <= 0, a odd
if (ok1 && ok2 && match_zero(c, a1, b1, e1, a2, b2, e2, fi))
return true;
// v > q
// 2^k*a*v + b > 0
// TODO: is !ok2 required?
if (ok1 && !ok2 && match_non_zero(c, a1, b1, e1, fi))
return true;
@ -77,6 +70,14 @@ namespace polysat {
SASSERT(b1.is_val());
SASSERT(b2.is_val());
// a*v <= 0, a odd
if (match_zero(c, a1, b1, e1, a2, b2, e2, fi))
return true;
// a*v + b > 0, a odd
if (match_non_zero_linear(c, a1, b1, e1, a2, b2, e2, fi))
return true;
if (match_linear1(c, a1, b1, e1, a2, b2, e2, fi))
return true;
if (match_linear2(c, a1, b1, e1, a2, b2, e2, fi))
@ -271,6 +272,10 @@ namespace polysat {
/**
* a*v <= 0, a odd
* forbidden interval for v is [1,0[
*
* TODO: extend to
* 2^k*a*v <= 0, a odd
* (using periodic intervals?)
*/
bool forbidden_intervals::match_zero(
signed_constraint const& c,
@ -294,6 +299,42 @@ namespace polysat {
return false;
}
/**
* a*v + b > 0, a odd
*
* TODO: extend to
* 2^k*a*v + b > 0, a odd
* (using periodic intervals?)
*/
bool forbidden_intervals::match_non_zero_linear(
signed_constraint const& c,
rational const & a1, pdd const& b1, pdd const& e1,
rational const & a2, pdd const& b2, pdd const& e2,
fi_record& fi) {
if (c.is_negative() && a1.is_odd() && a2.is_zero() && b2.is_zero()) {
// a*v + b > 0
// <=> a*v + b != 0
// <=> v + a^-1 * b != 0
// <=> v != - a^-1 * b
auto& m = e1.manager();
rational const& mod_value = m.two_to_N();
rational a1_inv;
VERIFY(a1.mult_inverse(m.power_of_2(), a1_inv));
rational lo_val(mod(-b1.val() * a1_inv, mod_value));
auto lo = -e1 * a1_inv;
rational hi_val(mod(lo_val + 1, mod_value));
auto hi = lo + 1;
fi.coeff = 1;
fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
if (b1 != e1)
fi.side_cond.push_back(s.eq(b1, e1));
if (b2 != e2)
fi.side_cond.push_back(s.eq(b2, e2));
return true;
}
return false;
}
/**
* v > q
* forbidden interval for v is [0,1[

5
src/math/polysat/forbidden_intervals.h
View file

@ -57,6 +57,11 @@ namespace polysat {
rational const & a2, pdd const& b2, pdd const& e2,
fi_record& fi);
bool match_non_zero_linear(signed_constraint const& c,
rational const & a1, pdd const& b1, pdd const& e1,
rational const & a2, pdd const& b2, pdd const& e2,
fi_record& fi);
bool match_non_zero(signed_constraint const& c,
rational const & a1, pdd const& b1, pdd const& e1,
fi_record& fi);

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

@ -170,7 +170,7 @@ namespace polysat {
}
void solver::assign_eh(signed_constraint c, dep_t dep) {
void solver::assign_eh(signed_constraint c, dependency dep) {
SASSERT(at_base_level());
SASSERT(c);
if (is_conflict())
@ -599,7 +599,7 @@ namespace polysat {
SASSERT(!m_conflict.empty());
}
void solver::unsat_core(svector<dep_t>& deps) {
void solver::unsat_core(dependency_vector& deps) {
deps.reset();
for (auto c : m_conflict) {
auto d = m_bvars.dep(c.blit());

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

@ -256,7 +256,7 @@ namespace polysat {
/**
* retrieve unsat core dependencies
*/
void unsat_core(svector<dep_t>& deps);
void unsat_core(dependency_vector& deps);
/**
* Add variable with bit-size.
@ -316,6 +316,7 @@ namespace polysat {
signed_constraint eq(pdd const& p, rational const& q) { return eq(p - q); }
signed_constraint eq(pdd const& p, unsigned q) { return eq(p - q); }
signed_constraint diseq(pdd const& p, rational const& q) { return diseq(p - q); }
signed_constraint diseq(pdd const& p, unsigned q) { return diseq(p - q); }
signed_constraint ule(pdd const& p, pdd const& q) { return m_constraints.ule(p, q); }
signed_constraint ule(pdd const& p, rational const& q) { return ule(p, p.manager().mk_val(q)); }
signed_constraint ule(rational const& p, pdd const& q) { return ule(q.manager().mk_val(p), q); }
@ -331,33 +332,39 @@ namespace polysat {
signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); }
/** Create and activate polynomial constraints. */
void add_eq(pdd const& p, dep_t dep = null_dependency) { assign_eh(eq(p), dep); }
void add_diseq(pdd const& p, dep_t dep = null_dependency) { assign_eh(diseq(p), dep); }
void add_ule(pdd const& p, pdd const& q, dep_t dep = null_dependency) { assign_eh(ule(p, q), dep); }
void add_ult(pdd const& p, pdd const& q, dep_t dep = null_dependency) { assign_eh(ult(p, q), dep); }
void add_sle(pdd const& p, pdd const& q, dep_t dep = null_dependency) { assign_eh(sle(p, q), dep); }
void add_slt(pdd const& p, pdd const& q, dep_t dep = null_dependency) { assign_eh(slt(p, q), dep); }
void add_noovfl(pdd const& p, pdd const& q, dep_t dep = null_dependency) { assign_eh(~mul_ovfl(p, q), dep); }
void add_ovfl(pdd const& p, pdd const& q, dep_t dep = null_dependency) { assign_eh(mul_ovfl(p, q), dep); }
void add_eq(pdd const& p, dependency dep = null_dependency) { assign_eh(eq(p), dep); }
void add_eq(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(eq(p, q), dep); }
void add_eq(pdd const& p, rational const& q, dependency dep = null_dependency) { assign_eh(eq(p, q), dep); }
void add_eq(pdd const& p, unsigned q, dependency dep = null_dependency) { assign_eh(eq(p, q), dep); }
void add_diseq(pdd const& p, dependency dep = null_dependency) { assign_eh(diseq(p), dep); }
void add_diseq(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(diseq(p, q), dep); }
void add_diseq(pdd const& p, rational const& q, dependency dep = null_dependency) { assign_eh(diseq(p, q), dep); }
void add_diseq(pdd const& p, unsigned q, dependency dep = null_dependency) { assign_eh(diseq(p, q), dep); }
void add_ule(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(ule(p, q), dep); }
void add_ult(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(ult(p, q), dep); }
void add_sle(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(sle(p, q), dep); }
void add_slt(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(slt(p, q), dep); }
void add_noovfl(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(~mul_ovfl(p, q), dep); }
void add_ovfl(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(mul_ovfl(p, q), dep); }
void add_ule(pdd const& p, rational const& q, dep_t dep = null_dependency) { add_ule(p, p.manager().mk_val(q), dep); }
void add_ule(rational const& p, pdd const& q, dep_t dep = null_dependency) { add_ule(q.manager().mk_val(p), q, dep); }
void add_ule(pdd const& p, unsigned q, dep_t dep = null_dependency) { add_ule(p, rational(q), dep); }
void add_ule(unsigned p, pdd const& q, dep_t dep = null_dependency) { add_ule(rational(p), q, dep); }
void add_ult(pdd const& p, rational const& q, dep_t dep = null_dependency) { add_ult(p, p.manager().mk_val(q), dep); }
void add_ult(rational const& p, pdd const& q, dep_t dep = null_dependency) { add_ult(q.manager().mk_val(p), q, dep); }
void add_ult(pdd const& p, unsigned q, dep_t dep = null_dependency) { add_ult(p, rational(q), dep); }
void add_ult(unsigned p, pdd const& q, dep_t dep = null_dependency) { add_ult(rational(p), q, dep); }
void add_noovfl(pdd const& p, rational const& q, dep_t dep = null_dependency) { add_noovfl(p, p.manager().mk_val(q), dep); }
void add_noovfl(rational const& p, pdd const& q, dep_t dep = null_dependency) { add_noovfl(q, p, dep); }
void add_noovfl(pdd const& p, unsigned q, dep_t dep = null_dependency) { add_noovfl(p, rational(q), dep); }
void add_noovfl(unsigned p, pdd const& q, dep_t dep = null_dependency) { add_noovfl(q, p, dep); }
void add_ule(pdd const& p, rational const& q, dependency dep = null_dependency) { add_ule(p, p.manager().mk_val(q), dep); }
void add_ule(rational const& p, pdd const& q, dependency dep = null_dependency) { add_ule(q.manager().mk_val(p), q, dep); }
void add_ule(pdd const& p, unsigned q, dependency dep = null_dependency) { add_ule(p, rational(q), dep); }
void add_ule(unsigned p, pdd const& q, dependency dep = null_dependency) { add_ule(rational(p), q, dep); }
void add_ult(pdd const& p, rational const& q, dependency dep = null_dependency) { add_ult(p, p.manager().mk_val(q), dep); }
void add_ult(rational const& p, pdd const& q, dependency dep = null_dependency) { add_ult(q.manager().mk_val(p), q, dep); }
void add_ult(pdd const& p, unsigned q, dependency dep = null_dependency) { add_ult(p, rational(q), dep); }
void add_ult(unsigned p, pdd const& q, dependency dep = null_dependency) { add_ult(rational(p), q, dep); }
void add_noovfl(pdd const& p, rational const& q, dependency dep = null_dependency) { add_noovfl(p, p.manager().mk_val(q), dep); }
void add_noovfl(rational const& p, pdd const& q, dependency dep = null_dependency) { add_noovfl(q, p, dep); }
void add_noovfl(pdd const& p, unsigned q, dependency dep = null_dependency) { add_noovfl(p, rational(q), dep); }
void add_noovfl(unsigned p, pdd const& q, dependency dep = null_dependency) { add_noovfl(q, p, dep); }
/**
* Activate the constraint corresponding to the given boolean variable.
* Note: to deactivate, use push/pop.
*/
void assign_eh(signed_constraint c, dep_t dep);
void assign_eh(signed_constraint c, dependency dep);
/**
* Unit propagation accessible over API.

26
src/math/polysat/types.h
View file

@ -28,9 +28,29 @@ namespace polysat {
typedef dd::pdd pdd;
typedef dd::bdd bdd;
typedef dd::bddv bddv;
typedef unsigned pvar;
typedef unsigned dep_t;
const dep_t null_dependency = std::numeric_limits<unsigned>::max();;
const pvar null_var = UINT_MAX;
inline const pvar null_var = UINT_MAX;
class dependency {
unsigned m_val;
public:
explicit dependency(unsigned val): m_val(val) {}
unsigned val() const { return m_val; }
bool is_null() const { return m_val == UINT_MAX; }
unsigned hash() const { return val(); }
};
inline const dependency null_dependency = dependency(UINT_MAX);
typedef svector<dependency> dependency_vector;
inline bool operator<(dependency const& d1, dependency const& d2) { return d1.val() < d2.val(); }
inline bool operator==(dependency const& d1, dependency const& d2) { return d1.val() == d2.val(); }
inline bool operator!=(dependency const& d1, dependency const& d2) { return d1.val() != d2.val(); }
inline std::ostream& operator<<(std::ostream& out, dependency const& d) {
out << "dep(" << d.val() << ")";
return out;
}
}