Add MSVC build support and install rules to CMake build.

.gitignore

@@ -60,6 +60,5 @@ tags
 
 /arch_flags
 
-/cmake
 /cscope
 abc.history

cmake/abcConfig.cmake.in

@@ -0,0 +1,7 @@
+@PACKAGE_INIT@
+
+include(CMakeFindDependencyMacro)
+
+include("${CMAKE_CURRENT_LIST_DIR}/abcTargets.cmake")
+
+check_required_components(abc)

src/misc/util/abc_global.h

@@ -83,8 +83,11 @@
 #include <string.h>
 
 // catch memory leaks in Visual Studio
+// Note: _CRTDBG_MAP_ALLOC remaps malloc/free/etc. as macros, which collides with
+// C++ class members named the same (e.g. cadical's DeferDeleteArray::free), so
+// only enable it in C TUs.
 #ifdef WIN32
-  #ifdef _DEBUG
+  #if defined(_DEBUG) && !defined(__cplusplus)
     #define _CRTDBG_MAP_ALLOC
     #include <crtdbg.h>
   #endif

src/opt/eslim/utils.hpp

@@ -74,9 +74,9 @@ namespace eSLIM {
       if (tt == 0) {
         return -1;
       }
-      int x = 0;
-      bool status = _BitScanForward64(x, tt);
-      return x;
+      unsigned long x = 0;
+      _BitScanForward64(&x, tt);
+      return (int)x;
     #else
       if (tt == 0) {
         return -1;

src/opt/eslim/windowMan.tpp

@@ -126,7 +126,7 @@ namespace eSLIM {
       std::cout << "PThreads not available, minimize random window.\n";
       std::uniform_int_distribution<> udist(0, windows.size() - 1);
       int wid = udist(rng);
-      eSLIM_Man<SynthesisEngine, SelectionStrategy>::applyeSLIM(windows[wid], cfg, wlogs[wid])
+      eSLIM_Man<SynthesisEngine, SelectionStrategy>::applyeSLIM(windows[wid], cfg, wlogs[wid]);
     #endif
   }
 

src/opt/ufar/UfarPthStub.c

@@ -0,0 +1,33 @@
+// No-op stubs for the subset of pthread functions referenced by UfarPth.cpp.
+// Linked into libabc only when no real pthread implementation is available
+// (currently: MSVC builds, where ABC_USE_PTHREADS is not set).
+// RunConcurrentSolver simply won't do real parallel work in this build.
+
+#include "../../../lib/pthread.h"
+
+int pthread_create(pthread_t * thread, const pthread_attr_t * attr,
+                   void * (*start_routine)(void *), void * arg)
+{
+    (void)thread; (void)attr; (void)start_routine; (void)arg;
+    return -1;
+}
+
+void pthread_exit(void * retval) { (void)retval; }
+
+int pthread_join(pthread_t thread, void ** retval)
+{
+    (void)thread; (void)retval;
+    return 0;
+}
+
+int pthread_mutex_lock(pthread_mutex_t * mutex) { (void)mutex; return 0; }
+int pthread_mutex_unlock(pthread_mutex_t * mutex) { (void)mutex; return 0; }
+
+int pthread_cond_timedwait(pthread_cond_t * cond, pthread_mutex_t * mutex,
+                           const struct timespec * abstime)
+{
+    (void)cond; (void)mutex; (void)abstime;
+    return 0;
+}
+
+int pthread_cond_signal(pthread_cond_t * cond) { (void)cond; return 0; }

src/proof/cec/cecProve.c

@@ -61,8 +61,10 @@ struct Cec_SproveTrace_t_;
 static int Cec_SProveCallback( void * pUser, int fSolved, unsigned Result );
 static Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare, struct Cec_ScorrStop_t_ * pStopOut );
 static Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare, struct Cec_ScorrStop_t_ * pStopOut );
+#ifdef ABC_USE_PTHREADS
 static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int nTimeOut, int nTimeOutU, Wlc_Ntk_t * pWlc, const char * pUfarArgs, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare, int * pEngines, int StageId, int NetId, struct Cec_SproveTrace_t_ * pTrace );
 static void Cec_GiaStopThreads( Par_ThData_t * ThData, pthread_t * WorkerThread, int nWorkers );
+#endif
 static int Cec_GiaWaitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int RetValue, int * pRetEngine );
 
 extern int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId, const char * pArgs );