mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
Create callbacks for min_maximize_cmd
Enable VS_PROJ = true for temporary use
This commit is contained in:
parent
7993ca53fe
commit
ac97a12bb8
|
@ -59,7 +59,7 @@ SHOW_CPPS = True
|
|||
VS_X64 = False
|
||||
ONLY_MAKEFILES = False
|
||||
Z3PY_SRC_DIR=None
|
||||
VS_PROJ = False
|
||||
VS_PROJ = True
|
||||
TRACE = False
|
||||
DOTNET_ENABLED=False
|
||||
JAVA_ENABLED=False
|
||||
|
|
|
@ -10,7 +10,7 @@ Abstract:
|
|||
|
||||
Author:
|
||||
|
||||
Anh-Phan Dung (t-anphan) 2013-10-14
|
||||
Anh-Dung Phan (t-anphan) 2013-10-14
|
||||
|
||||
Notes:
|
||||
|
||||
|
@ -23,6 +23,7 @@ class opt_context {
|
|||
ast_manager& m;
|
||||
expr_ref_vector m_formulas;
|
||||
vector<rational> m_weights;
|
||||
|
||||
public:
|
||||
opt_context(ast_manager& m):
|
||||
m(m),
|
||||
|
@ -43,6 +44,7 @@ class assert_weighted_cmd : public cmd {
|
|||
unsigned m_idx;
|
||||
expr_ref m_formula;
|
||||
rational m_weight;
|
||||
|
||||
public:
|
||||
assert_weighted_cmd(cmd_context& ctx, opt_context* opt_ctx):
|
||||
cmd("assert-weighted"),
|
||||
|
@ -60,6 +62,7 @@ public:
|
|||
m_idx = 0;
|
||||
m_formula = 0;
|
||||
}
|
||||
|
||||
virtual char const * get_usage() const { return "<formula> <rational-weight>"; }
|
||||
virtual char const * get_descr(cmd_context & ctx) const { return "assert soft constraint with weight"; }
|
||||
virtual unsigned get_arity() const { return 2; }
|
||||
|
@ -107,22 +110,39 @@ public:
|
|||
// to do the feasibility check.
|
||||
class min_maximize_cmd : public cmd {
|
||||
bool m_is_max;
|
||||
expr_ref m_term;
|
||||
opt_context* m_opt_ctx;
|
||||
|
||||
public:
|
||||
min_maximize_cmd(cmd_context& ctx, opt_context* opt_ctx, bool is_max):
|
||||
cmd(is_max?"maximize":"minimize"),
|
||||
m_is_max(is_max),
|
||||
m_term(ctx.m()),
|
||||
m_opt_ctx(opt_ctx)
|
||||
{}
|
||||
|
||||
virtual void reset(cmd_context & ctx) {
|
||||
m_term = 0;
|
||||
}
|
||||
|
||||
virtual char const * get_usage() const { return "<term>"; }
|
||||
virtual char const * get_descr(cmd_context & ctx) const { return "check sat modulo objective function";}
|
||||
virtual unsigned get_arity() const { return 1; }
|
||||
|
||||
// etc. TODO: Phan, add the appropriate callbacks as a warmup.
|
||||
virtual void prepare(cmd_context & ctx) {}
|
||||
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_EXPR; }
|
||||
|
||||
virtual void set_next_arg(cmd_context & ctx, expr * t) {
|
||||
m_term = t;
|
||||
}
|
||||
|
||||
virtual void failure_cleanup(cmd_context & ctx) {
|
||||
reset(ctx);
|
||||
}
|
||||
|
||||
virtual void execute(cmd_context & ctx) {
|
||||
// here is how to retrieve the soft constraints:
|
||||
std::cout << "TODO: " << mk_pp(m_term, ctx.m()) << "\n";
|
||||
// Here is how to retrieve the soft constraints
|
||||
m_opt_ctx->formulas();
|
||||
m_opt_ctx->weights();
|
||||
get_background(ctx);
|
||||
|
@ -134,14 +154,13 @@ private:
|
|||
ptr_vector<expr>::const_iterator it = ctx.begin_assertions();
|
||||
ptr_vector<expr>::const_iterator end = ctx.end_assertions();
|
||||
for (; it != end; ++it) {
|
||||
// need a solver object that supports soft constraints
|
||||
// Need a solver object that supports soft constraints
|
||||
// m_solver.assert_expr(*it);
|
||||
}
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
|
||||
void install_opt_cmds(cmd_context & ctx) {
|
||||
opt_context* opt_ctx = alloc(opt_context, ctx.m());
|
||||
ctx.insert(alloc(assert_weighted_cmd, ctx, opt_ctx));
|
||||
|
|
|
@ -10,7 +10,7 @@ Abstract:
|
|||
|
||||
Author:
|
||||
|
||||
Anh-Phan Dung (t-anphan) 2013-10-14
|
||||
Anh-Dung Phan (t-anphan) 2013-10-14
|
||||
|
||||
Notes:
|
||||
|
||||
|
|
9
src/opt/plan.txt
Normal file
9
src/opt/plan.txt
Normal file
|
@ -0,0 +1,9 @@
|
|||
Create file with command-line extensions.
|
||||
Similar to muz\fp\dl_cmds:
|
||||
- Add command (minimize <term>)
|
||||
- Add command (assert-weighted <expr> <weight> [:id]) the weight is a positive
|
||||
rational number, 1 can be handled as a special case sd not weighted SAT,
|
||||
but as ordinary MAXSAT (e.g., using Fu Malik algorithm. This is a sample).
|
||||
Identifier is optional and used to group constraints together.
|
||||
The F# sample illustrates what is meant.
|
||||
|
Loading…
Reference in a new issue