diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2020-11-15 19:02:41 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2020-11-15 19:02:41 -0800 |
| commit | dd07ec57be48b79d07b39d4e5607f4178a32dc1b (patch) | |
| tree | 085b7864a57e9f768b169e6b87f8ad4c1c2a5f3b /src/sat/glucose/AbcGlucose.cpp | |
| parent | 28ea3adedb507ff3766135d27faade20ca1483aa (diff) | |
| download | abc-dd07ec57be48b79d07b39d4e5607f4178a32dc1b.tar.gz abc-dd07ec57be48b79d07b39d4e5607f4178a32dc1b.tar.bz2 abc-dd07ec57be48b79d07b39d4e5607f4178a32dc1b.zip | |
Extending sweeper to handle XORs.
Diffstat (limited to 'src/sat/glucose/AbcGlucose.cpp')
| -rw-r--r-- | src/sat/glucose/AbcGlucose.cpp | 64 |
1 files changed, 64 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; |