mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

add separate get-objectives command #1107

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-06-23 16:34:38 -07:00
parent e3ec7e7d05
commit 9d1852343c
2 changed files with 24 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/cmd_context/cmd_context.cpp
View file

@ -1360,7 +1360,6 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
throw ex; throw ex;
} }
catch (z3_exception & ex) { catch (z3_exception & ex) {
get_opt()->display_assignment(regular_stream());
throw cmd_exception(ex.msg()); throw cmd_exception(ex.msg());
} }
if (m_processing_pareto && r != l_true) { if (m_processing_pareto && r != l_true) {
@ -1398,7 +1397,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
} }
validate_check_sat_result(r); validate_check_sat_result(r);
if (was_opt && r != l_false && !m_processing_pareto) { if (was_opt && r != l_false && !m_processing_pareto) {
get_opt()->display_assignment(regular_stream()); // get_opt()->display_assignment(regular_stream());
} }
if (r == l_true && m_params.m_dump_models) { if (r == l_true && m_params.m_dump_models) {

23
src/opt/opt_cmds.cpp
View file

@ -143,12 +143,35 @@ public:
} }
}; };
class get_objectives_cmd : public cmd {
opt::context* m_opt;
public:
get_objectives_cmd(opt::context* opt):
cmd("get-objectives"),
m_opt(opt)
{}
virtual void reset(cmd_context & ctx) { }
virtual char const * get_usage() const { return "(get-objectives)"; }
virtual char const * get_descr(cmd_context & ctx) const { return "retrieve the objective values (after optimization)"; }
virtual unsigned get_arity() const { return 0; }
virtual void prepare(cmd_context & ctx) {}
virtual void failure_cleanup(cmd_context & ctx) {
reset(ctx);
}
virtual void execute(cmd_context & ctx) {
get_opt(ctx, m_opt).display_assignment(ctx.regular_stream());
}
};
void install_opt_cmds(cmd_context & ctx, opt::context* opt) { void install_opt_cmds(cmd_context & ctx, opt::context* opt) {
ctx.insert(alloc(assert_soft_cmd, opt)); ctx.insert(alloc(assert_soft_cmd, opt));
ctx.insert(alloc(min_maximize_cmd, true, opt)); ctx.insert(alloc(min_maximize_cmd, true, opt));
ctx.insert(alloc(min_maximize_cmd, false, opt)); ctx.insert(alloc(min_maximize_cmd, false, opt));
ctx.insert(alloc(get_objectives_cmd, opt));
} }