mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

debug opt

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-12-12 15:39:38 -06:00
parent f41d23bc0f
commit df5c2adc4e
2 changed files with 12 additions and 10 deletions

3
src/opt/opt_context.cpp
View file

@ -92,7 +92,8 @@ namespace opt {
case 1:
return execute(m_objectives[0], false);
default: {
symbol pri = m_params.get_sym("priority", symbol("lex"));
opt_params optp(m_params);
symbol pri = optp.priority();
if (pri == symbol("pareto")) {
return execute_pareto();
}

19
src/tactic/arith/elim01_tactic.cpp
View file

@ -23,6 +23,7 @@ Notes:
#include"expr_safe_replace.h" // NB: should use proof-producing expr_substitute in polished version.
#include"arith_decl_plugin.h"
#include"elim01_tactic.h"
#include"model_smt2_pp.h"
class bool2int_model_converter : public model_converter {
ast_manager& m;
@ -63,15 +64,15 @@ public:
else {
new_model->register_decl(f, fi);
}
num = old_model->get_num_functions();
for (unsigned i = 0; i < num; i++) {
func_decl * f = old_model->get_function(i);
func_interp * fi = old_model->get_func_interp(f);
new_model->register_decl(f, fi->copy());
}
new_model->copy_usort_interps(*old_model);
old_model = new_model;
}
}
num = old_model->get_num_functions();
for (unsigned i = 0; i < num; i++) {
func_decl * f = old_model->get_function(i);
func_interp * fi = old_model->get_func_interp(f);
new_model->register_decl(f, fi->copy());
}
new_model->copy_usort_interps(*old_model);
old_model = new_model;
}
void insert(func_decl* x_new, func_decl* x_old) {