mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

debugging multi-objective interface and pb revisions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-12-02 14:30:17 -08:00
parent faa59ba7f9
commit c14c778735
2 changed files with 1 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/opt/objective_decl_plugin.cpp
View file

@ -48,6 +48,7 @@ namespace opt{
SASSERT(num_parameters == 0);
symbol name = get_name(static_cast<obj_kind>(k));
func_decl_info info(get_family_id(), k, num_parameters, parameters);
range = mk_sort(OBJECTIVE_SORT, 0, 0);
return m_manager->mk_func_decl(name, arity, domain, range, info);
}

8
src/opt/opt_cmds.cpp
View file

@ -80,9 +80,6 @@ public:
}
virtual void reset(cmd_context & ctx) {
if (m_formula) {
ctx.m().dec_ref(m_formula);
}
m_idx = 0;
m_formula = 0;
m_id = symbol::null;
@ -116,7 +113,6 @@ public:
throw cmd_exception("Invalid type for expression. Expected Boolean type.");
}
m_formula = t;
ctx.m().inc_ref(t);
++m_idx;
}
@ -298,9 +294,6 @@ public:
reset(ctx);
}
virtual void reset(cmd_context& ctx) {
if (m_objective) {
ctx.m().dec_ref(m_objective);
}
m_objective = 0;
m_idx = 0;
}
@ -312,7 +305,6 @@ public:
virtual void set_next_arg(cmd_context & ctx, expr * arg) {
m_objective = arg;
ctx.m().inc_ref(arg);
++m_idx;
}