Logic.exactlyOne

packages/logic-solver/logic.js

@@ -673,3 +673,31 @@ Logic._defineFormula(Logic.EquivFormula, 'equiv', {
     return t.generate(!isTrue, Logic.xor(this.A, this.B));
   }
 });
+
+Logic.exactlyOne = function (/*formulaOrArray, ...*/) {
+  var args = _.flatten(arguments);
+  if (args.length === 0) {
+    return Logic.FALSE;
+  } else if (args.length === 1) {
+    return args[0];
+  } else {
+    return new Logic.ExactlyOneFormula(args);
+  }
+};
+
+Logic.ExactlyOneFormula = function (operands) {
+  check(operands, [Logic.FormulaOrTerm]);
+  this.operands = operands;
+};
+
+Logic._defineFormula(Logic.ExactlyOneFormula, 'exactlyOne', {
+  generateClauses: function (isTrue, t) {
+    var args = this.operands;
+    if (args.length < 3) {
+      return t.generate(isTrue, Logic.xor(args));
+    } else {
+      return t.generate(isTrue, Logic.and(Logic.atMostOne(args),
+                                          Logic.or(args)));
+    }
+  }
+});

packages/logic-solver/logic_tests.js

@@ -582,3 +582,41 @@ Tinytest.add("logic-solver - Logic.implies, Logic.equiv", function (test) {
      "-$or1 v $or2"]
   ]);
 });
+
+Tinytest.add("logic-solver - Logic.exactlyOne", function (test) {
+  runClauseTests(test, [
+    function (s) {
+      s.require(Logic.exactlyOne()); },
+    [""],
+    function (s) {
+      s.forbid(Logic.exactlyOne()); },
+    [],
+    function (s) {
+      s.require(Logic.exactlyOne("A")); },
+    ["A"],
+    function (s) {
+      s.forbid(Logic.exactlyOne("A")); },
+    ["-A"],
+    function (s) {
+      s.require(Logic.exactlyOne("A", "B")); },
+    ["A v B", "-A v -B"],
+    function (s) {
+      s.forbid(Logic.exactlyOne("A", "B")); },
+    ["A v -B", "-A v B"],
+    function (s) {
+      s.require(Logic.exactlyOne("A", "B", "C")); },
+    ["-A v -B",
+     "-A v -C",
+     "-B v -C",
+     "A v B v C"],
+    function (s) {
+      s.forbid(Logic.exactlyOne("A", "B", "C")); },
+    ["A v B v $atMostOne1",
+     "A v C v $atMostOne1",
+     "B v C v $atMostOne1",
+     "-A v $or1",
+     "-B v $or1",
+     "-C v $or1",
+     "-$atMostOne1 v -$or1"]
+  ]);
+});