Multi-origin vOrigins with per-node cap

.github/scripts/abcexe.vcxproj

@@ -33,6 +33,7 @@
     <ClCompile>
       <WarningLevel>Level3</WarningLevel>
       <DisableSpecificWarnings>4146;4334;4996;4703;%(DisableSpecificWarnings)</DisableSpecificWarnings>
+      <TreatSpecificWarningsAsErrors>4013</TreatSpecificWarningsAsErrors>
       <FunctionLevelLinking>true</FunctionLevelLinking>
       <IntrinsicFunctions>true</IntrinsicFunctions>
       <SDLCheck>true</SDLCheck>

.github/scripts/abclib.vcxproj.template

@@ -32,6 +32,7 @@
     <ClCompile>
       <WarningLevel>Level3</WarningLevel>
       <DisableSpecificWarnings>4146;4334;4996;4703;%(DisableSpecificWarnings)</DisableSpecificWarnings>
+      <TreatSpecificWarningsAsErrors>4013</TreatSpecificWarningsAsErrors>
       <FunctionLevelLinking>true</FunctionLevelLinking>
       <IntrinsicFunctions>true</IntrinsicFunctions>
       <SDLCheck>true</SDLCheck>

.gitignore

@@ -8,11 +8,14 @@ ReleaseExt/
 
 _/
 _TEST/
+tools/
+temp/
 lib/abc*
 lib/m114*
 lib/bip*
 docs/
 .cache/
+.vscode/
 
 src/ext*
 src/xxx/
@@ -62,4 +65,4 @@ tags
 
 /cmake
 /cscope
-abc.history
+abc.history

Makefile

@@ -37,7 +37,7 @@ MODULES := \
 	src/base/abc src/base/abci src/base/cmd src/base/io src/base/main src/base/exor \
 	src/base/ver src/base/wlc src/base/wln src/base/acb src/base/bac src/base/cba src/base/pla src/base/test \
 	src/map/mapper src/map/mio src/map/super src/map/if src/map/if/acd \
-	src/map/amap src/map/cov src/map/scl src/map/mpm \
+	src/map/amap src/map/cov src/map/scl src/map/mpm src/map/emap \
 	src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/nm \
 	src/misc/vec src/misc/hash src/misc/tim src/misc/bzlib src/misc/zlib \
 	src/misc/mem src/misc/bar src/misc/bbl src/misc/parse src/misc/btor \
@@ -185,32 +185,32 @@ DEP := $(OBJ:.o=.d)
 %.o: %.c
 	@mkdir -p $(dir $@)
 	@echo "$(MSG_PREFIX)\`\` Compiling:" $(LOCAL_PATH)/$<
-	$(VERBOSE)$(CC) -c $(OPTFLAGS) $(INCLUDES) $(CFLAGS) $< -o $@
+	$(VERBOSE)$(CC) -c $(OPTFLAGS) $(INCLUDES) $(CPPFLAGS) $(CFLAGS) $< -o $@
 
 %.o: %.cc
 	@mkdir -p $(dir $@)
 	@echo "$(MSG_PREFIX)\`\` Compiling:" $(LOCAL_PATH)/$<
-	$(VERBOSE)$(CXX) -c $(OPTFLAGS) $(INCLUDES) $(CXXFLAGS) $< -o $@
+	$(VERBOSE)$(CXX) -c $(OPTFLAGS) $(INCLUDES) $(CPPFLAGS) $(CXXFLAGS) $< -o $@
 
 %.o: %.cpp
 	@mkdir -p $(dir $@)
 	@echo "$(MSG_PREFIX)\`\` Compiling:" $(LOCAL_PATH)/$<
-	$(VERBOSE)$(CXX) -c $(OPTFLAGS) $(INCLUDES) $(CXXFLAGS) $< -o $@
+	$(VERBOSE)$(CXX) -c $(OPTFLAGS) $(INCLUDES) $(CPPFLAGS) $(CXXFLAGS) $< -o $@
 
 %.d: %.c
 	@mkdir -p $(dir $@)
 	@echo "$(MSG_PREFIX)\`\` Generating dependency:" $(LOCAL_PATH)/$<
-	$(VERBOSE)$(ABCSRC)/depends.sh "$(CC)" `dirname $*.c` $(OPTFLAGS) $(INCLUDES) $(CFLAGS) $< > $@
+	$(VERBOSE)$(ABCSRC)/depends.sh "$(CC)" `dirname $*.c` $(OPTFLAGS) $(INCLUDES) $(CPPFLAGS) $(CFLAGS) $< > $@
 
 %.d: %.cc
 	@mkdir -p $(dir $@)
 	@echo "$(MSG_PREFIX)\`\` Generating dependency:" $(LOCAL_PATH)/$<
-	$(VERBOSE)$(ABCSRC)/depends.sh "$(CXX)" `dirname $*.cc` $(OPTFLAGS) $(INCLUDES) $(CXXFLAGS) $< > $@
+	$(VERBOSE)$(ABCSRC)/depends.sh "$(CXX)" `dirname $*.cc` $(OPTFLAGS) $(INCLUDES) $(CPPFLAGS) $(CXXFLAGS) $< > $@
 
 %.d: %.cpp
 	@mkdir -p $(dir $@)
 	@echo "$(MSG_PREFIX)\`\` Generating dependency:" $(LOCAL_PATH)/$<
-	$(VERBOSE)$(ABCSRC)/depends.sh "$(CXX)" `dirname $*.cpp` $(OPTFLAGS) $(INCLUDES) $(CXXFLAGS) $< > $@
+	$(VERBOSE)$(ABCSRC)/depends.sh "$(CXX)" `dirname $*.cpp` $(OPTFLAGS) $(INCLUDES) $(CPPFLAGS) $(CXXFLAGS) $< > $@
 
 ifndef ABC_MAKE_NO_DEPS
 -include $(DEP)

src/aig/gia/gia.h

@@ -30,6 +30,7 @@
 #include <stdlib.h>
 #include <string.h>
 #include <assert.h>
+#include <limits.h>
 
 #include "misc/vec/vec.h"
 #include "misc/vec/vecWec.h"
@@ -45,6 +46,35 @@ ABC_NAMESPACE_HEADER_START
 #define GIA_NONE 0x1FFFFFFF
 #define GIA_VOID 0x0FFFFFFF
 
+// Multi-origin tracking: small-buffer optimization with overflow
+#ifndef GIA_ORIGINS_INLINE
+#define GIA_ORIGINS_INLINE 4   // number of inline origin slots (configurable at compile time)
+#endif
+
+typedef union {
+    struct {
+        int origins[GIA_ORIGINS_INLINE];  // -1 = unused slot
+    } inl;
+    struct {
+        int sentinel;    // INT_MIN marks overflow mode
+        int count;       // number of origins in overflow array
+        int * overflow;  // heap-allocated origin array
+    } ovf;
+} Gia_OriginsEntry_t;
+
+#define GIA_ORIGINS_STRIDE   ((int)(sizeof(Gia_OriginsEntry_t) / sizeof(int)))
+#define GIA_ORIGINS_SENTINEL INT_MIN
+
+// Compile-time checks: inline slots must cover the overflow header
+// (sentinel + count + pointer; minimum 4 ints on 64-bit), and must
+// not exceed the hardcoded initial overflow capacity of 8.
+#if GIA_ORIGINS_INLINE < 4
+#  error "GIA_ORIGINS_INLINE must be >= 4 (overflow header needs sentinel+count+ptr, min 4 ints on 64-bit)"
+#endif
+#if GIA_ORIGINS_INLINE > 7
+#  error "GIA_ORIGINS_INLINE must be <= 7 (initial overflow capacity is 8)"
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -190,6 +220,8 @@ struct Gia_Man_t_
     Vec_Int_t *    vIdsOrig;      // original object IDs
     Vec_Int_t *    vIdsEquiv;     // original object IDs proved equivalent
     Vec_Int_t *    vEquLitIds;    // original object IDs proved equivalent
+    Vec_Int_t *    vOrigins;      // per-object origin mapping (from "y" extension)
+    int            nOriginsMax;   // max origins per object (0 = unlimited)
     Vec_Int_t *    vCofVars;      // cofactoring variables
     Vec_Vec_t *    vClockDoms;    // clock domains
     Vec_Flt_t *    vTiming;       // arrival/required/slack
@@ -462,6 +494,78 @@ static inline int          Gia_ManIsConst0Lit( int iLit )      { return (iLit ==
 static inline int          Gia_ManIsConst1Lit( int iLit )      { return (iLit == 1); }
 static inline int          Gia_ManIsConstLit( int iLit )       { return (iLit <= 1); }
 
+// Multi-origin accessors
+static inline Gia_OriginsEntry_t * Gia_ObjOriginsEntry( Gia_Man_t * p, int iObj )
+{
+    return (Gia_OriginsEntry_t *)(Vec_IntArray(p->vOrigins) + iObj * GIA_ORIGINS_STRIDE);
+}
+static inline int Gia_ObjOriginsIsOverflow( Gia_OriginsEntry_t * e )
+{
+    return e->inl.origins[0] == GIA_ORIGINS_SENTINEL;
+}
+static inline int Gia_ObjOriginsNum( Gia_Man_t * p, int iObj )
+{
+    Gia_OriginsEntry_t * e;
+    int k;
+    if ( !p->vOrigins || iObj * GIA_ORIGINS_STRIDE >= Vec_IntSize(p->vOrigins) )
+        return 0;
+    e = Gia_ObjOriginsEntry( p, iObj );
+    if ( Gia_ObjOriginsIsOverflow(e) )
+        return e->ovf.count;
+    for ( k = 0; k < GIA_ORIGINS_INLINE; k++ )
+        if ( e->inl.origins[k] == -1 ) break;
+    return k;
+}
+static inline int Gia_ObjOriginsGet( Gia_Man_t * p, int iObj, int idx )
+{
+    Gia_OriginsEntry_t * e;
+    if ( !p->vOrigins || iObj * GIA_ORIGINS_STRIDE >= Vec_IntSize(p->vOrigins) )
+        return -1;
+    e = Gia_ObjOriginsEntry( p, iObj );
+    if ( Gia_ObjOriginsIsOverflow(e) )
+        return (idx < e->ovf.count) ? e->ovf.overflow[idx] : -1;
+    return (idx < GIA_ORIGINS_INLINE) ? e->inl.origins[idx] : -1;
+}
+// Backward compatible: get first/primary origin
+static inline int Gia_ObjOrigin( Gia_Man_t * p, int iObj )
+{
+    Gia_OriginsEntry_t * e;
+    if ( !p->vOrigins || iObj * GIA_ORIGINS_STRIDE >= Vec_IntSize(p->vOrigins) )
+        return -1;
+    e = Gia_ObjOriginsEntry( p, iObj );
+    if ( Gia_ObjOriginsIsOverflow(e) )
+        return e->ovf.count > 0 ? e->ovf.overflow[0] : -1;
+    return e->inl.origins[0];
+}
+// Set single origin (clears any existing, for initialization)
+static inline void Gia_ObjSetOrigin( Gia_Man_t * p, int iObj, int iOrig )
+{
+    Gia_OriginsEntry_t * e;
+    int k;
+    if ( !p->vOrigins || iObj * GIA_ORIGINS_STRIDE >= Vec_IntSize(p->vOrigins) )
+        return;
+    e = Gia_ObjOriginsEntry( p, iObj );
+    if ( Gia_ObjOriginsIsOverflow(e) && e->ovf.overflow )
+        ABC_FREE( e->ovf.overflow );
+    e->inl.origins[0] = iOrig;
+    for ( k = 1; k < GIA_ORIGINS_INLINE; k++ )
+        e->inl.origins[k] = -1;
+}
+// Grow vOrigins to accommodate object iObj
+static inline void Gia_ManOriginsGrow( Gia_Man_t * p, int iObj )
+{
+    Vec_IntFillExtra( p->vOrigins, (iObj + 1) * GIA_ORIGINS_STRIDE, -1 );
+}
+// Allocate vOrigins for nObjs objects (all entries initialized to -1)
+static inline Vec_Int_t * Gia_ManOriginsAlloc( int nObjs )
+{
+    return Vec_IntStartFull( nObjs * GIA_ORIGINS_STRIDE );
+}
+// Iteration macro (caller must declare int _nOrig before use, or use nOrig variant)
+#define Gia_ObjForEachOrigin( p, iObj, orig, idx ) \
+    for ( idx = 0, _nOrig = Gia_ObjOriginsNum(p, iObj); \
+          (idx < _nOrig) && ((orig = Gia_ObjOriginsGet(p, iObj, idx)), 1); idx++ )
+
 static inline Gia_Obj_t *  Gia_Regular( Gia_Obj_t * p )        { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) & ~01);                           }
 static inline Gia_Obj_t *  Gia_Not( Gia_Obj_t * p )            { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^  01);                           }
 static inline Gia_Obj_t *  Gia_NotCond( Gia_Obj_t * p, int c ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c));                           }
@@ -1312,10 +1416,14 @@ extern void                Cbs_ManStop( Cbs_Man_t * p );
 extern int                 Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj );
 extern int                 Cbs_ManSolve2( Cbs_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
 extern Vec_Int_t *         Cbs_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int f0Proved, int fVerbose );
+extern Vec_Int_t *         Cbs_ManSolveMiterNcOutVals( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int f0Proved, int fVerbose, Vec_Int_t * vOutLits, Vec_Int_t ** pvOutVals );
+extern void                Cbs_ManSyncCore( Cbs_Man_t * p );
+extern Vec_Int_t *         Cbs_ManSolveRoots( Cbs_Man_t * p, Vec_Int_t * vRootLits, Vec_Str_t ** pvStatus, int fVerbose );
 extern void                Cbs_ManSetConflictNum( Cbs_Man_t * p, int Num );
 extern Vec_Int_t *         Cbs_ReadModel( Cbs_Man_t * p );
 /*=== giaCTas.c ============================================================*/
 extern Vec_Int_t *         Tas_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
+extern Vec_Int_t *         Tas_ManSolveMiterNcOutVals( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose, Vec_Int_t * vOutLits, Vec_Int_t ** pvOutVals );
 /*=== giaCof.c =============================================================*/
 extern void                Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes );
 extern Gia_Man_t *         Gia_ManDupCof( Gia_Man_t * p, int iVar );
@@ -1348,6 +1456,15 @@ extern Gia_Man_t *         Gia_ManDupOrderDfsReverse( Gia_Man_t * p, int fRevFan
 extern Gia_Man_t *         Gia_ManDupOutputGroup( Gia_Man_t * p, int iOutStart, int iOutStop );
 extern Gia_Man_t *         Gia_ManDupOutputVec( Gia_Man_t * p, Vec_Int_t * vOutPres );
 extern Gia_Man_t *         Gia_ManDupSelectedOutputs( Gia_Man_t * p, Vec_Int_t * vOutsLeft );
+extern void                Gia_ObjAddOrigin( Gia_Man_t * p, int iObj, int iOrig );
+extern void                Gia_ObjUnionOrigins( Gia_Man_t * p, int iDst, Gia_Man_t * pSrc, int iSrc );
+extern void                Gia_ManOriginsFreeOverflows( Gia_Man_t * p );
+extern void                Gia_ManOriginsReset( Gia_Man_t * p );
+extern void                Gia_ManOriginsDup( Gia_Man_t * pNew, Gia_Man_t * pOld );
+extern void                Gia_ManOriginsDupFill( Gia_Man_t * pNew, Gia_Man_t * pOld );
+extern void                Gia_ManOriginsDupVec( Gia_Man_t * pNew, Gia_Man_t * pOld, Vec_Int_t * vCopies );
+extern void                Gia_ManOriginsAfterRoundTrip( Gia_Man_t * pNew, Gia_Man_t * pOld );
+extern void                Gia_ManOriginsDupIf( Gia_Man_t * pNew, Gia_Man_t * p, void * pIfMan );
 extern Gia_Man_t *         Gia_ManDupOrderAiger( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupLastPis( Gia_Man_t * p, int nLastPis );
 extern Gia_Man_t *         Gia_ManDupFlip( Gia_Man_t * p, int * pInitState );