module Solver: sig .. end
Solver for checking if formulas hold on structures.
Interface
module M: sig .. end
Interface to the solver.
val register_dnf_param : int Pervasives.ref
Parameter for dnf conversion in registration. Change to 1 in case of problems.
val eval_counter : int Pervasives.ref
Counter of internal formula evaluations for profiling.
val clear_cache : unit -> unit
Clear cache.
val so_to_qbf : ?ids:(string * int array, int) Hashtbl.t ->
?rev_ids:(int, string * int array) Hashtbl.t ->
?assigned:(Formula.var * int) list ->
Structure.structure ->
Formula.formula ->
QBF.qbf * (string * int array, int) Hashtbl.t *
(int, string * int array) Hashtbl.t
Compute the QBF equivalent to the given SO formula on the given structure.
val find_so : ?maximize:bool ->
?logtime:float ->
?logprefix:string ->
?tnf:bool ->
Structure.structure -> Formula.formula -> Structure.structure * bool
Find assignment for second-order variables and add it to the structure.
val add_def_rels : Structure.structure ->
(string * string list * Formula.formula) list -> Structure.structure
Add defined relations to a structure.
val add_def_funs : Structure.structure ->
(string * string * Formula.real_expr) list -> Structure.structure
Add defined functions to a structure.