mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

only assign, if there isn't already a true literal incube/clause mode

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-09 10:33:56 -07:00
parent efe440839e
commit 8373bec6ad
1 changed files with 9 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/smt/smt_context.cpp
View file

@ -3186,6 +3186,7 @@ namespace smt {
if (m_tmp_clauses.empty()) return l_true; if (m_tmp_clauses.empty()) return l_true;
for (auto & tmp_clause : m_tmp_clauses) { for (auto & tmp_clause : m_tmp_clauses) {
literal_vector& lits = tmp_clause.second; literal_vector& lits = tmp_clause.second;
literal unassigned = null_literal;
for (literal l : lits) { for (literal l : lits) {
switch (get_assignment(l)) { switch (get_assignment(l)) {
case l_false: case l_false:
@ -3193,12 +3194,16 @@ namespace smt {
case l_true: case l_true:
goto next_clause; goto next_clause;
default: default:
unassigned = l;
}
}
if (unassigned != null_literal) {
shuffle(lits.size(), lits.c_ptr(), m_random); shuffle(lits.size(), lits.c_ptr(), m_random);
push_scope(); push_scope();
assign(l, b_justification::mk_axiom(), true); assign(unassigned, b_justification::mk_axiom(), true);
return l_undef; return l_undef;
} }
}
if (lits.size() == 1) { if (lits.size() == 1) {
set_conflict(b_justification(), ~lits[0]); set_conflict(b_justification(), ~lits[0]);