(>>>) [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] |