mirror of
https://github.com/Z3Prover/z3
synced 2026-02-14 21:01:49 +00:00
ebc0688470
* Initial plan * Refactor mk_and and mk_or call sites to use overloaded methods Changed 130 call sites across 64 files to use vector overloads directly instead of manually passing .size() and .data()/.c_ptr() Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Revert mk_or changes for ptr_buffer/ptr_vector (no overload exists in ast_util.h) * Fix compilation errors from mk_and/mk_or refactoring Fixed type mismatches by: - Removing m parameter for expr_ref_vector (ast_util.h has mk_and/mk_or(expr_ref_vector) overloads) - Reverting changes for ref_buffer types (no overload exists in ast_util.h, only in ast.h for m.mk_and) - Verified build succeeds and Z3 works correctly Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix test files to use correct mk_and/mk_or overloads Changed test/doc.cpp and test/udoc_relation.cpp to use mk_and(expr_ref_vector) and mk_or(expr_ref_vector) without m parameter Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
916 lines
25 KiB
C++
916 lines
25 KiB
C++
/*++
|
|
Copyright (c) 2017 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
opt_parse.cpp
|
|
|
|
Abstract:
|
|
|
|
Parse utilities for optimization.
|
|
|
|
Author:
|
|
|
|
Nikolaj Bjorner (nbjorner) 2017-11-19
|
|
|
|
Revision History:
|
|
|
|
--*/
|
|
#include "opt/opt_context.h"
|
|
#include "opt/opt_parse.h"
|
|
#include <iostream>
|
|
|
|
class opt_stream_buffer {
|
|
std::istream & m_stream;
|
|
int m_val;
|
|
unsigned m_line;
|
|
public:
|
|
opt_stream_buffer(std::istream & s):
|
|
m_stream(s),
|
|
m_line(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_line;
|
|
next();
|
|
}
|
|
}
|
|
void skip_space() {
|
|
while (ch() != 10 && ((ch() >= 9 && ch() <= 13) || ch() == 32))
|
|
next();
|
|
}
|
|
void skip_line() {
|
|
while(true) {
|
|
if (eof()) {
|
|
return;
|
|
}
|
|
if (ch() == '\n') {
|
|
++m_line;
|
|
next();
|
|
return;
|
|
}
|
|
next();
|
|
}
|
|
}
|
|
bool parse_token(char const* token);
|
|
int parse_int();
|
|
unsigned parse_unsigned();
|
|
};
|
|
|
|
|
|
|
|
bool opt_stream_buffer::parse_token(char const* token) {
|
|
skip_whitespace();
|
|
char const* t = token;
|
|
while (*t && ch() && ch() == *t) {
|
|
next();
|
|
++t;
|
|
}
|
|
return 0 == *t;
|
|
}
|
|
|
|
unsigned opt_stream_buffer::parse_unsigned() {
|
|
skip_space();
|
|
if (ch() == '\n') {
|
|
return UINT_MAX;
|
|
}
|
|
unsigned val = 0;
|
|
while (ch() >= '0' && ch() <= '9') {
|
|
val = val*10 + (ch() - '0');
|
|
next();
|
|
}
|
|
return val;
|
|
}
|
|
|
|
int opt_stream_buffer::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;
|
|
opt_stream_buffer& in;
|
|
unsigned_vector& m_handles;
|
|
|
|
app_ref read_clause(unsigned& weight) {
|
|
int parsed_lit;
|
|
int var;
|
|
weight = in.parse_unsigned();
|
|
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((unsigned)var), m.mk_bool_sort());
|
|
if (parsed_lit < 0) p = m.mk_not(p);
|
|
ors.push_back(p);
|
|
}
|
|
result = to_app(mk_or(ors));
|
|
return result;
|
|
}
|
|
|
|
app_ref read_hard_clause() {
|
|
int parsed_lit;
|
|
int var;
|
|
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((unsigned)var), m.mk_bool_sort());
|
|
if (parsed_lit < 0)
|
|
p = m.mk_not(p);
|
|
ors.push_back(p);
|
|
}
|
|
result = to_app(mk_or(ors));
|
|
return result;
|
|
}
|
|
|
|
void parse_spec(unsigned& num_vars, unsigned& num_clauses, unsigned& max_weight) {
|
|
in.parse_token("wcnf");
|
|
num_vars = in.parse_unsigned();
|
|
num_clauses = in.parse_unsigned();
|
|
max_weight = in.parse_unsigned();
|
|
}
|
|
|
|
public:
|
|
|
|
wcnf(opt::context& opt, opt_stream_buffer& in, unsigned_vector& h): opt(opt), m(opt.get_manager()), in(in), m_handles(h) {
|
|
opt.set_clausal(true);
|
|
}
|
|
|
|
void parse() {
|
|
unsigned num_vars = 0, num_clauses = 0, max_weight = UINT_MAX;
|
|
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 if (*in == 'h') {
|
|
in.next();
|
|
app_ref cls = read_hard_clause();
|
|
opt.add_hard_constraint(cls);
|
|
}
|
|
else {
|
|
unsigned weight = 0;
|
|
app_ref cls = read_clause(weight);
|
|
if (weight >= max_weight) {
|
|
opt.add_hard_constraint(cls);
|
|
}
|
|
else {
|
|
unsigned id = opt.add_soft_constraint(cls, rational(weight), symbol::null);
|
|
if (m_handles.empty()) {
|
|
m_handles.push_back(id);
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
};
|
|
|
|
|
|
class opb {
|
|
opt::context& opt;
|
|
ast_manager& m;
|
|
opt_stream_buffer& in;
|
|
unsigned_vector& m_handles;
|
|
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()) << "\" expected \"x\")\n";
|
|
exit(3);
|
|
}
|
|
app_ref p(m);
|
|
int id = in.parse_int();
|
|
p = m.mk_const(symbol((unsigned)id), m.mk_bool_sort());
|
|
if (negated) p = m.mk_not(p);
|
|
in.skip_whitespace();
|
|
return p;
|
|
}
|
|
|
|
app_ref parse_ids() {
|
|
app_ref result = parse_id();
|
|
while (*in == '~' || *in == 'x') {
|
|
result = m.mk_and(result, parse_id());
|
|
}
|
|
return result;
|
|
}
|
|
|
|
rational parse_coeff_r() {
|
|
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 ('0' <= *in && *in <='9') num.push_back(*in), ++in;
|
|
num.push_back(0);
|
|
return rational(num.data());
|
|
}
|
|
|
|
app_ref parse_coeff() {
|
|
return app_ref(arith.mk_numeral(parse_coeff_r(), 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(bool is_min) {
|
|
app_ref t = parse_term();
|
|
while (!in.parse_token(";") && !in.eof()) {
|
|
if (is_min) {
|
|
t = arith.mk_add(t, parse_term());
|
|
}
|
|
else {
|
|
t = arith.mk_sub(t, parse_term());
|
|
}
|
|
}
|
|
m_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;
|
|
}
|
|
if (in.parse_token("<=")) {
|
|
t = arith.mk_le(t, parse_coeff());
|
|
in.parse_token(";");
|
|
break;
|
|
}
|
|
t = arith.mk_add(t, parse_term());
|
|
}
|
|
opt.add_hard_constraint(t);
|
|
}
|
|
public:
|
|
opb(opt::context& opt, opt_stream_buffer& in, unsigned_vector& h):
|
|
opt(opt), m(opt.get_manager()),
|
|
in(in), m_handles(h), 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(true);
|
|
}
|
|
else if (in.parse_token("max:")) {
|
|
parse_objective(false);
|
|
}
|
|
else {
|
|
parse_constraint();
|
|
}
|
|
}
|
|
}
|
|
};
|
|
|
|
void parse_wcnf(opt::context& opt, std::istream& is, unsigned_vector& h) {
|
|
opt_stream_buffer _is(is);
|
|
wcnf w(opt, _is, h);
|
|
w.parse();
|
|
}
|
|
|
|
void parse_opb(opt::context& opt, std::istream& is, unsigned_vector& h) {
|
|
opt_stream_buffer _is(is);
|
|
opb opb(opt, _is, h);
|
|
opb.parse();
|
|
}
|
|
|
|
/**
|
|
* \brief Parser for a modest subset of the CPLEX LP format.
|
|
* Reference: http://eaton.math.rpi.edu/cplex90html/reffileformatscplex/reffileformatscplex5.html
|
|
*/
|
|
|
|
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) {}
|
|
};
|
|
|
|
std::ostream& operator<<(std::ostream& out, asymbol const& c) {
|
|
if (c.m_is_num) {
|
|
return out << c.m_num;
|
|
}
|
|
else {
|
|
return out << c.m_sym;
|
|
}
|
|
}
|
|
|
|
class lp_tokenizer {
|
|
vector<asymbol> m_tokens;
|
|
unsigned m_pos;
|
|
svector<char> m_buffer;
|
|
public:
|
|
lp_tokenizer(opt_stream_buffer& 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;
|
|
}
|
|
bool neg = false;
|
|
if (c == '-') {
|
|
in.next();
|
|
c = in.ch();
|
|
m_buffer.reset();
|
|
m_buffer.push_back('-');
|
|
if (is_num(c)) {
|
|
neg = true;
|
|
}
|
|
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.data()), in.line()));
|
|
IF_VERBOSE(10, verbose_stream() << "tok: " << m_tokens.back() << "\n");
|
|
continue;
|
|
}
|
|
}
|
|
|
|
if (is_num(c)) {
|
|
rational n(0);
|
|
rational div(1);
|
|
while (is_num(c) && !in.eof()) {
|
|
n = n*rational(10) + rational(c - '0');
|
|
in.next();
|
|
c = in.ch();
|
|
}
|
|
if (c == '.') {
|
|
in.next();
|
|
c = in.ch();
|
|
while (is_num(c) && !in.eof()) {
|
|
n = n*rational(10) + rational(c - '0');
|
|
in.next();
|
|
div *= rational(10);
|
|
c = in.ch();
|
|
}
|
|
}
|
|
if (div > rational(1)) n = n / div;
|
|
if (neg) n.neg();
|
|
m_tokens.push_back(asymbol(n, in.line()));
|
|
IF_VERBOSE(10, verbose_stream() << "num: " << m_tokens.back() << "\n");
|
|
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.data()), in.line()));
|
|
IF_VERBOSE(10, verbose_stream() << "tok: " << m_tokens.back() << "\n");
|
|
}
|
|
}
|
|
|
|
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 == '(' ||
|
|
c == ')' ||
|
|
c == '~';
|
|
}
|
|
|
|
};
|
|
|
|
class lp_parse {
|
|
typedef vector<std::pair<rational, symbol> > lin_term;
|
|
|
|
struct objective {
|
|
bool m_is_max;
|
|
symbol m_name;
|
|
lin_term m_expr;
|
|
};
|
|
|
|
enum rel_op {
|
|
le, ge, eq
|
|
};
|
|
|
|
struct constraint {
|
|
symbol m_name;
|
|
symbol m_bvar;
|
|
rational m_bval;
|
|
lin_term m_expr;
|
|
rel_op m_rel;
|
|
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 {
|
|
std::optional<rational> m_lo, m_hi;
|
|
bool m_int;
|
|
bound() : m_int(false) {}
|
|
};
|
|
|
|
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, opt_stream_buffer& in, unsigned_vector& h) :
|
|
opt(opt), m_h(h), tok(in) {}
|
|
|
|
void parse() {
|
|
parse_objective();
|
|
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 const * token) {
|
|
if (peek(0) == token) {
|
|
tok.next();
|
|
return true;
|
|
}
|
|
return false;
|
|
}
|
|
|
|
void parse_objective() {
|
|
m_objective.m_is_max = minmax();
|
|
if (peek(1) == ":") {
|
|
m_objective.m_name = peek(0);
|
|
tok.next(2);
|
|
}
|
|
parse_expr(m_objective.m_expr);
|
|
}
|
|
|
|
bool minmax() {
|
|
if (try_accept("minimize"))
|
|
return false;
|
|
if (try_accept("min"))
|
|
return false;
|
|
if (try_accept("maximize"))
|
|
return true;
|
|
if (try_accept("max"))
|
|
return true;
|
|
error("expected min or max objective");
|
|
return false;
|
|
}
|
|
|
|
void parse_constraint() {
|
|
symbol name;
|
|
if (peek(1) == ":") {
|
|
name = peek(0);
|
|
tok.next(2);
|
|
}
|
|
IF_VERBOSE(10, verbose_stream() << name << "\n");
|
|
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));
|
|
}
|
|
|
|
void parse_expr(lin_term& terms) {
|
|
if (is_relation()) {
|
|
return;
|
|
}
|
|
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) == "=<";
|
|
}
|
|
|
|
bool peek_minus_infty_long(unsigned pos) {
|
|
return peek(pos) == "-" && (peek(pos+1) == "inf" || peek(pos+1) == "infinity");
|
|
}
|
|
|
|
bool peek_minus_infty_short(unsigned pos) {
|
|
return peek(pos) == "-inf" || peek(pos) == "-infinity";
|
|
}
|
|
|
|
bool peek_plus_infty_long(unsigned pos) {
|
|
return peek(pos) == "+" && (peek(pos+1) == "inf" || peek(pos+1) == "infinity");
|
|
}
|
|
|
|
bool peek_plus_infty_short(unsigned pos) {
|
|
return peek(pos) == "+inf" || peek(pos) == "+infinity";
|
|
}
|
|
|
|
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 is_relation() { return peek(0) == "=" || peek(0) == "=<" || peek(0) == ">=" || peek(0) == "=>" || peek(0) == "<="; }
|
|
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);
|
|
parse_upper(v);
|
|
}
|
|
else if (peek_minus_infty_long(0) && peek_le(2)) {
|
|
v = peek(3);
|
|
tok.next(4);
|
|
parse_upper(v);
|
|
}
|
|
else if (peek_minus_infty_short(0) && peek_le(1)) {
|
|
v = peek(2);
|
|
tok.next(3);
|
|
parse_upper(v);
|
|
}
|
|
else if (peek_plus_infty_long(2) && peek_le(1)) {
|
|
tok.next(4);
|
|
}
|
|
else if (peek_plus_infty_short(2) && peek_le(1)) {
|
|
tok.next(3);
|
|
}
|
|
else 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);
|
|
}
|
|
else {
|
|
error("bound expected");
|
|
}
|
|
}
|
|
|
|
void parse_upper(symbol const& v) {
|
|
if (peek_le(0) && tok.peek_num(1)) {
|
|
rational rhs = tok.get_num(1);
|
|
update_upper(v, rhs);
|
|
tok.next(2);
|
|
}
|
|
else if (peek_le(0) && peek_plus_infty_long(1)) {
|
|
tok.next(3);
|
|
}
|
|
else if (peek_le(0) && peek_plus_infty_short(1)) {
|
|
tok.next(2); }
|
|
|
|
}
|
|
|
|
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 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);
|
|
}
|
|
|
|
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();
|
|
}
|
|
|
|
void parse_general() {
|
|
if (peek(1) == ":" && peek(3) == "=") {
|
|
symbol const& v = peek(2);
|
|
std::cout << "TBD: " << v << "\n";
|
|
return;
|
|
}
|
|
symbol const& v = peek(0);
|
|
bound b;
|
|
m_bounds.find(v, b);
|
|
b.m_int = true;
|
|
m_bounds.insert(v, b);
|
|
tok.next();
|
|
}
|
|
|
|
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));
|
|
}
|
|
|
|
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.data()), m);
|
|
}
|
|
|
|
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, unsigned_vector& h) {
|
|
opt_stream_buffer _is(is);
|
|
lp_parse lp(opt, _is, h);
|
|
lp.parse();
|
|
}
|
|
|