Plans regarding the basic notions of "conditions" and "constraints".
More...
Go to the source code of this file.
Detailed Description
Plans regarding the basic notions of "conditions" and "constraints".
 Todo:
 Connections
 Todo:
 0,1 versus false,true

Shall a condition return 0,1 or false,true ?
 Todo:
 Notions, names and abbreviations

"cdn" for "condition".

"cst" for "constraint".

The notion of "constraint"

Are positional arguments underlying the evaluation function, or named arguments, i.e., variables? That is, is a solution presented by a tuple or by a clause?

I (OK) regard it as an innovation and improvement to use clauses (in the various forms).

But then, since constraints are then nothing else then formal clausesets (in their various forms), perhaps we should drop the notion?

We can not just speak of "clausesets", but must qualify them as CNF or DNF.

Perhaps we should just use "constraint" for a full formal clauseset in DNFinterpretation, and in general we speak of CNF/DNF formal clausesets?

Or we use "constraint" really when using sets of tuples of values and an ordered domain of variables? As a kind of (slighly) compressed representation of formal clausesets?

What about active literals, active clauses and active clausesets? Likely these are refinements which speak about the various interfaces.

Falsifying versus satisfying assignments in a constraint

We could speak of "negative" versus "positive" constraints, or of "CNF" versus "DNF" constraints, or just of CNF and DNFclausesets.
 Todo:
 snbl2cdn

See "Creating functionterms via lambda", especially "How to simplify
the function term?", for the general discussion of how to simplify the lambdafunction in case the sign is a concrete value.

For variables and values we can not distinguish between "concrete
instances" and metavariables, since they are just arbitrary terms (if not standardised), however a sign is either 1 or +1, and so here we can allow (or not) metavariables, e.g., [1,2,x].

When allowing metavariables, the question then is what do we assume on their evaluation (for the created lambdafunction)? If the evaluation neither determines +1 or 1, should we then just return the unevaluated term (itself), or shall we return "unknown" (as we do now)?

The is(x=y)test used returns false if equality can not be established, and accordingly we have then is(x::y)=true in such cases, where actually "unknown" would perhaps be more appropriate.

This could be repaired by using "is(equal(x,y))" instead of "is(x=y)", since the former uses a "full" evaluation, while the latter "approximates" syntactical equality by only performing "simple" evaluations.

The default for the Maximavariable "prederror" is false, and setting it to true does not change anything here when using "=", but when using "equal" then an error would be triggered.

The current general understanding in the Maximapart of the OKlibrary is that "variables, literals" etc. are simple syntactical objects, and we should not assume that we can make them variable in sophisticated ways. But nevertheless, by using "is(x=y)" in this context we treat positive literals rather different from negative literals (for undetermined values)? But this might be justified, since positive literals in "most" cases are false, while negative literals in "most" cases are true.
Definition in file Conditions.hpp.