diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-03-02 11:10:16 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-03-02 11:10:16 -0800 |
| commit | 160d1311c9ca687cffe0d9ee6752afdc3f43864c (patch) | |
| tree | 899f438e82aa29a722914162ae7dbcbc5bf7fc09 /src | |
| parent | f419f2e81298df40f90a6ce7d7cdd2e3eaed4918 (diff) | |
| download | abc-160d1311c9ca687cffe0d9ee6752afdc3f43864c.tar.gz abc-160d1311c9ca687cffe0d9ee6752afdc3f43864c.tar.bz2 abc-160d1311c9ca687cffe0d9ee6752afdc3f43864c.zip | |
Adding efficient procedure to minimize the set of assumptions (improved literal reordering).
Diffstat (limited to 'src')
| -rw-r--r-- | src/sat/bsat/satSolver.c | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 47fba5e3..aad0df51 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -2203,8 +2203,15 @@ int sat_solver_minimize_assumptions( sat_solver* s, int * pLits, int nLits, int sat_solver_pop(s); // swap literals assert( nResL <= nLitsL ); +// for ( i = 0; i < nResL; i++ ) +// ABC_SWAP( int, pLits[i], pLits[nLitsL+i] ); + veci_resize( &s->temp_clause, 0 ); + for ( i = 0; i < nLitsL; i++ ) + veci_push( &s->temp_clause, pLits[i] ); for ( i = 0; i < nResL; i++ ) - ABC_SWAP( int, pLits[i], pLits[nLitsL+i] ); + pLits[i] = pLits[nLitsL+i]; + for ( i = 0; i < nLitsL; i++ ) + pLits[nResL+i] = veci_begin(&s->temp_clause)[i]; // assume the right lits for ( i = 0; i < nResL; i++ ) if ( !sat_solver_push(s, pLits[i]) ) |