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

Blast only one bit per conflict

Browse source
This commit is contained in:
Clemens Eisenhofer 2023-02-17 17:26:19 +01:00
parent a6fbd71c6b
commit ae70a8e9f0
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/polysat/op_constraint.cpp
View file

@ -545,11 +545,11 @@ namespace polysat {
if (rb == (pb && qb))
continue;
if (pb && qb && !rb)
s.add_clause(s.mk_clause(~andc, ~s.bit(p(), i), ~s.bit(q(), i), s.bit(r(), i), true));
return s.mk_clause(~andc, ~s.bit(p(), i), ~s.bit(q(), i), s.bit(r(), i), true);
else if (!pb && rb)
s.add_clause(s.mk_clause(~andc, s.bit(p(), i), ~s.bit(r(), i), true));
return s.mk_clause(~andc, s.bit(p(), i), ~s.bit(r(), i), true);
else if (!qb && rb)
s.add_clause(s.mk_clause(~andc, s.bit(q(), i), ~s.bit(r(), i), true));
return s.mk_clause(~andc, s.bit(q(), i), ~s.bit(r(), i), true);
else
UNREACHABLE();
}