Add argument set reduction operators

extension/boolexpr/argset.c

@@ -10,6 +10,35 @@
 #include "boolexpr.h"
 
 
+/* boolexpr.c */
+struct BoolExpr * _bx_op_from(BoolExprKind kind, size_t n, struct BoolExpr **xs);
+
+
+static struct BoolExpr **
+_set2array(struct BoolExprSet *set)
+{
+    struct BoolExpr **array;
+    struct BoolExprSetIter *it;
+
+    array = malloc(set->length * sizeof(struct BoolExpr *));
+    if (array == NULL)
+        return NULL; // LCOV_EXCL_LINE
+
+    it = BoolExprSetIter_New(set);
+    if (it == NULL) {
+        free(array); // LCOV_EXCL_LINE
+        return NULL; // LCOV_EXCL_LINE
+    }
+
+    for (size_t i = 0; !it->done; BoolExprSetIter_Next(it))
+        array[i++] = BoolExprSetIter_Key(it);
+
+    BoolExprSetIter_Del(it);
+
+    return array;
+}
+
+
 struct BoolExprOrAndArgSet *
 BoolExprOrAndArgSet_New(BoolExprKind kind)
 {
@@ -81,6 +110,30 @@ BoolExprOrAndArgSet_Insert(struct BoolExprOrAndArgSet *argset, struct BoolExpr *
 }
 
 
+struct BoolExpr *
+BoolExprOrAndArgSet_Reduce(struct BoolExprOrAndArgSet *argset)
+{
+    struct BoolExpr **xs;
+    size_t length = argset->xs->length;
+
+    if (argset->min)
+        return BoolExpr_IncRef(IDENTITY[argset->kind]);
+
+    if (argset->max)
+        return BoolExpr_IncRef(DOMINATOR[argset->kind]);
+
+    CHECK_NULL(xs, _set2array(argset->xs));
+
+    if (length == 1) {
+        struct BoolExpr *y = BoolExpr_IncRef(xs[0]);
+        free(xs);
+        return y;
+    }
+
+    return _bx_op_from(argset->kind, length, xs);
+}
+
+
 struct BoolExprXorArgSet *
 BoolExprXorArgSet_New(bool parity)
 {
@@ -162,6 +215,42 @@ BoolExprXorArgSet_Insert(struct BoolExprXorArgSet *argset, struct BoolExpr *key)
 }
 
 
+struct BoolExpr *
+BoolExprXorArgSet_Reduce(struct BoolExprXorArgSet *argset)
+{
+    struct BoolExpr **xs;
+    struct BoolExpr *temp;
+    struct BoolExpr *y;
+    size_t length = argset->xs->length;
+
+    if (length == 0) {
+        temp = BoolExpr_IncRef(IDENTITY[OP_XOR]);
+        y = argset->parity ? BoolExpr_IncRef(temp) : Not(temp);
+        BoolExpr_DecRef(temp);
+        return y;
+    }
+
+    CHECK_NULL(xs, _set2array(argset->xs));
+
+    if (length == 1) {
+        temp = BoolExpr_IncRef(xs[0]);
+        free(xs);
+    }
+    else {
+        temp = _bx_op_from(OP_XOR, length, xs);
+        if (temp == NULL) {
+            free(xs);    // LCOV_EXCL_LINE
+            return NULL; // LCOV_EXCL_LINE
+        }
+    }
+
+    y = argset->parity ? BoolExpr_IncRef(temp) : Not(temp);
+    BoolExpr_DecRef(temp);
+
+    return y;
+}
+
+
 struct BoolExprEqArgSet *
 BoolExprEqArgSet_New(void)
 {
@@ -228,3 +317,62 @@ BoolExprEqArgSet_Insert(struct BoolExprEqArgSet *argset, struct BoolExpr *key)
     return BoolExprSet_Insert(argset->xs, key);
 }
 
+
+struct BoolExpr *
+BoolExprEqArgSet_Reduce(struct BoolExprEqArgSet *argset)
+{
+    struct BoolExpr **xs;
+    struct BoolExpr *y;
+    size_t length = argset->xs->length;
+
+    /* Equal(0, 1) = 0 */
+    if (argset->zero && argset->one)
+        return BoolExpr_IncRef(&Zero);
+
+    /* Equal() = Equal(0) = Equal(1) = 1 */
+    if (((size_t) argset->zero + (size_t) argset->one + length) <= 1)
+        return BoolExpr_IncRef(&One);
+
+    CHECK_NULL(xs, _set2array(argset->xs));
+
+    /* Equal(0, x) = ~x */
+    if (argset->zero && length == 1) {
+        y = Not(xs[0]);
+        free(xs);
+        return y;
+    }
+
+    /* Equal(1, x) = x */
+    if (argset->one && length == 1) {
+        y = BoolExpr_IncRef(xs[0]);
+        free(xs);
+        return y;
+    }
+
+    /* Equal(0, x, y) = Nor(x, y) */
+    if (argset->zero) {
+        struct BoolExpr *temp = _bx_op_from(OP_OR, length, xs);
+        if (temp == NULL) {
+            free(xs);    // LCOV_EXCL_LINE
+            return NULL; // LCOV_EXCL_LINE
+        }
+        y = Not(temp);
+        BoolExpr_DecRef(temp);
+        return y;
+    }
+
+    /* Equal(1, x, y) = Nand(x, y) */
+    if (argset->one) {
+        struct BoolExpr *temp = _bx_op_from(OP_AND, length, xs);
+        if (temp == NULL) {
+            free(xs);    // LCOV_EXCL_LINE
+            return NULL; // LCOV_EXCL_LINE
+        }
+        y = Not(temp);
+        BoolExpr_DecRef(temp);
+        return y;
+    }
+
+    return _bx_op_from(OP_EQ, length, xs);
+}
+

extension/boolexpr/boolexpr.c

@@ -28,6 +28,9 @@ do { \
 } while (0)
 
 
+/* array.c */
+struct BoolExprArray * _bx_array_from(size_t length, struct BoolExpr **items);
+
 /* util.c */
 size_t _uniqid2index(long uniqid);
 bool _is_clause(struct BoolExpr *op);
@@ -138,7 +141,7 @@ _lit_del(struct BoolExpr *lit)
 
 
 struct BoolExpr *
-_op_new(BoolExprKind kind, size_t n, struct BoolExpr **xs)
+_bx_op_from(BoolExprKind kind, size_t n, struct BoolExpr **xs)
 {
     struct BoolExpr *op;
 
@@ -149,7 +152,7 @@ _op_new(BoolExprKind kind, size_t n, struct BoolExpr **xs)
     op->refcount = 1;
     op->kind = kind;
     op->flags = (BoolExprFlags) 0;
-    op->data.xs = BoolExprArray_New(n, xs);
+    op->data.xs = _bx_array_from(n, xs);
     if (op->data.xs == NULL) {
         free(op);    // LCOV_EXCL_LINE
         return NULL; // LCOV_EXCL_LINE
@@ -159,6 +162,22 @@ _op_new(BoolExprKind kind, size_t n, struct BoolExpr **xs)
 }
 
 
+struct BoolExpr *
+_op_new(BoolExprKind kind, size_t n, struct BoolExpr **xs)
+{
+    struct BoolExpr **xs_copy;
+
+    xs_copy = malloc(n * sizeof(struct BoolExpr *));
+    if (xs_copy == NULL)
+        return NULL; // LCOV_EXCL_LINE
+
+    for (size_t i = 0; i < n; ++i)
+        xs_copy[i] = xs[i];
+
+    return _bx_op_from(kind, n, xs_copy);
+}
+
+
 struct BoolExpr *
 _orandxor_new(BoolExprKind kind, size_t n, struct BoolExpr **xs)
 {

extension/boolexpr/boolexpr.h

@@ -513,6 +513,8 @@ void BoolExprOrAndArgSet_Del(struct BoolExprOrAndArgSet *);
 
 bool BoolExprOrAndArgSet_Insert(struct BoolExprOrAndArgSet *, struct BoolExpr *key);
 
+struct BoolExpr * BoolExprOrAndArgSet_Reduce(struct BoolExprOrAndArgSet *);
+
 
 /*
 ** Return a new XOR/XNOR set
@@ -523,6 +525,8 @@ void BoolExprXorArgSet_Del(struct BoolExprXorArgSet *);
 
 bool BoolExprXorArgSet_Insert(struct BoolExprXorArgSet *, struct BoolExpr *key);
 
+struct BoolExpr * BoolExprXorArgSet_Reduce(struct BoolExprXorArgSet *);
+
 
 /*
 ** Return a new Equal set
@@ -533,6 +537,8 @@ void BoolExprEqArgSet_Del(struct BoolExprEqArgSet *);
 
 bool BoolExprEqArgSet_Insert(struct BoolExprEqArgSet *, struct BoolExpr *key);
 
+struct BoolExpr * BoolExprEqArgSet_Reduce(struct BoolExprEqArgSet *);
+
 
 #ifdef __cplusplus
 }