Module Dpll

module Dpll: sig .. end

A term-level DPLL solver.

A term level interface to a DPLL solver. The implementation uses a form of multi-input and-inverter graphs internally as a semi-canonical term representation. More information about and-inverter graph schemes can be found in the following papers:

Andreas Kuehlmann, Viresh Paruthi, Florian Krohm, Malay K. Ganai. Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 21(12):1377-1394, 2002.
Per Bjesse, Arne Boralv. DAG-aware circuit compression for formal verification. Computer Aided Design: Proceedings of the IEEE/ACM International Conference, pp 42-49, 2004.

class make : unit -> Solver_api.dpll

Hosted by the

^* web site.
^*Other names and brands may be claimed as the property of others.