mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 14:53:40 +00:00
Code Activity

forbidden intervals create a lemma

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-08 06:54:36 +02:00
parent 8bcec83ee8
commit 7980b05cc1
2 changed files with 11 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/math/polysat/forbidden_intervals.cpp
View file

@ -73,13 +73,13 @@ namespace polysat {
* We assume that neg_cond is a consequence of src that * We assume that neg_cond is a consequence of src that
* does not mention the variable v to be eliminated. * does not mention the variable v to be eliminated.
*/ */
void forbidden_intervals::full_interval_conflict(signed_constraint src, signed_constraint neg_cond, conflict_core& core) { void forbidden_intervals::full_interval_conflict(signed_constraint src, signed_constraint neg_cond, clause_builder& lemma) {
SASSERT(neg_cond); SASSERT(neg_cond);
core.insert(~neg_cond); lemma.push(neg_cond);
core.remove(src); // or add a lemma? lemma.push(~src);
} }
bool forbidden_intervals::perform(solver& s, pvar v, conflict_core& core) { bool forbidden_intervals::perform(solver& s, pvar v, conflict_core& core, clause_builder& lemma) {
// Extract forbidden intervals from conflicting constraints // Extract forbidden intervals from conflicting constraints
vector<fi_record> records; vector<fi_record> records;
@ -97,7 +97,7 @@ namespace polysat {
if (interval.is_full()) { if (interval.is_full()) {
// We have a single interval covering the whole domain // We have a single interval covering the whole domain
// => the side conditions of that interval are enough to produce a conflict // => the side conditions of that interval are enough to produce a conflict
full_interval_conflict(c, neg_cond, core); full_interval_conflict(c, neg_cond, lemma);
return true; return true;
} }
else { else {
@ -161,14 +161,14 @@ namespace polysat {
// the level of a literal is when it was assigned. Lemmas could have unassigned literals. // the level of a literal is when it was assigned. Lemmas could have unassigned literals.
signed_constraint c = s.m_constraints.ult(lemma_lvl, lhs, rhs); signed_constraint c = s.m_constraints.ult(lemma_lvl, lhs, rhs);
LOG("constraint: " << c); LOG("constraint: " << c);
core.insert(c); lemma.push(~c);
// Side conditions // Side conditions
// TODO: check whether the condition is subsumed by c? maybe at the end do a "lemma reduction" step, to try and reduce branching? // TODO: check whether the condition is subsumed by c? maybe at the end do a "lemma reduction" step, to try and reduce branching?
signed_constraint& neg_cond = records[i].neg_cond; signed_constraint& neg_cond = records[i].neg_cond;
if (neg_cond) if (neg_cond)
core.insert(std::move(~neg_cond)); lemma.push(std::move(neg_cond));
core.remove(records[i].src); lemma.push(~records[i].src);
} }
return true; return true;
} }

6
src/math/polysat/forbidden_intervals.h
View file

@ -20,10 +20,10 @@ Author:
namespace polysat { namespace polysat {
class forbidden_intervals : public variable_elimination_engine { class forbidden_intervals {
void full_interval_conflict(signed_constraint c, signed_constraint neg_cond, conflict_core& core); void full_interval_conflict(signed_constraint c, signed_constraint neg_cond, clause_builder& lemma);
bool get_interval(solver& s, signed_constraint const& c, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond); bool get_interval(solver& s, signed_constraint const& c, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond);
public: public:
bool perform(solver& s, pvar v, conflict_core& core) override; bool perform(solver& s, pvar v, conflict_core& core, clause_builder& lemma);
}; };
} }