<commit_before>/*
 * Copyright 2011-2014 Formal Methods and Tools, University of Twente
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *     http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */

#include <sylvan_config.h>

#include <assert.h>
#include <inttypes.h>
#include <math.h>
#include <pthread.h>
#include <stdint.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>

#include <atomics.h>
#include <avl.h>
#include <refs.h>
#include <sha2.h>
#include <sylvan.h>
#include <sylvan_common.h>

/**
 * Complement handling macros
 */
#define BDD_HASMARK(s)              (s&sylvan_complement?1:0)
#define BDD_TOGGLEMARK(s)           (s^sylvan_complement)
#define BDD_STRIPMARK(s)            (s&~sylvan_complement)
#define BDD_TRANSFERMARK(from, to)  (to ^ (from & sylvan_complement))
// Equal under mark
#define BDD_EQUALM(a, b)            ((((a)^(b))&(~sylvan_complement))==0)

static inline BDD BDD_SETDATA(BDD s, uint32_t data)
{
    return (s & 0x800000ffffffffff) | (((uint64_t)data & 0x7fffff)<<40);
}

typedef struct __attribute__((packed)) bddnode {
    uint64_t high     : 40;
    uint32_t level    : 24;
    uint64_t low      : 40;
    unsigned int data : 23;
    uint8_t comp      : 1;
} *bddnode_t; // 16 bytes

#define GETNODE(bdd) ((bddnode_t)llmsset_index_to_ptr(nodes, BDD_STRIPMARK(bdd)))

/**
 * Implementation of garbage collection.
 */

/* Recursively mark BDD nodes as 'in use' */
VOID_TASK_IMPL_1(sylvan_gc_mark_rec, BDD, bdd)
{
    if (bdd == sylvan_false || bdd == sylvan_true) return;

    if (llmsset_mark(nodes, bdd&0x000000ffffffffff)) {
        bddnode_t n = GETNODE(bdd);
        SPAWN(sylvan_gc_mark_rec, n->low);
        CALL(sylvan_gc_mark_rec, n->high);
        SYNC(sylvan_gc_mark_rec);
    }
}

/**
 * External references
 */

refs_table_t bdd_refs;
refs_table_t bdd_protected;
static int bdd_protected_created = 0;

BDD
sylvan_ref(BDD a)
{
    if (a == sylvan_false || a == sylvan_true) return a;
    refs_up(&bdd_refs, BDD_STRIPMARK(a));
    return a;
}

void
sylvan_deref(BDD a)
{
    if (a == sylvan_false || a == sylvan_true) return;
    refs_down(&bdd_refs, BDD_STRIPMARK(a));
}

void
sylvan_protect(BDD *a)
{
    if (!bdd_protected_created) {
        // In C++, sometimes sylvan_protect is called before Sylvan is initialized. Just create a table.
        protect_create(&bdd_protected, 4096);
        bdd_protected_created = 1;
    }
    protect_up(&bdd_protected, (size_t)a);
}

void
sylvan_unprotect(BDD *a)
{
    protect_down(&bdd_protected, (size_t)a);
}

size_t
sylvan_count_refs()
{
    return refs_count(&bdd_refs);
}

size_t
sylvan_count_protected()
{
    return protect_count(&bdd_protected);
}

/* Called during garbage collection */
VOID_TASK_0(sylvan_gc_mark_external_refs)
{
    // iterate through refs hash table, mark all found
    size_t count=0;
    uint64_t *it = refs_iter(&bdd_refs, 0, bdd_refs.refs_size);
    while (it != NULL) {
        BDD to_mark = refs_next(&bdd_refs, &it, bdd_refs.refs_size);
        SPAWN(sylvan_gc_mark_rec, to_mark);
        count++;
    }
    while (count--) {
        SYNC(sylvan_gc_mark_rec);
    }
}

VOID_TASK_0(sylvan_gc_mark_protected)
{
    // iterate through refs hash table, mark all found
    size_t count=0;
    uint64_t *it = protect_iter(&bdd_protected, 0, bdd_protected.refs_size);
    while (it != NULL) {
        BDD *to_mark = (BDD*)protect_next(&bdd_protected, &it, bdd_protected.refs_size);
        SPAWN(sylvan_gc_mark_rec, *to_mark);
        count++;
    }
    while (count--) {
        SYNC(sylvan_gc_mark_rec);
    }
}

/* Infrastructure for internal markings */
DECLARE_THREAD_LOCAL(bdd_refs_key, bdd_refs_internal_t);

VOID_TASK_0(bdd_refs_mark_task)
{
    LOCALIZE_THREAD_LOCAL(bdd_refs_key, bdd_refs_internal_t);
    size_t i, j=0;
    for (i=0; i<bdd_refs_key->r_count; i++) {
        if (j >= 40) {
            while (j--) SYNC(sylvan_gc_mark_rec);
            j=0;
        }
        SPAWN(sylvan_gc_mark_rec, bdd_refs_key->results[i]);
        j++;
    }
    for (i=0; i<bdd_refs_key->s_count; i++) {
        Task *t = bdd_refs_key->spawns[i];
        if (!TASK_IS_STOLEN(t)) break;
        if (TASK_IS_COMPLETED(t)) {
            if (j >= 40) {
                while (j--) SYNC(sylvan_gc_mark_rec);
                j=0;
            }
            SPAWN(sylvan_gc_mark_rec, *(BDD*)TASK_RESULT(t));
            j++;
        }
    }
    while (j--) SYNC(sylvan_gc_mark_rec);
}

VOID_TASK_0(bdd_refs_mark)
{
    TOGETHER(bdd_refs_mark_task);
}

VOID_TASK_0(bdd_refs_init_task)
{
    bdd_refs_internal_t s = (bdd_refs_internal_t)malloc(sizeof(struct bdd_refs_internal));
    s->r_size = 128;
    s->r_count = 0;
    s->s_size = 128;
    s->s_count = 0;
    s->results = (BDD*)malloc(sizeof(BDD) * 128);
    s->spawns = (Task**)malloc(sizeof(Task*) * 128);
    SET_THREAD_LOCAL(bdd_refs_key, s);
}

VOID_TASK_0(bdd_refs_init)
{
    INIT_THREAD_LOCAL(bdd_refs_key);
    TOGETHER(bdd_refs_init_task);
    sylvan_gc_add_mark(10, TASK(bdd_refs_mark));
}

/**
 * Initialize and quit functions
 */

static int granularity = 1; // default

static void
sylvan_quit_bdd()
{
    refs_free(&bdd_refs);
    if (bdd_protected_created) {
        protect_free(&bdd_protected);
        bdd_protected_created = 0;
    }
}

void
sylvan_init_bdd(int _granularity)
{
    sylvan_register_quit(sylvan_quit_bdd);
    sylvan_gc_add_mark(10, TASK(sylvan_gc_mark_external_refs));
    sylvan_gc_add_mark(10, TASK(sylvan_gc_mark_protected));

    granularity = _granularity;

    // Sanity check
    if (sizeof(struct bddnode) != 16) {
        fprintf(stderr, "Invalid size of bdd nodes: %ld\n", sizeof(struct bddnode));
        exit(1);
    }

    refs_create(&bdd_refs, 1024);
    if (!bdd_protected_created) {
        protect_create(&bdd_protected, 4096);
        bdd_protected_created = 1;
    }

    LACE_ME;
    CALL(bdd_refs_init);
}

/**
 * Core BDD operations
 */

BDD
sylvan_makenode(BDDVAR level, BDD low, BDD high)
{
    if (low == high) return low;

    // Normalization to keep canonicity
    // low will have no mark

    struct bddnode n;
    int mark;

    if (BDD_HASMARK(low)) {
        mark = 1;
        n = (struct bddnode){high, level, low, 0, (uint8_t)(BDD_HASMARK(high) ? 0 : 1)};
    } else {
        mark = 0;
        n = (struct bddnode){high, level, low, 0, (uint8_t)(BDD_HASMARK(high) ? 1 : 0)};
    }

    BDD result;
    int created;
    uint64_t index = llmsset_lookup(nodes, &n, &created);
    if (index == 0) {
        LACE_ME;

        //size_t before_gc = llmsset_count_marked(nodes);
        bdd_refs_push(low);
        bdd_refs_push(high);
        sylvan_gc();
        bdd_refs_pop(2);
        //size_t after_gc = llmsset_count_marked(nodes);
        //size_t total = llmsset_get_size(nodes);
        //fprintf(stderr, "GC: %.01f%% to %.01f%%\n", 100.0*(double)before_gc/total, 100.0*(double)after_gc/total);

        index = llmsset_lookup(nodes, &n, &created);
        if (index == 0) {
            fprintf(stderr, "BDD Unique table full, %zu of %zu buckets filled!\n", llmsset_count_marked(nodes), llmsset_get_size(nodes));
            exit(1);
        }
    }

    if (created) sylvan_stats_count(BDD_NODES_CREATED);
    else sylvan_stats_count(BDD_NODES_REUSED);

    result = index;
    return mark ? result | sylvan_complement : result;
}

BDD
sylvan_ithvar(BDDVAR level)
{
    return sylvan_makenode(level, sylvan_false, sylvan_true);
}

BDDVAR
sylvan_var(BDD bdd)
{
    if (bdd == sylvan_false || bdd == sylvan_true) bdd = sylvan_invalid; // force crash
    return GETNODE(bdd)->level;
}

static inline BDD
node_lowedge(bddnode_t node)
{
    return node->low;
}

static inline BDD
node_highedge(bddnode_t node)
{
    return node->high | (node->comp ? sylvan_complement : 0LL);
}

static inline BDD
node_low(BDD bdd, bddnode_t node)
{
    return BDD_TRANSFERMARK(bdd, node_lowedge(node));
}

static inline BDD
node_high(BDD bdd, bddnode_t node)
{
    return BDD_TRANSFERMARK(bdd, node_highedge(node));
}

BDD
sylvan_low(BDD bdd)
{
    if (sylvan_isconst(bdd)) return bdd;
    return node_low(bdd, GETNODE(bdd));
}

BDD
sylvan_high(BDD bdd)
{
    if (sylvan_isconst(bdd)) return bdd;
    return node_high(bdd, GETNODE(bdd));
}

/**
 * Debugging functionality that converts a BDD to one without complemented edges.
 */

BDD
sylvan_makenode_nocomp(BDDVAR level, BDD low, BDD high)
{
    if (low == high) return low;

    struct bddnode n = (struct bddnode){high, level, low, 0, 0};

    int created;
    uint64_t index = llmsset_lookup(nodes, &n, &created);
    if (index == 0) {
        LACE_ME;
        bdd_refs_push(low);
        bdd_refs_push(high);
        sylvan_gc();
        bdd_refs_pop(2);
        index = llmsset_lookup(nodes, &n, &created);
        if (index == 0) {
            fprintf(stderr, "BDD Unique table full, %zu of %zu buckets filled!\n", llmsset_count_marked(nodes), llmsset_get_size(nodes));
            exit(1);
        }
    }

    return (BDD)index;
}

BDD
sylvan_bdd_to_nocomp(BDD bdd)
{
    if (bdd == sylvan_true) return sylvan_true_nc;
    if (bdd == sylvan_false) return sylvan_false;

    bddnode_t n = GETNODE(bdd);
    return sylvan_makenode_nocomp(n->level, sylvan_bdd_to_nocomp(node_low(bdd, n)), sylvan_bdd_to_nocomp(node_high(bdd, n)));
}

/**
 * Implementation of unary, binary and if-then-else operators.
 */
TASK_IMPL_3(BDD, sylvan_and, BDD, a, BDD, b, BDDVAR, prev_level)
{
    /* Terminal cases */
    if (a == sylvan_true) return b;
    if (b == sylvan_true) return a;
    if (a == sylvan_false) return sylvan_false;
    if (b == sylvan_false) return sylvan_false;

    sylvan_gc_test();

    sylvan_stats_count(BDD_AND);

    /* Improve for caching */
    if (BDD_STRIPMARK(a) > BDD_STRIPMARK(b)) {
        BDD t = b;
        b = a;
        a = t;
    }

    bddnode_t na = GETNODE(a);
    bddnode_t nb = GETNODE(b);

    BDDVAR level = na->level < nb->level ? na->level : nb->level;

    int cachenow = granularity < 2 || prev_level == 0 ? 1 : prev_level / granularity != level / granularity;
    if (cachenow) {
        BDD result;
        if (cache_get(BDD_SETDATA(a, CACHE_AND), b, sylvan_false, &result)) {
            sylvan_stats_count(BDD_AND_CACHED);
            return result;
        }
    }

    // Get cofactors
    BDD aLow = a, aHigh = a;
    BDD bLow = b, bHigh = b;
    if (level == na->level) {
        aLow = node_low(a, na);
        aHigh = node_high(a, na);
    }
    if (level == nb->level) {
        bLow = node_low(b, nb);
        bHigh = node_high(b, nb);
    }

    // Recursive computation
    BDD low=sylvan_invalid, high=sylvan_invalid, result;

    int n=0;

    if (aHigh == sylvan_true) {
        high = bHigh;
    } else if (aHigh == sylvan_false || bHigh == sylvan_false) {
        high = sylvan_false;
    } else if (bHigh == sylvan_true) {
        high = aHigh;
    } else {
        bdd_refs_spawn(SPAWN(sylvan_and, aHigh, bHigh, level));
        n=1;
    }

    if (aLow == sylvan_true) {
        low = bLow;
    } else if (aLow == sylvan_false || bLow == sylvan_false) {
        low = sylvan_false;
    } else if (bLow == sylvan_true) {
        low = aLow;
    } else {
        low = CALL(sylvan_and, aLow, bLow, level);
    }

    if (n) {
        bdd_refs_push(low);
        high = bdd_refs_sync(SYNC(sylvan_and));
        bdd_refs_pop(1);
    }

    result = sylvan_makenode(level, low, high);

    if (cachenow) {
        cache_put(BDD_SETDATA(a, CACHE_AND), b, sylvan_false, result);
    }

    return result;
}

TASK_IMPL_3(BDD, sylvan_xor, BDD, a, BDD, b, BDDVAR, prev_level)
{
    /* Terminal cases */
    if (a == sylvan_false) return b;
    if (b == sylvan_false) return a;
    if (a == sylvan_true) return sylvan_not(b);
    if (b == sylvan_true) return sylvan_not(a);
    if (a == b) return sylvan_false;
    if (a == sylvan_not(b)) return sylvan_true;

    sylvan_gc_test();

    sylvan_stats_count(BDD_XOR);

    /* Improve for caching */
    if (BDD_STRIPMARK(a) > BDD_STRIPMARK(b)) {
        BDD t = b;
        b = a;
        a = t;
    }

    // XOR(~A,B) => XOR(A,~B)
    if (BDD_HASMARK(a)) {
        a = BDD_STRIPMARK(a);
        b = sylvan_not(b);
    }

    bddnode_t na = GETNODE(a);
    bddnode_t nb = GETNODE(b);

    BDDVAR level = na->level < nb->level ? na->level : nb->level;

    int cachenow = granularity < 2 || prev_level == 0 ? 1 : prev_level / granularity != level / granularity;
    if (cachenow) {
        BDD result;
        if (cache_get(BDD_SETDATA(a, CACHE_XOR), b, sylvan_false, &result)) {
            sylvan_stats_count(BDD_XOR_CACHED);
            return result;
        }
    }

    // Get cofactors
    BDD aLow = a, aHigh = a;
    BDD bLow = b, bHigh = b;
    if (level == na->level) {
        aLow = node_low(a, na);
        aHigh = node_high(a, na);
    }
    if (level == nb->level) {
        bLow = node_low(b, nb);
        bHigh = node_high(b, nb);
    }

    // Recursive computation
    BDD low, high, result;

    bdd_refs_spawn(SPAWN(sylvan_xor, aHigh, bHigh, level));
    low = CALL(sylvan_xor, aLow, bLow, level);
    bdd_refs_push(low);
    high = bdd_refs_sync(SYNC(sylvan_xor));
    bdd_refs_pop(1);

    result = sylvan_makenode(level, low, high);

    if (cachenow) {
        cache_put(BDD_SETDATA(a, CACHE_XOR), b, sylvan_false, result);
    }

    return result;
}


TASK_IMPL_4(BDD, sylvan_ite, BDD, a, BDD, b, BDD, c, BDDVAR, prev_level)
{
    /* Terminal cases */
    if (a == sylvan_true) return b;
    if (a == sylvan_false) return c;
    if (a == b) b = sylvan_true;
    if (a == sylvan_not(b)) b = sylvan_false;
    if (a == c) c = sylvan_false;
    if (a == sylvan_not(c)) c = sylvan_true;
    if (b == c) return b;
    if (b == sylvan_true && c == sylvan_false) return a;
    if (b == sylvan_false && c == sylvan_true) return sylvan_not(a);

    /* Cases that reduce to AND and XOR */

    // ITE(A,B,0) => AND(A,B)
    if (c == sylvan_false) return CALL(sylvan_and, a, b, prev_level);

    // ITE(A,1,C) => ~AND(~A,~C)
    if (b == sylvan_true) return sylvan_not(CALL(sylvan_and, sylvan_not(a), sylvan_not(c), prev_level));

    // ITE(A,0,C) => AND(~A,C)
    if (b == sylvan_false) return CALL(sylvan_and, sylvan_not(a), c, prev_level);

    // ITE(A,B,1) => ~AND(A,~B)
    if (c == sylvan_true) return sylvan_not(CALL(sylvan_and, a, sylvan_not(b), prev_level));

    // ITE(A,B,~B) => XOR(A,~B)
    if (b == sylvan_not(c)) return CALL(sylvan_xor, a, c, 0);

    /* At this point, there are no more terminals */

    /* Canonical for optimal cache use */

    // ITE(~A,B,C) => ITE(A,C,B)
    if (BDD_HASMARK(a)) {
        a = BDD_STRIPMARK(a);
        BDD t = c;
        c = b;
        b = t;
    }

    // ITE(A,~B,C) => ~ITE(A,B,~C)
    int mark = 0;
    if (BDD_HASMARK(b)) {
        b = sylvan_not(b);
        c = sylvan_not(c);
        mark = 1;
    }

    sylvan_gc_test();

    sylvan_stats_count(BDD_ITE);

    bddnode_t na = GETNODE(a);
    bddnode_t nb = GETNODE(b);
    bddnode_t nc = GETNODE(c);

    // Get lowest level
    BDDVAR level = nb->level < nc->level ? nb->level : nc->level;

    // Fast case
    if (na->level < level && node_low(a, na) == sylvan_false && node_high(a, na) == sylvan_true) {
        BDD result = sylvan_makenode(na->level, c, b);
        return mark ? sylvan_not(result) : result;
    }

    if (na->level < level) level = na->level;

    int cachenow = granularity < 2 || prev_level == 0 ? 1 : prev_level / granularity != level / granularity;
    if (cachenow) {
        BDD result;
        if (cache_get(BDD_SETDATA(a, CACHE_ITE), b, c, &result)) {
            sylvan_stats_count(BDD_ITE_CACHED);
            return mark ? sylvan_not(result) : result;
        }
    }

    // Get cofactors
    BDD aLow = a, aHigh = a;
    BDD bLow = b, bHigh = b;
    BDD cLow = c, cHigh = c;
    if (level == na->level) {
        aLow = node_low(a, na);
        aHigh = node_high(a, na);
    }
    if (level == nb->level) {
        bLow = node_low(b, nb);
        bHigh = node_high(b, nb);
    }
    if (level == nc->level) {
        cLow = node_low(c, nc);
        cHigh = node_high(c, nc);
    }

    // Recursive computation
    BDD low=sylvan_invalid, high=sylvan_invalid, result;

    int n=0;

    if (aHigh == sylvan_true) {
        high = bHigh;
    } else if (aHigh == sylvan_false) {
        high = cHigh;
    } else {
        bdd_refs_spawn(SPAWN(sylvan_ite, aHigh, bHigh, cHigh, level));
        n=1;
    }

    if (aLow == sylvan_true) {
        low = bLow;
    } else if (aLow == sylvan_false) {
        low = cLow;
    } else {
        low = CALL(sylvan_ite, aLow, bLow, cLow, level);
    }

    if (n) {
        bdd_refs_push(low);
        high = bdd_refs_sync(SYNC(sylvan_ite));
        bdd_refs_pop(1);
    }

    result = sylvan_makenode(level, low, high);

    if (cachenow) {
        cache_put(BDD_SETDATA(a, CACHE_ITE), b, c, result);
    }

    return mark ? sylvan_not(result) : result;
}

/**
 * Calculate constrain a @ c
 */
TASK_IMPL_3(BDD, sylvan_constrain, BDD, a, BDD, b, BDDVAR, prev_level)
{
    /* Trivial cases */
    if (b == sylvan_true) return a;
    if (b == sylvan_false) return sylvan_false;
    if (sylvan_isconst(a)) return a;
    if (a == b) return sylvan_true;
    if (a == sylvan_not(b)) return sylvan_false;

    /* Perhaps execute garbage collection */
    sylvan_gc_test();

    /* Count operation */
    sylvan_stats_count(BDD_CONSTRAIN);

    // a != constant and b != constant
    bddnode_t na = GETNODE(a);
    bddnode_t nb = GETNODE(b);

    BDDVAR level = na->level < nb->level ? na->level : nb->level;

    // CONSULT CACHE

    int cachenow = granularity < 2 || prev_level == 0 ? 1 : prev_level / granularity != level / granularity;
    if (cachenow) {
        BDD result;
        if (cache_get(BDD_SETDATA(a, CACHE_CONSTRAIN), b, 0, &result)) {
            sylvan_stats_count(BDD_CONSTRAIN_CACHED);
            return result;
        }
    }

    // DETERMINE TOP BDDVAR AND COFACTORS

    BDD aLow, aHigh, bLow, bHigh;

    if (na->level == level) {
        aLow = node_low(a, na);
        aHigh = node_high(a, na);
    } else {
        aLow = aHigh = a;
    }

    if (nb->level == level) {
        bLow = node_low(b, nb);
        bHigh = node_high(b, nb);
    } else {
        bLow = bHigh = b;
    }

    BDD result;

    BDD low=sylvan_invalid, high=sylvan_invalid;
    if (bLow == sylvan_false) return CALL(sylvan_constrain, aHigh, bHigh, level);
    if (bLow == sylvan_true) {
        if (bHigh == sylvan_false) return aLow;
        if (bHigh == sylvan_true) {
            result = sylvan_makenode(level, aLow, bHigh);
        } else {
            high = CALL(sylvan_constrain, aHigh, bHigh, level);
            result = sylvan_makenode(level, aLow, high);
        }
    } else {
        if (bHigh == sylvan_false) return CALL(sylvan_constrain, aLow, bLow, level);
        if (bHigh == sylvan_true) {
            low = CALL(sylvan_constrain, aLow, bLow, level);
            result = sylvan_makenode(level, low, bHigh);
        } else {
            bdd_refs_spawn(SPAWN(sylvan_constrain, aLow, bLow, level));
            high = CALL(sylvan_constrain, aHigh, bHigh, level);
            bdd_refs_push(high);
            low = bdd_refs_sync(SYNC(sylvan_constrain));
            bdd_refs_pop(1);
            result = sylvan_makenode(level, low, high);
        }
    }

    if (cachenow) {
        cache_put(BDD_SETDATA(a, CACHE_CONSTRAIN), b, 0, result);
    }

    return result;
}

/**
 * Calculate restrict a @ b
 */
TASK_IMPL_3(BDD, sylvan_restrict, BDD, a, BDD, b, BDDVAR, prev_level)
{
    /* Trivial cases */
    if (b == sylvan_true) return a;
    if (b == sylvan_false) return sylvan_false;
    if (sylvan_isconst(a)) return a;
    if (a == b) return sylvan_true;
    if (a == sylvan_not(b)) return sylvan_false;

    /* Perhaps execute garbage collection */
    sylvan_gc_test();

    /* Count operation */
    sylvan_stats_count(BDD_RESTRICT);

    // a != constant and b != constant
    bddnode_t na = GETNODE(a);
    bddnode_t nb = GETNODE(b);

    BDDVAR level = na->level < nb->level ? na->level : nb->level;

    /* Consult cache */
    int cachenow = granularity < 2 || prev_level == 0 ? 1 : prev_level / granularity != level / granularity;
    if (cachenow) {
        BDD result;
        if (cache_get(BDD_SETDATA(a, CACHE_RESTRICT), b, 0, &result)) {
            sylvan_stats_count(BDD_RESTRICT_CACHED);
            return result;
        }
    }

    BDD result;

    if (nb->level < na->level) {
        BDD c = CALL(sylvan_ite, node_low(b,nb), sylvan_true, node_high(b,nb), 0);
        bdd_refs_push(c);
        result = CALL(sylvan_restrict, a, c, level);
        bdd_refs_pop(1);
    } else {
        BDD aLow=node_low(a,na),aHigh=node_high(a,na),bLow=b,bHigh=b;
        if (na->level == nb->level) {
            bLow = node_low(b,nb);
            bHigh = node_high(b,nb);
        }
        if (bLow == sylvan_false) {
            result = CALL(sylvan_restrict, aHigh, bHigh, level);
        } else if (bHigh == sylvan_false) {
            result = CALL(sylvan_restrict, aLow, bLow, level);
        } else {
            bdd_refs_spawn(SPAWN(sylvan_restrict, aLow, bLow, level));
            BDD high = CALL(sylvan_restrict, aHigh, bHigh, level);
            bdd_refs_push(high);
            BDD low = bdd_refs_sync(SYNC(sylvan_restrict));
            bdd_refs_pop(1);
            result = sylvan_makenode(level, low, high);
        }
    }

    if (cachenow) {
        cache_put(BDD_SETDATA(a, CACHE_RESTRICT), b, 0, result);
    }

    return result;
}

/**
 * Calculates \exists variables . a
 */
TASK_IMPL_3(BDD, sylvan_exists, BDD, a, BDD, variables, BDDVAR, prev_level)
{
    /* Terminal cases */
    if (a == sylvan_true) return sylvan_true;
    if (a == sylvan_false) return sylvan_false;
    if (sylvan_set_isempty(variables)) return a;

    sylvan_gc_test();

    sylvan_stats_count(BDD_EXISTS);

    // a != constant
    bddnode_t na = GETNODE(a);
    BDDVAR level = na->level;

    // Get cofactors
    BDD aLow = node_low(a, na);
    BDD aHigh = node_high(a, na);

    while (!sylvan_set_isempty(variables) && sylvan_var(variables) < level) {
        // Skip variables before x
        variables = sylvan_set_next(variables);
    }

    if (sylvan_set_isempty(variables)) return a; // nothing to quantify

    int cachenow = granularity < 2 || prev_level == 0 ? 1 : prev_level / granularity != level / granularity;
    if (cachenow) {
        BDD result;
        if (cache_get(BDD_SETDATA(a, CACHE_EXISTS), variables, 0, &result)) {
            sylvan_stats_count(BDD_EXISTS_CACHED);
            return result;
        }
    }

    BDD result;

    if (sylvan_set_var(variables) == level) {
        // level is in variable set, perform abstraction
        variables = sylvan_set_next(variables);
        BDD low = CALL(sylvan_exists, aLow, variables, level);
        if (low == sylvan_true) {
            result = sylvan_true;
        } else {
            bdd_refs_push(low);
            BDD high = CALL(sylvan_exists, aHigh, variables, level);
            if (high == sylvan_true) {
                result = sylvan_true;
                bdd_refs_pop(1);
            } else if (low == sylvan_false && high == sylvan_false) {
                result = sylvan_false;
                bdd_refs_pop(1);
            } else {
                bdd_refs_push(high);
                result = CALL(sylvan_ite, low, sylvan_true, high, 0); // or
                bdd_refs_pop(2);
            }
        }
    } else {
        // level is not in variable set
        BDD low, high;
        bdd_refs_spawn(SPAWN(sylvan_exists, aHigh, variables, level));
        low = CALL(sylvan_exists, aLow, variables, level);
        bdd_refs_push(low);
        high = bdd_refs_sync(SYNC(sylvan_exists));
        bdd_refs_pop(1);
        result = sylvan_makenode(level, low, high);
    }

    if (cachenow) {
        cache_put(BDD_SETDATA(a, CACHE_EXISTS), variables, 0, result);
    }

    return result;
}

/**
 * Calculate exists(a AND b, v)
 */
TASK_IMPL_4(BDD, sylvan_and_exists, BDD, a, BDD, b, BDDSET, v, BDDVAR, prev_level)
{
    /* Terminal cases */
    if (a == sylvan_false) return sylvan_false;
    if (b == sylvan_false) return sylvan_false;
    if (a == sylvan_not(b)) return sylvan_false;

    /* Cases that reduce to "exists" and "and" */
    if (a == sylvan_true) return CALL(sylvan_exists, b, v, 0);
    if (b == sylvan_true) return CALL(sylvan_exists, a, v, 0);
    if (a == b) return CALL(sylvan_exists, a, v, 0);
    if (sylvan_set_isempty(v)) return sylvan_and(a, b);

    /* At this point, a and b are proper nodes, and v is non-empty */

    /* Improve for caching */
    if (BDD_STRIPMARK(a) > BDD_STRIPMARK(b)) {
        BDD t = b;
        b = a;
        a = t;
    }

    /* Maybe perform garbage collection */
    sylvan_gc_test();

    sylvan_stats_count(BDD_AND_EXISTS);

    // a != constant
    bddnode_t na = GETNODE(a);
    bddnode_t nb = GETNODE(b);
    bddnode_t nv = GETNODE(v);

    BDDVAR level = na->level < nb->level ? na->level : nb->level;

    /* Skip levels in v that are not in a and b */
    while (nv->level < level) {
        v = node_high(v, nv); // get next variable in conjunction
        if (sylvan_set_isempty(v)) return sylvan_and(a, b);
        nv = GETNODE(v);
    }

    BDD result;

    int cachenow = granularity < 2 || prev_level == 0 ? 1 : prev_level / granularity != level / granularity;
    if (cachenow) {
        if (cache_get(BDD_SETDATA(a, CACHE_AND_EXISTS), b, v, &result)) {
            sylvan_stats_count(BDD_AND_EXISTS_CACHED);
            return result;
        }
    }

    // Get cofactors
    BDD aLow, aHigh, bLow, bHigh;
    if (level == na->level) {
        aLow = node_low(a, na);
        aHigh = node_high(a, na);
    } else {
        aLow = a;
        aHigh = a;
    }
    if (level == nb->level) {
        bLow = node_low(b, nb);
        bHigh = node_high(b, nb);
    } else {
        bLow = b;
        bHigh = b;
    }

    if (nv->level == level) {
        // level is in variable set, perform abstraction
        BDD _v = node_high(v, nv);
        BDD low = CALL(sylvan_and_exists, aLow, bLow, _v, level);
        if (low == sylvan_true) {
            result = sylvan_true;
        } else {
            bdd_refs_push(low);
            BDD high = CALL(sylvan_and_exists, aHigh, bHigh, _v, level);
            if (high == sylvan_true) {
                result = sylvan_true;
                bdd_refs_pop(1);
            } else if (high == sylvan_false) {
                result = low;
                bdd_refs_pop(1);
            } else if (low == sylvan_false) {
                result = high;
                bdd_refs_pop(1);
            } else {
                bdd_refs_push(high);
                result = sylvan_or(low, high);
                bdd_refs_pop(2);
            }
        }
    } else {
        // level is not in variable set
        bdd_refs_spawn(SPAWN(sylvan_and_exists, aHigh, bHigh, v, level));
        BDD low = CALL(sylvan_and_exists, aLow, bLow, v, level);
        bdd_refs_push(low);
        BDD high = bdd_refs_sync(SYNC(sylvan_and_exists));
        bdd_refs_pop(1);
        result = sylvan_makenode(level, low, high);
    }

    if (cachenow) {
        cache_put(BDD_SETDATA(a, CACHE_AND_EXISTS), b, v, result);<commit_msg>bdd: improved sylvan_and_exists implementation<commit_after>/*
 * Copyright 2011-2014 Formal Methods and Tools, University of Twente
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *     http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */

#include <sylvan_config.h>

#include <assert.h>
#include <inttypes.h>
#include <math.h>
#include <pthread.h>
#include <stdint.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>

#include <atomics.h>
#include <avl.h>
#include <refs.h>
#include <sha2.h>
#include <sylvan.h>
#include <sylvan_common.h>

/**
 * Complement handling macros
 */
#define BDD_HASMARK(s)              (s&sylvan_complement?1:0)
#define BDD_TOGGLEMARK(s)           (s^sylvan_complement)
#define BDD_STRIPMARK(s)            (s&~sylvan_complement)
#define BDD_TRANSFERMARK(from, to)  (to ^ (from & sylvan_complement))
// Equal under mark
#define BDD_EQUALM(a, b)            ((((a)^(b))&(~sylvan_complement))==0)

static inline BDD BDD_SETDATA(BDD s, uint32_t data)
{
    return (s & 0x800000ffffffffff) | (((uint64_t)data & 0x7fffff)<<40);
}

typedef struct __attribute__((packed)) bddnode {
    uint64_t high     : 40;
    uint32_t level    : 24;
    uint64_t low      : 40;
    unsigned int data : 23;
    uint8_t comp      : 1;
} *bddnode_t; // 16 bytes

#define GETNODE(bdd) ((bddnode_t)llmsset_index_to_ptr(nodes, BDD_STRIPMARK(bdd)))

/**
 * Implementation of garbage collection.
 */

/* Recursively mark BDD nodes as 'in use' */
VOID_TASK_IMPL_1(sylvan_gc_mark_rec, BDD, bdd)
{
    if (bdd == sylvan_false || bdd == sylvan_true) return;

    if (llmsset_mark(nodes, bdd&0x000000ffffffffff)) {
        bddnode_t n = GETNODE(bdd);
        SPAWN(sylvan_gc_mark_rec, n->low);
        CALL(sylvan_gc_mark_rec, n->high);
        SYNC(sylvan_gc_mark_rec);
    }
}

/**
 * External references
 */

refs_table_t bdd_refs;
refs_table_t bdd_protected;
static int bdd_protected_created = 0;

BDD
sylvan_ref(BDD a)
{
    if (a == sylvan_false || a == sylvan_true) return a;
    refs_up(&bdd_refs, BDD_STRIPMARK(a));
    return a;
}

void
sylvan_deref(BDD a)
{
    if (a == sylvan_false || a == sylvan_true) return;
    refs_down(&bdd_refs, BDD_STRIPMARK(a));
}

void
sylvan_protect(BDD *a)
{
    if (!bdd_protected_created) {
        // In C++, sometimes sylvan_protect is called before Sylvan is initialized. Just create a table.
        protect_create(&bdd_protected, 4096);
        bdd_protected_created = 1;
    }
    protect_up(&bdd_protected, (size_t)a);
}

void
sylvan_unprotect(BDD *a)
{
    protect_down(&bdd_protected, (size_t)a);
}

size_t
sylvan_count_refs()
{
    return refs_count(&bdd_refs);
}

size_t
sylvan_count_protected()
{
    return protect_count(&bdd_protected);
}

/* Called during garbage collection */
VOID_TASK_0(sylvan_gc_mark_external_refs)
{
    // iterate through refs hash table, mark all found
    size_t count=0;
    uint64_t *it = refs_iter(&bdd_refs, 0, bdd_refs.refs_size);
    while (it != NULL) {
        BDD to_mark = refs_next(&bdd_refs, &it, bdd_refs.refs_size);
        SPAWN(sylvan_gc_mark_rec, to_mark);
        count++;
    }
    while (count--) {
        SYNC(sylvan_gc_mark_rec);
    }
}

VOID_TASK_0(sylvan_gc_mark_protected)
{
    // iterate through refs hash table, mark all found
    size_t count=0;
    uint64_t *it = protect_iter(&bdd_protected, 0, bdd_protected.refs_size);
    while (it != NULL) {
        BDD *to_mark = (BDD*)protect_next(&bdd_protected, &it, bdd_protected.refs_size);
        SPAWN(sylvan_gc_mark_rec, *to_mark);
        count++;
    }
    while (count--) {
        SYNC(sylvan_gc_mark_rec);
    }
}

/* Infrastructure for internal markings */
DECLARE_THREAD_LOCAL(bdd_refs_key, bdd_refs_internal_t);

VOID_TASK_0(bdd_refs_mark_task)
{
    LOCALIZE_THREAD_LOCAL(bdd_refs_key, bdd_refs_internal_t);
    size_t i, j=0;
    for (i=0; i<bdd_refs_key->r_count; i++) {
        if (j >= 40) {
            while (j--) SYNC(sylvan_gc_mark_rec);
            j=0;
        }
        SPAWN(sylvan_gc_mark_rec, bdd_refs_key->results[i]);
        j++;
    }
    for (i=0; i<bdd_refs_key->s_count; i++) {
        Task *t = bdd_refs_key->spawns[i];
        if (!TASK_IS_STOLEN(t)) break;
        if (TASK_IS_COMPLETED(t)) {
            if (j >= 40) {
                while (j--) SYNC(sylvan_gc_mark_rec);
                j=0;
            }
            SPAWN(sylvan_gc_mark_rec, *(BDD*)TASK_RESULT(t));
            j++;
        }
    }
    while (j--) SYNC(sylvan_gc_mark_rec);
}

VOID_TASK_0(bdd_refs_mark)
{
    TOGETHER(bdd_refs_mark_task);
}

VOID_TASK_0(bdd_refs_init_task)
{
    bdd_refs_internal_t s = (bdd_refs_internal_t)malloc(sizeof(struct bdd_refs_internal));
    s->r_size = 128;
    s->r_count = 0;
    s->s_size = 128;
    s->s_count = 0;
    s->results = (BDD*)malloc(sizeof(BDD) * 128);
    s->spawns = (Task**)malloc(sizeof(Task*) * 128);
    SET_THREAD_LOCAL(bdd_refs_key, s);
}

VOID_TASK_0(bdd_refs_init)
{
    INIT_THREAD_LOCAL(bdd_refs_key);
    TOGETHER(bdd_refs_init_task);
    sylvan_gc_add_mark(10, TASK(bdd_refs_mark));
}

/**
 * Initialize and quit functions
 */

static int granularity = 1; // default

static void
sylvan_quit_bdd()
{
    refs_free(&bdd_refs);
    if (bdd_protected_created) {
        protect_free(&bdd_protected);
        bdd_protected_created = 0;
    }
}

void
sylvan_init_bdd(int _granularity)
{
    sylvan_register_quit(sylvan_quit_bdd);
    sylvan_gc_add_mark(10, TASK(sylvan_gc_mark_external_refs));
    sylvan_gc_add_mark(10, TASK(sylvan_gc_mark_protected));

    granularity = _granularity;

    // Sanity check
    if (sizeof(struct bddnode) != 16) {
        fprintf(stderr, "Invalid size of bdd nodes: %ld\n", sizeof(struct bddnode));
        exit(1);
    }

    refs_create(&bdd_refs, 1024);
    if (!bdd_protected_created) {
        protect_create(&bdd_protected, 4096);
        bdd_protected_created = 1;
    }

    LACE_ME;
    CALL(bdd_refs_init);
}

/**
 * Core BDD operations
 */

BDD
sylvan_makenode(BDDVAR level, BDD low, BDD high)
{
    if (low == high) return low;

    // Normalization to keep canonicity
    // low will have no mark

    struct bddnode n;
    int mark;

    if (BDD_HASMARK(low)) {
        mark = 1;
        n = (struct bddnode){high, level, low, 0, (uint8_t)(BDD_HASMARK(high) ? 0 : 1)};
    } else {
        mark = 0;
        n = (struct bddnode){high, level, low, 0, (uint8_t)(BDD_HASMARK(high) ? 1 : 0)};
    }

    BDD result;
    int created;
    uint64_t index = llmsset_lookup(nodes, &n, &created);
    if (index == 0) {
        LACE_ME;

        //size_t before_gc = llmsset_count_marked(nodes);
        bdd_refs_push(low);
        bdd_refs_push(high);
        sylvan_gc();
        bdd_refs_pop(2);
        //size_t after_gc = llmsset_count_marked(nodes);
        //size_t total = llmsset_get_size(nodes);
        //fprintf(stderr, "GC: %.01f%% to %.01f%%\n", 100.0*(double)before_gc/total, 100.0*(double)after_gc/total);

        index = llmsset_lookup(nodes, &n, &created);
        if (index == 0) {
            fprintf(stderr, "BDD Unique table full, %zu of %zu buckets filled!\n", llmsset_count_marked(nodes), llmsset_get_size(nodes));
            exit(1);
        }
    }

    if (created) sylvan_stats_count(BDD_NODES_CREATED);
    else sylvan_stats_count(BDD_NODES_REUSED);

    result = index;
    return mark ? result | sylvan_complement : result;
}

BDD
sylvan_ithvar(BDDVAR level)
{
    return sylvan_makenode(level, sylvan_false, sylvan_true);
}

BDDVAR
sylvan_var(BDD bdd)
{
    if (bdd == sylvan_false || bdd == sylvan_true) bdd = sylvan_invalid; // force crash
    return GETNODE(bdd)->level;
}

static inline BDD
node_lowedge(bddnode_t node)
{
    return node->low;
}

static inline BDD
node_highedge(bddnode_t node)
{
    return node->high | (node->comp ? sylvan_complement : 0LL);
}

static inline BDD
node_low(BDD bdd, bddnode_t node)
{
    return BDD_TRANSFERMARK(bdd, node_lowedge(node));
}

static inline BDD
node_high(BDD bdd, bddnode_t node)
{
    return BDD_TRANSFERMARK(bdd, node_highedge(node));
}

BDD
sylvan_low(BDD bdd)
{
    if (sylvan_isconst(bdd)) return bdd;
    return node_low(bdd, GETNODE(bdd));
}

BDD
sylvan_high(BDD bdd)
{
    if (sylvan_isconst(bdd)) return bdd;
    return node_high(bdd, GETNODE(bdd));
}

/**
 * Debugging functionality that converts a BDD to one without complemented edges.
 */

BDD
sylvan_makenode_nocomp(BDDVAR level, BDD low, BDD high)
{
    if (low == high) return low;

    struct bddnode n = (struct bddnode){high, level, low, 0, 0};

    int created;
    uint64_t index = llmsset_lookup(nodes, &n, &created);
    if (index == 0) {
        LACE_ME;
        bdd_refs_push(low);
        bdd_refs_push(high);
        sylvan_gc();
        bdd_refs_pop(2);
        index = llmsset_lookup(nodes, &n, &created);
        if (index == 0) {
            fprintf(stderr, "BDD Unique table full, %zu of %zu buckets filled!\n", llmsset_count_marked(nodes), llmsset_get_size(nodes));
            exit(1);
        }
    }

    return (BDD)index;
}

BDD
sylvan_bdd_to_nocomp(BDD bdd)
{
    if (bdd == sylvan_true) return sylvan_true_nc;
    if (bdd == sylvan_false) return sylvan_false;

    bddnode_t n = GETNODE(bdd);
    return sylvan_makenode_nocomp(n->level, sylvan_bdd_to_nocomp(node_low(bdd, n)), sylvan_bdd_to_nocomp(node_high(bdd, n)));
}

/**
 * Implementation of unary, binary and if-then-else operators.
 */
TASK_IMPL_3(BDD, sylvan_and, BDD, a, BDD, b, BDDVAR, prev_level)
{
    /* Terminal cases */
    if (a == sylvan_true) return b;
    if (b == sylvan_true) return a;
    if (a == sylvan_false) return sylvan_false;
    if (b == sylvan_false) return sylvan_false;

    sylvan_gc_test();

    sylvan_stats_count(BDD_AND);

    /* Improve for caching */
    if (BDD_STRIPMARK(a) > BDD_STRIPMARK(b)) {
        BDD t = b;
        b = a;
        a = t;
    }

    bddnode_t na = GETNODE(a);
    bddnode_t nb = GETNODE(b);

    BDDVAR level = na->level < nb->level ? na->level : nb->level;

    int cachenow = granularity < 2 || prev_level == 0 ? 1 : prev_level / granularity != level / granularity;
    if (cachenow) {
        BDD result;
        if (cache_get(BDD_SETDATA(a, CACHE_AND), b, sylvan_false, &result)) {
            sylvan_stats_count(BDD_AND_CACHED);
            return result;
        }
    }

    // Get cofactors
    BDD aLow = a, aHigh = a;
    BDD bLow = b, bHigh = b;
    if (level == na->level) {
        aLow = node_low(a, na);
        aHigh = node_high(a, na);
    }
    if (level == nb->level) {
        bLow = node_low(b, nb);
        bHigh = node_high(b, nb);
    }

    // Recursive computation
    BDD low=sylvan_invalid, high=sylvan_invalid, result;

    int n=0;

    if (aHigh == sylvan_true) {
        high = bHigh;
    } else if (aHigh == sylvan_false || bHigh == sylvan_false) {
        high = sylvan_false;
    } else if (bHigh == sylvan_true) {
        high = aHigh;
    } else {
        bdd_refs_spawn(SPAWN(sylvan_and, aHigh, bHigh, level));
        n=1;
    }

    if (aLow == sylvan_true) {
        low = bLow;
    } else if (aLow == sylvan_false || bLow == sylvan_false) {
        low = sylvan_false;
    } else if (bLow == sylvan_true) {
        low = aLow;
    } else {
        low = CALL(sylvan_and, aLow, bLow, level);
    }

    if (n) {
        bdd_refs_push(low);
        high = bdd_refs_sync(SYNC(sylvan_and));
        bdd_refs_pop(1);
    }

    result = sylvan_makenode(level, low, high);

    if (cachenow) {
        cache_put(BDD_SETDATA(a, CACHE_AND), b, sylvan_false, result);
    }

    return result;
}

TASK_IMPL_3(BDD, sylvan_xor, BDD, a, BDD, b, BDDVAR, prev_level)
{
    /* Terminal cases */
    if (a == sylvan_false) return b;
    if (b == sylvan_false) return a;
    if (a == sylvan_true) return sylvan_not(b);
    if (b == sylvan_true) return sylvan_not(a);
    if (a == b) return sylvan_false;
    if (a == sylvan_not(b)) return sylvan_true;

    sylvan_gc_test();

    sylvan_stats_count(BDD_XOR);

    /* Improve for caching */
    if (BDD_STRIPMARK(a) > BDD_STRIPMARK(b)) {
        BDD t = b;
        b = a;
        a = t;
    }

    // XOR(~A,B) => XOR(A,~B)
    if (BDD_HASMARK(a)) {
        a = BDD_STRIPMARK(a);
        b = sylvan_not(b);
    }

    bddnode_t na = GETNODE(a);
    bddnode_t nb = GETNODE(b);

    BDDVAR level = na->level < nb->level ? na->level : nb->level;

    int cachenow = granularity < 2 || prev_level == 0 ? 1 : prev_level / granularity != level / granularity;
    if (cachenow) {
        BDD result;
        if (cache_get(BDD_SETDATA(a, CACHE_XOR), b, sylvan_false, &result)) {
            sylvan_stats_count(BDD_XOR_CACHED);
            return result;
        }
    }

    // Get cofactors
    BDD aLow = a, aHigh = a;
    BDD bLow = b, bHigh = b;
    if (level == na->level) {
        aLow = node_low(a, na);
        aHigh = node_high(a, na);
    }
    if (level == nb->level) {
        bLow = node_low(b, nb);
        bHigh = node_high(b, nb);
    }

    // Recursive computation
    BDD low, high, result;

    bdd_refs_spawn(SPAWN(sylvan_xor, aHigh, bHigh, level));
    low = CALL(sylvan_xor, aLow, bLow, level);
    bdd_refs_push(low);
    high = bdd_refs_sync(SYNC(sylvan_xor));
    bdd_refs_pop(1);

    result = sylvan_makenode(level, low, high);

    if (cachenow) {
        cache_put(BDD_SETDATA(a, CACHE_XOR), b, sylvan_false, result);
    }

    return result;
}


TASK_IMPL_4(BDD, sylvan_ite, BDD, a, BDD, b, BDD, c, BDDVAR, prev_level)
{
    /* Terminal cases */
    if (a == sylvan_true) return b;
    if (a == sylvan_false) return c;
    if (a == b) b = sylvan_true;
    if (a == sylvan_not(b)) b = sylvan_false;
    if (a == c) c = sylvan_false;
    if (a == sylvan_not(c)) c = sylvan_true;
    if (b == c) return b;
    if (b == sylvan_true && c == sylvan_false) return a;
    if (b == sylvan_false && c == sylvan_true) return sylvan_not(a);

    /* Cases that reduce to AND and XOR */

    // ITE(A,B,0) => AND(A,B)
    if (c == sylvan_false) return CALL(sylvan_and, a, b, prev_level);

    // ITE(A,1,C) => ~AND(~A,~C)
    if (b == sylvan_true) return sylvan_not(CALL(sylvan_and, sylvan_not(a), sylvan_not(c), prev_level));

    // ITE(A,0,C) => AND(~A,C)
    if (b == sylvan_false) return CALL(sylvan_and, sylvan_not(a), c, prev_level);

    // ITE(A,B,1) => ~AND(A,~B)
    if (c == sylvan_true) return sylvan_not(CALL(sylvan_and, a, sylvan_not(b), prev_level));

    // ITE(A,B,~B) => XOR(A,~B)
    if (b == sylvan_not(c)) return CALL(sylvan_xor, a, c, 0);

    /* At this point, there are no more terminals */

    /* Canonical for optimal cache use */

    // ITE(~A,B,C) => ITE(A,C,B)
    if (BDD_HASMARK(a)) {
        a = BDD_STRIPMARK(a);
        BDD t = c;
        c = b;
        b = t;
    }

    // ITE(A,~B,C) => ~ITE(A,B,~C)
    int mark = 0;
    if (BDD_HASMARK(b)) {
        b = sylvan_not(b);
        c = sylvan_not(c);
        mark = 1;
    }

    sylvan_gc_test();

    sylvan_stats_count(BDD_ITE);

    bddnode_t na = GETNODE(a);
    bddnode_t nb = GETNODE(b);
    bddnode_t nc = GETNODE(c);

    // Get lowest level
    BDDVAR level = nb->level < nc->level ? nb->level : nc->level;

    // Fast case
    if (na->level < level && node_low(a, na) == sylvan_false && node_high(a, na) == sylvan_true) {
        BDD result = sylvan_makenode(na->level, c, b);
        return mark ? sylvan_not(result) : result;
    }

    if (na->level < level) level = na->level;

    int cachenow = granularity < 2 || prev_level == 0 ? 1 : prev_level / granularity != level / granularity;
    if (cachenow) {
        BDD result;
        if (cache_get(BDD_SETDATA(a, CACHE_ITE), b, c, &result)) {
            sylvan_stats_count(BDD_ITE_CACHED);
            return mark ? sylvan_not(result) : result;
        }
    }

    // Get cofactors
    BDD aLow = a, aHigh = a;
    BDD bLow = b, bHigh = b;
    BDD cLow = c, cHigh = c;
    if (level == na->level) {
        aLow = node_low(a, na);
        aHigh = node_high(a, na);
    }
    if (level == nb->level) {
        bLow = node_low(b, nb);
        bHigh = node_high(b, nb);
    }
    if (level == nc->level) {
        cLow = node_low(c, nc);
        cHigh = node_high(c, nc);
    }

    // Recursive computation
    BDD low=sylvan_invalid, high=sylvan_invalid, result;

    int n=0;

    if (aHigh == sylvan_true) {
        high = bHigh;
    } else if (aHigh == sylvan_false) {
        high = cHigh;
    } else {
        bdd_refs_spawn(SPAWN(sylvan_ite, aHigh, bHigh, cHigh, level));
        n=1;
    }

    if (aLow == sylvan_true) {
        low = bLow;
    } else if (aLow == sylvan_false) {
        low = cLow;
    } else {
        low = CALL(sylvan_ite, aLow, bLow, cLow, level);
    }

    if (n) {
        bdd_refs_push(low);
        high = bdd_refs_sync(SYNC(sylvan_ite));
        bdd_refs_pop(1);
    }

    result = sylvan_makenode(level, low, high);

    if (cachenow) {
        cache_put(BDD_SETDATA(a, CACHE_ITE), b, c, result);
    }

    return mark ? sylvan_not(result) : result;
}

/**
 * Calculate constrain a @ c
 */
TASK_IMPL_3(BDD, sylvan_constrain, BDD, a, BDD, b, BDDVAR, prev_level)
{
    /* Trivial cases */
    if (b == sylvan_true) return a;
    if (b == sylvan_false) return sylvan_false;
    if (sylvan_isconst(a)) return a;
    if (a == b) return sylvan_true;
    if (a == sylvan_not(b)) return sylvan_false;

    /* Perhaps execute garbage collection */
    sylvan_gc_test();

    /* Count operation */
    sylvan_stats_count(BDD_CONSTRAIN);

    // a != constant and b != constant
    bddnode_t na = GETNODE(a);
    bddnode_t nb = GETNODE(b);

    BDDVAR level = na->level < nb->level ? na->level : nb->level;

    // CONSULT CACHE

    int cachenow = granularity < 2 || prev_level == 0 ? 1 : prev_level / granularity != level / granularity;
    if (cachenow) {
        BDD result;
        if (cache_get(BDD_SETDATA(a, CACHE_CONSTRAIN), b, 0, &result)) {
            sylvan_stats_count(BDD_CONSTRAIN_CACHED);
            return result;
        }
    }

    // DETERMINE TOP BDDVAR AND COFACTORS

    BDD aLow, aHigh, bLow, bHigh;

    if (na->level == level) {
        aLow = node_low(a, na);
        aHigh = node_high(a, na);
    } else {
        aLow = aHigh = a;
    }

    if (nb->level == level) {
        bLow = node_low(b, nb);
        bHigh = node_high(b, nb);
    } else {
        bLow = bHigh = b;
    }

    BDD result;

    BDD low=sylvan_invalid, high=sylvan_invalid;
    if (bLow == sylvan_false) return CALL(sylvan_constrain, aHigh, bHigh, level);
    if (bLow == sylvan_true) {
        if (bHigh == sylvan_false) return aLow;
        if (bHigh == sylvan_true) {
            result = sylvan_makenode(level, aLow, bHigh);
        } else {
            high = CALL(sylvan_constrain, aHigh, bHigh, level);
            result = sylvan_makenode(level, aLow, high);
        }
    } else {
        if (bHigh == sylvan_false) return CALL(sylvan_constrain, aLow, bLow, level);
        if (bHigh == sylvan_true) {
            low = CALL(sylvan_constrain, aLow, bLow, level);
            result = sylvan_makenode(level, low, bHigh);
        } else {
            bdd_refs_spawn(SPAWN(sylvan_constrain, aLow, bLow, level));
            high = CALL(sylvan_constrain, aHigh, bHigh, level);
            bdd_refs_push(high);
            low = bdd_refs_sync(SYNC(sylvan_constrain));
            bdd_refs_pop(1);
            result = sylvan_makenode(level, low, high);
        }
    }

    if (cachenow) {
        cache_put(BDD_SETDATA(a, CACHE_CONSTRAIN), b, 0, result);
    }

    return result;
}

/**
 * Calculate restrict a @ b
 */
TASK_IMPL_3(BDD, sylvan_restrict, BDD, a, BDD, b, BDDVAR, prev_level)
{
    /* Trivial cases */
    if (b == sylvan_true) return a;
    if (b == sylvan_false) return sylvan_false;
    if (sylvan_isconst(a)) return a;
    if (a == b) return sylvan_true;
    if (a == sylvan_not(b)) return sylvan_false;

    /* Perhaps execute garbage collection */
    sylvan_gc_test();

    /* Count operation */
    sylvan_stats_count(BDD_RESTRICT);

    // a != constant and b != constant
    bddnode_t na = GETNODE(a);
    bddnode_t nb = GETNODE(b);

    BDDVAR level = na->level < nb->level ? na->level : nb->level;

    /* Consult cache */
    int cachenow = granularity < 2 || prev_level == 0 ? 1 : prev_level / granularity != level / granularity;
    if (cachenow) {
        BDD result;
        if (cache_get(BDD_SETDATA(a, CACHE_RESTRICT), b, 0, &result)) {
            sylvan_stats_count(BDD_RESTRICT_CACHED);
            return result;
        }
    }

    BDD result;

    if (nb->level < na->level) {
        BDD c = CALL(sylvan_ite, node_low(b,nb), sylvan_true, node_high(b,nb), 0);
        bdd_refs_push(c);
        result = CALL(sylvan_restrict, a, c, level);
        bdd_refs_pop(1);
    } else {
        BDD aLow=node_low(a,na),aHigh=node_high(a,na),bLow=b,bHigh=b;
        if (na->level == nb->level) {
            bLow = node_low(b,nb);
            bHigh = node_high(b,nb);
        }
        if (bLow == sylvan_false) {
            result = CALL(sylvan_restrict, aHigh, bHigh, level);
        } else if (bHigh == sylvan_false) {
            result = CALL(sylvan_restrict, aLow, bLow, level);
        } else {
            bdd_refs_spawn(SPAWN(sylvan_restrict, aLow, bLow, level));
            BDD high = CALL(sylvan_restrict, aHigh, bHigh, level);
            bdd_refs_push(high);
            BDD low = bdd_refs_sync(SYNC(sylvan_restrict));
            bdd_refs_pop(1);
            result = sylvan_makenode(level, low, high);
        }
    }

    if (cachenow) {
        cache_put(BDD_SETDATA(a, CACHE_RESTRICT), b, 0, result);
    }

    return result;
}

/**
 * Calculates \exists variables . a
 */
TASK_IMPL_3(BDD, sylvan_exists, BDD, a, BDD, variables, BDDVAR, prev_level)
{
    /* Terminal cases */
    if (a == sylvan_true) return sylvan_true;
    if (a == sylvan_false) return sylvan_false;
    if (sylvan_set_isempty(variables)) return a;

    sylvan_gc_test();

    sylvan_stats_count(BDD_EXISTS);

    // a != constant
    bddnode_t na = GETNODE(a);
    BDDVAR level = na->level;

    // Get cofactors
    BDD aLow = node_low(a, na);
    BDD aHigh = node_high(a, na);

    while (!sylvan_set_isempty(variables) && sylvan_var(variables) < level) {
        // Skip variables before x
        variables = sylvan_set_next(variables);
    }

    if (sylvan_set_isempty(variables)) return a; // nothing to quantify

    int cachenow = granularity < 2 || prev_level == 0 ? 1 : prev_level / granularity != level / granularity;
    if (cachenow) {
        BDD result;
        if (cache_get(BDD_SETDATA(a, CACHE_EXISTS), variables, 0, &result)) {
            sylvan_stats_count(BDD_EXISTS_CACHED);
            return result;
        }
    }

    BDD result;

    if (sylvan_set_var(variables) == level) {
        // level is in variable set, perform abstraction
        variables = sylvan_set_next(variables);
        BDD low = CALL(sylvan_exists, aLow, variables, level);
        if (low == sylvan_true) {
            result = sylvan_true;
        } else {
            bdd_refs_push(low);
            BDD high = CALL(sylvan_exists, aHigh, variables, level);
            if (high == sylvan_true) {
                result = sylvan_true;
                bdd_refs_pop(1);
            } else if (low == sylvan_false && high == sylvan_false) {
                result = sylvan_false;
                bdd_refs_pop(1);
            } else {
                bdd_refs_push(high);
                result = CALL(sylvan_ite, low, sylvan_true, high, 0); // or
                bdd_refs_pop(2);
            }
        }
    } else {
        // level is not in variable set
        BDD low, high;
        bdd_refs_spawn(SPAWN(sylvan_exists, aHigh, variables, level));
        low = CALL(sylvan_exists, aLow, variables, level);
        bdd_refs_push(low);
        high = bdd_refs_sync(SYNC(sylvan_exists));
        bdd_refs_pop(1);
        result = sylvan_makenode(level, low, high);
    }

    if (cachenow) {
        cache_put(BDD_SETDATA(a, CACHE_EXISTS), variables, 0, result);
    }

    return result;
}

/**
 * Calculate exists(a AND b, v)
 */
TASK_IMPL_4(BDD, sylvan_and_exists, BDD, a, BDD, b, BDDSET, v, BDDVAR, prev_level)
{
    /* Terminal cases */
    if (a == sylvan_false) return sylvan_false;
    if (b == sylvan_false) return sylvan_false;
    if (a == sylvan_not(b)) return sylvan_false;
    if (a == sylvan_true && b == sylvan_true) return sylvan_true;

    /* Cases that reduce to "exists" and "and" */
    if (a == sylvan_true) return CALL(sylvan_exists, b, v, 0);
    if (b == sylvan_true) return CALL(sylvan_exists, a, v, 0);
    if (a == b) return CALL(sylvan_exists, a, v, 0);
    if (sylvan_set_isempty(v)) return sylvan_and(a, b);

    /* At this point, a and b are proper nodes, and v is non-empty */

    /* Improve for caching */
    if (BDD_STRIPMARK(a) > BDD_STRIPMARK(b)) {
        BDD t = b;
        b = a;
        a = t;
    }

    /* Maybe perform garbage collection */
    sylvan_gc_test();

    sylvan_stats_count(BDD_AND_EXISTS);

    // a != constant
    bddnode_t na = GETNODE(a);
    bddnode_t nb = GETNODE(b);
    bddnode_t nv = GETNODE(v);

    BDDVAR level = na->level < nb->level ? na->level : nb->level;

    /* Skip levels in v that are not in a and b */
    while (nv->level < level) {
        v = node_high(v, nv); // get next variable in conjunction
        if (sylvan_set_isempty(v)) return sylvan_and(a, b);
        nv = GETNODE(v);
    }

    BDD result;

    int cachenow = granularity < 2 || prev_level == 0 ? 1 : prev_level / granularity != level / granularity;
    if (cachenow) {
        if (cache_get(BDD_SETDATA(a, CACHE_AND_EXISTS), b, v, &result)) {
            sylvan_stats_count(BDD_AND_EXISTS_CACHED);
            return result;
        }
    }

    // Get cofactors
    BDD aLow, aHigh, bLow, bHigh;
    if (level == na->level) {
        aLow = node_low(a, na);
        aHigh = node_high(a, na);
    } else {
        aLow = a;
        aHigh = a;
    }
    if (level == nb->level) {
        bLow = node_low(b, nb);
        bHigh = node_high(b, nb);
    } else {
        bLow = b;
        bHigh = b;
    }

    if (nv->level == level) {
        // level is in variable set, perform abstraction
        BDD _v = node_high(v, nv);
        BDD low = CALL(sylvan_and_exists, aLow, bLow, _v, level);
        if (low == sylvan_true || low == aHigh || low == bHigh) {
            result = low;
        } else {
            bdd_refs_push(low);
            BDD high;
            if (low == sylvan_not(aHigh)) {
                high = CALL(sylvan_exists, bHigh, _v, 0);
            } else if (low == sylvan_not(bHigh)) {
                high = CALL(sylvan_exists, aHigh, _v, 0);
            } else {
                high = CALL(sylvan_and_exists, aHigh, bHigh, _v, level);
            }
            if (high == sylvan_true) {
                result = sylvan_true;
                bdd_refs_pop(1);
            } else if (high == sylvan_false) {
                result = low;
                bdd_refs_pop(1);
            } else if (low == sylvan_false) {
                result = high;
                bdd_refs_pop(1);
            } else {
                bdd_refs_push(high);
                result = sylvan_or(low, high);
                bdd_refs_pop(2);
            }
        }
    } else {
        // level is not in variable set
        bdd_refs_spawn(SPAWN(sylvan_and_exists, aHigh, bHigh, v, level));
        BDD low = CALL(sylvan_and_exists, aLow, bLow, v, level);
        bdd_refs_push(low);
        BDD high = bdd_refs_sync(SYNC(sylvan_and_exists));
        bdd_refs_pop(1);
        result = sylvan_makenode(level, low, high);
    }

    if (cachenow) {
        cache_put(BDD_SETDATA(a, CACHE_AND_EXISTS), b, v, result);
{'fraction_non_alphanumeric': 0.13028352133134874, 'fraction_numerical': 0.007998134964044258, 'mean_word_length': 2.4907042253521126, 'pattern_counts': {'":': 0, '<': 77, '<?xml version=': 0, '>': 185, 'https://': 0, 'lorem ipsum': 0, 'www.': 2, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 4, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2175816', 'n_tokens_mistral': 22554, 'n_tokens_neox': 21384, 'n_words': 4678}