diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-08-02 00:29:57 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-08-02 00:29:57 -0700 |
| commit | 8822e811caa23a6e33818d9337aa25c5e96bea73 (patch) | |
| tree | cf3337b005c477b5a4e7b4075b62917355dab6d8 /src/sat/bsat | |
| parent | 68c70bcb8ecab9b419adf18c976a22da69062b1d (diff) | |
| download | abc-8822e811caa23a6e33818d9337aa25c5e96bea73.tar.gz abc-8822e811caa23a6e33818d9337aa25c5e96bea73.tar.bz2 abc-8822e811caa23a6e33818d9337aa25c5e96bea73.zip | |
Scalable gate-level abstraction.
Diffstat (limited to 'src/sat/bsat')
| -rw-r--r-- | src/sat/bsat/satSolver2.c | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 47c7b72f..dfe01a23 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -1289,6 +1289,18 @@ int sat_solver2_addclause(sat_solver2* s, lit* begin, lit* end, int Id) } sat_solver2_setnvars(s,maxvar+1); + + // delete duplicates + for (i = j = begin + 1; i < end; i++) + { + if ( *(i-1) == lit_neg(*i) ) // tautology + return clause2_create_new( s, begin, end, 0, 0 ); // add it anyway, to preserve proper clause count + if ( *(i-1) != *i ) + *j++ = *i; + } + end = j; + assert( begin < end ); + // coount the number of 0-literals count = 0; for ( i = begin; i < end; i++ ) |