From f651145b4c14896a577b7e2d95e7382e84732c7f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 10 Oct 2014 14:23:58 -0700 Subject: [PATCH] add optimization front-ends directly to the shell Signed-off-by: Nikolaj Bjorner --- examples/opt/opt.cpp | 6 + src/shell/dimacs_frontend.h | 2 +- src/shell/main.cpp | 21 ++- src/shell/opt_frontend.cpp | 332 ++++++++++++++++++++++++++++++++++++ src/shell/opt_frontend.h | 20 +++ 5 files changed, 379 insertions(+), 2 deletions(-) create mode 100644 src/shell/opt_frontend.cpp create mode 100644 src/shell/opt_frontend.h diff --git a/examples/opt/opt.cpp b/examples/opt/opt.cpp index 6f99efb54..1195fac38 100644 --- a/examples/opt/opt.cpp +++ b/examples/opt/opt.cpp @@ -304,6 +304,12 @@ void parse_cmd_line_args(int argc, char ** argv) { else if (!strcmp(arg,"st") || !strcmp(arg,"statistics")) { g_display_statistics = true; } + else if (strcmp(opt_name, "T") == 0) { + if (!opt_arg) + error("option argument (-T:timeout) is missing."); + long tm = strtol(opt_arg, 0, 10); + //set_timeout(tm * 1000); + } else if (!strcmp(arg,"t") || !strcmp(arg,"timeout")) { if (!opt_arg) { display_usage(); diff --git a/src/shell/dimacs_frontend.h b/src/shell/dimacs_frontend.h index 9521c8256..5448d1af0 100644 --- a/src/shell/dimacs_frontend.h +++ b/src/shell/dimacs_frontend.h @@ -21,5 +21,5 @@ Revision History: unsigned read_dimacs(char const * benchmark_file); -#endif /* _DATALOG_FRONTEND_H_ */ +#endif /* _DIMACS_FRONTEND_H_ */ diff --git a/src/shell/main.cpp b/src/shell/main.cpp index f23bc470c..10fc916ca 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -29,13 +29,14 @@ Revision History: #include"version.h" #include"dimacs_frontend.h" #include"datalog_frontend.h" +#include"opt_frontend.h" #include"timeout.h" #include"z3_exception.h" #include"error_codes.h" #include"gparams.h" #include"env_params.h" -typedef enum { IN_UNSPECIFIED, IN_SMTLIB, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_Z3_LOG } input_kind; +typedef enum { IN_UNSPECIFIED, IN_SMTLIB, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_WCNF, IN_PBO, IN_Z3_LOG } input_kind; std::string g_aux_input_file; char const * g_input_file = 0; @@ -168,6 +169,12 @@ void parse_cmd_line_args(int argc, char ** argv) { else if (strcmp(opt_name, "dimacs") == 0) { g_input_kind = IN_DIMACS; } + else if (strcmp(opt_name, "wcnf") == 0) { + g_input_kind = IN_WCNF; + } + else if (strcmp(opt_name, "bpo") == 0) { + g_input_kind = IN_PBO; + } else if (strcmp(opt_name, "log") == 0) { g_input_kind = IN_Z3_LOG; } @@ -306,6 +313,12 @@ int main(int argc, char ** argv) { else if (strcmp(ext, "dimacs") == 0 || strcmp(ext, "cnf") == 0) { g_input_kind = IN_DIMACS; } + else if (strcmp(ext, "wcnf") == 0) { + g_input_kind = IN_WCNF; + } + else if (strcmp(ext, "pbo") == 0) { + g_input_kind = IN_PBO; + } else if (strcmp(ext, "log") == 0) { g_input_kind = IN_Z3_LOG; } @@ -328,6 +341,12 @@ int main(int argc, char ** argv) { case IN_DIMACS: return_value = read_dimacs(g_input_file); break; + case IN_WCNF: + return_value = parse_opt(g_input_file, true); + break; + case IN_PBO: + return_value = parse_opt(g_input_file, false); + break; case IN_DATALOG: read_datalog(g_input_file); break; diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp new file mode 100644 index 000000000..f00d111ad --- /dev/null +++ b/src/shell/opt_frontend.cpp @@ -0,0 +1,332 @@ +#include +#include +#include +#include"opt_context.h" +#include"ast_util.h" +#include"arith_decl_plugin.h" +#include"gparams.h" +#include"timeout.h" +#include"reg_decl_plugins.h" + +static bool g_display_statistics = false; +static bool g_first_interrupt = true; +static int g_timeout = 0; +static bool g_display_model = false; +static opt::context* g_opt = 0; +static double g_start_time = 0; +static unsigned_vector g_handles; + +class stream_buffer { + std::istream & m_stream; + int m_val; + unsigned m_lines; +public: + stream_buffer(std::istream & s): + m_stream(s), + m_lines(0) { + m_val = m_stream.get(); + } + int operator *() const { return m_val;} + void operator ++() { m_val = m_stream.get(); } + int ch() const { return m_val; } + void next() { m_val = m_stream.get(); } + bool eof() const { return ch() == EOF; } + unsigned line() const { return m_line; } + void skip_whitespace() { + while ((ch() >= 9 && ch() <= 13) || ch() == 32) { + if (ch() == 10) ++m_lines; + next(); + } + } + void skip_line() { + while(true) { + if (eof()) { + return; + } + if (ch() == '\n') { + ++m_lines; + next(); + return; + } + next(); + } + } + + bool parse_token(char const* token) { + skip_whitespace(); + char const* t = token; + while (ch() == *t) { + next(); + ++t; + } + return 0 == *t; + } + + int parse_int() { + int val = 0; + bool neg = false; + skip_whitespace(); + + if (ch() == '-') { + neg = true; + next(); + } + else if (ch() == '+') { + next(); + } + if (ch() < '0' || ch() > '9') { + std::cerr << "(error line " << line() << " \"unexpected char: " << ((char)ch()) << "\)\n"; + exit(3); + } + while (ch() >= '0' && ch() <= '9') { + val = val*10 + (ch() - '0'); + next(); + } + return neg ? -val : val; + } +}; + +class wcnf { + opt::context& opt; + ast_manager& m; + stream_buffer& in; + + app_ref read_clause(unsigned& weight) { + int parsed_lit; + int var; + parsed_lit = in.parse_int(); + weight = static_cast(parsed_lit); + app_ref result(m), p(m); + expr_ref_vector ors(m); + while (true) { + parsed_lit = in.parse_int(); + if (parsed_lit == 0) + break; + var = abs(parsed_lit); + p = m.mk_const(symbol(var), m.mk_bool_sort()); + if (parsed_lit < 0) p = m.mk_not(p); + ors.push_back(p); + } + result = to_app(mk_or(m, ors.size(), ors.c_ptr())); + return result; + } + + void parse_spec(int& num_vars, int& num_clauses, int& max_weight) { + in.parse_token("wcnf"); + num_vars = in.parse_int(); + num_clauses = in.parse_int(); + max_weight = in.parse_int(); + } + +public: + + wcnf(opt::context& opt, stream_buffer& in): opt(opt), m(opt.get_manager()), in(in) {} + + void parse() { + int num_vars = 0, num_clauses = 0, max_weight = 0; + while (true) { + in.skip_whitespace(); + if (in.eof()) { + break; + } + else if (*in == 'c') { + in.skip_line(); + } + else if (*in == 'p') { + ++in; + parse_spec(num_vars, num_clauses, max_weight); + } + else { + unsigned weight = 0; + app_ref cls = read_clause(weight); + if (weight == max_weight) { + opt.add_hard_constraint(cls); + } + else { + opt.add_soft_constraint(cls, rational(weight), symbol::null); + } + } + } + } +}; + + +class opb { + opt::context& opt; + ast_manager& m; + stream_buffer& in; + arith_util arith; + + app_ref parse_id() { + bool negated = in.parse_token("~"); + if (!in.parse_token("x")) { + std::cerr << "(error line " << in.line() << " \"unexpected char: " << ((char)in.ch()) << "\)\n"; + exit(3); + } + app_ref p(m); + int id = in.parse_int(); + p = m.mk_const(symbol(id), m.mk_bool_sort()); + if (negated) p = m.mk_not(p); + return p; + } + + app_ref parse_ids() { + app_ref result = parse_id(); + while (*in == '~' || *in == 'x') { + result = m.mk_and(result, parse_id()); + } + return result; + } + + app_ref parse_coeff() { + in.skip_whitespace(); + svector num; + bool pos = true; + if (*in == '-') pos = false, ++in; + if (*in == '+') ++in; + if (!pos) num.push_back('-'); + in.skip_whitespace(); + while (*in >= '0' && *in <='9') num.push_back(*in), ++in; + num.push_back(0); + return app_ref(arith.mk_numeral(rational(num.c_ptr()), true), m); + } + + app_ref parse_term() { + app_ref c = parse_coeff(); + app_ref e = parse_ids(); + return app_ref(m.mk_ite(e, c, arith.mk_numeral(rational(0), true)), m); + } + + void parse_objective() { + app_ref t = parse_term(); + while (!in.parse_token(";") && !in.eof()) { + t = arith.mk_add(t, parse_term()); + } + g_handles.push_back(opt.add_objective(t, false)); + } + + void parse_constraint() { + app_ref t = parse_term(); + while (!in.eof()) { + if (in.parse_token(">=")) { + t = arith.mk_ge(t, parse_coeff()); + in.parse_token(";"); + break; + } + if (in.parse_token("=")) { + t = m.mk_eq(t, parse_coeff()); + in.parse_token(";"); + break; + } + t = arith.mk_add(t, parse_term()); + } + opt.add_hard_constraint(t); + } +public: + opb(opt::context& opt, stream_buffer& in): + opt(opt), m(opt.get_manager()), + in(in), arith(m) {} + + void parse() { + + while (true) { + in.skip_whitespace(); + if (in.eof()) { + break; + } + else if (*in == '*') { + in.skip_line(); + } + else if (in.parse_token("min:")) { + parse_objective(); + } + else { + parse_constraint(); + } + } + } +}; + + + +static void display_statistics() { + if (g_display_statistics && g_opt) { + ::statistics stats; + g_opt->collect_statistics(stats); + stats.display(std::cout); + double end_time = static_cast(clock()); + std::cout << "time: " << (end_time - g_start_time)/CLOCKS_PER_SEC << " secs\n"; + for (unsigned i = 0; i < g_handles.size(); ++i) { + std::cout << " [" << g_opt->get_lower(g_handles[i]) << ":" << g_opt->get_upper(g_handles[i]) << "]\n"; + } + } +} + +static void on_ctrl_c(int) { + if (g_opt && g_first_interrupt) { + g_opt->set_cancel(true); + g_first_interrupt = false; + } + else { + signal (SIGINT, SIG_DFL); + #pragma omp critical (g_display_stats) + { + display_statistics(); + } + raise(SIGINT); + } +} + +static void on_timeout() { + #pragma omp critical (g_display_stats) + { + display_statistics(); + exit(0); + } +} + +static unsigned parse_opt(std::istream& in, bool is_wcnf) { + ast_manager m; + reg_decl_plugins(m); + opt::context opt(m); + g_opt = &opt; + params_ref p = gparams::get_module("opt"); + opt.updt_params(p); + stream_buffer _in(in); + if (is_wcnf) { + wcnf wcnf(opt, _in); + wcnf.parse(); + } + else { + opb opb(opt, _in); + opb.parse(); + } + lbool r = opt.optimize(); + std::cout << r << "\n"; + #pragma omp critical (g_display_stats) + { + display_statistics(); + register_on_timeout_proc(0); + g_opt = 0; + } + return 0; +} + +unsigned parse_opt(char const* file_name, bool is_wcnf) { + g_start_time = static_cast(clock()); + register_on_timeout_proc(on_timeout); + signal(SIGINT, on_ctrl_c); + unsigned result = 0; + if (file_name) { + std::ifstream in(file_name); + if (in.bad() || in.fail()) { + std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl; + exit(ERR_OPEN_FILE); + } + return parse_opt(in, is_wcnf); + } + else { + return parse_opt(std::cin, is_wcnf); + } +} + diff --git a/src/shell/opt_frontend.h b/src/shell/opt_frontend.h new file mode 100644 index 000000000..df6070378 --- /dev/null +++ b/src/shell/opt_frontend.h @@ -0,0 +1,20 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + opt_frontend.h + +Author: + + Nikolaj Bjorner (nbjorner) 2014-10-10. + +--*/ +#ifndef _OPT_FRONTEND_H_ +#define _OPT_FRONTEND_H_ + +unsigned parse_opt(char const* file_name, bool is_wcnf); + +#endif /* _OPT_FRONTEND_H_ */ + +