Skip to content

#1199 CIF/BDD: Improve performance of BddUtils.getVarDomain + avoid using BDDDomain.ithVar in it

  • Best to review per commit.
  • End-user visible changes:
    • The CIF data-based synthesis tool now more efficiently creates certain predicates for variables with many possible values, namely initial value predicates for discrete variables initialized using in any, update relation predicates for input variables, and implicit variable-never-out-of-range requirements.
    • The CIF controller properties checker, for BDD-based checks, now more efficiently creates certain predicates for variables with many possible values, namely initial value predicates for discrete variables initialized using in any, and update relation predicates for input variables.
  • Detailed/other changes:
    • BddUtils.getVarDomain has been optimized, deferring its work to either BddUtils.getVarDomainByDisjunction or BddUtils.getVarDomainByComparison. The latter is new.
    • BddUtils.getVarDomainByDisjunction has some code improvements.
    • BddUtils.getVarDomain* methods have improved JavaDocs.
    • BddUtils.getVarValue method added to replace BDDDomain.ithVar. This is in preparation for other changes in #458 (closed).
  • Note that CIF/BDD variables don't yet support negative values, and neither do BddUtils.getVarDomain* and BddUtils.getVarValue methods. That is to be done as a next step in #458 (closed).

Closes #1199 (closed)

Edited by Dennis Hendriks

Merge request reports

Loading