Merge branch 'master' into deploy

Makefile

@@ -54,5 +54,5 @@ compile-macos-arm:
 
 .PHONY: test
 test:
-	python -m pytest --ignore=venv
+	export PYTHONPATH=.;python -m pytest --ignore=venv --ignore-glob="venv_*"
 

pysdd/lib/sdd-2.0/include/sddapi.h

@@ -23,8 +23,8 @@
 
 //sdd types
 typedef size_t SddSize; //number of nodes, sizes of hash tables, etc
-typedef unsigned int SddNodeSize; //size of decomposition for sdd nodes
-typedef unsigned int SddRefCount; //refcount
+typedef size_t SddNodeSize; //size of decomposition for sdd nodes, changed to size_t for cross-platform compatibility
+typedef size_t SddRefCount; //refcount, changed to size_t for cross-platform compatibility
 typedef unsigned long long SddModelCount; //model counts
 typedef double SddWmc; // weighted model count
 typedef long SddLiteral; //literals of clauses

pysdd/lib/sdd-2.0/src/fnf/compiler.c

@@ -25,7 +25,7 @@ SddNode* degenerate_fnf_test(Fnf* fnf, SddManager* manager) {
 
   if(count==0) return ONE(manager,op);
 
-  for(int i=0; i<count; i++) {
+  for(SddSize i=0; i<count; i++) {
     if (fnf->litsets[i].literal_count == 0)
       return ZERO(manager,op);
   }
@@ -43,7 +43,7 @@ SddNode* fnf_to_sdd_auto(Fnf* fnf, SddManager* manager) {
 
   if(verbose) { printf("\nclauses: %ld ",count); fflush(stdout); }
   SddNode* node = ONE(manager,op);
-  for(int i=0; i<count; i++) {
+  for(SddSize i=0; i<count; i++) {
     sort_litsets_by_lca(litsets+i,count-i,manager);
     sdd_ref(node,manager);
     SddNode* l = apply_litset(litsets[i],manager);
@@ -67,7 +67,7 @@ SddNode* fnf_to_sdd_manual(Fnf* fnf, SddManager* manager) {
 
   if(verbose) { printf("\nclauses: %ld ",count); fflush(stdout); }
   SddNode* node = ONE(manager,op);
-  for(int i=0; i<count; i++) {
+  for(SddSize i=0; i<count; i++) {
     if(period > 0 && i > 0 && i%period==0) {
       // after every period clauses
       sdd_ref(node,manager);

pysdd/lib/sdd-2.0/src/fnf/utils.c

@@ -57,7 +57,8 @@ int litset_cmp_lca(const void* litset1_loc, const void* litset2_loc) {
 //last: by id to obtain unique order
 void sort_litsets_by_lca(LitSet** litsets, SddSize size, SddManager* manager) {
   //compute lcas of litsets
-  for(SddLiteral i=0; i<size; i++) {
+  // i was SddLiteral but to be type compatible and since i is always positive, changed to SddSize
+  for(SddSize i=0; i<size; i++) {
     LitSet* litset = litsets[i];
     litset->vtree  = sdd_manager_lca_of_literals(litset->literal_count,litset->literals,manager);
   }

pysdd/sdd.pyx

@@ -27,13 +27,13 @@ import cython
 import collections
 
 
-IF HAVE_CYSIGNALS:
-    from cysignals.signals cimport sig_on, sig_off
-ELSE:
-    # for non-POSIX systems
-    noop = lambda: None
-    sig_on = noop
-    sig_off = noop
+# IF HAVE_CYSIGNALS:  # IF is deprecated in cython, drop cysignals support for now
+#     from cysignals.signals cimport sig_on, sig_off
+# ELSE:
+# for non-POSIX systems
+noop = lambda: None
+sig_on = noop
+sig_off = noop
 
 
 cdef class SddNode:
@@ -324,7 +324,7 @@ cdef class SddNode:
     def print_ptr(self):
         #cdef long t = <long>self._sddnode
         #print(t)
-        print("{0:x}".format(<unsigned int>&self._sddnode))
+        print("{0:x}".format(<size_t>&self._sddnode))
 
     def save(self, char* filename):
         return self._manager.save(filename, self)

pysdd/sddapi_c.pxd

@@ -9,8 +9,8 @@ pysdd.sddapi_c
 """
 cdef extern from "sddapi.h":
     ctypedef size_t SddSize;  # TODO: only for 64bit
-    ctypedef unsigned int SddNodeSize
-    ctypedef unsigned int SddRefCount
+    ctypedef size_t SddNodeSize
+    ctypedef size_t SddRefCount
     ctypedef unsigned long long SddModelCount
     ctypedef double SddWmc
     ctypedef long SddLiteral

setup.py

@@ -93,7 +93,7 @@ def __init__(self, attrs=None):
 #     compile_time_env['HAVE_CYSIGNALS'] = True
 
 c_args = {
-    'unix': ['-O3'],
+    'unix': ['-O3', '-Wall'],
     'msvc': ['/Ox', '/fp:fast', '/favor:INTEL64', '/Og'],
     'mingw32': ['-O3', '-march=native']
 }