Merge remote-tracking branch 'upstream/master' into yosys-experimental

12 files changed, 153 insertions, 23 deletions

diff --git a/src/sat/bsat2/Solver.cpp b/src/sat/bsat2/Solver.cpp
index 451beed8..0f8b415a 100644
--- a/src/sat/bsat2/Solver.cpp
+++ b/src/sat/bsat2/Solver.cpp
@@ -820,7 +820,7 @@ void Solver::toDimacs(FILE* f, Clause& c, vec<Var>& map, Var& max)
 
 void Solver::toDimacs(const char *file, const vec<Lit>& assumps)
 {
-    FILE* f = fopen(file, "wr");
+    FILE* f = fopen(file, "wb");
     if (f == NULL)
         fprintf(stderr, "could not open file %s\n", file), exit(1);
     toDimacs(f, assumps);
diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp
index ad595ab9..9c23e0d0 100644
--- a/src/sat/glucose/AbcGlucose.cpp
+++ b/src/sat/glucose/AbcGlucose.cpp
@@ -818,7 +818,7 @@ void Glucose_ReadDimacs( char * pFileName, SimpSolver& s )
   SeeAlso     []
 
 ***********************************************************************/
-void Glucose_SolveCnf( char * pFileName, Glucose_Pars * pPars )
+void Glucose_SolveCnf( char * pFileName, Glucose_Pars * pPars, int fDumpCnf )
 {
     abctime clk = Abc_Clock();
 
@@ -844,6 +844,15 @@ void Glucose_SolveCnf( char * pFileName, Glucose_Pars * pPars )
         S.eliminate(true);
         printf( "c Simplication removed %d variables and %d clauses.  ", S.eliminated_vars, S.eliminated_clauses );
         Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+
+        if ( fDumpCnf )
+        {
+            char * pFileCnf = Extra_FileNameGenericAppend( pFileName, "_out.cnf" );
+            S.toDimacs(pFileCnf);
+            printf( "Finished dumping CNF after preprocessing into file \"%s\".\n", pFileCnf );
+            printf( "SAT solving is not performed.\n" );
+            return;
+        }
     }
 
     vec<Lit> dummy;
diff --git a/src/sat/glucose/AbcGlucose.h b/src/sat/glucose/AbcGlucose.h
index 89a3652f..c73f9918 100644
--- a/src/sat/glucose/AbcGlucose.h
+++ b/src/sat/glucose/AbcGlucose.h
@@ -105,7 +105,7 @@ extern void              bmcg_sat_solver_start_new_round( bmcg_sat_solver * s );
 extern void              bmcg_sat_solver_mark_cone( bmcg_sat_solver * s, int var );
 
 
-extern void              Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars );
+extern void              Glucose_SolveCnf( char * pFilename, Glucose_Pars * pPars, int fDumpCnf );
 extern int               Glucose_SolveAig( Gia_Man_t * p, Glucose_Pars * pPars );
 
 ABC_NAMESPACE_HEADER_END
diff --git a/src/sat/glucose/AbcGlucoseCmd.cpp b/src/sat/glucose/AbcGlucoseCmd.cpp
index 2e819e49..bb957547 100644
--- a/src/sat/glucose/AbcGlucoseCmd.cpp
+++ b/src/sat/glucose/AbcGlucoseCmd.cpp
@@ -81,10 +81,11 @@ int Abc_CommandGlucose( Abc_Frame_t * pAbc, int argc, char ** argv )
     int pre     = 1;
     int verb    = 0;
     int nConfls = 0;
+    int fDumpCnf = 0;
 
     Glucose_Pars pPars;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Cpvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Cpdvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -102,6 +103,9 @@ int Abc_CommandGlucose( Abc_Frame_t * pAbc, int argc, char ** argv )
             case 'p':
                 pre ^= 1;
                 break;
+            case 'd':
+                fDumpCnf ^= 1;
+                break;
             case 'v':
                 verb ^= 1;
                 break;
@@ -116,7 +120,7 @@ int Abc_CommandGlucose( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( argc == globalUtilOptind + 1 )
     {
-        Glucose_SolveCnf( argv[globalUtilOptind], &pPars );
+        Glucose_SolveCnf( argv[globalUtilOptind], &pPars, fDumpCnf );
         return 0;
     }
 
@@ -132,10 +136,11 @@ int Abc_CommandGlucose( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
     
 usage:
-    Abc_Print( -2, "usage: &glucose [-C num] [-pvh] <file.cnf>\n" );
+    Abc_Print( -2, "usage: &glucose [-C num] [-pdvh] <file.cnf>\n" );
     Abc_Print( -2, "\t             run Glucose 3.0 by Gilles Audemard and Laurent Simon\n" );
     Abc_Print( -2, "\t-C num     : conflict limit [default = %d]\n",  nConfls );
     Abc_Print( -2, "\t-p         : enable preprocessing [default = %d]\n",pre);
+    Abc_Print( -2, "\t-d         : enable dumping CNF after proprocessing [default = %d]\n",fDumpCnf);
     Abc_Print( -2, "\t-v         : verbosity [default = %d]\n",verb);
     Abc_Print( -2, "\t-h         : print the command usage\n");
     Abc_Print( -2, "\t<file.cnf> : (optional) CNF file to solve\n");
diff --git a/src/sat/glucose/Glucose.cpp b/src/sat/glucose/Glucose.cpp
index c975c6ca..cfb388de 100644
--- a/src/sat/glucose/Glucose.cpp
+++ b/src/sat/glucose/Glucose.cpp
@@ -1330,7 +1330,7 @@ void Solver::toDimacs(FILE* f, Clause& c, vec<Var>& map, Var& max)
 
 void Solver::toDimacs(const char *file, const vec<Lit>& assumps)
 {
-    FILE* f = fopen(file, "wr");
+    FILE* f = fopen(file, "wb");
     if (f == NULL)
         fprintf(stderr, "could not open file %s\n", file), exit(1);
     toDimacs(f, assumps);
diff --git a/src/sat/glucose2/AbcGlucose2.cpp b/src/sat/glucose2/AbcGlucose2.cpp
index 9a8b97eb..99ca112a 100644
--- a/src/sat/glucose2/AbcGlucose2.cpp
+++ b/src/sat/glucose2/AbcGlucose2.cpp
@@ -132,6 +132,10 @@ void glucose2_solver_setstop(Gluco2::SimpSolver* S, int * pstop)
     S->pstop = pstop;
 }
 
+void glucose2_markapprox( Gluco2::SimpSolver* S, int v0, int v1, int nlim )
+{
+    S->markApprox(v0, v1, nlim);
+}
 
 /**Function*************************************************************
 
@@ -228,6 +232,11 @@ void bmcg2_sat_solver_set_stop(bmcg2_sat_solver* s, int * pstop)
     glucose2_solver_setstop((Gluco2::SimpSolver*)s, pstop);
 }
 
+void bmcg2_sat_solver_markapprox(bmcg2_sat_solver* s, int v0, int v1, int nlim)
+{
+    glucose2_markapprox((Gluco2::SimpSolver*)s, v0, v1, nlim);
+}
+
 abctime bmcg2_sat_solver_set_runtime_limit(bmcg2_sat_solver* s, abctime Limit)
 {
     abctime nRuntimeLimit = ((Gluco2::SimpSolver*)s)->nRuntimeLimit;
@@ -474,6 +483,11 @@ void glucose2_solver_setstop(Gluco2::Solver* S, int * pstop)
     S->pstop = pstop;
 }
 
+void glucose2_markapprox( Gluco2::Solver* S, int v0, int v1, int nlim )
+{
+    S->markApprox(v0, v1, nlim);
+}
+
 
 /**Function*************************************************************
 
@@ -570,6 +584,11 @@ void bmcg2_sat_solver_set_stop(bmcg2_sat_solver* s, int * pstop)
     glucose2_solver_setstop((Gluco2::Solver*)s, pstop);
 }
 
+void bmcg2_sat_solver_markapprox(bmcg2_sat_solver* s, int v0, int v1, int nlim)
+{
+    glucose2_markapprox((Gluco2::Solver*)s, v0, v1, nlim);
+}
+
 abctime bmcg2_sat_solver_set_runtime_limit(bmcg2_sat_solver* s, abctime Limit)
 {
     abctime nRuntimeLimit = ((Gluco2::Solver*)s)->nRuntimeLimit;
diff --git a/src/sat/glucose2/AbcGlucose2.h b/src/sat/glucose2/AbcGlucose2.h
index 9299d290..d1c15639 100644
--- a/src/sat/glucose2/AbcGlucose2.h
+++ b/src/sat/glucose2/AbcGlucose2.h
@@ -86,6 +86,7 @@ extern int               bmcg2_sat_solver_elim_varnum(bmcg2_sat_solver* s);
 extern int *             bmcg2_sat_solver_read_cex( bmcg2_sat_solver* s );
 extern int               bmcg2_sat_solver_read_cex_varvalue( bmcg2_sat_solver* s, int );
 extern void              bmcg2_sat_solver_set_stop( bmcg2_sat_solver* s, int * pstop );
+extern void              bmcg2_sat_solver_markapprox(bmcg2_sat_solver* s, int v0, int v1, int nlim);
 extern abctime           bmcg2_sat_solver_set_runtime_limit( bmcg2_sat_solver* s, abctime Limit );
 extern void              bmcg2_sat_solver_set_conflict_budget( bmcg2_sat_solver* s, int Limit );
 extern int               bmcg2_sat_solver_varnum( bmcg2_sat_solver* s );
diff --git a/src/sat/glucose2/CGlucoseCore.h b/src/sat/glucose2/CGlucoseCore.h
index c0f96fc4..22de92d2 100644
--- a/src/sat/glucose2/CGlucoseCore.h
+++ b/src/sat/glucose2/CGlucoseCore.h
@@ -613,6 +613,85 @@ inline void Solver::prelocate( int base_var_num ){
 	polarity   .prelocate( base_var_num );
 }
 
+
+inline void Solver::markTill( Var v, int nlim ){
+	if( var2TravId[v] == travId )
+		return;
+
+	vMarked.push(v);
+	
+	if( vMarked.size() >= nlim )
+		return;
+	if( var2TravId[v] == travId-1 || !isTwoFanin(v) )
+		goto finalize;
+
+	markTill( getFaninVar0(v), nlim );
+	markTill( getFaninVar1(v), nlim );
+finalize:
+	var2TravId[v] = travId;
+}
+
+inline void Solver::markApprox( Var v0, Var v1, int nlim ){
+    int i;
+	if( travId <= 1 || nSkipMark>=4 || 0 == nlim )
+		goto finalize;
+
+	vMarked.shrink_( vMarked.size() );
+	travId ++ ; // travId = t+1
+	assert(travId>1);
+
+	markTill(v0, nlim);
+	if( vMarked.size() >= nlim )
+		goto finalize;
+
+	markTill(v1, nlim);
+	if( vMarked.size() >= nlim )
+		goto finalize;
+
+	travId -- ; // travId = t
+	for(i = 0; i < vMarked.size(); i ++){
+		var2TravId  [ vMarked[i] ]      = travId;   // set new nodes to time t 
+		var2NodeData[ vMarked[i] ].sort = 0;
+	}
+	nSkipMark ++ ;
+	return;
+finalize:
+
+	travId ++ ;
+	nSkipMark = 0;
+	markCone(v0);
+	markCone(v1);
+}
+
+inline void Solver::loadJust_rec( Var v ){
+	//assert( value(v) != l_Undef );
+	if( var2TravId[v] == travId || value(v) == l_Undef )
+		return;
+	assert( var2TravId[v] == travId-1 );
+	var2TravId[v] = travId;
+	vMarked.push(v);
+
+	if( !isTwoFanin(v) ){
+		JustModel.push( mkLit( v, value(v) == l_False ) );
+		return;
+	}
+	loadJust_rec( getFaninVar0(v) );
+	loadJust_rec( getFaninVar1(v) );
+}
+inline void Solver::loadJust(){
+    int i;
+	travId ++ ;
+	JustModel.shrink_(JustModel.size());
+	vMarked.shrink_(vMarked.size());
+	JustModel.push(toLit(0));
+	for(i = 0; i < assumptions.size(); i ++)
+		loadJust_rec( var(assumptions[i]) );
+	JustModel[0] = toLit( JustModel.size()-1 );
+	travId -- ;
+	for(i = 0; i < vMarked.size(); i ++)
+		var2TravId[ vMarked[i] ] = travId;
+}
+
 };
 
 ABC_NAMESPACE_IMPL_END
diff --git a/src/sat/glucose2/Glucose2.cpp b/src/sat/glucose2/Glucose2.cpp
index 7a8b265b..d345cd0a 100644
--- a/src/sat/glucose2/Glucose2.cpp
+++ b/src/sat/glucose2/Glucose2.cpp
@@ -186,6 +186,7 @@ Solver::Solver() :
   itpc = ca.alloc(tmp);
   ca[itpc].shrink( ca[itpc].size() );
 
+  nSkipMark = 0;
   #endif
 }
 
@@ -1452,15 +1453,20 @@ printf("c ==================================[ Search Statistics (every %6d confl
     if (status == l_True){
 
         if( justUsage() ){
-            JustModel.shrink_(JustModel.size());
-            assert(jheap.empty());
-            //JustModel.growTo(nVars());
-            int i = 0, j = 0;
-            JustModel.push(toLit(0));
-            for (; i < trail.size(); i++) 
-                if( isRoundWatch(var(trail[i])) && !isTwoFanin(var(trail[i])) )
-                    JustModel.push(trail[i]), j++;
-            JustModel[0] = toLit(j);
+            if( nSkipMark ){
+                loadJust();
+            } else {
+                JustModel.shrink_(JustModel.size());
+                assert(jheap.empty());
+                //JustModel.growTo(nVars());
+                int i = 0, j = 0;
+                JustModel.push(toLit(0));
+                for (; i < trail.size(); i++) 
+                    if( isRoundWatch(var(trail[i])) && !isTwoFanin(var(trail[i])) )
+                        JustModel.push(trail[i]), j++;
+                JustModel[0] = toLit(j);
+            }
+            
         } else {
             // Extend & copy model:
             model.shrink_(model.size());
@@ -1535,7 +1541,7 @@ void Solver::toDimacs(FILE* f, Clause& c, vec<Var>& map, Var& max)
 
 void Solver::toDimacs(const char *file, const vec<Lit>& assumps)
 {
-    FILE* f = fopen(file, "wr");
+    FILE* f = fopen(file, "wb");
     if (f == NULL)
         fprintf(stderr, "could not open file %s\n", file), exit(1);
     toDimacs(f, assumps);
@@ -1743,6 +1749,9 @@ void Solver::reset()
         itpc = ca.alloc(tmp);
         ca[itpc].shrink( ca[itpc].size() );
     }
+
+    vMarked.shrink_( vMarked.size() );
+    nSkipMark = 0;
     #endif
 }
 
diff --git a/src/sat/glucose2/Solver.h b/src/sat/glucose2/Solver.h
index b1d38d79..004fdc95 100644
--- a/src/sat/glucose2/Solver.h
+++ b/src/sat/glucose2/Solver.h
@@ -453,7 +453,15 @@ protected:
     Heap2<JustOrderLt2, JustKey> jheap;
     vec<int> jlevel;
     vec<int> jnext;
+
+    int nSkipMark;
+    void loadJust_rec( Var v );
+    void loadJust();
+    vec<Var> vMarked;
 public:
+    void markTill( Var v0, int nlim );
+    void markApprox( Var v0, Var v1, int nlim );
+
     void prelocate( int var_num );
     void setVarFaninLits( Var v, Lit lit1, Lit lit2 );
     void setVarFaninLits( int v, int lit1, int lit2 ){ setVarFaninLits( Var(v), toLit(lit1), toLit(lit2) ); }
diff --git a/src/sat/msat/msatClause.c b/src/sat/msat/msatClause.c
index 6b1b9e98..3d1fa2fc 100644
--- a/src/sat/msat/msatClause.c
+++ b/src/sat/msat/msatClause.c
@@ -522,7 +522,7 @@ void Msat_ClausePrintSymbols( Msat_Clause_t * pC )
 //        if ( pC->fLearned )
 //            printf( "Act = %.4f  ", Msat_ClauseReadActivity(pC) );
         for ( i = 0; i < (int)pC->nSize; i++ )
-            printf(" "L_LIT, L_lit(pC->pData[i]));
+            printf(" " L_LIT, L_lit(pC->pData[i]));
     }
     printf( "\n" );
 }
diff --git a/src/sat/msat/msatSolverSearch.c b/src/sat/msat/msatSolverSearch.c
index b3190e39..2eda5038 100644
--- a/src/sat/msat/msatSolverSearch.c
+++ b/src/sat/msat/msatSolverSearch.c
@@ -52,7 +52,7 @@ int  Msat_SolverAssume( Msat_Solver_t * p, Msat_Lit_t Lit )
 {
     assert( Msat_QueueReadSize(p->pQueue) == 0 );
     if ( p->fVerbose )
-        printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(Lit));
+        printf(L_IND "assume(" L_LIT ")\n", L_ind, L_lit(Lit));
     Msat_IntVecPush( p->vTrailLim, Msat_IntVecReadSize(p->vTrail) );
 //    assert( Msat_IntVecReadSize(p->vTrailLim) <= Msat_IntVecReadSize(p->vTrail) + 1 );
 //    assert( Msat_IntVecReadSize( p->vTrailLim ) < p->nVars );
@@ -83,7 +83,7 @@ void Msat_SolverUndoOne( Msat_Solver_t * p )
     Msat_OrderVarUnassigned( p->pOrder, Var );
 
     if ( p->fVerbose )
-        printf(L_IND"unbind("L_LIT")\n", L_ind, L_lit(Lit)); 
+        printf(L_IND "unbind(" L_LIT")\n", L_ind, L_lit(Lit)); 
 }
 
 /**Function*************************************************************
@@ -107,7 +107,7 @@ void Msat_SolverCancel( Msat_Solver_t * p )
         {
             Msat_Lit_t Lit;
             Lit = Msat_IntVecReadEntry( p->vTrail, Msat_IntVecReadEntryLast(p->vTrailLim) ); 
-            printf(L_IND"cancel("L_LIT")\n", L_ind, L_lit(Lit));
+            printf(L_IND "cancel(" L_LIT ")\n", L_ind, L_lit(Lit));
         }
     }
     for ( c = Msat_IntVecReadSize(p->vTrail) - Msat_IntVecPop( p->vTrailLim ); c != 0; c-- )
@@ -188,7 +188,7 @@ int  Msat_SolverEnqueue( Msat_Solver_t * p, Msat_Lit_t Lit, Msat_Clause_t * pC )
     if ( p->fVerbose )
     {
 //        printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(Lit));
-        printf(L_IND"bind("L_LIT")  ", L_ind, L_lit(Lit));
+        printf(L_IND "bind(" L_LIT ")  ", L_ind, L_lit(Lit));
         Msat_ClausePrintSymbols( pC );
     }
     p->pAssigns[Var] = Lit;
@@ -513,7 +513,7 @@ void Msat_SolverAnalyze( Msat_Solver_t * p, Msat_Clause_t * pC, Msat_IntVec_t *
         nReasonSize  = Msat_IntVecReadSize( vLits_out );
         pReasonArray = Msat_IntVecReadArray( vLits_out );
         for ( j = 0; j < nReasonSize; j++ ) 
-            printf(" "L_LIT, L_lit(pReasonArray[j]));
+            printf(" " L_LIT, L_lit(pReasonArray[j]));
         printf(" } at level %d\n", *pLevel_out); 
     }
 }