mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-13 02:34:43 +00:00
Code Activity

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-07 15:09:28 +02:00
commit 9450ac0d18
8 changed files with 88 additions and 80 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -66,6 +66,9 @@ namespace polysat {
bool forbidden_intervals::explain(solver& s, vector<signed_constraint> const& conflict, pvar v, clause_ref& out_lemma) {
return false;
#if 0
// Extract forbidden intervals from conflicting constraints
vector<fi_record> records;
bool has_full = false;
@ -174,6 +177,7 @@ namespace polysat {
}
out_lemma = clause.build();
return true;
#endif
}
}