Updates to arithmetic verification.

abclib.dsp

@@ -1963,6 +1963,10 @@ SOURCE=.\src\sat\xsat\xsatCnfReader.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\sat\xsat\xsatFloat.h
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\sat\xsat\xsatHeap.h
 # End Source File
 # Begin Source File
@@ -5553,6 +5557,10 @@ SOURCE=.\src\proof\acec\acecTree.c
 
 SOURCE=.\src\proof\acec\acecUtil.c
 # End Source File
+# Begin Source File
+
+SOURCE=.\src\proof\acec\acecXor.c
+# End Source File
 # End Group
 # End Group
 # End Group

src/proof/acec/acecInt.h

@@ -56,6 +56,12 @@ struct Acec_Box_t_
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
+static inline int Acec_SignBit( Vec_Int_t * vAdds, int iBox, int b )  { return (Vec_IntEntry(vAdds, 6*iBox+5) >> b)      & 1; }
+static inline int Acec_SignBit2( Vec_Int_t * vAdds, int iBox, int b ) { return (Vec_IntEntry(vAdds, 6*iBox+5) >> (16+b)) & 1; }
+
+static inline void Acec_SignSetBit( Vec_Int_t * vAdds, int iBox, int b, int v )  { if ( v ) *Vec_IntEntryP(vAdds, 6*iBox+5) |= (1 << b);      }
+static inline void Acec_SignSetBit2( Vec_Int_t * vAdds, int iBox, int b, int v ) { if ( v ) *Vec_IntEntryP(vAdds, 6*iBox+5) |= (1 << (16+b)); }
+
 ////////////////////////////////////////////////////////////////////////
 ///                             ITERATORS                            ///
 ////////////////////////////////////////////////////////////////////////
@@ -75,11 +81,14 @@ extern void          Acec_InsertFadd( Gia_Man_t * pNew, int In[3], int Out[2] );
 extern Gia_Man_t *   Acec_InsertBox( Acec_Box_t * pBox, int fAll );
 /*=== acecTree.c ========================================================*/
 extern void          Acec_PrintAdders( Vec_Wec_t * vBoxes, Vec_Int_t * vAdds );
+extern void          Acec_TreePrintBox( Acec_Box_t * pBox, Vec_Int_t * vAdds );
 extern Acec_Box_t *  Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fFilterIn, int fFilterOut, int fVerbose );
 extern void          Acec_BoxFreeP( Acec_Box_t ** ppBox );
 /*=== acecUtil.c ========================================================*/
 extern void          Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose );
 extern Vec_Int_t *   Gia_PolynCollectLastXor( Gia_Man_t * pGia, int fVerbose );
+/*=== acecUtil.c ========================================================*/
+extern Acec_Box_t *  Acec_DetectXorTrees( Gia_Man_t * p, int fVerbose );
 
 
 

src/proof/acec/acecMult.c

@@ -499,6 +499,7 @@ Vec_Int_t * Acec_MultFindPPs( Gia_Man_t * p )
         {
             if ( Truth == Saved[i] || Truth == ~Saved[i] )
             {
+                //printf( "*** Node %d is PP with support %d.\n", iObj, Vec_IntSize(vSupp) );
                 Acec_MultFindPPs_rec( p, iObj, vBold );
                 nProds++;
                 break;

src/proof/acec/acecTree.c

@@ -27,12 +27,6 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline int Acec_SignBit( Vec_Int_t * vAdds, int iBox, int b )  { return (Vec_IntEntry(vAdds, 6*iBox+5) >> b)      & 1; }
-static inline int Acec_SignBit2( Vec_Int_t * vAdds, int iBox, int b ) { return (Vec_IntEntry(vAdds, 6*iBox+5) >> (16+b)) & 1; }
-
-static inline void Acec_SignSetBit( Vec_Int_t * vAdds, int iBox, int b, int v )  { if ( v ) *Vec_IntEntryP(vAdds, 6*iBox+5) |= (1 << b);      }
-static inline void Acec_SignSetBit2( Vec_Int_t * vAdds, int iBox, int b, int v ) { if ( v ) *Vec_IntEntryP(vAdds, 6*iBox+5) |= (1 << (16+b)); }
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -558,7 +552,7 @@ void Acec_PrintAdders( Vec_Wec_t * vBoxes, Vec_Int_t * vAdds )
         printf( " }\n" );
     }
 }
-void Acec_PrintBox( Acec_Box_t * pBox, Vec_Int_t * vAdds )
+void Acec_TreePrintBox( Acec_Box_t * pBox, Vec_Int_t * vAdds )
 {
     printf( "Adders:\n" );
     Acec_PrintAdders( pBox->vAdds, vAdds );
@@ -703,7 +697,7 @@ void Acec_CreateBoxTest( Gia_Man_t * p )
         printf( "Processing tree %d:  Ranks = %d.  Adders = %d.  Leaves = %d.  Roots = %d.\n", 
             i, Vec_WecSize(pBox->vAdds), Vec_WecSizeSize(pBox->vAdds), 
             Vec_WecSizeSize(pBox->vLeafLits), Vec_WecSizeSize(pBox->vRootLits)  );
-        Acec_PrintBox( pBox, vAdds );
+        Acec_TreePrintBox( pBox, vAdds );
         Acec_BoxFreeP( &pBox );
     }
 
@@ -737,7 +731,7 @@ Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, Vec_Bit_t * vIgnore, int fFilterIn,
             0, Vec_WecSize(pBox->vAdds), Vec_WecSizeSize(pBox->vAdds), 
             Vec_WecSizeSize(pBox->vLeafLits), Vec_WecSizeSize(pBox->vRootLits)  );
     if ( pBox && fVerbose )
-        Acec_PrintBox( pBox, vAdds );
+        Acec_TreePrintBox( pBox, vAdds );
     //Acec_PrintAdders( pBox0->vAdds, vAdds );
     //Acec_MultDetectInputs( p, pBox->vLeafLits, pBox->vRootLits );
     Vec_WecFreeP( &vTrees );

src/proof/acec/module.make

@@ -14,4 +14,5 @@ SRC +=    src/proof/acec/acecCl.c \
     src/proof/acec/acecPolyn.c \
     src/proof/acec/acecSt.c \
     src/proof/acec/acecTree.c \
-    src/proof/acec/acecUtil.c      
+    src/proof/acec/acecUtil.c \
+    src/proof/acec/acecXor.c