mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
parent
0c32989144
commit
e187023304
|
@ -351,6 +351,7 @@ namespace opt {
|
|||
void context::get_model_core(model_ref& mdl) {
|
||||
mdl = m_model;
|
||||
fix_model(mdl);
|
||||
mdl->set_model_completion(true);
|
||||
TRACE("opt", tout << *mdl;);
|
||||
}
|
||||
|
||||
|
@ -528,7 +529,7 @@ namespace opt {
|
|||
k += obj.m_weights[i];
|
||||
}
|
||||
else {
|
||||
TRACE("opt", tout << val << "\n";);
|
||||
TRACE("opt", tout << (*mdl)(obj.m_terms[i]) << "\n";);
|
||||
}
|
||||
}
|
||||
if (is_ge) {
|
||||
|
@ -1539,6 +1540,7 @@ namespace opt {
|
|||
expr_ref tmp(m);
|
||||
model_ref mdl;
|
||||
get_model(mdl);
|
||||
mdl->set_model_completion(true);
|
||||
for (expr * f : fmls) {
|
||||
if (!mdl->is_true(f)) {
|
||||
//IF_VERBOSE(0, m_fm->display(verbose_stream() << "fm\n"));
|
||||
|
|
|
@ -40,6 +40,7 @@ namespace opt {
|
|||
}
|
||||
m_solver->get_model(m_model);
|
||||
m_solver->get_labels(m_labels);
|
||||
m_model->set_model_completion(true);
|
||||
IF_VERBOSE(1,
|
||||
model_ref mdl(m_model);
|
||||
cb.fix_model(mdl);
|
||||
|
@ -99,6 +100,7 @@ namespace opt {
|
|||
if (is_sat == l_true) {
|
||||
m_solver->get_model(m_model);
|
||||
m_solver->get_labels(m_labels);
|
||||
m_model->set_model_completion(true);
|
||||
mk_not_dominated_by();
|
||||
}
|
||||
return is_sat;
|
||||
|
|
|
@ -93,11 +93,8 @@ private:
|
|||
obj_hashtable<func_decl> const & consts,
|
||||
ptr_vector<func_decl> & next_consts) {
|
||||
TRACE("sine",
|
||||
tout << "size of consts is "; tout << consts.size(); tout << "\n";
|
||||
obj_hashtable<func_decl>::iterator it = consts.begin();
|
||||
obj_hashtable<func_decl>::iterator end = consts.end();
|
||||
for (; it != end; it++)
|
||||
tout << *it << "\n"; );
|
||||
tout << "size of consts is "; tout << consts.size(); tout << "\n";
|
||||
for (func_decl* f : consts) tout << f->get_name() << "\n";);
|
||||
|
||||
bool matched = false;
|
||||
for (unsigned i = 0; i < q->get_num_patterns(); i++) {
|
||||
|
@ -156,10 +153,8 @@ private:
|
|||
if (!consts.contains(f)) {
|
||||
consts.insert(f);
|
||||
if (const2quantifier.contains(f)) {
|
||||
obj_pair_hashtable<expr, expr>::iterator it = const2quantifier[f].begin();
|
||||
obj_pair_hashtable<expr, expr>::iterator end = const2quantifier[f].end();
|
||||
for (; it != end; it++)
|
||||
stack.push_back(*it);
|
||||
for (auto const& p : const2quantifier[f])
|
||||
stack.push_back(p);
|
||||
const2quantifier.remove(f);
|
||||
}
|
||||
}
|
||||
|
@ -220,16 +215,11 @@ private:
|
|||
visiting = to_visit.back();
|
||||
to_visit.pop_back();
|
||||
visited.insert(visiting);
|
||||
obj_hashtable<func_decl>::iterator it = exp2const[visiting].begin();
|
||||
obj_hashtable<func_decl>::iterator end = exp2const[visiting].end();
|
||||
for (; it != end; it++) {
|
||||
obj_hashtable<expr>::iterator exprit = const2exp[*it].begin();
|
||||
obj_hashtable<expr>::iterator exprend = const2exp[*it].end();
|
||||
for (; exprit != exprend; exprit++) {
|
||||
if (!visited.contains(*exprit))
|
||||
to_visit.push_back(*exprit);
|
||||
for (func_decl* f : exp2const[visiting])
|
||||
for (expr* e : const2exp[f]) {
|
||||
if (!visited.contains(e))
|
||||
to_visit.push_back(e);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < g->size(); i++) {
|
||||
|
|
Loading…
Reference in a new issue