Closed riccardodebenedictis closed 5 years ago
this number of variable saving, probably, cannot be done
consider the following example: we want to introduce the constraint x∨y this should result in the introduction of the constraint ν⇒x∨y which is different from ν=x∨y as it would result from using the controllable operators introduced in commit 14f7fdb13c15bc6e8280e7eaf9ab7913294135b8
in other words, the implied term should be free to become true
without affecting the implying term.
Check the execution of the expression statements. Asserting facts could be refactored, exploiting the ν variable and the controllable operators introduced in commit 14f7fdb13c15bc6e8280e7eaf9ab7913294135b8, so as to save the number of propositional variables.