mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 09:55:19 +00:00
initial opt commands
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
0a964c324e
commit
726f66a77c
|
@ -63,6 +63,7 @@ def init_project_def():
|
|||
add_lib('tab', ['muz', 'transforms'], 'muz/tab')
|
||||
add_lib('bmc', ['muz', 'transforms'], 'muz/bmc')
|
||||
add_lib('fp', ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc'], 'muz/fp')
|
||||
add_lib('opt', ['smt'], 'opt')
|
||||
add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe'], 'tactic/smtlogics')
|
||||
add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
|
||||
add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
|
||||
|
@ -70,7 +71,7 @@ def init_project_def():
|
|||
API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h']
|
||||
add_lib('api', ['portfolio', 'user_plugin', 'smtparser', 'realclosure'],
|
||||
includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files)
|
||||
add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3')
|
||||
add_exe('shell', ['api', 'sat', 'extra_cmds','opt'], exe_name='z3')
|
||||
add_exe('test', ['api', 'fuzzing'], exe_name='test-z3', install=False)
|
||||
add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll',
|
||||
reexports=['api'],
|
||||
|
|
|
@ -335,10 +335,10 @@ cmd_context::~cmd_context() {
|
|||
if (m_main_ctx) {
|
||||
set_verbose_stream(std::cerr);
|
||||
}
|
||||
reset(true);
|
||||
finalize_cmds();
|
||||
finalize_tactic_cmds();
|
||||
finalize_probes();
|
||||
reset(true);
|
||||
m_solver = 0;
|
||||
m_check_sat_result = 0;
|
||||
}
|
||||
|
|
150
src/opt/opt_cmds.cpp
Normal file
150
src/opt/opt_cmds.cpp
Normal file
|
@ -0,0 +1,150 @@
|
|||
/*++
|
||||
Copyright (c) 2013 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
opt_cmds.cpp
|
||||
|
||||
Abstract:
|
||||
Commands for optimization benchmarks
|
||||
|
||||
Author:
|
||||
|
||||
Anh-Phan Dung (t-anphan) 2013-10-14
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#include "opt_cmds.h"
|
||||
#include "cmd_context.h"
|
||||
#include "ast_pp.h"
|
||||
|
||||
class opt_context {
|
||||
ast_manager& m;
|
||||
expr_ref_vector m_formulas;
|
||||
vector<rational> m_weights;
|
||||
public:
|
||||
opt_context(ast_manager& m):
|
||||
m(m),
|
||||
m_formulas(m)
|
||||
{}
|
||||
|
||||
void add_formula(expr* f, rational const& w) {
|
||||
m_formulas.push_back(f);
|
||||
m_weights.push_back(w);
|
||||
}
|
||||
|
||||
expr_ref_vector const& formulas() const { return m_formulas; }
|
||||
vector<rational> const& weights() const { return m_weights; }
|
||||
};
|
||||
|
||||
class assert_weighted_cmd : public cmd {
|
||||
opt_context* m_opt_ctx;
|
||||
unsigned m_idx;
|
||||
expr_ref m_formula;
|
||||
rational m_weight;
|
||||
public:
|
||||
assert_weighted_cmd(cmd_context& ctx, opt_context* opt_ctx):
|
||||
cmd("assert-weighted"),
|
||||
m_opt_ctx(opt_ctx),
|
||||
m_idx(0),
|
||||
m_formula(ctx.m()),
|
||||
m_weight(0)
|
||||
{}
|
||||
|
||||
virtual ~assert_weighted_cmd() {
|
||||
dealloc(m_opt_ctx);
|
||||
}
|
||||
|
||||
virtual void reset(cmd_context & ctx) {
|
||||
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; }
|
||||
|
||||
// command invocation
|
||||
virtual void prepare(cmd_context & ctx) {}
|
||||
virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { if (m_idx == 0) return CPK_EXPR; return CPK_NUMERAL; }
|
||||
virtual void set_next_arg(cmd_context & ctx, rational const & val) {
|
||||
SASSERT(m_idx == 1);
|
||||
if (!val.is_pos()) {
|
||||
throw cmd_exception("Invalid weight. Weights must be positive.");
|
||||
}
|
||||
m_weight = val;
|
||||
++m_idx;
|
||||
}
|
||||
|
||||
virtual void set_next_arg(cmd_context & ctx, expr * t) {
|
||||
SASSERT(m_idx == 0);
|
||||
if (!ctx.m().is_bool(t)) {
|
||||
throw cmd_exception("Invalid type for expression. Expected Boolean type.");
|
||||
}
|
||||
m_formula = t;
|
||||
++m_idx;
|
||||
}
|
||||
|
||||
virtual void failure_cleanup(cmd_context & ctx) {
|
||||
reset(ctx);
|
||||
}
|
||||
|
||||
virtual void execute(cmd_context & ctx) {
|
||||
std::cout << "TODO: " << mk_pp(m_formula, ctx.m()) << " " << m_weight << "\n";
|
||||
m_opt_ctx->add_formula(m_formula, m_weight);
|
||||
reset(ctx);
|
||||
}
|
||||
|
||||
virtual void finalize(cmd_context & ctx) {
|
||||
std::cout << "FINALIZE\n";
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
// what amounts to check-sat, but uses the *single* objective function.
|
||||
// alternative is to register multiple objective functions using
|
||||
// minimize/maximize and then use check-sat or some variant of it
|
||||
// to do the feasibility check.
|
||||
class min_maximize_cmd : public cmd {
|
||||
bool m_is_max;
|
||||
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_opt_ctx(opt_ctx)
|
||||
{}
|
||||
|
||||
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 execute(cmd_context & ctx) {
|
||||
// here is how to retrieve the soft constraints:
|
||||
m_opt_ctx->formulas();
|
||||
m_opt_ctx->weights();
|
||||
get_background(ctx);
|
||||
// reset m_opt_ctx?
|
||||
}
|
||||
|
||||
private:
|
||||
void get_background(cmd_context& ctx) {
|
||||
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
|
||||
// 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));
|
||||
ctx.insert(alloc(min_maximize_cmd, ctx, opt_ctx, true));
|
||||
ctx.insert(alloc(min_maximize_cmd, ctx, opt_ctx, false));
|
||||
}
|
28
src/opt/opt_cmds.h
Normal file
28
src/opt/opt_cmds.h
Normal file
|
@ -0,0 +1,28 @@
|
|||
/*++
|
||||
Copyright (c) 2013 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
opt_cmds.h
|
||||
|
||||
Abstract:
|
||||
Commands for optimization benchmarks
|
||||
|
||||
Author:
|
||||
|
||||
Anh-Phan Dung (t-anphan) 2013-10-14
|
||||
|
||||
Notes:
|
||||
|
||||
--*/
|
||||
#ifndef _OPT_CMDS_H_
|
||||
#define _OPT_CMDS_H_
|
||||
|
||||
#include "ast.h"
|
||||
|
||||
class cmd_context;
|
||||
|
||||
void install_opt_cmds(cmd_context & ctx);
|
||||
|
||||
|
||||
#endif
|
|
@ -26,6 +26,7 @@ Revision History:
|
|||
#include"smt2parser.h"
|
||||
#include"dl_cmds.h"
|
||||
#include"dbg_cmds.h"
|
||||
#include"opt_cmds.h"
|
||||
#include"polynomial_cmds.h"
|
||||
#include"subpaving_cmds.h"
|
||||
#include"smt_strategic_solver.h"
|
||||
|
@ -110,6 +111,7 @@ unsigned read_smtlib2_commands(char const * file_name) {
|
|||
install_dbg_cmds(ctx);
|
||||
install_polynomial_cmds(ctx);
|
||||
install_subpaving_cmds(ctx);
|
||||
install_opt_cmds(ctx);
|
||||
|
||||
g_cmd_context = &ctx;
|
||||
signal(SIGINT, on_ctrl_c);
|
||||
|
|
Loading…
Reference in a new issue