Updates to arithmetic verification.

3 files changed, 65 insertions, 2 deletions

diff --git a/src/aig/gia/giaTruth.c b/src/aig/gia/giaTruth.c
index f636a573..ab5f569e 100644
--- a/src/aig/gia/giaTruth.c
+++ b/src/aig/gia/giaTruth.c
@@ -184,6 +184,8 @@ word Gia_ObjComputeTruth6Cis( Gia_Man_t * p, int iLit, Vec_Int_t * vSupp, Vec_Wr
     if ( !iObj ) return Abc_LitIsCompl(iLit) ? ~(word)0 : (word)0;
     Gia_ManIncrementTravId( p );
     Gia_ObjComputeTruth6CisSupport_rec( p, iObj, vSupp );
+    if ( Vec_IntSize(vSupp) > 6 )
+        return 0;
     Gia_ObjComputeTruth6( p, iObj, vSupp, vTemp );
     return Abc_LitIsCompl(iLit) ? ~Vec_WrdEntry(vTemp, iObj) : Vec_WrdEntry(vTemp, iObj);
 }
diff --git a/src/proof/acec/acecMult.c b/src/proof/acec/acecMult.c
index 397f6d57..33c32144 100644
--- a/src/proof/acec/acecMult.c
+++ b/src/proof/acec/acecMult.c
@@ -389,7 +389,7 @@ Vec_Int_t * Acec_MultDetectInputs( Gia_Man_t * p, Vec_Wec_t * vLeafLits, Vec_Wec
         Vec_IntForEachEntry( vLevel, iLit, k )
         {
             word Truth = Gia_ObjComputeTruth6Cis( p, iLit, vSupp, vTemp );
-            if ( Vec_IntSize(vSupp) >= 4 )
+            if ( Vec_IntSize(vSupp) >= 0 )
             {
                 printf( "Leaf = %4d : ", Abc_Lit2Var(iLit) );
                 printf( "Rank = %2d  ", i );
diff --git a/src/proof/acec/acecTree.c b/src/proof/acec/acecTree.c
index 53e1cb60..8be8a340 100644
--- a/src/proof/acec/acecTree.c
+++ b/src/proof/acec/acecTree.c
@@ -63,6 +63,65 @@ void Acec_BoxFreeP( Acec_Box_t ** ppBox )
 
 /**Function*************************************************************
 
+  Synopsis    [Filters trees by removing TFO of roots.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Acec_TreeFilterOne( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vTree )
+{
+    Vec_Bit_t * vIsRoot = Vec_BitStart( Gia_ManObjNum(p) );
+    Vec_Bit_t * vMarked = Vec_BitStart( Gia_ManObjNum(p) ) ;
+    Gia_Obj_t * pObj;
+    int i, k = 0, Box, Rank;
+    // mark roots
+    Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
+    {
+        Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+3), 1 );
+        Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+4), 1 );
+    }
+    Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
+    {
+        Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+0), 0 );
+        Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+1), 0 );
+        Vec_BitWriteEntry( vIsRoot, Vec_IntEntry(vAdds, 6*Box+2), 0 );
+    }
+    // iterate through nodes to detect TFO of roots
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( Vec_BitEntry(vIsRoot, Gia_ObjFaninId0(pObj,i)) || Vec_BitEntry(vIsRoot, Gia_ObjFaninId1(pObj,i)) ||
+             Vec_BitEntry(vMarked, Gia_ObjFaninId0(pObj,i)) || Vec_BitEntry(vMarked, Gia_ObjFaninId1(pObj,i)) )
+            Vec_BitWriteEntry( vMarked, i, 1 );
+    }
+    // remove those that overlap with roots
+    Vec_IntForEachEntryDouble( vTree, Box, Rank, i )
+    {
+        if ( Vec_BitEntry(vMarked, Vec_IntEntry(vAdds, 6*Box+3)) || Vec_BitEntry(vMarked, Vec_IntEntry(vAdds, 6*Box+4)) )
+        {
+            printf( "Removing box %d=(%d,%d) of rank %d.\n", Box, Vec_IntEntry(vAdds, 6*Box+3), Vec_IntEntry(vAdds, 6*Box+4), Rank ); 
+            continue;
+        }
+        Vec_IntWriteEntry( vTree, k++, Box );
+        Vec_IntWriteEntry( vTree, k++, Rank );
+    }
+    Vec_IntShrink( vTree, k );
+    Vec_BitFree( vIsRoot );
+    Vec_BitFree( vMarked );
+}
+void Acec_TreeFilterTrees( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Wec_t * vTrees )
+{
+    Vec_Int_t * vLevel;
+    int i;
+    Vec_WecForEachLevel( vTrees, vLevel, i )
+        Acec_TreeFilterOne( p, vAdds, vLevel );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Find internal cut points with exactly one adder fanin/fanout.]
 
   Description [Returns a map of point into its input/output adder.]
@@ -163,6 +222,8 @@ Vec_Wec_t * Acec_TreeFindTrees( Gia_Man_t * p, Vec_Int_t * vAdds )
     }
     Vec_BitFree( vFound );
     Vec_IntFree( vMap );
+    // filter trees
+    Acec_TreeFilterTrees( p, vAdds, vTrees );
     // sort by size
     Vec_WecSort( vTrees, 1 );
     return vTrees;
@@ -580,7 +641,7 @@ Acec_Box_t * Acec_DeriveBox( Gia_Man_t * p, int fVerbose )
             Vec_WecSizeSize(pBox->vLeafLits), Vec_WecSizeSize(pBox->vRootLits)  );
     if ( pBox && fVerbose )
         Acec_PrintBox( pBox, vAdds );
-//    Acec_MultDetectInputs( p, pBox->vLeafLits, pBox->vRootLits );
+    //Acec_MultDetectInputs( p, pBox->vLeafLits, pBox->vRootLits );
     Vec_WecFreeP( &vTrees );
     Vec_IntFree( vAdds );
     return pBox;