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

nits

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-12 18:30:55 +02:00
parent e365ad0e9e
commit 8bc4932092
2 changed files with 15 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/math/polysat/conflict_core.cpp
View file

@ -201,7 +201,7 @@ namespace polysat {
clause_builder conflict_core::build_fallback_lemma(unsigned lvl) {
LOG_H3("Creating fallback lemma for level " << lvl);
LOG_V("m_search: " << s().m_search);
clause_builder lemma(*m_solver);
clause_builder lemma(s());
unsigned todo = lvl;
unsigned i = 0;
while (todo > 0) {
@ -211,7 +211,7 @@ namespace polysat {
LOG_V("Adding: " << item);
if (item.is_assignment()) {
pvar v = item.var();
auto c = ~cm().eq(s().var(v) - s().m_value[v]);
auto c = ~s().eq(s().var(v), s().get_value(v));
cm().ensure_bvar(c.get());
lemma.push(c.blit());
} else {
@ -227,7 +227,7 @@ namespace polysat {
LOG_H3("Build lemma from core");
LOG("core: " << *this);
LOG("model_level: " << model_level);
clause_builder lemma(*m_solver);
clause_builder lemma(s());
for (auto c : m_constraints) {
if (!c->has_bvar())
@ -241,9 +241,9 @@ namespace polysat {
// SASSERT(!s().is_assigned(v)); // TODO: why does this trigger????
if (!s().is_assigned(v))
continue;
if (s().m_justification[v].level() > model_level)
if (s().get_level(v) > model_level)
continue;
auto diseq = ~cm().eq(s().var(v) - s().m_value[v]);
auto diseq = ~s().eq(s().var(v), s().get_value(v));
cm().ensure_bvar(diseq.get());
lemma.push(diseq);
}
@ -288,10 +288,10 @@ namespace polysat {
// No value resolution method was successful => fall back to saturation and variable elimination
while (s().inc()) {
// TODO: as a last resort, substitute v by m_value[v]?
if (!try_saturate(v))
break;
if (try_eliminate(v))
return true;
if (!try_saturate(v))
break;
}
m_vars.insert(v);
return false;

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

@ -211,6 +211,10 @@ namespace polysat {
signed_constraint eq(pdd const& p);
signed_constraint diseq(pdd const& p);
signed_constraint eq(pdd const& p, pdd const& q) { return eq(p - q); }
signed_constraint diseq(pdd const& p, pdd const& q) { return diseq(p - q); }
signed_constraint eq(pdd const& p, rational const& q) { return eq(p - q); }
signed_constraint diseq(pdd const& p, rational const& q) { return diseq(p - q); }
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);
@ -275,9 +279,11 @@ namespace polysat {
pdd value(rational const& v, unsigned sz);
/**
* Return value of v in the current model (only meaningful if check_sat() returned l_true).
* Return value / level of v in the current model (only meaningful if check_sat() returned l_true).
*/
rational get_value(pvar v) const { SASSERT(!m_justification[v].is_unassigned()); return m_value[v]; }
rational get_value(pvar v) const { SASSERT(is_assigned(v)); return m_value[v]; }
unsigned get_level(pvar v) const { SASSERT(is_assigned(v)); return m_justification[v].level(); }
/**
* Create polynomial constraints (but do not activate them).