mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-04-13 12:22:49 +02:00
commit f1b10b0ea4
3 changed files with 18 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -57,7 +57,7 @@ namespace polysat {
if (!m_out)
m_out = alloc(std::ofstream, "conflicts.txt");
else
out() << "\n\n\n\n\n" << hline() << "\n" << hline() << "\n" << hline() << "\n\n\n\n\n";
out() << "\n\n\n\n\n\n\n\n\n\n\n\n";
out() << "CONFLICT #" << ++m_conflicts << "\n";
}
@ -74,13 +74,15 @@ namespace polysat {
m_used_constraints.insert(c.blit().index());
}
for (auto v : core.vars()) {
out_indent() << "v" << v << "\n";
out_indent() << "v" << v << " := " << core.s.get_value(v) << "\n";
m_used_vars.insert(v);
}
for (auto v : core.bail_vars()) {
out_indent() << "v" << v << " (bail)\n";
out_indent() << "v" << v << " := " << core.s.get_value(v) << " (bail)\n";
m_used_vars.insert(v);
}
if (core.is_bailout())
out_indent() << "(bailout)\n";
out().flush();
}

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

@ -106,6 +106,7 @@ namespace polysat {
uint_set m_vars; // variable assignments used as premises
uint_set m_bail_vars;
friend class inference_logger;
scoped_ptr<inference_logger> m_logger;
// If this is not null_var, the conflict was due to empty viable set for this variable.

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

@ -143,6 +143,17 @@ namespace polysat {
}
}
struct inference_sup : public inference {
const char* name;
pvar var;
signed_constraint reduced;
signed_constraint reducer;
inference_sup(const char* name, pvar var, signed_constraint reduced, signed_constraint reducer) : name(name), var(var), reduced(reduced), reducer(reducer) {}
std::ostream& display(std::ostream& out) const override {
return out << "Superposition " << name << ", reduced v" << var << " in " << reduced << " by " << reducer;
}
};
bool ex_polynomial_superposition::reduce_by(pvar v, signed_constraint eq, conflict& core) {
pdd p = eq.eq();
LOG("using v" << v << " " << eq);
@ -189,7 +200,7 @@ namespace polysat {
return true;
}
core.set(c2);
core.log_inference("superposition 5");
core.log_inference(inference_sup("5", v, c, eq));
return true;
}
return false;