Skip to content

Commit

Permalink
more flexible term parsing (#19)
Browse files Browse the repository at this point in the history
* more flexible term parsing
* update readme
* update deployment scripts
  • Loading branch information
rkaminsk authored Sep 13, 2024
1 parent 03805e7 commit 0692e0f
Show file tree
Hide file tree
Showing 11 changed files with 448 additions and 148 deletions.
9 changes: 5 additions & 4 deletions .github/conda/conda_build_config.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -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]
14 changes: 9 additions & 5 deletions .github/deploy.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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'
Expand Down Expand Up @@ -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:
Expand Down
29 changes: 18 additions & 11 deletions .github/workflows/cibuildwheel.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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:
Expand Down Expand Up @@ -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

Expand 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/[email protected]
if: ${{ github.event.inputs.wip == 'true' }}
Expand Down
4 changes: 2 additions & 2 deletions .github/workflows/conda-dev.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 3 additions & 1 deletion Makefile
Original file line number Diff line number Diff line change
@@ -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
Expand Down
30 changes: 26 additions & 4 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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 }.
Expand All @@ -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 }.
Expand Down Expand Up @@ -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
13 changes: 13 additions & 0 deletions libclingo-lpx/src/number_flint.hh
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,10 @@

#include <ios>
#include <iostream>
#include <limits>
#include <memory>
#include <new>
#include <optional>
#include <stdexcept>
#include <string>

Expand Down Expand Up @@ -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<int>;

private:
mutable fmpz num_;
Expand Down Expand Up @@ -239,6 +242,16 @@ inline auto Integer::neg() -> Integer & {
return *this;
}

inline auto Integer::as_int() const -> std::optional<int> {
if (fmpz_fits_si(&num_)) {
if (auto res = fmpz_get_si(&num_);
std::numeric_limits<int>::min() <= res && res <= std::numeric_limits<int>::max()) {
return res;
}
}
return std::nullopt;
}

inline auto Integer::impl() const -> fmpz & { return num_; }

// addition
Expand Down
13 changes: 13 additions & 0 deletions libclingo-lpx/src/number_imath.hh
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,10 @@

#include <ios>
#include <iostream>
#include <limits>
#include <memory>
#include <new>
#include <optional>
#include <stdexcept>
#include <string>

Expand Down Expand Up @@ -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<int>;
[[nodiscard]] auto impl() const -> mpz_t &;

private:
Expand Down Expand Up @@ -251,6 +254,16 @@ inline auto Integer::neg() -> Integer & {
return *this;
}

inline auto Integer::as_int() const -> std::optional<int> {
auto res = mp_small{};
if (mp_int_to_int(&num_, &res) == MP_OK) {
if (std::numeric_limits<int>::min() <= res && res <= std::numeric_limits<int>::max()) {
return res;
}
}
return std::nullopt;
}

inline auto Integer::impl() const -> mpz_t & { return num_; }

// addition
Expand Down
Loading

0 comments on commit 0692e0f

Please sign in to comment.