From bd4724e9d2b9a29cf991e8ffaad4e3edecaf21d3 Mon Sep 17 00:00:00 2001
From: Matthias Koeppe <mkoeppe@math.ucdavis.edu>
Date: Tue, 18 Jun 2024 16:59:18 -0700
Subject: [PATCH] src/sage/features/sat.py: New

---
 src/sage/features/sat.py              | 103 ++++++++++++++++++++++++++
 src/sage/sat/solvers/cryptominisat.py |   6 +-
 src/sage/sat/solvers/picosat.py       |   6 +-
 3 files changed, 109 insertions(+), 6 deletions(-)
 create mode 100644 src/sage/features/sat.py

diff --git a/src/sage/features/sat.py b/src/sage/features/sat.py
new file mode 100644
index 00000000000..6a05491ddb7
--- /dev/null
+++ b/src/sage/features/sat.py
@@ -0,0 +1,103 @@
+# sage_setup: distribution = sagemath-environment
+r"""
+Feature for testing the presence of SAT solvers
+"""
+
+from . import Executable, PythonModule
+
+
+class Glucose(Executable):
+    r"""
+    A :class:`~sage.features.Feature` describing the presence of an
+    executable from the :ref:`Glucose SAT solver <spkg_glucose>`.
+
+    EXAMPLES::
+
+        sage: from sage.features.sat import Glucose
+        sage: GlucoseExecutable().is_present()                  # optional - glucose
+        FeatureTestResult('glucose', True)
+    """
+    def __init__(self, executable="glucose"):
+        r"""
+        TESTS::
+
+            sage: from sage.features.sat import Glucose
+            sage: isinstance(Glucose(), Glucose)
+            True
+        """
+        Executable.__init__(self, name=executable, executable=executable,
+                            spkg="glucose", type="optional")
+
+
+class Kissat(Executable):
+    r"""
+    A :class:`~sage.features.Feature` describing the presence of the
+    :ref:`Kissat SAT solver <spkg_kissat>`.
+
+    EXAMPLES::
+
+        sage: from sage.features.sat import Kissat
+        sage: Kissat().is_present()                             # optional - kissat
+        FeatureTestResult('kissat', True)
+    """
+    def __init__(self):
+        r"""
+        TESTS::
+
+            sage: from sage.features.sat import Kissat
+            sage: isinstance(Kissat(), Kissat)
+            True
+        """
+        Executable.__init__(self, name="kissat", executable="kissat",
+                            spkg="kissat", type="optional")
+
+
+class Pycosat(PythonModule):
+    r"""
+    A :class:`~sage.features.Feature` describing the presence of :ref:`spkg_pycosat`.
+
+    EXAMPLES::
+
+        sage: from sage.features.sat import Pycosat
+        sage: PycosatExecutable().is_present()                  # optional - pycosat
+        FeatureTestResult('pycosat', True)
+    """
+    def __init__(self):
+        r"""
+        TESTS::
+
+            sage: from sage.features.sat import Pycosat
+            sage: isinstance(Pycosat(), Pycosat)
+            True
+        """
+        PythonModule.__init__(self, "pycosat",
+                              spkg="pycosat", type="optional")
+
+
+class Pycryptosat(PythonModule):
+    r"""
+    A :class:`~sage.features.Feature` describing the presence of :ref:`spkg_pycryptosat`.
+
+    EXAMPLES::
+
+        sage: from sage.features.sat import Pycryptosat
+        sage: PycryptosatExecutable().is_present()              # optional - pycryptosat
+        FeatureTestResult('pycryptosat', True)
+    """
+    def __init__(self):
+        r"""
+        TESTS::
+
+            sage: from sage.features.sat import Pycryptosat
+            sage: isinstance(Pycryptosat(), Pycryptosat)
+            True
+        """
+        PythonModule.__init__(self, "pycryptosat",
+                              spkg="pycryptosat", type="optional")
+
+
+def all_features():
+    return [Glucose(),
+            Kissat(),
+            Pycosat(),
+            Pycryptosat()]
diff --git a/src/sage/sat/solvers/cryptominisat.py b/src/sage/sat/solvers/cryptominisat.py
index 27955c43eef..dfb1295195d 100644
--- a/src/sage/sat/solvers/cryptominisat.py
+++ b/src/sage/sat/solvers/cryptominisat.py
@@ -22,9 +22,9 @@
 from .satsolver import SatSolver
 
 from sage.misc.lazy_import import lazy_import
-from sage.features import PythonModule
-lazy_import('pycryptosat', ['Solver'],
-            feature=PythonModule('pycryptosat', spkg='pycryptosat'))
+from sage.features.sat import Pycryptosat
+
+lazy_import('pycryptosat', ['Solver'], feature=Pycryptosat())
 
 
 class CryptoMiniSat(SatSolver):
diff --git a/src/sage/sat/solvers/picosat.py b/src/sage/sat/solvers/picosat.py
index a88f69da883..89e82170b7f 100644
--- a/src/sage/sat/solvers/picosat.py
+++ b/src/sage/sat/solvers/picosat.py
@@ -21,9 +21,9 @@
 from .satsolver import SatSolver
 
 from sage.misc.lazy_import import lazy_import
-from sage.features import PythonModule
-lazy_import('pycosat', ['solve'],
-            feature=PythonModule('pycosat', spkg='pycosat'))
+from sage.features.sat import Pycosat
+
+lazy_import('pycosat', ['solve'], feature=Pycosat())
 
 
 class PicoSAT(SatSolver):