Adding support of candinality clause to the SAT solver.

1 files changed, 10 insertions, 1 deletions

diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 89391d2d..f1738eb5 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -100,6 +100,9 @@ struct sat_solver_t
     int         hLearnts;      // the first learnt clause
     int         hBinary;       // the special binary clause
     clause *    binary;
+    clause *    cardinality;   // cardinality clause
+    int         nCard;         // cardinality size
+    int         nCardClauses;  // cardinality conflicts
     veci*       wlists;        // watcher lists
     veci        act_clas;      // contain clause activities
 
@@ -291,7 +294,13 @@ static inline int sat_solver_count_usedvars(sat_solver* s)
         }
     return nVars;
 }
-
+static inline void sat_solver_start_cardinality(sat_solver* s, int nSize)
+{
+    assert( s->cardinality == NULL );
+    s->cardinality = (clause*)ABC_CALLOC(int, nSize+2);
+    s->nCard = nSize;
+    s->nCardClauses = 0;
+}
 static inline int sat_solver_add_const( sat_solver * pSat, int iVar, int fCompl )
 {
     lit Lits[1];