diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-04-12 11:58:55 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-04-12 11:58:55 -0700 |
commit | 3a553e15ac2f6c035bab1bec32c76ca8830ac4d7 (patch) | |
tree | efec3db04fe9b191572c275573477a287f7da755 /src/sat/bsat/satSolver.h | |
parent | 90cf0b579f2c6e710e82aae2c032301f7cfbcb35 (diff) | |
download | abc-3a553e15ac2f6c035bab1bec32c76ca8830ac4d7.tar.gz abc-3a553e15ac2f6c035bab1bec32c76ca8830ac4d7.tar.bz2 abc-3a553e15ac2f6c035bab1bec32c76ca8830ac4d7.zip |
Removing unused feature of the SAT solver (native support for cardinality constraint).
Diffstat (limited to 'src/sat/bsat/satSolver.h')
-rw-r--r-- | src/sat/bsat/satSolver.h | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index c7e324cd..e19b0b15 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -100,9 +100,6 @@ 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 @@ -294,13 +291,6 @@ 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 void sat_solver_set_polarity(sat_solver* s, int * pVars, int nVars ) { int i; |