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

use vectors instead of hash-tables in dimacs serialization to avoid hash-table contention

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-12 11:05:00 -08:00
parent e623f1e9c9
commit e4d6aa07dc
3 changed files with 26 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/sat_solver.cpp
View file

@ -344,11 +344,11 @@ namespace sat {
void solver::mk_bin_clause(literal l1, literal l2, bool learned) {
if (find_binary_watch(get_wlist(~l1), ~l2)) {
assign_core(l1, 0, justification(l2));
assign_core(l1, 0, justification(l1));
return;
}
if (find_binary_watch(get_wlist(~l2), ~l1)) {
assign_core(l2, 0, justification(l1));
assign_core(l2, 0, justification(l2));
return;
}
watched* w0 = find_binary_watch(get_wlist(~l1), l2);