Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/constraint_compiler into...
authorHamed <hamed.gorjiara@gmail.com>
Tue, 18 Jul 2017 18:52:43 +0000 (11:52 -0700)
committerHamed <hamed.gorjiara@gmail.com>
Tue, 18 Jul 2017 18:52:43 +0000 (11:52 -0700)
Getting updates

1  2 
src/Backend/sattranslator.c

index a3245d85b10a92da0421d49836e0e81133f573a8,9632fbf401405b5ac24116d6d4d6eaee18f2b314..a872b62dd4992a6ca034e7bf68a0b08781a5fd08
@@@ -21,10 -21,16 +21,16 @@@ uint64_t getElementValueBinaryValueSATT
        uint64_t value=0;
        for(int i=elemEnc->numVars-1;i>=0;i--) {
                value=value<<1;
 -              if (This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[i] ) ])
 +              if (getValueSolver(This->satEncoder->cnf->solver, getEdgeVar( elemEnc->variables[i] )) )
                        value |= 1;
        }
+       if (elemEnc->isBinaryValSigned &&
+                       This->satEncoder->cnf->solver->solution[ getEdgeVar( elemEnc->variables[elemEnc->numVars-1])]) {
+               //Do sign extension of negative number
+               uint64_t highbits=0xffffffffffffffff - ((1 << (elemEnc->numVars)) - 1);
+               value+=highbits;
+       }
+       value+=elemEnc->offset;
        return value;
  }