feature: define a combinatory binary language

[FreeYourSoul]

A programming structure representing a combinatory logic language (maybe that could be serialised in the future)

This combinatory logic language will be converted into a CNF representation (sat solver binary clauses) via Tseytin transformation.

Before storing those clause in the sat. We can implement optimization (logic redundancy, etc... See paper of minisat about logic synthesis)

[FreeYourSoul]

Make a new langage from scratch ?

[H4E]

Language should express:

• TODO

  Language should permit:

• compact serialization

• TODO

[FreeYourSoul]

The language skills be under the form of a c++ library for now

[FreeYourSoul]

C v ((A ^ B) v e(D v E)

Will convert to

X¹ = A ^ B
X² = D v E
X³ = e(X²)
X⁴ = X¹ v X³
R = C v X⁴
R

R being the result gate that would enforce truthfulness of the operation.

• then (or before) a proper execution of custom implementation to details them (existence e for example)

• then a tseitin transformation should be applied

[FreeYourSoul]

Creation of the concept of set (that could be extended into matrix with span of the set)

auto s = set(4);

// Add constraint on the first to third variable of the set. One has to be A, the rest can be either B C or D
s[0, 2].and_cstrnt("A").or_cstrnt("B", "C", "D");

// Add constraint on the 4th variable of the set. It has to be D
s[3].and_constraint("D");

[] Operates on variable(s)

This is a representation that provides an unknown number of variables in the cnf. The "position" of those variable in the set is what add value to set.

It will be needed to generate variable automatically out of a condition (via Tseytin transformation)