mirror of
https://github.com/Z3Prover/z3
synced 2025-06-23 06:13:40 +00:00
working on weighted maxsat
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
d30f183476
commit
1878d64b02
1 changed files with 3 additions and 0 deletions
|
@ -166,6 +166,9 @@ namespace opt {
|
||||||
}
|
}
|
||||||
lbool result = s.check_sat_core(0,0);
|
lbool result = s.check_sat_core(0,0);
|
||||||
wth->get_assignment(soft_constraints);
|
wth->get_assignment(soft_constraints);
|
||||||
|
if (!soft_constraints.empty() && result == l_false) {
|
||||||
|
result = l_true;
|
||||||
|
}
|
||||||
return result;
|
return result;
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue