mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-07-02 03:33:51 -07:00
parent 788de7d614
commit 9e69e1614e
3 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -217,7 +217,7 @@ namespace polysat {
constraint_literal& operator=(nullptr_t) { m_literal = sat::null_literal; m_constraint = nullptr; return *this; } constraint_literal& operator=(nullptr_t) { m_literal = sat::null_literal; m_constraint = nullptr; return *this; }
private: private:
friend class constraint_manager; friend class constraint_manager;
explicit constraint_literal(polysat::constraint* c): constraint_literal(sat::literal(c->bvar()), c) {} explicit constraint_literal(constraint* c): constraint_literal(sat::literal(c->bvar()), c) {}
}; };

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

@ -19,7 +19,7 @@ Author:
namespace polysat { namespace polysat {
std::ostream& eq_constraint::display(std::ostream& out) const { std::ostream& eq_constraint::display(std::ostream& out) const {
out << p() << (is_positive() ? " == 0 " : " != 0"); out << p() << " == 0";
return display_extra(out); return display_extra(out);
} }

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

@ -91,6 +91,7 @@ namespace polysat {
clause_ref conflict_explainer::by_polynomial_superposition() { clause_ref conflict_explainer::by_polynomial_superposition() {
LOG_H3("units-size: " << m_conflict.units().size() << " conflict-clauses " << m_conflict.clauses().size()); LOG_H3("units-size: " << m_conflict.units().size() << " conflict-clauses " << m_conflict.clauses().size());
constraint* c1 = nullptr, *c2 = nullptr; constraint* c1 = nullptr, *c2 = nullptr;
if (m_conflict.units().size() == 2 && m_conflict.clauses().size() == 0) { if (m_conflict.units().size() == 2 && m_conflict.clauses().size() == 0) {
c1 = m_conflict.units()[0]; c1 = m_conflict.units()[0];
c2 = m_conflict.units()[1]; c2 = m_conflict.units()[1];
@ -111,6 +112,8 @@ namespace polysat {
if (lit.sign()) if (lit.sign())
continue; continue;
constraint* c = m_solver.m_constraints.lookup(lit.var()); constraint* c = m_solver.m_constraints.lookup(lit.var());
c->assign(true);
// this clause is really a unit.
LOG("unit clause: " << *c); LOG("unit clause: " << *c);
if (c->is_eq() && c->is_positive()) { if (c->is_eq() && c->is_positive()) {
c1 = c; c1 = c;
@ -127,7 +130,6 @@ namespace polysat {
break; break;
} }
} }
std::cout << c1 << " " << c2 << "\n";
#endif #endif
} }
if (!c1 || !c2 || c1 == c2) if (!c1 || !c2 || c1 == c2)