|
Connect++ 0.1
A fast, readable connection prover for first-order logic.
|
General representation of terms. More...
#include <Term.hpp>
Public Member Functions | |
| Variable * | get_v () const |
| Self-explanatory access function. | |
| Function * | get_f () const |
| Self-explanatory access function. | |
| bool | is_variable () const |
| Self-explanatory. | |
| bool | is_function () const |
| Self-explanatory. | |
| Arity | arity () const |
| Self-explanatory access function. | |
| Term * | operator[] (size_t) const |
| Access to args, but don't mess with them! | |
| string | to_string (bool=false, bool=false) const |
| Make a string representation of the Term, taking into account any substitutions that have been made. | |
| string | to_prolog_string () const |
| Convert to a string that can be read by Prolog. | |
| string | make_LaTeX (bool=false) const |
| Make a useable LaTeX representation. | |
| bool | operator== (const Term &) const |
| For the TermIndex you want strict equaliity of the data members. | |
| bool | is_subbed () const |
| Test whether any variable has been substituted. | |
| bool | subbed_equal (Term *) const |
| Equality test, taking substitution into account. | |
| bool | is_unsubbed_variable () const |
| Is this a variable that hasn't been substituted? | |
| bool | subbed_is_function () const |
| Is this term a function, taking substitution into accoumt? | |
| bool | subbed_is_variable () const |
| Is this term a variable, taking substitution into accoumt? | |
| bool | contains_variable (Variable *) const |
| Taking substitution into account, does the term include the variable passed? | |
| Variable * | subbed_variable () const |
| Taking substitution into account, what variable do we actually have? | |
| Function * | get_subbed_f () const |
| Taking substitution into account, what function do we actually have? | |
| Arity | get_subbed_arity () const |
| Taking substitution into account, what arity do we actually have? | |
| Term * | skip_leading_variables () const |
| It may be that there is a chain of substitutions attached to a variable. | |
| void | find_subbed_vars (set< Variable * > &) const |
| Taking substitution into account, find all the variables in a term. | |
| Term * | make_copy_with_new_vars (VariableIndex &, TermIndex &) const |
| Does as the name suggests. | |
| Term * | make_copy_with_new_vars_helper (VariableIndex &, TermIndex &, unordered_map< Variable *, Term * > &) const |
| Main implementation of make_copy_with_new_vars. | |
Friends | |
| class | TermIndex |
| ostream & | operator<< (ostream &, const Term &) |
General representation of terms.
Terms can be variables or function-based. This requires care, because after you substitute the former for the latter, it effectively becomes the latter. Similarly, function-based terms are altered by substitution. If a method has "subbed" in the name it means substitutions will be taken into account.
And, yes, the OO mob want to do this with inheritance, but I don't because ultimately I want hash consing, and inheritance would stuff that up BIG TIME!
| bool Term::contains_variable | ( | Variable * | v2 | ) | const |
Taking substitution into account, does the term include the variable passed?
Note that this acts on the eventual term, so if you look for something that has itself been subbed then the answer is "no".
| void Term::find_subbed_vars | ( | set< Variable * > & | vs | ) | const |
Taking substitution into account, find all the variables in a term.
Does not clear the parameter – you may be adding to it across a bunch of terms.
|
inline |
Self-explanatory access function.
Everything you do with these should really be done via pointers, so disallow copying where you can because that would mean you're doing something wrong.
As usual, let the compiler help detect any errors.
Unfortunately it turns out that if you want to use unordered_map to hash cons Terms then you do in fact need these.
| Term * Term::make_copy_with_new_vars | ( | VariableIndex & | vi, |
| TermIndex & | ti | ||
| ) | const |
Does as the name suggests.
Not straightforward! See documentation for make_copy_with_new_vars_helper
Implementation is in TermIndex.cpp
| vi | Reference to the VariableIndex |
| ti | Reference to the TermIndex |
| Term * Term::make_copy_with_new_vars_helper | ( | VariableIndex & | vi, |
| TermIndex & | ti, | ||
| unordered_map< Variable *, Term * > & | v_map | ||
| ) | const |
Main implementation of make_copy_with_new_vars.
Requires care. You need to build this so that the hash consing is maintained.
In general you might also need to account for substituted variables. This method removes them entirely, so you end up with a term whose only variables are new, and which are also leaves.
This needs to be maintained because the TermIndex should only ever have unsubstituted terms added. (In fact at present TermIndex doesn't make any distinction.)
It may be necessary at some point to add something that also replaces subbed variables with new ones, and additionally updates the current substitution so that they are subbed to the newly constructed terms. However, for Connection Calculus, this method is only needed with stuff in the matrix, and as variables are never directly substituted for things in the matrix the issue never arises.
Implementation is in TermIndex.cpp
| vi | Reference to the VariableIndex |
| ti | Reference to the TermIndex |
| v_map | Reference to an unordered_map from pointers to Variables, to pointers to Terms. Initially empty. On completion contains a map from variables, to the terms corresponding to the new variables made to replace them. |
| string Term::make_LaTeX | ( | bool | subbed = false | ) | const |
Make a useable LaTeX representation.
Assumes you are in Math mode.
| subbed | Implement substitutions if true |
| bool Term::operator== | ( | const Term & | t | ) | const |
For the TermIndex you want strict equaliity of the data members.
This will not take substitutions into account.
| Term * Term::operator[] | ( | size_t | i | ) | const |
Access to args, but don't mess with them!
Do you really need to use this? Be careful as the parameter isn't checked.
| i | Index of the argument you want. |
| Term * Term::skip_leading_variables | ( | ) | const |
It may be that there is a chain of substitutions attached to a variable.
When doing unification we actually want a pointer either to the final variable in a chain or to the first term that's a function. This returns it.
| bool Term::subbed_equal | ( | Term * | t | ) | const |
Equality test, taking substitution into account.
For unification you have to take substitution into account, so this needs different treatment to operator==.
| string Term::to_prolog_string | ( | ) | const |
Convert to a string that can be read by Prolog.
Does not apply substitutions.
| string Term::to_string | ( | bool | subbed = false, |
| bool | show_addresses = false |
||
| ) | const |
1.9.7