diff --git a/.github/conda/conda_build_config.yaml b/.github/conda/conda_build_config.yaml index a70cd90..52a49f7 100644 --- a/.github/conda/conda_build_config.yaml +++ b/.github/conda/conda_build_config.yaml @@ -11,7 +11,8 @@ clingo: pin_run_as_build: clingo: x.x -# from https://github.com/phracker/MacOSX-SDKs -CONDA_BUILD_SYSROOT: - - /opt/MacOSX10.9.sdk # [osx and not arm64] - - /opt/MacOSX11.3.sdk # [osx and arm64] +MACOSX_DEPLOYMENT_TARGET: 10.15 # [osx and not arm64] +MACOSX_DEPLOYMENT_TARGET: 11.3 # [osx and arm64] +CONDA_BUILD_SYSROOT: # [osx] + - /opt/MacOSX10.15.sdk # [osx and not arm64] + - /opt/MacOSX11.3.sdk # [osx and arm64] diff --git a/.github/deploy.yml b/.github/deploy.yml index a370f2e..60abca2 100644 --- a/.github/deploy.yml +++ b/.github/deploy.yml @@ -6,6 +6,9 @@ cibw: m = match(r'#define CLINGOLPX_VERSION "([0-9]+\.[0-9]+\.[0-9]+)"', line) if m is not None: version = m.group(1) + macosx_deployment_target: + x86_64: 10.15 + arm64: 10.15 conda: package_name: @@ -15,7 +18,7 @@ conda: - 'macos-latest' - 'windows-2019' macosx-sdk: - - 'MacOSX10.9.sdk.tar.xz' + - 'MacOSX10.15.sdk.tar.xz' - 'MacOSX11.3.sdk.tar.xz' channels_release: - 'potassco' @@ -109,10 +112,11 @@ conda: pin_run_as_build: clingo: x.x - # from https://github.com/phracker/MacOSX-SDKs - CONDA_BUILD_SYSROOT: - - /opt/MacOSX10.9.sdk # [osx and not arm64] - - /opt/MacOSX11.3.sdk # [osx and arm64] + MACOSX_DEPLOYMENT_TARGET: 10.15 # [osx and not arm64] + MACOSX_DEPLOYMENT_TARGET: 11.3 # [osx and arm64] + CONDA_BUILD_SYSROOT: # [osx] + - /opt/MacOSX10.15.sdk # [osx and not arm64] + - /opt/MacOSX11.3.sdk # [osx and arm64] ppa: package_name: diff --git a/.github/workflows/cibuildwheel.yml b/.github/workflows/cibuildwheel.yml index f1092e1..d4a3aad 100644 --- a/.github/workflows/cibuildwheel.yml +++ b/.github/workflows/cibuildwheel.yml @@ -13,7 +13,7 @@ jobs: name: Build source distribution runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 with: submodules: recursive @@ -28,8 +28,9 @@ jobs: - name: Build sdist run: pipx run build --sdist - - uses: actions/upload-artifact@v3 + - uses: actions/upload-artifact@v4 with: + name: cibw-sdist path: dist/*.tar.gz build_wheels: @@ -78,19 +79,23 @@ jobs: name: "cp*-win*" env: CIBW_BUILD: "cp*-win*" - - os: macos-11 - name: "*-macos_{x86_64,arm64}" + - os: macos-13 + name: "*-macos_x86_64" env: - CIBW_ARCHS_MACOS: x86_64 arm64 + MACOSX_DEPLOYMENT_TARGET: "10.15" + - os: macos-14 + name: "*-macos_arm64" + env: + MACOSX_DEPLOYMENT_TARGET: "10.15" steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v4 with: submodules: recursive - name: Set up QEMU if: runner.os == 'Linux' - uses: docker/setup-qemu-action@v2 + uses: docker/setup-qemu-action@v3 with: platforms: all @@ -103,21 +108,23 @@ jobs: run: python .github/adjust_version.py --release - name: Build wheels - uses: pypa/cibuildwheel@v2.19.1 + uses: pypa/cibuildwheel@v2.20.0 env: ${{ matrix.cfg.env }} - - uses: actions/upload-artifact@v3 + - uses: actions/upload-artifact@v4 with: + name: cibw-wheels-${{ matrix.cfg.os }}-${{ strategy.job-index }} path: ./wheelhouse/*.whl upload_pypi: needs: [build_wheels, build_sdist] runs-on: ubuntu-latest steps: - - uses: actions/download-artifact@v3 + - uses: actions/download-artifact@v4 with: - name: artifact + pattern: cibw-* path: dist + merge-multiple: true - uses: pypa/gh-action-pypi-publish@v1.5.0 if: ${{ github.event.inputs.wip == 'true' }} diff --git a/.github/workflows/conda-dev.yml b/.github/workflows/conda-dev.yml index 7aec0bb..1f9526f 100644 --- a/.github/workflows/conda-dev.yml +++ b/.github/workflows/conda-dev.yml @@ -44,8 +44,8 @@ jobs: if: ${{ matrix.os == 'macos-latest' }} shell: pwsh run: | - Invoke-WebRequest -Uri 'https://github.com/phracker/MacOSX-SDKs/releases/download/11.3/MacOSX10.9.sdk.tar.xz' -OutFile 'MacOSX10.9.sdk.tar.xz' - sudo tar xf MacOSX10.9.sdk.tar.xz -C /opt + Invoke-WebRequest -Uri 'https://github.com/phracker/MacOSX-SDKs/releases/download/11.3/MacOSX10.15.sdk.tar.xz' -OutFile 'MacOSX10.15.sdk.tar.xz' + sudo tar xf MacOSX10.15.sdk.tar.xz -C /opt Invoke-WebRequest -Uri 'https://github.com/phracker/MacOSX-SDKs/releases/download/11.3/MacOSX11.3.sdk.tar.xz' -OutFile 'MacOSX11.3.sdk.tar.xz' sudo tar xf MacOSX11.3.sdk.tar.xz -C /opt diff --git a/Makefile b/Makefile index 58c03ee..a2e7e7b 100644 --- a/Makefile +++ b/Makefile @@ -1,12 +1,14 @@ BUILD_TYPE:=debug CLINGO_DIR:=${HOME}/.local/opt/potassco/$(BUILD_TYPE)/lib/cmake/Clingo -CXXFLAGS=-Wall -Wextra -Wpedantic -Werror +CXX=clang++ +CXXFLAGS=-Wall -Wextra -Wpedantic -Werror -stdlib=libc++ define cmake_options -G Ninja \ -S . \ -B "build/$(BUILD_TYPE)" \ -DCMAKE_INSTALL_PREFIX=${HOME}/.local/opt/potassco/$(BUILD_TYPE) \ -DCMAKE_CXX_FLAGS="$(CXXFLAGS)" \ +-DCMAKE_CXX_COMPILER="$(CXX)" \ -DClingo_DIR="$(CLINGO_DIR)" \ -DCLINGOLPX_BUILD_TESTS=On \ -DCMAKE_EXPORT_COMPILE_COMMANDS=On diff --git a/README.md b/README.md index 936790c..66152ef 100644 --- a/README.md +++ b/README.md @@ -45,17 +45,25 @@ Note that packages from the [conda-forge] channel offer better performance than ## Input format The system supports `&sum` constraints over rationals with relations among `<=`, `>=`, and `=`. -The elements of the sum constraints must have form `x`, `-x`, `n*x`, `-n*x`, or `-n/d*x` -where `x` is a function symbol or tuple, and `n` and `d` are numbers. -A number has to be either a non negative integer or decimal number in quotes. +The elements of the sum constraints and terms of guards must be linear expressions. +Quoted strings can be used to represent decimal numbers of arbitrary precision. +Terms can be nested using operators `+`, `-`, `*`, `/`. +Usage of multiplication and division is limited. +Only expressions of form `c * t`, `t * c`, and `t / c` are accepted +where `c` must not refer to variables and must be non-zero in the latter case. +If functions are used as variable names, operators `+`, `-`, `*`, `/` in their arguments are evaluated as well. +There is no special handling of strings for function arguments though. For example, the following program is accepted: ``` { x }. -&sum { x; -y; 2*x; -3*y; 2/3*x; -3/4*y, "0.75"*z } >= 100 :- x. +&sum { 2*var(1+2) } = "0.3". +&sum { var(3) } <= 3 * ("0.75"*z) :- x. +&sum { var(3); (100*y)/2 } <= 0 :- not x. ``` Furthermore, `&dom` constraints are supported, which are shortcuts for `&sum` constraints. +Terms in braces must be numbers and the right-hand-side must be a variable. The program ``` { x }. @@ -68,6 +76,19 @@ is equivalent to &sum { x } <= 2. ``` +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. +``` +{ x }. +&diff { a-b } <= 5. +``` +is equivalent to +``` +{ x }. +&sum { a-b } <= 5. +``` + When option `--strict` is passed to the solver, then also strict constraints are supported: ``` { x }. @@ -140,6 +161,7 @@ Furthermore, note that [IMath] uses the MIT and [FLINT] the LGPL license. [IMath]: https://github.com/creachadair/imath [cmake]: https://cmake.org [clingo]: https://github.com/potassco/clingo +[clingo-dl]: https://github.com/potassco/clingo-dl [conda-forge]: https://conda-forge.org/ [gperftools]: https://gperftools.github.io/gperftools/cpuprofile.html [miniconda]: https://docs.conda.io/en/latest/miniconda.html diff --git a/libclingo-lpx/src/number_flint.hh b/libclingo-lpx/src/number_flint.hh index 9059c1f..77ba3f2 100644 --- a/libclingo-lpx/src/number_flint.hh +++ b/libclingo-lpx/src/number_flint.hh @@ -7,8 +7,10 @@ #include #include +#include #include #include +#include #include #include @@ -83,6 +85,7 @@ class Integer { auto add_mul(Integer const &a, Integer const &b) && -> Integer; auto neg() -> Integer &; [[nodiscard]] auto impl() const -> fmpz &; + [[nodiscard]] auto as_int() const -> std::optional; private: mutable fmpz num_; @@ -239,6 +242,16 @@ inline auto Integer::neg() -> Integer & { return *this; } +inline auto Integer::as_int() const -> std::optional { + if (fmpz_fits_si(&num_)) { + if (auto res = fmpz_get_si(&num_); + std::numeric_limits::min() <= res && res <= std::numeric_limits::max()) { + return res; + } + } + return std::nullopt; +} + inline auto Integer::impl() const -> fmpz & { return num_; } // addition diff --git a/libclingo-lpx/src/number_imath.hh b/libclingo-lpx/src/number_imath.hh index 928c3b3..7ea37da 100644 --- a/libclingo-lpx/src/number_imath.hh +++ b/libclingo-lpx/src/number_imath.hh @@ -7,8 +7,10 @@ #include #include +#include #include #include +#include #include #include @@ -83,6 +85,7 @@ class Integer { auto add_mul(Integer const &a, Integer const &b) & -> Integer &; auto add_mul(Integer const &a, Integer const &b) && -> Integer; auto neg() -> Integer &; + [[nodiscard]] auto as_int() const -> std::optional; [[nodiscard]] auto impl() const -> mpz_t &; private: @@ -251,6 +254,16 @@ inline auto Integer::neg() -> Integer & { return *this; } +inline auto Integer::as_int() const -> std::optional { + auto res = mp_small{}; + if (mp_int_to_int(&num_, &res) == MP_OK) { + if (std::numeric_limits::min() <= res && res <= std::numeric_limits::max()) { + return res; + } + } + return std::nullopt; +} + inline auto Integer::impl() const -> mpz_t & { return num_; } // addition diff --git a/libclingo-lpx/src/parsing.cc b/libclingo-lpx/src/parsing.cc index 37963e3..dd1eb68 100644 --- a/libclingo-lpx/src/parsing.cc +++ b/libclingo-lpx/src/parsing.cc @@ -5,13 +5,17 @@ #include #include -#include +#include #include #include #include +#include namespace { +#define MATCHES(a, b) std::is_same_v>, b> +#define FWD(a) std::forward(a) + template [[nodiscard]] auto throw_syntax_error(char const *message = "Invalid Syntax") -> T { throw std::runtime_error(message); } @@ -28,7 +32,7 @@ void check_syntax(bool condition, char const *message = "Invalid Syntax") { term.arguments().size() == arity); } -auto is_string(Clingo::TheoryTerm const &term) -> bool { +[[nodiscard]] auto is_string(Clingo::TheoryTerm const &term) -> bool { if (term.type() != Clingo::TheoryTermType::Symbol) { return false; } @@ -38,166 +42,342 @@ auto is_string(Clingo::TheoryTerm const &term) -> bool { return len >= 2 && name[0] == '"' && name[len - 1] == '"'; } -[[nodiscard]] auto evaluate(Clingo::TheoryTerm const &term) -> Clingo::Symbol { - if (is_string(term)) { - char const *name = term.name(); - size_t len = std::strlen(term.name()); - // NOLINTNEXTLINE(cppcoreguidelines-pro-bounds-pointer-arithmetic) - return Clingo::String(std::string{name + 1, name + len - 1}.c_str()); - } +[[nodiscard]] auto is_invalid(Clingo::Symbol const &sym) -> bool { + return sym.type() == Clingo::SymbolType::Number && sym.number() == 0; +} - if (term.type() == Clingo::TheoryTermType::Symbol) { - return Clingo::Function(term.name(), {}); +[[nodiscard]] auto evaluate_cmp(char const *rel) -> Relation { + if (std::strcmp(rel, "<=") == 0) { + return Relation::LessEqual; + } + if (std::strcmp(rel, ">=") == 0) { + return Relation::GreaterEqual; + } + if (std::strcmp(rel, "=") == 0) { + return Relation::Equal; + } + if (std::strcmp(rel, ">") == 0) { + return Relation::Greater; + } + if (std::strcmp(rel, "<") == 0) { + return Relation::Less; } + return throw_syntax_error(); +} - if (term.type() == Clingo::TheoryTermType::Number) { - return Clingo::Number(term.number()); +template struct EB { + EB(F &f) : f{f} {} + auto operator()(Rational &&a, Rational &&b) -> Rational { return f(std::move(a), std::move(b)); } + template auto operator()([[maybe_unused]] A &&a, [[maybe_unused]] B &&b) -> Rational { + return throw_syntax_error(); } + F &f; +}; - if (match(term, "-", 1)) { - auto arg = evaluate(term.arguments().back()); - if (arg.type() == Clingo::SymbolType::Number) { - return Clingo::Number(-arg.number()); +struct EU { + auto operator()(Rational &&a) -> std::variant { return -std::move(a); } + auto operator()(Clingo::Symbol &&a) -> std::variant { + if (a.type() == Clingo::SymbolType::Function && std::strlen(a.name()) > 0) { + return Clingo::Function(a.name(), a.arguments(), !a.is_positive()); } - if (arg.type() == Clingo::SymbolType::Function) { - return Clingo::Function(arg.name(), arg.arguments(), !arg.is_positive()); + return throw_syntax_error(); + } +}; + +struct AS { + auto operator()(Rational &&a) -> Clingo::Symbol { + if (auto v = a.num().as_int(); a.den() == 1 && v) { + return Clingo::Number(*v); } return throw_syntax_error(); } + auto operator()(Clingo::Symbol &&a) -> Clingo::Symbol { return std::move(a); } +}; - check_syntax(!match(term, "..", 2) && !match(term, "*", 2) && !match(term, "/", 2)); +[[nodiscard]] auto as_sym(std::variant &&x) -> Clingo::Symbol { + return std::visit(AS{}, std::move(x)); +} - if (term.type() == Clingo::TheoryTermType::Tuple || term.type() == Clingo::TheoryTermType::Function) { - std::vector args; - args.reserve(term.arguments().size()); - for (auto const &arg : term.arguments()) { - args.emplace_back(evaluate(arg)); +[[nodiscard]] auto as_num(char const *name) -> std::optional { + size_t len = std::strlen(name); + // NOLINTNEXTLINE(cppcoreguidelines-pro-bounds-pointer-arithmetic) + if (len <= 2 || name[0] != '"' || name[len - 1] != '"') { + return std::nullopt; + } + std::regex const rgx{"(-)?([0-9]+)(\\.([0-9]+))?"}; + std::cmatch match; + // NOLINTNEXTLINE(cppcoreguidelines-pro-bounds-pointer-arithmetic) + if (!std::regex_match(name + 1, name + len - 1, match, rgx)) { + return std::nullopt; + } + std::string a = match[2]; + if (match[4].matched) { + auto const *ib = match[4].first; + auto const *it = match[4].second; + // NOLINTNEXTLINE(cppcoreguidelines-pro-bounds-pointer-arithmetic) + for (; it != ib && *(it - 1) == '0'; --it) { } - return Clingo::Function(term.type() == Clingo::TheoryTermType::Function ? term.name() : "", args); + a.append(ib, it); + a.append("/1"); + a.append(it - ib, '0'); } + // NOLINTNEXTLINE(cppcoreguidelines-avoid-magic-numbers) + Rational n{a, 10}; + if (match[1].matched) { + n.neg(); + } + n.canonicalize(); + return n; +} - return throw_syntax_error(); +[[nodiscard]] auto unquote(Clingo::Span str) -> std::string { + std::string res; + bool slash = false; + for (auto c : str) { + if (slash) { + switch (c) { + case 'n': { + res.push_back('\n'); + break; + } + case '\\': { + res.push_back('\\'); + break; + } + case '"': { + res.push_back('"'); + break; + } + default: { + assert(false); + break; + } + } + slash = false; + } else if (c == '\\') { + slash = true; + } else { + res.push_back(c); + } + } + return res; } -[[nodiscard]] auto evaluate_var(Clingo::TheoryTerm const &term) -> Clingo::Symbol { - check_syntax(!match(term, "-", 1) && !match(term, "..", 2) && !match(term, "*", 2) && !match(term, "/", 2)); - check_syntax(term.type() == Clingo::TheoryTermType::Tuple || term.type() == Clingo::TheoryTermType::Function || - term.type() == Clingo::TheoryTermType::Symbol); +[[nodiscard]] auto evaluate(bool num_str, Clingo::TheoryTerm const &term) -> std::variant; - return evaluate(term); +template +[[nodiscard]] auto evaluate(bool num_str, Clingo::TheoryTerm const &a, Clingo::TheoryTerm const &b, F f) -> Rational { + return std::visit(EB{f}, evaluate(num_str, a), evaluate(num_str, b)); } -[[nodiscard]] auto evaluate_num(Clingo::TheoryTerm const &term) -> Rational { - if (is_string(term)) { - auto const *name = term.name(); - std::regex const rgx{"(-)?([0-9]+)(\\.([0-9]+))?"}; - std::cmatch match; - // NOLINTNEXTLINE(cppcoreguidelines-pro-bounds-pointer-arithmetic) - check_syntax(std::regex_match(name + 1, name + strlen(name) - 1, match, rgx)); - std::string a = match[2]; - if (match[4].matched) { - auto const *ib = match[4].first; - auto const *it = match[4].second; - // NOLINTNEXTLINE(cppcoreguidelines-pro-bounds-pointer-arithmetic) - for (; it != ib && *(it - 1) == '0'; --it) { +auto evaluate(bool num_str, Clingo::TheoryTerm const &term) -> std::variant { + if (term.type() == Clingo::TheoryTermType::Symbol) { + const auto *cname = term.name(); + Clingo::Span name{cname, std::strlen(cname)}; + if (is_string(term)) { + if (num_str) { + if (auto res = as_num(cname); res) { + return *std::move(res); + } } - a.append(ib, it); - a.append("/1"); - a.append(it - ib, '0'); + return Clingo::String(unquote({name.begin() + 1, name.end() - 1}).c_str()); } - // NOLINTNEXTLINE(cppcoreguidelines-avoid-magic-numbers) - Rational n{a, 10}; - if (match[1].matched) { - n.neg(); - } - n.canonicalize(); - return n; + return Clingo::Function(cname, {}); } if (term.type() == Clingo::TheoryTermType::Number) { - return {term.number()}; + return Rational(term.number()); } - if (match(term, "-", 1)) { - return -evaluate_num(term.arguments().front()); + if (match(term, "+", 2)) { + return evaluate(num_str, term.arguments().front(), term.arguments().back(), + [](Rational &&a, Rational &&b) { return std::move(a) + std::move(b); }); + } + if (match(term, "-", 2)) { + return evaluate(num_str, term.arguments().front(), term.arguments().back(), + [](Rational &&a, Rational &&b) { return std::move(a) - std::move(b); }); } if (match(term, "*", 2)) { - return evaluate_num(term.arguments().front()) * evaluate_num(term.arguments().back()); + return evaluate(num_str, term.arguments().front(), term.arguments().back(), + [](Rational &&a, Rational &&b) { return std::move(a) * std::move(b); }); } if (match(term, "/", 2)) { - return evaluate_num(term.arguments().front()) / evaluate_num(term.arguments().back()); + return evaluate(num_str, term.arguments().front(), term.arguments().back(), + [](Rational &&a, Rational &&b) { return std::move(a) / std::move(b); }); } - return throw_syntax_error(); -} - -[[nodiscard]] auto evaluate_cmp(char const *rel) -> Relation { - if (std::strcmp(rel, "<=") == 0) { - return Relation::LessEqual; - } - if (std::strcmp(rel, ">=") == 0) { - return Relation::GreaterEqual; + if (match(term, "-", 1)) { + return std::visit(EU{}, evaluate(num_str, term.arguments().front())); } - if (std::strcmp(rel, "=") == 0) { - return Relation::Equal; + + check_syntax(!match(term, "..", 2)); + + if (term.type() == Clingo::TheoryTermType::Tuple || term.type() == Clingo::TheoryTermType::Function) { + std::vector args; + args.reserve(term.arguments().size()); + for (auto const &arg : term.arguments()) { + args.emplace_back(as_sym(evaluate(false, arg))); + } + return Clingo::Function(term.type() == Clingo::TheoryTermType::Function ? term.name() : "", args); } - if (std::strcmp(rel, ">") == 0) { - return Relation::Greater; + + return throw_syntax_error(); +} + +struct EvaluateVar { + auto operator()([[maybe_unused]] Rational &&a) -> Clingo::Symbol { return throw_syntax_error(); } + auto operator()(Clingo::Symbol &&a) -> Clingo::Symbol { return std::move(a); } +}; + +[[nodiscard]] auto evaluate_var(Clingo::TheoryTerm const &term) -> Clingo::Symbol { + return std::visit(EvaluateVar{}, evaluate(false, term)); +} + +struct EvaluateNum { + auto operator()(Rational &&a) -> Rational { return std::move(a); } + auto operator()([[maybe_unused]] Clingo::Symbol &&a) -> Rational { return throw_syntax_error(); } +}; + +[[nodiscard]] auto evaluate_num(Clingo::TheoryTerm const &term) -> Rational { + return std::visit(EvaluateNum{}, evaluate(true, term)); +} + +void parse_diff_elem(Clingo::TheoryTerm const &term, std::vector &res) { + if (match(term, "-", 2)) { + auto args = term.arguments(); + std::visit( + [&res](auto &&a) { + if constexpr (MATCHES(a, Rational)) { + res.emplace_back(Term{FWD(a), Clingo::Number(0)}); + } + if constexpr (MATCHES(a, Clingo::Symbol)) { + res.emplace_back(Term{Rational(1), FWD(a)}); + } + }, + evaluate(true, args.front())); + std::visit( + [&res](auto &&a) { + if constexpr (MATCHES(a, Rational)) { + res.emplace_back(Term{-FWD(a), Clingo::Number(0)}); + } + if constexpr (MATCHES(a, Clingo::Symbol)) { + res.emplace_back(Term{Rational(-1), FWD(a)}); + } + }, + evaluate(true, args.back())); + } else { + throw_syntax_error("Invalid Syntax: invalid difference constraint"); } - if (std::strcmp(rel, "<") == 0) { - return Relation::Less; +} + +void parse_sum_elem(Clingo::TheoryTerm const &term, std::vector &res) { + if (term.type() == Clingo::TheoryTermType::Number) { + res.emplace_back(Term{FWD(term.number()), Clingo::Number(0)}); + } else if (match(term, "+", 2)) { + auto args = term.arguments(); + parse_sum_elem(args.front(), res); + parse_sum_elem(args.back(), res); + } else if (match(term, "-", 2)) { + auto args = term.arguments(); + parse_sum_elem(args.front(), res); + auto pos = res.size(); + parse_sum_elem(args.back(), res); + for (auto it = res.begin() + pos, ie = res.end(); it != ie; ++it) { + it->co = -it->co; + } + } else if (match(term, "-", 1)) { + auto pos = res.size(); + parse_sum_elem(term.arguments().front(), res); + for (auto it = res.begin() + pos, ie = res.end(); it != ie; ++it) { + it->co = -it->co; + } + } else if (match(term, "+", 1)) { + parse_sum_elem(term.arguments().front(), res); + } else if (match(term, "*", 2)) { + auto args = term.arguments(); + std::vector lhs; + std::vector rhs; + parse_sum_elem(args.front(), lhs); + parse_sum_elem(args.back(), rhs); + for (auto &[l_co, l_var] : lhs) { + for (auto &[r_co, r_var] : rhs) { + check_syntax(is_invalid(l_var) || is_invalid(r_var)); + auto var = is_invalid(l_var) ? r_var : l_var; + res.emplace_back(Term{l_co * r_co, var}); + } + } + } else if (match(term, "/", 2)) { + auto args = term.arguments(); + std::vector lhs; + parse_sum_elem(args.front(), lhs); + auto rhs = evaluate_num(args.back()); + check_syntax(rhs != 0); + for (auto &[co, var] : lhs) { + res.emplace_back(Term{std::move(co) / rhs, var}); + } + } else if (is_string(term)) { + if (auto num = as_num(term.name())) { + res.emplace_back(Term{*num, Clingo::Number(0)}); + } else { + res.emplace_back(Term{1, evaluate_var(term)}); + } + } else if (term.type() == Clingo::TheoryTermType::Symbol || term.type() == Clingo::TheoryTermType::Function || + term.type() == Clingo::TheoryTermType::Tuple) { + res.emplace_back(Term{1, evaluate_var(term)}); + } else { + throw_syntax_error("Invalid Syntax: invalid sum constraint"); } - return throw_syntax_error(); } -[[nodiscard]] auto evaluate_terms(LitMapper const &mapper, VarMap &var_map, std::vector &iqs, - Clingo::TheoryElementSpan elements) -> std::vector { +[[nodiscard]] auto parse_sum_elems(LitMapper const &mapper, VarMap &var_map, std::vector &iqs, + Clingo::TheoryElementSpan elements) -> std::vector { std::vector lhs; for (auto &&elem : elements) { check_syntax(elem.tuple().size() == 1); auto &&term = elem.tuple().front(); - if (match(term, "-", 1)) { - lhs.emplace_back(Term{-1, evaluate_var(term.arguments().back())}); - } else if (match(term, "*", 2)) { - lhs.emplace_back(Term{evaluate_num(term.arguments().front()), evaluate_var(term.arguments().back())}); - } else { - lhs.emplace_back(Term{1, evaluate_var(term)}); - } + size_t n = lhs.size(); + parse_sum_elem(term, lhs); if (!elem.condition().empty()) { - auto res = var_map.try_emplace(std::make_pair(lhs.back().var, elem.condition_id()), - Clingo::Number(safe_cast(var_map.size()))); - if (res.second) { - auto lit = mapper(elem.condition_id()); - iqs.emplace_back(Inequality{{{1, res.first->second}}, 0, Relation::Equal, -lit}); - iqs.emplace_back(Inequality{{{1, res.first->second}, {-1, lhs.back().var}}, 0, Relation::Equal, lit}); + for (auto it = lhs.begin() + n, ie = lhs.end(); it != ie; ++it) { + auto res = var_map.try_emplace(std::make_pair(it->var, elem.condition_id()), + Clingo::Number(safe_cast(var_map.size() + 1))); + if (res.second) { + auto lit = mapper(elem.condition_id()); + iqs.emplace_back(Inequality{{{1, res.first->second}}, 0, Relation::Equal, -lit}); + iqs.emplace_back(Inequality{{{1, res.first->second}, {-1, it->var}}, 0, Relation::Equal, lit}); + } + it->var = res.first->second; } - lhs.back().var = res.first->second; } } return lhs; } -void simplify(std::unordered_map &cos, std::vector &terms) { +auto simplify(std::unordered_map &cos, std::vector &terms) -> Rational { auto ib = terms.begin(); auto ie = terms.end(); + auto rhs = Rational{0}; // combine cofficients cos.clear(); - std::for_each(ib, ie, [&cos](Term &term) { - if (auto [jt, res] = cos.emplace(term.var, term); !res) { - jt->second.co += term.co; + std::for_each(ib, ie, [&cos, &rhs](Term &term) { + if (is_invalid(term.var)) { + rhs -= std::move(term.co); + term.co = 0; + } else if (auto [jt, res] = cos.emplace(term.var, term); !res) { + jt->second.co += std::move(term.co); term.co = 0; } }); // remove terms with zero coeffcients terms.erase(std::remove_if(ib, ie, [](Term const &term) { return term.co == 0; }), ie); -} -} // namespace + return rhs; +} -void evaluate_theory(Clingo::TheoryAtoms const &theory, LitMapper const &mapper, VarMap &var_map, - std::vector &iqs, std::vector &objective) { +void parse_theory(Clingo::TheoryAtoms const &theory, LitMapper const &mapper, VarMap &var_map, + std::vector &iqs, std::vector &objective) { std::unordered_map cos; for (auto &&atom : theory) { if (match(atom.term(), "dom", 0)) { @@ -212,15 +392,29 @@ void evaluate_theory(Clingo::TheoryAtoms const &theory, LitMapper const &mapper, iqs.emplace_back(Inequality{{{1, var}}, evaluate_num(term.arguments().back()), Relation::LessEqual, lit}); iqs.emplace_back( Inequality{{{1, var}}, evaluate_num(term.arguments().front()), Relation::GreaterEqual, lit}); + } else if (match(atom.term(), "diff", 0)) { + 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 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}); } else if (match(atom.term(), "sum", 0)) { check_syntax(atom.has_guard(), "&sum constraints need guards"); - auto lhs = evaluate_terms(mapper, var_map, iqs, atom.elements()); + auto lhs = parse_sum_elems(mapper, var_map, iqs, atom.elements()); + 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()); - simplify(cos, lhs); - iqs.emplace_back( - Inequality{std::move(lhs), evaluate_num(atom.guard().second), evaluate_cmp(atom.guard().first), lit}); + iqs.emplace_back(Inequality{std::move(lhs), std::move(rhs), evaluate_cmp(atom.guard().first), lit}); } else if (match(atom.term(), "minimize", 0) || match(atom.term(), "maximize", 0)) { - auto lhs = evaluate_terms(mapper, var_map, iqs, atom.elements()); + auto lhs = parse_sum_elems(mapper, var_map, iqs, atom.elements()); if (match(atom.term(), "minimize", 0)) { for (auto &term : lhs) { term.co.neg(); @@ -229,5 +423,13 @@ void evaluate_theory(Clingo::TheoryAtoms const &theory, LitMapper const &mapper, std::move(lhs.begin(), lhs.end(), std::back_inserter(objective)); } } - simplify(cos, objective); + auto rhs = simplify(cos, objective); + check_syntax(rhs == 0, "objective must not contain constants"); +} + +} // namespace + +void evaluate_theory(Clingo::TheoryAtoms const &theory, LitMapper const &mapper, VarMap &var_map, + std::vector &iqs, std::vector &objective) { + parse_theory(theory, mapper, var_map, iqs, objective); } diff --git a/libclingo-lpx/src/parsing.hh b/libclingo-lpx/src/parsing.hh index 0d56d29..6b02ccb 100644 --- a/libclingo-lpx/src/parsing.hh +++ b/libclingo-lpx/src/parsing.hh @@ -7,40 +7,50 @@ constexpr char const *THEORY = R"( #theory lp { sum_term { - - : 3, unary; - * : 1, binary, left; - / : 1, binary, left + + : 1, binary, left; + - : 1, binary, left; + * : 2, binary, left; + / : 2, binary, left; + - : 3, unary }; dom_term { .. : 0, binary, left; - * : 1, binary, left; - / : 1, binary, left; + + : 1, binary, left; + - : 1, binary, left; + * : 2, binary, left; + / : 2, binary, left; - : 3, unary }; &minimize/0 : sum_term, directive; &maximize/0 : sum_term, directive; - &sum/0 : sum_term, {<=,=,>=}, sum_term, head; - &dom/0 : dom_term, {=}, sum_term, head + &sum/0 : sum_term, {<=,=,>=}, sum_term, head; + &diff/0 : sum_term, {<=,=,>=}, diff_term, head; + &dom/0 : dom_term, {=}, dom_term, head }. )"; constexpr char const *THEORY_Q = R"( #theory lp { sum_term { - - : 3, unary; - * : 1, binary, left; - / : 1, binary, left + + : 1, binary, left; + - : 1, binary, left; + * : 2, binary, left; + / : 2, binary, left; + - : 3, unary }; dom_term { .. : 0, binary, left; - * : 1, binary, left; - / : 1, binary, left; + + : 1, binary, left; + - : 1, binary, left; + * : 2, binary, left; + / : 2, binary, left; - : 3, unary }; &minimize/0 : sum_term, directive; &maximize/0 : sum_term, directive; - &sum/0 : sum_term, {<=,=,>=,<,>}, sum_term, head; - &dom/0 : dom_term, {=}, sum_term, head + &sum/0 : sum_term, {<=,=,>=,<,>}, sum_term, head; + &diff/0 : sum_term, {<=,=,>=,<,>}, diff_term, head; + &dom/0 : dom_term, {=}, dom_term, head }. )"; diff --git a/libclingo-lpx/tests/parsing.cc b/libclingo-lpx/tests/parsing.cc index 2a8f8f9..d5cd70a 100644 --- a/libclingo-lpx/tests/parsing.cc +++ b/libclingo-lpx/tests/parsing.cc @@ -58,7 +58,7 @@ TEST_CASE("parsing") { REQUIRE(str(eqs.front()) == "-x + 2/3*y = -1"); } - SECTION("example 3") { + SECTION("example 4") { ctl.add("base", {}, "&minimize { 3*x }. &maximize { -y }."); ctl.ground({{"base", {}}}); @@ -72,4 +72,30 @@ TEST_CASE("parsing") { [](auto &a, auto &b) { return std::make_pair(a.var, a.co) < std::make_pair(b.var, b.co); }); REQUIRE(str(Inequality{objective, 0, Relation::Equal, 0}) == "-3*x + -y = 0"); } + + SECTION("example 5") { + ctl.add("base", {}, "&sum { 2*(x+3*y)/7; 10 } = x*3-z.\n"); + ctl.ground({{"base", {}}}); + + VarMap vars; + std::vector eqs; + std::vector objective; + evaluate_theory(ctl.theory_atoms(), mapper, vars, eqs, objective); + REQUIRE(eqs.size() == 1); + REQUIRE(objective.empty()); + REQUIRE(str(eqs.front()) == "-19/7*x + 6/7*y + z = -10"); + } + + SECTION("example 5") { + ctl.add("base", {}, R"(&sum { x } = "123.0".)"); + ctl.ground({{"base", {}}}); + + VarMap vars; + std::vector eqs; + std::vector objective; + evaluate_theory(ctl.theory_atoms(), mapper, vars, eqs, objective); + REQUIRE(eqs.size() == 1); + REQUIRE(objective.empty()); + REQUIRE(str(eqs.front()) == "x = 123"); + } }