fix: dev: prep msvc cl and github environment for conda on windows

* disable pthreads when using msvc compiler
* fix build errors on windows, including the following:
  missing symbols, non-const, designated initializers, and
  non-standard explicit type conversions
* uncork sys/stat.h and add missing win32 define for S_ISDIR
* add clang++ flag to get errors on c++20 initializers and set C99 std

Signed-off-by: Stephen L Arnold <[email protected]>

.github/workflows/conda-dev.yml

@@ -34,27 +34,54 @@ jobs:
           - os: 'windows-2019'
             generator: 'Ninja'
             build_type: 'Debug'
-            extra_args: '-DBUILD_SHARED_LIBS=OFF -DABC_USE_NO_READLINE=ON -DVENDOR_GTEST=ON'
+            extra_args: '-DBUILD_SHARED_LIBS=OFF -DABC_USE_NO_PTHREADS=ON -DABC_USE_NO_READLINE=ON -DVENDOR_GTEST=ON'
     env:
       OS: ${{ matrix.os }}
       PY_VER: ${{ matrix.python-version }}
       PYTHONIOENCODING: utf-8
       CMAKE_ARGS: ${{ matrix.use_namespace && '-DABC_USE_NAMESPACE=xxx' || '' }}
 
     steps:
+    #- if: matrix.os == 'windows-2019'
+      #name: Install newer windows compiler
+      #id: install_cc
+      #uses: rlalik/setup-cpp-compiler@master
+      #with:
+        #compiler: g++-11.2.0
+
+    #- if: matrix.os == 'windows-2019'
+      #name: Use compiler
+      #shell: bash -l {0}
+      #env:
+          #CC: ${{ steps.install_cc.outputs.cc }}
+          #CXX: ${{ steps.install_cc.outputs.cxx }}
+      #run: |
+
     - uses: actions/checkout@v4
 
     - name: Setup base python
       uses: actions/setup-python@v5
       with:
         python-version: ${{ matrix.python-version }}
 
+    - name: Prepare build environment for windows
+      if: runner.os == 'Windows'
+      uses: ilammy/msvc-dev-cmd@v1
+      with:
+        arch: x64
+
+    - name: Env (Windows)
+      if: runner.os == 'Windows'
+      run: |
+        echo "CXX=cl.exe" >> $GITHUB_ENV
+        echo "CC=cl.exe" >> $GITHUB_ENV
+
     - name: Cache conda
       id: cache
       uses: actions/cache@v4
       env:
         # Increase this value to reset cache if environment.devenv.yml has not changed
-        CACHE_NUMBER: 1
+        CACHE_NUMBER: 2
       with:
         path: ~/conda_pkgs_dir
         key: ${{ runner.os }}-conda-${{ env.CACHE_NUMBER }}-${{ hashFiles('environment.devenv.yml') }}

CMakeLists.txt

@@ -28,6 +28,8 @@ set(CMAKE_CXX_STANDARD 17)
 set(CMAKE_CXX_STANDARD_REQUIRED ON)
 set(CMAKE_CXX_EXTENSIONS OFF)
 
+set(CMAKE_C_STANDARD 99)
+
 # MSVC has symbols hidden by default. On GCC and Clang we need to explicitly
 # set the visibility to hidden to achieve the same result and then manually
 # expose what we need. This results in smaller abc dynamic library and thus
@@ -160,6 +162,10 @@ if(CMAKE_CXX_COMPILER_ID STREQUAL "GNU" AND NOT (CMAKE_CXX_COMPILER_VERSION VERS
     target_compile_options(abc_interface
         INTERFACE -fno-aggressive-loop-optimizations -Wno-unused-but-set-variable
     )
+elseif(CMAKE_CXX_COMPILER_ID STREQUAL "Clang" OR CMAKE_CXX_COMPILER_ID STREQUAL "AppleClang")
+    target_compile_options(abc_interface
+        INTERFACE -Werror=c99-designator
+    )
 endif()
 
 if(CMAKE_CXX_COMPILER_ID STREQUAL "GNU" OR CMAKE_CXX_COMPILER_ID STREQUAL "Clang" OR CMAKE_CXX_COMPILER_ID STREQUAL "AppleClang")
@@ -182,6 +188,7 @@ elseif(CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
             "_MBCS"
             "_SCL_SECURE_NO_WARNINGS"
             "_CRT_SECURE_NO_WARNINGS"
+            "_CRT_INTERNAL_NONSTDC_NAMES"
             "_XKEYCHECK_H"
             "_ALLOW_KEYWORD_MACROS=1"
     )

Makefile

@@ -71,6 +71,7 @@ ifdef ABC_USE_NAMESPACE
   DLIBS := -lstdc++
   $(info $(MSG_PREFIX)Compiling in namespace $(ABC_NAMESPACE))
 else
+  CFLAGS += -std=gnu99
   CXXFLAGS := $(CFLAGS)
   ABC_USE_LIBSTDCXX := 1
 endif

src/base/abci/abcNpn.c

@@ -340,7 +340,7 @@ void Abc_TruthNpnPerform( Abc_TtStore_t * p, int NpnType, int fVerbose )
 //        typedef unsigned(*TtCanonicizeFunc)(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int flag);
         unsigned Abc_TtCanonicizeWrap(TtCanonicizeFunc func, Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int flag);
         unsigned Abc_TtCanonicizeAda(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int iThres);
-        unsigned Abc_TtCanonicizeCA(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int iThres);
+        extern unsigned Abc_TtCanonicizeCA(Abc_TtHieMan_t * p, word * pTruth, int nVars, char * pCanonPerm, int iThres);
 
 		Abc_TtHieMan_t * pMan = Abc_TtHieManStart(p->nVars, 5);
 		for ( i = 0; i < p->nFuncs; i++ )

src/sat/kissat/bump.c

@@ -85,7 +85,7 @@ static void move_analyzed_variables_to_front_of_queue (kissat *solver) {
   const links *const links = solver->links;
   for (all_stack (unsigned, idx, solver->analyzed)) {
     // clang-format off
-    const datarank rank = { .data = idx, .rank = links[idx].stamp };
+    const datarank rank = { /*.data = */idx, /*.rank = */links[idx].stamp };  // c++20 only
     // clang-format on
     PUSH_STACK (solver->ranks, rank);
   }

src/sat/kissat/colors.c

@@ -1,6 +1,7 @@
 #include "colors.h"
 
 #if defined(WIN32) && !defined(__MINGW32__)
+#include <io.h>
 #define isatty _isatty
 #else
 #include <unistd.h>

src/sat/kissat/congruence.c

@@ -846,7 +846,7 @@ static void add_binary_clause (closure *closure, unsigned a, unsigned b) {
     kissat_new_binary_clause (solver, a, b);
   else {
     kissat_new_unwatched_binary_clause (solver, a, b);
-    litpair litpair = {.lits = {a < b ? a : b, a < b ? b : a}};
+    litpair litpair = {/*.lits = */{a < b ? a : b, a < b ? b : a}};  // c++20 only
     PUSH_STACK (closure->binaries, litpair);
   }
 }
@@ -2500,7 +2500,7 @@ static bool indexed_binary (closure *closure, unsigned lit,
   SWAP (unsigned, lit, other);
   if (lit > other)
     SWAP (unsigned, lit, other);
-  binary_clause binary = {.lits = {lit, other}};
+  binary_clause binary = {/*.lits = */{lit, other}};  // c++20 only
   const unsigned hash = hash_binary (closure, &binary);
   const size_t size = bintab->size;
   const size_t size2 = bintab->size2;
@@ -2986,7 +2986,7 @@ static void index_binary (closure *closure, unsigned lit, unsigned other) {
   KISSAT_assert (lit < other);
   binary_hash_table *bintab = &closure->bintab;
   KISSAT_assert (!binaries_hash_table_is_full (bintab));
-  binary_clause binary = {.lits = {lit, other}};
+  binary_clause binary = {/*.lits = */{lit, other}};  // c++20 only
   const unsigned hash = hash_binary (closure, &binary);
   const size_t size = bintab->size;
   const size_t size2 = bintab->size2;
@@ -3416,10 +3416,10 @@ static void copy_conditional_equivalences (kissat *solver, unsigned lit,
     KISSAT_assert (second != INVALID_LIT);
     litpair pair;
     if (first < second)
-      pair = (litpair){.lits = {first, second}};
+      pair.lits[0] = first, pair.lits[1] = second;
     else {
       KISSAT_assert (second < first);
-      pair = (litpair){.lits = {second, first}};
+      pair.lits[0] = second, pair.lits[1] = first;
     }
     LOG ("literal %s conditional binary clause %s %s", LOGLIT (lit),
          LOGLIT (first), LOGLIT (second));
@@ -3491,13 +3491,13 @@ static void search_condeq (closure *closure, unsigned lit, unsigned pos_lit,
       KISSAT_assert (first < second);
       check_ternary (closure, lit, first, NOT (second));
       check_ternary (closure, lit, NOT (first), second);
-      litpair equivalence = {.lits = {first, second}};
+      litpair equivalence = {/*.lits = */{first, second}};  // c++20 only
       PUSH_STACK (*condeq, equivalence);
       if (NEGATED (second)) {
-        litpair inverse_equivalence = {.lits = {NOT (second), NOT (first)}};
+        litpair inverse_equivalence = {/*.lits = */{NOT (second), NOT (first)}};  // c++20 only
         PUSH_STACK (*condeq, inverse_equivalence);
       } else {
-        litpair inverse_equivalence = {.lits = {second, first}};
+        litpair inverse_equivalence = {/*.lits = */{second, first}};  // c++20 only
         PUSH_STACK (*condeq, inverse_equivalence);
       }
     }
@@ -4549,7 +4549,7 @@ static void forward_subsume_matching_clauses (closure *closure) {
     }
     const reference ref = kissat_reference_clause (solver, c);
     KISSAT_assert (size <= UINT_MAX);
-    refsize refsize = {.ref = ref, .size = (unsigned)size};
+    refsize refsize = {/*.ref = */ref, /*.size = */(unsigned)size};  // c++20 only
     PUSH_STACK (candidates, refsize);
   }
   DEALLOC (matchable, VARS);

src/sat/kissat/dense.c

@@ -60,7 +60,7 @@ static void flush_large_watches (kissat *solver, litpairs *irredundant) {
             if (irredundant) {
               const unsigned other = watch.binary.lit;
               if (lit < other) {
-                const litpair litpair = {.lits = {lit, other}};
+                const litpair litpair = {/*.lits = */{lit, other}};  // c++20 only
                 PUSH_STACK (*irredundant, litpair);
               }
             } else

src/sat/kissat/file.c

@@ -5,14 +5,19 @@
 #include <errno.h>
 #include <stdlib.h>
 #include <string.h>
-#include <sys/stat.h>
+
 #include <sys/types.h>
+#include <sys/stat.h>
 
 #ifdef WIN32
+#include <io.h>
 #define unlink _unlink
 #define access _access
 #define R_OK 4
 #define W_OK 2
+#ifndef S_ISDIR
+#  define S_ISDIR(mode)  (((mode) & _S_IFMT) == _S_IFDIR)
+#endif
 #else
 #include <unistd.h>
 #endif

src/sat/kissat/kitten.c

@@ -1892,7 +1892,7 @@ unsigned kitten_compute_clausal_core (kitten *kitten,
     if (reason_ref == INVALID) {
       LOG ("assumptions mutually inconsistent");
 
-      
+
       //      goto DONE;
   if (learned_ptr)
     *learned_ptr = learned;
@@ -1907,7 +1907,7 @@ unsigned kitten_compute_clausal_core (kitten *kitten,
 
   return original;
 
-  
+
     }
   }
 
@@ -2412,7 +2412,7 @@ static inline void print_lit (line *line, int lit) {
 
 static void print_witness (kitten *kitten, int max_var) {
   KISSAT_assert (max_var >= 0);
-  line line = {.size = 0};
+  line line = {/*.size = */0};  // c++20 only
   const size_t parsed_lits = 2 * (size_t) max_var;
   for (size_t ulit = 0; ulit < parsed_lits; ulit += 2) {
     const value sign = kitten_value (kitten, ulit);

src/sat/kissat/proplit.h

@@ -8,7 +8,7 @@ static inline void kissat_watch_large_delayed (kissat *solver,
   while (d != end_delayed) {
     const unsigned lit = *d++;
     KISSAT_assert (d != end_delayed);
-    const watch watch = {.raw = *d++};
+    const watch watch = {/*.raw =*/ *d++};  // c++20 only
     KISSAT_assert (!watch.type.binary);
     KISSAT_assert (lit < LITS);
     watches *const lit_watches = all_watches + lit;

src/sat/kissat/sweep.c

@@ -877,8 +877,8 @@ static void substitute_connected_clauses (sweeper *sweeper, unsigned lit,
         REMOVE_CHECKER_BINARY (lit, other);
         DELETE_BINARY_FROM_PROOF (lit, other);
         PUSH_STACK (*delayed, head.raw);
-        watch src = {.raw = head.raw};
-        watch dst = {.raw = head.raw};
+        watch src = {/*.raw = */head.raw};  // c++20 only
+        watch dst = {/*.raw = */head.raw};  // c++20 only
         src.binary.lit = lit;
         dst.binary.lit = repr;
         watches *other_watches = &WATCHES (other);
@@ -970,7 +970,7 @@ static void substitute_connected_clauses (sweeper *sweeper, unsigned lit,
                   LOGLIT (second));
           KISSAT_assert (first == repr || second == repr);
           const unsigned other = first ^ second ^ repr;
-          const watch src = {.raw = head.raw};
+          const watch src = {/*.raw = */head.raw};  // c++20 only
           watch dst = kissat_binary_watch (repr);
           watches *other_watches = &WATCHES (other);
           kissat_substitute_large_watch (solver, other_watches, src, dst);
@@ -1029,7 +1029,7 @@ static void substitute_connected_clauses (sweeper *sweeper, unsigned lit,
     const unsigned *const begin_delayed = BEGIN_STACK (*delayed);
     const unsigned *const end_delayed = END_STACK (*delayed);
     for (const unsigned *p = begin_delayed; p != end_delayed; p++) {
-      const watch head = {.raw = *p};
+      const watch head = {/*.raw = */*p};  // c++20 only
       watches *repr_watches = &WATCHES (repr);
       PUSH_WATCHES (*repr_watches, head);
     }

src/sat/kissat/walk.c

@@ -28,7 +28,7 @@ struct tagged {
 
 static inline tagged make_tagged (bool binary, unsigned ref) {
   KISSAT_assert (ref <= MAX_WALK_REF);
-  tagged res = {.ref = ref, .binary = binary};
+  tagged res = {/*.ref = */ref, /*.binary = */binary};  // c++20 only
   return res;
 }
 

src/sat/kissat/watch.c

@@ -36,7 +36,7 @@ void kissat_remove_binary_watch (kissat *solver, watches *watches,
   KISSAT_assert (begin + 1 <= end);
   watches->end -= 1;
 #endif
-  const watch empty = {.raw = INVALID_VECTOR_ELEMENT};
+  const watch empty = {/*.raw = */INVALID_VECTOR_ELEMENT};  // c++20 only
   end[-1] = empty;
   KISSAT_assert (solver->vectors.usable < MAX_SECTOR - 1);
   solver->vectors.usable += 1;
@@ -73,7 +73,7 @@ void kissat_remove_blocking_watch (kissat *solver, watches *watches,
   KISSAT_assert (begin + 2 <= end);
   watches->end -= 2;
 #endif
-  const watch empty = {.raw = INVALID_VECTOR_ELEMENT};
+  const watch empty = {/*.raw = */INVALID_VECTOR_ELEMENT};  // c++20 only
   end[-2] = end[-1] = empty;
   KISSAT_assert (solver->vectors.usable < MAX_SECTOR - 2);
   solver->vectors.usable += 2;