From a8a7902ad2275cae61124247e8aa19359a4704a3 Mon Sep 17 00:00:00 2001
From: David Greenspan <dgreenspan@alum.mit.edu>
Date: Sun, 4 Jan 2015 19:18:22 -0800
Subject: [PATCH] create Logic.Solution

---
 packages/logic-solver/logic.js       | 54 ++++++++++++++++++++++++++++
 packages/logic-solver/logic_tests.js | 19 ++++++++++
 2 files changed, 73 insertions(+)

diff --git a/packages/logic-solver/logic.js b/packages/logic-solver/logic.js
index 37b281c4fb..3dcd805142 100644
--- a/packages/logic-solver/logic.js
+++ b/packages/logic-solver/logic.js
@@ -102,6 +102,10 @@ Logic.Solver = function () {
   // Map of Formulas whose info has `false` for either
   // `occursPositively` or `occursNegatively`
   this._ungeneratedFormulas = {}; // varNum -> Formula
+
+  this._numClausesAddedToMiniSat = 0;
+  this._unsat = false; // once true, no solution henceforth
+  this._minisat = null; // created lazily
 };
 
 // Get a var number for vname, assigning it a number if it is new.
@@ -1008,3 +1012,53 @@ Logic.sum = function (/*formulaOrBitsOrArray, ...*/) {
 
   return new Logic.Bits(binaryWeightedSum(binaryWeighted));
 };
+
+////////////////////////////////////////
+
+Logic.Solver.prototype.solve = function () {
+  var self = this;
+
+  if (self._unsat) {
+    return null;
+  }
+
+  if (! self._minisat) {
+    self._minisat = new MiniSat();
+  }
+
+  while (self._numClausesAddedToMiniSat < self.clauses.length) {
+    var i = self._numClausesAddedToMiniSat;
+    var stillSat = self._minisat.addClause(self.clauses[i].terms);
+    self._numClausesAddedToMiniSat++;
+    if (! stillSat) {
+      self._unsat = true;
+      return null;
+    }
+  }
+
+  var stillSat = self._minisat.solve();
+  if (! stillSat) {
+    self._unsat = true;
+    return null;
+  }
+
+  return new Logic.Solution(self, self._minisat.getSolution());
+};
+
+Logic.Solution = function (_solver, _assignment) {
+  this._solver = _solver;
+  this._assignment = _assignment;
+};
+
+Logic.Solution.prototype.getMap = function () {
+  var solver = this._solver;
+  var assignment = this._assignment;
+  var result = {};
+  for (var i = 1; i < assignment.length; i++) {
+    var name = solver.getVarName(i);
+    if (name && name.charAt(0) !== '$') {
+      result[name] = assignment[i];
+    }
+  }
+  return result;
+};
diff --git a/packages/logic-solver/logic_tests.js b/packages/logic-solver/logic_tests.js
index 85764ecc0a..2cd21c8d61 100644
--- a/packages/logic-solver/logic_tests.js
+++ b/packages/logic-solver/logic_tests.js
@@ -1118,3 +1118,22 @@ Tinytest.add("logic-solver - MiniSat", function (test) {
   test.isFalse(M.solve());
   test.isFalse(M.addClause([4]));
 });
+
+Tinytest.add("logic-solver - simple solve", function (test) {
+  var s = new Logic.Solver;
+  // Unique solution is (1,2,3,4) = (0,1,0,0)
+  s.require("-D");
+  s.require(Logic.or("-A", "-B"));
+  s.require(Logic.or("D", "-A", "B"));
+  s.require(Logic.or("A", "B", "C"));
+  s.require(Logic.or("A", "B", "-C", "D"));
+  s.require(Logic.or("A", "-B", "-C"));
+  var sol = s.solve();
+  test.isTrue(sol);
+  test.equal(sol.getMap(), {
+    A: false, B: true, C: false, D: false
+  });
+  s.require(Logic.or("A", "-B", "C", "D"));
+  var sol2 = s.solve();
+  test.isFalse(sol2);
+});