From 1f56f20e1bcd7528b526cf6d48776a606edf61fd Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sun, 24 Apr 2022 09:29:52 -0700
Subject: Experiments with SAT sweeping.

---
 src/sat/glucose2/AbcGlucose2.cpp |  6 +++
 src/sat/glucose2/CGlucoseCore.h  | 79 ++++++++++++++++++++++++++++++++++++++++
 src/sat/glucose2/Glucose2.cpp    | 27 +++++++++-----
 src/sat/glucose2/Solver.h        |  8 ++++
 4 files changed, 111 insertions(+), 9 deletions(-)

(limited to 'src/sat/glucose2')

diff --git a/src/sat/glucose2/AbcGlucose2.cpp b/src/sat/glucose2/AbcGlucose2.cpp
index 9a8b97eb..c1d77587 100644
--- a/src/sat/glucose2/AbcGlucose2.cpp
+++ b/src/sat/glucose2/AbcGlucose2.cpp
@@ -1536,6 +1536,12 @@ int Glucose2_SolveAig(Gia_Man_t * p, Glucose2_Pars * pPars)
     return (ret == l_True ? 10 : ret == l_False ? 20 : 0);
 }
 
+extern "C" {
+    void glucose2_markapprox( void * pSat, int v0, int v1, int nlim ){
+        ((Gluco2::Solver*) pSat)->markApprox(v0, v1, nlim);
+    }
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
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 4b4c28e7..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());
@@ -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) ); }
-- 
cgit v1.2.3