Extending sweeper to handle XORs.

4 files changed, 130 insertions, 0 deletions

diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp
index da6a3add..ad595ab9 100644
--- a/src/sat/glucose/AbcGlucose.cpp
+++ b/src/sat/glucose/AbcGlucose.cpp
@@ -326,6 +326,38 @@ int bmcg_sat_solver_add_and( bmcg_sat_solver * s, int iVar, int iVar0, int iVar1
     return 1;
 }
 
+int bmcg_solver_add_xor( bmcg_sat_solver * pSat, int iVarA, int iVarB, int iVarC, int fCompl )
+{
+    int Lits[3];
+    int Cid;
+    assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );
+
+    Lits[0] = Abc_Var2Lit( iVarA, !fCompl );
+    Lits[1] = Abc_Var2Lit( iVarB, 1 );
+    Lits[2] = Abc_Var2Lit( iVarC, 1 );
+    Cid = bmcg_sat_solver_addclause( pSat, Lits, 3 );
+    assert( Cid );
+
+    Lits[0] = Abc_Var2Lit( iVarA, !fCompl );
+    Lits[1] = Abc_Var2Lit( iVarB, 0 );
+    Lits[2] = Abc_Var2Lit( iVarC, 0 );
+    Cid = bmcg_sat_solver_addclause( pSat, Lits, 3 );
+    assert( Cid );
+
+    Lits[0] = Abc_Var2Lit( iVarA, fCompl );
+    Lits[1] = Abc_Var2Lit( iVarB, 1 );
+    Lits[2] = Abc_Var2Lit( iVarC, 0 );
+    Cid = bmcg_sat_solver_addclause( pSat, Lits, 3 );
+    assert( Cid );
+
+    Lits[0] = Abc_Var2Lit( iVarA, fCompl );
+    Lits[1] = Abc_Var2Lit( iVarB, 0 );
+    Lits[2] = Abc_Var2Lit( iVarC, 1 );
+    Cid = bmcg_sat_solver_addclause( pSat, Lits, 3 );
+    assert( Cid );
+    return 4;
+}
+
 int bmcg_sat_solver_jftr(bmcg_sat_solver* s)
 {
     return ((Gluco::SimpSolver*)s)->jftr;
@@ -633,6 +665,38 @@ int bmcg_sat_solver_add_and( bmcg_sat_solver * s, int iVar, int iVar0, int iVar1
     return 1;
 }
 
+int bmcg_solver_add_xor( bmcg_sat_solver * pSat, int iVarA, int iVarB, int iVarC, int fCompl )
+{
+    int Lits[3];
+    int Cid;
+    assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );
+
+    Lits[0] = Abc_Var2Lit( iVarA, !fCompl );
+    Lits[1] = Abc_Var2Lit( iVarB, 1 );
+    Lits[2] = Abc_Var2Lit( iVarC, 1 );
+    Cid = bmcg_sat_solver_addclause( pSat, Lits, 3 );
+    assert( Cid );
+
+    Lits[0] = Abc_Var2Lit( iVarA, !fCompl );
+    Lits[1] = Abc_Var2Lit( iVarB, 0 );
+    Lits[2] = Abc_Var2Lit( iVarC, 0 );
+    Cid = bmcg_sat_solver_addclause( pSat, Lits, 3 );
+    assert( Cid );
+
+    Lits[0] = Abc_Var2Lit( iVarA, fCompl );
+    Lits[1] = Abc_Var2Lit( iVarB, 1 );
+    Lits[2] = Abc_Var2Lit( iVarC, 0 );
+    Cid = bmcg_sat_solver_addclause( pSat, Lits, 3 );
+    assert( Cid );
+
+    Lits[0] = Abc_Var2Lit( iVarA, fCompl );
+    Lits[1] = Abc_Var2Lit( iVarB, 0 );
+    Lits[2] = Abc_Var2Lit( iVarC, 1 );
+    Cid = bmcg_sat_solver_addclause( pSat, Lits, 3 );
+    assert( Cid );
+    return 4;
+}
+
 int bmcg_sat_solver_jftr(bmcg_sat_solver* s)
 {
     return ((Gluco::Solver*)s)->jftr;
diff --git a/src/sat/glucose/AbcGlucose.h b/src/sat/glucose/AbcGlucose.h
index 02816131..89a3652f 100644
--- a/src/sat/glucose/AbcGlucose.h
+++ b/src/sat/glucose/AbcGlucose.h
@@ -94,6 +94,7 @@ extern int               bmcg_sat_solver_learntnum( bmcg_sat_solver* s );
 extern int               bmcg_sat_solver_conflictnum( bmcg_sat_solver* s );
 extern int               bmcg_sat_solver_minimize_assumptions( bmcg_sat_solver * s, int * plits, int nlits, int pivot );
 extern int               bmcg_sat_solver_add_and( bmcg_sat_solver * s, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl );
+extern int               bmcg_sat_solver_add_xor( bmcg_sat_solver * s, int iVarA, int iVarB, int iVarC, int fCompl );
 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 );
diff --git a/src/sat/glucose2/AbcGlucose2.cpp b/src/sat/glucose2/AbcGlucose2.cpp
index bbb1460a..23c904c8 100644
--- a/src/sat/glucose2/AbcGlucose2.cpp
+++ b/src/sat/glucose2/AbcGlucose2.cpp
@@ -326,6 +326,38 @@ int bmcg2_sat_solver_add_and( bmcg2_sat_solver * s, int iVar, int iVar0, int iVa
     return 1;
 }
 
+int bmcg2_sat_solver_add_xor( bmcg2_sat_solver * pSat, int iVarA, int iVarB, int iVarC, int fCompl )
+{
+    int Lits[3];
+    int Cid;
+    assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );
+
+    Lits[0] = Abc_Var2Lit( iVarA, !fCompl );
+    Lits[1] = Abc_Var2Lit( iVarB, 1 );
+    Lits[2] = Abc_Var2Lit( iVarC, 1 );
+    Cid = bmcg2_sat_solver_addclause( pSat, Lits, 3 );
+    assert( Cid );
+
+    Lits[0] = Abc_Var2Lit( iVarA, !fCompl );
+    Lits[1] = Abc_Var2Lit( iVarB, 0 );
+    Lits[2] = Abc_Var2Lit( iVarC, 0 );
+    Cid = bmcg2_sat_solver_addclause( pSat, Lits, 3 );
+    assert( Cid );
+
+    Lits[0] = Abc_Var2Lit( iVarA, fCompl );
+    Lits[1] = Abc_Var2Lit( iVarB, 1 );
+    Lits[2] = Abc_Var2Lit( iVarC, 0 );
+    Cid = bmcg2_sat_solver_addclause( pSat, Lits, 3 );
+    assert( Cid );
+
+    Lits[0] = Abc_Var2Lit( iVarA, fCompl );
+    Lits[1] = Abc_Var2Lit( iVarB, 0 );
+    Lits[2] = Abc_Var2Lit( iVarC, 1 );
+    Cid = bmcg2_sat_solver_addclause( pSat, Lits, 3 );
+    assert( Cid );
+    return 4;
+}
+
 int bmcg2_sat_solver_jftr(bmcg2_sat_solver* s)
 {
     return ((Gluco2::SimpSolver*)s)->jftr;
@@ -632,6 +664,38 @@ int bmcg2_sat_solver_add_and( bmcg2_sat_solver * s, int iVar, int iVar0, int iVa
     return 1;
 }
 
+int bmcg2_solver_add_xor( bmcg2_sat_solver * pSat, int iVarA, int iVarB, int iVarC, int fCompl )
+{
+    int Lits[3];
+    int Cid;
+    assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );
+
+    Lits[0] = Abc_Var2Lit( iVarA, !fCompl );
+    Lits[1] = Abc_Var2Lit( iVarB, 1 );
+    Lits[2] = Abc_Var2Lit( iVarC, 1 );
+    Cid = bmcg2_sat_solver_addclause( pSat, Lits, 3 );
+    assert( Cid );
+
+    Lits[0] = Abc_Var2Lit( iVarA, !fCompl );
+    Lits[1] = Abc_Var2Lit( iVarB, 0 );
+    Lits[2] = Abc_Var2Lit( iVarC, 0 );
+    Cid = bmcg2_sat_solver_addclause( pSat, Lits, 3 );
+    assert( Cid );
+
+    Lits[0] = Abc_Var2Lit( iVarA, fCompl );
+    Lits[1] = Abc_Var2Lit( iVarB, 1 );
+    Lits[2] = Abc_Var2Lit( iVarC, 0 );
+    Cid = bmcg2_sat_solver_addclause( pSat, Lits, 3 );
+    assert( Cid );
+
+    Lits[0] = Abc_Var2Lit( iVarA, fCompl );
+    Lits[1] = Abc_Var2Lit( iVarB, 0 );
+    Lits[2] = Abc_Var2Lit( iVarC, 1 );
+    Cid = bmcg2_sat_solver_addclause( pSat, Lits, 3 );
+    assert( Cid );
+    return 4;
+}
+
 int bmcg2_sat_solver_jftr(bmcg2_sat_solver* s)
 {
     return ((Gluco2::Solver*)s)->jftr;
diff --git a/src/sat/glucose2/AbcGlucose2.h b/src/sat/glucose2/AbcGlucose2.h
index 28304e52..7c060ccc 100644
--- a/src/sat/glucose2/AbcGlucose2.h
+++ b/src/sat/glucose2/AbcGlucose2.h
@@ -94,6 +94,7 @@ extern int               bmcg2_sat_solver_learntnum( bmcg2_sat_solver* s );
 extern int               bmcg2_sat_solver_conflictnum( bmcg2_sat_solver* s );
 extern int               bmcg2_sat_solver_minimize_assumptions( bmcg2_sat_solver * s, int * plits, int nlits, int pivot );
 extern int               bmcg2_sat_solver_add_and( bmcg2_sat_solver * s, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl );
+extern int               bmcg2_sat_solver_add_xor( bmcg2_sat_solver * s, int iVarA, int iVarB, int iVarC, int fCompl );
 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 );