The method Logic::printTerm computes string representation of a term by
recursively computing string representation of its arguments. This is
not efficient in a DAG term when a subterm is reachable on multiple
paths, because such a subterm would be stringified multiple times, one
per each path. Instead, we use our helper method that uses let terms for
conjunctions and disjunctions.
This method could be optimized to introduce let only for subterms
reachable by more than one path, but we leave that as future work.
The method Logic::printTerm computes string representation of a term by recursively computing string representation of its arguments. This is not efficient in a DAG term when a subterm is reachable on multiple paths, because such a subterm would be stringified multiple times, one per each path. Instead, we use our helper method that uses let terms for conjunctions and disjunctions. This method could be optimized to introduce let only for subterms reachable by more than one path, but we leave that as future work.
Fixes #54.