mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
working on maxres
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
83a7d1a658
commit
afe7fc367b
|
@ -503,7 +503,8 @@ public:
|
|||
TRACE("opt", display_vec(tout << "corr_set: ", corr_set.size(), corr_set.c_ptr()););
|
||||
remove_core(corr_set);
|
||||
rational w = split_core(corr_set);
|
||||
cs_max_resolve(corr_set, w);
|
||||
cs_max_resolve(corr_set, w);
|
||||
IF_VERBOSE(2, verbose_stream() << "(opt.maxres.correction-set " << corr_set.size() << ")\n";);
|
||||
}
|
||||
|
||||
lbool process_unsat() {
|
||||
|
|
|
@ -136,7 +136,6 @@ namespace opt {
|
|||
m_wth = s.ensure_wmax_theory();
|
||||
}
|
||||
maxsmt_solver_base::scoped_ensure_theory::~scoped_ensure_theory() {
|
||||
//m_wth->reset();
|
||||
}
|
||||
smt::theory_wmaxsat& maxsmt_solver_base::scoped_ensure_theory::operator()() { return *m_wth; }
|
||||
|
||||
|
|
|
@ -40,7 +40,6 @@ namespace opt {
|
|||
lbool operator()() {
|
||||
TRACE("opt", tout << "weighted maxsat\n";);
|
||||
scoped_ensure_theory wth(*this);
|
||||
solver::scoped_push _s1(s());
|
||||
lbool is_sat = l_true;
|
||||
bool was_sat = false;
|
||||
for (unsigned i = 0; i < m_soft.size(); ++i) {
|
||||
|
|
|
@ -171,7 +171,6 @@ void theory_wmaxsat::reset_local() {
|
|||
m_vars.reset();
|
||||
m_fmls.reset();
|
||||
m_rweights.reset();
|
||||
m_costs.reset();
|
||||
m_rmin_cost.reset();
|
||||
m_rcost.reset();
|
||||
m_zweights.reset();
|
||||
|
|
Loading…
Reference in a new issue