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