summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat/satSolver.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/bsat/satSolver.h')
-rw-r--r--src/sat/bsat/satSolver.h10
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;