diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-09-16 12:37:27 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-09-16 12:37:27 -0700 |
| commit | f5cb9d6448a9c1d450fd9f578c18b7b51c290fd4 (patch) | |
| tree | e58a94c523187f692d17cbf3d9bb3fcc8fc93dec /src/sat/glucose/Glucose.cpp | |
| parent | adce11979f0c6df2c67fdf71b946f9bbb91cd6dc (diff) | |
| download | abc-f5cb9d6448a9c1d450fd9f578c18b7b51c290fd4.tar.gz abc-f5cb9d6448a9c1d450fd9f578c18b7b51c290fd4.tar.bz2 abc-f5cb9d6448a9c1d450fd9f578c18b7b51c290fd4.zip | |
Bug fix in Glucose integration.
Diffstat (limited to 'src/sat/glucose/Glucose.cpp')
| -rw-r--r-- | src/sat/glucose/Glucose.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/sat/glucose/Glucose.cpp b/src/sat/glucose/Glucose.cpp index 8d520474..2a67d903 100644 --- a/src/sat/glucose/Glucose.cpp +++ b/src/sat/glucose/Glucose.cpp @@ -209,7 +209,7 @@ Var Solver::newVar(bool sign, bool dvar) //activity .push(0); activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0); seen .push(0); - permDiff .push(0); + permDiff .push(0); polarity .push(sign); decision .push(); trail .capacity(v+1); @@ -226,7 +226,7 @@ bool Solver::addClause_(vec<Lit>& ps) if ( 0 ) { for ( int i = 0; i < ps.size(); i++ ) - printf( "%d ", toInt(ps[i]) ); + printf( "%s%d ", (toInt(ps[i]) & 1) ? "-":"", toInt(ps[i]) >> 1 ); printf( "\n" ); } |