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.