Adding and integrating new SAT solver APIs.

1 files changed, 83 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