diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-12-28 23:04:24 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-12-28 23:04:24 -0800 |
| commit | 7d7ce3ecd03059602f70f26612aabd4a2ec49422 (patch) | |
| tree | b811916386ecfb045cc08f9be78a43a2f0307f30 /src/sat/glucose | |
| parent | c3dccf3020e467da9fa62c9f609bce86b55ccd0a (diff) | |
| download | abc-7d7ce3ecd03059602f70f26612aabd4a2ec49422.tar.gz abc-7d7ce3ecd03059602f70f26612aabd4a2ec49422.tar.bz2 abc-7d7ce3ecd03059602f70f26612aabd4a2ec49422.zip | |
New exact synthesis command 'allexact'.
Diffstat (limited to 'src/sat/glucose')
| -rw-r--r-- | src/sat/glucose/Glucose.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/sat/glucose/Glucose.cpp b/src/sat/glucose/Glucose.cpp index 3ca372a8..0f2d2fce 100644 --- a/src/sat/glucose/Glucose.cpp +++ b/src/sat/glucose/Glucose.cpp @@ -253,6 +253,12 @@ bool Solver::addClause_(vec<Lit>& ps) else if (value(ps[i]) != l_False && ps[i] != p) ps[j++] = p = ps[i]; ps.shrink(i - j); + + if ( 0 ) { + for ( int i = 0; i < ps.size(); i++ ) + printf( "%s%d ", (toInt(ps[i]) & 1) ? "-":"", toInt(ps[i]) >> 1 ); + printf( "\n" ); + } if (flag && (certifiedUNSAT)) { for (i = j = 0, p = lit_Undef; i < ps.size(); i++) |