Adding and integrating new SAT solver APIs.

6 files changed, 196 insertions, 0 deletions

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: