Version abc60222

2 files changed, 27 insertions, 12 deletions

diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index d286ea9c..2129bfb0 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -37,16 +37,15 @@ struct ABC_ManagerStruct_t
     char *                pDumpFileName; // the name of the file to dump the target network
     Extra_MmFlex_t *      pMmNames;      // memory manager for signal names
     // solving parameters
-    int                   mode;          // 0 = brute-force SAT;  1 = resource-aware FRAIG
+    int                   mode;          // 0 = resource-aware integration; 1 = brute-force SAT
     int                   nConfLimit;    // time limit for pure SAT solving
     int                   nImpLimit;     // time limit for pure SAT solving
-//    Fraig_Params_t        Params;        // the set of parameters to call FRAIG package
     // information about the target 
     int                   nog;           // the numbers of gates in the target
     Vec_Ptr_t *           vNodes;        // the gates in the target
     Vec_Int_t *           vValues;       // the values of gate's outputs in the target
     // solution
-    CSAT_Target_ResultT *  pResult;       // the result of solving the target
+    CSAT_Target_ResultT * pResult;       // the result of solving the target
 };
 
 static CSAT_Target_ResultT * ABC_TargetResAlloc( int nVars );
@@ -89,6 +88,7 @@ ABC_Manager ABC_InitManager()
     mng->vValues    = Vec_IntAlloc( 100 );
     mng->nConfLimit = ABC_DEFAULT_CONF_LIMIT;
     mng->nImpLimit  = ABC_DEFAULT_IMP_LIMIT;
+    mng->mode       = 0; // set "resource-aware integration" as the default mode
     return mng;
 }
 
@@ -121,7 +121,7 @@ void ABC_ReleaseManager( ABC_Manager mng )
 
   Synopsis    [Sets solver options for learning.]
 
-  Description [0 = brute-force SAT;  1 = resource-aware FRAIG.]
+  Description []
                
   SideEffects []
 
@@ -130,15 +130,23 @@ void ABC_ReleaseManager( ABC_Manager mng )
 ***********************************************************************/
 void ABC_SetSolveOption( ABC_Manager mng, enum CSAT_OptionT option )
 {
-    mng->mode = option;
-    if ( option == 0 )
-        printf( "ABC_SetSolveOption: Setting brute-force SAT mode.\n" );
-    else if ( option == 1 )
-        printf( "ABC_SetSolveOption: Setting resource-aware FRAIG mode.\n" );
-    else
-        printf( "ABC_SetSolveOption: Unknown solving mode.\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Sets solving mode by brute-force SAT.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void ABC_UseOnlyCoreSatSolver( ABC_Manager mng )
+{
+    mng->mode = 1;  // switch to "brute-force SAT" as the solving option
+}
 
 /**Function*************************************************************
 
@@ -535,7 +543,10 @@ enum CSAT_StatusT ABC_Solve( ABC_Manager mng )
         { printf( "ABC_Solve: Target network is not derived by ABC_SolveInit().\n" ); return UNDETERMINED; }
 
     // try to prove the miter using a number of techniques
-    RetValue = Abc_NtkMiterProve( &mng->pTarget, mng->nConfLimit, mng->nImpLimit, 1, 1, 0 );
+    if ( mng->mode )
+        RetValue = Abc_NtkMiterSat( mng->pTarget, mng->nConfLimit, mng->nImpLimit, 0 );
+    else
+        RetValue = Abc_NtkMiterProve( &mng->pTarget, mng->nConfLimit, mng->nImpLimit, 1, 1, 0 );
 
     // analyze the result
     mng->pResult = ABC_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) );
diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h
index faba9ee4..e187845c 100644
--- a/src/sat/csat/csat_apis.h
+++ b/src/sat/csat/csat_apis.h
@@ -150,6 +150,10 @@ extern void ABC_ReleaseManager(ABC_Manager mng);
 // set solver options for learning
 extern void                  ABC_SetSolveOption(ABC_Manager mng, enum CSAT_OptionT option);
 
+// enable checking by brute-force SAT solver (MiniSat-1.14)
+extern void                  ABC_UseOnlyCoreSatSolver(ABC_Manager mng);
+
+
 // add a gate to the circuit
 // the meaning of the parameters are:
 // type: the type of the gate to be added