Updates to support clingo-cffi (#20657)
* Support clingo when used with cffi
Clingo recently merged in a new Python module option based on cffi.
Compatibility with this module requires a few changes to spack - it does not automatically convert strings/ints/etc to Symbol and clingo.Symbol.string throws on failure.
manually convert str/int to clingo.Symbol types
catch stringify exceptions
add job for clingo-cffi to Spack CI
switch to potassco-vendored wheel for clingo-cffi CI
on_unsat argument when cffi
(cherry picked from commit 93ed1a410c
)
This commit is contained in:
parent
8d13193434
commit
14e179398f
51
.github/workflows/linux_unit_tests.yaml
vendored
51
.github/workflows/linux_unit_tests.yaml
vendored
@ -138,3 +138,54 @@ jobs:
|
|||||||
- uses: codecov/codecov-action@v1
|
- uses: codecov/codecov-action@v1
|
||||||
with:
|
with:
|
||||||
flags: unittests,linux,clingo
|
flags: unittests,linux,clingo
|
||||||
|
clingo-cffi:
|
||||||
|
# Test for the clingo based solver using the CFFI package
|
||||||
|
runs-on: ubuntu-latest
|
||||||
|
steps:
|
||||||
|
- uses: actions/checkout@v2
|
||||||
|
with:
|
||||||
|
fetch-depth: 0
|
||||||
|
- uses: actions/setup-python@v2
|
||||||
|
with:
|
||||||
|
python-version: 3.8
|
||||||
|
- name: Install System packages
|
||||||
|
run: |
|
||||||
|
sudo apt-get -y update
|
||||||
|
# Needed for unit tests
|
||||||
|
sudo apt-get install -y coreutils gfortran graphviz gnupg2 mercurial
|
||||||
|
sudo apt-get install -y ninja-build patchelf
|
||||||
|
# Needed for kcov
|
||||||
|
sudo apt-get -y install cmake binutils-dev libcurl4-openssl-dev
|
||||||
|
sudo apt-get -y install zlib1g-dev libdw-dev libiberty-dev
|
||||||
|
- name: Install Python packages
|
||||||
|
run: |
|
||||||
|
pip install --upgrade pip six setuptools codecov coverage cffi
|
||||||
|
pip install -i https://test.pypi.org/simple/ clingo-cffi
|
||||||
|
- name: Setup git configuration
|
||||||
|
run: |
|
||||||
|
# Need this for the git tests to succeed.
|
||||||
|
git --version
|
||||||
|
. .github/workflows/setup_git.sh
|
||||||
|
- name: Install kcov for bash script coverage
|
||||||
|
env:
|
||||||
|
KCOV_VERSION: 34
|
||||||
|
run: |
|
||||||
|
KCOV_ROOT=$(mktemp -d)
|
||||||
|
wget --output-document=${KCOV_ROOT}/${KCOV_VERSION}.tar.gz https://github.com/SimonKagstrom/kcov/archive/v${KCOV_VERSION}.tar.gz
|
||||||
|
tar -C ${KCOV_ROOT} -xzvf ${KCOV_ROOT}/${KCOV_VERSION}.tar.gz
|
||||||
|
mkdir -p ${KCOV_ROOT}/build
|
||||||
|
cd ${KCOV_ROOT}/build && cmake -Wno-dev ${KCOV_ROOT}/kcov-${KCOV_VERSION} && cd -
|
||||||
|
make -C ${KCOV_ROOT}/build && sudo make -C ${KCOV_ROOT}/build install
|
||||||
|
- name: Run unit tests
|
||||||
|
run: |
|
||||||
|
whoami && echo PWD=$PWD && echo HOME=$HOME && echo SPACK_TEST_SOLVER=$SPACK_TEST_SOLVER
|
||||||
|
python -c "import clingo; print(hasattr(clingo.Symbol, '_rep'), clingo.__version__)"
|
||||||
|
. share/spack/setup-env.sh
|
||||||
|
spack compiler find
|
||||||
|
spack solve mpileaks%gcc
|
||||||
|
coverage run $(which spack) unit-test -v
|
||||||
|
coverage combine
|
||||||
|
coverage xml
|
||||||
|
- uses: codecov/codecov-action@v1
|
||||||
|
with:
|
||||||
|
flags: unittests,linux,clingo
|
||||||
|
@ -18,6 +18,8 @@
|
|||||||
|
|
||||||
try:
|
try:
|
||||||
import clingo
|
import clingo
|
||||||
|
# There may be a better way to detect this
|
||||||
|
clingo_cffi = hasattr(clingo.Symbol, '_rep')
|
||||||
except ImportError:
|
except ImportError:
|
||||||
clingo = None
|
clingo = None
|
||||||
|
|
||||||
@ -119,11 +121,11 @@ def __call__(self, *args):
|
|||||||
def symbol(self, positive=True):
|
def symbol(self, positive=True):
|
||||||
def argify(arg):
|
def argify(arg):
|
||||||
if isinstance(arg, bool):
|
if isinstance(arg, bool):
|
||||||
return str(arg)
|
return clingo.String(str(arg))
|
||||||
elif isinstance(arg, int):
|
elif isinstance(arg, int):
|
||||||
return arg
|
return clingo.Number(arg)
|
||||||
else:
|
else:
|
||||||
return str(arg)
|
return clingo.String(str(arg))
|
||||||
return clingo.Function(
|
return clingo.Function(
|
||||||
self.name, [argify(arg) for arg in self.args], positive=positive)
|
self.name, [argify(arg) for arg in self.args], positive=positive)
|
||||||
|
|
||||||
@ -318,18 +320,26 @@ def solve(
|
|||||||
def on_model(model):
|
def on_model(model):
|
||||||
models.append((model.cost, model.symbols(shown=True, terms=True)))
|
models.append((model.cost, model.symbols(shown=True, terms=True)))
|
||||||
|
|
||||||
solve_result = self.control.solve(
|
solve_kwargs = {"assumptions": self.assumptions,
|
||||||
assumptions=self.assumptions,
|
"on_model": on_model,
|
||||||
on_model=on_model,
|
"on_core": cores.append}
|
||||||
on_core=cores.append
|
if clingo_cffi:
|
||||||
)
|
solve_kwargs["on_unsat"] = cores.append
|
||||||
|
solve_result = self.control.solve(**solve_kwargs)
|
||||||
timer.phase("solve")
|
timer.phase("solve")
|
||||||
|
|
||||||
# once done, construct the solve result
|
# once done, construct the solve result
|
||||||
result.satisfiable = solve_result.satisfiable
|
result.satisfiable = solve_result.satisfiable
|
||||||
|
|
||||||
def stringify(x):
|
def stringify(x):
|
||||||
return x.string or str(x)
|
if clingo_cffi:
|
||||||
|
# Clingo w/ CFFI will throw an exception on failure
|
||||||
|
try:
|
||||||
|
return x.string
|
||||||
|
except RuntimeError:
|
||||||
|
return str(x)
|
||||||
|
else:
|
||||||
|
return x.string or str(x)
|
||||||
|
|
||||||
if result.satisfiable:
|
if result.satisfiable:
|
||||||
builder = SpecBuilder(specs)
|
builder = SpecBuilder(specs)
|
||||||
|
Loading…
Reference in New Issue
Block a user