package DAGaml

  1. Overview
  2. Docs
package DAGaml
Legend:
Library
Module
Module type
Parameter
Class
Class type
val prefix : string
type tree =
  1. | Const of bool
  2. | Units of CnfTypes.term list * tree
  3. | OrUnits of CnfTypes.term list * tree
  4. | Sha3 of int * tree * tree * tree
  5. | DSAnd of tree list
module ToS : sig ... end
module ToSTree : sig ... end
module ToPrettyS : sig ... end
val support : CnfTypes.clause -> int list
val clause_sorted : ?last:int -> CnfTypes.clause -> bool
val formule_sorted : CnfTypes.formule -> bool
val file_sorted : CnfTypes.file -> bool
val clause_tauto_rec : int -> bool -> CnfTypes.clause -> bool
val clause_tauto : CnfTypes.clause -> bool
val clause_trivial : CnfTypes.clause -> bool option
val formule_trivial : CnfTypes.formule -> CnfTypes.formule option
val terml_set : ?carry:CnfTypes.clause -> CnfTypes.term -> CnfTypes.clause -> (CnfTypes.clause, bool) result
val clause_addl : ?carry:CnfTypes.clause -> CnfTypes.term list -> CnfTypes.clause -> CnfTypes.clause
val clause_set : ?carry:CnfTypes.clause -> CnfTypes.term -> CnfTypes.clause -> (CnfTypes.clause, bool) result
val clause_setl : ?carry:CnfTypes.clause -> CnfTypes.term list -> CnfTypes.clause -> (CnfTypes.clause, bool) result
val tos_result : ('a -> string) -> ('b -> string) -> ('a, 'b) result -> string
val formule_set : ?carry:CnfTypes.formule -> CnfTypes.term -> CnfTypes.formule -> (CnfTypes.formule, bool) result
val formule_add_units : CnfTypes.term list -> CnfTypes.formule -> CnfTypes.formule
type units_formule_result = (CnfTypes.term list * CnfTypes.formule, CnfTypes.term list option) result
val formule_unit_setl : ?units:CnfTypes.clause -> CnfTypes.term list -> CnfTypes.formule -> units_formule_result
val connected_components : int -> (int * 'a) list list -> (int * 'a) list list list
val clause_trisjunction : int -> ?carry:CnfTypes.clause -> CnfTypes.clause -> (bool * CnfTypes.clause) option
val formule_trisjunction : int -> ?assert_noempty:bool -> ?carry0:CnfTypes.formule -> ?carry1:CnfTypes.formule -> ?carryX:CnfTypes.formule -> CnfTypes.formule -> CnfTypes.formule * CnfTypes.formule * CnfTypes.formule
val clause_unique : CnfTypes.clause -> (CnfTypes.clause, bool) result
val clause_sort : CnfTypes.clause -> (CnfTypes.clause, bool) result
val formule_sort : ?carry:CnfTypes.formule -> CnfTypes.formule -> (CnfTypes.formule, bool) result
val cons_orunits : CnfTypes.clause -> tree -> tree
val cons_units : CnfTypes.term list -> tree -> tree
val treefy_shannon_nosimpl : int list -> CnfTypes.formule -> tree
val treefy_shannon : int list -> int -> CnfTypes.formule -> tree
val formule_in_order : CnfTypes.formule -> int list -> bool
val treefy_shannon_cc : int list -> int -> CnfTypes.formule -> tree
val tree_size : tree -> int
val tree_simplify_const : tree -> tree
val pprint : tree -> unit
val bucketize_clause_asap : int list array -> CnfTypes.clause -> CnfTypes.formule array -> CnfTypes.formule ref -> unit
val bucketize_clause_alap : int list array -> CnfTypes.clause -> CnfTypes.formule array -> CnfTypes.formule ref -> unit
val bucketize_clause_all : int list array -> CnfTypes.clause -> CnfTypes.formule array -> CnfTypes.formule ref -> unit
val bucketize_clause : ?mode:GuaCaml.Tools.prio_t -> int list array -> CnfTypes.clause -> CnfTypes.formule array -> CnfTypes.formule ref -> unit
val bucketize_formule : ?mode:GuaCaml.Tools.prio_t -> int list array -> CnfTypes.formule -> CnfTypes.formule array * CnfTypes.formule
module Wap : sig ... end
module CnfRbtf : sig ... end
module type CnfRbtf_Sig = sig ... end
val file_of_formule : ?input:int -> ?quants:CnfTypes.quants -> CnfTypes.formule -> CnfTypes.file
val formule_support : CnfTypes.file -> bool array
val file_rename : CnfTypes.file -> int -> int array -> CnfTypes.file
val relative_file_of_formule : int -> ?quants:CnfTypes.quants -> CnfTypes.formule -> int option array * int array * CnfTypes.file