|
Connect++ 0.1
A fast, readable connection prover for first-order logic.
|
Basic representation of variables. More...
#include <Variable.hpp>
Public Member Functions | |
| Variable (const Variable &)=delete | |
| Explicitly disallow copying as this is a very bad idea. | |
| Variable (const Variable &&)=delete | |
| Variable & | operator= (const Variable &)=delete |
| Variable & | operator= (const Variable &&)=delete |
| ID | get_id () const |
| Self-explanatory access function. | |
| string | get_name () const |
| Self-explanatory access function. | |
| string | to_string (bool=false) const |
| Convert to a (coloured) string. | |
| bool | is_subbed () const |
| Self-explanatory. | |
| Term * | get_subbed_term () const |
| Self-explanatory. | |
| void | remove_substitution () |
| Self-explanatory, but be careful! | |
| void | substitute (Term *t) |
| Self-explanatory, but be careful! | |
| bool | subbed_is_function () const |
| Is the variable now a function, taking substitution into account? | |
| bool | subbed_is_variable () const |
| Is the variable still in fact a variable, taking substitution into account? | |
| Variable * | subbed_variable () const |
| If the variable is unsubbed then return "this"; otherwise a pointer to the variable at the end of a chain of substitutions of variables for variables. | |
| bool | contains_variable (Variable *) const |
| Does the substitution turn the variable into something that includes the variable passed? | |
| Function * | get_subbed_f () const |
| If there is a chain of substitutions ending in a function, find that function. | |
| Arity | get_subbed_arity () const |
| If there is a chain of substitutions ending in a function, find that function's arity. | |
| Term * | skip_leading_variables () const |
| It may be that there is a chain of substitutions attached to this variable: skip the leading ones. | |
| string | make_LaTeX (bool=false) const |
| Convert the Variable to a useable LaTeX representation. | |
Friends | |
| class | VariableIndex |
| ostream & | operator<< (ostream &, const Variable &) |
| Some methods are in Term.cpp to make the dependencies work. | |
Basic representation of variables.
This way of treating variables makes substitution and the removal thereof extremely easy. BUT, you have to be somewhat careful, because once substituted you may no longer have a variable.
A Variable has an id and a namem Substitution is by way of setting the substitution pointer from nullptr to the address of a Term.
Some of the implementation is in Term.cpp in order to allow the compiler to do things in the right order.
You should never try to construct one of these yourself. Only do it by way of the VariableIndex.
|
delete |
Explicitly disallow copying as this is a very bad idea.
You should never have to do this, and by explicitly disallowing it we help the compiler to find our errors for us.
| bool Variable::contains_variable | ( | Variable * | v2 | ) | const |
Does the substitution turn the variable into something that includes 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".
| v2 | Pointer to Variable to search for. |
|
inline |
Self-explanatory access function.
Only return the variable name – do not follow substitutions.
| string Variable::make_LaTeX | ( | bool | subbed = false | ) | const |
Convert the Variable to a useable LaTeX representation.
Note that this makes a limited attempt to deal with all situations. Anonymous variables will work fine, but if your named variables have symbols that need an escape or similar it may not work as expected.
Assumes that the output will be typeset in math mode. Parameter implements substitutions if true.
| subbed | Include effect of substitution if true. |
|
inline |
Self-explanatory, but be careful!
As long as your Term* pointers are only generated buy the TermIndex, then you don't have to worry about memory allocation or de-allocation.
If you did a "new Term" anywhere yourself then you must live with the consequences.
| Term * Variable::skip_leading_variables | ( | ) | const |
It may be that there is a chain of substitutions attached to this variable: skip the leading ones.
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 Variable::subbed_is_function | ( | ) | const |
Is the variable now a function, taking substitution into account?
Note that this it false if the variable is unsubstituted.
| bool Variable::subbed_is_variable | ( | ) | const |
Is the variable still in fact a variable, taking substitution into account?
Note that this it true if the variable is unsubstituted.
| Variable * Variable::subbed_variable | ( | ) | const |
If the variable is unsubbed then return "this"; otherwise a pointer to the variable at the end of a chain of substitutions of variables for variables.
You should probably only call this if you know the substitution is a chain of variables. (Otherwise you're getting a nullptr and an error message.)
|
inline |
Self-explanatory, but be careful!
As long as your Term* pointers are only generated buy the TermIndex, then you don't have to worry about memory allocation or de-allocation.
If you did a "new Term" anywhere yourself then you must live with the consequences.
| t | Pointer to Term to substitute. |
| string Variable::to_string | ( | bool | subbed = false | ) | const |
Convert to a (coloured) string.
| subbed | Include effect of substitution if true. |
|
friend |
Some methods are in Term.cpp to make the dependencies work.
What?!! Where is everything?!! The file you need is Term.cpp. This is mainly for debugging. If you want actual representations then use Variable::to_string or similar.
1.9.7