Support getting MiniSat's conflict clause

It really just says which assumptions created the conflict when
solveAssuming is used.  And currently we only support one assumption
(which may represent a formula).  If we supported N assumptions, it's
possible MiniSat's analysis would tell us which of the N is the
problem.  It's not clear if it would be a minimal set though.

Still, might as well have the capability at the level of interfacing
with MiniSat in case it comes in handy.

packages/logic-solver/logic.js

@@ -1152,6 +1152,7 @@ Logic.Solver.prototype.solveAssuming = function (formula) {
   // The formula may be used again, however.  (For example, you
   // can solve assuming a formula F, and if it works, require F.)
   this._minisat.retireVar(assumpVar);
+
   return result;
 };
 

packages/logic-solver/minisat_wrapper.js

@@ -72,3 +72,17 @@ MiniSat.prototype.getSolution = function () {
 MiniSat.prototype.retireVar = function (v) {
   this._C._retireVar(v);
 };
+
+MiniSat.prototype.getConflictClause = function () {
+  var C = this._C;
+  var numTerms = C._getConflictClauseSize();
+  var clausePtr = C._getConflictClause();
+  var terms = [];
+  for (var i = 0; i < numTerms; i++) {
+    var t = C.getValue(clausePtr + i*4, 'i32');
+    var v = (t >>> 1) + 1;
+    var s = (t & 1) ? -1 : 1;
+    terms[i] = v * s;
+  }
+  return terms;
+};