module Solver_dpllt: sig .. end
A DPLL(T) solver.
This module implements a DPLL(T) style scheme for combining a DPLL
solver with a theory solver. The combination scheme is described
in the following papers.
- Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert
Oliveras, Cesare Tinelli.
DPLL(T): Fast decision procedures. Lecture Notes in
Computer Science 3114:175-188, 2004.
- Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli.
Solving SAT and
SAT modulo theories: From an abstract
Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM 53(6):937-977, 2006.
- Sava Krsic, Amit Goel.
Architecting
Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL. Lecture Notes in Computer Science 4720:1-27, 2007.
class make : Solver_api.dpll -> Solver_api.theory -> Solver_api.solver
Hosted by the
* web site.
*Other names and brands may be claimed as the property
of others.