mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
return box model based on index. Issue #955
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
0fb3161113
commit
c99205fa7e
|
@ -100,13 +100,34 @@ public:
|
|||
|
||||
ATOMIC_CMD(exit_cmd, "exit", "exit.", ctx.print_success(); throw stop_parser_exception(););
|
||||
|
||||
ATOMIC_CMD(get_model_cmd, "get-model", "retrieve model for the last check-sat command", {
|
||||
if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0)
|
||||
throw cmd_exception("model is not available");
|
||||
model_ref m;
|
||||
ctx.get_check_sat_result()->get_model(m);
|
||||
ctx.display_model(m);
|
||||
});
|
||||
class get_model_cmd : public cmd {
|
||||
unsigned m_index;
|
||||
public:
|
||||
get_model_cmd(): cmd("get-model"), m_index(0) {}
|
||||
virtual char const * get_usage() const { return "[<index of box objective>]"; }
|
||||
virtual char const * get_descr(cmd_context & ctx) const {
|
||||
return "retrieve model for the last check-sat command.\nSupply optional index if retrieving a model corresponding to a box optimization objective";
|
||||
}
|
||||
virtual unsigned get_arity() const { return VAR_ARITY; }
|
||||
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_UINT; }
|
||||
virtual void set_next_arg(cmd_context & ctx, unsigned index) { m_index = index; }
|
||||
virtual void execute(cmd_context & ctx) {
|
||||
if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0)
|
||||
throw cmd_exception("model is not available");
|
||||
model_ref m;
|
||||
if (m_index > 0 && ctx.get_opt()) {
|
||||
ctx.get_opt()->get_box_model(m, m_index);
|
||||
}
|
||||
else {
|
||||
ctx.get_check_sat_result()->get_model(m);
|
||||
}
|
||||
ctx.display_model(m);
|
||||
}
|
||||
virtual void reset(cmd_context& ctx) {
|
||||
m_index = 0;
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
ATOMIC_CMD(get_assignment_cmd, "get-assignment", "retrieve assignment", {
|
||||
if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0)
|
||||
|
|
|
@ -124,6 +124,7 @@ public:
|
|||
virtual bool is_pareto() = 0;
|
||||
virtual void set_logic(symbol const& s) = 0;
|
||||
virtual bool print_model() const = 0;
|
||||
virtual void get_box_model(model_ref& mdl, unsigned index) = 0;
|
||||
virtual void updt_params(params_ref const& p) = 0;
|
||||
};
|
||||
|
||||
|
|
|
@ -342,6 +342,14 @@ namespace opt {
|
|||
fix_model(mdl);
|
||||
}
|
||||
|
||||
void context::get_box_model(model_ref& mdl, unsigned index) {
|
||||
if (index >= m_box_models.size()) {
|
||||
throw default_exception("index into models is out of bounds");
|
||||
}
|
||||
mdl = m_box_models[index];
|
||||
fix_model(mdl);
|
||||
}
|
||||
|
||||
lbool context::execute_min_max(unsigned index, bool committed, bool scoped, bool is_max) {
|
||||
if (scoped) get_solver().push();
|
||||
lbool result = m_optsmt.lex(index, is_max);
|
||||
|
|
|
@ -186,6 +186,7 @@ namespace opt {
|
|||
virtual bool print_model() const;
|
||||
virtual void set_model(model_ref& _m) { m_model = _m; }
|
||||
virtual void get_model(model_ref& _m);
|
||||
virtual void get_box_model(model_ref& _m, unsigned index);
|
||||
virtual void fix_model(model_ref& _m);
|
||||
virtual void collect_statistics(statistics& stats) const;
|
||||
virtual proof* get_proof() { return 0; }
|
||||
|
|
Loading…
Reference in a new issue