summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/bsat')
-rw-r--r--src/sat/bsat/satSolver.c23
-rw-r--r--src/sat/bsat/satSolver.h10
-rw-r--r--src/sat/bsat/satUtil.c2
3 files changed, 2 insertions, 33 deletions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 58f2ed21..433f7c5f 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -508,12 +508,6 @@ static inline int sat_solver_enqueue(sat_solver* s, lit l, int from)
s->reasons[v] = from;
s->trail[s->qtail++] = l;
order_assigned(s, v);
- // if cardinality clause is present, add positive literals
- if ( s->cardinality && !lit_sign(l) && s->nCard >= (int)s->cardinality->size )
- {
-//printf( "setting trail[%d] = %d\n", s->qtail-1, l );
- s->cardinality->lits[s->nCard - s->cardinality->size++] = lit_neg(l);
- }
return true;
}
}
@@ -555,13 +549,6 @@ static void sat_solver_canceluntil(sat_solver* s, int level) {
s->reasons[x] = 0;
if ( c < lastLev )
var_set_polar( s, x, !lit_sign(s->trail[c]) );
- // if cardinality clause is present, remove positive
- if ( s->cardinality && s->cardinality->lits[s->nCard+1 - s->cardinality->size] == lit_neg(s->trail[c]) )
- {
-//printf( "undoing trail[%d] = %d\n", c, s->trail[c] );
- assert( s->cardinality->size > 0 );
- s->cardinality->size--;
- }
}
//printf( "\n" );
@@ -795,7 +782,7 @@ static void sat_solver_analyze(sat_solver* s, int h, veci* learnt)
lit p = lit_Undef;
int ind = s->qtail-1;
lit* lits;
- int i, j, minl;// int hTemp = h;
+ int i, j, minl;
veci_push(learnt,lit_Undef);
do{
assert(h != 0);
@@ -810,7 +797,7 @@ static void sat_solver_analyze(sat_solver* s, int h, veci* learnt)
veci_push(learnt,clause_read_lit(h));
}
}else{
- clause* c = h == -2 ? s->cardinality : clause_read(s, h);
+ clause* c = clause_read(s, h);
if (clause_learnt(c))
act_clause_bump(s,c);
@@ -893,8 +880,6 @@ static void sat_solver_analyze(sat_solver* s, int h, veci* learnt)
printf(" } at level %d\n", lev);
}
#endif
-// if ( hTemp == -2 )
-// printf( "%d ", veci_size(learnt) );
}
//#define TEST_CNF_LOAD
@@ -1200,7 +1185,6 @@ void sat_solver_delete(sat_solver* s)
}
sat_solver_store_free(s);
- ABC_FREE(s->cardinality);
ABC_FREE(s);
}
@@ -1641,8 +1625,6 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts)
for (;;){
int hConfl = sat_solver_propagate(s);
- if ( hConfl == 0 && s->cardinality && (int)s->cardinality->size == s->nCard+1 )
- hConfl = -2, s->nCardClauses++;
if (hConfl != 0){
// CONFLICT
int blevel;
@@ -1925,7 +1907,6 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
fflush(stdout);
}
nof_conflicts = (ABC_INT64_T)( 100 * luby(2, restart_iter++) );
-// assert( s->cardinality->size == 0 );
status = sat_solver_search(s, nof_conflicts);
// nof_learnts = nof_learnts * 11 / 10; //*= 1.1;
// quit the loop if reached an external limit
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;
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
index 188c308b..f1f03ce2 100644
--- a/src/sat/bsat/satUtil.c
+++ b/src/sat/bsat/satUtil.c
@@ -195,8 +195,6 @@ void Sat_SolverPrintStats( FILE * pFile, sat_solver * p )
// printf( "calls : %10d (%d)\n", (int)p->nCalls, (int)p->nCalls2 );
printf( "starts : %16.0f\n", Sat_Wrd2Dbl(p->stats.starts) );
printf( "conflicts : %16.0f\n", Sat_Wrd2Dbl(p->stats.conflicts) );
- if ( p->nCardClauses )
- printf( "conflictsCard : %16.0f\n", Sat_Wrd2Dbl((word)p->nCardClauses) );
printf( "decisions : %16.0f\n", Sat_Wrd2Dbl(p->stats.decisions) );
printf( "propagations : %16.0f\n", Sat_Wrd2Dbl(p->stats.propagations) );
// printf( "inspects : %10d\n", (int)p->stats.inspects );