From 73bb7932f7edad95086d67a795444537c438309e Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sat, 7 Oct 2006 08:01:00 -0700
Subject: Version abc61007

---
 src/base/abci/abcSat.c | 35 ++++++++++++++++++++++++++++++-----
 1 file changed, 30 insertions(+), 5 deletions(-)

(limited to 'src/base/abci/abcSat.c')

diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 3e0d6ba0..8d5dd2a7 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -56,8 +56,8 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
     assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkLatchNum(pNtk) == 0 );
 
-    if ( Abc_NtkPoNum(pNtk) > 1 )
-        fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) );
+//    if ( Abc_NtkPoNum(pNtk) > 1 )
+//        fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) );
 
     // load clauses into the solver
     clk = clock();
@@ -169,6 +169,29 @@ int Abc_NtkClauseTriv( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
     return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
 }
  
+/**Function*************************************************************
+
+  Synopsis    [Adds trivial clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkClauseTop( solver * pSat, Vec_Ptr_t * vNodes, Vec_Int_t * vVars )
+{
+    Abc_Obj_t * pNode;
+    int i;
+//printf( "Adding triv %d.         %d\n", Abc_ObjRegular(pNode)->Id, (int)pSat->solver_stats.clauses );
+    vVars->nSize = 0;
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+        Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->pCopy, Abc_ObjIsComplement(pNode) ) );
+//    Vec_IntPush( vVars, toLitCond( (int)Abc_ObjRegular(pNode)->Id, Abc_ObjIsComplement(pNode) ) );
+    return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+}
+ 
 /**Function*************************************************************
 
   Synopsis    [Adds trivial clause.]
@@ -467,8 +490,8 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
         Vec_PtrPush( vNodes, pNode );
     }
 */
-
     // collect the nodes that need clauses and top-level assignments
+    Vec_PtrClear( vSuper );
     Abc_NtkForEachCo( pNtk, pNode, i )
     {
         // get the fanin
@@ -481,9 +504,11 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
             Vec_PtrPush( vNodes, pFanin );
         }
         // add the trivial clause
-        if ( !Abc_NtkClauseTriv( pSat, Abc_ObjChild0(pNode), vVars ) )
-            goto Quits;
+        Vec_PtrPush( vSuper, Abc_ObjChild0(pNode) );
     }
+    if ( !Abc_NtkClauseTop( pSat, vSuper, vVars ) )
+        goto Quits;
+
 
     // add the clauses
     Vec_PtrForEachEntry( vNodes, pNode, i )
-- 
cgit v1.2.3