Module `OLCoq.Ol`Source

Sourceval total_formula : int ref

Sourceval total_polar : int ref

Sourceval total_normal : int ref

Sourcetype formula =

| Variable of {
1. id : int;
2. unique_key : int;
3. mutable polar_formula : polar_formula option;
}
| Neg of {
1. child : formula;
2. unique_key : int;
3. mutable polar_formula : polar_formula option;
}
| Or of {
1. children : formula list;
2. unique_key : int;
3. mutable polar_formula : polar_formula option;
}
| And of {
1. children : formula list;
2. unique_key : int;
3. mutable polar_formula : polar_formula option;
}
| Literal of {
1. b : bool;
2. unique_key : int;
3. mutable polar_formula : polar_formula option;
}

Sourceand polar_formula =

| PolarVariable of {
1. id : int;
2. polarity : bool;
3. unique_key : int;
4. mutable inverse : polar_formula option;
5. mutable normal_form : normal_formula option;
}
| PolarAnd of {
1. children : polar_formula list;
2. polarity : bool;
3. unique_key : int;
4. mutable inverse : polar_formula option;
5. mutable normal_form : normal_formula option;
}
| PolarLiteral of {
1. b : bool;
2. unique_key : int;
3. mutable inverse : polar_formula option;
4. mutable normal_form : normal_formula option;
}

Sourceand normal_formula =

| NormalVariable of {
1. id : int;
2. polarity : bool;
3. unique_key : int;
4. mutable inverse : normal_formula option;
5. mutable formulaP : formula option;
6. mutable formulaN : formula option;
7. lt_cache : (int, bool) Hashtbl.t;
}
| NormalAnd of {
1. children : normal_formula list;
2. polarity : bool;
3. unique_key : int;
4. mutable inverse : normal_formula option;
5. mutable formulaP : formula option;
6. mutable formulaN : formula option;
7. lt_cache : (int, bool) Hashtbl.t;
}
| NormalLiteral of {
1. b : bool;
2. unique_key : int;
3. mutable inverse : normal_formula option;
4. mutable formulaP : formula option;
5. mutable formulaN : formula option;
6. lt_cache : (int, bool) Hashtbl.t;
}

Sourceval new_variable : int -> formula

Sourceval new_neg : formula -> formula

Sourceval new_or : formula list -> formula

Sourceval new_and : formula list -> formula

Sourceval new_literal : bool -> formula

Sourceval new_p_variable : int -> bool -> polar_formula

Sourceval new_p_and : polar_formula list -> bool -> polar_formula

Sourceval new_p_literal : bool -> polar_formula

Sourceval new_n_variable : int -> bool -> normal_formula

Sourceval new_n_and : normal_formula list -> bool -> normal_formula

Sourceval new_n_literal : bool -> normal_formula

Sourceval get_key : formula -> int

Sourceval get_polar_formula : formula -> polar_formula option

Sourceval set_polar_formula : formula -> polar_formula option -> unit

Sourceval get_p_normal_form : polar_formula -> normal_formula option

Sourceval set_p_normal_form : polar_formula -> normal_formula option -> unit

Sourceval size : formula -> int

Sourceval get_p_key : polar_formula -> int

Sourceval get_p_inverse_option : polar_formula -> polar_formula option

Sourceval set_p_inverse_option : polar_formula -> polar_formula option -> unit

Sourceval get_n_key : normal_formula -> int

Sourceval get_n_inverse_option : normal_formula -> normal_formula option

Sourceval set_n_inverse_option : normal_formula -> normal_formula option -> unit

Sourceval get_formulaP : normal_formula -> formula option

Sourceval set_formulaP : normal_formula -> formula option -> unit

Sourceval get_formulaN : normal_formula -> formula option

Sourceval set_formulaN : normal_formula -> formula option -> unit

Sourceval get_lt_cache : normal_formula -> (int, bool) Hashtbl.t

Sourceval lt_cached : normal_formula -> normal_formula -> bool option

Sourceval set_lt_cached : normal_formula -> normal_formula -> bool -> unit

Sourceval formula_to_string : formula -> string

Sourceval polar_formula_to_string : polar_formula -> string

Sourceval normal_formula_to_string : normal_formula -> string

Sourceval get_polar_inverse : polar_formula -> polar_formula

Sourceval polarize : formula -> bool -> polar_formula

Sourceval get_normal_inverse : normal_formula -> normal_formula

Sourceval to_formula_nnf : normal_formula -> bool -> formula

Sourceval to_formula : normal_formula -> formula

Sourceval lattices_leq : normal_formula -> normal_formula -> bool

Sourceval simplify : normal_formula list -> bool -> normal_formula

Sourceval check_for_contradiction : normal_formula -> bool

Sourceval polar_to_normal_form : polar_formula -> normal_formula

Sourceval reduced_form : formula -> formula

Sourceval show_ol : unit -> unit

package orthologic-coq

Module OLCoq.OlSource

Module `OLCoq.Ol`Source