mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-05 14:55:45 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-12-11 17:38:09 -08:00
parent 59acd77981
commit f1d46b58a4
5 changed files with 39 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -147,10 +147,6 @@ namespace polysat {
if (c.is_eq())
continue;
LOG("try-reduce: " << c << " " << c.is_currently_false(s));
#if 0
if (!c.is_currently_false(s))
continue;
#endif
if (!c->is_ule())
continue;
auto lhs = c->to_ule().lhs();
@ -166,9 +162,13 @@ namespace polysat {
LOG("try-reduce is false " << c2.is_currently_false(s));
if (!c2.is_currently_false(s))
continue;
SASSERT(c2.is_currently_false(s));
if (!c2->has_bvar() || l_undef == c2.bvalue(s))
core.keep(c2); // adds propagation of c to the search stack
if (!c2->has_bvar() || l_undef == c2.bvalue(s)) {
vector<signed_constraint> premises;
premises.push_back(c);
premises.push_back(eq);
core.insert(c2, premises);
}
// core.keep(c2); // adds propagation of c to the search stack
core.reset();
LOG_H3("Polynomial superposition " << eq << " " << c << " reduced to " << c2);
if (c2.bvalue(s) == l_false) {

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

@ -782,7 +782,7 @@ namespace polysat {
LOG("Lemma: " << lemma);
for (sat::literal lit : lemma) {
LOG(" Literal " << lit << " is: " << lit2cnstr(lit));
SASSERT(m_bvars.value(lit) != l_true);
// SASSERT(m_bvars.value(lit) != l_true);
}
SASSERT(!lemma.empty());
m_constraints.store(&lemma, *this);