Module Reduction

module Reduction: sig .. end
Reductions between structure classes and SO queries.

type reduction = {
   rels :(string * string list * Formula.formula) list;
   consts :(string * (int, string) Aux.choice) list;
}
Reduction with definitions for relations and constants.
val str : reduction -> string
Print a reduction
val parse_reduct : string -> reduction
Parse a reduction.
val find_example : ?timelog:bool -> int -> Formula.formula -> Structure.structure * bool
Find an example structure of a given size for a formula.
val check_reduct : ?maximize:bool ->
?log:bool ->
?xy:bool ->
?consts:bool ->
Formula.formula ->
Formula.formula ->
reduction -> size:int -> int -> Structure.structure option * bool
Check if reduct is a correct reduction of dimention dim from class defined by cfrom to one given by cto, on structures of size size.
val find_reduct : ?log:bool ->
int ->
Formula.formula ->
Formula.formula ->
size:int -> dim:int -> ?fp:bool -> int * int -> reduction option
Find reduction from cfrom to cto of dimension dim, correct upto size size and with at most nbr_cl clauses.
val find_reduct_iter : ?log:bool ->
int ->
Formula.formula ->
Formula.formula ->
smin:int ->
smax:int ->
dim:int ->
?fp:bool -> ?stepwise:bool -> int * int -> reduction option
Find reduction iterating on counter-examples. If smin < smax then make sure to set -max and -nbrs in syntax to false and -dim to one.
val find_reduct_iter_start : ?log:bool ->
int ->
Formula.formula ->
Formula.formula ->
smin:int -> smax:int -> dim:int -> ?fp:bool -> int * int -> unit
Find reduction iterating on counter-exaples as above - start
val find_reduct_iter_step : ?log:bool ->
int ->
int ->
Formula.formula ->
Formula.formula -> int -> reduction option * bool
Find reduction iterating on counter-exaples as above - step
val find_reduct_iter_counterexample : unit -> Structure.structure
Return the current counterexample structure.
val print_reduct_find : fmt:int ->
?fn:string ->
?log:bool ->
int ->
Formula.formula ->
Formula.formula ->
size:int * int -> dim:int -> ?fp:bool -> ?expand:int -> int * int -> string
Print reduction-finding condition in qpro (fmt=0), lp (fmt=1),or qdimacs. All other options as in find_reduct, but now we only print it out.