mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-26 18:45:33 +00:00
Code Activity

add optimization front-ends directly to the shell

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-10 14:23:58 -07:00
parent d1a2e61220
commit f651145b4c
5 changed files with 379 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
examples/opt/opt.cpp
View file

@ -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();

2
src/shell/dimacs_frontend.h
View file

@ -21,5 +21,5 @@ Revision History:
unsigned read_dimacs(char const * benchmark_file);
#endif /* _DATALOG_FRONTEND_H_ */
#endif /* _DIMACS_FRONTEND_H_ */

21
src/shell/main.cpp
View file

@ -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;

332
src/shell/opt_frontend.cpp Normal file
View file

@ -0,0 +1,332 @@
#include<fstream>
#include<signal.h>
#include<time.h>
#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<unsigned>(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<char> 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<double>(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<double>(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);
}
}

20
src/shell/opt_frontend.h Normal file
View file

@ -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_ */