The current Expression methodology is to have dual kinds for Zero/One and Complement/Variable, but to actually add a separate Not operator to negate all other operators. For example, to negate an Or operator, you would construct this expression: Not(Or(...)).
Unfortunately, adding a separate graph node for each Not operator bloats the size of the graph. I'm sure there's a theoretical way to describe this, but I'm guessing the data structure will tend to be about 30%-50% bigger than it needs to be.
The solution is to get rid of Not operators altogether, and just make negation a part of the expression kind encoding. So for every Or operator, there will now be a dual Nor operator kind, And/Nand, and so on.
My proposal for a new encoding:
Name
4
3
2
1
0
hex
zero
0
0
0
0
0
0x0
one
0
0
0
0
1
0x1
comp
0
1
0
0
0
0x8
var
0
1
0
0
1
0x9
nor
1
0
0
0
0
0x10
or
1
0
0
0
1
0x11
nand
1
0
0
1
0
0x12
and
1
0
0
1
1
0x13
xnor
1
0
1
0
0
0x14
xor
1
0
1
0
1
0x15
neq
1
0
1
1
0
0x16
eq
1
0
1
1
1
0x17
nimpl
1
1
0
0
0
0x18
impl
1
1
0
0
1
0x19
nite
1
1
0
1
0
0x1A
ite
1
1
0
1
1
0x1B
Observations:
Bit 4 tells you whether the node is an atom or operator
Bit 0 tells you whether the node is negated
Constants start with 00, literals start with 01
Nary operators start with 10, fixed operators start with 11
A couple encodings left over for future enhancement, such as Majority-3
cjdrake
commented
7 years ago
The current
Expressionmethodology is to have dual kinds forZero/OneandComplement/Variable, but to actually add a separateNotoperator to negate all other operators. For example, to negate anOroperator, you would construct this expression:Not(Or(...)).Unfortunately, adding a separate graph node for each
Notoperator bloats the size of the graph. I'm sure there's a theoretical way to describe this, but I'm guessing the data structure will tend to be about 30%-50% bigger than it needs to be.The solution is to get rid of
Notoperators altogether, and just make negation a part of the expression kind encoding. So for everyOroperator, there will now be a dualNoroperator kind,And/Nand, and so on.My proposal for a new encoding:
Observations: