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

add PB operators to C-based API

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-11-13 17:09:10 -08:00
parent 133ba2d02a
commit d1937b2032
8 changed files with 77 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/opt/core_maxsat.cpp
View file

@ -65,6 +65,7 @@ namespace opt {
for (unsigned i = 0; i < ans.size(); ++i) {
tout << mk_pp(ans[i].get(), m) << "\n";
});
IF_VERBOSE(1, verbose_stream() << "(maxsat.core sat: " << ans.size() << "\n";);
if (ans.size() > m_answer.size()) {
m_answer.reset();
m_answer.append(ans);
@ -91,6 +92,7 @@ namespace opt {
core_vars.insert(get_not(core[i]));
block_vars.remove(core[i]);
}
IF_VERBOSE(1, verbose_stream() << "(maxsat.core unsat (core size = " << core.size() << ")\n";);
if (core.empty()) {
m_upper = m_answer.size();
return l_true;

2
src/opt/fu_malik.cpp
View file

@ -73,7 +73,7 @@ namespace opt {
*/
lbool step() {
IF_VERBOSE(1, verbose_stream() << "(opt.max_sat step)\n";);
IF_VERBOSE(1, verbose_stream() << "(opt.max_sat step)\n";); // add some count, add some information of # of soft constraints still possibly sat.
expr_ref_vector assumptions(m), block_vars(m);
for (unsigned i = 0; i < m_soft.size(); ++i) {
assumptions.push_back(m.mk_not(m_aux[i].get()));