mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

use unsat_core from viable_fallback

Browse source
This commit is contained in:
Jakob Rath 2022-08-26 16:35:12 +02:00
parent acf9976df9
commit 68e313ed24
2 changed files with 11 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/math/polysat/conflict2.cpp
View file

@ -68,16 +68,21 @@ namespace polysat {
SASSERT(!empty());
}
void conflict2::init(pvar v) {
void conflict2::init(pvar v, bool by_viable_fallback) {
// NOTE: do forbidden interval projection in this method (rather than keeping a separate state like we did before)
// Option 1: forbidden interval projection
// Option 2: add all constraints from m_viable + dependent variables
// TODO: we need to know whether the conflict is from m_viable for m_viable_fallback
// - m_viable: standard forbidden interval lemma
// - m_viable_fallback: initial conflict is the unsat core of the univariate solver
// (a flag on this method might be good enough)
if (by_viable_fallback) {
// Conflict detected by viable fallback:
// initial conflict is the unsat core of the univariate solver
signed_constraints unsat_core = s.m_viable_fallback.unsat_core(v);
for (auto c : unsat_core)
insert(c);
return;
}
// TODO:
// VERIFY(s.m_viable.resolve(v, *this));
// log_inference(inf_fi_lemma(v));
}

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

@ -114,7 +114,7 @@ namespace polysat {
/** conflict because the constraint c is false under current variable assignment */
void init(signed_constraint c);
/** conflict because there is no viable value for the variable v */
void init(pvar v);
void init(pvar v, bool by_viable_fallback = false);
bool contains(signed_constraint c) const { SASSERT(c); return contains(c.blit()); }
bool contains(sat::literal lit) const;