3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

add LP parser option to front-end and opt context

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-02-06 14:02:44 -08:00
parent 20fe08d80c
commit 43441d0fd5
8 changed files with 459 additions and 176 deletions

View file

@ -302,6 +302,11 @@ extern "C" {
parse_wcnf(*to_optimize_ptr(opt), s, h);
return;
}
if (ext && std::string("lp") == ext) {
unsigned_vector h;
parse_lp(*to_optimize_ptr(opt), s, h);
return;
}
scoped_ptr<cmd_context> ctx = alloc(cmd_context, false, &m);
install_opt_cmds(*ctx.get(), to_optimize_ptr(opt));
ctx->set_ignore_check(true);

View file

@ -310,41 +310,164 @@ void parse_opb(opt::context& opt, std::istream& is, unsigned_vector& h) {
opb.parse();
}
#if 0
/**
* \brief Parser for a modest subset of the CPLEX LP format.
* Reference: http://eaton.math.rpi.edu/cplex90html/reffileformatscplex/reffileformatscplex5.html
*/
class lp_stream_buffer : opt_stream_buffer {
public:
lp_stream_buffer(std::istream & s):
opt_stream_buffer(s)
{}
char lower(char c) {
return ('A' <= c && c <= 'Z') ? c - 'A' + 'a' : c;
}
bool parse_token_nocase(char const* token) {
skip_whitespace();
char const* t = token;
while (lower(ch()) == *t) {
next();
++t;
}
return 0 == *t;
}
struct asymbol {
bool m_is_num;
symbol m_sym;
rational m_num;
unsigned m_line;
asymbol(symbol const& s, unsigned l): m_is_num(false), m_sym(s), m_line(l) {}
asymbol(rational const& r, unsigned l): m_is_num(true), m_num(r), m_line(l) {}
};
class lp_tokenizer {
opt_stream_buffer& in;
vector<asymbol> m_tokens;
unsigned m_pos;
svector<char> m_buffer;
public:
lp_tokenizer(opt_stream_buffer& in):
in(in)
{}
m_pos(0)
{
parse_all(in);
}
symbol const& peek(unsigned i) {
if (i + m_pos >= m_tokens.size()) {
return symbol::null;
}
return m_tokens[i + m_pos].m_sym;
}
bool peek_num(unsigned i) {
if (i + m_pos >= m_tokens.size()) {
return false;
}
return m_tokens[i + m_pos].m_is_num;
}
rational const& get_num(unsigned i) {
return m_tokens[i + m_pos].m_num;
}
void next(unsigned delta = 1) {
m_pos += delta;
}
bool eof() const {
return m_pos == m_tokens.size();
}
unsigned line() const {
if (m_pos < m_tokens.size()) return m_tokens[m_pos].m_line;
return 0;
}
private:
bool is_separator(char c) {
return c == '\n' || c == '\\' || c == '*' || c == '+';
}
char lower(char c) {
if ('A' <= c && c <= 'Z')
return c - ('A' - 'a');
return c;
}
void parse_all(opt_stream_buffer& in) {
while (!in.eof()) {
in.skip_whitespace();
char c = in.ch();
if (c == '\\') {
in.skip_line();
continue;
}
if (is_num(c)) {
rational n(0);
unsigned div = 1;
while (is_num(c) && !in.eof()) {
n = n*rational(10) + rational(c - '0');
in.next();
c = in.ch();
}
if (c == '.') {
in.next();
while (is_num(c) && !in.eof()) {
n = n*rational(10) + rational(c - '0');
in.next();
div *= 10;
c = in.ch();
}
}
if (div > 1) n = n / rational(div);
m_tokens.push_back(asymbol(n, in.line()));
continue;
}
m_buffer.reset();
if (is_alpha(c)) {
while (is_sym(c) && !in.eof()) {
m_buffer.push_back(lower(c));
in.next();
c = in.ch();
}
}
else {
while (!is_ws(c) && !in.eof()) {
m_buffer.push_back(c);
in.next();
c = in.ch();
}
}
m_buffer.push_back(0);
m_tokens.push_back(asymbol(symbol(m_buffer.c_ptr()), in.line()));
}
}
bool is_alpha(char c) const {
return ('a' <= c && c <= 'z') || ('A' <= c && c <= 'Z');
}
bool is_num(char c) const {
return '0' <= c && c <= '9';
}
bool is_ws(char c) const {
return c == ' ' || c == '\n' || c == '\t';
}
bool is_sym(char c) const {
return
is_alpha(c) ||
is_num(c) ||
c == '!' ||
c == '"' ||
c == '#' ||
c == '$' ||
c == '%' ||
c == '&' ||
c == '{' ||
c == '}' ||
c == ',' ||
c == '.' ||
c == ';' ||
c == '?' ||
c == '@' ||
c == '`' ||
c == '\'' ||
c == '(' ||
c == ')' ||
c == '~';
}
};
class lp_parse {
typedef svector<std::pair<int, symbol> > lin_term;
typedef vector<std::pair<rational, symbol> > lin_term;
struct objective {
bool m_is_max;
@ -356,47 +479,96 @@ class lp_parse {
le, ge, eq
};
struct indicator {
symbol m_var;
bool m_true;
};
struct constraint {
optional<indicator> m_ind;
symbol m_name;
symbol m_bvar;
rational m_bval;
lin_term m_expr;
rel_op m_rel;
int m_bound;
rational m_bound;
constraint(symbol const& name, symbol const& v, rational const& val, lin_term& terms, rel_op r, rational const& bound):
m_name(name), m_bvar(v), m_bval(val), m_expr(terms), m_rel(r), m_bound(bound) {}
};
struct bound {
symbol m_var;
option<rational> m_lo, m_hi;
optional<rational> m_lo, m_hi;
bool m_int;
bound() : m_int(false) {}
};
opt::context& opt;
lp_tokenizer& tok;
objective m_objective;
vector<constraint> m_constraints;
vector<bound> m_bounds;
hashtable<symbol, symbol_hash_proc, symbol_eq_proc> m_binary;
opt::context& opt;
unsigned_vector& m_h;
lp_tokenizer tok;
objective m_objective;
vector<constraint> m_constraints;
map<symbol, bound, symbol_hash_proc, symbol_eq_proc> m_bounds;
public:
lp_parse(opt::context& opt, lp_stream_buffer& in):
opt(opt), tok(is) {}
lp_parse(opt::context& opt, opt_stream_buffer& in, unsigned_vector& h) :
opt(opt), m_h(h), tok(in) {}
void parse() {
parse_objective();
parse_subject_to();
parse_bounds();
parse_general();
parse_binary();
if (!try_subject_to()) {
error("subject to section expected");
return;
}
while (!is_section()) {
parse_constraint();
}
while (true) {
if (is_bounds()) {
tok.next();
while (!is_section()) {
parse_bound();
}
}
else if (is_binary()) {
tok.next();
while (!is_section()) {
parse_binary();
}
}
else if (is_general()) {
tok.next();
while (!is_section()) {
parse_general();
}
}
else {
break;
}
}
post_process();
}
private:
void error(char const* msg) {
std::ostringstream ous;
ous << tok.line() << ": " << msg << " got: " << peek(0) << "\n";
throw default_exception(ous.str());
}
symbol const& peek(unsigned i) { return tok.peek(i); }
bool try_accept(char * token) {
if (peek(0) == token) {
tok.next();
return true;
}
return false;
}
void parse_objective() {
m_objective.m_is_max = minmax();
m_objective.m_name = try_name();
if (peek(1) == ":") {
m_objective.m_name = peek(0);
tok.next(2);
}
parse_expr(m_objective.m_expr);
}
@ -413,132 +585,218 @@ public:
return false;
}
void parse_constraint() {
symbol name;
if (peek(1) == ":") {
name = peek(0);
tok.next(2);
}
rational val(0);
symbol var;
parse_indicator(var, val);
lin_term terms;
parse_expr(terms);
rel_op op = parse_relation();
rational rhs = tok.get_num(0);
tok.next();
m_constraints.push_back(constraint(name, var, val, terms, op, rhs));
}
bool try_accept(char const* token) {
void parse_expr(lin_term& terms) {
bool pos = true;
if (peek(0) == "-") {
pos = false;
tok.next();
}
while (peek(0) == "+") {
tok.next();
}
terms.push_back(parse_term());
if (!pos) terms.back().first = -terms.back().first;
while (peek(0) == "+" || peek(0) == "-") {
bool pos = peek(0) == "+";
tok.next();
terms.push_back(parse_term());
if (!pos) terms.back().first = -terms.back().first;
}
}
std::pair<rational, symbol> parse_term() {
std::pair<rational, symbol> r(rational::one(), peek(0));
if (tok.peek_num(0)) {
r.first = tok.get_num(0);
r.second = peek(1);
tok.next(2);
}
else {
tok.next(1);
}
return r;
}
rel_op parse_relation() {
if (try_accept("<=")) return le;
if (try_accept("=<")) return le;
if (try_accept(">=")) return ge;
if (try_accept("=>")) return ge;
if (try_accept("=")) return eq;
error("expected relation");
return eq;
}
bool peek_le(unsigned pos) {
return peek(pos) == "<=" || peek(pos) == "=<";
}
void parse_indicator(symbol& var, rational& val) {
if (peek(1) == "=" && tok.peek_num(2) && peek(3) == "->") {
var = peek(0);
val = tok.get_num(2);
tok.next(4);
}
}
bool try_subject_to() {
if (try_accept("subject") && try_accept("to")) return true;
if (try_accept("such") && try_accept("that")) return true;
if (try_accept("st")) return true;
if (try_accept("s.t.")) return true;
return false;
}
bool parse_indicator(symbol& var, bool& val) {
if (!peek("=", 1)) return false;
if (!peek(":", 3)) return false;
if (!peek("1", 2) && !peek("0", 2)) return false;
val = peek("1",2);
parse_variable(var);
accept("=");
accept();
accept(":");
return true;
bool is_section() { return is_general() || is_binary() || is_bounds() || is_end();}
bool is_bounds() { return peek(0) == "bounds"; }
bool is_general() { return peek(0) == "general" || peek(0) == "gen" || peek(0) == "generals"; }
bool is_binary() { return peek(0) == "binary" || peek(0) == "binaries" || peek(0) == "bin"; }
bool is_end() { return peek(0) == "end" || tok.eof(); }
// lo <= x
// x <= hi
// lo <= x <= hi
//
void parse_bound() {
symbol v;
if (peek_le(1) && tok.peek_num(0)) {
rational lhs = tok.get_num(0);
v = peek(2);
update_lower(lhs, v);
tok.next(3);
if (peek_le(0) && tok.peek_num(1)) {
rational rhs = tok.get_num(1);
update_upper(v, rhs);
tok.next(2);
}
}
if (peek_le(1) && tok.peek_num(2)) {
v = peek(0);
tok.next(2);
rational rhs = tok.get_num(0);
update_upper(v, rhs);
tok.next(1);
}
}
void parse_bounds() {
if (!try_accept("bounds")) return;
void update_lower(rational const& r, symbol const& v) {
bound b;
m_bounds.find(v, b);
b.m_lo = r;
m_bounds.insert(v, b);
}
void parse_indicator() {
void update_upper(symbol const& v, rational const& r) {
bound b;
if (!m_bounds.find(v, b)) {
// set the lower bound to default 0
b.m_lo = rational::zero();
}
b.m_hi = r;
m_bounds.insert(v, b);
}
def indicator(self):
v = self.variable()
self.accept("=")
val = self.try_accept("1")
if val is None:
val = self.accept("0")
self.accept("->")
return (var, val)
def try_indicator(self):
try:
return self.indicator()
with:
return None
void parse_binary() {
symbol const& v = peek(0);
update_lower(rational::zero(), v);
update_upper(v, rational::one());
m_bounds[v].m_int = true;
tok.next();
}
def constraints(self):
return [c for c in self._constraints()]
void parse_general() {
symbol const& v = peek(0);
bound b;
m_bounds.find(v, b);
b.m_int = true;
m_bounds.insert(v, b);
tok.next();
}
def _constraints(self):
while True:
c = self.try_constraint()
if c in None:
return
yield c
void post_process() {
ast_manager& m = opt.get_manager();
arith_util a(m);
for (constraint const& c : m_constraints) {
expr_ref fml(m);
expr_ref term = process_terms(c.m_expr);
bool is_int = a.is_int(term) && c.m_bound.is_int();
switch (c.m_rel) {
case le: fml = a.mk_le(term, a.mk_numeral(c.m_bound, is_int)); break;
case ge: fml = a.mk_ge(term, a.mk_numeral(c.m_bound, is_int)); break;
case eq: fml = m.mk_eq(term, a.mk_numeral(c.m_bound, is_int)); break;
}
if (c.m_bvar != symbol::null) {
term = mk_var(c.m_bvar);
bool is_int = c.m_bval.is_int() && a.is_int(term);
term = m.mk_eq(mk_var(c.m_bvar), a.mk_numeral(c.m_bval, is_int));
fml = m.mk_implies(term, fml);
}
opt.add_hard_constraint(fml);
}
for (auto const& kv : m_bounds) {
bound const& b = kv.m_value;
expr_ref term = mk_var(kv.m_key);
if (b.m_lo) {
bool is_int = b.m_lo->is_int() && a.is_int(term);
opt.add_hard_constraint(a.mk_le(a.mk_numeral(*b.m_lo, is_int), term));
}
if (b.m_hi) {
bool is_int = b.m_hi->is_int() && a.is_int(term);
opt.add_hard_constraint(a.mk_le(term, a.mk_numeral(*b.m_hi, is_int)));
}
}
expr_ref term = process_terms(m_objective.m_expr);
m_h.push_back(opt.add_objective(to_app(term), m_objective.m_is_max));
}
def try_constraint(self):
try:
return self.constraint()
except:
return None
def constraint(self):
name = self.try_label()
guard = self.try_guard()
e = self.expr()
op = self.relation()
rhs = self.numeral()
return (name, guard, e, ops, rhs)
expr_ref process_terms(lin_term const& terms) {
ast_manager& m = opt.get_manager();
arith_util a(m);
expr_ref_vector result(m);
for (auto const& kv : terms) {
expr_ref term = mk_var(kv.second);
if (!kv.first.is_one()) {
bool is_int = kv.first.is_int() && a.is_int(term);
term = a.mk_mul(a.mk_numeral(kv.first, is_int), term);
}
result.push_back(term);
}
return expr_ref(a.mk_add(result.size(), result.c_ptr()), m);
}
def expr(self):
return [t for t in self.terms()]
def terms(self):
while True:
t = self.term()
if t is None:
return None
yield t
def term(self):
sign = self.sign()
coeff = self.coeff()
v = self.variable()
return (sign*coeff, v)
def sign(self):
if self.try_accept("-"):
return -1
return 1
def coeff(self):
tok = self.peek()
if tok is int:
self.next()
return (int) tok
return 1
def relation(self):
if self.try_accept("<="):
return "<="
if self.try_accept(">="):
return ">="
if self.try_accept("=<"):
return "<="
if self.try_accept("=>"):
return ">="
if self.try_accept("="):
return "="
return None
def subject_to(self):
if self.accept("subject") and self.accept("to"):
return
if self.accept("such") and self.accept("that"):
return
if self.accept("st"):
return
if self.accept("s"):
self.try_accept(".")
self.accept("t")
self.accept(".")
return
expr_ref mk_var(symbol const& v) {
ast_manager& m = opt.get_manager();
arith_util a(m);
bound b;
if (!m_bounds.find(v, b)) {
b.m_lo = rational::zero();
m_bounds.insert(v, b);
}
return expr_ref(m.mk_const(v, b.m_int ? a.mk_int() : a.mk_real()), m);
}
};
void parse_lp(opt::context& opt, std::istream& is) {
lp_stream_buffer _is(is);
lp_parse lp(opt, _is);
void parse_lp(opt::context& opt, std::istream& is, unsigned_vector& h) {
opt_stream_buffer _is(is);
lp_parse lp(opt, _is, h);
lp.parse();
}
#endif

View file

@ -23,6 +23,8 @@ void parse_wcnf(opt::context& opt, std::istream& is, unsigned_vector& h);
void parse_opb(opt::context& opt, std::istream& is, unsigned_vector& h);
void parse_lp(opt::context& opt, std::istream& is, unsigned_vector& h);
#endif /* OPT_PARSE_H_ */

View file

@ -85,7 +85,7 @@ namespace sat {
}
}
wlist.set_end(it2);
VERIFY(found);
//VERIFY(found);
}
void conflict_cleanup(watch_list::iterator it, watch_list::iterator it2, watch_list& wlist) {

View file

@ -38,7 +38,7 @@ Revision History:
#include "util/env_params.h"
#include "shell/lp_frontend.h"
typedef enum { IN_UNSPECIFIED, IN_SMTLIB, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_WCNF, IN_OPB, IN_Z3_LOG, IN_MPS } input_kind;
typedef enum { IN_UNSPECIFIED, IN_SMTLIB, IN_SMTLIB_2, IN_DATALOG, IN_DIMACS, IN_WCNF, IN_OPB, IN_LP, IN_Z3_LOG, IN_MPS } input_kind;
std::string g_aux_input_file;
char const * g_input_file = 0;
@ -71,10 +71,12 @@ void display_usage() {
std::cout << "]. (C) Copyright 2006-2016 Microsoft Corp.\n";
std::cout << "Usage: z3 [options] [-file:]file\n";
std::cout << "\nInput format:\n";
std::cout << " -smt use parser for SMT input format.\n";
std::cout << " -smt2 use parser for SMT 2 input format.\n";
std::cout << " -dl use parser for Datalog input format.\n";
std::cout << " -dimacs use parser for DIMACS input format.\n";
std::cout << " -wcnf use parser for Weighted CNF DIMACS input format.\n";
std::cout << " -opb use parser for PB optimization input format.\n";
std::cout << " -lp use parser for a modest subset of CPLEX LP input format.\n";
std::cout << " -log use parser for Z3 log input format.\n";
std::cout << " -in read formula from standard input.\n";
std::cout << "\nMiscellaneous:\n";
@ -188,9 +190,12 @@ void parse_cmd_line_args(int argc, char ** argv) {
else if (strcmp(opt_name, "wcnf") == 0) {
g_input_kind = IN_WCNF;
}
else if (strcmp(opt_name, "bpo") == 0) {
else if (strcmp(opt_name, "pbo") == 0) {
g_input_kind = IN_OPB;
}
else if (strcmp(opt_name, "lp") == 0) {
g_input_kind = IN_LP;
}
else if (strcmp(opt_name, "log") == 0) {
g_input_kind = IN_Z3_LOG;
}
@ -322,6 +327,9 @@ int STD_CALL main(int argc, char ** argv) {
else if (strcmp(ext, "opb") == 0) {
g_input_kind = IN_OPB;
}
else if (strcmp(ext, "lp") == 0) {
g_input_kind = IN_LP;
}
else if (strcmp(ext, "log") == 0) {
g_input_kind = IN_Z3_LOG;
}
@ -349,10 +357,13 @@ int STD_CALL main(int argc, char ** argv) {
return_value = read_dimacs(g_input_file);
break;
case IN_WCNF:
return_value = parse_opt(g_input_file, true);
return_value = parse_opt(g_input_file, wcnf_t);
break;
case IN_OPB:
return_value = parse_opt(g_input_file, false);
return_value = parse_opt(g_input_file, opb_t);
break;
case IN_LP:
return_value = parse_opt(g_input_file, lp_t);
break;
case IN_DATALOG:
read_datalog(g_input_file);

View file

@ -14,6 +14,7 @@ Copyright (c) 2015 Microsoft Corporation
#include "util/timeout.h"
#include "ast/reg_decl_plugins.h"
#include "opt/opt_parse.h"
#include "shell/opt_frontend.h"
extern bool g_display_statistics;
static bool g_first_interrupt = true;
@ -73,18 +74,23 @@ static void on_timeout() {
}
}
static unsigned parse_opt(std::istream& in, bool is_wcnf) {
static unsigned parse_opt(std::istream& in, opt_format f) {
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);
if (is_wcnf) {
switch (f) {
case wcnf_t:
parse_wcnf(opt, in, g_handles);
}
else {
break;
case opb_t:
parse_opb(opt, in, g_handles);
break;
case lp_t:
parse_lp(opt, in, g_handles);
break;
}
try {
lbool r = opt.optimize();
@ -121,7 +127,7 @@ static unsigned parse_opt(std::istream& in, bool is_wcnf) {
return 0;
}
unsigned parse_opt(char const* file_name, bool is_wcnf) {
unsigned parse_opt(char const* file_name, opt_format f) {
g_first_interrupt = true;
g_start_time = static_cast<double>(clock());
register_on_timeout_proc(on_timeout);
@ -132,10 +138,10 @@ unsigned parse_opt(char const* file_name, bool is_wcnf) {
std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl;
exit(ERR_OPEN_FILE);
}
return parse_opt(in, is_wcnf);
return parse_opt(in, f);
}
else {
return parse_opt(std::cin, is_wcnf);
return parse_opt(std::cin, f);
}
}

View file

@ -13,7 +13,9 @@ Author:
#ifndef OPT_FRONTEND_H_
#define OPT_FRONTEND_H_
unsigned parse_opt(char const* file_name, bool is_wcnf);
enum opt_format { opb_t, wcnf_t, lp_t };
unsigned parse_opt(char const* file_name, opt_format f);
#endif /* OPT_FRONTEND_H_ */

View file

@ -160,11 +160,10 @@ public:
expr_ref_vector xs(m);
expr_ref last_v(m);
if (!m_mc) m_mc = alloc(generic_model_converter, m, "lia2card");
for (unsigned i = 0; i < hi; ++i) {
if (i < lo) {
xs.push_back(a.mk_int(1));
continue;
}
if (lo > 0) {
xs.push_back(a.mk_int(lo));
}
for (unsigned i = lo; i < hi; ++i) {
std::string name(x->get_decl()->get_name().str());
expr_ref v(m.mk_fresh_const(name.c_str(), m.mk_bool_sort()), m);
if (last_v) axioms.push_back(m.mk_implies(v, last_v));
@ -195,7 +194,7 @@ public:
if (a.is_int(x) &&
is_uninterp_const(x) &&
bounds.has_lower(x, lo, s1) && !s1 && lo.is_unsigned() &&
bounds.has_upper(x, hi, s2) && !s2 && hi.is_unsigned() && hi.get_unsigned() <= m_max_ub) {
bounds.has_upper(x, hi, s2) && !s2 && hi.is_unsigned() && hi.get_unsigned() - lo.get_unsigned() <= m_max_ub) {
expr_ref b = mk_bounded(axioms, to_app(x), lo.get_unsigned(), hi.get_unsigned());
rep.insert(x, b);
m_bounds.insert(x, bound(lo.get_unsigned(), hi.get_unsigned(), b));