Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add pycosat as an optional dependency. #17440

Merged
merged 23 commits into from Aug 22, 2019
Merged
Changes from 22 commits
Commits
Show all changes
23 commits
Select commit Hold shift + click to select a range
7a28684
Add a Pycosat wrapper
certik Oct 20, 2013
14107f3
Allow to use pycosat
certik Oct 20, 2013
043ec88
Benchmark dpll2 and pycosat
certik Oct 20, 2013
497015d
Fix merge conflicts
debugger22 Aug 12, 2015
4e71126
Enable pycosat by default when installed
debugger22 Aug 12, 2015
6920e7f
Add the feature for all_models using pycosat
debugger22 Aug 12, 2015
3430c27
Fix some failing tests
debugger22 Aug 12, 2015
2038ea2
Remove benchmark file as benchmarks have been moved to other repo
debugger22 Aug 13, 2015
5797a10
Enabled exclusive tests for pycosat in the test matrix
debugger22 Aug 13, 2015
2087c9d
return a generator function
debugger22 Aug 18, 2015
5295179
Merge pycosat tests with matplotlib tests in Travis CI matrix
debugger22 Aug 19, 2015
09732cc
Convert clauses to list
debugger22 Aug 19, 2015
3a3f631
Remove the map list and update the .travis.yml for latest pycosat
debugger22 Aug 21, 2015
28fdd99
Enable testing of logic module in the respective block
debugger22 Aug 21, 2015
9de745c
Merge branch 'master' into pycosat
debugger22 Aug 23, 2015
908666d
Updated code according to present requirements
ShubhamKJha Aug 17, 2019
9c38328
Updated pycosat_satisfiable to return a generator object compatible w…
ShubhamKJha Aug 17, 2019
ecfb27c
Merge branch 'master' into pycosat
ShubhamKJha Aug 17, 2019
a9c305c
Added tests for optional dependency of pycosat and added ImportError …
ShubhamKJha Aug 21, 2019
5688c89
Added tests for optional dependency of pycosat
ShubhamKJha Aug 21, 2019
c81750b
minor fixes
ShubhamKJha Aug 21, 2019
c1aca37
Merge branch 'master' into pycosat
ShubhamKJha Aug 21, 2019
2d70eb5
Added tests for optional dependency (pycosat) as suggested
ShubhamKJha Aug 22, 2019
File filter...
Filter file types
Jump to…
Jump to file or symbol
Failed to load files and symbols.

Always

Just for now

@@ -63,7 +63,7 @@ matrix:
env:
- TEST_ASCII="true"
# space separated list of optional dependencies(conda packages) to install and test
- TEST_OPT_DEPENDENCY="numpy scipy gmpy2 matplotlib>=2.2 theano llvmlite autowrap cython wurlitzer python-symengine=0.3.* tensorflow numexpr ipython antlr-python-runtime>=4.7,<4.8 antlr>=4.7,<4.8 cloudpickle python=2.7 pyglet python-clang"
- TEST_OPT_DEPENDENCY="numpy scipy gmpy2 matplotlib>=2.2 theano llvmlite autowrap cython wurlitzer python-symengine=0.3.* tensorflow numexpr ipython antlr-python-runtime>=4.7,<4.8 antlr>=4.7,<4.8 cloudpickle python=2.7 pyglet pycosat python-clang"
addons:
apt:
packages:
@@ -78,7 +78,7 @@ matrix:
# and we aren't actually using the Travis Python anyway.
env:
- TEST_ASCII="true"
- TEST_OPT_DEPENDENCY="numpy scipy gmpy2 matplotlib theano llvmlite autowrap cython wurlitzer python-symengine=0.3.* tensorflow numexpr ipython antlr-python-runtime>=4.7,<4.8 antlr>=4.7,<4.8 cloudpickle pyglet lfortran python-clang"
- TEST_OPT_DEPENDENCY="numpy scipy gmpy2 matplotlib theano llvmlite autowrap cython wurlitzer python-symengine=0.3.* tensorflow numexpr ipython antlr-python-runtime>=4.7,<4.8 antlr>=4.7,<4.8 cloudpickle pyglet pycosat lfortran python-clang"
- TEST_SAGE="true"
addons:
apt:
@@ -25,7 +25,7 @@
# These libraries are optional, but are always imported at SymPy import time
# when they are installed. External libraries should only be added to this
# list if they are required for core SymPy functionality.
hard_optional_dependencies = ['gmpy', 'gmpy2', 'fastcache']
hard_optional_dependencies = ['gmpy', 'gmpy2', 'fastcache', 'pycosat']

import sys
import os
@@ -150,6 +150,7 @@ test_list = [
# cloudpickle
'pickling',
]
blacklist = [
@@ -187,6 +188,7 @@ doctest_list = [
# codegen
'sympy/codegen/',
]
if not (sympy.test(*test_list, blacklist=blacklist) and sympy.doctest(*doctest_list)):
@@ -227,6 +229,15 @@ EOF
unset USE_SYMENGINE
fi

if [[ "${TEST_OPT_DEPENDENCY}" == *"pycosat"* ]]; then

This comment has been minimized.

Copy link
@asmeurer

This comment has been minimized.

Copy link
@asmeurer

asmeurer Aug 21, 2019

Member

I guess you removed those lines. Having it in those lists is the correct way, with a single test/doctest run for all the modules that use optional dependencies.

This comment has been minimized.

Copy link
@ShubhamKJha

ShubhamKJha Aug 22, 2019

Author Member

Ok, done

cat << EOF | python
print('Testing PYCOSAT')
import sympy
if not (sympy.test('sympy/logic', 'sympy/assumptions') and sympy.doctest('sympy/logic'):
raise Exception('Tests failed')
EOF
fi

if [[ "${TEST_SYMPY}" == "true" ]]; then
# -We:invalid makes invalid escape sequences error in Python 3.6. See
# -#12028.
@@ -0,0 +1,48 @@
from __future__ import print_function, division

from collections import defaultdict
from heapq import heappush, heappop

from sympy import default_sort_key
from sympy.assumptions.cnf import EncodedCNF
from sympy.logic.boolalg import conjuncts, to_cnf, to_int_repr, _find_predicates, Boolean


def pycosat_satisfiable(expr, all_models=False):
import pycosat
if not isinstance(expr, EncodedCNF):
exprs = EncodedCNF()
exprs.add_prop(expr)
expr = exprs

# Return UNSAT when False (encoded as 0) is present in the CNF
if {0} in expr.data:
if all_models:
return (f for f in [False])
return False

if not all_models:
r = pycosat.solve(expr.data)
result = (r != "UNSAT")
if not result:
return result
return dict((expr.symbols[abs(lit) - 1], lit > 0) for lit in r)
else:
r = pycosat.itersolve(expr.data)
result = (r != "UNSAT")
if not result:
return result

# Make solutions sympy compatible by creating a generator
def _gen(results):
satisfiable = False
try:
while True:
sol = next(results)
yield dict((expr.symbols[abs(lit) - 1], lit > 0) for lit in sol)
satisfiable = True
except StopIteration:
if not satisfiable:
yield False

return _gen(r)
@@ -4,6 +4,7 @@
from sympy.logic.boolalg import And, Not, conjuncts, to_cnf
from sympy.core.compatibility import ordered
from sympy.core.sympify import sympify
from sympy.external.importtools import import_module


def literal_symbol(literal):
@@ -35,7 +36,7 @@ def literal_symbol(literal):
raise ValueError("Argument must be a boolean literal.")


def satisfiable(expr, algorithm="dpll2", all_models=False):
def satisfiable(expr, algorithm=None, all_models=False):
"""
Check satisfiability of a propositional sentence.
Returns a model when it succeeds.
@@ -77,12 +78,26 @@ def satisfiable(expr, algorithm="dpll2", all_models=False):
UNSAT
"""
if algorithm is None or algorithm == "pycosat":
pycosat = import_module('pycosat')
if pycosat is not None:
algorithm = "pycosat"
else:
if algorithm == "pycosat":
raise ImportError("pycosat module is not present")
# Silently fall back to dpll2 if pycosat
# is not installed

This comment has been minimized.

Copy link
@asmeurer

asmeurer Aug 20, 2019

Member

If the algorithm is given explicitly as "pycosat" it should raise an exception in this case.

algorithm = "dpll2"

if algorithm == "dpll":
from sympy.logic.algorithms.dpll import dpll_satisfiable
return dpll_satisfiable(expr)
elif algorithm == "dpll2":
from sympy.logic.algorithms.dpll2 import dpll_satisfiable
return dpll_satisfiable(expr, all_models)
elif algorithm == "pycosat":
from sympy.logic.algorithms.pycosat_wrapper import pycosat_satisfiable
return pycosat_satisfiable(expr, all_models)
raise NotImplementedError


ProTip! Use n and p to navigate between commits in a pull request.
You can’t perform that action at this time.