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
rkaminsk authored Sep 13, 2024
1 parent 03805e7 commit 0692e0f
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
@@ -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
@@ -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:
29 changes: 18 additions & 11 deletions .github/workflows/cibuildwheel.yml
Original file line number Diff line number Diff line change
@@ -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' }}
4 changes: 2 additions & 2 deletions .github/workflows/conda-dev.yml
Original file line number Diff line number Diff line change
@@ -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
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
30 changes: 26 additions & 4 deletions README.md
Original file line number Diff line number Diff line change
@@ -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
13 changes: 13 additions & 0 deletions libclingo-lpx/src/number_flint.hh
Original file line number Diff line number Diff line change
@@ -7,8 +7,10 @@

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

@@ -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_;
@@ -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
13 changes: 13 additions & 0 deletions libclingo-lpx/src/number_imath.hh
Original file line number Diff line number Diff line change
@@ -7,8 +7,10 @@

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

@@ -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:
@@ -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
Loading

0 comments on commit 0692e0f

Please sign in to comment.