From: Hamed <hamed.gorjiara@gmail.com>
Date: Tue, 18 Jul 2017 18:52:43 +0000 (-0700)
Subject: Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/constraint_compiler into... 
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=d3c7acaeed7864d6857eaf5961c649132cd601bd;p=satune.git

Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/constraint_compiler into hamed
Getting updates
---

d3c7acaeed7864d6857eaf5961c649132cd601bd
diff --cc src/Backend/sattranslator.c
index a3245d8,9632fbf..a872b62
--- a/src/Backend/sattranslator.c
+++ b/src/Backend/sattranslator.c
@@@ -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;
  }