mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

working on SLS

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-03-19 15:53:28 -07:00
parent a9281777cc
commit 2909e8cd9e
1 changed files with 0 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/opt/weighted_maxsat.cpp
View file

@ -552,7 +552,6 @@ namespace opt {
for (unsigned i = 0; i < m_soft.size(); ++i) { for (unsigned i = 0; i < m_soft.size(); ++i) {
wth().assert_weighted(m_soft[i].get(), m_weights[i]); wth().assert_weighted(m_soft[i].get(), m_weights[i]);
} }
s.display(std::cout);
solver::scoped_push __s(s); solver::scoped_push __s(s);
while (l_true == is_sat) { while (l_true == is_sat) {
@ -601,7 +600,6 @@ namespace opt {
ws.push_back(wth().assert_weighted(m_soft[i].get(), m_weights[i])); ws.push_back(wth().assert_weighted(m_soft[i].get(), m_weights[i]));
sls.add(m_soft[i].get(), m_weights[i]); sls.add(m_soft[i].get(), m_weights[i]);
} }
s.display(std::cout);
expr_ref fml(m); expr_ref fml(m);
solver::scoped_push __s(s); solver::scoped_push __s(s);