Index of values


(>>>) [Encoding]
Infix notation for composition
__magic [Encoding.EncodedClause]
Don't use unless you know what you're doing.

A
add [Prover]
Add a clause
add [Plugin.Set]
add [Reasoner]
Add a clause to the DB, and propagate.
add_fact [Prover]
add_fact [Reasoner]
Add a fact to the DB.
add_fo_clause [Prover]
Add a first-order clause (as "holds" predicate)
axiom [Plugin]
axioms present in the problem (name of axiom+type args+argument)

C
clause_of_foclause [Encoding]
Convert back to a list of formulas
clause_prop [Encoding]
compose [Encoding]
Compose two encodings together
currying [Encoding]

E
empty [Prover]
Fresh meta-prover (using default plugins' signature)
empty [Plugin.Set]
empty [Reasoner]
Empty DB

F
fact [Reasoner.Clause]
fact t is a shortcut for rule t []
facts [Plugin]
Iterate on values that belong to the given plugin and are currently facts in the reasoner
facts [Reasoner.Seq]
facts [Reasoner.Proof]
Iterate on the facts that have been used
fmap_clause [Encoding]
fmap_lit [Encoding]
foclause_of_clause [Encoding]

H
holds [Plugin]
holds: statement about which First-Order clause is true in the current problem

I
id [Encoding]
Identity encoding
is_fact [Reasoner.Clause]

L
lemma [Plugin]
Lemma: similar to Plugin.holds, but explicitely used for facts deduced by the meta-prover.

O
of_consequence [Plugin]
Try to extract a value from a consequence
of_consequences [Plugin]
of_ho_ast [Prover]
Add the given declarations to the meta-prover.
of_seq [Prover.Seq]
of_seq [Reasoner.Seq]

P
parse_file [Prover]
Attempt to parse file using Libzipperposition_parsers.Parse_ho and add the parsed content to the prover
pp_clause [Encoding]
Printer of clauses
pre_rewrite [Plugin]
Encodes a rewriting system used for pre-processing a set of clauses, into a meta-property.
property_id [Reasoner]
property_ty [Reasoner]
Type of meta-level statements.

R
reasoner [Prover]
The inner reasoner, holding a set of clauses and facts
rewrite [Plugin]
Encodes a set of first-order rewrite rules into a meta-property.
rule [Reasoner.Clause]
Build a rule.
rules [Reasoner.Proof]
Iterate on the rules that have been used

S
set [Plugin.Base]
The set of default plugins
signature [Prover]
Current signature
signature [Plugin.Base]
signature [Plugin.Set]

T
terms [Reasoner.Clause.Seq]
theory [Plugin]
theories that are present in the problem (name of theory +type args +argument)
to_seq [Prover.Seq]
to_seq [Reasoner.Seq]
Only iterate on axioms

V
vars [Reasoner.Clause.Seq]