Extend Python API

.github/workflows/pages.yml

@@ -33,7 +33,7 @@ jobs:
       - name: Install Python package
         run: pip install --no-index --find-links target/wheels/ rustsat
       - name: Build Python API docs
-        run: pip install pdoc && pdoc -o _site/pyapi/ rustsat
+        run: pip install pdoc && pdoc -o _site/pyapi/ --no-show-source rustsat
       - name: Upload artifact
         # Automatically uploads an artifact from the './_site' directory by default
         uses: actions/upload-pages-artifact@v3

pyapi/Cargo.toml

@@ -19,6 +19,7 @@ pyo3 = { version = "0.23.3", features = [
   "extension-module",
   "abi3",
   "abi3-py37",
+  "multiple-pymethods",
 ] }
 
 [build-dependencies]

pyapi/examples/pyapi-dpw.py

@@ -1,19 +1,19 @@
 from rustsat import Lit, VarManager
-from rustsat.encodings import DynamicPolyWatchdog as Dpw
+from rustsat.encodings.pb import DynamicPolyWatchdog as Dpw
 
 # Lit creates a literal object from an ipasir integer representation.  The
 # encoding takes a list of (lit, weight) pairs as input.
 input_lits = [
-  (Lit(1), 5),
-  (Lit(-2), 4),
-  (Lit(3), 3),
-  (Lit(-4), 2),
-  (Lit(5), 1),
+    (Lit(1), 5),
+    (Lit(-2), 4),
+    (Lit(3), 3),
+    (Lit(-4), 2),
+    (Lit(5), 1),
 ]
 
 # Getting unused variables is handled by a VarManager. Create one that has 5
 # variables already used.
-vm = VarManager(n_used = 5)
+vm = VarManager(n_used=5)
 
 dpw = Dpw(input_lits)
 
@@ -26,8 +26,8 @@
 # DIMACS format.
 for cl in cnf:
     for l in cl:
-        print(l.to_ipasir(), end=' ')
-    print('0')
+        print(l.to_ipasir(), end=" ")
+    print("0")
 
 # Get assumptions to enforce an upper bound of 4 on the input literals. The
 # assumptions are a list of literals.

pyapi/pyproject.toml

@@ -5,3 +5,6 @@ requires-python = ">=3.7"
 [build-system]
 requires = ["maturin>=1.0,<2.0"]
 build-backend = "maturin"
+
+[tool.maturin]
+python-source = "python"

pyapi/rustsat/__init__.pyi → pyapi/python/rustsat/__init__.pyi

@@ -1,13 +1,15 @@
 from typing import List, final
 
+from rustsat import encodings
+
 @final
 class Lit:
-    def __new__(cls, ipasir: int) -> Lit: ...
+    def __new__(cls, ipasir: int) -> "Lit": ...
     def to_ipasir(self) -> int: ...
 
 @final
 class Clause:
-    def __new__(cls, lits: List[Lit]) -> Clause: ...
+    def __new__(cls, lits: List[Lit]) -> "Clause": ...
     def is_unit(self) -> bool: ...
     def is_binary(self) -> bool: ...
     def add(self, lit: Lit) -> None: ...
@@ -17,7 +19,7 @@ class Clause:
 
 @final
 class Cnf:
-    def __new__(cls, clauses: List[Clause]) -> Cnf: ...
+    def __new__(cls, clauses: List[Clause]) -> "Cnf": ...
     def add_clause(self, clause: Clause) -> None: ...
     def add_unit(self, unit: Lit) -> None: ...
     def add_binary(self, lit1: Lit, lit2: Lit) -> None: ...
@@ -34,7 +36,7 @@ class Cnf:
 
 @final
 class VarManager:
-    def __new__(cls, n_used: int = 0) -> VarManager: ...
+    def __new__(cls, n_used: int = 0) -> "VarManager": ...
     def increase_used(self, n_used: int) -> None: ...
     def new_var(self) -> int: ...
     def n_used(self) -> int: ...

pyapi/python/rustsat/encodings/__init__.pyi

@@ -0,0 +1 @@
+from rustsat.encodings import card, pb, am1

pyapi/python/rustsat/encodings/am1/__init__.py

@@ -0,0 +1,5 @@
+from .rustsat.encodings.am1 import *
+
+__doc__ = rustsat.encodings.am1.__doc__
+if hasattr(rustsat.encodings.am1, "__all__"):
+    __all__ = rustsat.encodings.am1.__all__

pyapi/python/rustsat/encodings/am1/__init__.pyi

@@ -0,0 +1,34 @@
+from rustsat import Lit, Cnf, VarManager
+from typing import List, final
+
+@final
+class Bitwise:
+    def __new__(cls, lits: List[Lit]) -> "Bitwise": ...
+    def n_lits(self) -> int: ...
+    def n_clauses(self) -> int: ...
+    def n_vars(self) -> int: ...
+    def encode(self, var_manager: VarManager) -> Cnf: ...
+
+@final
+class Commander:
+    def __new__(cls, lits: List[Lit]) -> "Commander": ...
+    def n_lits(self) -> int: ...
+    def n_clauses(self) -> int: ...
+    def n_vars(self) -> int: ...
+    def encode(self, var_manager: VarManager) -> Cnf: ...
+
+@final
+class Ladder:
+    def __new__(cls, lits: List[Lit]) -> "Ladder": ...
+    def n_lits(self) -> int: ...
+    def n_clauses(self) -> int: ...
+    def n_vars(self) -> int: ...
+    def encode(self, var_manager: VarManager) -> Cnf: ...
+
+@final
+class Pairwise:
+    def __new__(cls, lits: List[Lit]) -> "Pairwise": ...
+    def n_lits(self) -> int: ...
+    def n_clauses(self) -> int: ...
+    def n_vars(self) -> int: ...
+    def encode(self, var_manager: VarManager) -> Cnf: ...

pyapi/python/rustsat/encodings/card/__init__.py

@@ -0,0 +1,5 @@
+from .rustsat.encodings.card import *
+
+__doc__ = rustsat.encodings.card.__doc__
+if hasattr(rustsat.encodings.card, "__all__"):
+    __all__ = rustsat.encodings.card.__all__

pyapi/python/rustsat/encodings/card/__init__.pyi

@@ -0,0 +1,12 @@
+from rustsat import Lit, Cnf, VarManager
+from typing import List, final
+
+@final
+class Totalizer:
+    def __new__(cls, lits: List[Lit]) -> "Totalizer": ...
+    def extend(self, lits: List[Lit]) -> None: ...
+    def n_lits(self) -> int: ...
+    def n_clauses(self) -> int: ...
+    def n_vars(self) -> int: ...
+    def encode_ub(self, min_ub: int, max_ub: int, var_manager: VarManager) -> Cnf: ...
+    def enforce_ub(self, ub) -> List[Lit]: ...

pyapi/python/rustsat/encodings/pb/__init__.py

@@ -0,0 +1,5 @@
+from .rustsat.encodings.pb import *
+
+__doc__ = rustsat.encodings.pb.__doc__
+if hasattr(rustsat.encodings.pb, "__all__"):
+    __all__ = rustsat.encodings.pb.__all__

pyapi/python/rustsat/encodings/pb/__init__.pyi

@@ -0,0 +1,37 @@
+from rustsat import Lit, Cnf, VarManager
+from typing import List, final
+
+@final
+class GeneralizedTotalizer:
+    def __new__(cls, wlits: List[tuple[int, Lit]]) -> "GeneralizedTotalizer": ...
+    def extend(self, lits: List[Lit]) -> None: ...
+    def weight_sum(self) -> int: ...
+    def n_clauses(self) -> int: ...
+    def n_vars(self) -> int: ...
+    def encode_ub(self, min_ub: int, max_ub: int, var_manager: VarManager) -> Cnf: ...
+    def enforce_ub(self, ub) -> List[Lit]: ...
+
+@final
+class DynamicPolyWatchdog:
+    def __new__(cls, wlits: List[tuple[int, Lit]]) -> "DynamicPolyWatchdog": ...
+    def weight_sum(self) -> int: ...
+    def n_clauses(self) -> int: ...
+    def n_vars(self) -> int: ...
+    def encode_ub(self, min_ub: int, max_ub: int, var_manager: VarManager) -> Cnf: ...
+    def enforce_ub(self, ub) -> List[Lit]: ...
+
+@final
+class BinaryAdder:
+    def __new__(cls, wlits: List[tuple[int, Lit]]) -> "BinaryAdder": ...
+    def extend(self, lits: List[Lit]) -> None: ...
+    def weight_sum(self) -> int: ...
+    def n_clauses(self) -> int: ...
+    def n_vars(self) -> int: ...
+    def encode_ub(self, min_ub: int, max_ub: int, var_manager: VarManager) -> Cnf: ...
+    def enforce_ub(self, ub) -> List[Lit]: ...
+    def encode_lb(self, min_lb: int, max_lb: int, var_manager: VarManager) -> Cnf: ...
+    def enforce_lb(self, lb) -> List[Lit]: ...
+    def encode_both(
+        self, min_bound: int, max_bound: int, var_manager: VarManager
+    ) -> Cnf: ...
+    def enforce_eq(self, val) -> List[Lit]: ...