Skip to content

Add early-return for bdd_exists and bdd_forall #11

Description

@ssoelvsten

Consider the following piece of code in quant_rec (buddy/src/bddop.c)

   PUSHREF( quant_rec(LOW(r)) );
   PUSHREF( quant_rec(HIGH(r)) );
   
   if (INVARSET(LEVEL(r)))
      res = apply_rec(READREF(2), READREF(1));
   else
      res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));

We can entirely circumvent the quant_rec(HIGH(r)) if

  1. The quant_rec(LOW(r)) returned a terminal that shortcuts the given operator (see the base cases for apply_rec in the same folder for how to do so).
  2. INVARSET(LEVEL(r)) is true

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions