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

fix logic for disabling theory case split heuristic (#4397)

Browse source
This commit is contained in:
Murphy Berzish 2020-05-28 11:57:44 -05:00 • committed by GitHub
parent 71ea7287bb
commit 3b0c8a7ff9
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 8 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/smt/smt_context.cpp
View file

@ -2939,12 +2939,14 @@ namespace smt {
// If we don't use the theory case split heuristic,
// for each pair of literals (l1, l2) we add the clause (~l1 OR ~l2)
// to enforce the condition that at most one literal can be assigned 'true'.
if (!m_fparams.m_theory_case_split && !m.proofs_enabled()) {
for (unsigned i = 0; i < num_lits; ++i) {
for (unsigned j = i+1; j < num_lits; ++j) {
literal l1 = lits[i];
literal l2 = lits[j];
mk_clause(~l1, ~l2, (justification*) nullptr);
if (!m_fparams.m_theory_case_split) {
if (!m.proofs_enabled()) {
for (unsigned i = 0; i < num_lits; ++i) {
for (unsigned j = i + 1; j < num_lits; ++j) {
literal l1 = lits[i];
literal l2 = lits[j];
mk_clause(~l1, ~l2, (justification*) nullptr);
}
}
}
} else {