diff --git a/README.md b/README.md index 66152ef..0944fc0 100644 --- a/README.md +++ b/README.md @@ -77,8 +77,9 @@ is equivalent to ``` Another shortcut (for compatibility with [clingo-dl]) are `&diff` constraints. -Terms in braces must be variables and the right-hand-side must be a number. -The same relations as for &sum constraints are accepted. +The same relations as for &sum constraints are accepted. +Terms in braces must should be variables and the right-hand-side should be a number. +The program ``` { x }. &diff { a-b } <= 5. diff --git a/libclingo-lpx/src/parsing.cc b/libclingo-lpx/src/parsing.cc index dd1eb68..5694683 100644 --- a/libclingo-lpx/src/parsing.cc +++ b/libclingo-lpx/src/parsing.cc @@ -242,7 +242,8 @@ struct EvaluateNum { return std::visit(EvaluateNum{}, evaluate(true, term)); } -void parse_diff_elem(Clingo::TheoryTerm const &term, std::vector &res) { +auto parse_diff_elem(Clingo::TheoryTerm const &term) -> std::vector { + std::vector res; if (match(term, "-", 2)) { auto args = term.arguments(); std::visit( @@ -268,6 +269,7 @@ void parse_diff_elem(Clingo::TheoryTerm const &term, std::vector &res) { } else { throw_syntax_error("Invalid Syntax: invalid difference constraint"); } + return res; } void parse_sum_elem(Clingo::TheoryTerm const &term, std::vector &res) { @@ -396,9 +398,12 @@ void parse_theory(Clingo::TheoryAtoms const &theory, LitMapper const &mapper, Va check_syntax(atom.has_guard() && atom.elements().size() == 1 && atom.elements().front().tuple().size() == 1 && atom.elements().front().condition().empty(), "&diff invalid difference constraint"); - auto lhs = std::vector{}; - auto &&elem = *atom.elements().begin(); - parse_diff_elem(elem.tuple().front(), lhs); + auto lhs = parse_diff_elem(atom.elements().begin()->tuple().front()); + size_t n = lhs.size(); + parse_sum_elem(atom.guard().second, lhs); + for (auto it = lhs.begin() + n, ie = lhs.end(); it != ie; ++it) { + it->co.neg(); + } auto rhs = simplify(cos, lhs); auto lit = mapper(atom.literal()); iqs.emplace_back(Inequality{std::move(lhs), std::move(rhs), evaluate_cmp(atom.guard().first), lit}); diff --git a/libclingo-lpx/src/parsing.hh b/libclingo-lpx/src/parsing.hh index 6b02ccb..0c406c5 100644 --- a/libclingo-lpx/src/parsing.hh +++ b/libclingo-lpx/src/parsing.hh @@ -24,7 +24,7 @@ constexpr char const *THEORY = R"( &minimize/0 : sum_term, directive; &maximize/0 : sum_term, directive; &sum/0 : sum_term, {<=,=,>=}, sum_term, head; - &diff/0 : sum_term, {<=,=,>=}, diff_term, head; + &diff/0 : sum_term, {<=,=,>=}, sum_term, head; &dom/0 : dom_term, {=}, dom_term, head }. )"; @@ -49,7 +49,7 @@ constexpr char const *THEORY_Q = R"( &minimize/0 : sum_term, directive; &maximize/0 : sum_term, directive; &sum/0 : sum_term, {<=,=,>=,<,>}, sum_term, head; - &diff/0 : sum_term, {<=,=,>=,<,>}, diff_term, head; + &diff/0 : sum_term, {<=,=,>=,<,>}, sum_term, head; &dom/0 : dom_term, {=}, dom_term, head }. )";