mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-01 02:18:46 +00:00
Code Activity

polynomial superposition needs a different constraint query

Browse source
This commit is contained in:
Jakob Rath 2023-12-14 15:43:43 +01:00
parent 6bde7e2c8c
commit d59b6e4efa
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/polysat/superposition.cpp
View file

@ -64,6 +64,8 @@ namespace polysat {
// c2 ... constraint that is currently false // c2 ... constraint that is currently false
// Try to replace it with a new false constraint (derived from superposition with a true constraint) // Try to replace it with a new false constraint (derived from superposition with a true constraint)
lbool ex_polynomial_superposition::find_replacement(signed_constraint c2, pvar v, conflict& core) { lbool ex_polynomial_superposition::find_replacement(signed_constraint c2, pvar v, conflict& core) {
#if 0
// TODO: propagation_reason is the wrong thing here; we could query the fallback solver for constraints in v
for (sat::literal lit1 : s.m_viable.get_propagation_reason(v)) { for (sat::literal lit1 : s.m_viable.get_propagation_reason(v)) {
signed_constraint c1 = s.lit2cnstr(lit1); signed_constraint c1 = s.lit2cnstr(lit1);
if (!c1->contains_var(v)) // side conditions and interval endpoint constraints do not contain v; skip them here if (!c1->contains_var(v)) // side conditions and interval endpoint constraints do not contain v; skip them here
@ -99,6 +101,7 @@ namespace polysat {
// core.log_inference(inference_sup(inf_name, v, c2, c1)); // core.log_inference(inference_sup(inf_name, v, c2, c1));
return c->contains_var(v) ? l_undef : l_true; return c->contains_var(v) ? l_undef : l_true;
} }
#endif
return l_false; return l_false;
} }