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

5 files changed, 126 insertions, 10 deletions

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) ); }