Adding and integrating new SAT solver APIs.

9 files changed, 284 insertions, 32 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 2ed1f5ef..8277a0b3 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -36290,6 +36290,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     Cec_ParFra_t ParsFra, * pPars = &ParsFra; Gia_Man_t * pTemp;
     int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoG2 = 0;
     Cec_ManFraSetDefaultParams( pPars );
+    pPars->jType          =       0;    // solver type
     pPars->fSatSweeping   =       1;    // conflict limit at a node
     pPars->nWords         =       4;    // simulation words
     pPars->nRounds        =     250;    // simulation rounds
@@ -36299,10 +36300,21 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nCallsRecycle  =     500;    // calls to perform before recycling SAT solver
     pPars->nGenIters      =       5;    // pattern generation iterations
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WRILDCPrmdckngxwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCPrmdckngxwvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'J':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-J\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->jType = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->jType < 0 )
+                goto usage;
+            break;
         case 'W':
             if ( globalUtilOptind >= argc )
             {
@@ -36431,8 +36443,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &fraig [-WRILDCP <num>] [-rmdckngwvh]\n" );
+    Abc_Print( -2, "usage: &fraig [-JWRILDCP <num>] [-rmdckngwvh]\n" );
     Abc_Print( -2, "\t         performs combinational SAT sweeping\n" );
+    Abc_Print( -2, "\t-J num : the solver type [default = %d]\n", pPars->jType );
     Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords );
     Abc_Print( -2, "\t-R num : the number of simulation rounds [default = %d]\n", pPars->nRounds );
     Abc_Print( -2, "\t-I num : the number of sweeping iterations [default = %d]\n", pPars->nItersMax );
diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h
index c5c5dbb7..3414842c 100644
--- a/src/proof/cec/cec.h
+++ b/src/proof/cec/cec.h
@@ -95,6 +95,7 @@ struct Cec_ParSmf_t_
 typedef struct Cec_ParFra_t_ Cec_ParFra_t;
 struct Cec_ParFra_t_
 {
+    int              jType;         // solver type
     int              nWords;        // the number of simulation words
     int              nRounds;       // the number of simulation rounds
     int              nItersMax;     // the maximum number of iterations of SAT sweeping
diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c
index 3b942f4f..0b3bf58b 100644
--- a/src/proof/cec/cecSatG2.c
+++ b/src/proof/cec/cecSatG2.c
@@ -28,33 +28,45 @@
 
 #include "sat/glucose2/AbcGlucose2.h"
 
-#define sat_solver                       bmcg2_sat_solver
-#define sat_solver_start                 bmcg2_sat_solver_start
-#define sat_solver_stop                  bmcg2_sat_solver_stop
-#define sat_solver_addclause             bmcg2_sat_solver_addclause
-#define sat_solver_addvar                bmcg2_sat_solver_addvar
-#define sat_solver_read_cex_varvalue     bmcg2_sat_solver_read_cex_varvalue
-#define sat_solver_reset                 bmcg2_sat_solver_reset
-#define sat_solver_set_conflict_budget   bmcg2_sat_solver_set_conflict_budget
-#define sat_solver_conflictnum           bmcg2_sat_solver_conflictnum
-#define sat_solver_solve                 bmcg2_sat_solver_solve
-#define sat_solver_read_cex_varvalue     bmcg2_sat_solver_read_cex_varvalue
+#define sat_solver                         bmcg2_sat_solver
+#define sat_solver_start                   bmcg2_sat_solver_start
+#define sat_solver_stop                    bmcg2_sat_solver_stop
+#define sat_solver_addclause               bmcg2_sat_solver_addclause
+#define sat_solver_addvar                  bmcg2_sat_solver_addvar
+#define sat_solver_read_cex_varvalue       bmcg2_sat_solver_read_cex_varvalue
+#define sat_solver_reset                   bmcg2_sat_solver_reset
+#define sat_solver_set_conflict_budget     bmcg2_sat_solver_set_conflict_budget
+#define sat_solver_conflictnum             bmcg2_sat_solver_conflictnum
+#define sat_solver_solve                   bmcg2_sat_solver_solve
+#define sat_solver_read_cex_varvalue       bmcg2_sat_solver_read_cex_varvalue
+#define sat_solver_read_cex                bmcg2_sat_solver_read_cex
+#define sat_solver_jftr                    bmcg2_sat_solver_jftr
+#define sat_solver_set_jftr                bmcg2_sat_solver_set_jftr
+#define sat_solver_set_var_fanin_lit       bmcg2_sat_solver_set_var_fanin_lit
+#define sat_solver_start_new_round         bmcg2_sat_solver_start_new_round
+#define sat_solver_mark_cone               bmcg2_sat_solver_mark_cone
 
 #else
 
 #include "sat/glucose/AbcGlucose.h"
 
-#define sat_solver                       bmcg_sat_solver
-#define sat_solver_start                 bmcg_sat_solver_start
-#define sat_solver_stop                  bmcg_sat_solver_stop
-#define sat_solver_addclause             bmcg_sat_solver_addclause
-#define sat_solver_addvar                bmcg_sat_solver_addvar
-#define sat_solver_read_cex_varvalue     bmcg_sat_solver_read_cex_varvalue
-#define sat_solver_reset                 bmcg_sat_solver_reset
-#define sat_solver_set_conflict_budget   bmcg_sat_solver_set_conflict_budget
-#define sat_solver_conflictnum           bmcg_sat_solver_conflictnum
-#define sat_solver_solve                 bmcg_sat_solver_solve
-#define sat_solver_read_cex_varvalue     bmcg_sat_solver_read_cex_varvalue
+#define sat_solver                         bmcg_sat_solver
+#define sat_solver_start                   bmcg_sat_solver_start
+#define sat_solver_stop                    bmcg_sat_solver_stop
+#define sat_solver_addclause               bmcg_sat_solver_addclause
+#define sat_solver_addvar                  bmcg_sat_solver_addvar
+#define sat_solver_read_cex_varvalue       bmcg_sat_solver_read_cex_varvalue
+#define sat_solver_reset                   bmcg_sat_solver_reset
+#define sat_solver_set_conflict_budget     bmcg_sat_solver_set_conflict_budget
+#define sat_solver_conflictnum             bmcg_sat_solver_conflictnum
+#define sat_solver_solve                   bmcg_sat_solver_solve
+#define sat_solver_read_cex_varvalue       bmcg_sat_solver_read_cex_varvalue
+#define sat_solver_read_cex                bmcg_sat_solver_read_cex
+#define sat_solver_jftr                    bmcg_sat_solver_jftr
+#define sat_solver_set_jftr                bmcg_sat_solver_set_jftr
+#define sat_solver_set_var_fanin_lit       bmcg_sat_solver_set_var_fanin_lit
+#define sat_solver_start_new_round         bmcg_sat_solver_start_new_round
+#define sat_solver_mark_cone               bmcg_sat_solver_mark_cone
 
 #endif
 
@@ -134,7 +146,8 @@ Cec4_Man_t * Cec4_ManCreate( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
     p->timeStart     = Abc_Clock();
     p->pPars         = pPars;
     p->pAig          = pAig;
-    p->pSat          = sat_solver_start();
+    p->pSat          = sat_solver_start();  
+    sat_solver_set_jftr( p->pSat, pPars->jType );
     p->vFrontier     = Vec_PtrAlloc( 1000 );
     p->vFanins       = Vec_PtrAlloc( 100 );
     p->vCexMin       = Vec_IntAlloc( 100 );
@@ -422,11 +435,19 @@ int Cec4_ObjGetCnfVar( Cec4_Man_t * p, int iObj )
     {
         Cec4_ObjGetCnfVar( p, Gia_ObjFaninId0(pObj, iObj) );
         Cec4_ObjGetCnfVar( p, Gia_ObjFaninId1(pObj, iObj) );
-        Vec_PtrClear( p->vFanins );
-        Vec_PtrPush( p->vFanins, Gia_ObjChild0(pObj) );
-        Vec_PtrPush( p->vFanins, Gia_ObjChild1(pObj) );
         Cec4_ObjSetSatId( p->pNew, pObj, sat_solver_addvar(p->pSat) );
-        Cec4_AddClausesSuper( p->pNew, pObj, p->vFanins, p->pSat );
+        if( sat_solver_jftr( p->pSat ) < 2 )
+        {
+            Vec_PtrClear( p->vFanins );
+            Vec_PtrPush( p->vFanins, Gia_ObjChild0(pObj) );
+            Vec_PtrPush( p->vFanins, Gia_ObjChild1(pObj) );
+            Cec4_AddClausesSuper( p->pNew, pObj, p->vFanins, p->pSat );
+        }
+        if( 0 < sat_solver_jftr( p->pSat ) )
+            sat_solver_set_var_fanin_lit( p->pSat\
+                , Cec4_ObjSatId( p->pNew, pObj )\
+                , Abc_Var2Lit( Cec4_ObjSatId( p->pNew, Gia_ObjFanin0(pObj) ), Gia_ObjFaninC0(pObj) )\
+                , Abc_Var2Lit( Cec4_ObjSatId( p->pNew, Gia_ObjFanin1(pObj) ), Gia_ObjFaninC1(pObj) ) );
         return Cec4_ObjSatId( p->pNew, pObj );
     }
     // start the frontier
@@ -1064,6 +1085,12 @@ int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pf
     clk = Abc_Clock();
     iVar0 = Cec4_ObjGetCnfVar( p, iObj0 );
     iVar1 = Cec4_ObjGetCnfVar( p, iObj1 );
+    if( sat_solver_jftr( p->pSat ) )
+    {
+        sat_solver_start_new_round( p->pSat );
+        sat_solver_mark_cone( p->pSat, Cec4_ObjSatId(p->pNew, Gia_ManObj(p->pNew, iObj0)) );
+        sat_solver_mark_cone( p->pSat, Cec4_ObjSatId(p->pNew, Gia_ManObj(p->pNew, iObj1)) );
+    }
     p->timeCnf += Abc_Clock() - clk;
     // perform solving
     Lits[0] = Abc_Var2Lit(iVar0, 1);
@@ -1135,20 +1162,35 @@ int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pf
 int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr )
 {
     abctime clk = Abc_Clock();
-    int i, IdAig, IdSat, status, fEasy, RetValue = 1;
+    int i, iLit, IdAig, IdSat, status, fEasy, RetValue = 1;
     Gia_Obj_t * pObj = Gia_ManObj( p->pAig, iObj );
     Gia_Obj_t * pRepr = Gia_ManObj( p->pAig, iRepr );
     int fCompl = Abc_LitIsCompl(pObj->Value) ^ Abc_LitIsCompl(pRepr->Value) ^ pObj->fPhase ^ pRepr->fPhase;
     status = Cec4_ManSolveTwo( p, Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value), fCompl, &fEasy, p->pPars->fVerbose );
     if ( status == GLUCOSE_SAT )
     {
+        int * pCex;
         //printf( "Disproved: %d == %d.\n", Abc_Lit2Var(pRepr->Value), Abc_Lit2Var(pObj->Value) );
         p->nSatSat++;
         p->nPatterns++;
         p->pAig->iPatsPi++;
         assert( p->pAig->iPatsPi > 0 && p->pAig->iPatsPi < 64 * p->pAig->nSimWords );
-        Vec_IntForEachEntryDouble( &p->pNew->vCopiesTwo, IdAig, IdSat, i )
-            Cec4_ObjSimSetInputBit( p->pAig, IdAig, sat_solver_read_cex_varvalue(p->pSat, IdSat) );
+        //Vec_IntForEachEntryDouble( &p->pNew->vCopiesTwo, IdAig, IdSat, i )
+        //    Cec4_ObjSimSetInputBit( p->pAig, IdAig, sat_solver_read_cex_varvalue(p->pSat, IdSat) );
+        pCex = sat_solver_read_cex( p->pSat );
+        Vec_IntClear( p->vPat );
+        if ( pCex == NULL )
+        {
+            Vec_IntForEachEntryDouble( &p->pNew->vCopiesTwo, IdAig, IdSat, i )
+                Vec_IntPush( p->vPat, Abc_Var2Lit(IdAig, sat_solver_read_cex_varvalue(p->pSat, IdSat)) );
+        }
+        else
+        {
+            for ( i = 0; i < pCex[0]; )
+                Vec_IntPush( p->vPat, Abc_LitNot(pCex[++i]) );
+        }
+        Vec_IntForEachEntry( p->vPat, iLit, i )
+            Cec4_ObjSimSetInputBit( p->pAig, Abc_Lit2Var(iLit), Abc_LitIsCompl(iLit) );
         if ( fEasy )
             p->timeSatSat0 += Abc_Clock() - clk;
         else
diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp
index f6eada93..da6a3add 100644
--- a/src/sat/glucose/AbcGlucose.cpp
+++ b/src/sat/glucose/AbcGlucose.cpp
@@ -326,6 +326,32 @@ int bmcg_sat_solver_add_and( bmcg_sat_solver * s, int iVar, int iVar0, int iVar1
     return 1;
 }
 
+int bmcg_sat_solver_jftr(bmcg_sat_solver* s)
+{
+    return ((Gluco::SimpSolver*)s)->jftr;
+}
+
+void bmcg_sat_solver_set_jftr(bmcg_sat_solver* s, int jftr)
+{
+    ((Gluco::SimpSolver*)s)->jftr = jftr;
+}
+
+void bmcg_sat_solver_set_var_fanin_lit(bmcg_sat_solver* s, int var, int lit0, int lit1)
+{
+    ((Gluco::SimpSolver*)s)->sat_solver_set_var_fanin_lit(var, lit0, lit1);
+}
+
+void bmcg_sat_solver_start_new_round(bmcg_sat_solver* s)
+{
+    ((Gluco::SimpSolver*)s)->sat_solver_start_new_round();
+}
+
+void bmcg_sat_solver_mark_cone(bmcg_sat_solver* s, int var)
+{
+    ((Gluco::SimpSolver*)s)->sat_solver_mark_cone(var);
+}
+
+
 #else
 
 /**Function*************************************************************
@@ -351,6 +377,11 @@ void glucose_solver_stop(Gluco::Solver* S)
     delete S;
 }
 
+void glucose_solver_reset(Gluco::Solver* S)
+{
+    S->reset();
+}
+
 int glucose_solver_addclause(Gluco::Solver* S, int * plits, int nlits)
 {
     vec<Lit> lits;
@@ -427,6 +458,10 @@ void bmcg_sat_solver_stop(bmcg_sat_solver* s)
 {
     glucose_solver_stop((Gluco::Solver*)s);
 }
+void bmcg_sat_solver_reset(bmcg_sat_solver* s)
+{
+    glucose_solver_reset((Gluco::Solver*)s);
+}
 
 int bmcg_sat_solver_addclause(bmcg_sat_solver* s, int * plits, int nlits)
 {
@@ -575,6 +610,54 @@ int bmcg_sat_solver_minimize_assumptions( bmcg_sat_solver * s, int * plits, int
     return nresL + nresR;
 }
 
+int bmcg_sat_solver_add_and( bmcg_sat_solver * s, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl )
+{
+    int Lits[3];
+
+    Lits[0] = Abc_Var2Lit( iVar, !fCompl );
+    Lits[1] = Abc_Var2Lit( iVar0, fCompl0 );
+    if ( !bmcg_sat_solver_addclause( s, Lits, 2 ) )
+        return 0;
+
+    Lits[0] = Abc_Var2Lit( iVar, !fCompl );
+    Lits[1] = Abc_Var2Lit( iVar1, fCompl1 );
+    if ( !bmcg_sat_solver_addclause( s, Lits, 2 ) )
+        return 0;
+
+    Lits[0] = Abc_Var2Lit( iVar,   fCompl );
+    Lits[1] = Abc_Var2Lit( iVar0, !fCompl0 );
+    Lits[2] = Abc_Var2Lit( iVar1, !fCompl1 );
+    if ( !bmcg_sat_solver_addclause( s, Lits, 3 ) )
+        return 0;
+
+    return 1;
+}
+
+int bmcg_sat_solver_jftr(bmcg_sat_solver* s)
+{
+    return ((Gluco::Solver*)s)->jftr;
+}
+
+void bmcg_sat_solver_set_jftr(bmcg_sat_solver* s, int jftr)
+{
+    ((Gluco::Solver*)s)->jftr = jftr;
+}
+
+void bmcg_sat_solver_set_var_fanin_lit(bmcg_sat_solver* s, int var, int lit0, int lit1)
+{
+    ((Gluco::Solver*)s)->sat_solver_set_var_fanin_lit(var, lit0, lit1);
+}
+
+void bmcg_sat_solver_start_new_round(bmcg_sat_solver* s)
+{
+    ((Gluco::Solver*)s)->sat_solver_start_new_round();
+}
+
+void bmcg_sat_solver_mark_cone(bmcg_sat_solver* s, int var)
+{
+    ((Gluco::Solver*)s)->sat_solver_mark_cone(var);
+}
+
 #endif
 
 
diff --git a/src/sat/glucose/AbcGlucose.h b/src/sat/glucose/AbcGlucose.h
index 026c22ee..02816131 100644
--- a/src/sat/glucose/AbcGlucose.h
+++ b/src/sat/glucose/AbcGlucose.h
@@ -97,6 +97,12 @@ extern int               bmcg_sat_solver_add_and( bmcg_sat_solver * s, int iVar,
 extern int               bmcg_sat_solver_quantify( bmcg_sat_solver * s[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits );
 extern int               bmcg_sat_solver_equiv_overlap_check( bmcg_sat_solver * s, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv );
 extern Vec_Str_t *       bmcg_sat_solver_sop( Gia_Man_t * p, int CubeLimit );
+extern int               bmcg_sat_solver_jftr( bmcg_sat_solver * s );
+extern void              bmcg_sat_solver_set_jftr( bmcg_sat_solver * s, int jftr );
+extern void              bmcg_sat_solver_set_var_fanin_lit( bmcg_sat_solver * s, int var, int lit0, int lit1 );
+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 int               Glucose_SolveAig( Gia_Man_t * p, Glucose_Pars * pPars );
diff --git a/src/sat/glucose/Solver.h b/src/sat/glucose/Solver.h
index 43b13db7..3d7d26ea 100644
--- a/src/sat/glucose/Solver.h
+++ b/src/sat/glucose/Solver.h
@@ -64,6 +64,12 @@ public:
     vec<int> user_vec;
     vec<Lit> user_lits;
 
+    // circuit-based solving
+    int jftr;
+    void sat_solver_set_var_fanin_lit(int, int, int);  
+    void sat_solver_start_new_round();  
+    void sat_solver_mark_cone(int);  
+
     // Problem specification:
     //
     Var     newVar    (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
@@ -457,6 +463,10 @@ inline void     Solver::toDimacs      (const char* file, Lit p, Lit q, Lit r){ v
 
 inline void     Solver::addVar(Var v) { while (v >= nVars()) newVar(); }
 
+inline void     Solver::sat_solver_set_var_fanin_lit(int var, int lit0, int lit1) {}  
+inline void     Solver::sat_solver_start_new_round()  {}  
+inline void     Solver::sat_solver_mark_cone(int var) {}  
+
 //=================================================================================================
 // Debug etc:
 
diff --git a/src/sat/glucose2/AbcGlucose2.cpp b/src/sat/glucose2/AbcGlucose2.cpp
index 1e70a2b2..bbb1460a 100644
--- a/src/sat/glucose2/AbcGlucose2.cpp
+++ b/src/sat/glucose2/AbcGlucose2.cpp
@@ -326,6 +326,31 @@ int bmcg2_sat_solver_add_and( bmcg2_sat_solver * s, int iVar, int iVar0, int iVa
     return 1;
 }
 
+int bmcg2_sat_solver_jftr(bmcg2_sat_solver* s)
+{
+    return ((Gluco2::SimpSolver*)s)->jftr;
+}
+
+void bmcg2_sat_solver_set_jftr(bmcg2_sat_solver* s, int jftr)
+{
+    ((Gluco2::SimpSolver*)s)->jftr = jftr;
+}
+
+void bmcg2_sat_solver_set_var_fanin_lit(bmcg2_sat_solver* s, int var, int lit0, int lit1)
+{
+    ((Gluco2::SimpSolver*)s)->sat_solver_set_var_fanin_lit(var, lit0, lit1);
+}
+
+void bmcg2_sat_solver_start_new_round(bmcg2_sat_solver* s)
+{
+    ((Gluco2::SimpSolver*)s)->sat_solver_start_new_round();
+}
+
+void bmcg2_sat_solver_mark_cone(bmcg2_sat_solver* s, int var)
+{
+    ((Gluco2::SimpSolver*)s)->sat_solver_mark_cone(var);
+}
+
 #else
 
 /**Function*************************************************************
@@ -351,6 +376,11 @@ void glucose2_solver_stop(Gluco2::Solver* S)
     delete S;
 }
 
+void glucose2_solver_reset(Gluco2::Solver* S)
+{
+    S->reset();
+}
+
 int glucose2_solver_addclause(Gluco2::Solver* S, int * plits, int nlits)
 {
     vec<Lit> lits;
@@ -427,6 +457,10 @@ void bmcg2_sat_solver_stop(bmcg2_sat_solver* s)
 {
     glucose2_solver_stop((Gluco2::Solver*)s);
 }
+void bmcg2_sat_solver_reset(bmcg2_sat_solver* s)
+{
+    glucose2_solver_reset((Gluco2::Solver*)s);
+}
 
 int bmcg2_sat_solver_addclause(bmcg2_sat_solver* s, int * plits, int nlits)
 {
@@ -575,6 +609,54 @@ int bmcg2_sat_solver_minimize_assumptions( bmcg2_sat_solver * s, int * plits, in
     return nresL + nresR;
 }
 
+int bmcg2_sat_solver_add_and( bmcg2_sat_solver * s, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl )
+{
+    int Lits[3];
+
+    Lits[0] = Abc_Var2Lit( iVar, !fCompl );
+    Lits[1] = Abc_Var2Lit( iVar0, fCompl0 );
+    if ( !bmcg2_sat_solver_addclause( s, Lits, 2 ) )
+        return 0;
+
+    Lits[0] = Abc_Var2Lit( iVar, !fCompl );
+    Lits[1] = Abc_Var2Lit( iVar1, fCompl1 );
+    if ( !bmcg2_sat_solver_addclause( s, Lits, 2 ) )
+        return 0;
+
+    Lits[0] = Abc_Var2Lit( iVar,   fCompl );
+    Lits[1] = Abc_Var2Lit( iVar0, !fCompl0 );
+    Lits[2] = Abc_Var2Lit( iVar1, !fCompl1 );
+    if ( !bmcg2_sat_solver_addclause( s, Lits, 3 ) )
+        return 0;
+
+    return 1;
+}
+
+int bmcg2_sat_solver_jftr(bmcg2_sat_solver* s)
+{
+    return ((Gluco2::Solver*)s)->jftr;
+}
+
+void bmcg2_sat_solver_set_jftr(bmcg2_sat_solver* s, int jftr)
+{
+    ((Gluco2::Solver*)s)->jftr = jftr;
+}
+
+void bmcg2_sat_solver_set_var_fanin_lit(bmcg2_sat_solver* s, int var, int lit0, int lit1)
+{
+    ((Gluco2::Solver*)s)->sat_solver_set_var_fanin_lit(var, lit0, lit1);
+}
+
+void bmcg2_sat_solver_start_new_round(bmcg2_sat_solver* s)
+{
+    ((Gluco2::Solver*)s)->sat_solver_start_new_round();
+}
+
+void bmcg2_sat_solver_mark_cone(bmcg2_sat_solver* s, int var)
+{
+    ((Gluco2::Solver*)s)->sat_solver_mark_cone(var);
+}
+
 #endif
 
 
diff --git a/src/sat/glucose2/AbcGlucose2.h b/src/sat/glucose2/AbcGlucose2.h
index 8fc774cd..28304e52 100644
--- a/src/sat/glucose2/AbcGlucose2.h
+++ b/src/sat/glucose2/AbcGlucose2.h
@@ -97,6 +97,11 @@ extern int               bmcg2_sat_solver_add_and( bmcg2_sat_solver * s, int iVa
 extern int               bmcg2_sat_solver_quantify( bmcg2_sat_solver * s[], Gia_Man_t * p, int iLit, int fHash, int(*pFuncCiToKeep)(void *, int), void * pData, Vec_Int_t * vDLits );
 extern int               bmcg2_sat_solver_equiv_overlap_check( bmcg2_sat_solver * s, Gia_Man_t * p, int iLit0, int iLit1, int fEquiv );
 extern Vec_Str_t *       bmcg2_sat_solver_sop( Gia_Man_t * p, int CubeLimit );
+extern int               bmcg2_sat_solver_jftr( bmcg2_sat_solver * s );
+extern void              bmcg2_sat_solver_set_jftr( bmcg2_sat_solver * s, int jftr );
+extern void              bmcg2_sat_solver_set_var_fanin_lit( bmcg2_sat_solver * s, int var, int lit0, int lit1 );
+extern void              bmcg2_sat_solver_start_new_round( bmcg2_sat_solver * s );
+extern void              bmcg2_sat_solver_mark_cone( bmcg2_sat_solver * s, int var );
 
 extern void              Glucose2_SolveCnf( char * pFilename, Glucose2_Pars * pPars );
 extern int               Glucose2_SolveAig( Gia_Man_t * p, Glucose2_Pars * pPars );
diff --git a/src/sat/glucose2/Solver.h b/src/sat/glucose2/Solver.h
index 3beb60e0..d71d1be8 100644
--- a/src/sat/glucose2/Solver.h
+++ b/src/sat/glucose2/Solver.h
@@ -64,6 +64,12 @@ public:
     vec<int> user_vec;
     vec<Lit> user_lits;
 
+    // circuit-based solving
+    int jftr;
+    void sat_solver_set_var_fanin_lit(int, int, int);  
+    void sat_solver_start_new_round();  
+    void sat_solver_mark_cone(int);  
+
     // Problem specification:
     //
     Var     newVar    (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
@@ -457,6 +463,10 @@ inline void     Solver::toDimacs      (const char* file, Lit p, Lit q, Lit r){ v
 
 inline void     Solver::addVar(Var v) { while (v >= nVars()) newVar(); }
 
+inline void     Solver::sat_solver_set_var_fanin_lit(int var, int lit0, int lit1) {}  
+inline void     Solver::sat_solver_start_new_round()  {}  
+inline void     Solver::sat_solver_mark_cone(int var) {}  
+
 //=================================================================================================
 // Debug etc: