Experiments with don't-cares.

abcexe.dsp

@@ -88,6 +88,10 @@ LINK32=link.exe
 # PROP Default_Filter "cpp;c;cxx;rc;def;r;odl;idl;hpj;bat"
 # Begin Source File
 
+SOURCE=.\src\base\acb\acbMfs.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\main\main.c
 # End Source File
 # End Group

src/base/acb/acb.h

@@ -91,6 +91,7 @@ struct Acb_Ntk_t_
     Vec_Flt_t       vCounts;    // priority counts
     Vec_Wec_t       vFanouts;   // fanouts
     Vec_Wec_t       vCnfs;      // CNF
+    Vec_Str_t       vCnf;       // CNF
     // other
     Vec_Que_t *     vQue;       // temporary
     Vec_Int_t       vCover;     // temporary
@@ -572,6 +573,7 @@ static inline void Acb_NtkFree( Acb_Ntk_t * p )
     Vec_FltErase( &p->vCounts );    
     Vec_WecErase( &p->vFanouts );
     Vec_WecErase( &p->vCnfs );    
+    Vec_StrErase( &p->vCnf );    
     // other
     Vec_QueFreeP( &p->vQue );
     Vec_IntErase( &p->vCover );    
@@ -970,7 +972,7 @@ extern int         Acb_NtkComputeLevelD( Acb_Ntk_t * p, Vec_Int_t * vTfo );
 extern void        Acb_NtkUpdateLevelD( Acb_Ntk_t * p, int iObj );
 extern void        Acb_NtkUpdateTiming( Acb_Ntk_t * p, int iObj );
 
-extern void        Acb_NtkCreateNode( Acb_Ntk_t * p, word uTruth, Vec_Int_t * vSupp );
+extern int         Acb_NtkCreateNode( Acb_Ntk_t * p, word uTruth, Vec_Int_t * vSupp );
 extern void        Acb_NtkUpdateNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp );
 
 ABC_NAMESPACE_HEADER_END

src/base/acb/acbUtil.c

@@ -300,13 +300,14 @@ void Acb_NtkUpdateTiming( Acb_Ntk_t * p, int iObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Acb_NtkCreateNode( Acb_Ntk_t * p, word uTruth, Vec_Int_t * vSupp )
+int Acb_NtkCreateNode( Acb_Ntk_t * p, word uTruth, Vec_Int_t * vSupp )
 {
     int Pivot = Acb_ObjAlloc( p, ABC_OPER_LUT, Vec_IntSize(vSupp), 0 );
     Acb_ObjSetTruth( p, Pivot, uTruth );
     Acb_ObjAddFanins( p, Pivot, vSupp );
     Acb_ObjAddFaninFanout( p, Pivot );
     Acb_ObjComputeLevelD( p, Pivot );
+    return Pivot;
 }
 void Acb_NtkResetNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp )
 {

src/sat/bsat/satSolver.c

@@ -1334,6 +1334,9 @@ void sat_solver_delete(sat_solver* s)
     veci_delete(&s->temp_clause);
     veci_delete(&s->conf_final);
 
+    veci_delete(&s->user_vars);
+    veci_delete(&s->user_values);
+
     // delete arrays
     if (s->reasons != 0){
         int i;
@@ -1963,6 +1966,13 @@ int sat_solver_solve_internal(sat_solver* s)
         printf("==============================================================================\n");
 
     sat_solver_canceluntil(s,s->root_level);
+    // save variable values
+    if ( status == l_True && s->user_vars.size )
+    {
+        int v;
+        for ( v = 0; v < s->user_vars.size; v++ )
+            veci_push(&s->user_values, sat_solver_var_value(s, s->user_vars.ptr[v]));
+    }
     return status;
 }
 
@@ -2186,6 +2196,7 @@ int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int
         s->nConfLimit = nConfLimit;
         status = sat_solver_solve_internal( s );
         s->nConfLimit = Temp;
+        //printf( "%c", status == l_False ? 'u' : 's' );
         return (int)(status != l_False); // return 1 if the problem is not UNSAT
     }
     assert( nLits >= 2 );

src/sat/bsat/satSolver.h

@@ -193,6 +193,10 @@ struct sat_solver_t
 
     veci        temp_clause;    // temporary storage for a CNF clause
 
+    // assignment storage
+    veci        user_vars;      // variable IDs
+    veci        user_values;    // values of these variables
+
     // CNF loading
     void *      pCnfMan;           // external CNF manager
     int(*pCnfFunc)(void * p, int); // external callback