\myheading{Referential transparency}

\leveldown{}

This is important -- a variable can be assigned only once.
Like in Verilog/VHDL, Haskell.

Like in \ac{SSA}:

\begin{framed}
\begin{quotation}
One important property that holds for all varieties of SSA, including the simplest definition above,
is referential transparency: i.e., since there is only a single
definition for each variable in the program text, a variable’s value is independent
of its position in the program.
\end{quotation}
\end{framed}
( \href{http://ssabook.gforge.inria.fr/latest/book.pdf}{Static Single Assignment Book} )

This is like immutability.

Hence, the order of variable assignments doesn't matter at all.
You see, how I do this in my MK85 toy solver: \ref{MK85_adder} (\verb|add_FA()| function).

Hence, an expression like $x=x+1$ wouldn't work.
How can you synthesize it?

\iffalse
\begin{lstlisting}
+-------+      +-------+
|const 1| ---> |       |
+-------+      | adder | ---+---> x
     x ---+--> |       |    |
          |    +-------+    |
          +-----------------+
\end{lstlisting}
\fi

\begin{figure}[H]
\centering
\includesvg[width=0.3\textwidth]{\CURPATH/5.svg}
\end{figure}

You see, such a digital circuit would be senseless.

However, you still can feed this expression to my MK85 toy solver (which is dumb enough to process such an expression)
and a circuit like this would be synthesized, but the result would be UNSAT. 

\myheading{Optimization}

All this can help in optimization.

For example, in my \verb|SAT_lib.py| Python library I'm using across this book in SAT examples,
each gate generated only once for the specific inputs:

\begin{lstlisting}[style=custompy]
    def AND(self, v1:int, v2:int) -> int:
        if (v1, v2) in self.AND_already_generated:
            return self.AND_already_generated[(v1,v2)]

        out=self.create_var()
        self.AND_Tseitin(v1, v2, out)

        self.AND_already_generated[(v1,v2)]=out
        return out
\end{lstlisting}

You can use \textit{cache} or \textit{memoization} words here.

In my toy MK85 SMT solver I'm going further: I cache expressions as strings.
Maybe this is a crude hack, but it works:

\begin{lstlisting}[style=customc]
struct ctx
{
...
        std::unordered_map<std::string, struct SMT_var*> gen_cache;
};

...

struct SMT_var* gen(struct ctx* ctx, struct expr* e)
{
...
	std::string tmp=cpp_expr_to_string(e);
	auto tmp2=ctx->gen_cache.find(tmp);

	if (tmp2!=ctx->gen_cache.end())
	{
		if (verbose)
			printf ("found this expression in gen_cache\n");
		return tmp2->second;
	}
	else
	{
		if (verbose)
			printf ("not found this expression in gen_cache\n");
	};

	...

		case EXPR_BINARY:
			if (verbose)
				printf ("%s:%d (after EXPR_BINARY) end\n", __FUNCTION__, __LINE__);
			rt=gen_binary(ctx, e);
			rt->e=e;
			ctx->gen_cache[tmp]=rt;
			return rt;
...
\end{lstlisting}

This is like \textit{common subexpression elimination}.
It would be way harder doing it in Algol-like programming languages.

I added this optimization to MK85 when it failed to generate the \textit{bit reverse} function
(\ref{bitrev}) -- because the expression \textit{explode} on each iteration drastically.

\levelup{}