• Alexandre Duret-Lutz's avatar
    * rsc/bdd.h (bdd_existcomp, bdd_forallcomp, · 4bf6c52b
    Alexandre Duret-Lutz authored
    bdd_uniquecomp, bdd_appexcomp, bdd_appallcomp,
    bdd_appunicomp): Declare for C and C++.
    * src/bddop.c (CACHEID_EXISTC, CACHEID_FORALLC,
    CACHEID_UNIQUEC, CACHEID_APPEXC, CACHEID_APPALC,
    CACHEID_APPUNCC): New macros.
    (quatvarsetcomp): New variables.
    (varset2vartable): Take a second argument to indicate negation,
    set quatvarsetcomp.
    (INVARSET): Honor quatvarsetcomp.
    (quantify): New function, extracted from bdd_exist, bdd_forall,
    and bdd_appunicomp.
    (bdd_exist, bdd_forall, bdd_appunicomp): Use quantify.
    (bdd_existcomp, bdd_forallcomp, bdd_appunicompcomp): New functions.
    (appquantify): New function, extracted from bdd_appex, bdd_appall,
    and bdd_appuni.
    (bdd_appex, bdd_appall, bdd_appuni): Use appquantify.
    (bdd_appexcomp, bdd_appallcomp, bdd_appunicomp): New functions.
    
    * src/bddop.c (bdd_support): Return bddtrue when the support
    is empty, because variable sets are conjunctions.
    4bf6c52b
To find the state of this project's repository at the time of any of these versions, check out the tags.