Module Solver_api

module Solver_api: sig .. end

Term level interface specifications.

General term level interfaces to DPLL and theory solvers for use with combination schemes. The interfaces are essentially in the style of the following paper

Sava Krstic, Amit Goel. Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL. Lecture Notes in Computer Science 4720:1-27, 2007.

class type dpll = object .. end

Term level interface to a DPLL solver.

class type theory = object .. end

Term level interface to all theory solvers.

class type solver = object .. end

The interface for a solver.

Hosted by the

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