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 <sarnold@vctlabs.com>

Author: sarnold

.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/abc/abcHieNew.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/base/abci/abcNpn.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/bump.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/colors.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/congruence.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/dense.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