Index of values


(%%) [LogtkUtil.Infix]
Function composition
(%>) [LogtkUtil.Infix]
Function composition
(++) [LogtkLazyGraph.Infix]
Union of graphs (alias for LogtkLazyGraph.union)
(++) [LogtkComparison]
Infix version of LogtkComparison.lexico
(<=.) [LogtkType]
Unary function type.
(<==) [LogtkType]
General function type.
(>>=) [LogtkTypeInference.Closure]
(>>>) [LogtkComparison]
Lexicographic combination starting with the given function
(@>>) [LogtkComparison]
Combination of comparators that work on the same values.
(@@) [LogtkType]
s @@ args applies the sort s to arguments args.
(|>) [LogtkUtil.Infix]
Application pipeline
__bvar [LogtkType]
not documented.
__forall [LogtkType]
not documented.
__mk_exists [LogtkFormula.S.Base]
__mk_exists [LogtkHOTerm.TPTP]
__mk_forall [LogtkFormula.S.Base]
__mk_forall [LogtkHOTerm.TPTP]
__mk_forall_ty [LogtkFormula.S.Base]
__mk_lambda [LogtkHOTerm]
not documented
_var [LogtkScopedTerm]
Unsafe version of LogtkScopedTerm.var that accepts negative index

A
a_star [LogtkLazyGraph]
Shortest path from the first node to nodes that satisfy goal, according to the given (positive!) distance function.
abs [LogtkSymbol.ArithOp]
ac_eq [LogtkFormula.S]
Equal modulo AC?
ac_normal_form [LogtkFormula.S]
Normal form modulo AC of "or" and "and"
add [LogtkMultiset.S]
Add one occurrence of the element
add [LogtkTypedPrologTerm.Subst]
add [LogtkRewriting.FormRW]
add [LogtkRewriting.SIG_TRS]
add [LogtkRewriting.ORDERED]
add [LogtkIndex.UNIT_IDX]
LogtkIndex the given (in)equation
add [LogtkIndex.SUBSUMPTION_IDX]
LogtkIndex the clause
add [LogtkIndex.TERM_IDX]
add [LogtkIndex.LEAF]
add [LogtkHORewriting]
Add a rule.
add_coeff [LogtkMultiset.S]
Add several occurrences of the element
add_default_hook [LogtkScopedTerm]
Add a print hook that will be used from now on
add_edge [LogtkLazyGraph.Mutable]
Add an edge; the two vertices must already exist
add_hook [LogtkHOTerm]
add_hook [LogtkFOTerm]
Hook used by default for printing
add_list [LogtkRewriting.FormRW]
add_list [LogtkRewriting.SIG_TRS]
add_list [LogtkRewriting.ORDERED]
add_list [LogtkOrdering_intf.S]
Update precedence with symbols
add_list [LogtkPrecedence_intf.S]
Update the precedence with the given symbols
add_printer [LogtkInterfaces.PRINT_OVERLOAD]
add_seq [LogtkRewriting.FormRW]
add_seq [LogtkRewriting.SIG_TRS]
add_seq [LogtkRewriting.ORDERED]
add_seq [LogtkIndex.UNIT_IDX]
add_seq [LogtkIndex.SUBSUMPTION_IDX]
add_seq [LogtkOrdering_intf.S]
Update precedence with signature
add_seq [LogtkPrecedence_intf.S]
add_set [LogtkHOTerm.Seq]
add_set [LogtkPrologTerm.Seq]
add_set [LogtkType.Seq]
add_set [LogtkFOTerm.Seq]
add_set [LogtkScopedTerm.Seq]
add_set [LogtkSymbol.Seq]
add_signature [LogtkTypeInference.Ctx]
Specify the type of some symbols
add_stat [LogtkUtil]
add_tbl [LogtkScopedTerm.Seq]
add_term_rule [LogtkRewriting.FormRW]
add_term_rules [LogtkRewriting.FormRW]
add_vars [LogtkHOTerm]
add variables of the term to the set
add_vars [LogtkFOTerm]
add variables of the term to the set
add_vertex [LogtkLazyGraph.Mutable]
Add a vertex to the graph
all_definitions [LogtkSkolem]
Definitions that were introduced so far.
all_positions [LogtkFOTerm]
apply f to all non-variable positions in t, accumulating the results along.
all_positions [LogtkScopedTerm]
Fold on all subterms of the given term, with their position.
alpha [LogtkPrecedence_intf.S.Constr]
alphabetic ordering on symbols
and_ [LogtkFormula.S.Base]
and_ [LogtkHOTerm.TPTP]
and_ [LogtkPrologTerm.TPTP]
and_ [LogtkSymbol.Base]
app [LogtkTypedPrologTerm]
app [LogtkPrologTerm.TPTP]
app [LogtkPrologTerm]
app [LogtkType]
Parametrized type
app [LogtkFOTerm]
Apply a term to a list of terms
app [LogtkScopedTerm]
app_full [LogtkFOTerm]
Apply the term to types, then to terms
append [LogtkIArray]
append [LogtkSubsts]
append s1 s2 is the substitution that maps t to s2 (s1 t).
append [LogtkPosition]
Append two positions
apply [LogtkTypedPrologTerm.Visitor]
apply [LogtkTransform]
Apply the transformations to a formula
apply [LogtkSubsts.SPECIALIZED]
Apply the substitution to the given term/type.
apply [LogtkSubsts]
Apply the substitution to the given term.
apply [LogtkType]
Given a function/forall type, and an argument, return the type that results from applying the function/forall to the arguments.
apply_list [LogtkType]
List version of LogtkType.apply
apply_no_renaming [LogtkSubsts.SPECIALIZED]
Same as LogtkSubsts.SPECIALIZED.apply, but performs no renaming of free variables.
apply_no_renaming [LogtkSubsts]
Same as LogtkSubsts.apply, but performs no renaming of free variables.
are_unifiable [LogtkUnif.UNARY]
are_unifiable [LogtkUnif.NARY]
are_variant [LogtkUnif.Form]
are_variant [LogtkUnif.UNARY]
are_variant [LogtkUnif.NARY]
arg [LogtkPosition.Build]
Arg position at the end
arg [LogtkPosition]
arith_hook [LogtkFOTerm.TPTP.Arith]
hook to print arithmetic expressions
arity [LogtkPrecedence_intf.S.Constr]
decreasing arity constraint (big arity => high in precedence)
arity [LogtkSignature]
Arity of the given symbol, or failure.
arity [LogtkType]
Number of arguments the type expects.
array_except_idx [LogtkUtil]
Elements of array except the one at given index (reverse list)
array_exists [LogtkUtil]
exists on array
array_foldi [LogtkUtil]
fold left on array, with index
array_forall [LogtkUtil]
Forall on array
array_forall2 [LogtkUtil]
Forall on pairs of arrays (Invalid_argument if they have distinct lengths)
array_shuffle [LogtkUtil]
shuffle randomly the array, in place
arrow [LogtkType]
arrow l r is the type l -> r.
arrow [LogtkSymbol.Base]
arrow_list [LogtkType]
n-ary version of LogtkType.arrow
at [LogtkHOTerm.Pos]
retrieve subterm at pos
at [LogtkHOTerm]
Curried application.
at [LogtkFOTerm.Pos]
retrieve subterm at pos
at [LogtkScopedTerm.Pos]
retrieve subterm at pos, or raise Invalid_argument
at [LogtkScopedTerm]
at_cpos [LogtkFOTerm.Pos]
retrieve subterm at the compact pos, or raise Invalid_argument
at_full [LogtkHOTerm]
at_list [LogtkHOTerm]
Curried application to several terms, left-parenthesing.
at_loc [LogtkTypedPrologTerm]
at_loc [LogtkPrologTerm]
atom [LogtkFormula.S.Base]
atoms [LogtkFormula.S.Seq]

B
base [LogtkSignature.TPTP.Arith]
arith op
base [LogtkSignature.TPTP]
base_symbols [LogtkSignature.TPTP]
beta_reduce [LogtkLambda]
Beta-reduce the term
bfs [LogtkLazyGraph]
Lazy traversal in breadth first
bfs_full [LogtkLazyGraph.Full]
Lazy traversal in breadth first from a finite set of vertices
bind [LogtkTypedPrologTerm]
bind [LogtkSubsts.SPECIALIZED]
Add v -> t to the substitution.
bind [LogtkSubsts]
Add v -> t to the substitution.
bind [LogtkPrologTerm.TPTP]
bind [LogtkPrologTerm]
bind [LogtkScopedTerm]
bind_list [LogtkTypedPrologTerm]
bind_to_default [LogtkTypeInference.Ctx]
Free constructor variables are bound to the default type provided at creation of the context.
bind_vars [LogtkScopedTerm]
bind several free variables in the term, transforming it to use De Bruijn indices.
bvar [LogtkTypedPrologTerm]
bvar [LogtkHOTerm]
Create a bound variable.
bvar [LogtkFOTerm]
Create a bound variable.
bvar [LogtkScopedTerm]
by_name [LogtkOrdering_intf.S]
Choose ordering by name among registered ones, or

C
call [LogtkComparison]
Call a lexicographic combination on arguments
can_apply [LogtkLambda]
Can we apply a term with the given type to terms with the corresponding list of types?
cancel [LogtkMultiset.S]
Remove common elements from the multisets.
cardinal [LogtkMultiset.S]
Number of unique occurrences of elements (the multiplicity of each element is considered)
cardinal [LogtkSignature]
Number of symbols
cast [LogtkHOTerm]
Change the type.
cast [LogtkFOTerm]
Change the type.
cast [LogtkScopedTerm]
Change the type
ceiling [LogtkFOTerm.TPTP.Arith]
ceiling [LogtkSymbol.ArithOp]
ceiling [LogtkSymbol.TPTP.Arith]
change_kind [LogtkScopedTerm]
Change the kind
choose [LogtkMultiset.S]
Chose one element, or
clear [LogtkCongruence.S]
Clear the content of the congruence.
clear [LogtkTypeInference.Ctx]
Reset totally the context
clear [LogtkSubsts.Renaming]
clear [LogtkType.Conv]
clear [LogtkCache.S2]
Clear content of the cache
clear [LogtkCache.S]
Clear content of the cache
clear_cache [LogtkOrdering_intf.S]
clear_debug [LogtkUtil.Section]
Clear debug level (will be same as parent's)
clear_var [LogtkSkolem]
reset the variable counter (once a formula has been processed)
close_all [LogtkTypedPrologTerm]
Bind all free vars with the symbol
close_all [LogtkPrologTerm]
Bind all free vars with the symbol
close_exists [LogtkFormula.S]
Bind all free variables with exists
close_exists [LogtkHOTerm.TPTP]
Bind all free variables with 'exists'
close_forall [LogtkFormula.S]
Bind all free variables with forall
close_forall [LogtkHOTerm.TPTP]
Bind all free variables with 'forall'
close_forall [LogtkType]
bind free variables
close_vars [LogtkScopedTerm]
Close all free variables of the term using the binding symbol
closed [LogtkTypedPrologTerm]
closed t is true iff all bound variables of t occur under a binder (i.e.
closed [LogtkScopedTerm.DB]
check whether the term is closed (all DB vars are bound within the term).
cluster [LogtkPrecedence_intf.S.Constr]
ordering constraint by clustering symbols by decreasing order.
cmp [LogtkIndex.CLAUSE]
Compare two clauses
cmp [LogtkPrecedence.SYMBOL]
cmp [LogtkInterfaces.ORD]
cnf_of [LogtkCnf]
LogtkTransform the clause into proper CNF; returns a list of clauses.
cnf_of_list [LogtkCnf]
codomain [LogtkSubsts]
Codomain (image terms) of substitution
collatz_graph [LogtkLazyGraph]
If n is even, n points to n/2, otherwise to 3n+1
collatz_graph_bis [LogtkLazyGraph]
Same as LogtkLazyGraph.collatz_graph, but also with reverse edges (n -> n*2, and n -> (n-1)/3 if n mod 3 = 1.
column [LogtkPrologTerm]
combine [LogtkParseLocation]
LogtkPosition that spans the two given positions.
combine [LogtkComparison]
combine two partial comparisons, that are assumed to be compatible, ie they do not order differently if Incomparable is not one of the values.
combine_list [LogtkParseLocation]
N-ary version of LogtkParseLocation.combine.
compare [LogtkPartialOrder_intf.S]
compare two elements in the ordering.
compare [LogtkMultiset.S]
Compare two multisets with the multiset extension of E.compare
compare [LogtkIndex.EQUATION]
Total order on equations
compare [LogtkOrdering_intf.S]
Compare two terms using the given ordering
compare [LogtkPrecedence_intf.S]
Compare two symbols using the precedence
compare [LogtkPosition]
compare_partial [LogtkMultiset.S]
Compare two multisets with the multiset extension of the given ordering.
compare_partial_l [LogtkMultiset.S]
Compare two multisets represented as list of elements
complete [LogtkPartialOrder_intf.S]
complete po f completes po using the function f elements to compare still unordered pairs.
compute [LogtkFeatureVector.Make.Feature]
compute_fv [LogtkFeatureVector.Make]
connectives [LogtkSymbol.TPTP]
cons [LogtkLazyList]
const [LogtkTypedPrologTerm]
const [LogtkHOTerm]
Create a typed constant.
const [LogtkPrologTerm.TPTP]
const [LogtkPrologTerm]
const [LogtkType]
Constant sort
const [LogtkFOTerm]
Create a typed constant
const [LogtkScopedTerm]
constr_list [LogtkPrecedence_intf.S]
Obtain the list of constraints
constrain [LogtkTypeInference.HO]
Constrain the term to be well-typed and of boolean type
constrain_exn [LogtkTypeInference.HO]
constrain_form [LogtkTypeInference.FO]
Force the untyped term to be typable as a formula.
constrain_form_exn [LogtkTypeInference.FO]
constrain_term_term [LogtkTypeInference.S]
constrain_term_term_exn [LogtkTypeInference.S]
Force the two terms to have the same type in this context
constrain_term_type [LogtkTypeInference.S]
constrain_term_type_exn [LogtkTypeInference.S]
Force the term's type and the given type to be the same.
constrain_type_type [LogtkTypeInference.Ctx]
Constrain the two types to be equal
contains [LogtkScopedTerm.DB]
Does t contains the De Bruijn variable of index n?
contains_symbol [LogtkFormula.S]
contains_symbol [LogtkHOTerm]
Does the term contain this given symbol?
contains_symbol [LogtkFOTerm]
Does the term contain this given symbol?
convert [LogtkTypeInference.HO]
Convert a single untyped term to a typed term.
convert [LogtkTypeInference.FO]
Convert a term into a typed term.
convert_clause [LogtkTypeInference.FO]
Convert a "clause" (i.e.
convert_clause_exn [LogtkTypeInference.FO]
convert_exn [LogtkTypeInference.HO]
convert_exn [LogtkTypeInference.FO]
convert_form [LogtkTypeInference.FO]
Convert a formula into a typed formula.
convert_form_exn [LogtkTypeInference.FO]
convert_seq [LogtkTypeInference.HO]
Infer the types of those terms and annotate each term and subterm with its type.
convert_seq [LogtkTypeInference.FO]
Given the signature for those formulas, infer their type and convert untyped formulas into typed formulas.
convert_seq_exn [LogtkTypeInference.HO]
convert_seq_exn [LogtkTypeInference.FO]
copy [LogtkPartialOrder_intf.S]
Copy of the partial order
copy [LogtkTypeInference.Ctx]
Copy of the context
copy [LogtkType.Conv]
count_symb_minus [LogtkFeatureVector.Make.Feature]
occurrences of symbol in negative clause
count_symb_plus [LogtkFeatureVector.Make.Feature]
occurrences of symbol in positive clause
create [LogtkLazyGraph.Mutable]
Create a new graph from the given equality and hash function, plus a view of it as an abstract graph
create [LogtkPartialOrder_intf.S]
build an empty partial order for the list of elements
create [LogtkTransform.DAG]
Create a DAG that implements the given list of transformations
create [LogtkCongruence.S]
New congruence.
create [LogtkSkolem]
New skolem contex.
create [LogtkPrecedence_intf.S]
make a precedence from the given constraints.
create [LogtkTypeInference.Ctx]
New context with a signature and default types.
create [LogtkSubsts.Renaming]
create [LogtkUtil.Flag]
New generator
create [LogtkType.Conv]
create [LogtkCache.S2]
Create a new cache of the given size.
create [LogtkCache.S]
Create a new cache of the given size.
create_sort [LogtkPrecedence_intf.S]
Sort the list of constraints by increasing priority, then call LogtkPrecedence_intf.S.create to build a precedence.
cur_level [LogtkUtil.Section]
Current debug level, with parent inheritance
curry [LogtkHOTerm]
Curry all subterms
cycles [LogtkCongruence.S]
Checks whether there are cycles in inequalities.

D
de_bruijn_set [LogtkFormula.S]
Set of De Bruijn indices that are not bound for types and terms
debug [LogtkHOTerm]
debug printing, with sorts
debug [LogtkUtil]
Print a debug message, with the given section and verbosity level.
debug [LogtkFOTerm]
debug printing, with sorts
declare [LogtkTypeInference.Ctx]
Declare the type of a symbol.
declare [LogtkSignature]
Declare the symbol, or
declare_status [LogtkPrecedence_intf.S]
Change the status of the given precedence
default [LogtkHashcons.S]
default hashconsing table
default [LogtkPrecedence_intf.S]
default precedence.
default [LogtkOptions]
Default options
default_features [LogtkFeatureVector.Make]
default_fp [LogtkFastFingerprint.Make]
default_fp [LogtkFingerprint.Make]
default_hooks [LogtkFormula.TERM]
default_hooks [LogtkFOTerm]
List of default hooks
default_of_list [LogtkOrdering_intf.S]
default ordering on terms (RPO6) using default precedence
default_of_prec [LogtkOrdering_intf.S]
default_seq [LogtkPrecedence_intf.S]
default precedence on the given sequence of symbols
depth [LogtkHOTerm]
depth of the term
depth [LogtkType]
Depth of the type (length of the longest path to some leaf)
depth [LogtkFOTerm]
depth of the term
depth [LogtkScopedTerm]
detect [LogtkFormulaShape]
Detect shapes in the given sequence, and convert them into transformations over formulas
detect_def [LogtkFormulaShape]
Detect definitions.
detect_list [LogtkFormulaShape]
dfs [LogtkLazyGraph]
Lazy traversal in depth first
dfs_full [LogtkLazyGraph.Full]
Lazy traversal in depth first from a finite set of vertices
diff [LogtkSignature]
diff s1 s2 contains the symbols of s1 that do not appear in s2.
difference [LogtkMultiset.S]
Difference of multisets.
difference [LogtkFOTerm.TPTP.Arith]
difference [LogtkSymbol.ArithOp]
difference [LogtkSymbol.TPTP.Arith]
dijkstra [LogtkLazyGraph]
Shortest path from the first node to the second one, according to the given (positive!) distance function.
divides [LogtkSymbol.ArithOp]
divisors [LogtkSymbol.ArithOp]
List of non-trivial strict divisors of the int.
divisors_graph [LogtkLazyGraph]
domain [LogtkSubsts]
Domain of substitution
dominates [LogtkComparison]
dominates f l1 l2 returns true iff for all element y of l2, there is some x in l1 with f x y = Gt
doubleton [LogtkIArray]
doubleton [LogtkMultiset.S]

E
elements [LogtkPartialOrder_intf.S]
Elements of the partial order.
empty [LogtkLazyGraph.Heap]
empty [LogtkLazyGraph]
Empty graph
empty [LogtkIArray]
empty [LogtkMultiset.S]
Empty multiset
empty [LogtkTypedPrologTerm.Subst]
empty [LogtkRewriting.FormRW]
empty [LogtkRewriting.SIG_TRS]
empty [LogtkRewriting.ORDERED]
empty [LogtkIndex.UNIT_IDX]
empty [LogtkIndex.SUBSUMPTION_IDX]
Empty index
empty [LogtkIndex.TERM_IDX]
empty [LogtkIndex.LEAF]
empty [LogtkHORewriting]
No rules
empty [LogtkSignature]
Empty signature
empty [LogtkSubsts]
The identity substitution
empty [LogtkPosition.Build]
Empty builder (position=Stop)
empty [LogtkDBEnv]
Empty environment
empty_with [LogtkFeatureVector.Make]
empty_with [LogtkFastFingerprint.Make]
Empty index, using the given fingerprint function
empty_with [LogtkFingerprint.Make]
Empty index, using the given fingerprint function
enable_profiling [LogtkUtil]
Enable/disable profiling
enrich [LogtkPartialOrder_intf.S]
Compare unordered pairs with the given partial order function.
enter_prof [LogtkUtil]
Enter the profiler
eprintf [LogtkUtil]
eq [LogtkPartialOrder.ELEMENT]
Equality function on elements
eq [LogtkMultiset.S]
Check equality of two multisets
eq [LogtkParseLocation]
eq [LogtkCongruence.TERM]
Syntactic equality on terms
eq [LogtkPrecedence.SYMBOL]
eq [LogtkPrecedence_intf.S]
Check whether the two precedences are equal (same snapshot)
eq [LogtkUnif.UNARY]
eq subst t1 s1 t2 s2 returns true iff the two terms are equal under the given substitution, i.e.
eq [LogtkFormula.S.Base]
eq [LogtkHOTerm.TPTP]
eq [LogtkPosition]
eq [LogtkInterfaces.EQ]
eq [LogtkPrologTerm.TPTP]
eq [LogtkFOTerm.AC]
Check whether the two terms are AC-equal.
eq [LogtkSymbol.Base]
equal [LogtkCache.EQ]
equal [LogtkHashcons.HashedLogtkType]
equiv [LogtkFormula.S.Base]
equiv [LogtkHOTerm.TPTP]
equiv [LogtkPrologTerm.TPTP]
equiv [LogtkSymbol.Base]
eta_reduce [LogtkLambda]
Eta-reduce the term
eval [LogtkTypedPrologTerm.Subst]
eval [LogtkScopedTerm.DB]
Evaluate the term in the given De Bruijn environment, by replacing De Bruijn indices by their value in the environment.
eval_head [LogtkTypedPrologTerm.Subst]
exists [LogtkIArray]
exists [LogtkMultiset.S]
exists [LogtkFormula.S.Base]
exists [LogtkHOTerm.TPTP]
exists [LogtkPrologTerm.TPTP]
exists [LogtkSymbol.Base]
exit_prof [LogtkUtil]
Exit the profiler
exit_scope [LogtkTypeInference.Ctx]
Exit the current scope (formula, clause), meaning that all free variables' types are forgotten.
expected_args [LogtkType]
LogtkTypes expected as function argument by ty.
extend [LogtkPartialOrder_intf.S]
Add new elements to the ordering, creating a new ordering.
extract [LogtkIndex.EQUATION]
Obtain a representation of the (in)equation.

F
false_ [LogtkPrecedence.SYMBOL]
false_ [LogtkFormula.S.Base]
false_ [LogtkHOTerm.TPTP]
antilogy term
false_ [LogtkPrologTerm.TPTP]
false_ [LogtkFOTerm.TPTP]
antilogy term
false_ [LogtkSymbol.Base]
features [LogtkFeatureVector.Make]
features_of_signature [LogtkFeatureVector.Make]
Build a set of features from the given signature.
file [LogtkSourced]
filter [LogtkLazyGraph]
Filter out vertices and edges that do not satisfy the given predicates.
filter [LogtkMultiset.S]
Filter out elements that don't satisfy the predicate
filter [LogtkSignature]
Only keep part of the signature
filter_map [LogtkMultiset.S]
More powerful mapping
finally [LogtkUtil]
finally h f calls f () and returns its result.
find [LogtkMultiset.S]
Return the multiplicity of the element within the multiset.
find [LogtkCongruence.S]
Current representative of this term
find [LogtkSignature]
Lookup the type of a symbol
find [LogtkDBEnv]
Find to which value the given De Bruijn index is bound to, or return None
find_cycle [LogtkLazyGraph]
Find a cycle in the given graph.
find_exn [LogtkSignature]
Lookup the type of a symbol
find_exn [LogtkDBEnv]
Unsafe version of LogtkDBEnv.find.
flatMap [LogtkLazyGraph]
Replace each vertex by some vertices.
flat_map [LogtkMultiset.S]
replace each element by a multiset in its own
flatten [LogtkFormula.S]
Flatten AC connectives (or/and)
flatten [LogtkFOTerm.AC]
flatten_ac f l flattens the list of terms l by deconstructing all its elements that have f as head symbol.
floor [LogtkFOTerm.TPTP.Arith]
floor [LogtkSymbol.ArithOp]
floor [LogtkSymbol.TPTP.Arith]
fmt [LogtkParseLocation]
fmt [LogtkTransform]
fmt [LogtkFeatureVector.Make.Feature]
fmt [LogtkOrdering_intf.S]
fmt [LogtkPrecedence_intf.S]
fmt [LogtkPosition.Build]
fmt [LogtkPosition]
fmt [LogtkInterfaces.PRINT1]
fmt [LogtkInterfaces.PRINT]
fold [LogtkIArray]
fold [LogtkLazyList]
Fold on values
fold [LogtkMultiset.S]
fold on occurrences of elements
fold [LogtkIndex.SUBSUMPTION_IDX]
fold [LogtkIndex.TERM_IDX]
fold [LogtkIndex.LEAF]
fold [LogtkTypeInference.Closure]
fold [LogtkSignature]
fold [LogtkSubsts]
fold [LogtkFormula.S]
Fold on terms
fold_coeffs [LogtkMultiset.S]
Fold on elements with their multiplicity
fold_depth [LogtkFormula.S]
Fold on terms, but with an additional argument, the number of De Bruijn indexes bound on through the path to the term
fold_l [LogtkTypeInference.Closure]
fold_match [LogtkIndex.LEAF]
Match the indexed terms against the given query term
fold_matched [LogtkIndex.LEAF]
Match the query term against the indexed terms
fold_unify [LogtkIndex.LEAF]
LogtkUnify the given term with indexed terms
foldi [LogtkIArray]
for_all [LogtkIArray]
for_all [LogtkMultiset.S]
for_all [LogtkTypedPrologTerm.Visitor]
forall [LogtkFormula.S.Base]
forall [LogtkHOTerm.TPTP]
forall [LogtkPrologTerm.TPTP]
forall [LogtkType]
forall vars ty quantifies ty over vars.
forall [LogtkSymbol.Base]
forall_ty [LogtkFormula.S.Base]
forall_ty [LogtkPrologTerm.TPTP]
forall_ty [LogtkSymbol.Base]
fp16 [LogtkFastFingerprint]
fp16 [LogtkFingerprint]
fp3d [LogtkFastFingerprint]
fp3d [LogtkFingerprint]
fp3w [LogtkFastFingerprint]
fp3w [LogtkFingerprint]
fp4d [LogtkFastFingerprint]
fp4d [LogtkFingerprint]
fp4m [LogtkFastFingerprint]
fp4m [LogtkFingerprint]
fp4w [LogtkFastFingerprint]
fp4w [LogtkFingerprint]
fp5m [LogtkFastFingerprint]
fp5m [LogtkFingerprint]
fp6m [LogtkFastFingerprint]
fp6m [LogtkFingerprint]
fp7 [LogtkFastFingerprint]
fp7 [LogtkFingerprint]
fp7m [LogtkFastFingerprint]
fp7m [LogtkFingerprint]
fprintf [LogtkUtil]
free_vars [LogtkFormula.S]
Set of free vars
free_vars [LogtkPrologTerm.Seq]
free_vars_set [LogtkFormula.S]
Set of free variables
fresh_bvar [LogtkTypedPrologTerm]
fresh_sym [LogtkSkolem]
Just obtain a fresh skolem symbol.
fresh_sym_with [LogtkSkolem]
Fresh symbol with a different name
fresh_ty_const [LogtkSkolem]
New symbol to be used as a type constant (no need to declare it)
fresh_unique_id [LogtkHashcons.S]
Unique ID that will never occur again in this table (modulo 2^63...)
fresh_var [LogtkTypedPrologTerm]
fresh free variable with the given type.
fresh_var [LogtkSkolem]
Unique index for universal variables
fresh_var [LogtkType]
Fresh var, with negative index
fresh_var [LogtkScopedTerm]
fresh_var ~kind ~ty () returns a fresh, unique, NOT HASHCONSED variable that will therefore never be equal to any other variable.
fresh_var [LogtkSymbol.Base]
New, unique symbol (cycles after 2^63 calls...)
from_enum [LogtkLazyGraph]
Concrete (eager) representation of a Graph
from_fun [LogtkLazyGraph]
Convenient semi-lazy implementation of graphs
from_list [LogtkLazyGraph]
Simple way to generate a graph, from a list of edges
from_var [LogtkScopedTerm.DB]
db_from_var t ~var replace var by a De Bruijn symbol in t.
full [LogtkSignature.TPTP.Arith]
arith op + regular op
full_name [LogtkUtil.Section]
Full path to the section

G
gcd [LogtkSymbol.ArithOp]
generalize [LogtkTypeInference.Ctx]
Free constructor variables will be generalized, i.e., kept as variables
gensym [LogtkSymbol]
Fresh symbol (with unique name)
get [LogtkIArray]
get [LogtkSourced]
get_debug [LogtkUtil.Section]
Specific level of this section, if any
get_debug [LogtkUtil]
Current debug level for Section.root
get_definition [LogtkSkolem]
rename_form ~ctx f returns a (possibly new) predicate for f, with the free variables of f as arguments.
get_fingerprint [LogtkFastFingerprint.Make]
get_fingerprint [LogtkFingerprint.Make]
get_flag [LogtkScopedTerm]
get_new [LogtkUtil.Flag]
New flag from the generator (2*previous flag)
get_start_time [LogtkUtil]
time at which the program started
get_total_time [LogtkUtil]
time elapsed since start of program
get_var [LogtkSubsts]
Lookup recursively the var in the substitution, until it is not a variable anymore, or it is not bound
global [LogtkOptions]
Global parameters, can be used as a mutable default
global_opts [LogtkOptions]
Options that modify LogtkOptions.global.
greater [LogtkFOTerm.TPTP.Arith]
greater [LogtkSymbol.ArithOp]
greater [LogtkSymbol.TPTP.Arith]
greatereq [LogtkFOTerm.TPTP.Arith]
greatereq [LogtkSymbol.ArithOp]
greatereq [LogtkSymbol.TPTP.Arith]
ground [LogtkTypedPrologTerm]
true iff there is no free variable
ground [LogtkPrologTerm]
ground [LogtkScopedTerm]
true if the term contains no free variables

H
has_definition [LogtkSkolem]
Does this formula already have a definition (in which case it's very cheap to reduce it to CNF)
has_new_definitions [LogtkSkolem]
hash [LogtkPartialOrder.ELEMENT]
Hashing on elements
hash [LogtkParseLocation]
hash [LogtkCache.HASH]
hash [LogtkHashcons.HashedLogtkType]
hash [LogtkCongruence.TERM]
Hash function on terms
hash [LogtkPrecedence.SYMBOL]
hash [LogtkPosition]
hash [LogtkInterfaces.HASH]
hash_fun [LogtkInterfaces.HASH]
hashcons [LogtkHashcons.S]
LogtkHashcons the elements
hashcons_stats [LogtkScopedTerm]
head [LogtkHOTerm]
head symbol (or Invalid_argument)
head [LogtkPosition.Build]
head [LogtkPosition]
head [LogtkFOTerm]
head symbol
head [LogtkScopedTerm]
Head symbol, or None if the term is a (bound) variable
head_exn [LogtkFOTerm]
head symbol (or Invalid_argument)
heap_graph [LogtkLazyGraph]
maps an integer i to 2*i and 2*i+1

I
i [LogtkType.TPTP]
individuals
i [LogtkSymbol.TPTP]
id [LogtkTypedPrologTerm.Visitor]
imply [LogtkFormula.S.Base]
imply [LogtkHOTerm.TPTP]
imply [LogtkPrologTerm.TPTP]
imply [LogtkSymbol.Base]
incr_stat [LogtkUtil]
infer [LogtkTypeInference.S]
infer_exn [LogtkTypeInference.S]
Infer the type of this term under the given signature.
infer_form [LogtkTypeInference.FO]
Inferring the type of a formula is trivial, it's always LogtkType.o.
infer_form_exn [LogtkTypeInference.FO]
init [LogtkIArray]
insert [LogtkLazyGraph.Heap]
instantiate [LogtkSkolem]
Instantiate first open variable with the given term
instantiate_ty [LogtkSkolem]
Instantiate first open (type) variable with the given type
int [LogtkType.TPTP]
integers
int [LogtkSymbol.TPTP]
int_ [LogtkPrologTerm]
int_of_string [LogtkSymbol]
intersection [LogtkMultiset.S]
Intersection of multisets (min of multiplicies)
introduced [LogtkSubsts]
Variables introduced by the substitution (ie vars of codomain)
inverse [LogtkInterfaces.GROUP]
invfreq [LogtkPrecedence_intf.S.Constr]
symbols with high frequency are smaller
is_ac [LogtkFOTerm.AC_SPEC]
is_app [LogtkType]
is_app [LogtkFOTerm]
is_app [LogtkScopedTerm]
is_arith [LogtkSymbol.TPTP.Arith]
Is the symbol a TPTP arithmetic symbol?
is_at [LogtkHOTerm]
is_at [LogtkScopedTerm]
is_atomic [LogtkFormula.S]
No connectives?
is_base_symbol [LogtkSignature.TPTP]
is_bind [LogtkScopedTerm]
is_bool [LogtkSignature.TPTP]
Has the symbol a boolean return sort?
is_bvar [LogtkTypedPrologTerm]
is_bvar [LogtkHOTerm]
is_bvar [LogtkType]
is_bvar [LogtkFOTerm]
is_bvar [LogtkScopedTerm]
is_clause [LogtkCnf]
Is it a clause, ie a list of literals?
is_closed [LogtkFormula.S]
All variables bound?
is_cnf [LogtkCnf]
Is the formula in CNF?
is_comm [LogtkFOTerm.AC_SPEC]
is_conjecture [LogtkSourced]
is_connective [LogtkSymbol.TPTP]
is_const [LogtkHOTerm]
is_const [LogtkFOTerm]
is_const [LogtkScopedTerm]
is_const [LogtkSymbol]
is_const_definition [LogtkFormulaShape]
Checks whether the clause is "const = ground composite term", e.g.
is_const_pred_definition [LogtkFormulaShape]
Definition of constant predicate
is_dag [LogtkLazyGraph]
Is the subgraph explorable from the given vertex, a Directed Acyclic Graph?
is_dag_full [LogtkLazyGraph]
Is the Graph reachable from the given vertices, a DAG? See LogtkLazyGraph.is_dag
is_definition [LogtkFormulaShape]
Check whether the clause defines a symbol, e.g.
is_distinct [LogtkSymbol]
is_empty [LogtkLazyGraph.Heap]
is_empty [LogtkMultiset.S]
Is the multiset empty?
is_empty [LogtkIndex.UNIT_IDX]
is_empty [LogtkIndex.TERM_IDX]
is_empty [LogtkIndex.LEAF]
is_empty [LogtkSignature]
is_empty [LogtkSubsts]
Is the substitution empty?
is_empty [LogtkDBEnv]
Are there bindings?
is_eq [LogtkCongruence.S]
Returns true if the two terms are equal in the congruence.
is_fo [LogtkHOTerm]
Check whether the term is convertible to a first-order term (no binders, no variable applied to something...)
is_forall [LogtkType]
is_form [LogtkFormula.S]
is_fun [LogtkType]
is_ground [LogtkSignature]
Only ground types?
is_ground [LogtkFormula.S]
No variables?
is_ground [LogtkHOTerm]
is the term ground? (no free vars)
is_ground [LogtkType]
Is the type ground? (means that no Var not BVar occurs in it)
is_ground [LogtkFOTerm]
is the term ground? (no free vars)
is_int [LogtkSymbol.TPTP.Arith]
is_int [LogtkSymbol]
is_lambda [LogtkHOTerm]
is_less [LogtkCongruence.S]
Returns true if the first term is strictly lower than the second one in the congruence
is_lit [LogtkCnf]
Literal?
is_max [LogtkMultiset.S]
Is the given element maximal (ie not dominated by any other element) within the multiset?
is_minus_one [LogtkSymbol.ArithOp]
is_multiset [LogtkHOTerm]
is_multiset [LogtkScopedTerm]
is_not_bool [LogtkSignature.TPTP]
is_numeric [LogtkSymbol]
is_one [LogtkSymbol.ArithOp]
is_operator [LogtkSignature.TPTP.Arith]
is_pred_definition [LogtkFormulaShape]
Check whether the formula is a predicate definition
is_pred_rewrite_rule [LogtkFormulaShape]
LogtkRewriting rule for predicates
is_rat [LogtkSymbol.TPTP.Arith]
is_rat [LogtkSymbol]
is_record [LogtkHOTerm]
is_record [LogtkScopedTerm]
is_record_get [LogtkScopedTerm]
is_record_set [LogtkScopedTerm]
is_renaming [LogtkSubsts]
Check whether the substitution is a variable renaming
is_rewrite_rule [LogtkFormulaShape]
More general than definition.
is_rigid_var [LogtkScopedTerm]
is_term [LogtkHOTerm]
is_term [LogtkFOTerm]
is_total [LogtkPartialOrder_intf.S]
Is the ordering total (i.e.
is_total_details [LogtkPartialOrder_intf.S]
More details than is_total, which returns true iff this function returns `total.
is_trivial [LogtkFormula.S]
Trivially true formula?
is_tyapp [LogtkFOTerm]
is_tyat [LogtkHOTerm]
is_type [LogtkType]
Is the term a representation of a type?
is_var [LogtkTypedPrologTerm]
is_var [LogtkHOTerm]
is_var [LogtkPrologTerm]
is_var [LogtkType]
is_var [LogtkFOTerm]
is_var [LogtkScopedTerm]
is_zero [LogtkSymbol.ArithOp]
iter [LogtkIArray]
iter [LogtkMultiset.S]
Iterate on distinct occurrences of elements
iter [LogtkRewriting.FormRW]
iter [LogtkRewriting.SIG_TRS]
iter [LogtkCongruence.S]
Iterate on terms that are explicitely present in the congruence.
iter [LogtkIndex.UNIT_IDX]
Iterate on indexed equations
iter [LogtkIndex.SUBSUMPTION_IDX]
iter [LogtkIndex.TERM_IDX]
iter [LogtkIndex.LEAF]
iter [LogtkSignature]
iter [LogtkSubsts]
iter [LogtkFormula.S]
iter [LogtkUtil.Section]
all registered sections
iter_coeffs [LogtkMultiset.S]
Iterate on elements with their multiplicity
iter_roots [LogtkCongruence.S]
Iterate on the congruence classes' representative elements.
iteri [LogtkIArray]

K
kbo [LogtkOrdering_intf.S]
Knuth-Bendix simplification ordering
kind [LogtkFormula.TERM]
kind [LogtkFormula.S]
kind [LogtkHOTerm]
kind [LogtkType]
kind [LogtkFOTerm]
kind [LogtkScopedTerm]

L
lambda [LogtkPrologTerm.TPTP]
lambda [LogtkSymbol.Base]
lambda_abstract [LogtkLambda]
lambda_abstract term ~sub, applied to a curried term term, and a subterm sub of term, gives term' such that beta_reduce (term' @ sub_t) == term holds.
lambda_abstract_list [LogtkLambda]
Abstract successively the given subterms, starting from the right ones.
lambda_apply_list [LogtkLambda]
Apply a lambda to a list of arguments.
lambda_var_ty [LogtkHOTerm]
Only on lambda terms: returns the type of the function argument.
last [LogtkComparison]
Last comparator
lcm [LogtkSymbol.ArithOp]
left [LogtkPosition.Build]
Add left at the end
left [LogtkPosition]
length [LogtkIArray]
less [LogtkFOTerm.TPTP.Arith]
less [LogtkSymbol.ArithOp]
less [LogtkSymbol.TPTP.Arith]
lesseq [LogtkFOTerm.TPTP.Arith]
lesseq [LogtkSymbol.ArithOp]
lesseq [LogtkSymbol.TPTP.Arith]
lexico [LogtkComparison]
Lexicographic combination (the second is used only if the first is Incomparable
lexicograph [LogtkUtil]
lexicographic order on lists l1,l2 which elements are ordered by f
lexicograph_combine [LogtkUtil]
combine comparisons by lexicographic order
list_ [LogtkPrologTerm]
list_diagonal [LogtkUtil]
All pairs of distinct positions of the list.
list_drop [LogtkUtil]
drop n elements
list_find [LogtkUtil]
find the first index of element, elemnt s.t.
list_flatmap [LogtkUtil]
flatten map
list_fmap [LogtkUtil]
filter map
list_fold_product [LogtkUtil]
Fold on the cartesian product
list_foldi [LogtkUtil]
fold on list, with index
list_get [LogtkUtil]
get n-th element of list (linear), or Not_found
list_inter [LogtkUtil]
list intersection, given the comparison function
list_iteri [LogtkUtil]
iter with index
list_mapi [LogtkUtil]
map with index
list_mem [LogtkUtil]
test for membership using the given comparison function
list_merge [LogtkUtil]
merges elements from both sorted list, removing duplicates
list_pos [LogtkUtil]
zip the list with positions (starting at 0)
list_product [LogtkUtil]
Cartesian product
list_range [LogtkUtil]
range from i to j
list_remove [LogtkUtil]
all the list but i-th element (linear)
list_set [LogtkUtil]
set n-th element of list (linear)
list_shuffle [LogtkUtil]
shuffle randomly the list
list_split_at [LogtkUtil]
split_at n l returns l1, l2 with l1 @ l2 = l and length l1 = min n (length l)
list_subset [LogtkUtil]
test for inclusion
list_take [LogtkUtil]
take n elements
list_union [LogtkUtil]
list union, given the comparison function
list_uniq [LogtkUtil]
list uniq: remove duplicates w.r.t the equality predicate
loc [LogtkTypedPrologTerm]
logtk [LogtkUtil.Section]
Section for all Logtk-related things
lookup [LogtkSubsts]
Lookup variable in substitution.

M
make [LogtkLazyGraph]
Build a graph from the force function
make [LogtkIArray]
make [LogtkSourced]
make a new sourced item.
make [LogtkOptions]
Produce of list of options suitable for Arg.parse, that may modify global parameters and the given option reference.
make [LogtkDBEnv]
Empty environment of the given size
make [LogtkUtil.Section]
make ?parent ?inheriting name makes a new section with the given name.
map [LogtkLazyGraph]
Map vertice and edge labels
map [LogtkIArray]
map [LogtkMultiset.S]
Apply a function to all elements
map [LogtkSourced]
map [LogtkTypeInference.Closure]
map [LogtkFormula.Map]
map [LogtkFormula.S]
Map on terms
map [LogtkDBEnv]
Map bound objects to other bound objects
map_coeff [LogtkMultiset.S]
Apply a function to all coefficients.
map_depth [LogtkFormula.S]
Map each term to another term.
map_error_seq [LogtkTypeInference]
map_error_seq f seq maps f over the sequence seq, and returns the (persistent) sequence of result if all calls to f succeed.
map_l [LogtkTypeInference.Closure]
map_leaf [LogtkFormula.S]
Call the function on leaves (atom,equal,true,false) and replace the leaves by their image.
map_leaf_depth [LogtkFormula.S]
map_shallow [LogtkFormula.S]
Apply the function to the immediate subformulas
mapi [LogtkIArray]
match_types [LogtkLambda]
Match the first type's arguments with the list.
matches [LogtkUnif.UNARY]
matches [LogtkUnif.NARY]
matching [LogtkUnif.UNARY]
matching ~pattern scope_p b scope_b returns sigma such that sigma pattern = b, or fails.
matching [LogtkUnif.NARY]
matching of two terms.
matching_adapt_scope [LogtkUnif.UNARY]
Call either LogtkUnif.UNARY.matching or LogtkUnif.UNARY.matching_same_scope depending on whether the given scopes are the same or not.
matching_same_scope [LogtkUnif.UNARY]
matches pattern (more general) with the other term.
max [LogtkMultiset.S]
Maximal elements of the multiset, w.r.t the given ordering.
max [LogtkPrecedence_intf.S.Constr]
maximal symbols, in decreasing order
max_cpos [LogtkFOTerm.Pos]
maximum compact position in the term
max_depth_minus [LogtkFeatureVector.Make.Feature]
maximal depth of symb in negative clause
max_depth_plus [LogtkFeatureVector.Make.Feature]
maximal depth of symb in positive clause
max_l [LogtkMultiset.S]
Maximal elements of a list
max_seq [LogtkMultiset.S]
Fold on maximal elements
max_var [LogtkHOTerm.Seq]
max_var [LogtkHOTerm]
find the maximum variable index, or 0
max_var [LogtkType.Seq]
max_var [LogtkFOTerm.Seq]
max var, or 0
max_var [LogtkFOTerm]
find the maximum variable index, or 0
max_var [LogtkScopedTerm.Seq]
mem [LogtkMultiset.S]
Is the element part of the multiset?
mem [LogtkHashcons.S]
Is the element present in this table?
mem [LogtkPrecedence_intf.S]
Is the symbol part of the precedence?
mem [LogtkSignature]
Is the symbol declared?
mem [LogtkSubsts.SPECIALIZED]
Variable is bound?
mem [LogtkSubsts]
Check whether the variable is bound by the substitution
mem [LogtkDBEnv]
mem env i returns true iff find env i returns Some _ rather than None, ie.
merge [LogtkHORewriting]
Merge two rewrite systems
merge [LogtkSignature]
Merge two signatures together.
min [LogtkPrecedence_intf.S.Constr]
minimal symbols, in decreasing order
min_var [LogtkHOTerm.Seq]
min_var [LogtkHOTerm]
minimum variable, or 0 if ground
min_var [LogtkFOTerm.Seq]
min var, or 0
min_var [LogtkFOTerm]
minimum variable, or 0 if ground
min_var [LogtkScopedTerm.Seq]
miniscope [LogtkCnf]
Apply miniscoping transformation to the term.
mk [LogtkParseLocation]
mk_and [LogtkHOTerm.TPTP]
mk_and_list [LogtkHOTerm.TPTP]
mk_at [LogtkScopedTerm]
mk_atom [LogtkFormula.S.Base]
mk_eq [LogtkCongruence.S]
mk_eq congruence t1 t2 asserts that t1 = t2 belongs to the congruence
mk_eq [LogtkFormula.S.Base]
mk_eq [LogtkHOTerm.TPTP]
mk_equiv [LogtkHOTerm.TPTP]
mk_exists [LogtkHOTerm.TPTP]
mk_forall [LogtkHOTerm.TPTP]
mk_fun_ty [LogtkPrologTerm.TPTP]
mk_global_opts [LogtkOptions]
mk_imply [LogtkHOTerm.TPTP]
mk_int [LogtkSymbol]
mk_lambda [LogtkHOTerm]
(lambda v1,...,vn.
mk_less [LogtkCongruence.S]
mk_less congruence t1 t2 asserts that t1 < t2 belongs to the congruence
mk_neq [LogtkHOTerm.TPTP]
mk_not [LogtkHOTerm.TPTP]
mk_or [LogtkHOTerm.TPTP]
mk_or_list [LogtkHOTerm.TPTP]
mk_pair [LogtkParseLocation]
mk_pos [LogtkParseLocation]
mk_profiler [LogtkUtil]
Create a named profiler
mk_rat [LogtkSymbol]
mk_rewrite [LogtkRewriting.ORDERED]
Given a TRS and a cache size, build a memoized function that performs term rewriting
mk_stat [LogtkUtil]
mk_xor [LogtkHOTerm.TPTP]
monomorphic [LogtkHOTerm]
true if the term contains no type var
monomorphic [LogtkFOTerm]
true if the term contains no type var
multiset [LogtkTypedPrologTerm]
multiset [LogtkHOTerm]
Build a multiset.
multiset [LogtkType]
LogtkType of multiset
multiset [LogtkScopedTerm]
multiset [LogtkSymbol.Base]
type of multisets

N
name [LogtkSourced]
name [LogtkFeatureVector.Make.Feature]
name [LogtkIndex.SUBSUMPTION_IDX]
name [LogtkIndex.TERM_IDX]
name [LogtkOrdering_intf.S]
Name that describes this ordering
need_cleanup [LogtkUtil]
Cleanup line before printing?
neq [LogtkFormula.S.Base]
neq [LogtkHOTerm.TPTP]
neq [LogtkPrologTerm.TPTP]
neq [LogtkSymbol.Base]
new_flag [LogtkScopedTerm]
nil [LogtkLazyList]
nil [LogtkPrologTerm]
none [LogtkOrdering_intf.S]
All terms are incomparable (equality still works).
normal_form [LogtkFOTerm.AC]
normal form of the term modulo AC
normalize [LogtkHORewriting]
Normalize the term w.r.t to the rewrite system
normalize_collect [LogtkHORewriting]
Normalize the term, and returns a list of rules used to normalize it.
not_ [LogtkFormula.S.Base]
not_ [LogtkHOTerm.TPTP]
not_ [LogtkPrologTerm.TPTP]
not_ [LogtkSymbol.Base]
num_bindings [LogtkDBEnv]
How many variables are actually bound?

O
o [LogtkType.TPTP]
propositions
o [LogtkSymbol.TPTP]
of_array [LogtkMultiset.S]
of_array_unsafe [LogtkIArray]
Take ownership of the given array.
of_coeffs [LogtkMultiset.S.Seq]
of_coeffs [LogtkMultiset.S]
From list of elements with multiplicities.
of_form [LogtkTransform.FORM]
of_form_rule [LogtkTransform]
of_form_rules [LogtkTransform]
of_form_rules_seq [LogtkTransform]
of_hoterm [LogtkFormula.FO]
of_iarray [LogtkMultiset.S]
From immutable array
of_int [LogtkTypedPrologTerm]
of_int [LogtkPrologTerm]
of_int [LogtkSymbol]
of_lexbuf [LogtkParseLocation]
Recover a position from a lexbuf
of_list [LogtkIArray]
of_list [LogtkMultiset.S]
Multiset from list
of_list [LogtkRewriting.FormRW]
of_list [LogtkRewriting.SIG_TRS]
of_list [LogtkHORewriting]
of_list [LogtkPrecedence_intf.S.Constr]
symbols in the given list are in decreasing order
of_list [LogtkSignature]
of_list [LogtkSubsts]
of_list [LogtkHOTerm.Tbl]
of_list [LogtkDBEnv]
Map indices to objects
of_list [LogtkInterfaces.ITER]
of_list [LogtkFOTerm.Tbl]
of_list [LogtkScopedTerm.Tbl]
of_pos [LogtkPosition.Build]
Start from a given position
of_precedence [LogtkPrecedence_intf.S.Constr]
Copy of another precedence on the common symbols
of_prolog [LogtkType.Conv]
of_rat [LogtkSymbol]
of_seq [LogtkIArray.Seq]
of_seq [LogtkMultiset.S.Seq]
of_seq [LogtkRewriting.FormRW]
of_seq [LogtkRewriting.SIG_TRS]
of_seq [LogtkHORewriting.Seq]
of_seq [LogtkSignature.Seq]
of_seq [LogtkSubsts]
of_seq [LogtkHOTerm.Tbl]
of_seq [LogtkInterfaces.ITER]
of_seq [LogtkFOTerm.Tbl]
of_seq [LogtkScopedTerm.Tbl]
of_signature [LogtkFeatureVector.Make]
of_string [LogtkTypedPrologTerm]
of_string [LogtkSymbol]
of_term [LogtkFormula.TERM]
of_term [LogtkFormula.S]
of_term [LogtkHOTerm]
of_term [LogtkType]
Conversion from a term, if structure matches
of_term [LogtkFOTerm]
of_term_exn [LogtkFormula.TERM]
of_term_exn [LogtkFormula.S]
of_term_exn [LogtkHOTerm]
of_term_exn [LogtkType]
Same as of_term, but without option
of_term_exn [LogtkFOTerm]
of_term_rule [LogtkTransform]
of_term_rules [LogtkTransform]
of_term_rules_seq [LogtkTransform]
of_term_tr [LogtkTransform]
Lift a term transformation to the formula level
of_total [LogtkComparison]
Conversion from a total order
on_buffer [LogtkUtil]
one_i [LogtkSymbol.ArithOp]
one_of_ty [LogtkSymbol.ArithOp]
one_rat [LogtkSymbol.ArithOp]
open_and [LogtkTransform]
transformation that opens outermost "and" connectives
open_and [LogtkFormula.S]
If the formula is an outer conjunction, return the list of elements of the conjunction
open_app [LogtkFOTerm]
Open application recursively so as to gather all type arguments
open_at [LogtkHOTerm]
Open application recursively so as to gather all type arguments
open_forall [LogtkFormula.S]
Remove outer forall binders, using fresh vars instead of DB symbols
open_fun [LogtkType]
open_fun ty "unrolls" function arrows from the left, so that open_fun (a -> (b -> (c -> d))) returns [a;b;c], d.
open_or [LogtkFormula.S]
open_vars [LogtkScopedTerm.DB]
List of "open" De Bruijn variables (with too high an index)
operators [LogtkSignature.TPTP.Arith]
opp [LogtkComparison]
Opposite of the relation: a R b becomes b R a
opp [LogtkPosition]
Opposite position, when it makes sense (left/right)
opposite_order [LogtkUtil]
the opposite order, that sorts elements the opposite way
or_ [LogtkFormula.S.Base]
or_ [LogtkHOTerm.TPTP]
or_ [LogtkPrologTerm.TPTP]
or_ [LogtkSymbol.Base]

P
pairs [LogtkPartialOrder_intf.S]
list of pairs (a > b)
parse_num [LogtkSymbol.ArithOp]
partial_cmp [LogtkComparison.PARTIAL_ORD]
plus [LogtkInterfaces.MONOID]
pop [LogtkLazyGraph.Heap]
pop [LogtkCongruence.S]
Restore to the previous checkpoint.
pop [LogtkDBEnv]
Exit a scope, removing the top binding.
pop_new_definitions [LogtkSkolem]
List of new definitions, that were introduced since the last call to new_definitions.
popen [LogtkUtil]
Run the given command cmd with the given input, wait for it to terminate, and return its stdout.
pp [LogtkLazyGraph.Dot]
Pretty print the given graph (starting from the given set of vertices) to the channel in DOT format
pp [LogtkMultiset.S]
pp [LogtkParseLocation]
pp [LogtkTransform]
pp [LogtkFeatureVector.Make.Feature]
pp [LogtkOrdering_intf.S]
pp [LogtkPrecedence.SYMBOL]
pp [LogtkPrecedence_intf.S]
pp [LogtkPosition.Build]
pp [LogtkPosition]
pp [LogtkInterfaces.PRINT1]
pp [LogtkInterfaces.PRINT]
pp_array [LogtkUtil]
print an array of items with printing function
pp_arrayi [LogtkUtil]
print an array, giving the printing function both index and item
pp_debug [LogtkPrecedence.SYMBOL]
pp_debug [LogtkPrecedence_intf.S]
pp_debug [LogtkFOTerm.TPTP.Arith]
use arith_hook with pp_debug
pp_depth [LogtkInterfaces.PRINT_DE_BRUIJN]
pp_enum [LogtkLazyGraph.Dot]
pp_list [LogtkUtil]
print a list of items using the printing function
pp_no_base [LogtkSignature.TPTP]
Print the signature, minus the base symbols
pp_opt [LogtkParseLocation]
pp_opt [LogtkUtil]
pp_pair [LogtkUtil]
pp_pos [LogtkUtil]
pp_seq [LogtkUtil]
Print the sequence
pp_snapshot [LogtkPrecedence_intf.S]
pp_surrounded [LogtkType]
pp_with [LogtkInterfaces.PRINT_OVERLOAD]
prec [LogtkFOTerm.TPTP.Arith]
prec [LogtkSymbol.ArithOp]
prec [LogtkSymbol.TPTP.Arith]
precedence [LogtkOrdering_intf.S]
Current precedence
prefix [LogtkPosition.Build]
Prefix the builder with the given position
print_all_types [LogtkHOTerm]
print_all_types [LogtkFOTerm]
If true, pp will print the types of all annotated terms
print_global_stats [LogtkUtil]
printf [LogtkUtil]
priority [LogtkIndex.EQUATION]
How "useful" this equation is.
product [LogtkLazyGraph]
Cartesian product of the two graphs
product [LogtkMultiset.S]
Multiply all multiplicities with the given coefficient
product [LogtkFOTerm.TPTP.Arith]
product [LogtkSymbol.ArithOp]
product [LogtkSymbol.TPTP.Arith]
push [LogtkCongruence.S]
Push a checkpoint on the stack of the congruence.
push [LogtkDBEnv]
Create a new environment, when entering a scope, where the De Bruijn index 0 is bound to the given value
push_none [LogtkDBEnv]
Create a new environment, when entering a scope, where the De Bruijn index 0 is bound to nothing.
push_none_multiple [LogtkDBEnv]
Call push_none n times (after we've entered n scopes, for instances)

Q
quotient [LogtkFOTerm.TPTP.Arith]
quotient [LogtkSymbol.ArithOp]
quotient [LogtkSymbol.TPTP.Arith]
quotient_e [LogtkFOTerm.TPTP.Arith]
quotient_e [LogtkSymbol.ArithOp]
quotient_e [LogtkSymbol.TPTP.Arith]
quotient_f [LogtkFOTerm.TPTP.Arith]
quotient_f [LogtkSymbol.ArithOp]
quotient_f [LogtkSymbol.TPTP.Arith]
quotient_t [LogtkFOTerm.TPTP.Arith]
quotient_t [LogtkSymbol.ArithOp]
quotient_t [LogtkSymbol.TPTP.Arith]

R
rat [LogtkPrologTerm]
rat [LogtkType.TPTP]
rationals
rat [LogtkSymbol.TPTP]
rat_of_string [LogtkSymbol]
real [LogtkType.TPTP]
reals
real [LogtkSymbol.TPTP]
record [LogtkTypedPrologTerm]
Build a record with possibly a row variable.
record [LogtkHOTerm]
Build a record.
record [LogtkPrologTerm]
record [LogtkType]
Record type, with an optional extension
record [LogtkScopedTerm]
record_field [LogtkPosition.Build]
record_field [LogtkPosition]
record_get [LogtkScopedTerm]
record_rest [LogtkPosition.Build]
record_rest [LogtkPosition]
record_set [LogtkScopedTerm]
register [LogtkOrdering_intf.S]
Register a new ordering, which can depend on a precedence.
remainder_e [LogtkFOTerm.TPTP.Arith]
remainder_e [LogtkSymbol.ArithOp]
remainder_e [LogtkSymbol.TPTP.Arith]
remainder_f [LogtkFOTerm.TPTP.Arith]
remainder_f [LogtkSymbol.ArithOp]
remainder_f [LogtkSymbol.TPTP.Arith]
remainder_t [LogtkFOTerm.TPTP.Arith]
remainder_t [LogtkSymbol.ArithOp]
remainder_t [LogtkSymbol.TPTP.Arith]
remove [LogtkIndex.UNIT_IDX]
remove [LogtkIndex.SUBSUMPTION_IDX]
Un-index the clause
remove [LogtkIndex.TERM_IDX]
remove [LogtkIndex.LEAF]
remove [LogtkSubsts]
Remove the given binding.
remove_def [LogtkSkolem]
remove the definition of f, so that we're sure it will never be used again
remove_seq [LogtkIndex.UNIT_IDX]
remove_seq [LogtkIndex.SUBSUMPTION_IDX]
remove_trivial [LogtkTransform]
Tranformation that removes trivial formulas
rename [LogtkTypedPrologTerm]
Rename all free variables
replace [LogtkHOTerm.Pos]
replace t pos ~by replaces the subterm at position pos in t by the term by.
replace [LogtkHOTerm]
replace t ~old ~by syntactically replaces all occurrences of old in t by the term by.
replace [LogtkFOTerm.Pos]
replace t pos ~by replaces the subterm at position pos in t by the term by.
replace [LogtkFOTerm]
replace t ~old ~by syntactically replaces all occurrences of old in t by the term by.
replace [LogtkScopedTerm.Pos]
replace t|_p by the second term
replace [LogtkScopedTerm.DB]
db_from_term t ~sub replaces sub by a fresh De Bruijn index in t.
replace [LogtkScopedTerm]
replace t ~old ~by syntactically replaces all occurrences of old in t by the term by.
res_head [LogtkUnif]
Obtain the first result, if any
retrieve [LogtkIndex.UNIT_IDX]
retrieve ~sign (idx,si) (t,st) acc folds on (in)equations l ?= r of given sign and substitutions subst, such that subst(l, si) = t.
retrieve_alpha_equiv [LogtkFeatureVector.Make]
Retrieve clauses that are potentially alpha-equivalent to the given clause
retrieve_alpha_equiv_c [LogtkFeatureVector.Make]
retrieve_generalizations [LogtkIndex.TERM_IDX]
retrieve_specializations [LogtkIndex.TERM_IDX]
retrieve_subsumed [LogtkIndex.SUBSUMPTION_IDX]
Fold on a set of indexed candidate clauses, that may be subsumed by the given clause
retrieve_subsumed_c [LogtkIndex.SUBSUMPTION_IDX]
retrieve_subsuming [LogtkIndex.SUBSUMPTION_IDX]
Fold on a set of indexed candidate clauses, that may subsume the given clause.
retrieve_subsuming_c [LogtkIndex.SUBSUMPTION_IDX]
retrieve_unifiables [LogtkIndex.TERM_IDX]
return [LogtkTypeInference.Closure]
rev [LogtkPosition]
Reverse the position
rev_path [LogtkLazyGraph]
Reverse the path
rewrite [LogtkRewriting.FormRW]
rewrite [LogtkRewriting.SIG_TRS]
Compute normal form of the term.
rewrite_collect [LogtkRewriting.FormRW]
Compute normal form of the formula, and return it together with the list of rules that were used to rewrite.
rewrite_collect [LogtkRewriting.SIG_TRS]
Compute normal form of the term, and also return the list of rules that were used.
right [LogtkPosition.Build]
Add left at the end
right [LogtkPosition]
rigid_var [LogtkHOTerm]
Rigid variable.
rigid_var [LogtkScopedTerm]
rigid_vars [LogtkScopedTerm.Seq]
rigidify [LogtkHOTerm]
Replace Var occurrences with RigidVar ones.
root [LogtkUtil.Section]
Default section, with no parent
round [LogtkFOTerm.TPTP.Arith]
round [LogtkSymbol.ArithOp]
round [LogtkSymbol.TPTP.Arith]
rpo6 [LogtkOrdering_intf.S]
Efficient implementation of RPO (recursive path ordering)
rule_to_form [LogtkRewriting.FormRW]
Convert the rule back to a term
rule_to_form [LogtkRewriting.SIG_TRS]
Make a formula out of a rule (an equality)

S
seq [LogtkTypeInference.Closure]
set [LogtkIArray]
Copy the array and modify its copy
set [LogtkDBEnv]
Set the n-th variable to the given objects.
set_debug [LogtkUtil.Section]
Debug level for section (and its descendants)
set_debug [LogtkUtil]
Set debug level of Section.root
set_default_printer [LogtkInterfaces.PRINT_OVERLOAD]
Used by PRINT.pp...
set_file [LogtkParseLocation]
Change the file name used for positions in this lexbuf
set_flag [LogtkScopedTerm]
set_memory_limit [LogtkUtil]
Limit the amount of memory available to the process (in MB)
set_precedence [LogtkOrdering_intf.S]
Change the precedence.
set_time_limit [LogtkUtil]
Limit the CPU time available to the process (in seconds)
set_weight [LogtkPrecedence_intf.S]
Change the weight function of the precedence
shift [LogtkScopedTerm.DB]
shift the non-captured De Bruijn indexes in the term by n
sign [LogtkSymbol.ArithOp]
signature_forms [LogtkTypeInference.FO]
Infer signature for this sequence of formulas, starting with an initial signature
signature_forms_exn [LogtkTypeInference.FO]
simple_app [LogtkScopedTerm]
simplify [LogtkFormula.S]
Simplify the formula
singleton [LogtkLazyGraph]
Trivial graph, composed of one node
singleton [LogtkIArray]
singleton [LogtkMultiset.S]
singleton [LogtkSignature]
singleton [LogtkDBEnv]
Single binding
size [LogtkPartialOrder_intf.S]
Number of elements
size [LogtkMultiset.S]
Number of distinct elements.
size [LogtkRewriting.FormRW]
size [LogtkRewriting.SIG_TRS]
size [LogtkRewriting.ORDERED]
size [LogtkIndex.UNIT_IDX]
Number of indexed (in)equations
size [LogtkIndex.TERM_IDX]
size [LogtkIndex.LEAF]
size [LogtkFormula.TERM]
size [LogtkHOTerm]
Size (number of nodes)
size [LogtkDBEnv]
Number of scopes (number of times LogtkDBEnv.push or LogtkDBEnv.push_none were called to produce the given environement)
size [LogtkType]
Size of type, in number of "nodes"
size [LogtkFOTerm]
Size (number of nodes)
size [LogtkScopedTerm]
size_minus [LogtkFeatureVector.Make.Feature]
size of negative clause
size_plus [LogtkFeatureVector.Make.Feature]
size of positive clause
skolem_form [LogtkSkolem]
Skolemize the given formula at root (assumes it occurs just under an existential quantifier, whose De Bruijn variable 0 is replaced by a fresh symbol applied to free variables).
skolem_ho [LogtkSkolem]
Skolemize a higher order term.
slurp [LogtkUtil]
Read the whole filedescriptor into a string
smaller [LogtkParseLocation]
smaller p1 p2 is true if p1 is included in p2, ie p1 is a sub-location of p2 (interval inclusion)
snapshot [LogtkPrecedence_intf.S]
Current list of symbols, in decreasing order
sprintf [LogtkUtil]
print into a string
stack_size [LogtkCongruence.S]
Number of calls to LogtkCongruence.S.push that lead to the current state of the congruence.
stats [LogtkHashcons.S]
status [LogtkPrecedence_intf.S]
Status of the symbol
stop [LogtkPosition]
str_find [LogtkUtil]
Find sub in the string, returns its first index or -1
str_prefix [LogtkUtil]
str_prefix ~pre s returns true iff pre is a prefix of s
str_repeat [LogtkUtil]
The same char, repeated n times
str_split [LogtkUtil]
str_sub [LogtkUtil]
Equality from the given start position
sub [LogtkType.Seq]
subterm [LogtkOrdering_intf.S]
Subterm ordering.
subterm [LogtkFormula.S]
subterm t f true iff t occurs in some term of f
subterm [LogtkHOTerm]
checks whether sub is a (non-strict) subterm of t
subterm [LogtkPrologTerm]
is sub a (strict?) subterm of the other arg?
subterm [LogtkFOTerm]
checks whether sub is a (non-strict) subterm of t
subterms [LogtkTypedPrologTerm.Seq]
subterms [LogtkCongruence.TERM]
Subterms of the term (possibly empty list)
subterms [LogtkHOTerm.Seq]
subterms [LogtkPrologTerm.Seq]
subterms [LogtkFOTerm.Seq]
subterms [LogtkScopedTerm.Seq]
subterms_depth [LogtkHOTerm.Seq]
subterms_depth [LogtkFOTerm.Seq]
subterms_depth [LogtkScopedTerm.Seq]
subterms_with_bound [LogtkTypedPrologTerm.Seq]
subterms_with_bound [LogtkPrologTerm.Seq]
subterm and variables bound at this subterm
succ [LogtkFOTerm.TPTP.Arith]
succ [LogtkSymbol.ArithOp]
succ [LogtkSymbol.TPTP.Arith]
suffix [LogtkPosition.Build]
Append position at the end
sum [LogtkMultiset.S]
Sum of multiplicies
sum [LogtkFOTerm.TPTP.Arith]
sum [LogtkSymbol.ArithOp]
sum [LogtkSymbol.TPTP.Arith]
sum_of_depths [LogtkFeatureVector.Make.Feature]
sum of depths of symbols
symbols [LogtkPrecedence_intf.S.Seq]
symbols [LogtkSignature.Seq]
symbols [LogtkFormula.S.Seq]
symbols [LogtkFormula.S]
Set of symbols occurring in the formula
symbols [LogtkHOTerm.Seq]
symbols [LogtkHOTerm]
LogtkSymbols of the term (keys of signature)
symbols [LogtkPrologTerm.Seq]
symbols [LogtkFOTerm.AC]
Set of symbols occurring in the terms, that are AC
symbols [LogtkFOTerm.Seq]
symbols [LogtkFOTerm]
LogtkSymbols of the term (keys of signature)
symbols [LogtkScopedTerm.Seq]
symbols [LogtkSymbol.TPTP.Arith]
syntactic [LogtkPrologTerm]

T
tType [LogtkTypedPrologTerm]
tType [LogtkPrologTerm.TPTP]
tType [LogtkType]
Pseudo-type of types
tType [LogtkScopedTerm]
The root of the type system.
tType [LogtkSymbol.Base]
tag [LogtkHashcons.HashedLogtkType]
terms [LogtkFormula.S.Seq]
times [LogtkUtil]
call the function n times with unit
to_coeffs [LogtkMultiset.S.Seq]
to_dot [LogtkIndex.UNIT_IDX]
print the index in the DOT format
to_dot [LogtkIndex.TERM_IDX]
print oneself in DOT into the given file
to_form [LogtkTransform.FORM]
to_hoterm [LogtkFormula.FO]
to_int [LogtkSymbol.ArithOp]
to_int [LogtkSymbol.TPTP.Arith]
to_list [LogtkIArray]
to_list [LogtkLazyList]
Gather all values into a list
to_list [LogtkMultiset.S]
List of elements with their coefficients
to_list [LogtkHORewriting]
to_list [LogtkSignature]
to_list [LogtkSubsts]
to_list [LogtkHOTerm.Tbl]
to_list [LogtkInterfaces.ITER]
to_list [LogtkFOTerm.Tbl]
to_list [LogtkScopedTerm.Tbl]
to_lits [LogtkIndex.CLAUSE]
Iterate on literals of the clause
to_pos [LogtkPosition.Build]
Extract current position
to_prolog [LogtkFormula.TERM]
to_prolog [LogtkFormula.S]
to_prolog [LogtkType.Conv]
convert a type to a prolog term.
to_prolog [LogtkFOTerm]
to_rat [LogtkSymbol.ArithOp]
to_rat [LogtkSymbol.TPTP.Arith]
to_seq [LogtkIArray.Seq]
to_seq [LogtkLazyList]
Iterate on values
to_seq [LogtkMultiset.S.Seq]
to_seq [LogtkRewriting.FormRW]
to_seq [LogtkRewriting.SIG_TRS]
to_seq [LogtkRewriting.ORDERED]
to_seq [LogtkHORewriting.Seq]
to_seq [LogtkSignature.Seq]
to_seq [LogtkSubsts]
to_seq [LogtkHOTerm.Tbl]
to_seq [LogtkInterfaces.ITER]
to_seq [LogtkFOTerm.Tbl]
to_seq [LogtkScopedTerm.Tbl]
to_set [LogtkSignature]
Set of symbols of the signature
to_signature [LogtkSkolem]
Signature of all new skolem symbols that were created using this context.
to_signature [LogtkTypeInference.Ctx]
Obtain the type of all symbols whose type has been inferred.
to_string [LogtkParseLocation]
to_string [LogtkOrdering_intf.S]
to_string [LogtkPrecedence_intf.S]
to_string [LogtkComparison]
Infix Representation
to_string [LogtkPosition]
to_string [LogtkInterfaces.PRINT1]
to_string [LogtkInterfaces.PRINT]
to_total [LogtkComparison]
Conversion to a total ordering.
tptp_default [LogtkTypeInference]
Default TPTP types for ints, rats, etc.
transform [LogtkTransform.DAG]
LogtkTransform a set of formulas recursively
true_ [LogtkPrecedence.SYMBOL]
true_ [LogtkFormula.S.Base]
true_ [LogtkHOTerm.TPTP]
tautology term
true_ [LogtkPrologTerm.TPTP]
true_ [LogtkFOTerm.TPTP]
tautology term
true_ [LogtkSymbol.Base]
truncate [LogtkFOTerm.TPTP.Arith]
truncate [LogtkSymbol.ArithOp]
truncate [LogtkSymbol.TPTP.Arith]
ty [LogtkTypedPrologTerm]
ty [LogtkFormula.TERM]
ty [LogtkHOTerm]
ty [LogtkFOTerm]
Obtain the type of a term..
ty [LogtkScopedTerm]
LogtkType of the term, if any
ty [LogtkSymbol]
ty_exn [LogtkScopedTerm]
Same as LogtkScopedTerm.ty, but fails if the term has no type
ty_of_prolog [LogtkTypeInference.Ctx]
LogtkType conversion from LogtkPrologTerm
ty_vars [LogtkHOTerm.Seq]
ty_vars [LogtkHOTerm]
Set of free type variables
ty_vars [LogtkFOTerm.Seq]
ty_vars [LogtkFOTerm]
Set of free type variables
tyapp [LogtkFOTerm]
Apply a term to a type
tyat [LogtkHOTerm]
Curried type application.
tyat_list [LogtkHOTerm]
Application to a list of types
type_ [LogtkPosition.Build]
type_ [LogtkPosition]
typed_symbols [LogtkFOTerm.Seq]
types [LogtkSignature.Seq]
types [LogtkScopedTerm.Seq]

U
uminus [LogtkFOTerm.TPTP.Arith]
uminus [LogtkSymbol.ArithOp]
uminus [LogtkSymbol.TPTP.Arith]
uncurry [LogtkHOTerm]
Un-curry all subterms.
unification [LogtkUnif.UNARY]
LogtkUnify terms, returns a subst or
unification [LogtkUnif.NARY]
unification of two terms
unify [LogtkTypedPrologTerm]
LogtkUnify two terms, might fail
unify_exn [LogtkTypedPrologTerm]
Same as LogtkTypedPrologTerm.unify, but can raise.
union [LogtkLazyGraph]
Lazy union of the two graphs.
union [LogtkMultiset.S]
Union of multisets (max of multiplicies)
unrigidify [LogtkHOTerm]
Converse of LogtkHOTerm.rigidify
unshift [LogtkScopedTerm.DB]
unshift n t unshifts the term t's bound variables by n.
update_precedence [LogtkOrdering_intf.S]
Update the precedence with a function.
update_subterms [LogtkCongruence.TERM]
Replace immediate subterms by the given list.
update_var [LogtkSkolem]
Avoid collisions with variables of this term in calls to LogtkSkolem.fresh_var.

V
var [LogtkTypedPrologTerm]
var [LogtkHOTerm]
Create a variable.
var [LogtkPrologTerm.TPTP]
var [LogtkPrologTerm]
var [LogtkType]
Build a type variable.
var [LogtkFOTerm]
Create a variable.
var [LogtkScopedTerm]
var_occurs [LogtkHOTerm]
var_occurs ~var t true iff var in t
var_occurs [LogtkFOTerm]
var_occurs ~var t true iff var in t
variant [LogtkUnif.Form]
variant [LogtkUnif.UNARY]
Succeeds iff the first term is a variant of the second, ie if they are alpha-equivalent
variant [LogtkUnif.NARY]
alpha-equivalence checking of two terms
vars [LogtkTypedPrologTerm.Seq]
vars [LogtkTypedPrologTerm]
vars [LogtkFormula.TERM.Seq]
vars [LogtkFormula.S.Seq]
vars [LogtkHOTerm.Seq]
vars [LogtkHOTerm]
compute variables of the terms
vars [LogtkPrologTerm.Seq]
vars [LogtkType.Seq]
vars [LogtkType]
List of free variables (Var)
vars [LogtkFOTerm.Seq]
vars [LogtkFOTerm]
compute variables of the terms
vars [LogtkScopedTerm.Seq]
vars_prefix_order [LogtkHOTerm]
variables in prefix traversal order
vars_prefix_order [LogtkFOTerm]
variables in prefix traversal order
vars_set [LogtkType]
Add the free variables to the given set
view [LogtkTypedPrologTerm]
view [LogtkFormula.S]
View of the formula
view [LogtkHOTerm]
view [LogtkPrologTerm]
view [LogtkType]
LogtkType-centric view of the head of this type.
view [LogtkFOTerm.Classic]
view [LogtkFOTerm]
view [LogtkScopedTerm]
View on the term's head form
view [LogtkSymbol.ArithOp]
Arith centered view of symbols

W
weak_of [LogtkHashcons.S]
Get the underlying weak table
weight [LogtkPrecedence_intf.S]
Weight of a symbol (for KBO).
weight [LogtkFormula.S]
Number of 'nodes' of the formula, including the terms
weight [LogtkFOTerm]
Compute the weight of a term, given a weight for variables and one for symbols.
weight_constant [LogtkPrecedence_intf.S]
weight_modarity [LogtkPrecedence_intf.S]
well_founded [LogtkSignature]
Are there some symbols of arity 0 in the signature?
wildcard [LogtkTypedPrologTerm]
wildcard [LogtkPrologTerm]
wildcard [LogtkSymbol.Base]
$_ for type inference
with_cache [LogtkCache.S2]
Wrap the function with the cache
with_cache [LogtkCache.S]
Wrap the function with the cache
with_cache_rec [LogtkCache.S2]
Partially apply the given function with a cached version of itself.
with_cache_rec [LogtkCache.S]
Partially apply the given function with a cached version of itself.
with_constr_list [LogtkPrecedence_intf.S]
Update the precedence by replacing its list of constraints.
with_input [LogtkUtil]
Open the given file for reading, and returns the result of the action applied to the input channel
with_lock_file [LogtkUtil]
perform the action with a lock on the given file
with_output [LogtkUtil]
Open the given file for writing, and returns the result of the action applied to the output channel
with_ty [LogtkTypedPrologTerm]

X
xor [LogtkFormula.S.Base]
xor [LogtkHOTerm.TPTP]
xor [LogtkPrologTerm.TPTP]
xor [LogtkSymbol.Base]

Y
yield_prof [LogtkUtil]
Yield control to sub-call

Z
zero [LogtkInterfaces.MONOID]
zero_i [LogtkSymbol.ArithOp]
zero_of_ty [LogtkSymbol.ArithOp]
zero_rat [LogtkSymbol.ArithOp]