Fix build, linting, typechecking against cms5 v5.11.21

Signed-off-by: Alexander Scheel <[email protected]>

Makefile

@@ -53,7 +53,7 @@ build/.objects:
 	mkdir -p build/.objects
 
 cmslibs: dirs
-	cp -r ${CMS}/cmsat5-src/cryptominisat5 build/include/
+	cp -r ${CMS}/include/cryptominisat5 build/include/
 	cp -r ${CMS}/lib/libcryptominisat5.so* build/cmsh/
 
 native: dirs build/cmsh/libcmsh.so build/cmsh/_native${PYEXT}
@@ -81,6 +81,7 @@ test: check
 check: check-native
 	build/basic_api
 	build/sudoku
+	${PYTHON} -c 'import pytest' || ${PYTHON} -m pip install --user pytest
 	PYTHONPATH=build ${PYTHON} -m pytest --ignore=msoos_cryptominisat
 
 check-native: cmsh build/basic_api build/sudoku
@@ -102,9 +103,11 @@ clean:
 
 # Helpers
 lint:
+	${PYTHON} -c 'import pylint' || ${PYTHON} -m pip install --user pylint
 	${PYTHON} -m pylint --disable=R0914,E1136 build/cmsh
 
 typecheck:
+	${PYTHON} -c 'import mypy' || ${PYTHON} -m pip install --user mypy
 	cd build && ${PYTHON} -m mypy --python-executable ${PYTHON} cmsh
 	MYPYPATH="build" ${PYTHON} -m mypy --python-executable ${PYTHON} --ignore-missing-imports tests/python
 

python/model.py

@@ -2,7 +2,7 @@
 This module contains the main Module class.
 """
 
-# pylint: disable=line-too-long,no-name-in-module,no-self-use
+# pylint: disable=line-too-long,no-name-in-module
 
 import functools
 from typing import List, Optional

python/var.py

@@ -119,7 +119,7 @@ def __eq__(self, other):
             raise TypeError(msg)
 
         if not isinstance(other, (Variable, bool)):
-            msg = "Can't compare Variable with %s" % type(other)
+            msg = f"Can't compare Variable with {type(other)}"
             raise TypeError(msg)
         return b_eq(self, other)
 
@@ -131,7 +131,7 @@ def __ne__(self, other):
             raise TypeError(msg)
 
         if not isinstance(other, (Variable, bool)):
-            msg = "Can't compare Variable with %s" % type(other)
+            msg = f"Can't compare Variable with {type(other)}"
             raise TypeError(msg)
         return b_ne(self, other)
 

python/vec.py

@@ -21,7 +21,7 @@ class Vector:
     hash_code: int
     count: int
 
-    def __init__(self, model, width: Optional[int] = None, vector: Union['Vector', IVariableIs] = None):
+    def __init__(self, model, width: Optional[int] = None, vector: Union['Vector', IVariableIs, None] = None):
         """
         Initialize a new Vector object. Either specify width or vector, but not
         both. When width is specified, creates a new Vector with width number
@@ -273,7 +273,7 @@ def shiftl(self, amount: int = 1, filler: VariableSoft = False):
         new_vec = self.variables[amount:] + [filler]*amount
         return self.model.to_vector(new_vec)
 
-    def shiftr(self, amount: int = 1, filler: VariableSoft = None) -> Union[VectorLike, 'Vector']:
+    def shiftr(self, amount: int = 1, filler: Optional[VariableSoft] = None) -> Union[VectorLike, 'Vector']:
         """
         Create a new Vector representing this one shifted right by amount
         bits, optionally filling in with filler bits (when not None). This
@@ -485,7 +485,7 @@ def insert(self, index: int, obj: VariableSoft) -> None:
         """
         self.count += 1
         self.variables = self.variables[0:index] + [obj] + self.variables[index:]
-        self.hash_code = tuple(self.variables).__hash__()
+        self.hash_code = hash(tuple(self.variables))
 
     def __hash__(self) -> int:
         return self.hash_code
@@ -553,11 +553,11 @@ def __validate_size__(left: List[VariableSoft], l_fixed: bool, right: List[Varia
     r_len = len(right)
 
     if l_fixed and r_fixed and l_len != r_len and mismatch_fatal:
-        raise ValueError("Mismatch sizes: %d vs %d" % (l_len, r_len))
+        raise ValueError(f"Mismatch sizes: {l_len} vs {r_len}")
     if l_fixed and l_len < r_len and mismatch_fatal:
-        raise ValueError("Value of constant (%d) exceeds size: %d" % (r_len, l_len))
+        raise ValueError(f"Value of constant ({r_len}) exceeds size: {l_len}")
     if r_fixed and r_len < l_len and mismatch_fatal:
-        raise ValueError("Value of constant (%d) exceeds size: %d" % (l_len, r_len))
+        raise ValueError(f"Value of constant ({l_len}) exceeds size: {r_len}")
 
     if l_len < r_len:
         l_prefix: List[VariableSoft] = [False] * (r_len - l_len)

src/cmsh.h

@@ -84,7 +84,7 @@ namespace cmsh {
             // Operator for checking whether or not two 'constraint_t's are
             // equal. This is done on the basis of left, op, and right
             // variables. value is ignored.
-            bool operator==(const constraint_t& other);
+            bool operator==(const constraint_t& other) const;
 
             // A hash function for this class. Allows us to implement a
             // hashable interface and put constraint_t directly into a

src/constraint_t.cpp

@@ -42,7 +42,7 @@ void constraint_t::add(model_t *m) {
     tseitin(m);
 }
 
-bool constraint_t::operator==(const constraint_t& other) {
+bool constraint_t::operator==(const constraint_t& other) const {
     // Two constraint_t instances are equal <=> the operands are equal and
     // the operator are equal. The output of the gate may or may not be
     // present in either of these instances, so ignore it in this check.