package qbf

  1. Overview
  2. Docs

Bindings to Quantor

type lit = Qbf.Lit.t

Direct Bindings

module Raw : sig ... end

Solver

let cnf = Qbf.CNF.exists [1; 2] (Qbf.CNF.cnf [[1; ~-2]; [2; ~-3]]);;
Quantor.solve cnf;;
val solve : Qbf.QCNF.t -> Qbf.result
val solver : Qbf.solver