Version abc51005

6 files changed, 53 insertions, 8 deletions

diff --git a/src/sat/asat/added.c b/src/sat/asat/added.c
index d7358749..662fe1ff 100644
--- a/src/sat/asat/added.c
+++ b/src/sat/asat/added.c
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: added.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: added.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
 
 ***********************************************************************/
 
@@ -57,7 +57,7 @@ static void Asat_ClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement )
   SeeAlso     []
 
 ***********************************************************************/
-void Asat_SolverWriteDimacs( solver * p, char * pFileName )
+void Asat_SolverWriteDimacs( solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars )
 {
     FILE * pFile;
     void ** pClauses;
@@ -78,18 +78,31 @@ void Asat_SolverWriteDimacs( solver * p, char * pFileName )
     nClauses = p->clauses.size;
     pClauses = p->clauses.ptr;
     for ( i = 0; i < nClauses; i++ )
-        Asat_ClauseWriteDimacs( pFile, pClauses[i], 1 );
+        Asat_ClauseWriteDimacs( pFile, pClauses[i], incrementVars );
 
     // write the learned clauses
     nClauses = p->learnts.size;
     pClauses = p->learnts.ptr;
     for ( i = 0; i < nClauses; i++ )
-        Asat_ClauseWriteDimacs( pFile, pClauses[i], 1 );
+        Asat_ClauseWriteDimacs( pFile, pClauses[i], incrementVars );
 
     // write zero-level assertions
     for ( i = 0; i < p->size; i++ )
         if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
-            fprintf( pFile, "%s%d 0\n", (p->assigns[i] == l_False)? "-": "", i + 1 );
+            fprintf( pFile, "%s%d%s\n",
+                     (p->assigns[i] == l_False)? "-": "",
+                     i + (int)(incrementVars>0),
+                     (incrementVars) ? " 0" : "");
+
+    // write the assumptions
+    if (assumptionsBegin) {
+        for (; assumptionsBegin != assumptionsEnd; assumptionsBegin++) {
+            fprintf( pFile, "%s%d%s\n",
+                     lit_sign(*assumptionsBegin)? "-": "",
+                     lit_var(*assumptionsBegin) + (int)(incrementVars>0),
+                     (incrementVars) ? " 0" : "");
+        }
+    }
 
     fprintf( pFile, "\n" );
     fclose( pFile );
diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c
index d248b115..3927fac3 100644
--- a/src/sat/asat/solver.c
+++ b/src/sat/asat/solver.c
@@ -1099,7 +1099,7 @@ bool solver_solve(solver* s, lit* begin, lit* end, int nSeconds)
         nof_conflicts *= 1.5;
         nof_learnts   *= 1.1;
         // if the runtime limit is exceeded, quit the restart loop
-        if ( clock() - timeStart >= nSeconds * CLOCKS_PER_SEC )
+        if ( (nSeconds >= 0) && (clock() - timeStart >= nSeconds * CLOCKS_PER_SEC) )
             break;
     }
     if (s->verbosity >= 1)
diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h
index 9f80bc7e..b82601c4 100644
--- a/src/sat/asat/solver.h
+++ b/src/sat/asat/solver.h
@@ -73,7 +73,9 @@ extern int     solver_nvars(solver* s);
 extern int     solver_nclauses(solver* s);
 
 // additional procedures
-extern void    Asat_SolverWriteDimacs( solver * pSat, char * pFileName );
+extern void    Asat_SolverWriteDimacs( solver * pSat, char * pFileName,
+                                       lit* assumptionsBegin, lit* assumptionsEnd,
+                                       int incrementVars);
 
 struct stats_t
 {
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index 1f324c4b..a34f3b9a 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -542,7 +542,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
     else if ( mng->mode == 1 ) // resource-aware fraiging
     {
         // transform the target into a fraig
-        pMan = Abc_NtkToFraig( mng->pTarget, &mng->Params, 0 ); 
+        pMan = Abc_NtkToFraig( mng->pTarget, &mng->Params, 0, 0 ); 
         Fraig_ManProveMiter( pMan );
         RetValue = Fraig_ManCheckMiter( pMan );
 
diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h
index 75dfb812..dc679907 100644
--- a/src/sat/fraig/fraig.h
+++ b/src/sat/fraig/fraig.h
@@ -149,6 +149,7 @@ extern void                Fraig_NodeSetChoice( Fraig_Man_t * pMan, Fraig_Node_t
 
 /*=== fraigMan.c =============================================================*/
 extern void                Fraig_ParamsSetDefault( Fraig_Params_t * pParams );
+extern void                Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams );
 extern Fraig_Man_t *       Fraig_ManCreate( Fraig_Params_t * pParams );
 extern void                Fraig_ManFree( Fraig_Man_t * pMan );
 extern void                Fraig_ManPrintStats( Fraig_Man_t * p );
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index aa7e5999..1a34af86 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -60,6 +60,35 @@ void Fraig_ParamsSetDefault( Fraig_Params_t * pParams )
 
 /**Function*************************************************************
 
+  Synopsis    [Sets the default parameters of the package.]
+
+  Description [This set of parameters is tuned for complete FRAIGing.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams )
+{
+    memset( pParams, 0, sizeof(Fraig_Params_t) );
+    pParams->nPatsRand  = FRAIG_PATTERNS_RANDOM;  // the number of words of random simulation info
+    pParams->nPatsDyna  = FRAIG_PATTERNS_DYNAMIC; // the number of words of dynamic simulation info
+    pParams->nBTLimit   = -1;                     // the max number of backtracks to perform
+    pParams->nSeconds   = 20;                     // the max number of seconds to solve the miter
+    pParams->fFuncRed   =  1;                     // performs only one level hashing
+    pParams->fFeedBack  =  1;                     // enables solver feedback
+    pParams->fDist1Pats =  1;                     // enables distance-1 patterns
+    pParams->fDoSparse  =  1;                     // performs equiv tests for sparse functions 
+    pParams->fChoicing  =  0;                     // enables recording structural choices
+    pParams->fTryProve  =  0;                     // tries to solve the final miter
+    pParams->fVerbose   =  0;                     // the verbosiness flag
+    pParams->fVerboseP  =  0;                     // the verbose flag for reporting the proof
+    pParams->fInternal  =  0;                     // the flag indicates the internal run 
+}
+
+/**Function*************************************************************
+
   Synopsis    [Creates the new FRAIG manager.]
 
   Description []