Module Finite_domain (.ml)

module Finite_domain: sig .. end

finite domain model finding

see the paper Computing Finite Models by Reduction to Function-Free Clause Logic by Peter Baumgartner, Alexander Fuchs, Hans de Neville, Cesare Tinelli.

Types

type symbol = Symbol.symbol

type term = Term.term

type clause = Term.clause

type problem = Problem.problem

type arities = Problem.arities

type sorts = Sort_inference.sorts

type finite_domain

finite domain data type

Functions

val create : print_transformation:bool ->
       print_sorts:bool -> problem -> finite_domain

create print problem domain_size creates a finite domain representation based on problem, and infers the problem sorts.

prints the flattened clause set if print_transformation is true.

prints the sorts if print_sorts is true.

val get_problem : finite_domain -> problem

returns the original problem.

val get_flattened : finite_domain -> problem

returns the flattened problem.

val get_sorts : finite_domain -> sorts

returns the sorts of the problem.

val get_axioms : print:bool ->
       print_tptp:bool ->
       use_functionality_axioms:bool ->
       finite_domain -> int -> clause list

returns the axioms for the given domain size, that is for totality and equality.

if print is given the axioms are printed.

returns all axioms, not only the new ones for this domain size.

adds functionality axioms if use_functionality_axioms is true.

val get_domain_element : int -> Term.term

returns the i.th domain element.

val get_domain_elements : int -> Term.term list

returns all domain elements for the given domain size.

val relation_to_equations : finite_domain -> term -> term list

transforms a relational term into all the functional term represented by it. E.g., r_2(z, x, y, 1) --> with the 2-ary function symbols f and g: f(x, y) = 1 g(x, y) = 1