Returns the dual rail encoded variable.
Generates dual-rail variables for a list of literals (allows to control which indices ranges will be occupied by dual rail lits).
Generates dual-rail variables for a list of literals (allows to control which indices ranges will be occupied by dual rail lits). Must be called before encode() to guarantee intended control over the dual-rail literal indices. Literals not encoded a priori using this method will be enoded on the fly as discovered during the clause-level processing of encode().
the list of literals to encode
the list of dual-rail literals resulting from the translation
Return both dual-rail encoded literals in (l_x, l_not_x).
Returns the current translation cache as an immutable map.
Encodes source formula to target formula using dual-rail encoding.
Encodes source formula to target formula using dual-rail encoding.
Literals not encoded a priori using the apply(List[Int]) will be encoded on the fly as discovered during clause traversal, and hence no guarantees can be given about the index range they will occupy nor on their ordering.
Returns the current translation cache as an immutable map.
Returns ifPos if selector > 0 and isNeg otherwise.
Given a literal, returns a pair (pos, neg) where: - pos is the positive version of the literal.
Given a literal, returns a pair (pos, neg) where: - pos is the positive version of the literal. - neg the negative version of the literal.
Implements the dual-rail transformation at clause level. Does not split variables that are frozen in the source formula, and freezes them in the target formula.