search

Robbepop / stevia

A simple (unfinished) SMT solver for QF_ABV.
Other
36 stars 5 forks source link

Add Nand, Nor and Xnor #7

Open Robbepop opened 6 years ago

Robbepop commented 6 years ago

Stevia could profit by implementing or at least providing Nand, Nor and Xnor in addition to And, Or and Xor that currently exist. This could make some simplifications involving negation simpler or at least more performant temporarily.

These additional expression types could be implemented on several different layers.

  1. Factory-layer: Only provided by the expression build interface that internally directly forwards to And, Or and Xor. The downside is that this is quite intransparent to users that might be confused why no actual negated versions are created.
  2. In the expression AST. The advantage is that it is transparent, the downside is that it is a lot of repetition and requires another set of simplification rules for them. They could be simply directly reduced to their non-negated counterparts upon simplification without other simplifications occuring.
Robbepop commented 5 years ago

Question: Do we actually need those?