From bf218213f408d0b6f5982c3f6ea37c3aaf190ec2 Mon Sep 17 00:00:00 2001
From: David Greenspan <dgreenspan@alum.mit.edu>
Date: Sat, 27 Dec 2014 20:32:41 -0800
Subject: [PATCH] Half-adder, full-adder, and tests

---
 packages/logic-solver/logic.js       | 61 ++++++++++++++++++++++++++
 packages/logic-solver/logic_tests.js | 65 ++++++++++++++++++++++++++++
 2 files changed, 126 insertions(+)

diff --git a/packages/logic-solver/logic.js b/packages/logic-solver/logic.js
index bf3687f544..638e1370e5 100644
--- a/packages/logic-solver/logic.js
+++ b/packages/logic-solver/logic.js
@@ -854,3 +854,64 @@ Logic._defineFormula(Logic.EqualBitsFormula, 'equalBits', {
     return t.generate(isTrue, Logic.and(facts));
   }
 });
+
+Logic.HalfAdderSum = function (formula1, formula2) {
+  check(formula1, Logic.FormulaOrTerm);
+  check(formula2, Logic.FormulaOrTerm);
+  check(arguments.length, 2);
+  this.a = formula1;
+  this.b = formula2;
+};
+
+Logic._defineFormula(Logic.HalfAdderSum, 'hsum', {
+  generateClauses: function (isTrue, t) {
+    return t.generate(isTrue, Logic.xor(this.a, this.b));
+  }
+});
+
+Logic.HalfAdderCarry = function (formula1, formula2) {
+  check(formula1, Logic.FormulaOrTerm);
+  check(formula2, Logic.FormulaOrTerm);
+  check(arguments.length, 2);
+  this.a = formula1;
+  this.b = formula2;
+};
+
+Logic._defineFormula(Logic.HalfAdderCarry, 'hcarry', {
+  generateClauses: function (isTrue, t) {
+    return t.generate(isTrue, Logic.and(this.a, this.b));
+  }
+});
+
+Logic.FullAdderSum = function (formula1, formula2, formula3) {
+  check(formula1, Logic.FormulaOrTerm);
+  check(formula2, Logic.FormulaOrTerm);
+  check(formula3, Logic.FormulaOrTerm);
+  check(arguments.length, 3);
+  this.a = formula1;
+  this.b = formula2;
+  this.c = formula3;
+};
+
+Logic._defineFormula(Logic.FullAdderSum, 'fsum', {
+  generateClauses: function (isTrue, t) {
+    return t.generate(isTrue, Logic.xor(this.a, this.b, this.c));
+  }
+});
+
+Logic.FullAdderCarry = function (formula1, formula2, formula3) {
+  check(formula1, Logic.FormulaOrTerm);
+  check(formula2, Logic.FormulaOrTerm);
+  check(formula3, Logic.FormulaOrTerm);
+  check(arguments.length, 3);
+  this.a = formula1;
+  this.b = formula2;
+  this.c = formula3;
+};
+
+Logic._defineFormula(Logic.FullAdderCarry, 'fcarry', {
+  generateClauses: function (isTrue, t) {
+    return t.generate(! isTrue,
+                      Logic.atMostOne(this.a, this.b, this.c));
+  }
+});
diff --git a/packages/logic-solver/logic_tests.js b/packages/logic-solver/logic_tests.js
index f8cabe3d6d..16fd8e57ec 100644
--- a/packages/logic-solver/logic_tests.js
+++ b/packages/logic-solver/logic_tests.js
@@ -934,3 +934,68 @@ Tinytest.add("logic-solver - Logic.lessThan[OrEqual]", function (test) {
      "$xor3 v $xor2 v $xor1"]
   ]);
 });
+
+Tinytest.add("logic-solver - half/full sum/carry", function (test) {
+  runClauseTests(test, [
+    function (s) {
+      s.require(new Logic.HalfAdderSum("A", "B")); },
+    ["A v B", "-A v -B"],
+    function (s) {
+      s.forbid(new Logic.HalfAdderSum("A", "B")); },
+    ["A v -B", "-A v B"],
+    function (s) {
+      s.require(Logic.or(new Logic.HalfAdderSum("A", "B"), "C")); },
+    ["A v B v -$hsum1",
+     "-A v -B v -$hsum1",
+     "$hsum1 v C"],
+    function (s) {
+      s.require(new Logic.HalfAdderCarry("A", "B")); },
+    ["A", "B"],
+    function (s) {
+      s.forbid(new Logic.HalfAdderCarry("A", "B")); },
+    ["-A v -B"],
+    function (s) {
+      s.require(Logic.or(new Logic.HalfAdderCarry("A", "B"), "C")); },
+    ["A v -$hcarry1",
+     "B v -$hcarry1",
+     "$hcarry1 v C"]
+  ]);
+
+  runClauseTests(test, [
+    function (s) {
+      s.require(new Logic.FullAdderSum("A", "B", "C")); },
+    ["A v B v C",
+     "A v -B v -C",
+     "-A v B v -C",
+     "-A v -B v C"],
+    function (s) {
+      s.forbid(new Logic.FullAdderSum("A", "B", "C")); },
+    ["-A v -B v -C",
+     "-A v B v C",
+     "A v -B v C",
+     "A v B v -C"],
+    function (s) {
+      s.require(Logic.or(new Logic.FullAdderSum("A", "B", "C"), "D")); },
+    ["A v B v C v -$fsum1",
+     "A v -B v -C v -$fsum1",
+     "-A v B v -C v -$fsum1",
+     "-A v -B v C v -$fsum1",
+     "$fsum1 v D"],
+    function (s) {
+      s.require(new Logic.FullAdderCarry("A", "B", "C")); },
+    ["A v B",
+     "A v C",
+     "B v C"],
+    function (s) {
+      s.forbid(new Logic.FullAdderCarry("A", "B", "C")); },
+    ["-A v -B",
+     "-A v -C",
+     "-B v -C"],
+    function (s) {
+      s.require(Logic.or(new Logic.FullAdderCarry("A", "B", "C"), "D")); },
+    ["A v B v -$fcarry1",
+     "A v C v -$fcarry1",
+     "B v C v -$fcarry1",
+     "$fcarry1 v D"]
+  ]);
+});