From 8863d294646b0c084acd1b3059d0f4293365419a Mon Sep 17 00:00:00 2001 From: Alexander Scheel Date: Sat, 24 Feb 2024 21:07:16 -0500 Subject: [PATCH] Fix build, linting, typechecking against cms5 v5.11.21 Signed-off-by: Alexander Scheel --- Makefile | 5 ++++- python/model.py | 2 +- python/var.py | 4 ++-- python/vec.py | 12 ++++++------ src/cmsh.h | 2 +- src/constraint_t.cpp | 2 +- 6 files changed, 15 insertions(+), 12 deletions(-) diff --git a/Makefile b/Makefile index aa52494..b64fe57 100644 --- a/Makefile +++ b/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 diff --git a/python/model.py b/python/model.py index 14fd288..bd23ccd 100644 --- a/python/model.py +++ b/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 diff --git a/python/var.py b/python/var.py index 39fc0dc..a0dc674 100644 --- a/python/var.py +++ b/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) diff --git a/python/vec.py b/python/vec.py index 3eb236c..a4c992e 100644 --- a/python/vec.py +++ b/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) diff --git a/src/cmsh.h b/src/cmsh.h index 2377007..6c04efd 100644 --- a/src/cmsh.h +++ b/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 diff --git a/src/constraint_t.cpp b/src/constraint_t.cpp index 1fbfcd4..d62332e 100644 --- a/src/constraint_t.cpp +++ b/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.