From dd07ec57be48b79d07b39d4e5607f4178a32dc1b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 15 Nov 2020 19:02:41 -0800 Subject: Extending sweeper to handle XORs. --- src/sat/glucose2/AbcGlucose2.cpp | 64 ++++++++++++++++++++++++++++++++++++++++ src/sat/glucose2/AbcGlucose2.h | 1 + 2 files changed, 65 insertions(+) (limited to 'src/sat/glucose2') 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 ); -- cgit v1.2.3