Skip to content

v1.2
Compare
Choose a tag to compare
@jurajsic jurajsic released this 09 Apr 22:22
· 40 commits to master since this release
v1.2
bc27c41

This release updates the localisation algorithm to save memory/time and also fixes the problems with using copies of variables with the same name for localisation of existential quantifiers. Furthermore, this release can be compiled and run on Mac systems. It also uses newer version of HQSpre (the one packaged with the version of HQS from 18-03-2021). Finally, it adds support for prenex cleansed DQCIR format with a possibility to write the output of HQSpre preprocessing to DQCIR file.

Fixes

  • added checks in DQDIMACS parser for errors and fixed parsing of free variables
  • some solved instances by HQSpre during parsing were not caught, leading to a thrown exception
  • the copies of universal variables (which DQBDD does not rename) will now not be taken into account for computing the conditions of pushing existential variables for disjunction

New

  • added parser for QBFs in prenex cleansed (D)QCIR format (prenex DQCIR is like prenex QCIR, where we can add quantifier depend(v, v1, ..., vn) which represents existential variable v with dependency set {v1, ..., vn})
  • added an option to force file format (otherwise it is selected automatically by file type)
  • DQBDD now works also on Mac
  • changed how localisation is computed to save on memory/time
  • added option '--hqspre-dqcir-output' which takes filename.dqdimacs file, preprocesses it with HQSpre and transforms the result (with gate extraction) into filename.dqcir
Assets 4
Loading