141 lbool prop_solver::mss(expr_ref_vector &hard, expr_ref_vector &soft) {  in mss()  argument
143     iuc_solver::scoped_mk_proxy _p_(*m_ctx, hard);  in mss()
144     unsigned hard_sz = hard.size();  in mss()
146     lbool res = m_ctx->check_sat(hard.size(), hard.data());  in mss()
157     hard.append(soft);  in mss()
170     while (j < hard.size()) {  in mss()
174         for (unsigned k = j; k < hard.size(); ++k) {  in mss()
176             e = hard.get(k);  in mss()
179                 tmp = hard.get(i);  in mss()
180                 hard[i] = e;  in mss()
183                     if (j == k) {hard[j] = tmp;}  in mss()
185                         e = hard.get(j);  in mss()
186                         hard[j] = tmp;  in mss()
187                         hard[k] = e;  in mss()
193                     hard[k] = tmp;  in mss()
204         for (;j < hard.size(); ++j) {  in mss()
205             res = m_ctx->check_sat(j+1, hard.data());  in mss()
208                 hard[j] = mk_not(m, hard.get(j));  in mss()
217                 hard.resize(hard_sz);  in mss()
224     for (unsigned k = i; k < j; ++k) { soft.push_back(hard.get(k)); }  in mss()
226     hard.resize(hard_sz);  in mss()
233 lbool prop_solver::maxsmt(expr_ref_vector &hard, expr_ref_vector &soft,  in maxsmt()  argument
237     iuc_solver::scoped_mk_proxy _p_(*m_ctx, hard);  in maxsmt()
238     unsigned hard_sz = hard.size();  in maxsmt()
240     hard.append(soft);  in maxsmt()
242     lbool res = m_ctx->check_sat_cc(hard, clauses);  in maxsmt()
255     while (hard.size() > hard_sz) {  in maxsmt()
258         for (unsigned i = hard_sz, sz = hard.size(); i < sz; ++i)  in maxsmt()
259             if (core.contains(hard.get(i))) {  in maxsmt()
262                 saved = hard.get(i);  in maxsmt()
263                 hard[i] = hard.back();  in maxsmt()
264                 hard.pop_back();  in maxsmt()
271             hard.resize(hard_sz);  in maxsmt()
276         res = m_ctx->check_sat_cc(hard, clauses);  in maxsmt()
285         for (unsigned i = hard_sz, sz = hard.size(); i < sz; ++i)  in maxsmt()
286         { soft.push_back(hard.get(i)); }  in maxsmt()
290     hard.resize(hard_sz);  in maxsmt()
365     expr_ref_vector hard(m);  in check_assumptions()  local
366     hard.append(_hard.size(), _hard.data());  in check_assumptions()
367     flatten_and(hard);  in check_assumptions()
369     shuffle(hard.size(), hard.data(), m_random);  in check_assumptions()
386     lbool res = internal_check_assumptions(hard, soft, clauses);  in check_assumptions()
390           tout << "sat: " << mk_pp(mk_and(hard), m) << "\n"  in check_assumptions()