Plans regarding substitutions for clausesets.
More...
Go to the source code of this file.
Detailed Description
Plans regarding substitutions for clausesets.
 Todo:
 The notion of a "literal substitution":

These are functions with literals as values; the question is whether variables or literals are the basic arguments.

Mathematically, (all) literals (relevant here) seems appropriate.

But programmatically variables seems more appropriate, since so redundancy in the presentation is avoided.

Perhaps it's best to view substitutions as homomorphisms, and then we can specify a literal by an arbitrary mapping on a "free" set of literals, for example, a set of variables; in general a (finite) free sets of literals is just a clause.

But perhaps this complication is not worth the effort.

On a set V of variables: each variable v in V > literal f(v); more general, instead of V we have a clause.

We need then a standard wrapper which extends it to the literals: if the input is a negative literal, return f(v). This is more expensive if we originally defined the substitution on an arbitrary clause.

Applying a literal substitution f to a clause C is possible iff C is contained in the domain of f, and then yields f(C) = {f(x) : x in C}.

Applying a literal substitution f to a clauseset F is possible iff f is applicable to all C in F, and the result then is f(F) = {f(C) : C in F}.

A "varsubstitution" is a literal substitution which doesn't flip signs, i.e., for a variable v in the domain of f also f(v) is a variable.

A "signsubstitution" is a literal substitution which doesn't change underlying variables, i.e., for x in the domain of f we have var(f(x)) = var(x).

A problem is that substitution are not generally applicable to arbitrary literals.

One could extend them, using that "false" or "0" is not a literal.

We could use (additionally) "elsub" etc. for these extended versions? <li Or should we only use the extended versions? No, it is unnatural to assume all maps are global.

But these extended versions should know about their domains?

Perhaps these extended substitutions are pairs [V,f], where V is the variabledomain.

Not necessarily: the most natural case for an extended substitution is given by a hashmap, where the domain is extractable, but where it would be unnatural to additionally carry it around.

So an "extended substitution" in difference to a "normal
substitution" can be applied to arbitrary literals, acting identical for literals not in their domain, but the domain is only implicite.

Abbreviations:

"lsub" for "literalsubstitution".

"vsub" for "variablesubstitution".

"ssub" for "signsubstitution".

These only operate on variables. Extended to literals, clauses, clausesets, we could use the prefixes used for them, perhaps with an underscore.

So for example "fcs_lsub".

Given a basic literalsubstitution, it needs to be extended to literals:

Since it's just a case distinction, it seems just a trivial lambdawrapper is appropriate.


So alltogether, we have lsub,vsub,ssub for the behaviour of the substitutions, and v_xsub, l_xsub, c_xsub, cs_xsub etc. for their extensions. There are basic tools for creating v_xsub objects, and tools to extend v_xsub. These tools can create global l_xsub objects, but this is not the responsibility of the substitution, but only of the user.
 Todo:
 standardise_fcs

Perhaps, once a framework for literalsubstitutions is in place, then the renamingfunctions are updated using these more general substitutionmaps instead of hashmaps.

Ask on maximamailinglist whether a parallel substitution is available (this should speed up renaming).

DONE The current implementation (using iterated substitution) is incorrect in case the clauseset uses already natural numbers as variables.

DONE Otherwise, investigate how hashmaps can be made available, store the (whole) substitution via a hashmap, and compute the new clauseset via transforming clause for clause.

DONE (we can now rename w.r.t. a given list of variables) Perhaps we could establish general renaming functionality.
Definition in file Substitutions.hpp.